idp_engine.Parse

Classes to parse an IDP-Z3 theory.

class idp_engine.Parse.IDP(**kwargs)

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing an IDP-Z3 program.

execute()

Execute the IDP program

class idp_engine.Parse.Vocabulary(**kwargs)

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing a vocabulary block.

add_voc_to_block(block)

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

Parameters

block (Problem) – the block to be updated

class idp_engine.Parse.Annotations(**kwargs)

Bases: idp_engine.Expression.ASTNode

class idp_engine.Parse.Extern(**kwargs)

Bases: idp_engine.Expression.ASTNode

class idp_engine.Parse.ConstructedTypeDeclaration(**kwargs)

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) – Boolean Symbol

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

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

• interpretation (SymbolInterpretation) – the symbol interpretation

• translated (Z3) – the translation of the type in Z3

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

class idp_engine.Parse.RangeDeclaration(**kwargs)

Bases: idp_engine.Expression.ASTNode

class idp_engine.Parse.SymbolDeclaration(**kwargs)

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 beind 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

domain

the list of possible tuples of arguments

Type

List

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]

unit

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

Type

str

heading

the heading that the symbol should belong to

Type

str

class idp_engine.Parse.Symbol(**kwargs)

Bases: idp_engine.Expression.Expression

as_rigid()

returns a Number or Constructor, or None

class idp_engine.Parse.Theory(**kwargs)

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing a theory block.

class idp_engine.Parse.Definition(**kwargs)

Bases: idp_engine.Expression.ASTNode

class idp_engine.Parse.Rule(**kwargs)

Bases: idp_engine.Expression.ASTNode

rename_args(new_vars)

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

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 (Problem) – the context for the interpretation

Returns

a boolean expression

Return type

Expression

interpret(theory)

expand quantifiers and interpret

class idp_engine.Parse.Structure(**kwargs)

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing an structure block.

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 idp_engine.Parse.Enumeration(**kwargs)

Bases: idp_engine.Expression.ASTNode

contains(args, function, arity=None, rank=0, tuples=None)

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

class idp_engine.Parse.Tuple(**kwargs)

Bases: idp_engine.Expression.ASTNode

class idp_engine.Parse.Display(**kwargs)

Bases: idp_engine.Expression.ASTNode

class idp_engine.Parse.Procedure(**kwargs)

Bases: idp_engine.Expression.ASTNode