solver_next_split method

bool solver_next_split(
  1. Z3_context c,
  2. Z3_solver_callback cb,
  3. Z3_ast t,
  4. int idx,
  5. int phase,
)

Sets the next (registered) expression to split on. The function returns false and ignores the given expression in case the expression is already assigned internally (due to relevancy propagation, this assignments might not have been reported yet by the fixed callback). In case the function is called in the decide callback, it overrides the currently selected variable and phase.

def_API('Z3_solver_next_split', BOOL, (_in(CONTEXT), _in(SOLVER_CALLBACK), _in(AST), _in(UINT), _in(LBOOL)))

Implementation

bool solver_next_split(
  Z3_context c,
  Z3_solver_callback cb,
  Z3_ast t,
  int idx,
  int phase,
) {
  return _solver_next_split(
    c,
    cb,
    t,
    idx,
    phase,
  );
}