idp_engine.Expression¶
This module contains the ASTNode classes for expressions.
(Many methods are monkey-patched by other modules)
- class ASTNode[source]
Bases:
object
superclass of all AST nodes
- check(condition, msg)[source]
raises an exception if condition is not True
- Parameters
condition (Bool) – condition to be satisfied
msg (str) – error message
- Raises
IDPZ3Error – when condition is not met
- dedup_nodes(kwargs, arg_name)[source]
pops arg_name from kwargs as a list of named items and returns a mapping from name to items
- Parameters
kwargs (dict[str, List[ASTNode]]) – dictionary mapping named arguments to list of ASTNodes
arg_name (str) – name of the kwargs argument, e.g. “interpretations”
- Returns
mapping from name to AST nodes
- Return type
dict[str, ASTNode]
- Raises
AssertionError – in case of duplicate name
- class Annotations(parent, annotations)[source]
Bases:
idp_engine.Expression.ASTNode
- Parameters
annotations (List[str]) –
- __init__(parent, annotations)[source]
- Parameters
annotations (List[str]) –
- class Accessor(parent, out, accessor=None)[source]
Bases:
idp_engine.Expression.ASTNode
represents an accessor and a type
- Parameters
out (SetName) –
accessor (Optional[str]) –
- accessor
name of accessor function
- Type
str, Optional
- codomain
name of the output type of the accessor
- Type
SetName
- decl
declaration of the accessor function
- Type
SymbolDeclaration
- __init__(parent, out, accessor=None)[source]
- Parameters
out (idp_engine.Expression.SetName) –
accessor (Optional[str]) –
- class Expression(parent=None, annotations=None)[source]
Bases:
idp_engine.Expression.ASTNode
The abstract class of AST nodes representing (sub-)expressions.
- Parameters
parent (Optional[ASTNode]) –
annotations (Optional[Annotations]) –
- code
Textual representation of the expression. Often used as a key.
It is generated from the sub-tree.
- Type
string
- str
Textual representation of the simplified expression.
- Type
string
- sub_exprs
The children of the AST node.
The list may be reduced by simplification.
- Type
List[Expression]
- type
The type of the expression, e.g.,
bool
.- Type
SetName, Optional
- co_constraint
A constraint attached to the node.
For example, the co_constraint of
square(length(top()))
issquare(length(top())) = length(top())*length(top()).
, assumingsquare
is appropriately defined.The co_constraint of a defined symbol applied to arguments is the instantiation of the definition for those arguments. This is useful for definitions over infinite domains, as well as to compute relevant questions.
- Type
Expression, optional
- annotations
The set of annotations given by the expert in the IDP-Z3 program.
annotations['reading']
is the annotation giving the intended meaning of the expression (in English).- Type
dict[str, str]
- original
The original expression, before propagation and simplification.
- Type
Expression
- variables
The set of names of the variables in the expression, before interpretation.
- Type
Set(string)
- is_type_constraint_for
name of the symbol for which the expression is a type constraint
- Type
string
- __init__(parent=None, annotations=None)[source]
- Parameters
parent (Optional[idp_engine.Expression.ASTNode]) –
annotations (Optional[idp_engine.Expression.Annotations]) –
- 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
self (Expression) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.Expression) –
- Return type
idp_engine.Expression.Expression
- collect(questions, all_=True, co_constraints=True)[source]
collects the questions in self.
questions is an OrderedSet of Expression Questions are the terms and the simplest sub-formula that can be evaluated.
all_=False : ignore expanded formulas and AppliedSymbol interpreted in a structure
co_constraints=False : ignore co_constraints
default implementation for UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets
- Parameters
questions (idp_engine.utils.OrderedSet) –
all_ (bool) –
co_constraints (bool) –
- collect_symbols(symbols=None, co_constraints=True)[source]
returns the list of symbols occurring in self, ignoring type constraints and symbols created by aggregates
- Parameters
symbols (Optional[dict[str, SymbolDeclaration]]) –
co_constraints (bool) –
- Return type
dict[str, SymbolDeclaration]
- collect_nested_symbols(symbols, is_nested)
returns the set of symbol declarations that occur (in)directly under an aggregate or some nested term, where is_nested is flipped to True the moment we reach such an expression
returns {SymbolDeclaration}
- Parameters
symbols (Set[idp_engine.Parse.SymbolDeclaration]) –
is_nested (bool) –
- Return type
Set[idp_engine.Parse.SymbolDeclaration]
- generate_constructors(constructors)[source]
fills the list constructors with all constructors belonging to open types.
- Parameters
constructors (dict[str, List[Constructor]]) –
- collect_co_constraints(co_constraints, recursive=True)[source]
collects the constraints attached to AST nodes, e.g. instantiated definitions
- Parameters
recursive – if True, collect co_constraints of co_constraints too
co_constraints (idp_engine.utils.OrderedSet) –
- is_value()[source]
True for numerals, date, identifiers, and constructors applied to values.
Synomym: “is ground”, “is rigid”
- Returns
True if self represents a value.
- Return type
bool
- is_reified()[source]
False for values and for symbols applied to values.
- Returns
True if self has to be reified to obtain its value in a Z3 model.
- Return type
bool
- is_assignment()[source]
- Returns
True if self assigns a rigid term to a rigid function application
- Return type
bool
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.Expression) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- interpret(problem, subs)
expand quantifiers and replace symbols interpreted in the structure by their interpretation
- Parameters
self (Expression) – the expression to be interpreted
problem (Optional[Theory]) – the theory to be applied
subs (dict[str, Expression]) – a dictionary mapping variable names to their value
- Returns
the interpreted expression
- Return type
Expression
- substitute(e0, e1, assignments, tag=None)
recursively substitute e0 by e1 in self (e0 is not a Variable)
if tag is present, updates assignments with symbolic propagation of co-constraints.
implementation for everything but AppliedSymbol, UnappliedSymbol and Fresh_variable
- simplify_with(assignments, co_constraints_too=True)
simplify the expression using the assignments
- Parameters
self (idp_engine.Expression.Expression) –
assignments (idp_engine.Assignments.Assignments) –
- Return type
idp_engine.Expression.Expression
- symbolic_propagate(assignments, tag, truth=true)
updates assignments with the consequences of self=truth.
The consequences are obtained by symbolic processing (no calls to Z3).
- Parameters
assignments (Assignments) – The set of assignments to update.
truth (Expression, optional) – The truth value of the expression self. Defaults to TRUE.
tag (idp_engine.Assignments.Status) –
- propagate1(assignments, tag, truth)
returns the list of symbolic_propagate of self, ignoring value and simpler
- translate(problem, vars={})
Converts the syntax tree to a Z3 expression, with lookup in problem.z3
- 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
- split_equivalences()[source]
Returns an equivalent expression where equivalences are replaced by implications
- Returns
Expression
- Return type
idp_engine.Expression.Expression
- add_level_mapping(level_symbols, head, pos_justification, polarity, mode)
- Returns an expression where level mapping atoms (e.g., lvl_p > lvl_q)
are added to atoms containing recursive symbols.
- Parameters
level_symbols (-) – the level mapping symbols as well as their corresponding recursive symbols
head (-) – head of the rule we are adding level mapping symbols to.
pos_justification (-) – whether we are adding symbols to the direct positive justification (e.g., head => body) or direct negative justification (e.g., body => head) part of the rule.
polarity (-) – whether the current expression occurs under negation.
mode (Semantics) –
- Return type
Expression
- class Constructor(parent, name, args=None)[source]
Bases:
idp_engine.Expression.ASTNode
Constructor declaration
- Parameters
parent (Optional[ASTNode]) –
name (str) –
args (Optional[List[Accessor]]) –
- name
name of the constructor
- Type
string
- args
- Type
List[Accessor]
- sorts
types of the arguments of the constructor
- Type
List[SetName]
- out
type that contains this constructor
- Type
SetName
- arity
number of arguments of the constructor
- Type
Int
- tester
function to test if the constructor
- Type
SymbolDeclaration, Optional
- has been applied to some arguments
- Type
e.g., is_rgb
- concept_decl
declaration with name[1:],
- Type
SymbolDeclaration, Optional
- only for Concept constructors.
- range
the list of identifiers
- __init__(parent, name, args=None)[source]
- Parameters
parent (Optional[idp_engine.Expression.ASTNode]) –
name (str) –
args (Optional[List[idp_engine.Expression.Accessor]]) –
- class SetName(parent, name, ins=None, out=None)[source]
Bases:
idp_engine.Expression.Expression
ASTNode representing a (sub-)type or a Concept[aSignature], e.g., Concept[T*T->Bool]
Inherits from Expression
- Parameters
name (str) – name of the concept
concept_domains (List[SetName], Optional) – domain of the Concept signature, e.g., [T, T]
codomain (SetName, Optional) – range of the Concept signature, e.g., Bool
decl (Declaration, Optional) – declaration of the type
root_set (SetName, Optional) – a Type or a Concept with signature (Concept[T->T])
ins (Optional[List[SetName]]) –
out (Optional[SetName]) –
- __init__(parent, name, ins=None, out=None)[source]
- Parameters
name (str) –
ins (Optional[List[idp_engine.Expression.SetName]]) –
out (Optional[idp_engine.Expression.SetName]) –
- extension(extensions)
returns the extension of a SetName, given some interpretations.
Normally, the extension is already in extensions by SymbolDeclaration.interpret. However, for Concept[T->T], an additional filtering is applied.
- Parameters
interpretations (dict[str, SymbolInterpretation]) –
symbols (the known interpretations of types and) –
extensions (dict[str, Extension]) –
- Returns
a superset of the extension of self, and a function that, given arguments, returns an Expression that says whether the arguments are in the extension of self
- Return type
Extension
- is_value()[source]
True for numerals, date, identifiers, and constructors applied to values.
Synomym: “is ground”, “is rigid”
- Returns
True if self represents a value.
- Return type
bool
- has_element(term, 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
extensions (dict[str, Extension]) –
- Returns
whether term 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
self (Expression) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- translate(problem, vars={})
Converts the syntax tree to a Z3 expression, with lookup in problem.z3
- 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 AIfExpr(parent, if_f, then_f, else_f)[source]
Bases:
idp_engine.Expression.Expression
- Parameters
if_f (Expression) –
then_f (Expression) –
else_f (Expression) –
- __init__(parent, if_f, then_f, else_f)[source]
- Parameters
if_f (idp_engine.Expression.Expression) –
then_f (idp_engine.Expression.Expression) –
else_f (idp_engine.Expression.Expression) –
- collect_nested_symbols(symbols, is_nested)
returns the set of symbol declarations that occur (in)directly under an aggregate or some nested term, where is_nested is flipped to True the moment we reach such an expression
returns {SymbolDeclaration}
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.AIfExpr) –
- Return type
idp_engine.Expression.Expression
- translate1(problem, vars={})
Converts the syntax tree to a Z3 expression, without lookup in problem.z3
A lookup is wasteful when self is a subformula of a formula that is not in problem.z3.
- 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
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.AIfExpr) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class Quantee(parent, vars, subtype=None, sort=None)[source]
Bases:
idp_engine.Expression.Expression
represents the description of quantification, e.g., x in T or (x,y) in P The Concept type may be qualified, e.g. Concept[Color->Bool]
- Parameters
vars (Union[List[Variable], List[List[Variable]]]) –
subtype (Optional[SetName]) –
sort (Optional[SymbolExpr]) –
- vars
the (tuples of) variables being quantified
- Type
List[List[Variable]]
- subtype
a literal SetName to quantify over, e.g., Color or Concept[Color->Bool].
- Type
SetName, Optional
- sort
a dereferencing expression, e.g.,. $(i).
- Type
SymbolExpr, Optional
- sub_exprs
the (unqualified) type or predicate to quantify over,
- Type
List[SymbolExpr], Optional
- e.g., `[Color], [Concept] or [$
- Type
i
- arity
the length of the tuple of variables
- Type
int
- decl
the (unqualified) Declaration to quantify over, after resolution of $(i).
- Type
SymbolDeclaration, Optional
- e.g., the declaration of `Color`
- __init__(parent, vars, subtype=None, sort=None)[source]
- Parameters
vars (Union[List[idp_engine.Expression.Variable], List[List[idp_engine.Expression.Variable]]]) –
subtype (Optional[idp_engine.Expression.SetName]) –
sort (Optional[idp_engine.Expression.SymbolExpr]) –
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.AQuantification) –
- Return type
idp_engine.Expression.Expression
- translate(problem, vars={})
Converts the syntax tree to a Z3 expression, with lookup in problem.z3
- 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
- split_quantees(self)[source]
replaces an untyped quantee x,y,z into 3 quantees, so that each variable can have its own sort
- Parameters
self – either a AQuantification, AAggregate or Rule
- class AQuantification(parent, annotations, q, quantees, f)[source]
Bases:
idp_engine.Expression.Expression
ASTNode representing a quantified formula
- Parameters
annotations (dict[str, str]) –
The set of annotations given by the expert in the IDP-Z3 program.
annotations['reading']
is the annotation giving the intended meaning of the expression (in English).q (str) – either ‘∀’ or ‘∃’
quantees (List[Quantee]) – list of variable declarations
f (Expression) – the formula being quantified
supersets – attributes used in interpret
new_quantees – attributes used in interpret
vars1 – attributes used in interpret
parent (Optional[ASTNode]) –
- __init__(parent, annotations, q, quantees, f)[source]
- Parameters
parent (Optional[idp_engine.Expression.ASTNode]) –
annotations (Optional[idp_engine.Expression.Annotations]) –
q (str) –
quantees (List[idp_engine.Expression.Quantee]) –
f (idp_engine.Expression.Expression) –
- classmethod make(q, quantees, f, annotations=None)[source]
make and annotate a quantified formula
- Parameters
q (str) –
quantees (List[idp_engine.Expression.Quantee]) –
f (idp_engine.Expression.Expression) –
annotations (Optional[Dict[str, Union[str, Dict[str, Any]]]]) –
- Return type
AQuantification
- collect(questions, all_=True, co_constraints=True)[source]
collects the questions in self.
questions is an OrderedSet of Expression Questions are the terms and the simplest sub-formula that can be evaluated.
all_=False : ignore expanded formulas and AppliedSymbol interpreted in a structure
co_constraints=False : ignore co_constraints
default implementation for UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets
- collect_symbols(symbols=None, co_constraints=True)[source]
returns the list of symbols occurring in self, ignoring type constraints and symbols created by aggregates
- 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
self (Expression) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.AQuantification) –
- Return type
idp_engine.Expression.Expression
- symbolic_propagate(assignments, tag, truth=true)
updates assignments with the consequences of self=truth.
The consequences are obtained by symbolic processing (no calls to Z3).
- Parameters
assignments (Assignments) – The set of assignments to update.
truth (Expression, optional) – The truth value of the expression self. Defaults to TRUE.
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.AQuantification) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class Operator(parent, operator, sub_exprs, annotations=None)[source]
Bases:
idp_engine.Expression.Expression
- Parameters
annotations (Optional[Annotations]) –
- __init__(parent, operator, sub_exprs, annotations=None)[source]
- Parameters
annotations (Optional[idp_engine.Expression.Annotations]) –
- classmethod make(ops, operands, annotations=None, parent=None)[source]
creates a BinaryOp beware: cls must be specific for ops !
- Parameters
ops (Union[str, List[str]]) –
operands (List[idp_engine.Expression.Expression]) –
annotations (Optional[Dict[str, Union[str, Dict[str, Any]]]]) –
- Return type
idp_engine.Expression.Expression
- collect(questions, all_=True, co_constraints=True)[source]
collects the questions in self.
questions is an OrderedSet of Expression Questions are the terms and the simplest sub-formula that can be evaluated.
all_=False : ignore expanded formulas and AppliedSymbol interpreted in a structure
co_constraints=False : ignore co_constraints
default implementation for UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets
- collect_nested_symbols(symbols, is_nested)
returns the set of symbol declarations that occur (in)directly under an aggregate or some nested term, where is_nested is flipped to True the moment we reach such an expression
returns {SymbolDeclaration}
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.Operator) –
- Return type
idp_engine.Expression.Expression
- class AImplication(parent, operator, sub_exprs, annotations=None)[source]
Bases:
idp_engine.Expression.Operator
- Parameters
annotations (Optional[Annotations]) –
- add_level_mapping(level_symbols, head, pos_justification, polarity, mode)
- Returns an expression where level mapping atoms (e.g., lvl_p > lvl_q)
are added to atoms containing recursive symbols.
- Parameters
level_symbols (-) – the level mapping symbols as well as their corresponding recursive symbols
head (-) – head of the rule we are adding level mapping symbols to.
pos_justification (-) – whether we are adding symbols to the direct positive justification (e.g., head => body) or direct negative justification (e.g., body => head) part of the rule.
polarity (-) – whether the current expression occurs under negation.
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.AImplication) –
- Return type
idp_engine.Expression.Expression
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.AImplication) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class AEquivalence(parent, operator, sub_exprs, annotations=None)[source]
Bases:
idp_engine.Expression.Operator
- Parameters
annotations (Optional[Annotations]) –
- split_equivalences()[source]
Returns an equivalent expression where equivalences are replaced by implications
- Returns
Expression
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.AEquivalence) –
- Return type
idp_engine.Expression.Expression
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.AEquivalence) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class ARImplication(parent, operator, sub_exprs, annotations=None)[source]
Bases:
idp_engine.Expression.Operator
- Parameters
annotations (Optional[Annotations]) –
- add_level_mapping(level_symbols, head, pos_justification, polarity, mode)
- Returns an expression where level mapping atoms (e.g., lvl_p > lvl_q)
are added to atoms containing recursive symbols.
- Parameters
level_symbols (-) – the level mapping symbols as well as their corresponding recursive symbols
head (-) – head of the rule we are adding level mapping symbols to.
pos_justification (-) – whether we are adding symbols to the direct positive justification (e.g., head => body) or direct negative justification (e.g., body => head) part of the rule.
polarity (-) – whether the current expression occurs under negation.
- 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
self (ARImplication) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- class ADisjunction(parent, operator, sub_exprs, annotations=None)[source]
Bases:
idp_engine.Expression.Operator
- Parameters
annotations (Optional[Annotations]) –
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.Expression) –
- Return type
idp_engine.Expression.Expression
- propagate1(assignments, tag, truth=true)
returns the list of symbolic_propagate of self, ignoring value and simpler
- update_exprs(new_exprs, replace=True)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.Expression) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class AConjunction(parent, operator, sub_exprs, annotations=None)[source]
Bases:
idp_engine.Expression.Operator
- Parameters
annotations (Optional[Annotations]) –
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.Expression) –
- Return type
idp_engine.Expression.Expression
- propagate1(assignments, tag, truth=true)
returns the list of symbolic_propagate of self, ignoring value and simpler
- update_exprs(new_exprs, replace=True)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.Expression) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class AComparison(parent, operator, sub_exprs, annotations=None)[source]
Bases:
idp_engine.Expression.Operator
- Parameters
annotations (Optional[Annotations]) –
- is_assignment()[source]
- Returns
True if self assigns a rigid term to a rigid function application
- Return type
bool
- 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
self (AComparison) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.AppliedSymbol) –
- Return type
idp_engine.Expression.Expression
- propagate1(assignments, tag, truth=true)
returns the list of symbolic_propagate of self, ignoring value and simpler
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.AComparison) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class ASumMinus(parent, operator, sub_exprs, annotations=None)[source]
Bases:
idp_engine.Expression.Operator
- Parameters
annotations (Optional[Annotations]) –
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.ASumMinus) –
- Return type
idp_engine.Expression.Expression
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.ASumMinus) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class AMultDiv(parent, operator, sub_exprs, annotations=None)[source]
Bases:
idp_engine.Expression.Operator
- Parameters
annotations (Optional[Annotations]) –
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.AMultDiv) –
- Return type
idp_engine.Expression.Expression
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.AMultDiv) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class APower(parent, operator, sub_exprs, annotations=None)[source]
Bases:
idp_engine.Expression.Operator
- Parameters
annotations (Optional[Annotations]) –
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.APower) –
- Return type
idp_engine.Expression.Expression
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.APower) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class AUnary(parent, operators, f)[source]
Bases:
idp_engine.Expression.Expression
- Parameters
operators (List[str]) –
f (Expression) –
- __init__(parent, operators, f)[source]
- Parameters
operators (List[str]) –
f (idp_engine.Expression.Expression) –
- add_level_mapping(level_symbols, head, pos_justification, polarity, mode)
- Returns an expression where level mapping atoms (e.g., lvl_p > lvl_q)
are added to atoms containing recursive symbols.
- Parameters
level_symbols (-) – the level mapping symbols as well as their corresponding recursive symbols
head (-) – head of the rule we are adding level mapping symbols to.
pos_justification (-) – whether we are adding symbols to the direct positive justification (e.g., head => body) or direct negative justification (e.g., body => head) part of the rule.
polarity (-) – whether the current expression occurs under negation.
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.AUnary) –
- Return type
idp_engine.Expression.Expression
- propagate1(assignments, tag, truth=true)
returns the list of symbolic_propagate of self, ignoring value and simpler
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.AUnary) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class AAggregate(parent, aggtype, quantees, lambda_=None, f=None, if_=None)[source]
Bases:
idp_engine.Expression.Expression
- Parameters
aggtype (str) –
quantees (List[Quantee]) –
lambda_ (Optional[str]) –
f (Optional[Expression]) –
if_ (Optional[Expression]) –
- __init__(parent, aggtype, quantees, lambda_=None, f=None, if_=None)[source]
- Parameters
aggtype (str) –
quantees (List[idp_engine.Expression.Quantee]) –
lambda_ (Optional[str]) –
f (Optional[idp_engine.Expression.Expression]) –
if_ (Optional[idp_engine.Expression.Expression]) –
- collect(questions, all_=True, co_constraints=True)[source]
collects the questions in self.
questions is an OrderedSet of Expression Questions are the terms and the simplest sub-formula that can be evaluated.
all_=False : ignore expanded formulas and AppliedSymbol interpreted in a structure
co_constraints=False : ignore co_constraints
default implementation for UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets
- collect_symbols(symbols=None, co_constraints=True)[source]
returns the list of symbols occurring in self, ignoring type constraints and symbols created by aggregates
- 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
self (AAggregate) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- collect_nested_symbols(symbols, is_nested)
returns the set of symbol declarations that occur (in)directly under an aggregate or some nested term, where is_nested is flipped to True the moment we reach such an expression
returns {SymbolDeclaration}
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.AQuantification) –
- Return type
idp_engine.Expression.Expression
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.AAggregate) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class AppliedSymbol(parent, symbol, sub_exprs, annotations=None, is_enumerated='', is_enumeration='', in_enumeration='')[source]
Bases:
idp_engine.Expression.Expression
Represents a symbol applied to arguments
- Parameters
symbol (SymbolExpr) – the symbol to be applied to arguments
is_enumerated (string) – ‘’ or ‘is enumerated’
is_enumeration (string) – ‘’ or ‘in’
in_enumeration (Enumeration) – the enumeration following ‘in’
as_disjunction (Optional[Expression]) – the translation of ‘is_enumerated’ and ‘in_enumeration’ as a disjunction
decl (Declaration) – the declaration of the symbol, if known
in_head (Bool) – True if the AppliedSymbol occurs in the head of a rule
annotations (Optional[Annotations]) –
- __init__(parent, symbol, sub_exprs, annotations=None, is_enumerated='', is_enumeration='', in_enumeration='')[source]
- Parameters
annotations (Optional[idp_engine.Expression.Annotations]) –
- collect(questions, all_=True, co_constraints=True)[source]
collects the questions in self.
questions is an OrderedSet of Expression Questions are the terms and the simplest sub-formula that can be evaluated.
all_=False : ignore expanded formulas and AppliedSymbol interpreted in a structure
co_constraints=False : ignore co_constraints
default implementation for UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets
- collect_symbols(symbols=None, co_constraints=True)[source]
returns the list of symbols occurring in self, ignoring type constraints and symbols created by aggregates
- is_value()[source]
True for numerals, date, identifiers, and constructors applied to values.
Synomym: “is ground”, “is rigid”
- Returns
True if self represents a value.
- Return type
bool
- is_reified()[source]
False for values and for symbols applied to values.
- Returns
True if self has to be reified to obtain its value in a Z3 model.
- Return type
bool
- generate_constructors(constructors)[source]
fills the list constructors with all constructors belonging to open types.
- Parameters
constructors (dict) –
- add_level_mapping(level_symbols, head, pos_justification, polarity, mode)
- Returns an expression where level mapping atoms (e.g., lvl_p > lvl_q)
are added to atoms containing recursive symbols.
- Parameters
level_symbols (-) – the level mapping symbols as well as their corresponding recursive symbols
head (-) – head of the rule we are adding level mapping symbols to.
pos_justification (-) – whether we are adding symbols to the direct positive justification (e.g., head => body) or direct negative justification (e.g., body => head) part of the rule.
polarity (-) – whether the current expression occurs under negation.
- 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
self (AppliedSymbol) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- collect_nested_symbols(symbols, is_nested)
returns the set of symbol declarations that occur (in)directly under an aggregate or some nested term, where is_nested is flipped to True the moment we reach such an expression
returns {SymbolDeclaration}
- fill_attributes_and_check(type_check=True)
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.AppliedSymbol) –
- Return type
idp_engine.Expression.Expression
- substitute(e0, e1, assignments, tag=None)
recursively substitute e0 by e1 in self
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.AppliedSymbol) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class SymbolExpr(parent, name, eval, s)[source]
Bases:
idp_engine.Expression.Expression
represents either a type name, a symbol name or a $(..) expression evaluating to a type or symbol name
- Parameters
name (Optional[str]) –
eval (Optional[str]) –
s (Optional[Expression]) –
- name
name of the type or symbol, or None
- Type
Optional[str]
- eval
$ or None
- Type
Optional[str]
- s
argument of the $.
- Type
Optional[Expression]
- decl
the declaration of the symbol
- Type
Optional[Declaration]
Either name and decl`are not None, or `eval and s are not None. When eval is None, s is None too.
- __init__(parent, name, eval, s)[source]
- Parameters
name (Optional[str]) –
eval (Optional[str]) –
s (Optional[idp_engine.Expression.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
self (SymbolExpr) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.SymbolExpr) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression
- class UnappliedSymbol(parent, name)[source]
Bases:
idp_engine.Expression.Expression
The result of parsing a symbol not applied to arguments. Can be a constructor or a quantified variable.
Variables are converted to Variable() by annotate().
- Parameters
parent (Optional[ASTNode]) –
name (str) –
- __init__(parent, name)[source]
- Parameters
parent (Optional[idp_engine.Expression.ASTNode]) –
name (str) –
- classmethod construct(constructor)[source]
Create an UnappliedSymbol from a constructor
- Parameters
constructor (idp_engine.Expression.Constructor) –
- is_value()[source]
True for numerals, date, identifiers, and constructors applied to values.
Synomym: “is ground”, “is rigid”
- Returns
True if self represents a value.
- Return type
bool
- is_reified()[source]
False for values and for symbols applied to values.
- Returns
True if self has to be reified to obtain its value in a Z3 model.
- Return type
bool
- 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
self (UnappliedSymbol) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- class Variable(parent, name, type=None)[source]
Bases:
idp_engine.Expression.Expression
AST node for a variable in a quantification or aggregate
- Parameters
name (str) – name of the variable
type (Optional[Union[SetName]]) – sort of the variable, if known
- __init__(parent, name, type=None)[source]
- Parameters
name (str) –
type (Optional[idp_engine.Expression.SetName]) –
- fill_attributes_and_check()[source]
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.Expression) –
- Return type
idp_engine.Expression.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
self (Variable) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- substitute(e0, e1, assignments, tag=None)
recursively substitute e0 by e1 in self (e0 is not a Variable)
if tag is present, updates assignments with symbolic propagation of co-constraints.
implementation for everything but AppliedSymbol, UnappliedSymbol and Fresh_variable
- translate(problem, vars={})
Converts the syntax tree to a Z3 expression, with lookup in problem.z3
- 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 Number(**kwargs)[source]
Bases:
idp_engine.Expression.Expression
- __init__(**kwargs)[source]
- real()[source]
converts the INT number to REAL
- is_value()[source]
True for numerals, date, identifiers, and constructors applied to values.
Synomym: “is ground”, “is rigid”
- Returns
True if self represents a value.
- Return type
bool
- is_reified()[source]
False for values and for symbols applied to values.
- Returns
True if self has to be reified to obtain its value in a Z3 model.
- Return type
bool
- 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
self (Number) –
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
- translate(problem, vars={})
Converts the syntax tree to a Z3 expression, with lookup in problem.z3
- 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 Date(**kwargs)[source]
Bases:
idp_engine.Expression.Expression
- __init__(**kwargs)[source]
- is_value()[source]
True for numerals, date, identifiers, and constructors applied to values.
Synomym: “is ground”, “is rigid”
- Returns
True if self represents a value.
- Return type
bool
- is_reified()[source]
False for values and for symbols applied to values.
- Returns
True if self has to be reified to obtain its value in a Z3 model.
- Return type
bool
- translate(problem, vars={})
Converts the syntax tree to a Z3 expression, with lookup in problem.z3
- 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 Brackets(parent, f, annotations=None)[source]
Bases:
idp_engine.Expression.Expression
- Parameters
annotations (Optional[Annotations]) –
- __init__(parent, f, annotations=None)[source]
- Parameters
annotations (Optional[idp_engine.Expression.Annotations]) –
- fill_attributes_and_check()
annotations that are common to __init__ and make()
- Parameters
self (idp_engine.Expression.Brackets) –
- Return type
idp_engine.Expression.Expression
- symbolic_propagate(assignments, tag, truth=true)
updates assignments with the consequences of self=truth.
The consequences are obtained by symbolic processing (no calls to Z3).
- Parameters
assignments (Assignments) – The set of assignments to update.
truth (Expression, optional) – The truth value of the expression self. Defaults to TRUE.
- update_exprs(new_exprs)
change sub_exprs and simplify, while keeping relevant info.
- Parameters
self (idp_engine.Expression.Brackets) –
new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –
- Return type
idp_engine.Expression.Expression