Function z3_sys::Z3_fixedpoint_add_fact

source · 
pub unsafe extern "C" fn Z3_fixedpoint_add_fact(
    c: Z3_context,
    d: Z3_fixedpoint,
    r: Z3_func_decl,
    num_args: c_uint,
    args: *mut c_uint
)
Expand description

Add a Database fact.

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

The number of arguments num_args should be equal to the number of sorts in the domain of 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 r is applied to the arguments.