fixedpoint_add_fact method

void fixedpoint_add_fact(
  1. Z3_context c,
  2. Z3_fixedpoint d,
  3. Z3_func_decl r,
  4. int num_args,
  5. Pointer<UnsignedInt> args,
)

\brief Add a Database fact.

\param c - context \param d - fixed point context \param r - relation signature for the row. \param num_args - number of columns for the given row. \param args - array of the row elements.

The number of arguments \c num_args should be equal to the number of sorts in the domain of \c r. Each sort in the domain should be an integral (bit-vector, Boolean or or finite domain sort).

The call has the same effect as adding a rule where \c r is applied to the arguments.

def_API('Z3_fixedpoint_add_fact', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL), _in(UINT), _in_array(3, UINT)))

Implementation

void fixedpoint_add_fact(
  Z3_context c,
  Z3_fixedpoint d,
  Z3_func_decl r,
  int num_args,
  ffi.Pointer<ffi.UnsignedInt> args,
) {
  return _fixedpoint_add_fact(
    c,
    d,
    r,
    num_args,
    args,
  );
}