Method logicExample

examples/java/JavaExample.java:1076–1104

(Context ctx)

    // / @param ctx 
    void logicExample(Context ctx) throws TestFailedException
    {
        System.out.println("LogicTest");
        Log.append("LogicTest");

        com.microsoft.z3.Global.ToggleWarningMessages(true);

        BitVecSort bvs = ctx.mkBitVecSort(32);
        Expr x = ctx.mkConst("x", bvs);
        Expr y = ctx.mkConst("y", bvs);
        BoolExpr eq = ctx.mkEq(x, y);

        // Use a solver for QF_BV
        Solver s = ctx.mkSolver("QF_BV");
        s.add(eq);
        Status res = s.check();
        System.out.println("solver result: " + res);

        // Or perhaps a tactic for QF_BV
        Goal g = ctx.mkGoal(true, false, false);
        g.add(eq);

        Tactic t = ctx.mkTactic("qfbv");
        ApplyResult ar = t.apply(g);
        System.out.println("tactic result: " + ar);

        if (ar.getNumSubgoals() != 1 || !ar.getSubgoals()[0].isDecidedSat())
            throw new TestFailedException();
    }

    // / Demonstrates how to use the ParOr tactic.