idp_solver.Parse¶
Classes to parse and annotate an IDP-Z3 theory.
-
class
idp_solver.Parse.
Idp
(**kwargs)[source]¶ Bases:
idp_solver.Expression.ASTNode
The class of AST nodes representing an IDP-Z3 program.
-
execute
()¶ Execute the IDP program
-
-
class
idp_solver.Parse.
Vocabulary
(**kwargs)[source]¶ Bases:
idp_solver.Expression.ASTNode
The class of AST nodes representing a vocabulary block.
-
class
idp_solver.Parse.
ConstructedTypeDeclaration
(**kwargs)[source]¶ Bases:
idp_solver.Expression.ASTNode
AST node to represent type <symbol> := <enumeration>
- Parameters
name (string) – name of the type
constructors ([Constructor]) – list of constructors in the enumeration
interpretation (SymbolInterpretation) – the symbol interpretation
translated (Z3) – the translation of the type in Z3
map (Dict[string, Constructor]) – a mapping from code to Expression
-
class
idp_solver.Parse.
SymbolDeclaration
(**kwargs)[source]¶ Bases:
idp_solver.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
-
out
¶ the type of the symbol
-
type
¶ the name of the type of the symbol
- Type
string
-
arity
¶ the number of arguments
- Type
int
-
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]
-
typeConstraints
¶ the type constraint on the ranges of the symbol applied to each possible tuple of arguments
- Type
List[Expression]
-
unit
¶ the unit of the symbol, such as m (meters)
- Type
str
-
category
¶ the category that the symbol should belong to
- Type
str
-
-
class
idp_solver.Parse.
Theory
(**kwargs)[source]¶ Bases:
idp_solver.Expression.ASTNode
The class of AST nodes representing a theory block.
-
class
idp_solver.Parse.
Rule
(**kwargs)[source]¶ Bases:
idp_solver.Expression.ASTNode
-
class
idp_solver.Parse.
Structure
(**kwargs)[source]¶ Bases:
idp_solver.Expression.ASTNode
The class of AST nodes representing an structure block.