Method applyTactic

examples/java/JavaGenericExample.java:206–234

(Context ctx, Tactic t, Goal g)

    }

    ApplyResult applyTactic(Context ctx, Tactic t, Goal g)
    {
        System.out.printf("%nGoal: %s%n", g);

        ApplyResult res = t.apply(g);
        System.out.printf("Application result: %s%n", res);

        Status q = Status.UNKNOWN;
        for (Goal sg : res.getSubgoals())
            if (sg.isDecidedSat())
                q = Status.SATISFIABLE;
            else if (sg.isDecidedUnsat())
                q = Status.UNSATISFIABLE;

        switch (q)
        {
        case UNKNOWN:
            System.out.println("Tactic result: Undecided");
            break;
        case SATISFIABLE:
            System.out.println("Tactic result: SAT");
            break;
        case UNSATISFIABLE:
            System.out.println("Tactic result: UNSAT");
            break;
        }

        return res;
    }

    void prove(Context ctx, Expr<BoolSort> f, boolean useMBQI) throws TestFailedException
    {