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
- 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
- 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
- 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 withextended=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
, givenself
. bool: whether or not the timeout limit was reached.- Return type
list(list(Assignment))
- determine_relevance()
Determines the questions that are relevant in a consistent state of Theory
self
.Some definitions: * a consistent state s of theory T is a partial interpretation of vocabulary V of T that can be expanded in a model of T; * a solution S of theory T is a state such that every expansion of solution S is a model of theory T; * a minimal solution for theory T in state s is a solution that expands state s and is not more precise than another solution of theory T; * a symbol is relevant for theory T in state s iff it is interpreted in a minimal solution for theory T in state s.
This method must be called after a call to
propagate
, on a Theory created withextended=True
. The method 1) computes a simplified theory equivalent toself
, 2) collects the relevant questions in that theory. A question is considered relevant if: * it appears in a constraint; * or it is a goal symbol; * or it appears in a co_constraint for a relevant question.The result is found in the
relevant
attribute of the assignments inself.assignments
.- Returns
the Theory with relevant information in
self.assignments
.- Return type
- 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., fromT:={1..10}
andc: () -> T
).- Parameters
code (str) – the code of the law to be disabled
- Raises
AssertionError – if code is unknown
- Return type
- 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., fromT:={1..10}
andc: () -> T
).- Parameters
code (str) – the code of the law to be enabled
- Raises
AssertionError – if code is unknown
- Return type
- 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 ifmax
is 0. The search for new models is stopped when processing exceedstimeout_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 inself.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 minimizeterm
,False
to maximize it
- Return type
- 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
- Returns the theory with its
- simplify(for_relevance=False)
Returns a simpler copy of the theory, with a simplified formula obtained by substituting terms and atoms by their known values.
- Parameters
for_relevance – If true, numeric comparisons with known values are ignored.
- Return type
- 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
- to_smt_lib()
Returns an SMT-LIB version of the theory
- Return type
str