idp_engine.Parse

Classes to parse an IDP-Z3 theory.

class ViewType(value)[source]

Bases: enum.Enum

An enumeration.

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(capture_print=False)

Execute the main() procedure block in the IDP program

Parameters
Return type

Optional[str]

class Vocabulary(parent, name, declarations)[source]

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing a vocabulary block.

Parameters
  • parent (ASTNode) –

  • name (str) –

  • declarations (List[Union[Declaration, VarDeclaration, Import]]) –

__init__(parent, name, declarations)[source]
Parameters
  • parent (idp_engine.Expression.ASTNode) –

  • name (str) –

  • declarations (List[Union[idp_engine.Parse.TypeDeclaration, idp_engine.Parse.SymbolDeclaration, idp_engine.Parse.VarDeclaration, idp_engine.Parse.Import]]) –

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

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]
class TypeDeclaration(parent, name, constructors=None, enumeration=None)[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

  • domains (List[SetName]) – a singleton list with a set having the type’s name

  • codomain (SetName) – the Boolean type

  • 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

  • block (Vocabulary) – the vocabulary block that contains it

  • enumeration (Optional[Enumeration]) –

__init__(parent, name, constructors=None, enumeration=None)[source]
Parameters
  • name (str) –

  • constructors (Optional[List[idp_engine.Expression.Constructor]]) –

  • enumeration (Optional[idp_engine.Parse.Enumeration]) –

contains_element(term, extensions)[source]

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

Parameters
  • term (Expression) –

  • extensions (dict[str, Extension]) –

Return type

Expression

class SymbolDeclaration(parent, annotations, sorts, out, symbols=None, name=None)[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.

Parameters
  • annotations (Optional[Annotations]) –

  • sorts (List[SetName]) –

  • out (SetName) –

  • symbols (Optional[List[str]]) –

  • name (Optional[str]) –

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

[str]

name

the identifier of the symbol, after expansion of the node

Type

string

arity

the number of arguments

Type

int

domains

the types of the arguments

Type

List[SetName]

codomain

the type of the symbol

Type

SetName

symbol_expr

symbol expression of the same name

Type

SymbolExpr, Optional

symbol_expr

a SymbolExpr of the same name

Type

SymbolExpr, Optional

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

block

the vocabulary where it is defined

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

by_z3

True if the symbol is created by z3 (testers and accessors of constructors)

Type

Bool

__init__(parent, annotations, sorts, out, symbols=None, name=None)[source]
Parameters
  • annotations (Optional[idp_engine.Expression.Annotations]) –

  • sorts (List[idp_engine.Expression.SetName]) –

  • out (idp_engine.Expression.SetName) –

  • symbols (Optional[List[str]]) –

  • name (Optional[str]) –

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, 'SymbolInterpretation']) –

  • extensions (dict[str, Extension]) –

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 (Expression) –

  • interpretations (dict[str, 'SymbolInterpretation']) –

  • extensions (dict[str, Extension]) –

Return type

Expression

contains_element(term, extensions)[source]

returns an Expression that is TRUE when term satisfies the predicate

Parameters
  • term (Expression) –

  • extensions (dict[str, Extension]) –

Return type

Expression

