idp_engine.Theory

Class to represent a collection of theory and structure blocks.

class Propagation(value)

Describe propagation method

class Theory(*theories, extended=False)

A collection of theory and structure blocks.

assignments (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

Parameters
  • theories (Union[TheoryBlock, Structure, Theory]) –

  • extended (bool) –

Return type

None

EN()

returns a string containing the Theory in controlled English

Return type

str

__init__(*theories, extended=False)

Creates an instance of Theory for the list of theories, e.g., Theory(T,S).

Parameters
  • theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.

  • extended (bool, optional) – use True when the truth value of inequalities and quantified formula is of interest (e.g. for the Interactive Consultant). Defaults to False.

Return type

None

add(*theories)

Adds a list of theories to the theory.

Parameters

theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.

Return type

idp_engine.Theory.Theory

assert_(code, value, status=Status.GIVEN)

asserts that an expression has a value (or not), e.g. theory.assert_("p()", True)

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

Return type

idp_engine.Theory.Theory

constraintz()

list of constraints, co_constraints and definitions in Z3 form

Return type

List[z3.z3.BoolRef]

copy()

Returns an independent copy of a theory.

Return type

idp_engine.Theory.Theory

decision_table(goal_string='', timeout_seconds=20, max_rows=50, first_hit=True, verify=False)

Experimental. Returns the rows for a decision table that defines goal_string.

goal_string must be a predicate application defined in the theory. The theory must be created with extended=True.

Parameters
  • goal_string (str, optional) – the last column of the table.

  • timeout_seconds (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 for goal_string, given self. bool: whether or not the timeout limit was reached.

Return type

list(list(Assignment))

determine_relevance()

Determines the questions that are relevant in a model, or that can appear in a justification of a goal_symbol.

When an irrelevant value is changed in a model M of the theory, the resulting M’ structure is still a model. Relevant questions are those that are not irrelevant.

Call must be made after a propagation, on a Theory created with extended=True. The result is found in the relevant attribute of the assignments in self.assignments.

If goal_symbol has an enumeration in the theory (e.g., goal_symbol := {`tax_amount}.), relevance is computed relative to those goals.

Definitions in the theory are ignored, unless they influence axioms in the theory or goals in goal_symbol.

Returns

the Theory with relevant information in self.assignments.

Return type

Theory

Parameters

self (idp_engine.Theory.Theory) –

disable_law(code)

Disables a law, represented as a code string taken from the output of explain(…).

The law should not result from a structure (e.g., from p:=true.) or from a types (e.g., from T:={1..10} and c: () -> T).

Parameters

code (str) – the code of the law to be disabled

Raises

AssertionError – if code is unknown

Return type

idp_engine.Theory.Theory

enable_law(code)

Enables a law, represented as a code string taken from the output of explain(…).

The law should not result from a structure (e.g., from p:=true.) or from a types (e.g., from T:={1..10} and c: () -> T).

Parameters

code (str) – the code of the law to be enabled

Raises

AssertionError – if code is unknown

Return type

idp_engine.Theory.Theory

expand(max=10, timeout_seconds=10, complete=False)

Generates a list of models of the theory that are expansion of the known assignments.

The result is limited to max models (10 by default), or unlimited if max is 0. The search for new models is stopped when processing exceeds timeout_seconds (in seconds) (unless it is 0). The models can be asked to be complete or partial (i.e., in which “don’t care” terms are not specified).

The string message can be one of the following:

  • No models.

  • No model found in xx seconds.  Models may be available.  Change the timeout_seconds argument to see them.

  • More models may be available.  Change the max argument to see them.

  • More models may be available.  Change the timeout_seconds argument to see them.

  • More models may be available.  Change the max and timeout_seconds arguments to see them.

Parameters
  • max (int, optional) – maximum number of models. Defaults to 10.

  • timeout_seconds (int, optional) – timeout_seconds seconds. Defaults to 10.

  • complete (bool, optional) – True for complete models. Defaults to False.

Yields

the models, followed by a string message

Return type

Iterator[Union[idp_engine.Assignments.Assignments, str]]

explain(consequence=None, timeout_seconds=0)

Returns the facts and laws that make the Theory unsatisfiable, or that explains a consequence. Raises an IDPZ3Error if the Theory is satisfiable

Parameters
  • self (Theory) – the problem state

  • consequence (string, optional) – the code of the consequence to be explained. Must be a key in self.assignments

  • timeout_seconds (int) –

Returns

list of facts and laws that explain the consequence

Return type

(List[Assignment], List[Expression])]

formula()

Returns a Z3 object representing the logic formula equivalent to the theory.

This object can be converted to a string using str().

Return type

z3.z3.BoolRef

get_range(term)

Returns a list of the possible values of the term.

Parameters

term (str) – terms whose possible values are requested, e.g. subtype(). Must be a key in self.assignments

Returns

e.g., ['right triangle', 'regular triangle']

Return type

List[str]

optimize(term, minimize=True)

Updates the value of term in the assignments property of self to the optimal value that is compatible with the theory.

Chain it with a call to expand to obtain a model, or to propagate to propagate the optimal value.

Parameters
  • term (str) – e.g., "Length(1)"

  • minimize (bool) – True to minimize term, False to maximize it

Return type

idp_engine.Theory.Theory

propagate(tag=Status.CONSEQUENCE, method=Propagation.DEFAULT)
Returns the theory with its assignments property updated

with values for all terms and atoms that have the same value in every model of the theory.

self.satisfied is also updated to reflect satisfiability.

Terms and propositions starting with _ are ignored.

Args:

tag (S): the status of propagated assignments method (Propagation): the particular propagation to use

Parameters
  • tag (idp_engine.Assignments.Status) –

  • method (idp_engine.Theory.Propagation) –

Return type

idp_engine.Theory.Theory

simplify()

Returns a simpler copy of the theory, with a simplified formula obtained by substituting terms and atoms by their known values.

Assignments obtained by propagation become UNIVERSAL constraints.

Return type

idp_engine.Theory.Theory

property solver: z3.z3.Solver

Beware that the setting of timeout_seconds (e.g. in expand()) is not thread safe

symbolic_propagate(tag=Status.UNIVERSAL)

Returns the theory with its assignments property updated with direct consequences of the constraints of the theory.

This propagation is less complete than propagate().

Parameters

tag (S) – the status of propagated assignments

Return type

idp_engine.Theory.Theory

to_smt_lib()

Returns an SMT-LIB version of the theory

Return type

str