Function z3_sys::Z3_fixedpoint_add_fact [−][src]
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
: - contextd
: - fixed point contextr
: - 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.