Method arrayExample2

examples/java/JavaGenericExample.java:385–424

(Context ctx)

    // / <remarks>This example demonstrates how to use the array
    // theory.</remarks>
    public void arrayExample2(Context ctx) throws TestFailedException
    {
        System.out.println("ArrayExample2");
        Log.append("ArrayExample2");

        IntSort int_type = ctx.getIntSort();
        ArraySort<IntSort, IntSort> array_type = ctx.mkArraySort(int_type, int_type);

        Expr<ArraySort<IntSort, IntSort>> a1 = ctx.mkConst("a1", array_type);
        ArrayExpr<IntSort, IntSort> a2 = ctx.mkArrayConst("a2", int_type, int_type);
        Expr<IntSort> i1 = ctx.mkConst("i1", int_type);
        Expr<IntSort> i2 = ctx.mkConst("i2", int_type);
        Expr<IntSort> i3 = ctx.mkConst("i3", int_type);
        Expr<IntSort> v1 = ctx.mkConst("v1", int_type);
        Expr<IntSort> v2 = ctx.mkConst("v2", int_type);

        ArrayExpr<IntSort, IntSort> st1 = ctx.mkStore(a1, i1, v1);
        ArrayExpr<IntSort, IntSort> st2 = ctx.mkStore(a2, i2, v2);

        Expr<IntSort> sel1 = ctx.mkSelect(a1, i3);
        Expr<IntSort> sel2 = ctx.mkSelect(a2, i3);

        /* create antecedent */
        BoolExpr antecedent = ctx.mkEq(st1, st2);

        /*
         * create consequent: i1 = i3 or i2 = i3 or select(a1, i3) = select(a2,
         * i3)
         */
        BoolExpr consequent = ctx.mkOr(ctx.mkEq(i1, i3), ctx.mkEq(i2, i3), ctx.mkEq(sel1, sel2));

        /*
         * prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 =
         * i3 or select(a1, i3) = select(a2, i3))
         */
        BoolExpr thm = ctx.mkImplies(antecedent, consequent);
        System.out.println("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))");
        System.out.println(thm);
        prove(ctx, thm, false);
    }

    // / Show that <code>distinct(a_0, ... , a_n)</code> is
    // / unsatisfiable when <code>a_i</code>'s are arrays from boolean to