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 (Expression) – the atom whose value must be converted
val_string (str) – the string representation of the value
- Returns
the value cast as Expression, or None if unknown
- Return type
Expression
- str_to_IDP2(type_string, typ, val_string)[source]
recursive function to decode a val_string of type type_string and type
- Parameters
type_string (str) –
typ (TypeDeclaration) – type declaration of the value string
val_string (str) – value_string
- Raises
IDPZ3Error – if wrong value
- Returns
the internal representation of the value
- Return type
Expression
- 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
block (Vocabulary) – the vocabulary block that contains it
- __init__(**kwargs)[source]
- contains_element(term, interpretations, extensions)[source]
returns an Expression that is TRUE when term is in the type
- Parameters
term (Expression) –
interpretations (dict[str, 'SymbolInterpretation']) –
extensions (dict[str, Extension]) –
- Return type
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
- 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
- voc
the vocabulary block that contains it
- Type
Vocabulary
- __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, '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, interpretations, extensions)[source]
returns an Expression that is TRUE when term satisfies the predicate
- Parameters
term (Expression) –
interpretations (dict[str, 'SymbolInterpretation']) –
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
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(parent, annotations, mode, rules)[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)
- renamed (dict[Declaration, List[Rule]]):
rules with normalized body for each defined symbol, e.g., !x: p(x) <- q(p1_) (quantees and head are unchanged)
- canonicals (dict[Declaration, List[Rule]]):
normalized rule for each defined symbol, e.g., ! p1_: p(p1_) <- q(p1_)
- clarks (dict[Declaration, Transformed Rule]):
normalized rule for each defined symbol (used to be Clark completion) e.g., ! p1_: p(p1_) <=> q(p1_)
- def_vars (dict[String, dict[String, Variable]]):
Fresh variables for arguments and result
- inductive (set[SymbolDeclaration])
set of SymbolDeclaration with an inductive definition
- cache (dict[SymbolDeclaration, str, Expression]):
cache of instantiation of the definition
inst_def_level (int): depth of recursion during instantiation
- __init__(parent, annotations, mode, rules)[source]
- 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, SymbolInterpretation]]) –
extensions (Optional[dict[str, Extension]]) –
- Return type
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, SymbolInterpretation]]) –
extensions (Optional[dict[str, Extension]]) –
- Return type
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, SymbolInterpretation]]) –
extensions (Optional[dict[str, Extension]]) –
- Return type
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 RangeElement(**kwargs)[source]
Bases:
idp_engine.Expression.ASTNode
- __init__(**kwargs)[source]
- 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