Method ArrayExample1

examples/dotnet/Program.cs:333–370

A simple array example.

(Context ctx)

        /// </summary>
        /// <param name="ctx"></param>
        static void ArrayExample1(Context ctx)
        {
            Console.WriteLine("ArrayExample1");

            Goal g = ctx.MkGoal(true);
            ArraySort asort = ctx.MkArraySort(ctx.IntSort, ctx.MkBitVecSort(32));
            ArrayExpr aex = (ArrayExpr)ctx.MkConst(ctx.MkSymbol("MyArray"), asort);
            Expr sel = ctx.MkSelect(aex, ctx.MkInt(0));
            g.Assert(ctx.MkEq(sel, ctx.MkBV(42, 32)));
            Symbol xs = ctx.MkSymbol("x");
            IntExpr xc = (IntExpr)ctx.MkConst(xs, ctx.IntSort);

            Symbol fname = ctx.MkSymbol("f");
            Sort[] domain = { ctx.IntSort };
            FuncDecl fd = ctx.MkFuncDecl(fname, domain, ctx.IntSort);
            Expr[] fargs = { ctx.MkConst(xs, ctx.IntSort) };
            IntExpr fapp = (IntExpr)ctx.MkApp(fd, fargs);

            g.Assert(ctx.MkEq(ctx.MkAdd(xc, fapp), ctx.MkInt(123)));

            Solver s = ctx.MkSolver();
            foreach (BoolExpr a in g.Formulas)
                s.Assert(a);
            Console.WriteLine("Solver: " + s);

            Status q = s.Check();
            Console.WriteLine("Status: " + q);

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

            Console.WriteLine("Model = " + s.Model);

	    Console.WriteLine("Interpretation of MyArray:\n" + s.Model.ConstInterp(aex.FuncDecl));
            Console.WriteLine("Interpretation of x:\n" + s.Model.ConstInterp(xc));
            Console.WriteLine("Interpretation of f:\n" + s.Model.FuncInterp(fd));
            Console.WriteLine("Interpretation of MyArray as Term:\n" + s.Model.ConstInterp(aex.FuncDecl));
        }

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