idp_engine.idp_to_Z3

Translates AST tree to Z3

TODO: vocabulary

translate_expression(self, problem, vars={})[source]

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

translate1_aifexpr(self, problem, vars={})[source]

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

translate_acomparison_optimum(self, problem, lhs, op, rhs, vars={})[source]

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

at_most_at_least_possible(lhs, operator, rhs)[source]

Verifies whether an optimized Z3 encoding using “AtMost” or “AtLeast” is possible for two children of an AComparison. This is the case when one child is a cardinality, while the other child is a literal int. See: https://gitlab.com/krr/IDP-Z3/-/issues/362

Parameters
  • lhs (idp_engine.Expression.Expression) –

  • operator (str) –

  • rhs (idp_engine.Expression.Expression) –