idp_engine.Annotate

Methods to annotate the Abstract Syntax Tree (AST) of an IDP-Z3 program.

root_set(s)[source]

Recursively finds the root sets of a set in the hierarchy.

For a set of tuples of domain elements, it returns the list of root sets of the elements of the tuple. For example, the root sets of p: T1 * T2 -> Bool are [T1, T2]

It goes up the hierarchy until a declared type or a Concept[..] is found.

Parameters

s (idp_engine.Expression.SetName) –

Return type

List[idp_engine.Expression.SetName]

collect_warnings(expr, out)[source]

recursively finds the deepest Expression that is not well-defined in expr, and create a warning

Parameters

expr (idp_engine.Expression.Expression) –

rename_args(self, subs)[source]

replace old variables by new variables (ignoring arguments in the head before the it

Parameters

  • self (Parse.Rule) –

  • subs (dict[str, Expr.Expression]) –

Return type

None

annotate_block_struc(self, idp)[source]

Annotates the structure with the enumerations found in it. Every enumeration is converted into an assignment, which is added to self.assignments.

Parameters

  • idp (idp_engine.Parse.IDP) – a Parse.IDP object.

  • self (idp_engine.Expression.ASTNode) –

  • idp –

Returns None

Return type

Union[Exception, List[Exceptions]]

annotate_symbolinterpretation(self, voc, q_vars)[source]

Annotate the symbol.

Parameters

  • block – a Structure object

  • self (Expr.Expression) –

  • voc (Parse.Vocabulary) –

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

Returns None

Return type

Expr.Expression

annotate_expression(self, voc, q_vars)[source]

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

annotations that are common to __init__ and make()

Parameters

self (idp_engine.Expression.Expression) –

Return type

idp_engine.Expression.Expression

base_type(exprs, bases=None)[source]

Checks or determines the (sub)types of the expressions in exprs.

Raises an error if the (sub)type of an expression is not in bases. Raises an error if the expressions have incompatible (sub)types. Returns None if exprs is empty.

A mix of Int and Real (or Int and Date) is allowed.

Parameters

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

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

Return type

Optional[idp_engine.Expression.SetName]

agg_create_min_max_appliedsymbol(agg, name, voc, q_vars)[source]

Create an applied symbol representing a min/max aggregate. The actual logic for the min/max aggregate is contained in the co-constraints.

Parameters

  • agg (Expr.AAggregate) –

  • name (str) –

  • voc (Parse.Vocabulary) –

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

Return type

Expr.AppliedSymbol

annotate_aaggregate(self, voc, q_vars)[source]

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