fixedpoint_get_answer method

Z3_ast fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)

\brief Retrieve a formula that encodes satisfying answers to the query.

When used in Datalog mode, the returned answer is a disjunction of conjuncts. Each conjunct encodes values of the bound variables of the query that are satisfied. In PDR mode, the returned answer is a single conjunction.

When used in Datalog mode the previous call to #Z3_fixedpoint_query must have returned \c Z3_L_TRUE. When used with the PDR engine, the previous call must have been either \c Z3_L_TRUE or \c Z3_L_FALSE.

def_API('Z3_fixedpoint_get_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))

Implementation

Z3_ast fixedpoint_get_answer(
  Z3_context c,
  Z3_fixedpoint d,
) {
  return _fixedpoint_get_answer(
    c,
    d,
  );
}