idp_engine.Parse

Classes to parse an IDP-Z3 theory.

class IDP(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

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

class Vocabulary(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing a vocabulary block.

__init__(**kwargs)[source]
add_voc_to_block(block)[source]

adds the enumerations in a vocabulary to a theory or structure block

Parameters

block (Theory) – the block to be updated

class Annotations(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]
class Import(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]
class TypeDeclaration(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

AST node to represent type <symbol> := <enumeration>

Parameters
  • name (string) – name of the type

  • arity (int) – the number of arguments

  • sorts (List[Symbol]) – the types of the arguments

  • out (Symbol) – the Boolean Symbol

  • type (string) – Z3 type of an element of the type; same as name

  • base_type – self

  • constructors ([Constructor]) – list of constructors in the enumeration

  • interpretation (SymbolInterpretation) – the symbol interpretation

  • map (Dict[string, Expression]) – a mapping from code to Expression in range

__init__(**kwargs)[source]
contains_element(term, interpretations, extensions)[source]

returns an Expression that is TRUE when term is in the type

Parameters
  • term (idp_engine.Expression.Expression) –

  • interpretations (Dict[str, idp_engine.Parse.SymbolInterpretation]) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

Return type

idp_engine.Expression.Expression

class SymbolDeclaration(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing an entry in the vocabulary, declaring one or more symbols. Multi-symbols declaration are replaced by single-symbol declarations before the annotate() stage.

annotations

the annotations given by the expert.

annotations[‘reading’] is the annotation giving the intended meaning of the expression (in English).

symbols

the symbols being defined, before expansion

Type

[Symbol]

name

the identifier of the symbol, after expansion of the node

Type

string

arity

the number of arguments

Type

int

sorts

the types of the arguments

Type

List[Symbol]

out

the type of the symbol

Type

Symbol

type

name of the Z3 type of an instance of the symbol

Type

string

base_type

base type of the unary predicate (None otherwise)

Type

TypeDeclaration

instances

a mapping from the code of a symbol applied to a tuple of arguments to its parsed AST

Type

Dict[string, Expression]

range

the list of possible values

Type

List[Expression]

private

True if the symbol name starts with ‘_’ (for use in IC)

Type

Bool

unit

the unit of the symbol, such as m (meters)

Type

str

heading

the heading that the symbol should belong to

Type

str

optimizable

whether this symbol should get optimize buttons in the IC

Type

bool

__init__(**kwargs)[source]
has_in_domain(args, interpretations, extensions)[source]

Returns an expression that is TRUE when args are in the domain of the symbol.

Parameters
  • args (List[Expression]) – the list of arguments to be checked, e.g. [1, 2]

  • interpretations (Dict[str, idp_engine.Parse.SymbolInterpretation]) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

Returns

whether (1,2) is in the domain of the symbol

Return type

Expression

has_in_range(value, interpretations, extensions)[source]

Returns an expression that says whether value is in the range of the symbol.

Parameters
  • value (idp_engine.Expression.Expression) –

  • interpretations (Dict[str, idp_engine.Parse.SymbolInterpretation]) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

Return type

idp_engine.Expression.Expression

contains_element(term, interpretations, extensions)[source]

returns an Expression that is TRUE when term satisfies the predicate

Parameters
  • term (idp_engine.Expression.Expression) –

  • interpretations (Dict[str, idp_engine.Parse.SymbolInterpretation]) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

Return type

idp_engine.Expression.Expression

class Symbol(**kwargs)[source]

Bases: idp_engine.Expression.Expression

Represents a Symbol. Handles synonyms.

name

name of the symbol

Type

string

__init__(**kwargs)[source]
has_element(term, interpretations, extensions)[source]

Returns an expression that says whether term is in the type/predicate denoted by self.

Parameters
  • term (Expression) – the argument to be checked

  • interpretations (Dict[str, SymbolInterpretation]) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

Returns

whether term is in the type denoted by self.

Return type

Expression

annotate(voc, q_vars)

annotate tree after parsing

Resolve names and determine type as well as variables in the expression

Parameters
  • voc (Vocabulary) – the vocabulary

  • q_vars (Dict[str, Variable]) – the quantifier variables that may appear in the expression

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

instantiate(e0, e1, problem=None)

Recursively substitute Variable in e0 by e1 in a copy of self.

Interpret appliedSymbols immediately if grounded (and not occurring in head of definition). Update .variables.

translate(problem, vars={})

Converts the syntax tree to a Z3 expression, using .value and .simpler if present

Parameters
  • problem (Theory) – holds the context for the translation (e.g. a cache of translations).

  • vars (Dict[id, ExprRef], optional) – mapping from Variable’s id to Z3 translation. Filled in by AQuantifier. Defaults to {}.

Returns

Z3 expression

Return type

ExprRef

class TheoryBlock(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing a theory block.

__init__(**kwargs)[source]
class Definition(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing an inductive definition. id (num): unique identifier for each definition

rules ([Rule]):

set of rules for the definition, e.g., !x: p(x) <- q(x)

canonicals (Dict[Declaration, List[Rule]]):

normalized rule for each defined symbol, e.g., !$p!1$: p($p!1$) <- q($p!1$)

instantiables (Dict[Declaration], List[Expression]):

list of instantiable expressions for each symbol, e.g., p($p!1$) <=> q($p!1$)

clarks (Dict[Declaration, Transformed Rule]):

normalized rule for each defined symbol (used to be Clark completion) e.g., !$p!1$: p($p!1$) <=> q($p!1$)

def_vars (Dict[String, Dict[String, Variable]]):

Fresh variables for arguments and result

level_symbols (Dict[SymbolDeclaration, Symbol]):

map of recursively defined symbols to level mapping symbols

cache (Dict[SymbolDeclaration, str, Expression]):

cache of instantiation of the definition

inst_def_level (int): depth of recursion during instantiation

__init__(**kwargs)[source]
set_level_symbols(voc)[source]

Calculates which symbols in the definition are recursively defined, creates a corresponding level mapping symbol, and stores these in self.level_symbols.

add_def_constraints(instantiables, problem, result)

result is updated with the constraints for this definition.

The instantiables (of the definition) are expanded in problem.

Parameters
  • instantiables (Dict[SymbolDeclaration, List[Expression]]) – the constraints without the quantification

  • problem (Theory) – contains the structure for the expansion/interpretation of the constraints

  • result (Dict[SymbolDeclaration, Definition, List[Expression]]) – a mapping from (Symbol, Definition) to the list of constraints

get_instantiables(interpretations, extensions, for_explain=False)

compute Definition.instantiables, with level-mapping if definition is inductive

Uses implications instead of equivalence if for_explain is True

Example: { p() <- q(). p() <- r().} Result when not for_explain: p() <=> q() | r() Result when for_explain : p() <= q(). p() <= r(). p() => (q() | r()).

Parameters
  • for_explain (Bool) – Use implications instead of equivalence, for rule-specific explanations

  • interpretations (Dict[str, idp_engine.Parse.SymbolInterpretation]) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

interpret(problem)

updates problem.def_constraints, by expanding the definitions

Parameters

problem (Theory) – containts the enumerations for the expansion; is updated with the expanded definitions

class Rule(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]
instantiate_definition(new_args, theory)[source]

Create an instance of the definition for new_args, and interpret it for theory.

Parameters
  • new_args ([Expression]) – tuple of arguments to be applied to the defined symbol

  • theory (Theory) – the context for the interpretation

Returns

a boolean expression

Return type

Expression

rename_args(new_vars)

for Clark’s completion input : ‘!v: f(args) <- body(args)’ output: ‘!nv: f(nv) <- nv=args & body(args)’

class Structure(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing an structure block.

__init__(**kwargs)[source]

The textx parser creates the Structure object. All information used in this method directly comes from text.

annotate(idp)

Annotates the structure with the enumerations found in it. Every enumeration is converted into an assignment, which is added to self.assignments.

Parameters

idp – a Parse.IDP object.

Returns None

class Enumeration(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

Represents an enumeration of tuples of expressions. Used for predicates, or types without n-ary constructors.

tuples

OrderedSet of Tuple of Expression

Type

OrderedSet[Tuple]

constructors

List of Constructor

Type

List[Constructor], optional

__init__(**kwargs)[source]
contains(args, function, arity=None, rank=0, tuples=None, interpretations=None, extensions=None)[source]

returns an Expression that says whether Tuple args is in the enumeration

Parameters
  • interpretations (Optional[Dict[str, idp_engine.Parse.SymbolInterpretation]]) –

  • extensions (Optional[Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]]) –

Return type

idp_engine.Expression.Expression

extensionE(interpretations=None, extensions=None)[source]

computes the extension of an enumeration, i.e., a set of tuples and a filter

Parameters
  • interpretations (Dict[str, &quot;SymbolInterpretation&quot;], optional) – _description_. Defaults to None.

  • extensions (Dict[str, Extension], optional) – _description_. Defaults to None.

Returns

_description_

Return type

Extension

class Tuple(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]
class Display(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]
run(idp)[source]

apply the display block to the idp theory

class Procedure(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]