Function z3_sys::Z3_goal_assert

source · 
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.