fixedpoint_query_relations method

int fixedpoint_query_relations(
  1. Z3_context c,
  2. Z3_fixedpoint d,
  3. int num_relations,
  4. Pointer<Z3_func_decl> relations,
)

\brief Pose multiple queries against the asserted rules.

The queries are encoded as relations (function declarations).

query returns

  • \c Z3_L_FALSE if the query is unsatisfiable.
  • \c Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
  • \c Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.

def_API('Z3_fixedpoint_query_relations', LBOOL, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2, FUNC_DECL)))

Implementation

int fixedpoint_query_relations(
  Z3_context c,
  Z3_fixedpoint d,
  int num_relations,
  ffi.Pointer<Z3_func_decl> relations,
) {
  return _fixedpoint_query_relations(
    c,
    d,
    num_relations,
    relations,
  );
}