Function z3_sys::Z3_fixedpoint_get_answer

source ·

pub unsafe extern "C" fn Z3_fixedpoint_get_answer(
    c: Z3_context,
    d: Z3_fixedpoint
) -> Z3_ast

Expand description

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 Z3_L_TRUE. When used with the PDR engine, the previous call must have been either Z3_L_TRUE or Z3_L_FALSE.