fixedpoint_query_from_lvl method

int fixedpoint_query_from_lvl(
  1. Z3_context c,
  2. Z3_fixedpoint d,
  3. Z3_ast query,
  4. int lvl,
)

@name Spacer facilities / /**@{/ /** \brief Pose a query against the asserted rules at the given level.

\code query ::= (exists (bound-vars) query) | literals \endcode

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_from_lvl', LBOOL, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST), _in(UINT)))

Implementation

int fixedpoint_query_from_lvl(
  Z3_context c,
  Z3_fixedpoint d,
  Z3_ast query,
  int lvl,
) {
  return _fixedpoint_query_from_lvl(
    c,
    d,
    query,
    lvl,
  );
}