Method logicExample

examples/java/JavaGenericExample.java:868–896

(Context ctx)

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

        Global.ToggleWarningMessages(true);

        BitVecSort bvs = ctx.mkBitVecSort(32);
        Expr<BitVecSort> x = ctx.mkConst("x", bvs);
        Expr<BitVecSort> 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.printf("solver result: %s%n", 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.printf("tactic result: %s%n", ar);

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

    // / Demonstrates how to use the ParOr tactic.