fixedpoint_get_cover_delta method

Z3_ast fixedpoint_get_cover_delta(
  1. Z3_context c,
  2. Z3_fixedpoint d,
  3. int level,
  4. Z3_func_decl pred,
)

Retrieve the current cover of \c pred up to \c level unfoldings. Return just the delta that is known at \c level. To obtain the full set of properties of \c pred one should query at \c level+1 , \c level+2 etc, and include \c level=-1.

Note: this functionality is PDR specific.

def_API('Z3_fixedpoint_get_cover_delta', AST, (_in(CONTEXT), _in(FIXEDPOINT), _in(INT), _in(FUNC_DECL)))

Implementation

Z3_ast fixedpoint_get_cover_delta(
  Z3_context c,
  Z3_fixedpoint d,
  int level,
  Z3_func_decl pred,
) {
  return _fixedpoint_get_cover_delta(
    c,
    d,
    level,
    pred,
  );
}