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