Function z3_sys::Z3_goal_assert [−][src]
pub unsafe extern "C" fn Z3_goal_assert(
c: Z3_context,
g: Z3_goal,
a: Z3_ast
)
Expand description
Add a new formula a
to the given goal.
The formula is split according to the following procedure that is applied
until a fixed-point:
Conjunctions are split into separate formulas.
Negations are distributed over disjunctions, resulting in separate formulas.
If the goal is false
, adding new formulas is a no-op.
If the formula a
is true
, then nothing is added.
If the formula a
is false
, then the entire goal is replaced by the formula false
.