idp_engine.Parse¶
Classes to parse an IDP-Z3 theory.
-
class
idp_engine.Parse.
IDP
(**kwargs)[source]¶ Bases:
idp_engine.Expression.ASTNode
The class of AST nodes representing an IDP-Z3 program.
- Parameters
code (str) – source code of the IDP program
vocabularies (dict[str, Vocabulary]) – list of vocabulary blocks, by name
theories (dict[str, Theory]) – list of theory blocks, by name
structures (dict[str, Structure]) – list of structure blocks, by name
procedures (dict[str, Procedure]) – list of procedure blocks, by name
display (Display, Optional) – display block, if any
-
classmethod
from_file
(file: str) → idp_engine.Parse.IDP[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: str) → idp_engine.Parse.IDP[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: str) → idp_engine.Parse.IDP[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: List[str])[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, Theory, Structure, Procedure, Display]]
-
execute
()¶ Execute the IDP program
-
class
idp_engine.Parse.
Vocabulary
(**kwargs)[source]¶ Bases:
idp_engine.Expression.ASTNode
The class of AST nodes representing a vocabulary block.
-
class
idp_engine.Parse.
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
constructors ([Constructor]) – list of constructors in the enumeration
range ([Expression]) – list of expressions of that type
interpretation (SymbolInterpretation) – the symbol interpretation
map (Dict[string, Expression]) – a mapping from code to Expression in range
-
class
idp_engine.Parse.
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).
-
name
¶ the identifier of the symbol, after expansion of the node
- Type
string
-
arity
¶ the number of arguments
- Type
int
-
type
¶ name of the Z3 type of an instance of the symbol
- Type
string
-
domain
¶ the list of possible tuples of arguments
- Type
List
-
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
-
-
class
idp_engine.Parse.
Symbol
(**kwargs)[source]¶ Bases:
idp_engine.Expression.Expression
Represents a Symbol. Handles synonyms.
-
name
¶ name of the symbol
- Type
string
-
-
class
idp_engine.Parse.
Theory
(**kwargs)[source]¶ Bases:
idp_engine.Expression.ASTNode
The class of AST nodes representing a theory block.
-
class
idp_engine.Parse.
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
-
set_level_symbols
()[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 (Problem) – 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
(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
-
class
idp_engine.Parse.
Rule
(**kwargs)[source]¶ Bases:
idp_engine.Expression.ASTNode
-
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 (Problem) – the context for the interpretation
- Returns
a boolean expression
- Return type
-
rename_args
(new_vars)¶ for Clark’s completion input : ‘!v: f(args) <- body(args)’ output: ‘!nv: f(nv) <- nv=args & body(args)’
-
-
class
idp_engine.Parse.
Structure
(**kwargs)[source]¶ Bases:
idp_engine.Expression.ASTNode
The class of AST nodes representing an structure block.
-
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
idp_engine.Parse.
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
-
constructors
¶ List of Constructor
- Type
List[Constructor], optional
-