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]
- 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()
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]
- 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 Symbol(**kwargs)[source]
Bases:
idp_engine.Expression.Expression
Represents a Symbol. Handles synonyms.
- name
name of the symbol
- Type
string
- __init__(**kwargs)[source]
- has_element(term, interpretations, extensions)[source]
Returns an expression that says whether term is in the type/predicate denoted by self.
- Parameters
term (Expression) – the argument to be checked
interpretations (Dict[str, SymbolInterpretation]) –
extensions (Dict[str, Tuple[Optional[List[List[idp_engine.Expression.Expression]]], Optional[Callable]]]) –
- Returns
whether term is in the type denoted by self.
- 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
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- instantiate(e0, e1, problem=None)
Recursively substitute Variable in e0 by e1 in a copy of self. Update .variables.
- translate(problem, vars={})
Converts the syntax tree to a Z3 expression, using .value and .simpler if present
- 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 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 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]
- 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, "SymbolInterpretation"], optional) – _description_. Defaults to None.
extensions (Dict[str, Extension], optional) – _description_. Defaults to None.
- Returns
_description_
- Return type
Extension