Method arrayExample1

examples/java/JavaExample.java:353–396

(Context ctx)

    // / A simple array example.

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

        Goal g = ctx.mkGoal(true, false, false);
        ArraySort asort = ctx.mkArraySort(ctx.getIntSort(),
                ctx.mkBitVecSort(32));
        ArrayExpr aex = (ArrayExpr) ctx.mkConst(ctx.mkSymbol("MyArray"), asort);
        Expr sel = ctx.mkSelect(aex, ctx.mkInt(0));
        g.add(ctx.mkEq(sel, ctx.mkBV(42, 32)));
        Symbol xs = ctx.mkSymbol("x");
        IntExpr xc = (IntExpr) ctx.mkConst(xs, ctx.getIntSort());

        Symbol fname = ctx.mkSymbol("f");
        Sort[] domain = { ctx.getIntSort() };
        FuncDecl fd = ctx.mkFuncDecl(fname, domain, ctx.getIntSort());
        Expr[] fargs = { ctx.mkConst(xs, ctx.getIntSort()) };
        IntExpr fapp = (IntExpr) ctx.mkApp(fd, fargs);

        g.add(ctx.mkEq(ctx.mkAdd(xc, fapp), ctx.mkInt(123)));

        Solver s = ctx.mkSolver();
        for (BoolExpr a : g.getFormulas())
            s.add(a);
        System.out.println("Solver: " + s);

        Status q = s.check();
        System.out.println("Status: " + q);

        if (q != Status.SATISFIABLE)
            throw new TestFailedException();

        System.out.println("Model = " + s.getModel());

        System.out.println("Interpretation of MyArray:\n"
                + s.getModel().getFuncInterp(aex.getFuncDecl()));
        System.out.println("Interpretation of x:\n"
                + s.getModel().getConstInterp(xc));
        System.out.println("Interpretation of f:\n"
                + s.getModel().getFuncInterp(fd));
        System.out.println("Interpretation of MyArray as Term:\n"
                + s.getModel().getFuncInterp(aex.getFuncDecl()));
    }

    // / Prove <tt>store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2
    // = i3 or select(a1, i3) = select(a2, i3))</tt>.