idp_engine.Expression¶
(They are monkeypatched 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 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 IDPZ3 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

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

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

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: 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, tag=None)¶ recursively substitute e0 by e1 in self (e0 is not a Variable)
if tag is present, updates assignments with symbolic propagation of coconstraints.
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: idp_engine.Assignments.Assignments) → idp_engine.Expression.Expression¶ simplify the expression using the assignments

symbolic_propagate
(assignments: Assignments, tag: Status, truth: Optional[idp_engine.Expression.Expression] = 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.

propagate1
(assignments, tag, truth)¶ returns the list of symbolic_propagate of self, ignoring value and simpler

translate
(problem: Problem, vars={}) → z3.z3.ExprRef¶ Converts the syntax tree to a Z3 expression, using .value and .simpler if present
 Parameters
problem (Problem) – 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
() → 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]]

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

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


class
idp_engine.Expression.
IfExpr
(**kwargs)[source]¶ Bases:
idp_engine.Expression.Expression

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: Problem, vars={}) → z3.z3.ExprRef¶ Converts the syntax tree to a Z3 expression, ignoring .value and .simpler
 Parameters
problem (Problem) – 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
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

If the type is "Concept" with a particular signature, it is followed by the types in the signature.

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 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 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.
Operator
(**kwargs)[source]¶ Bases:
idp_engine.Expression.Expression

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

classmethod

class
idp_engine.Expression.
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
idp_engine.Expression.
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
idp_engine.Expression.
AUnary
(**kwargs)[source]¶ Bases:
idp_engine.Expression.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


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

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

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: dict)[source]¶ fills the list constructors with all constructors belonging to open types.

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