Function z3_sys::Z3_solver_cube

pub unsafe extern "C" fn Z3_solver_cube(
    c: Z3_context, 
    s: Z3_solver, 
    vars: Z3_ast_vector, 
    backtrack_level: c_uint
) -> Z3_ast_vector

Extract a next cube for a solver. The last cube is the constant true or 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.