idp_solver.Expression

(They are monkey-patched by other modules)

class idp_solver.Expression.Expression[source]

Bases: idp_solver.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())) 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()[source]

create a deep copy (except for Constructor and Number)

annotate(voc, q_vars)[source]

annotate tree after parsing

annotate1()[source]

annotations that are common to __init__ and make()

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

generate_constructors(constructors: dict)[source]

fills the list constructors with all constructors belonging to open types.

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

as_rigid()[source]

returns a Number or Constructor, or None

is_assignment() → bool[source]
Returns

True if self assigns a rigid term to a rigid function application

Return type

bool

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)

recursively substitute 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(problem)idp_solver.Expression.Expression

uses information in the problem and its vocabulary to: - expand quantifiers in the expression - simplify the expression using known assignments - instantiate definitions

Parameters

problem (Problem) – the Problem to apply

Returns

the resulting expression

Return type

Expression

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

as_rigid()[source]

returns a Number or Constructor, or None

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class idp_solver.Expression.IfExpr(**kwargs)[source]

Bases: idp_solver.Expression.Expression

annotate1()[source]

annotations that are common to __init__ and make()

class idp_solver.Expression.AQuantification(**kwargs)[source]

Bases: idp_solver.Expression.Expression

classmethod make(q, q_vars, f)[source]

make and annotate a quantified formula

annotate(voc, q_vars)[source]

annotate tree after parsing

annotate1()[source]

annotations that are common to __init__ and make()

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

class idp_solver.Expression.BinaryOperator(**kwargs)[source]

Bases: idp_solver.Expression.Expression

classmethod make(ops, operands)[source]

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

annotate1()[source]

annotations that are common to __init__ and make()

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

class idp_solver.Expression.AImplication(**kwargs)[source]

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.AEquivalence(**kwargs)[source]

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.ARImplication(**kwargs)[source]

Bases: idp_solver.Expression.BinaryOperator

annotate(voc, q_vars)[source]

annotate tree after parsing

class idp_solver.Expression.ADisjunction(**kwargs)[source]

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.AConjunction(**kwargs)[source]

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.AComparison(**kwargs)[source]

Bases: idp_solver.Expression.BinaryOperator

annotate(voc, q_vars)[source]

annotate tree after parsing

is_assignment()[source]

Returns: bool: True if self assigns a rigid term to a rigid function application

class idp_solver.Expression.ASumMinus(**kwargs)[source]

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.AMultDiv(**kwargs)[source]

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.APower(**kwargs)[source]

Bases: idp_solver.Expression.BinaryOperator

class idp_solver.Expression.AUnary(**kwargs)[source]

Bases: idp_solver.Expression.Expression

annotate1()[source]

annotations that are common to __init__ and make()

class idp_solver.Expression.AAggregate(**kwargs)[source]

Bases: idp_solver.Expression.Expression

annotate(voc, q_vars)[source]

annotate tree after parsing

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

class idp_solver.Expression.AppliedSymbol(**kwargs)[source]

Bases: idp_solver.Expression.Expression

annotate(voc, q_vars)[source]

annotate tree after parsing

annotate1()[source]

annotations that are common to __init__ and make()

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

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

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class idp_solver.Expression.UnappliedSymbol(**kwargs)[source]

Bases: idp_solver.Expression.Expression

The result of parsing a symbol not applied to arguments. Can be a constructor, a quantified variable, or a symbol application without arguments (by abuse of notation, e.g. ‘p’). (The parsing of numbers result directly in Number nodes)

Converted to the proper AST class by annotate().

annotate(voc, q_vars)[source]

annotate tree after parsing

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

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class idp_solver.Expression.Variable(name, sort)[source]

Bases: idp_solver.Expression.Expression

AST node for a variable in a quantification or aggregate

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class idp_solver.Expression.Number(**kwargs)[source]

Bases: idp_solver.Expression.Expression

as_rigid()[source]

returns a Number or Constructor, or None

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class idp_solver.Expression.Brackets(**kwargs)[source]

Bases: idp_solver.Expression.Expression

as_rigid()[source]

returns a Number or Constructor, or None

annotate1()[source]

annotations that are common to __init__ and make()