idp_engine.Expression¶
(They 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, ASTNode]) –
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
Expression
[source] Bases:
idp_engine.Expression.ASTNode
The abstract class of AST nodes representing (sub-)expressions.
-
code
Textual representation of the expression. Often used as a key.
It is generated from the sub-tree. Some tree transformations change it (e.g., instantiate), others don’t.
- Type
string
-
sub_exprs
The children of the AST node.
The list may be reduced by simplification.
- Type
List[Expression]
-
type
The name of the type of the expression, e.g.,
bool
.- Type
string
-
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
-
simpler
A simpler, equivalent expression.
Equivalence is computed in the context of the theory and structure. Simplifying an expression is useful for efficiency and to compute relevant questions.
- Type
Expression, optional
-
value
A rigid term equivalent to the expression, obtained by transformation.
Equivalence is computed in the context of the theory and structure.
- Type
Optional[Expression]
-
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.
- Type
Set(string)
-
is_type_constraint_for
name of the symbol for which the expression is a type constraint
- Type
string
-
__init__
()[source] Initialize self. See help(type(self)) for accurate signature.
-
copy
()[source] create a deep copy (except for rigid terms and variables)
-
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. collect uses the simplified version of the expression.
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 symbol declarations in self, ignoring type constraints
returns Dict[name, Declaration]
-
collect_nested_symbols
(symbols, is_nested)[source] 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}
-
generate_constructors
(constructors)[source] fills the list constructors with all constructors belonging to open types.
- Parameters
constructors (dict) –
-
co_constraints
(co_constraints)[source] collects the constraints attached to AST nodes, e.g. instantiated definitions
co_constraints is an OrderedSet of Expression
-
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.
-
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
-
instantiate
(e0, e1, problem=None) Recursively substitute Variable in e0 by e1 in a copy of self.
Interpret appliedSymbols immediately if grounded (and not occurring in head of definition). Update .variables.
-
instantiate1
(e0, e1, problem=None) Recursively substitute Variable in e0 by e1 in self.
Interpret appliedSymbols immediately if grounded (and not occurring in head of definition). Update .variables.
-
simplify_with
(assignments) 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 (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, using .value and .simpler if present
- 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
-
as_set_condition
()[source] Returns an equivalent expression of the type “x in y”, or None
- Returns
meaning “expr is (not) in enumeration”
- Return type
Tuple[Optional[AppliedSymbol], Optional[bool], Optional[Enumeration]]
-
split_equivalences
()[source] Returns an equivalent expression where equivalences are replaced by implications
- Returns
Expression
-
add_level_mapping
(level_symbols, head, pos_justification, polarity)[source] - 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.
- Returns
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
- Returns
an equivalent AST node, with updated type, .variables
- Return type
Expression
-
annotate1
() annotations that are common to __init__ and make()
-
interpret
(problem) uses information in the problem and its vocabulary to: - expand quantifiers in the expression - simplify the expression using known assignments and enumerations - instantiate definitions
- Parameters
problem (Theory) – the Theory to apply
- Returns
the resulting expression
- Return type
Expression
-
-
class
Constructor
(**kwargs)[source] Bases:
idp_engine.Expression.ASTNode
Constructor declaration
-
name
name of the constructor
- Type
string
-
sorts
types of the arguments of the constructor
- Type
List[Symbol]
-
type
name of the type that contains this constructor
- Type
string
-
arity
number of arguments of the constructor
- Type
Int
-
tester
function to test if the constructor
- Type
SymbolDeclaration
-
has been applied to some arguments
- Type
e.g., is_rgb
-
symbol
only for Symbol constructors
- Type
Symbol
-
__init__
(**kwargs)[source] Initialize self. See help(type(self)) for accurate signature.
-
-
class
AIfExpr
(**kwargs)[source] Bases:
idp_engine.Expression.Expression
-
__init__
(**kwargs)[source] Initialize self. See help(type(self)) for accurate signature.
-
collect_nested_symbols
(symbols, is_nested)[source] 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}
-
translate1
(problem, vars={}) Converts the syntax tree to a Z3 expression, ignoring .value and .simpler
- 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
Quantee
(**kwargs)[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]
-
vars
the (tuples of) variables being quantified
- Type
List[List[Variable]
-
domain
a literal Domain to quantify over, e.g., Color or Concept[Color->Bool].
- Type
Domain, 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__
(**kwargs)[source] Initialize self. See help(type(self)) for accurate signature.
-
-
class
AQuantification
(**kwargs)[source] Bases:
idp_engine.Expression.Expression
-
__init__
(**kwargs)[source] Initialize self. See help(type(self)) for accurate signature.
-
classmethod
make
(q, quantees, f, annotations=None)[source] make and annotate a quantified formula
-
copy
()[source] create a deep copy (except for rigid terms and variables)
-
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. collect uses the simplified version of the expression.
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 symbol declarations in self, ignoring type constraints
returns Dict[name, Declaration]
-
interpret
(problem) apply information in the problem and its vocabulary
- Parameters
problem (Theory) – the problem to be applied
- Returns
the expanded quantifier expression
- Return type
Expression
-
-
class
Operator
(**kwargs)[source] Bases:
idp_engine.Expression.Expression
-
__init__
(**kwargs)[source] Initialize self. See help(type(self)) for accurate signature.
-
classmethod
make
(ops, operands, annotations=None)[source] creates a BinaryOp beware: cls must be specific for ops !
-
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. collect uses the simplified version of the expression.
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)[source] 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}
-
-
class
AImplication
(**kwargs)[source] Bases:
idp_engine.Expression.Operator
-
add_level_mapping
(level_symbols, head, pos_justification, polarity)[source] - 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.
- Returns
Expression
-
-
class
AEquivalence
(**kwargs)[source] Bases:
idp_engine.Expression.Operator
-
split_equivalences
()[source] Returns an equivalent expression where equivalences are replaced by implications
- Returns
Expression
-
-
class
ARImplication
(**kwargs)[source] Bases:
idp_engine.Expression.Operator
-
add_level_mapping
(level_symbols, head, pos_justification, polarity)[source] - 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.
- Returns
Expression
-
-
class
ADisjunction
(**kwargs)[source] Bases:
idp_engine.Expression.Operator
-
class
AConjunction
(**kwargs)[source] Bases:
idp_engine.Expression.Operator
-
class
AComparison
(**kwargs)[source] Bases:
idp_engine.Expression.Operator
-
__init__
(**kwargs)[source] Initialize self. See help(type(self)) for accurate signature.
-
is_assignment
()[source] Returns: bool: True if self assigns a rigid term to a rigid function application
-
-
class
ASumMinus
(**kwargs)[source] Bases:
idp_engine.Expression.Operator
-
class
AMultDiv
(**kwargs)[source] Bases:
idp_engine.Expression.Operator
-
class
APower
(**kwargs)[source] Bases:
idp_engine.Expression.Operator
-
class
AUnary
(**kwargs)[source] Bases:
idp_engine.Expression.Expression
-
__init__
(**kwargs)[source] Initialize self. See help(type(self)) for accurate signature.
-
add_level_mapping
(level_symbols, head, pos_justification, polarity)[source] - 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.
- Returns
Expression
-
-
class
AAggregate
(**kwargs)[source] Bases:
idp_engine.Expression.Expression
-
__init__
(**kwargs)[source] Initialize self. See help(type(self)) for accurate signature.
-
copy
()[source] create a deep copy (except for rigid terms and variables)
-
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. collect uses the simplified version of the expression.
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 symbol declarations in self, ignoring type constraints
returns Dict[name, Declaration]
-
collect_nested_symbols
(symbols, is_nested)[source] 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}
-
-
class
AppliedSymbol
(**kwargs)[source] Bases:
idp_engine.Expression.Expression
Represents a symbol applied to arguments
- Parameters
symbol (Expression) – the symbol to be applied to arguments
is_enumerated (string) – ‘’ or ‘is enumerated’ or ‘is not enumerated’
is_enumeration (string) – ‘’ or ‘in’ or ‘not in’
in_enumeration (Enumeration) – the enumeration following ‘in’
decl (Declaration) – the declaration of the symbol, if known
in_head (Bool) – True if the AppliedSymbol occurs in the head of a rule
-
__init__
(**kwargs)[source] Initialize self. See help(type(self)) for accurate signature.
-
copy
()[source] create a deep copy (except for rigid terms and variables)
-
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. collect uses the simplified version of the expression.
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 symbol declarations in self, ignoring type constraints
returns Dict[name, Declaration]
-
collect_nested_symbols
(symbols, is_nested)[source] 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}
-
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)[source] - 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.
- Returns
Expression
-
substitute
(e0, e1, assignments, tag=None) recursively substitute e0 by e1 in self
-
class
UnappliedSymbol
(**kwargs)[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().
-
__init__
(**kwargs)[source] Initialize self. See help(type(self)) for accurate signature.
-
classmethod
construct
(constructor)[source] Create an UnappliedSymbol from a constructor
- Parameters
constructor (idp_engine.Expression.Constructor) –
-
-
class
Variable
(**kwargs)[source] Bases:
idp_engine.Expression.Expression
AST node for a variable in a quantification or aggregate
- Parameters
name (str) – name of the variable
sort (Optional[Symbol]) – sort of the variable, if known
-
__init__
(**kwargs)[source] Initialize self. See help(type(self)) for accurate signature.
-
copy
()[source] create a deep copy (except for rigid terms and variables)
-
annotate1
()[source] annotations that are common to __init__ and make()