idp_solver.Expression

(They are monkey-patched by other modules)

class idp_solver.Expression.Expression

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 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())) is square(length(top())) = length(top())*length(top())., assuming square 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)

copy()

create a deep copy (except for Constructor and NumberConstant)

annotate(voc, q_vars)

annotate tree after parsing

annotate1()

annotations that are common to __init__ and make()

collect(questions, all_=True, co_constraints=True)

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

unknown_symbols(co_constraints=True)

returns the list of symbol declarations in self, ignoring type constraints

returns Dict[name, Declaration]

co_constraints(co_constraints)

collects the constraints attached to AST nodes, e.g. instantiated definitions

`co_constraints is an OrderedSet of Expression

as_rigid()

returns a NumberConstant or Constructor, or None

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 co-constraint

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]]

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)

Bases: idp_solver.Expression.Expression

as_rigid()

returns a NumberConstant or Constructor, or None

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class idp_solver.Expression.IfExpr(**kwargs)

Bases: idp_solver.Expression.Expression

annotate1()

annotations that are common to __init__ and make()

class idp_solver.Expression.AQuantification(**kwargs)

Bases: idp_solver.Expression.Expression

classmethod make(q, q_vars, f)

make and annotate a quantified formula

annotate(voc, q_vars)

annotate tree after parsing

annotate1()

annotations that are common to __init__ and make()

collect(questions, all_=True, co_constraints=True)

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

class idp_solver.Expression.BinaryOperator(**kwargs)

Bases: idp_solver.Expression.Expression

classmethod make(ops, operands)

creates a BinaryOp beware: cls must be specific for ops !

annotate1()

annotations that are common to __init__ and make()

collect(questions, all_=True, co_constraints=True)

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

class idp_solver.Expression.AImplication(**kwargs)

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.AEquivalence(**kwargs)

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.ARImplication(**kwargs)

Bases: idp_solver.Expression.BinaryOperator

annotate(voc, q_vars)

annotate tree after parsing

class idp_solver.Expression.ADisjunction(**kwargs)

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.AConjunction(**kwargs)

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.AComparison(**kwargs)

Bases: idp_solver.Expression.BinaryOperator

annotate(voc, q_vars)

annotate tree after parsing

annotate1()

annotations that are common to __init__ and make()

class idp_solver.Expression.ASumMinus(**kwargs)

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.AMultDiv(**kwargs)

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.APower(**kwargs)

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.AUnary(**kwargs)

Bases: idp_solver.Expression.Expression

annotate1()

annotations that are common to __init__ and make()

class idp_solver.Expression.AAggregate(**kwargs)

Bases: idp_solver.Expression.Expression

annotate(voc, q_vars)

annotate tree after parsing

collect(questions, all_=True, co_constraints=True)

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

class idp_solver.Expression.AppliedSymbol(**kwargs)

Bases: idp_solver.Expression.Expression

annotate(voc, q_vars)

annotate tree after parsing

annotate1()

annotations that are common to __init__ and make()

collect(questions, all_=True, co_constraints=True)

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 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)

Bases: idp_solver.Expression.AppliedSymbol

annotate(voc, q_vars)

annotate tree after parsing

collect(questions, all_=True, co_constraints=True)

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 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)

Bases: idp_solver.Expression.Expression

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class idp_solver.Expression.NumberConstant(**kwargs)

Bases: idp_solver.Expression.Expression

as_rigid()

returns a NumberConstant or Constructor, or None

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class idp_solver.Expression.Brackets(**kwargs)

Bases: idp_solver.Expression.Expression

as_rigid()

returns a NumberConstant or Constructor, or None

annotate1()

annotations that are common to __init__ and make()