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

class
idp_engine.Problem.
Problem
(*blocks, extended=False)[source]¶ A collection of theory and structure blocks.

extended
¶ True when the truth value of inequalities and quantified formula is of interest (e.g. in the Interactive Consultant)
 Type
Bool

declarations
¶ the list of type and symbol declarations
 Type
dict[str, Type]

constraints
¶ a set of assertions.
 Type

assignments
¶ the set of assignments. The assignments are updated by the different steps of the problem resolution. Assignments include inequalities and quantified formula when the problem is extended
 Type

definitions
¶ a list of definitions in this problem
 Type

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

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

goals
¶ A set of goal symbols
 Type
dict[string, SymbolDeclaration]

_constraintz
¶ a list of assertions, co_constraints and definitions in Z3 form
 Type
List(ExprRef), Optional

_formula
¶ the Z3 formula that represents the problem (assertions, co_constraints, definitions and assignments).
 Type
ExprRef, optional

co_constraints
¶ the set of co_constraints in the problem.
 Type

propagated
¶ true if a propagation has been done
 Type
Bool

assigned
¶ set of questions asserted since last propagate
 Type

cleared
¶ set of questions unassigned since last propagate
 Type

propagate_success
¶ whether the last propagate call failed or not
 Type
Bool

z3
¶ mapping from string of the code to Z3 expression, to avoid recomputing it
 Type
dict[str, ExprRef]

ctx
¶ Z3 context

assert_
(code: str, value: Any, status: idp_engine.Assignments.Status = <Status.GIVEN: 2>)[source]¶ asserts that an expression has a value (or not)
 Parameters
code (str) – the code of the expression, e.g., “p()”
value (Any) – a Python value, e.g., True
status (Status, Optional) – how the value was obtained. Default: S.GIVEN

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

propagate
(tag=<Status.CONSEQUENCE: 6>, method=<Propagation.DEFAULT: 1>)[source]¶ determine all the consequences of the constraints

explain
(consequence=None)[source]¶ Pre: the problem is UNSAT (under the negation of the consequence if not None)
Returns the facts and laws that make the problem UNSAT.
 Parameters
self (Problem) – the problem state
consequence (string  None) – the code of the sentence to be explained. Must be a key in self.assignments
 Returns
list of facts and laws that explain the consequence
 Return type
(facts, laws) (List[Assignment], List[Expression])]

simplify
()[source]¶ returns a simpler copy of the Problem, using known assignments
Assignments obtained by propagation become fixed 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))
