Method modelConverterTest

examples/java/JavaExample.java:315–349

(Context ctx)

    }

    void modelConverterTest(Context ctx) throws TestFailedException
    {
        System.out.println("ModelConverterTest");

        ArithExpr xr = (ArithExpr) ctx.mkConst(ctx.mkSymbol("x"),
                ctx.mkRealSort());
        ArithExpr yr = (ArithExpr) ctx.mkConst(ctx.mkSymbol("y"),
                ctx.mkRealSort());
        Goal g4 = ctx.mkGoal(true, false, false);
        g4.add(ctx.mkGt(xr, ctx.mkReal(10, 1)));
        g4.add(ctx.mkEq(yr, ctx.mkAdd(xr, ctx.mkReal(1, 1))));
        g4.add(ctx.mkGt(yr, ctx.mkReal(1, 1)));

        ApplyResult ar = applyTactic(ctx, ctx.mkTactic("simplify"), g4);
        if (ar.getNumSubgoals() == 1
                && (ar.getSubgoals()[0].isDecidedSat() || ar.getSubgoals()[0]
                        .isDecidedUnsat()))
            throw new TestFailedException();

        ar = applyTactic(ctx, ctx.andThen(ctx.mkTactic("simplify"),
                ctx.mkTactic("solve-eqs")), g4);
        if (ar.getNumSubgoals() == 1
                && (ar.getSubgoals()[0].isDecidedSat() || ar.getSubgoals()[0]
                        .isDecidedUnsat()))
            throw new TestFailedException();

        Solver s = ctx.mkSolver();
        for (BoolExpr e : ar.getSubgoals()[0].getFormulas())
            s.add(e);
        Status q = s.check();
        System.out.println("Solver says: " + q);
        System.out.println("Model: \n" + s.getModel());
        if (q != Status.SATISFIABLE)
            throw new TestFailedException();
    }

    // / A simple array example.