Function z3_sys::Z3_fixedpoint_query_from_lvl [−][src]
pub unsafe extern "C" fn Z3_fixedpoint_query_from_lvl(
c: Z3_context,
d: Z3_fixedpoint,
query: Z3_ast,
lvl: c_uint
) -> Z3_lbool
Expand description
Pose a query against the asserted rules at the given level.
query ::= (exists (bound-vars) query) | literals
query returns
Z3_L_FALSE
if the query is unsatisfiable.Z3_L_TRUE
if the query is satisfiable. Obtain the answer by callingZ3_fixedpoint_get_answer
.Z3_L_UNDEF
if the query was interrupted, timed out or otherwise failed.