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 calling Z3_fixedpoint_get_answer.
  • Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.