class VarDeclaration(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

represents a declaration of variable (IEP 24)

name

name of the variable

Type

str

subtype

type of the variable

Type

SetName

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

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing a theory block.

__init__(**kwargs)[source]
class Definition(parent, annotations, mode, rules)[source]

Bases: idp_engine.Expression.Expression

The class of AST nodes representing an inductive definition.

Parameters

annotations (Optional[Annotations]) –

id

unique identifier for each definition

Type

num

rules

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

Type

[Rule]

renamed

rules with normalized body for each defined symbol, e.g., !x: p(x) <- q(p1_) (quantees and head are unchanged)

Type

dict[Declaration, List[Rule]]

canonicals

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

Type

dict[Declaration, List[Rule]]

clarks

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

Type

dict[Declaration, Transformed Rule]

def_vars

Fresh variables for arguments and result

Type

dict[String, dict[String, Variable]]

inductive

set of SymbolDeclaration with an inductive definition

Type

set[SymbolDeclaration]

cache

cache of instantiation of the definition

Type

dict[SymbolDeclaration, str, Expression]

inst_def_level

depth of recursion during instantiation

Type

int

__init__(parent, annotations, mode, rules)[source]
Parameters

annotations (Optional[idp_engine.Expression.Annotations]) –

get_def_constraints(problem, for_explain=False)

returns the constraints for this definition.

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

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

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

  • self (Definition) –

Returns

a mapping from (SymbolDeclaration, Definition) to the list of constraints

Return type

dict[SymbolDeclaration, Definition, List[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

  • self (Expression) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

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

  • self (idp_engine.Parse.Definition) –

class Rule(parent, annotations, quantees, definiendum, out, body)[source]

Bases: idp_engine.Expression.Expression

Parameters
  • annotations (Annotations) –

  • quantees (List[Quantee]) –

  • definiendum (AppliedSymbol) –

  • out (Expression) –

  • body (Expression) –

__init__(parent, annotations, quantees, definiendum, out, body)[source]
Parameters
  • annotations (idp_engine.Expression.Annotations) –

  • quantees (List[idp_engine.Expression.Quantee]) –

  • definiendum (idp_engine.Expression.AppliedSymbol) –

  • out (idp_engine.Expression.Expression) –

  • body (idp_engine.Expression.Expression) –

instantiate_definition(new_args, theory)

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

  • self (idp_engine.Parse.Rule) –

Returns

a boolean expression

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

  • self (Expression) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

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_block(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 (idp_engine.Parse.IDP) – a Parse.IDP object.

  • self (idp_engine.Expression.ASTNode) –

  • idp

Returns None

Return type

Union[Exception, List[Exceptions]]

class SymbolInterpretation(parent, name, sign, enumeration, default)[source]

Bases: idp_engine.Expression.Expression

AST node representing <symbol> := { <identifiers*> } else <default>.

Parameters
  • name (UnappliedSymbol) –

  • sign (str) –

  • enumeration (Enumeration) –

  • default (Optional[Expression]) –

name

name of the symbol being enumerated.

Type

string

symbol_decl

symbol being enumerated

Type

SymbolDeclaration

enumeration

enumeration.

Type

[Enumeration]

default

default value (for function enumeration).

Type

Expression

is_type_enumeration

True if the enumeration is for a type symbol.

Type

Bool

__init__(parent, name, sign, enumeration, default)[source]
Parameters
  • name (idp_engine.Expression.UnappliedSymbol) –

  • sign (str) –

  • enumeration (idp_engine.Parse.Enumeration) –

  • default (Optional[idp_engine.Expression.Expression]) –

interpret_application(rank, applied, args, tuples=None)[source]

returns an expression equivalent to self.symbol applied to args, simplified by the interpretation of self.symbol.

This is a recursive function.

Example: assume f>>{(1,2)->A, (1, 3)->B, (2,1)->C} and args=[g(1),2)]. The returned expression is: ` if g(1) = 1 then A else if g(1)=2 then f(g(1),2) else f(g(1),2) `

Parameters
  • rank (Int) – iteration number (from 0)

  • applied (AppliedSymbol) – template to create new AppliedSymbol (ex: g(1),a(), before interpretation)

  • args (List(Expression)) – interpreted arguments applied to the symbol (ex: g(1),2)

  • tuples (OrderedSet[TupleIDP], optional) – relevant tuples for this iteration. Initialized with [[1,2,A], [1,3,B], [2,1,C]]

Returns

Grounded interpretation of self.symbol applied to args

Return type

Expression

annotate(voc, q_vars)

Annotate the symbol.

Parameters
  • block – a Structure object

  • self (Expression) –

  • voc (Vocabulary) –

  • q_vars (dict[str, Variable]) –

Returns None

Return type

Annotated

interpret(problem)

expand quantifiers and replace symbols interpreted in the structure by their interpretation

Parameters
  • self (idp_engine.Parse.SymbolInterpretation) – the expression to be interpreted

  • problem (idp_engine.Theory.Theory) – the theory to be applied

  • subs – a dictionary mapping variable names to their value

Returns

the interpreted expression

Return type

Expression

class Enumeration(parent, tuples)[source]

Bases: idp_engine.Expression.Expression

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

Parameters
  • parent (ASTNode) –

  • tuples (List[TupleIDP]) –

tuples

OrderedSet of TupleIDP of Expression

Type

OrderedSet[TupleIDP]

sorted_tuples

a sorted list of tuples

lookup

dictionary from arguments to values

constructors

List of Constructor

Type

List[Constructor], optional

__init__(parent, tuples)[source]
Parameters
  • parent (idp_engine.Expression.ASTNode) –

  • tuples (List[idp_engine.Parse.TupleIDP]) –

contains(args, arity=None, rank=0, tuples=None, theory=None)[source]

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

Parameters
  • arity (Optional[int]) –

  • rank (int) –

  • tuples (Optional[List[TupleIDP]]) –

  • theory (Optional[Theory]) –

Return type

Expression

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

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

  • self (Expression) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

interpret(problem)

expand quantifiers and replace symbols interpreted in the structure by their interpretation

Parameters
  • self (idp_engine.Parse.Enumeration) – the expression to be interpreted

  • problem (idp_engine.Theory.Theory) – the theory to be applied

  • subs – a dictionary mapping variable names to their value

Returns

the interpreted expression

Return type

Expression

class FunctionEnum(parent, tuples)[source]

Bases: idp_engine.Parse.Enumeration

Parameters
  • parent (ASTNode) –

  • tuples (List[TupleIDP]) –

extensionE(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 CSVEnumeration(parent, tuples)[source]

Bases: idp_engine.Parse.Enumeration

Parameters
  • parent (ASTNode) –

  • tuples (List[TupleIDP]) –

class ConstructedFrom(parent, constructed, constructors)[source]

Bases: idp_engine.Parse.Enumeration

Represents a ‘constructed from’ enumeration of constructors

Parameters
  • parent (Optional[ASTNode]) –

  • constructed (str) –

  • constructors (List[Constructor]) –

tuples

OrderedSet of tuples of Expression

Type

OrderedSet[TupleIDP], Optional

constructors

List of Constructor

Type

List[Constructor]

accessors

index of the accessor in the constructors

Type

dict[str, int]

__init__(parent, constructed, constructors)[source]
Parameters
  • parent (Optional[idp_engine.Expression.ASTNode]) –

  • constructed (str) –

  • constructors (List[idp_engine.Expression.Constructor]) –

contains(args, arity=None, rank=0, tuples=None, theory=None)[source]

returns True if args belong to the type enumeration

Parameters
  • arity (Optional[int]) –

  • rank (int) –

  • tuples (Optional[List[TupleIDP]]) –

  • theory (Optional[Theory]) –

Return type

Expression

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

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

  • self (ASTNode) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

interpret(problem)

expand quantifiers and replace symbols interpreted in the structure by their interpretation

Parameters
  • self (idp_engine.Parse.ConstructedFrom) – the expression to be interpreted

  • problem (idp_engine.Theory.Theory) – the theory to be applied

  • subs – a dictionary mapping variable names to their value

Returns

the interpreted expression

Return type

Expression

class TupleIDP(**kwargs)[source]

Bases: idp_engine.Expression.Expression

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

  • self (Expression) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

translate(problem)

Converts the syntax tree to a Z3 expression, with lookup in problem.z3

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

Bases: idp_engine.Parse.TupleIDP

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

Bases: idp_engine.Parse.TupleIDP

class Ranges(parent, **kwargs)[source]

Bases: idp_engine.Parse.Enumeration

Parameters

parent (ASTNode) –

__init__(parent, **kwargs)[source]
Parameters

parent (idp_engine.Expression.ASTNode) –

contains(args, arity=None, rank=0, tuples=None, theory=None)[source]

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

Parameters
  • arity (Optional[int]) –

  • rank (int) –

  • tuples (Optional[List[TupleIDP]]) –

  • theory (Optional[Theory]) –

Return type

Expression

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

Bases: idp_engine.Expression.Expression

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

Bases: idp_engine.Parse.Ranges

__init__()[source]
extensionE(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 RealRange[source]

Bases: idp_engine.Parse.Ranges

__init__()[source]
extensionE(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 DateRange[source]

Bases: idp_engine.Parse.Ranges

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

Bases: idp_engine.Expression.ASTNode

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

Bases: idp_engine.Expression.ASTNode

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

Bases: idp_engine.Expression.ASTNode

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

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]