Method parOrExample

examples/java/JavaGenericExample.java:900–921

(Context ctx)

    // / Demonstrates how to use the ParOr tactic.

    void parOrExample(Context ctx) throws TestFailedException
    {
        System.out.println("ParOrExample");
        Log.append("ParOrExample");

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

        Goal g = ctx.mkGoal(true, false, false);
        g.add(q);

        Tactic t1 = ctx.mkTactic("qfbv");
        Tactic t2 = ctx.mkTactic("qfbv");
        Tactic p = ctx.parOr(t1, t2);

        ApplyResult ar = p.apply(g);

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

    void bigIntCheck(Context ctx, RatNum r)
    {