Function z3_sys::Z3_fixedpoint_query_relations [−][src]
pub unsafe extern "C" fn Z3_fixedpoint_query_relations(
c: Z3_context,
d: Z3_fixedpoint,
num_relations: c_uint,
relations: *const Z3_func_decl
) -> Z3_lbool
Expand description
Pose multiple queries against the asserted rules.
The queries are encoded as relations (function declarations).
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.