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

counter

whether this symbol should get a number counter 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]