[−][src]Function z3_sys::Z3_fixedpoint_add_rule
pub unsafe extern "C" fn Z3_fixedpoint_add_rule(
c: Z3_context,
d: Z3_fixedpoint,
rule: Z3_ast,
name: Z3_symbol
)
Add a universal Horn clause as a named rule.
The horn_rule
should be of the form:
horn_rule ::= (forall (bound-vars) horn_rule)
| (=> atoms horn_rule)
| atom