idp_solver.Expression¶
(They are monkeypatched by other modules)

class
idp_solver.Expression.
Expression
[source]¶ Bases:
object
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 subtree. 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 transformation.
Type: Expression

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 subformula 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 Constructor, IfExpr, AUnary, Fresh_Variable, Number_constant, Brackets

unknown_symbols
(co_constraints=True)[source]¶ returns the list of symbol declarations in self, ignoring type constraints
returns Dict[name, Declaration]

co_constraints
(co_constraints)[source]¶ collects the constraints attached to AST nodes, e.g. instantiated definitions
`co_constraints is an OrderedSet of Expression

substitute
(e0, e1, assignments, todo=None)¶ recursively substitute e0 by e1 in self (e0 is not a Fresh_Variable)
implementation for everything but AppliedSymbol, Variable and Fresh_variable

instantiate
(e0, e1, theory)¶ recursively substitute Fresh_Variable e0 by e1 in self
instantiating e0=`x by e1=`f in self=`x(y) returns f(y) (or any instance of f if arities don’t match)

interpret
(theory)¶ for every defined term in self, add the instantiated definition as coconstraint
implementation for everything but AppliedSymbol, Variable and Fresh_variable

expand_quantifiers
(theory)¶ replaces quantified formula by its expansion
implementation for everything but AQuantification and AAgregate

symbolic_propagate
(assignments: idp_solver.Assignments.Assignments, truth: Optional[idp_solver.Expression.Constructor] = true) → List[Tuple[idp_solver.Expression.Expression, idp_solver.Expression.Constructor]]¶ 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 (Constructor, 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]]


class
idp_solver.Expression.
Constructor
(**kwargs)[source]¶ Bases:
idp_solver.Expression.Expression

update_exprs
(new_exprs)¶ change sub_exprs and simplify, while keeping relevant info.


class
idp_solver.Expression.
AQuantification
(**kwargs)[source]¶ Bases:
idp_solver.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 subformula 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 Constructor, IfExpr, AUnary, Fresh_Variable, Number_constant, Brackets


class
idp_solver.Expression.
BinaryOperator
(**kwargs)[source]¶ Bases:
idp_solver.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 subformula 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 Constructor, IfExpr, AUnary, Fresh_Variable, Number_constant, Brackets


class
idp_solver.Expression.
AAggregate
(**kwargs)[source]¶ Bases:
idp_solver.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 subformula 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 Constructor, IfExpr, AUnary, Fresh_Variable, Number_constant, Brackets


class
idp_solver.Expression.
AppliedSymbol
(**kwargs)[source]¶ Bases:
idp_solver.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 subformula 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 Constructor, IfExpr, AUnary, Fresh_Variable, Number_constant, Brackets

substitute
(e0, e1, assignments, todo=None)¶ recursively substitute e0 by e1 in self

update_exprs
(new_exprs)¶ change sub_exprs and simplify, while keeping relevant info.


class
idp_solver.Expression.
Variable
(**kwargs)[source]¶ Bases:
idp_solver.Expression.AppliedSymbol

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 subformula 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 Constructor, IfExpr, AUnary, Fresh_Variable, Number_constant, Brackets

substitute
(e0, e1, assignments, todo=None)¶ recursively substitute e0 by e1 in self

update_exprs
(new_exprs)¶ change sub_exprs and simplify, while keeping relevant info.


class
idp_solver.Expression.
Fresh_Variable
(name, sort)[source]¶ Bases:
idp_solver.Expression.Expression

update_exprs
(new_exprs)¶ change sub_exprs and simplify, while keeping relevant info.


class
idp_solver.Expression.
NumberConstant
(**kwargs)[source]¶ Bases:
idp_solver.Expression.Expression

update_exprs
(new_exprs)¶ change sub_exprs and simplify, while keeping relevant info.
