Method assertAndTrack

src/api/java/Solver.java:153–165

Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean constants in ps. Remarks: This API is an alternative to #check() with assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination

(Expr<BoolSort>[] constraints, Expr<BoolSort>[] ps)

     * provided using {@link #check()} with assumptions.
     **/
    public void assertAndTrack(Expr<BoolSort>[] constraints, Expr<BoolSort>[] ps)
    {
        getContext().checkContextMatch(constraints);
        getContext().checkContextMatch(ps);
        if (constraints.length != ps.length) {
            throw new Z3Exception("Argument size mismatch");
        }

        for (int i = 0; i < constraints.length; i++) {
            Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
                constraints[i].getNativeObject(), ps[i].getNativeObject());
        }
    }

    /** 
     * Assert a constraint into the solver, and track it (in the unsat) core