IDP-Z3¶
IDP-Z3 is used to perform reasoning on FO[·] knowledge bases. It can be invoked in 3 ways:
via a web interface, called webIDE.
in a shell, using the Command Line Interface of IDP-Z3.
in a Python program: by using classes and functions imported from the
idp_engine
package available on Pypi.
These methods are further described below.
Warning
An FO-dot program is a text file containing only vocabulary, theory and, structure blocks, as described in FO-dot. An IDP program may additionally contain a main() procedure block, with instructions to process the FO-dot program. This procedure block is described later in this chapter.
webIDE¶
The webIDE of IDP-Z3 is accessible online, and can be run locally.
The webIDE allows you to enter an IDP-Z3 program, with FO-dot vocabulary, theory, structure blocks and a main block, and to run it.
Main block¶
The main block consists of python-like statements to be executed by the IDP-Z3 executable or the webIDE, in the context of the knowledge base. Below is an example of a main block.
procedure main() {
pretty_print(Theory(T, S).propagate())
duration("End")
}
Within that block, the following variables, classes and functions are available:
idp_engine
functions¶
The following Python functions can be used to perform computations using FO-dot knowledge bases:
- model_check(*theories)[source]¶
Returns a string stating whether the combination of theories is satisfiable.
For example,
print(model_check(T, S))
will printsat
if theory namedT
has a model expanding structure namedS
.- Parameters
theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.
- Returns
sat
,unsat
orunknown
- Return type
str
- model_expand(*theories, max=10, timeout_seconds=10, complete=False, extended=False, sort=False)[source]¶
Returns a (possibly empty) list of models of the combination of theories, followed by a string message.
For example,
print(model_expand(T, S))
will return (up to) 10 string representations of models of theory namedT
expanding structure namedS
.The string message can be one of the following:
No models.
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
theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.
max (int, optional) – max number of models. Defaults to 10.
timeout_seconds (int, optional) – timeout_seconds seconds. Defaults to 10.
complete (bool, optional) – True to obtain complete structures. Defaults to False.
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.
sort (bool, optional) – True if the models should be in alphabetical order. Defaults to False.
- Yields
str
- Return type
Iterator[str]
- model_propagate(*theories, sort=False)[source]¶
Returns a list of assignments that are true in any model of the combination of theories.
Terms and symbols starting with ‘_’ are ignored.
For example,
print(model_propagate(T, S))
will return the assignments that are true in any expansion of the structure namedS
consistent with the theory namedT
.- Parameters
theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.
sort (bool, optional) – True if the assignments should be in alphabetical order. Defaults to False.
- Yields
str
- Return type
Iterator[str]
- maximize(*theories, term)[source]¶
Returns a model that maximizes term.
- Parameters
theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.
term (str) – a string representing a term
- Yields
str
- Return type
- minimize(*theories, term)[source]¶
Returns a model that minimizes term.
- Parameters
theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.
term (str) – a string representing a term
- Yields
str
- Return type
- decision_table(*theories, goal_string='', timeout_seconds=20, max_rows=50, first_hit=True, verify=False)[source]¶
Experimental. Returns a decision table for goal_string, given the combination of theories.
- Parameters
theories (Union[TheoryBlock, Structure, Theory]) – 1 or more (data) theories.
goal_string (str, optional) – the last column of the table. Must be a predicate application defined in the theory, e.g.
eligible()
.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
- Yields
a textual representation of each rule
- Return type
Iterator[str]
- determine_relevance(*theories)[source]¶
Generates a list of questions that are relevant, or that can appear in a justification of a
goal_symbol
.The questions are preceded with `` ? `` when their answer is unknown.
When an irrelevant value is changed in a model M of the theories, the resulting M’ structure is still a model. Relevant questions are those that are not irrelevant.
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
.- Yields
relevant questions
- Parameters
theories (Union[idp_engine.Parse.TheoryBlock, idp_engine.Parse.Structure, idp_engine.Theory.Theory]) –
- Return type
Iterator[str]
Theory class¶
Instances of the Theory
class represent a collection of theory and structure blocks.
Many operations on Theory instances can be chained, e.g., Theory(T,S).propagate().simplify().formula()
.
The class has the following methods:
- 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 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 therelevant
attribute of the assignments inself.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
- 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()¶
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
- 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
Command Line Interface¶
IDP-Z3 can be run through a Command Line Interface.
If you have downloaded IDP-Z3 from the GitLab repo, you may run the CLI using poetry (see Installation):
poetry run python3 idp-engine.py path/to/file.idp
where path/to/file.idp is the path to the file containing the IDP-Z3 program to be run. This file must contain an FO-dot knowledge base (vocabulary, theory and structure blocks), and a main block.
Alternatively, if you installed it via pip, you can run it with the following command:
idp-engine path/to/file.idp
The usage of the CLI is as follows:
usage: idp-engine.py [-h] [--version] [-o OUTPUT] [--full-formula] [--no-timing] FILE
IDP-Z3
positional arguments:
FILE path to the .idp file
options:
-h, --help show this help message and exit
--version, -v show program's version number and exit
-o OUTPUT, --output OUTPUT
name of the output file
--full-formula show the full formula
--no-timing don't display timing information
Python API¶
The core of the IDP-Z3 software is a Python component available on Pypi. The following code illustrates how to invoke it.
from idp_engine import IDP, Theory, duration
kb = IDP.from_file("path/to/file.idp")
T, S = kb.get_blocks("T, S")
theory = Theory(T, S)
for model in theory.expand():
print(model)
duration("End")
The file path/to/file.idp
must contain an FO-dot knowledge base (with vocabulary, theory and, optionally, structure blocks).
idp_engine
exposes useful functions, as well as the Theory
(described here) and IDP
classes.
IDP class¶
The IDP
class exposes the following methods:
- class IDP(**kwargs)[source]¶
The class of AST nodes representing an IDP-Z3 program.
- classmethod from_file(file)[source]¶
parse an IDP program from file
- Parameters
file (str) – path to the source file
- Returns
the result of parsing the IDP program
- Return type
- classmethod from_str(code)[source]¶
parse an IDP program
- Parameters
code (str) – source code to be parsed
- Returns
the result of parsing the IDP program
- Return type
- classmethod parse(file_or_string)[source]¶
DEPRECATED: parse an IDP program
- Parameters
file_or_string (str) – path to the source file, or the source code itself
- Returns
the result of parsing the IDP program
- Return type
- get_blocks(blocks)[source]¶
returns the AST nodes for the blocks whose names are given
- Parameters
blocks (List[str]) – list of names of the blocks to retrieve
- Returns
list of AST nodes
- Return type
List[Union[Vocabulary, TheoryBlock, Structure, Procedure, Display]]
- execute()¶
Execute the
main()
procedure block in the IDP program- Parameters
self (idp_engine.Parse.IDP) –
- Return type
None