Method Check

src/api/java/Optimize.java:200–225

Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded and don't use strict inequalities) is optimal.

(Expr<BoolSort>... assumptions)

     * don't use strict inequalities) is optimal.
     **/
    public Status Check(Expr<BoolSort>... assumptions)
    {
        Z3_lbool r;
        if (assumptions == null) {
          r = Z3_lbool.fromInt(
              Native.optimizeCheck(
                  getContext().nCtx(), 
                  getNativeObject(), 0, null));
        }
        else {
          r = Z3_lbool.fromInt(
              Native.optimizeCheck(
                  getContext().nCtx(), 
                  getNativeObject(), 
                  assumptions.length, 
                  AST.arrayToNative(assumptions)));
        }
        switch (r) {
            case Z3_L_TRUE:
                return Status.SATISFIABLE;
            case Z3_L_FALSE:
                return Status.UNSATISFIABLE;
            default:
                return Status.UNKNOWN;
        }
    }

    /**
     * Creates a backtracking point.