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