idp_engine.Parse

Classes to parse an IDP-Z3 theory.

class IDP(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

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

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

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

Execute the main() procedure block in the IDP program

Parameters

self (idp_engine.Parse.IDP) –

Return type

None

class Vocabulary(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing a vocabulary block.

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

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

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

class Import(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

class 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

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

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

class 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[Subtype]

out

the type of the symbol

Type

Subtype

type

name of the Z3 type of an instance of the symbol

Type

string

in_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

optimizable

whether this symbol should get optimize buttons in the IC

Type

bool

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

has_in_domain(args)[source]

Returns an expression that says whether the args are in the domain of the symbol.

Parameters

args (List[Expression]) – the list of arguments to be checked, e.g. [1, 2]

Returns

whether (1,2) is in the domain of the symbol

Return type

Expression

has_in_range(value)[source]

Returns an expression that says whether value is in the range of the symbol.

Parameters

value (idp_engine.Expression.Expression) –

Return type

idp_engine.Expression.Expression

class Symbol(**kwargs)[source]

Bases: idp_engine.Expression.Expression

Represents a Symbol. Handles synonyms.

name

name of the symbol

Type

string

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

has_element(term)[source]

Returns an expression that says whether term is in the type denoted by self.

Parameters

term (Expression) – the argument to be checked

Returns

whether term is in the type denoted by self.

Return type

Expression

class TheoryBlock(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

The class of AST nodes representing a theory block.

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

class 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

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

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
  • instantiables (Dict[SymbolDeclaration, list[Expression]]) – the constraints without the quantification

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

  • result (Dict[SymbolDeclaration, Definition, list[Expression]]) – a mapping from (Symbol, Definition) to the list of constraints

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 (Theory) – containts the enumerations for the expansion; is updated with the expanded definitions

class Rule(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

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

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

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

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

class Tuple(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

class Display(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.

run(idp)[source]

apply the display block to the idp theory

class Procedure(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]

Initialize self. See help(type(self)) for accurate signature.