idp_engine.Parse

Classes to parse an IDP-Z3 theory.

str_to_IDP(atom, val_string)[source]

cast a string value for ‘atom into an Expr object, or None

used to convert Z3 models or json data from GUI

Parameters
  • atom (Expr) – the atom whose value must be converted

  • val_string (str) – the string representation of the value

Returns

the value cast as Expr, or None if unknown

Return type

Expr?

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

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]
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(**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

  • base_type – self

  • 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

__init__(**kwargs)[source]
contains_element(term, interpretations, extensions)[source]

returns an Expression that is TRUE when term is in the type

Parameters
  • term (idp_engine.Expression.Expression) –

  • interpretations (Dict[str, idp_engine.Parse.SymbolInterpretation]) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

Return type

idp_engine.Expression.Expression

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[Symbol]

out

the type of the symbol

Type

Symbol

type

name of the Z3 type of an instance of the symbol

Type

string

base_type

base type of the unary predicate (None otherwise)

Type

TypeDeclaration

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

needs_interpretation

whether its interpretation must be sent to Z3

Type

bool

__init__(**kwargs)[source]
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, idp_engine.Parse.SymbolInterpretation]) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

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 (idp_engine.Expression.Expression) –

  • interpretations (Dict[str, idp_engine.Parse.SymbolInterpretation]) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

Return type

idp_engine.Expression.Expression

contains_element(term, interpretations, extensions)[source]

returns an Expression that is TRUE when term satisfies the predicate

Parameters
  • term (idp_engine.Expression.Expression) –

  • interpretations (Dict[str, idp_engine.Parse.SymbolInterpretation]) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

Return type

idp_engine.Expression.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

Type

__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(**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]
set_level_symbols(voc)[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(interpretations, extensions, 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

  • interpretations (Dict[str, idp_engine.Parse.SymbolInterpretation]) –

  • extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –

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

Bases: idp_engine.Expression.ASTNode

AST node representing <symbol> := { <identifiers*> } else <default>.

name

name of the symbol being enumerated.

Type

string

symbol

symbol being enumerated

Type

Symbol

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

Annotate the symbol.

Parameters

block – a Structure 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 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__(**kwargs)[source]
contains(args, function, arity=None, rank=0, tuples=None, interpretations=None, extensions=None)[source]

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

Parameters
  • interpretations (Optional[Dict[str, idp_engine.Parse.SymbolInterpretation]]) –

  • extensions (Optional[Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]]) –

Return type

idp_engine.Expression.Expression

extensionE(interpretations=None, 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 FunctionEnum(**kwargs)[source]

Bases: idp_engine.Parse.Enumeration

extensionE(interpretations=None, 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(**kwargs)[source]

Bases: idp_engine.Parse.Enumeration

class ConstructedFrom(**kwargs)[source]

Bases: idp_engine.Parse.Enumeration

Represents a ‘constructed from’ enumeration of constructors

tuples

OrderedSet of tuples of Expression

Type

OrderedSet[TupleIDP]

constructors

List of Constructor

Type

List[Constructor]

accessors

index of the accessor in the constructors

Type

Dict[str, Int]

__init__(**kwargs)[source]
contains(args, function, arity=None, rank=0, tuples=None, interpretations=None, extensions=None)[source]

returns True if args belong to the type enumeration

Parameters
  • interpretations (Optional[Dict[str, idp_engine.Parse.SymbolInterpretation]]) –

  • extensions (Optional[Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]]) –

Return type

idp_engine.Expression.Expression

extensionE(interpretations=None, 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 TupleIDP(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]
class FunctionTuple(**kwargs)[source]

Bases: idp_engine.Parse.TupleIDP

__init__(**kwargs)[source]
class CSVTuple(**kwargs)[source]

Bases: idp_engine.Parse.TupleIDP

class Ranges(**kwargs)[source]

Bases: idp_engine.Parse.Enumeration

__init__(**kwargs)[source]
contains(args, function, arity=None, rank=0, tuples=None, interpretations=None, extensions=None)[source]

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

Parameters
  • interpretations (Optional[Dict[str, idp_engine.Parse.SymbolInterpretation]]) –

  • extensions (Optional[Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]]) –

Return type

idp_engine.Expression.Expression

extensionE(interpretations=None, 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 IntRange[source]

Bases: idp_engine.Parse.Ranges

__init__()[source]
extensionE(interpretations=None, 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(interpretations=None, 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(interpretations=None, 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]