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