idp_engine.Expression

This module contains the ASTNode classes for expressions. Note that many methods are imported from other modules, as done at the top of each class.

class ASTNode

Bases: object

superclass of all AST nodes

check(condition, msg)

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

dedup_nodes(kwargs, arg_name)

pops arg_name from kwargs as a list of named items and returns a mapping from name to items

Parameters

• kwargs (dict[str, List[ASTNode]]) – dictionary mapping named arguments to list of ASTNodes

• arg_name (str) – name of the kwargs argument, e.g. “interpretations”

Returns

mapping from name to AST nodes

Return type

dict[str, ASTNode]

Raises

AssertionError – in case of duplicate name

class Annotations(parent, annotations)

Bases: idp_engine.Expression.ASTNode

Parameters

annotations (List[str]) –

__init__(parent, annotations)

Parameters

annotations (List[str]) –

class Accessor(parent, out, accessor=None)

Bases: idp_engine.Expression.ASTNode

represents an accessor and a type

Parameters

• out (SetName) –

• accessor (Optional[str]) –

accessor

name of accessor function

Type

str, Optional

codomain

name of the output type of the accessor

Type

SetName

decl

declaration of the accessor function

Type

SymbolDeclaration

__init__(parent, out, accessor=None)

Parameters

• out (idp_engine.Expression.SetName) –

• accessor (Optional[str]) –

class Expression(parent=None, annotations=None)

Bases: idp_engine.Expression.ASTNode

The abstract class of AST nodes representing (sub-)expressions.

Parameters

• parent (Optional[ASTNode]) –

• annotations (Optional[Annotations]) –

code

Textual representation of the expression. Often used as a key.

It is generated from the sub-tree.

Type

string

str

Textual representation of the simplified expression.

Type

string

sub_exprs

The children of the AST node.

The list may be reduced by simplification.

Type

List[Expression]

type

The type of the expression, e.g., bool.

Type

SetName, Optional

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

annotations

The set of annotations given by the expert in the IDP-Z3 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

Expression

variables

The set of names of the variables in the expression, before interpretation.

Type

Set(string)

is_type_constraint_for

name of the symbol for which the expression is a type constraint

Type

string

WDF

a formula that is true only when self is well-defined (for partial functions)

Type

Expression, optional

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

• self (Expr.Expression) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.Expression) –

Return type

idp_engine.Expression.Expression

add_level_mapping(level_symbols, head, pos_justification, polarity, mode)

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.

• self (Expr.Expression) –

• mode (Semantics) –

Return type

Expr.Expression

collect_nested_symbols(symbols, is_nested)

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 {Parse.SymbolDeclaration}

Parameters

• self (idp_engine.Expression.Expression) –

• symbols (Set[idp_engine.Parse.SymbolDeclaration]) –

• is_nested (bool) –

Return type

Set[idp_engine.Parse.SymbolDeclaration]

translate(problem, vars={})

Converts the syntax tree to a Z3 expression, with lookup in problem.z3

Parameters

• problem (Theory) – 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

interpret(problem, subs)

expand quantifiers and replace symbols interpreted in the structure by their interpretation

Parameters

• self (Expr.Expression) – the expression to be interpreted

• problem (Optional[Theory]) – the theory to be applied

• subs (dict[str, Expr.Expression]) – a dictionary mapping variable names to their value

Returns

the interpreted expression

Return type

Expression

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.Expression) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

propagate1(assignments, tag, truth)

returns the list of symbolic_propagate of self, ignoring value and simpler

simplify_with(assignments, co_constraints_too=True)

simplify the expression using the assignments

Parameters

• self (Expr.Expression) –

• assignments (Assignments) –

Return type

Expr.Expression

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 co-constraints.

implementation for everything but AppliedSymbol, UnappliedSymbol and Fresh_variable

symbolic_propagate(assignments, tag, truth=None)

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.

• tag (Status) –

fill_WDF()

Compute the Well-definedness condition of an Expression

Parameters

self (idp_engine.Expression.Expression) –

Return type

idp_engine.Expression.Expression

merge_WDFs()

Combine the WDF of the sub-expressions of self

Parameters

