idp_engine.Expression

(They are monkey-patched by other modules)

class 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

dedup_nodes(kwargs, arg_name)[source]

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

Parameters
  • kwargs (Dict[str, ASTNode]) –

  • 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)[source]

Bases: idp_engine.Expression.ASTNode

Parameters

annotations (List[str]) –

__init__(parent, annotations)[source]
Parameters

annotations (List[str]) –

class Constructor(parent, name, args=None)[source]

Bases: idp_engine.Expression.ASTNode

Constructor declaration

Parameters
  • name (Union[UnappliedSymbol, str]) –

  • args (List[Accessor]) –

name

name of the constructor

Type

string

sorts

types of the arguments of the constructor

Type

List[Symbol]

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

SymbolDeclaration

has been applied to some arguments
Type

e.g., is_rgb

symbol

only for Symbol constructors

Type

Symbol

__init__(parent, name, args=None)[source]
Parameters
  • name (Union[idp_engine.Expression.UnappliedSymbol, str]) –

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

class Accessor(parent, type, accessor=None)[source]

Bases: idp_engine.Expression.ASTNode

represents an accessor and a type

Parameters
  • type (UnappliedSymbol) –

  • accessor (UnappliedSymbol) –

accessor

name of accessor function

Type

UnappliedSymbol, Optional

type

name of the output type of the accessor

Type

string

decl

declaration of the accessor function

Type

SymbolDeclaration

__init__(parent, type, accessor=None)[source]
Parameters
  • type (idp_engine.Expression.UnappliedSymbol) –

  • accessor (Optional[idp_engine.Expression.UnappliedSymbol]) –

