idp_engine.Problem

Class to represent a collection of theory and structure blocks.

class idp_engine.Problem.Propagation(value)[source]

Describe propagation method

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

OrderedSet

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

Assignment

definitions

a list of definitions in this problem

Type

[Definition]

def_constraints

A mapping of defined symbol to the whole-domain 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

OrderedSet

propagated

true if a propagation has been done

Type

Bool

assigned

set of questions asserted since last propagate

Type

OrderedSet

cleared

set of questions unassigned since last propagate

Type

OrderedSet

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

classmethod make(theories, structures, extended=False)[source]

polymorphic creation

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

constraintz()[source]

list of constraints, co_constraints and definitions in Z3 form

formula()[source]

the formula encoding the knowledge base

expand(max=10, timeout=10, complete=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>, method=<Propagation.DEFAULT: 1>)[source]

determine all the consequences of the constraints

get_range(term: str)[source]

Returns a list of the possible values of the term.

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 hit-policy. Defaults to True.

  • verify (bool, optional) – request verification of table completeness. Defaults to False

Returns

the non-empty cells of the decision table

Return type

list(list(Assignment))