idp_engine.Expression¶
(They are monkey-patched by other modules)
-
class
idp_engine.Expression.
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
-
-
class
idp_engine.Expression.
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 source code.
annotations['reading']
is the annotation giving the intended meaning of the expression (in English).- Type
Dict
-
original
¶ The original expression, before propagation and simplification.
- Type
-
fresh_vars
¶ The set of names of the variables in the expression.
- Type
Set(string)
-
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, IfExpr, 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]
-
generate_constructors
(constructors: dict)[source]¶ fills the list constructors with all constructors belonging to open types.
-
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
() → bool[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, todo=None)¶ recursively substitute e0 by e1 in self (e0 is not a Variable)
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 fresh_vars.
-
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 fresh_vars.
-
symbolic_propagate
(assignments: idp_engine.Assignments.Assignments, truth: Optional[idp_engine.Expression.Expression] = true) → List[Tuple[idp_engine.Expression.Expression]]¶ returns the consequences of self=truth that are in assignments.
The consequences are obtained by symbolic processing (no calls to Z3).
- Parameters
assignments (Assignments) – The set of questions to chose from. Their value is ignored.
truth (Expression, optional) – The truth value of the expression self. Defaults to TRUE.
- Returns
A list of pairs (Expression, bool), descring the literals that are implicant
-
propagate1
(assignments, truth)¶ returns the list of symbolic_propagate of self (default implementation)
-
as_set_condition
() → Tuple[Optional[AppliedSymbol], Optional[bool], Optional[Enumeration]][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]]
-
annotate
(voc, q_vars)¶ annotate tree after parsing
-
annotate1
()¶ annotations that are common to __init__ and make()
-
interpret
(problem) → idp_engine.Expression.Expression¶ 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 (Problem) – the Problem to apply
- Returns
the resulting expression
- Return type
-
-
class
idp_engine.Expression.
Constructor
(**kwargs)[source]¶ Bases:
idp_engine.Expression.ASTNode
Constructor declaration
-
name
¶ name of the constructor
- Type
string
-
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
-
has been applied to some arguments
- Type
e.g., is_rgb
-
translated
¶ the value in Z3
- Type
DataTypeRef
-
-
class
idp_engine.Expression.
Quantee
(**kwargs)[source]¶ Bases:
idp_engine.Expression.Expression
represents the description of quantification, e.g., x in T or (x,y) in P
-
sub_exprs
¶ the type or predicate to quantify over
- Type
List[SymbolExpr], Optional
-
arity
¶ the length of the tuple of variable
- Type
int
-
-
class
idp_engine.Expression.
AQuantification
(**kwargs)[source]¶ Bases:
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. 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, IfExpr, 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]
-
-
class
idp_engine.Expression.
BinaryOperator
(**kwargs)[source]¶ Bases:
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. 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, IfExpr, AUnary, Variable, Number_constant, Brackets
-
-
class
idp_engine.Expression.
AAggregate
(**kwargs)[source]¶ Bases:
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. 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, IfExpr, AUnary, Variable, Number_constant, Brackets
-
-
class
idp_engine.Expression.
AppliedSymbol
(**kwargs)[source]¶ Bases:
idp_engine.Expression.Expression
Represents a symbol applied to arguments
- Parameters
eval (string) – ‘$’ if the symbol must be evaluated, else ‘’
s (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
-
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, IfExpr, 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]
-
generate_constructors
(constructors: dict)[source]¶ fills the list constructors with all constructors belonging to open types.
-
substitute
(e0, e1, assignments, todo=None)¶ recursively substitute e0 by e1 in self
-
class
idp_engine.Expression.
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().
-
classmethod
construct
(constructor: idp_engine.Expression.Constructor)[source]¶ Create an UnappliedSymbol from a constructor
-
classmethod
-
class
idp_engine.Expression.
Variable
(**kwargs)[source]¶ Bases:
idp_engine.Expression.Expression
AST node for a variable in a quantification or aggregate