self (idp_engine.Expression.Expression) –

Return type

idp_engine.Expression.Expression

__init__(parent=None, annotations=None)

Parameters

• parent (Optional[idp_engine.Expression.ASTNode]) –

• annotations (Optional[idp_engine.Expression.Annotations]) –

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.

all_=False : ignore expanded formulas and AppliedSymbol interpreted in a structure

co_constraints=False : ignore co_constraints

default implementation for UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets

Parameters

• questions (idp_engine.utils.OrderedSet) –

• all_ (bool) –

• co_constraints (bool) –

collect_symbols(symbols=None, co_constraints=True)

returns the list of symbols occurring in self, ignoring type constraints and symbols created by aggregates

Parameters

• symbols (Optional[dict[str, SymbolDeclaration]]) –

• co_constraints (bool) –

Return type

dict[str, SymbolDeclaration]

generate_constructors(constructors)

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

Parameters

constructors (dict[str, List[Constructor]]) –

collect_co_constraints(co_constraints, recursive=True)

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

Parameters

• recursive – if True, collect co_constraints of co_constraints too

• co_constraints (idp_engine.utils.OrderedSet) –

is_value()

True for numerals, date, identifiers, and constructors applied to values.

Synomym: “is ground”, “is rigid”

Returns

True if self represents a value.

Return type

bool

is_reified()

False for values and for symbols applied to values.

Returns

True if self has to be reified to obtain its value in a Z3 model.

Return type

bool

is_assignment()

Returns

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

Return type

bool

as_set_condition()

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

Returns an equivalent expression where equivalences are replaced by implications

Returns

Expression

Return type

idp_engine.Expression.Expression

class Constructor(parent, name, args=None)

Bases: idp_engine.Expression.ASTNode

Constructor declaration

Parameters

• parent (Optional[ASTNode]) –

• name (str) –

• args (Optional[List[Accessor]]) –

name

name of the constructor

Type

string

args

Type

List[Accessor]

sorts

types of the arguments of the constructor

Type

List[SetName]

out

type that contains this constructor

Type

SetName

arity

number of arguments of the constructor

Type

Int

tester

function to test if the constructor

Type

SymbolDeclaration, Optional

has been applied to some arguments

Type

e.g., is_rgb

concept_decl

declaration with name[1:],

Type

SymbolDeclaration, Optional

only for Concept constructors.

range

the list of identifiers

prefix

the constructor’s prefix

Type

str, Optional

__init__(parent, name, args=None)

Parameters

• parent (Optional[idp_engine.Expression.ASTNode]) –

• name (str) –

• args (Optional[List[idp_engine.Expression.Accessor]]) –

class SetName(parent, name, ins=None, out=None)

Bases: idp_engine.Expression.Expression

ASTNode representing a (sub-)type or a Concept[aSignature], e.g., Concept[T*T->Bool]

Inherits from Expression

Parameters

• name (str) – name of the concept

• concept_domains (List[SetName], Optional) – domain of the Concept signature, e.g., [T, T]

• codomain (SetName, Optional) – range of the Concept signature, e.g., Bool

• decl (Declaration, Optional) – declaration of the type

• root_set (List[SetName]) – cross-product of root sets that include this set. Used for type checking.

• ins (Optional[List[SetName]]) –

• out (Optional[SetName]) –

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

• self (Expr.Expression) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

translate(problem, vars={})

Converts the syntax tree to a Z3 expression, with lookup in problem.z3

Parameters

• problem (Theory) – 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

extension(extensions)

returns the extension of a SetName, given some interpretations.

Normally, the extension is already in extensions by SymbolDeclaration.interpret. However, for Concept[T->T], an additional filtering is applied.

Parameters

• interpretations (dict[str, SymbolInterpretation]) –

• symbols (the known interpretations of types and) –

• extensions (dict[str, Expr.Extension]) –

Returns

a superset of the extension of self, and a function that, given arguments, returns an Expression that says whether the arguments are in the extension of self

Return type

Extension

__init__(parent, name, ins=None, out=None)

Parameters

• name (str) –

• ins (Optional[List[idp_engine.Expression.SetName]]) –

• out (Optional[idp_engine.Expression.SetName]) –

