idp_engine.Parse¶

Classes to parse an IDP-Z3 theory.

class idp_engine.Parse.IDP(**kwargs)[source]¶

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)[source]¶

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing a vocabulary block.

add_voc_to_block(block)[source]¶

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)[source]¶: Bases: idp_engine.Expression.ASTNode

class idp_engine.Parse.Extern(**kwargs)[source]¶: Bases: idp_engine.Expression.ASTNode

class idp_engine.Parse.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
constructors ([Constructor]) – list of constructors in the enumeration
range ([Expression]) – list of expressions of that type
interpretation (SymbolInterpretation) – the symbol interpretation
translated (Z3) – the translation of the type in Z3
map (Dict[string, Expression]) – a mapping from code to Expression in range

class idp_engine.Parse.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 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)[source]¶

Bases: idp_engine.Expression.Expression

Represents a Symbol. Handles synonyms.

name¶

name of the symbol

Type: string

class idp_engine.Parse.Theory(**kwargs)[source]¶

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing a theory block.

class idp_engine.Parse.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

clarks ({Declaration: Transformed Rule}): normalized rule for each defined symbol (used to be Clark completion)

def_vars ({String: {String: Variable}}): Fresh variables for arguments and result

class idp_engine.Parse.Rule(**kwargs)[source]¶

Bases: idp_engine.Expression.ASTNode

rename_args(new_vars)[source]¶: for Clark’s completion input : ‘!v: f(args) <- body(args)’ output: ‘!nv: f(nv) <- nv=args & body(args)’

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 (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)[source]¶

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)[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

contains(args, function, arity=None, rank=0, tuples=None)[source]¶: returns an Expression that says whether Tuple args is in the enumeration

class idp_engine.Parse.Tuple(**kwargs)[source]¶: Bases: idp_engine.Expression.ASTNode

class idp_engine.Parse.Display(**kwargs)[source]¶: Bases: idp_engine.Expression.ASTNode

class idp_engine.Parse.Procedure(**kwargs)[source]¶: Bases: idp_engine.Expression.ASTNode