solver_cube method

Z3_ast_vector solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, int backtrack_level,)

\brief extract a next cube for a solver. The last cube is the constant \c true or \c false. The number of (non-constant) cubes is by default 1. For the sat solver cubing is controlled using parameters sat.lookahead.cube.cutoff and sat.lookahead.cube.fraction.

The third argument is a vector of variables that may be used for cubing. The contents of the vector is only used in the first call. The initial list of variables is used in subsequent calls until it returns the unsatisfiable cube. The vector is modified to contain a set of Autarky variables that occur in clauses that are affected by the (last literal in the) cube. These variables could be used by a different cuber (on a different solver object) for further recursive cubing.

The last argument is a backtracking level. It instructs the cube process to backtrack below the indicated level for the next cube.

def_API('Z3_solver_cube', AST_VECTOR, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(UINT)))

Implementation

Z3_ast_vector solver_cube(
  Z3_context c,
  Z3_solver s,
  Z3_ast_vector vars,
  int backtrack_level,
) {
  return _solver_cube(
    c,
    s,
    vars,
    backtrack_level,
  );
}