idp_engine.Parse¶
Classes to parse an IDP-Z3 theory.
- 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
- 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
- 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
- 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(capture_print=False)
Execute the
main()
procedure block in the IDP program- Parameters
self (idp_engine.Parse.IDP) –
capture_print (bool) –
- Return type
Optional[str]
- class Vocabulary(parent, name, declarations)[source]
Bases:
idp_engine.Expression.ASTNode
The class of AST nodes representing a vocabulary block.
- Parameters
parent (ASTNode) –
name (str) –
declarations (List[Union[Declaration, VarDeclaration, Import]]) –
- __init__(parent, name, declarations)[source]
- Parameters
parent (idp_engine.Expression.ASTNode) –
name (str) –
declarations (List[Union[idp_engine.Parse.TypeDeclaration, idp_engine.Parse.SymbolDeclaration, idp_engine.Parse.VarDeclaration, idp_engine.Parse.Import]]) –
- class TypeDeclaration(parent, name, constructors=None, enumeration=None)[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
domains (List[SetName]) – a singleton list with a set having the type’s name
codomain (SetName) – the Boolean type
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
enumeration (Optional[Enumeration]) –
- __init__(parent, name, constructors=None, enumeration=None)[source]
- Parameters
name (str) –
constructors (Optional[List[idp_engine.Expression.Constructor]]) –
enumeration (Optional[idp_engine.Parse.Enumeration]) –
- contains_element(term, extensions)[source]
returns an Expression that is TRUE when term is in the type
- Parameters
term (Expression) –
extensions (dict[str, Extension]) –
- Return type
Expression
- class SymbolDeclaration(parent, annotations, sorts, out, symbols=None, name=None)[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.
- Parameters
annotations (Optional[Annotations]) –
sorts (List[SetName]) –
out (SetName) –
symbols (Optional[List[str]]) –
name (Optional[str]) –
- 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
[str]
- name
the identifier of the symbol, after expansion of the node
- Type
string
- arity
the number of arguments
- Type
int
- domains
the types of the arguments
- Type
List[SetName]
- codomain
the type of the symbol
- Type
SetName
- symbol_expr
symbol expression of the same name
- Type
SymbolExpr, Optional
- symbol_expr
a SymbolExpr of the same name
- Type
SymbolExpr, Optional
- 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
- by_z3
True if the symbol is created by z3 (testers and accessors of constructors)
- Type
Bool
- __init__(parent, annotations, sorts, out, symbols=None, name=None)[source]
- Parameters
annotations (Optional[idp_engine.Expression.Annotations]) –
sorts (List[idp_engine.Expression.SetName]) –
out (idp_engine.Expression.SetName) –
symbols (Optional[List[str]]) –
name (Optional[str]) –
- 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, extensions)[source]
returns an Expression that is TRUE when term satisfies the predicate
- Parameters
term (Expression) –
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
SetName
- __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.Expression
The class of AST nodes representing an inductive definition.
- Parameters
annotations (Optional[Annotations]) –
- id
unique identifier for each definition
- Type
num
- rules
set of rules for the definition, e.g., !x: p(x) <- q(x)
- Type
[Rule]
- renamed
rules with normalized body for each defined symbol, e.g., !x: p(x) <- q(p1_) (quantees and head are unchanged)
- Type
dict[Declaration, List[Rule]]
- canonicals
normalized rule for each defined symbol, e.g., ! p1_: p(p1_) <- q(p1_)
- Type
dict[Declaration, List[Rule]]
- clarks
normalized rule for each defined symbol (used to be Clark completion) e.g., ! p1_: p(p1_) <=> q(p1_)
- Type
dict[Declaration, Transformed Rule]
- def_vars
Fresh variables for arguments and result
- Type
dict[String, dict[String, Variable]]
- inductive
set of SymbolDeclaration with an inductive definition
- Type
set[SymbolDeclaration]
- cache
cache of instantiation of the definition
- Type
dict[SymbolDeclaration, str, Expression]
- inst_def_level
depth of recursion during instantiation
- Type
int
- __init__(parent, annotations, mode, rules)[source]
- Parameters
annotations (Optional[idp_engine.Expression.Annotations]) –
- get_def_constraints(problem, for_explain=False)
returns the constraints for this definition.
The instantiables (of the definition) are expanded in problem.
- Parameters
problem (Theory) – contains the structure for the expansion/interpretation of the constraints
for_explain (Bool) – Use implications instead of equivalence, for rule-specific explanations
self (Definition) –
- Returns
a mapping from (SymbolDeclaration, Definition) to the list of constraints
- Return type
dict[SymbolDeclaration, Definition, List[Expression]]
- annotate(voc, q_vars)
annotate tree after parsing
Resolve names and determine type as well as variables in the expression
- Parameters
voc (Vocabulary) – the vocabulary
q_vars (dict[str, Variable]) – the quantifier variables that may appear in the expression
self (Expression) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- 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
self (idp_engine.Parse.Definition) –
- class Rule(parent, annotations, quantees, definiendum, out, body)[source]
Bases:
idp_engine.Expression.Expression
- Parameters
annotations (Annotations) –
quantees (List[Quantee]) –
definiendum (AppliedSymbol) –
out (Expression) –
body (Expression) –
- __init__(parent, annotations, quantees, definiendum, out, body)[source]
- Parameters
annotations (idp_engine.Expression.Annotations) –
quantees (List[idp_engine.Expression.Quantee]) –
definiendum (idp_engine.Expression.AppliedSymbol) –
out (idp_engine.Expression.Expression) –
body (idp_engine.Expression.Expression) –
- instantiate_definition(new_args, theory)
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
self (idp_engine.Parse.Rule) –
- Returns
a boolean expression
- Return type
Expression
- annotate(voc, q_vars)
annotate tree after parsing
Resolve names and determine type as well as variables in the expression
- Parameters
voc (Vocabulary) – the vocabulary
q_vars (dict[str, Variable]) – the quantifier variables that may appear in the expression
self (Expression) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- 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_block(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 (idp_engine.Parse.IDP) – a Parse.IDP object.
self (idp_engine.Expression.ASTNode) –
idp –
- Returns None
- Return type
Union[Exception, List[Exceptions]]
- class SymbolInterpretation(parent, name, sign, enumeration, default)[source]
Bases:
idp_engine.Expression.Expression
AST node representing <symbol> := { <identifiers*> } else <default>.
- Parameters
name (UnappliedSymbol) –
sign (str) –
enumeration (Enumeration) –
default (Optional[Expression]) –
- name
name of the symbol being enumerated.
- Type
string
- symbol_decl
symbol being enumerated
- Type
SymbolDeclaration
- 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__(parent, name, sign, enumeration, default)[source]
- Parameters
name (idp_engine.Expression.UnappliedSymbol) –
sign (str) –
enumeration (idp_engine.Parse.Enumeration) –
default (Optional[idp_engine.Expression.Expression]) –
- 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(voc, q_vars)
Annotate the symbol.
- Parameters
block – a Structure object
self (Expression) –
voc (Vocabulary) –
q_vars (dict[str, Variable]) –
- Returns None
- Return type
Annotated
- interpret(problem)
expand quantifiers and replace symbols interpreted in the structure by their interpretation
- Parameters
self (idp_engine.Parse.SymbolInterpretation) – the expression to be interpreted
problem (idp_engine.Theory.Theory) – the theory to be applied
subs – a dictionary mapping variable names to their value
- Returns
the interpreted expression
- Return type
Expression
- class Enumeration(parent, tuples)[source]
Bases:
idp_engine.Expression.Expression
Represents an enumeration of tuples of expressions. Used for predicates, or types without n-ary constructors.
- Parameters
parent (ASTNode) –
tuples (List[TupleIDP]) –
- 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__(parent, tuples)[source]
- Parameters
parent (idp_engine.Expression.ASTNode) –
tuples (List[idp_engine.Parse.TupleIDP]) –
- contains(args, arity=None, rank=0, tuples=None, theory=None)[source]
returns an Expression that says whether Tuple args is in the enumeration
- Parameters
arity (Optional[int]) –
rank (int) –
tuples (Optional[List[TupleIDP]]) –
theory (Optional[Theory]) –
- Return type
Expression
- extensionE(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
- annotate(voc, q_vars)
annotate tree after parsing
Resolve names and determine type as well as variables in the expression
- Parameters
voc (Vocabulary) – the vocabulary
q_vars (dict[str, Variable]) – the quantifier variables that may appear in the expression
self (Expression) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- interpret(problem)
expand quantifiers and replace symbols interpreted in the structure by their interpretation
- Parameters
self (idp_engine.Parse.Enumeration) – the expression to be interpreted
problem (idp_engine.Theory.Theory) – the theory to be applied
subs – a dictionary mapping variable names to their value
- Returns
the interpreted expression
- Return type
Expression
- class FunctionEnum(parent, tuples)[source]
Bases:
idp_engine.Parse.Enumeration
- Parameters
parent (ASTNode) –
tuples (List[TupleIDP]) –
- extensionE(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(parent, tuples)[source]
Bases:
idp_engine.Parse.Enumeration
- Parameters
parent (ASTNode) –
tuples (List[TupleIDP]) –
- class ConstructedFrom(parent, constructed, constructors)[source]
Bases:
idp_engine.Parse.Enumeration
Represents a ‘constructed from’ enumeration of constructors
- Parameters
parent (Optional[ASTNode]) –
constructed (str) –
constructors (List[Constructor]) –
- tuples
OrderedSet of tuples of Expression
- Type
OrderedSet[TupleIDP], Optional
- constructors
List of Constructor
- Type
List[Constructor]
- accessors
index of the accessor in the constructors
- Type
dict[str, int]
- __init__(parent, constructed, constructors)[source]
- Parameters
parent (Optional[idp_engine.Expression.ASTNode]) –
constructed (str) –
constructors (List[idp_engine.Expression.Constructor]) –
- contains(args, arity=None, rank=0, tuples=None, theory=None)[source]
returns True if args belong to the type enumeration
- Parameters
arity (Optional[int]) –
rank (int) –
tuples (Optional[List[TupleIDP]]) –
theory (Optional[Theory]) –
- Return type
Expression
- extensionE(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
- annotate(voc, q_vars)
annotate tree after parsing
Resolve names and determine type as well as variables in the expression
- Parameters
voc (Vocabulary) – the vocabulary
q_vars (dict[str, Variable]) – the quantifier variables that may appear in the expression
self (ASTNode) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- interpret(problem)
expand quantifiers and replace symbols interpreted in the structure by their interpretation
- Parameters
self (idp_engine.Parse.ConstructedFrom) – the expression to be interpreted
problem (idp_engine.Theory.Theory) – the theory to be applied
subs – a dictionary mapping variable names to their value
- Returns
the interpreted expression
- Return type
Expression
- class TupleIDP(**kwargs)[source]
Bases:
idp_engine.Expression.Expression
- __init__(**kwargs)[source]
- annotate(voc, q_vars)
annotate tree after parsing
Resolve names and determine type as well as variables in the expression
- Parameters
voc (Vocabulary) – the vocabulary
q_vars (dict[str, Variable]) – the quantifier variables that may appear in the expression
self (Expression) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- translate(problem)
Converts the syntax tree to a Z3 expression, with lookup in problem.z3
- Parameters
problem (Theory) – holds the context for the translation (e.g. a cache of translations).
vars (dict[id, ExprRef], optional) – mapping from Variable’s id to Z3 translation. Filled in by AQuantifier. Defaults to {}.
- Returns
Z3 expression
- Return type
ExprRef
- class CSVTuple(**kwargs)[source]
Bases:
idp_engine.Parse.TupleIDP
- class Ranges(parent, **kwargs)[source]
Bases:
idp_engine.Parse.Enumeration
- Parameters
parent (ASTNode) –
- __init__(parent, **kwargs)[source]
- Parameters
parent (idp_engine.Expression.ASTNode) –
- contains(args, arity=None, rank=0, tuples=None, theory=None)[source]
returns an Expression that says whether Tuple args is in the enumeration
- Parameters
arity (Optional[int]) –
rank (int) –
tuples (Optional[List[TupleIDP]]) –
theory (Optional[Theory]) –
- Return type
Expression
- extensionE(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.Expression
- __init__(**kwargs)[source]
- class IntRange[source]
Bases:
idp_engine.Parse.Ranges
- __init__()[source]
- extensionE(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(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(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