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.

Parameters
  • code (str) – source code of the IDP program

  • vocabularies (dict[str, Vocabulary]) – list of vocabulary blocks, by name

  • theories (dict[str, Theory]) – list of theory blocks, by name

  • structures (dict[str, Structure]) – list of structure blocks, by name

  • procedures (dict[str, Procedure]) – list of procedure blocks, by name

  • display (Display, Optional) – display block, if any

classmethod from_file(file: str)idp_engine.Parse.IDP[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: str)idp_engine.Parse.IDP[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: str)idp_engine.Parse.IDP[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: List[str])[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, Theory, Structure, Procedure, Display]]

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

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]

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

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

set_level_symbols()[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
get_instantiables(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

interpret(problem)

updates problem.def_constraints, by expanding the definitions

Parameters

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

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

Bases: idp_engine.Expression.ASTNode

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

rename_args(new_vars)

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

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