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 (Expression) – the atom whose value must be converted
val_string (str) – the string representation of the value

Returns

the value cast as Expression, or None if unknown

Return type

Expression

str_to_IDP2(type_string, typ, val_string)[source]

recursive function to decode a val_string of type type_string and type

Parameters

type_string (str) –
typ (TypeDeclaration) – type declaration of the value string
val_string (str) – value_string

Raises

IDPZ3Error – if wrong value

Returns

the internal representation of the value

Return type

Expression

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
block (Vocabulary) – the vocabulary block that contains it

__init__(**kwargs)[source]

contains_element(term, interpretations, extensions)[source]

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

Parameters

term (Expression) –
interpretations (dict[str, 'SymbolInterpretation']) –
extensions (dict[str, Extension]) –

Return type

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

block: the vocabulary where it is defined

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

voc

the vocabulary block that contains it

Type: Vocabulary

__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, 'SymbolInterpretation']) –
extensions (dict[str, Extension]) –

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 (Expression) –
interpretations (dict[str, 'SymbolInterpretation']) –
extensions (dict[str, Extension]) –

Return type

Expression

contains_element(term, interpretations, extensions)[source]

returns an Expression that is TRUE when term satisfies the predicate

Parameters

term (Expression) –
interpretations (dict[str, 'SymbolInterpretation']) –
extensions (dict[str, Extension]) –

Return type

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(parent, annotations, mode, rules)[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)
renamed (dict[Declaration, List[Rule]]):: rules with normalized body for each defined symbol, e.g., !x: p(x) <- q(p1_) (quantees and head are unchanged)
canonicals (dict[Declaration, List[Rule]]):: normalized rule for each defined symbol, e.g., ! p1_: p(p1_) <- q(p1_)
clarks (dict[Declaration, Transformed Rule]):: normalized rule for each defined symbol (used to be Clark completion) e.g., ! p1_: p(p1_) <=> q(p1_)
def_vars (dict[String, dict[String, Variable]]):: Fresh variables for arguments and result
inductive (set[SymbolDeclaration]): set of SymbolDeclaration with an inductive definition
cache (dict[SymbolDeclaration, str, Expression]):: cache of instantiation of the definition

inst_def_level (int): depth of recursion during instantiation

__init__(parent, annotations, mode, rules)[source]

class Rule(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]

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, SymbolInterpretation]]) –
extensions (Optional[dict[str, Extension]]) –

Return type

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, "SymbolInterpretation"], 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, "SymbolInterpretation"], 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, SymbolInterpretation]]) –
extensions (Optional[dict[str, Extension]]) –

Return type

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, "SymbolInterpretation"], 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, SymbolInterpretation]]) –
extensions (Optional[dict[str, Extension]]) –

Return type

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, "SymbolInterpretation"], optional) – _description_. Defaults to None.
extensions (dict[str, Extension], optional) – _description_. Defaults to None.

Returns

_description_

Return type

Extension

class RangeElement(**kwargs)[source]

Bases: idp_engine.Expression.ASTNode

__init__(**kwargs)[source]

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, "SymbolInterpretation"], 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, "SymbolInterpretation"], 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, "SymbolInterpretation"], 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]