is_value()

True for numerals, date, identifiers, and constructors applied to values.

Synomym: “is ground”, “is rigid”

Returns

True if self represents a value.

Return type

bool

has_element(term, extensions)

Returns an Expression that says whether term is in the type/predicate denoted by self.

Parameters

• term (Expression) – the argument to be checked

• extensions (dict[str, Extension]) –

Returns

whether term term is in the type denoted by self.

Return type

Expression

class AIfExpr(parent, if_f, then_f, else_f)

Bases: idp_engine.Expression.Expression

Parameters

• if_f (Expression) –

• then_f (Expression) –

• else_f (Expression) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.AIfExpr) –

Return type

idp_engine.Expression.Expression

collect_nested_symbols(symbols, is_nested)

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 {Parse.SymbolDeclaration}

Parameters

• self (idp_engine.Expression.AIfExpr) –

• symbols (Set[idp_engine.Parse.SymbolDeclaration]) –

• is_nested (bool) –

Return type

Set[idp_engine.Parse.SymbolDeclaration]

translate1(problem, vars={})

Converts the syntax tree to a Z3 expression, without lookup in problem.z3

A lookup is wasteful when self is a subformula of a formula that is not in problem.z3.

Parameters

• problem (Theory) – 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

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.AIfExpr) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

merge_WDFs()

Combine the WDF of the sub-expressions of self

__init__(parent, if_f, then_f, else_f)

Parameters

• if_f (idp_engine.Expression.Expression) –

• then_f (idp_engine.Expression.Expression) –

• else_f (idp_engine.Expression.Expression) –

class Quantee(parent, vars, subtype=None, sort=None)

Bases: idp_engine.Expression.Expression

represents the description of quantification, e.g., x in T or (x,y) in P The Concept type may be qualified, e.g. Concept[Color->Bool]

Parameters

• vars (Union[List[Variable], List[List[Variable]]]) –

• subtype (Optional[SetName]) –

• sort (Optional[SymbolExpr]) –

vars

the (tuples of) variables being quantified

Type

List[List[Variable]]

subtype

a literal SetName to quantify over, e.g., Color or Concept[Color->Bool].

Type

SetName, Optional

sort

a dereferencing expression, e.g.,. $(i).

Type

SymbolExpr, Optional

sub_exprs

the (unqualified) type or predicate to quantify over,

Type

List[SymbolExpr], Optional

