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:

  • variables containing the vocabularies, theories and structures specified in the same IDP-Z3 program. The variables have the name of the block;

  • the functions exposed by the idp_engine, described here;

  • the Theory class, described here.

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 print sat if theory named T has a model expanding structure named S.

Parameters

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

Returns

sat, unsat or unknown

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 named T expanding structure named S.

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 named S consistent with the theory named T.

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

idp_engine.Theory.Theory

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

idp_engine.Theory.Theory

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]

pretty_print(x='')[source]

Prints its argument on stdout, in a readable form.

Parameters

x (Any, optional) – the result of an API call. Defaults to “”.

Return type

None

duration(msg='')[source]

Returns the processing time since the last call to duration(), or since the begining of execution

Parameters

msg (str) –

Return type

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

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

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.

__init__(**kwargs)[source]
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

IDP

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

IDP

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

IDP

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