idp_solver.Problem¶
Class to represent a collection of theory and structure blocks.

class
idp_solver.Problem.
Problem
(*blocks)[source]¶ A collection of theory and structure blocks.

constraints
¶ a set of assertions.
 Type

assignments
¶ the set of assignments. The assignments are updated by the different steps of the problem resolution.
 Type

clark
¶ A mapping of defined symbol to the rule that defines it.
 Type
dict[SymbolDeclaration, Rule]

def_constraints
¶ A mapping of defined symbol to the wholedomain constraint equivalent to its definition.
 Type
dict[SymbolDeclaration], Expression

interpretations
¶ A mapping of enumerated symbols to their interpretation.
 Type
dict[string, SymbolInterpretation]

_formula
¶ the logic formula that represents the problem.
 Type
Expression, optional

questions
¶ the set of questions in the problem. Questions include predicates and functions applied to arguments, comparisons, and variablefree quantified expressions.
 Type

co_constraints
¶ the set of co_constraints in the problem.
 Type

expand
(max=10, complete=False, extended=False)[source]¶ output: a list of Assignments, ending with a string

symbolic_propagate
(tag=<Status.UNIVERSAL: 4>)[source]¶ determine the immediate consequences of the constraints

propagate
(tag=<Status.CONSEQUENCE: 6>, extended=False)[source]¶ determine all the consequences of the constraints

decision_table
(goal_string='', timeout=20, max_rows=50, first_hit=True, verify=False)[source]¶ returns a decision table for goal_string, given self.
 Parameters
goal_string (str, optional) – the last column of the table.
timeout (int, optional) – maximum duration in seconds. Defaults to 20.
max_rows (int, optional) – maximum number of rows. Defaults to 50.
first_hit (bool, optional) – requested hitpolicy. Defaults to True.
verify (bool, optional) – request verification of table completeness. Defaults to False
 Returns
the nonempty cells of the decision table
 Return type
list(list(Assignment))
