fixedpoint_get_num_levels method

int fixedpoint_get_num_levels(
  1. Z3_context c,
  2. Z3_fixedpoint d,
  3. Z3_func_decl pred
)

\brief Query the PDR engine for the maximal levels properties are known about predicate.

This call retrieves the maximal number of relevant unfoldings of \c pred with respect to the current exploration state. Note: this functionality is PDR specific.

def_API('Z3_fixedpoint_get_num_levels', UINT, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL)))

Implementation

int fixedpoint_get_num_levels(
  Z3_context c,
  Z3_fixedpoint d,
  Z3_func_decl pred,
) {
  return _fixedpoint_get_num_levels(
    c,
    d,
    pred,
  );
}