class Expression(parent=None)[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 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

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

Type

Set(string)

is_type_constraint_for

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

Type

string

__init__(parent=None)[source]
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 UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets

Parameters
  • questions (idp_engine.utils.OrderedSet) –

  • all_ (bool) –

  • co_constraints (bool) –

Return type

idp_engine.utils.OrderedSet

collect_symbols(symbols=None, co_constraints=True)[source]

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

Parameters
  • symbols (Dict[str, SymbolDeclaration]) –

  • co_constraints (bool) –

Return type

Dict[str, 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}

Parameters
  • symbols (Set[SymbolDeclaration]) –

  • is_nested (bool) –

Return type

Set[SymbolDeclaration]

generate_constructors(constructors)[source]

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

Parameters

constructors (Dict[str, List[idp_engine.Expression.Constructor]]) –

co_constraints(co_constraints)[source]

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

Parameters

co_constraints (idp_engine.utils.OrderedSet) –

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

simplify_with(assignments)

simplify the expression using the assignments

Parameters
  • self (idp_engine.Expression.Expression) –

  • assignments (Assignments) –

Return type

idp_engine.Expression.Expression

symbolic_propagate(assignments, tag, truth=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.

  • tag (Status) –

propagate1(assignments, tag, truth)

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

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

Return type

idp_engine.Expression.Expression

add_level_mapping(level_symbols, head, pos_justification, polarity, mode)[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.

  • mode (Semantics) –

Return type

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

Expression

annotate1()

annotations that are common to __init__ and make()

class Symbol(parent, name)[source]

Bases: idp_engine.Expression.Expression

Represents a Symbol. Handles synonyms.

Parameters

name (str) –

name

name of the symbol

Type

string

__init__(parent, name)[source]
Parameters

name (str) –

has_element(term, interpretations, extensions)[source]

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

Parameters
  • term (Expression) – the argument to be checked

  • interpretations (Dict[str, SymbolInterpretation]) –

  • extensions (Dict[str, Extension]) –

Returns

whether term is in the type denoted by self.

Return type

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

Expression

class Type(parent, name, ins=None, out=None)[source]

Bases: idp_engine.Expression.Symbol

ASTNode representing aType or Concept[aSignature], e.g., Concept[T*T->Bool]

Inherits from Symbol

Parameters
  • name (Symbol) – name of the concept

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

  • out (Symbol, Optional) – range of the Concept signature, e.g., Bool

__init__(parent, name, ins=None, out=None)[source]
Parameters
  • name (str) –

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

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

has_element(term, interpretations, extensions)[source]

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

Parameters
  • term (Expression) – the argument to be checked

  • interpretations (Dict[str, SymbolInterpretation]) –

  • extensions (Dict[str, Extension]) –

Returns

whether term term is in the type denoted by self.

Return type

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

Expression

class AIfExpr(parent, if_f, then_f, else_f)[source]

Bases: idp_engine.Expression.Expression

Parameters
  • if_f (Expression) –

  • then_f (Expression) –

  • else_f (Expression) –

Return type

AIfExpr

__init__(parent, if_f, then_f, else_f)[source]
Parameters
  • if_f (idp_engine.Expression.Expression) –

  • then_f (idp_engine.Expression.Expression) –

  • else_f (idp_engine.Expression.Expression) –

Return type

idp_engine.Expression.AIfExpr

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}

annotate1()

annotations that are common to __init__ and make()

translate1(problem, vars={})

Converts the syntax tree to a Z3 expression, ignoring .value

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.

class Quantee(parent, vars, subtype=None, sort=None)[source]

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 (List[List[Variable]]) –

  • subtype (Type) –

  • sort (SymbolExpr) –

vars

the (tuples of) variables being quantified

Type

List[List[Variable]]

subtype

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

Type

Type, 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`
__init__(parent, vars, subtype=None, sort=None)[source]
Parameters
  • vars (List[List[idp_engine.Expression.Variable]]) –

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

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

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class AQuantification(parent, annotations, q, quantees, f)[source]

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

__init__(parent, annotations, q, quantees, f)[source]
classmethod make(q, quantees, f, annotations=None)[source]

make and annotate a quantified formula

Parameters
  • q (str) –

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

  • f (idp_engine.Expression.Expression) –

Return type

AQuantification

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

collect_symbols(symbols=None, co_constraints=True)[source]

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

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

Expression

annotate1()

annotations that are common to __init__ and make()

symbolic_propagate(assignments, tag, truth=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.

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class Operator(parent, operator, sub_exprs, annotations=None)[source]

Bases: idp_engine.Expression.Expression

__init__(parent, operator, sub_exprs, annotations=None)[source]
classmethod make(ops, operands, annotations=None, parent=None)[source]

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

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

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

Return type

Operator

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

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}

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

Expression

annotate1()

annotations that are common to __init__ and make()

class AImplication(parent, operator, sub_exprs, annotations=None)[source]

Bases: idp_engine.Expression.Operator

add_level_mapping(level_symbols, head, pos_justification, polarity, mode)[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.

annotate1()

annotations that are common to __init__ and make()

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class AEquivalence(parent, operator, sub_exprs, annotations=None)[source]

Bases: idp_engine.Expression.Operator

split_equivalences()[source]

Returns an equivalent expression where equivalences are replaced by implications

Returns

Expression

annotate1()

annotations that are common to __init__ and make()

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class ARImplication(parent, operator, sub_exprs, annotations=None)[source]

Bases: idp_engine.Expression.Operator

add_level_mapping(level_symbols, head, pos_justification, polarity, mode)[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.

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

Expression

class ADisjunction(parent, operator, sub_exprs, annotations=None)[source]

Bases: idp_engine.Expression.Operator

propagate1(assignments, tag, truth=true)

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

update_exprs(new_exprs, replace=True)

change sub_exprs and simplify, while keeping relevant info.

class AConjunction(parent, operator, sub_exprs, annotations=None)[source]

Bases: idp_engine.Expression.Operator

propagate1(assignments, tag, truth=true)

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

update_exprs(new_exprs, replace=True)

change sub_exprs and simplify, while keeping relevant info.

class AComparison(parent, operator, sub_exprs, annotations=None)[source]

Bases: idp_engine.Expression.Operator

is_assignment()[source]
Returns

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

Return type

bool

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

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

propagate1(assignments, tag, truth=true)

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

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class ASumMinus(parent, operator, sub_exprs, annotations=None)[source]

Bases: idp_engine.Expression.Operator

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class AMultDiv(parent, operator, sub_exprs, annotations=None)[source]

Bases: idp_engine.Expression.Operator

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class APower(parent, operator, sub_exprs, annotations=None)[source]

Bases: idp_engine.Expression.Operator

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class AUnary(parent, operators, f)[source]

Bases: idp_engine.Expression.Expression

Parameters
  • operators (List[str]) –

  • f (Expression) –

__init__(parent, operators, f)[source]
Parameters
  • operators (List[str]) –

  • f (idp_engine.Expression.Expression) –

add_level_mapping(level_symbols, head, pos_justification, polarity, mode)[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.

annotate1()

annotations that are common to __init__ and make()

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

propagate1(assignments, tag, truth=true)

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

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class AAggregate(parent, aggtype, quantees, lambda_=None, f=None, if_=None)[source]

Bases: idp_engine.Expression.Expression

Parameters
  • aggtype (str) –

  • quantees (List[Quantee]) –

  • lambda_ (str) –

  • f (Expression) –

  • if_ (Expression) –

__init__(parent, aggtype, quantees, lambda_=None, f=None, if_=None)[source]
Parameters
  • aggtype (str) –

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

  • lambda_ (Optional[str]) –

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

  • if_ (Optional[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 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 UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets

collect_symbols(symbols=None, co_constraints=True)[source]

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

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}

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

Expression

annotate1()

annotations that are common to __init__ and make()

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

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

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

__init__(parent, symbol, sub_exprs, annotations=None, is_enumerated='', is_enumeration='', in_enumeration='')[source]
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 UnappliedSymbol, AIfExpr, AUnary, Variable, Number_constant, Brackets

collect_symbols(symbols=None, co_constraints=True)[source]

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

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)[source]

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

Parameters

constructors (dict) –

add_level_mapping(level_symbols, head, pos_justification, polarity, mode)[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.

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

Expression

annotate1()

annotations that are common to __init__ and make()

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

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class SymbolExpr(parent, s, eval='')[source]

Bases: idp_engine.Expression.Expression

__init__(parent, s, eval='')[source]
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

Expression

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class UnappliedSymbol(parent, s)[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().

__init__(parent, s)[source]
classmethod construct(constructor)[source]

Create an UnappliedSymbol from a constructor

Parameters

constructor (idp_engine.Expression.Constructor) –

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

Expression

class Variable(parent, name, sort=None)[source]

Bases: idp_engine.Expression.Expression

AST node for a variable in a quantification or aggregate

Parameters
  • name (str) – name of the variable

  • sort (Optional[Union[Type, Symbol]]) – sort of the variable, if known

__init__(parent, name, sort=None)[source]
Parameters
  • name (str) –

  • sort (Optional[Union[idp_engine.Expression.Type, idp_engine.Expression.Symbol]]) –

annotate1()[source]

annotations that are common to __init__ and make()

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

Expression

class Number(**kwargs)[source]

Bases: idp_engine.Expression.Expression

__init__(**kwargs)[source]
real()[source]

converts the INT number to REAL

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

Expression

class Date(**kwargs)[source]

Bases: idp_engine.Expression.Expression

__init__(**kwargs)[source]
class Brackets(**kwargs)[source]

Bases: idp_engine.Expression.Expression

__init__(**kwargs)[source]
annotate1()

annotations that are common to __init__ and make()

symbolic_propagate(assignments, tag, truth=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.

update_exprs(new_exprs)

change sub_exprs and simplify, while keeping relevant info.

class RecDef(parent, name, vars, expr)[source]

Bases: idp_engine.Expression.Expression

represents a recursive definition

__init__(parent, name, vars, expr)[source]