Method arrayExample1

examples/java/JavaGenericExample.java:338–378

(Context ctx)

    // / A simple array example.

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

        Goal g = ctx.mkGoal(true, false, false);
        ArraySort<IntSort, BitVecSort> asort = ctx.mkArraySort(ctx.getIntSort(),
                ctx.mkBitVecSort(32));
        Expr<ArraySort<IntSort, BitVecSort>> aex = ctx.mkConst(ctx.mkSymbol("MyArray"), asort);
        Expr<BitVecSort> 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<IntSort> fd = ctx.mkFuncDecl(fname, domain, ctx.getIntSort());
        Expr<?>[] fargs = { ctx.mkConst(xs, ctx.getIntSort()) };
        Expr<IntSort> fapp = 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.printf("Solver: %s%n", s);

        Status q = s.check();
        System.out.printf("Status: %s%n", q);

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

        System.out.printf("Model = %s%n", s.getModel());

        System.out.printf("Interpretation of MyArray:%n%s%n", s.getModel().getFuncInterp(aex.getFuncDecl()));
        System.out.printf("Interpretation of x:%n%s%n", s.getModel().getConstInterp(xc));
        System.out.printf("Interpretation of f:%n%s%n", s.getModel().getFuncInterp(fd));
        System.out.printf("Interpretation of MyArray as Term:%n%s%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>.