e.g., `[Color], [Concept] or [$

Type

i

arity

the length of the tuple of variables

Type

int

decl

the (unqualified) Declaration to quantify over, after resolution of $(i).

Type

SymbolDeclaration, Optional

e.g., the declaration of `Color`

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.AQuantification) –

Return type

idp_engine.Expression.Expression

translate(problem, vars={})

Converts the syntax tree to a Z3 expression, with lookup in problem.z3

Parameters

• problem (Theory) – 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

__init__(parent, vars, subtype=None, sort=None)

Parameters

• vars (Union[List[idp_engine.Expression.Variable], List[List[idp_engine.Expression.Variable]]]) –

• subtype (Optional[idp_engine.Expression.SetName]) –

• sort (Optional[idp_engine.Expression.SymbolExpr]) –

split_quantees(self)

replaces an untyped quantee x,y,z into 3 quantees, so that each variable can have its own sort

Parameters

self – either a AQuantification, AAggregate or Rule

class AQuantification(parent, annotations, q, quantees, f)

Bases: idp_engine.Expression.Expression

ASTNode representing a quantified formula

Parameters

• annotations (dict[str, str]) –

  The set of annotations given by the expert in the IDP-Z3 program.

  annotations['reading'] is the annotation giving the intended meaning of the expression (in English).

• q (str) – either ‘∀’ or ‘∃’

• quantees (List[Quantee]) – list of variable declarations

• f (Expression) – the formula being quantified

• supersets – attributes used in interpret

• new_quantees – attributes used in interpret

• vars1 – attributes used in interpret

• parent (Optional[ASTNode]) –

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

• self (Expr.Expression) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.AQuantification) –

Return type

idp_engine.Expression.Expression

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.AQuantification) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

Union[idp_engine.Expression.AConjunction, idp_engine.Expression.ADisjunction]

merge_WDFs()

Combine the WDF of the sub-expressions of self

__init__(parent, annotations, q, quantees, f)

Parameters

• parent (Optional[idp_engine.Expression.ASTNode]) –

• annotations (Optional[idp_engine.Expression.Annotations]) –

• q (str) –

• quantees (List[idp_engine.Expression.Quantee]) –

• f (idp_engine.Expression.Expression) –

classmethod make(q, quantees, f, annotations=None)

make and annotate a quantified formula

Parameters

• q (str) –

• quantees (List[idp_engine.Expression.Quantee]) –

• f (idp_engine.Expression.Expression) –

• annotations (Optional[Dict[str, Union[str, Dict[str, Any]]]]) –

Return type

AQuantification

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.

all_=False : ignore expanded formulas and AppliedSymbol interpreted in a structure

co_constraints=False : ignore co_constraints

default implementation for UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets

collect_symbols(symbols=None, co_constraints=True)

returns the list of symbols occurring in self, ignoring type constraints and symbols created by aggregates

class AGenExist(parent, annotations, q, operator, number, quantees, f)

Bases: idp_engine.Expression.Expression

Represents a generalised existential quantification of the form “∃ OP INT quantor: f”, with OP a comparison operator and INT an integer literal. It represents a shorthand for a cardinality, “#{OP: f} OP INT”. For example, “∃=1 c in Country: color_of(c) = Blue” states that there must be exactly one country that is assigned blue.

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

• self (Expression) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

__init__(parent, annotations, q, operator, number, quantees, f)

class Operator(parent, operator, sub_exprs, annotations=None)

Bases: idp_engine.Expression.Expression

Parameters

annotations (Optional[Annotations]) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.Operator) –

Return type

idp_engine.Expression.Expression

collect_nested_symbols(symbols, is_nested)

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 {Parse.SymbolDeclaration}

Parameters

• self (idp_engine.Expression.Operator) –

• symbols (Set[idp_engine.Parse.SymbolDeclaration]) –

• is_nested (bool) –

__init__(parent, operator, sub_exprs, annotations=None)

Parameters

annotations (Optional[idp_engine.Expression.Annotations]) –

classmethod make(ops, operands, annotations=None, parent=None)

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

Parameters

• ops (Union[str, List[str]]) –

• operands (List[idp_engine.Expression.Expression]) –

• annotations (Optional[Dict[str, Union[str, Dict[str, Any]]]]) –

Return type

idp_engine.Expression.Expression

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.

all_=False : ignore expanded formulas and AppliedSymbol interpreted in a structure

co_constraints=False : ignore co_constraints

default implementation for UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets

class AImplication(parent, operator, sub_exprs, annotations=None)

Bases: idp_engine.Expression.Operator

Parameters

annotations (Optional[Annotations]) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.AImplication) –

Return type

idp_engine.Expression.Expression

add_level_mapping(level_symbols, head, pos_justification, polarity, mode)

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.

• self (Expr.Expression) –

• mode (Semantics) –

Return type

Expr.Expression

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.AImplication) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

merge_WDFs()

Combine the WDF of the sub-expressions of self

class AEquivalence(parent, operator, sub_exprs, annotations=None)

Bases: idp_engine.Expression.Operator

Parameters

annotations (Optional[Annotations]) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.AEquivalence) –

Return type

idp_engine.Expression.Expression

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.AEquivalence) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

split_equivalences()

Returns an equivalent expression where equivalences are replaced by implications

Returns

Expression

class ARImplication(parent, operator, sub_exprs, annotations=None)

Bases: idp_engine.Expression.Operator

Parameters

annotations (Optional[Annotations]) –

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

• self (Expr.ARImplication) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

add_level_mapping(level_symbols, head, pos_justification, polarity, mode)

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.

• self (Expr.ARimplication) –

• mode (Semantics) –

Return type

Expr.Expression

class ADisjunction(parent, operator, sub_exprs, annotations=None)

Bases: idp_engine.Expression.Operator

Parameters

annotations (Optional[Annotations]) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.Expression) –

Return type

idp_engine.Expression.Expression

update_exprs(new_exprs, replace=True)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.Expression) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

• replace (bool) –

Return type

idp_engine.Expression.Expression

merge_WDFs()

Combine the WDF of the sub-expressions of self

class AConjunction(parent, operator, sub_exprs, annotations=None)

Bases: idp_engine.Expression.Operator

Parameters

annotations (Optional[Annotations]) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.Expression) –

Return type

idp_engine.Expression.Expression

update_exprs(new_exprs, replace=True)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.Expression) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

• replace (bool) –

Return type

idp_engine.Expression.Expression

propagate1(assignments, tag, truth=None)

returns the list of symbolic_propagate of self, ignoring value and simpler

merge_WDFs()

Combine the WDF of the sub-expressions of self

class AComparison(parent, operator, sub_exprs, annotations=None)

Bases: idp_engine.Expression.Operator

Parameters

annotations (Optional[Annotations]) –

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

• self (Expr.AComparison) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.AppliedSymbol) –

Return type

idp_engine.Expression.Expression

translate_acomparison_optimum(problem, lhs, op, rhs, vars={})

Optimized translation method for _very_ specific circumstances in which one child is a count and the other child is a literal int (or a symbol interpreted as one). This allows us to use Z3’s AtLeast and AtMost (https://z3prover.github.io/api/html/namespacez3py.html#a0369f15ecdb913e47fc7bb645fcfcf08) instead of converting the aggregate to a sum of ite’s.

Parameters

• problem (Theory) –

• lhs (Expr.Expression) –

• op (Expr.Expression) –

• rhs (Expr.Expression) –

Return type

ExprRef

as_set_condition()

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

Parameters

self (idp_engine.Expression.AComparison) –

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.AComparison) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

propagate1(assignments, tag, truth=None)

returns the list of symbolic_propagate of self, ignoring value and simpler

is_assignment()

Returns

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

Return type

bool

class ASumMinus(parent, operator, sub_exprs, annotations=None)

Bases: idp_engine.Expression.Operator

Parameters

annotations (Optional[Annotations]) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.ASumMinus) –

Return type

idp_engine.Expression.Expression

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.ASumMinus) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

class AMultDiv(parent, operator, sub_exprs, annotations=None)

Bases: idp_engine.Expression.Operator

Parameters

annotations (Optional[Annotations]) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.AMultDiv) –

Return type

idp_engine.Expression.Expression

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.AMultDiv) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

merge_WDFs()

Combine the WDF of the sub-expressions of self

class APower(parent, operator, sub_exprs, annotations=None)

Bases: idp_engine.Expression.Operator

Parameters

annotations (Optional[Annotations]) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.APower) –

Return type

idp_engine.Expression.Expression

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.APower) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

class AUnary(parent, operators, f)

Bases: idp_engine.Expression.Expression

Parameters

• operators (List[str]) –

• f (Expression) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.AUnary) –

Return type

idp_engine.Expression.Expression

add_level_mapping(level_symbols, head, pos_justification, polarity, mode)

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.

• self (Expr.AUnary) –

• mode (Semantics) –

Return type

Expr.Expression

as_set_condition()

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

Parameters

self (idp_engine.Expression.AUnary) –

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.AUnary) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

propagate1(assignments, tag, truth=None)

returns the list of symbolic_propagate of self, ignoring value and simpler

__init__(parent, operators, f)

Parameters

• operators (List[str]) –

• f (idp_engine.Expression.Expression) –

class AAggregate(parent, aggtype, quantees, term=None, condition=None)

Bases: idp_engine.Expression.Expression

Parameters

• parent (Optional[Expression]) –

• aggtype (str) –

• quantees (List[Quantee]) –

• term (Optional[Expression]) –

• condition (Optional[Expression]) –

annotate(voc, q_vars)

Annotation is dependent on the aggtype.

• Sum/card: the sub_exprs are replaced by equivalent ite expressions

• Min/max: the aggregate is replaced by an applied symbol representing the

  min/max, together with a set of co-constraints to define this.

Parameters

• self (Expr.AAggregate) –

• voc (Parse.Vocabulary) –

• q_vars (dict[str, Expr.Variable]) –

Return type

Expr.AAggregate | Expr.AppliedSymbol

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.AQuantification) –

Return type

idp_engine.Expression.Expression

collect_nested_symbols(symbols, is_nested)

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 {Parse.SymbolDeclaration}

Parameters

• self (idp_engine.Expression.AAggregate) –

• symbols (Set[idp_engine.Parse.SymbolDeclaration]) –

• is_nested (bool) –

Return type

Set[idp_engine.Parse.SymbolDeclaration]

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.AAggregate) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

merge_WDFs()

Combine the WDF of the sub-expressions of self

__init__(parent, aggtype, quantees, term=None, condition=None)

Parameters

• parent (Optional[idp_engine.Expression.Expression]) –

• aggtype (str) –

• quantees (List[idp_engine.Expression.Quantee]) –

• term (Optional[idp_engine.Expression.Expression]) –

• condition (Optional[idp_engine.Expression.Expression]) –

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.

all_=False : ignore expanded formulas and AppliedSymbol interpreted in a structure

co_constraints=False : ignore co_constraints

default implementation for UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets

collect_symbols(symbols=None, co_constraints=True)

returns the list of symbols occurring in self, ignoring type constraints and symbols created by aggregates

class AppliedSymbol(parent, symbol, sub_exprs, annotations=None, is_enumerated='', is_enumeration='', in_enumeration='')

Bases: idp_engine.Expression.Expression

Represents a symbol applied to arguments

Parameters

• symbol (SymbolExpr) – the symbol to be applied to arguments

• is_enumerated (string) – ‘’ or ‘is enumerated’

• is_enumeration (string) – ‘’ or ‘in’

• in_enumeration (Enumeration) – the enumeration following ‘in’

• as_disjunction (Optional[Expression]) – the translation of ‘is_enumerated’ and ‘in_enumeration’ as a disjunction

• decl (Declaration) – the declaration of the symbol, if known

• in_head (Bool) – True if the AppliedSymbol occurs in the head of a rule

• prefix (Optional[str]) – the prefix of the symbol

• annotations (Optional[Annotations]) –

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

• self (Expr.AppliedSymbol) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

fill_attributes_and_check(type_check=True)

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.AppliedSymbol) –

Return type

idp_engine.Expression.Expression

add_level_mapping(level_symbols, head, pos_justification, polarity, mode)

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.

• self (Expr.AppliedSymbol) –

• mode (Semantics) –

Return type

Expr.Expression

collect_nested_symbols(symbols, is_nested)

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 {Parse.SymbolDeclaration}

Parameters

• self (idp_engine.Expression.AppliedSymbol) –

• symbols (Set[idp_engine.Parse.SymbolDeclaration]) –

• is_nested (bool) –

as_set_condition()

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

Parameters

self (idp_engine.Expression.AppliedSymbol) –

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.AppliedSymbol) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

propagate1(assignments, tag, truth=None)

returns the list of symbolic_propagate of self, ignoring value and simpler

substitute(e0, e1, assignments, tag=None)

recursively substitute e0 by e1 in self

merge_WDFs()

Combine the WDF of the sub-expressions of self

__init__(parent, symbol, sub_exprs, annotations=None, is_enumerated='', is_enumeration='', in_enumeration='')

Parameters

annotations (Optional[idp_engine.Expression.Annotations]) –

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.

all_=False : ignore expanded formulas and AppliedSymbol interpreted in a structure

co_constraints=False : ignore co_constraints

default implementation for UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets

collect_symbols(symbols=None, co_constraints=True)

returns the list of symbols occurring in self, ignoring type constraints and symbols created by aggregates

is_value()

True for numerals, date, identifiers, and constructors applied to values.

Synomym: “is ground”, “is rigid”

Returns

True if self represents a value.

Return type

bool

is_reified()

False for values and for symbols applied to values.

Returns

True if self has to be reified to obtain its value in a Z3 model.

Return type

bool

generate_constructors(constructors)

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

Parameters

constructors (dict) –

class SymbolExpr(parent, name, eval, s)

Bases: idp_engine.Expression.Expression

represents either a type name, a symbol name or a $(..) expression evaluating to a type or symbol name

Parameters

• name (Optional[str]) –

• eval (Optional[str]) –

• s (Optional[Expression]) –

name

name of the type or symbol, or None

Type

Optional[str]

eval

$ or None

Type

Optional[str]

s

argument of the $.

Type

Optional[Expression]

decl

the declaration of the symbol

Type

Optional[Declaration]

Either name and decl`are not None, or `eval and s are not None. When eval is None, s is None too.

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

• self (Expr.SymbolExpr) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.SymbolExpr) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

__init__(parent, name, eval, s)

Parameters

• name (Optional[str]) –

• eval (Optional[str]) –

• s (Optional[idp_engine.Expression.Expression]) –

class UnappliedSymbol(parent, name)

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

Parameters

• parent (Optional[ASTNode]) –

• name (str) –

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

• self (Expr.UnappliedSymbol) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

__init__(parent, name)

Parameters

• parent (Optional[idp_engine.Expression.ASTNode]) –

• name (str) –

classmethod construct(constructor)

Create an UnappliedSymbol from a constructor

Parameters

constructor (idp_engine.Expression.Constructor) –

is_value()

True for numerals, date, identifiers, and constructors applied to values.

Synomym: “is ground”, “is rigid”

Returns

True if self represents a value.

Return type

bool

is_reified()

False for values and for symbols applied to values.

Returns

True if self has to be reified to obtain its value in a Z3 model.

Return type

bool

class Variable(parent, name, type=None)

Bases: idp_engine.Expression.Expression

AST node for a variable in a quantification or aggregate

Parameters

• name (str) – name of the variable

• type (Optional[Union[SetName]]) – sort of the variable, if known

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

• self (Expr.Variable) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

translate(problem, vars={})

Converts the syntax tree to a Z3 expression, with lookup in problem.z3

Parameters

• problem (Theory) – 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

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 co-constraints.

implementation for everything but AppliedSymbol, UnappliedSymbol and Fresh_variable

__init__(parent, name, type=None)

Parameters

• name (str) –

• type (Optional[idp_engine.Expression.SetName]) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.Expression) –

Return type

idp_engine.Expression.Expression

class Number(**kwargs)

Bases: idp_engine.Expression.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

• self (Expr.Number) –

Returns

an equivalent AST node, with updated type, .variables

Return type

Expression

translate(problem, vars={})

Converts the syntax tree to a Z3 expression, with lookup in problem.z3

Parameters

• problem (Theory) – 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

__init__(**kwargs)

real()

converts the INT number to REAL

is_value()

True for numerals, date, identifiers, and constructors applied to values.

Synomym: “is ground”, “is rigid”

Returns

True if self represents a value.

Return type

bool

is_reified()

False for values and for symbols applied to values.

Returns

True if self has to be reified to obtain its value in a Z3 model.

Return type

bool

class Date(**kwargs)

Bases: idp_engine.Expression.Expression

translate(problem, vars={})

Converts the syntax tree to a Z3 expression, with lookup in problem.z3

Parameters

• problem (Theory) – 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

__init__(**kwargs)

is_value()

True for numerals, date, identifiers, and constructors applied to values.

Synomym: “is ground”, “is rigid”

Returns

True if self represents a value.

Return type

bool

is_reified()

False for values and for symbols applied to values.

Returns

True if self has to be reified to obtain its value in a Z3 model.

Return type

bool

class Brackets(parent, f, annotations=None)

Bases: idp_engine.Expression.Expression

Parameters

annotations (Optional[Annotations]) –

fill_attributes_and_check()

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.Brackets) –

Return type

idp_engine.Expression.Expression

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

Parameters

• self (idp_engine.Expression.Brackets) –

• new_exprs (Generator[idp_engine.Expression.Expression, None, None]) –

Return type

idp_engine.Expression.Expression

symbolic_propagate(assignments, tag, truth=None)

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.

__init__(parent, f, annotations=None)

Parameters

annotations (Optional[idp_engine.Expression.Annotations]) –

class RecDef(parent, name, vars, expr)

Bases: idp_engine.Expression.Expression

represents a recursive definition

__init__(parent, name, vars, expr)