Method cube

src/api/java/Solver.java:422–465

Return a sequence of cubes (conjunctions of literals) for partitioning the search space. Each cube represents a partial assignment that can be used as a starting point for parallel solving. This is primarily useful for cube-and-conquer parallel SAT solving strategies, where different cubes can be so

(Expr<?>[] vars, int cutoff)

     * @throws Z3Exception
     **/
    public java.util.Iterator<BoolExpr[]> cube(Expr<?>[] vars, int cutoff)
    {
        ASTVector cubeVars = new ASTVector(getContext());
        if (vars != null) {
            for (Expr<?> v : vars) {
                cubeVars.push(v);
            }
        }
        
        return new java.util.Iterator<BoolExpr[]>() {
            private BoolExpr[] nextCube = computeNext();
            
            private BoolExpr[] computeNext() {
                ASTVector result = new ASTVector(getContext(), 
                    Native.solverCube(getContext().nCtx(), getNativeObject(), 
                                     cubeVars.getNativeObject(), cutoff));
                BoolExpr[] cube = result.ToBoolExprArray();
                
                // Check for termination conditions
                if (cube.length == 1 && cube[0].isFalse()) {
                    return null; // No more cubes
                }
                if (cube.length == 0) {
                    return null; // Search space exhausted
                }
                return cube;
            }
            
            @Override
            public boolean hasNext() {
                return nextCube != null;
            }
            
            @Override
            public BoolExpr[] next() {
                if (nextCube == null) {
                    throw new java.util.NoSuchElementException();
                }
                BoolExpr[] current = nextCube;
                nextCube = computeNext();
                return current;
            }
        };
    }

    /**
     * Set an initial value for a variable to guide the solver's search heuristics.