Method EvalExample2

examples/dotnet/Program.cs:1781–1818

Demonstrate how to use #Eval on tuples.

(Context ctx)

        /// Demonstrate how to use #Eval on tuples.
        /// </summary>
        public static void EvalExample2(Context ctx)
        {
            Console.WriteLine("EvalExample2");

            Sort int_type = ctx.IntSort;
            TupleSort tuple = ctx.MkTupleSort(
             ctx.MkSymbol("mk_tuple"),                        // name of tuple constructor
             new Symbol[] { ctx.MkSymbol("first"), ctx.MkSymbol("second") },    // names of projection operators
             new Sort[] { int_type, int_type } // types of projection operators
             );
            FuncDecl first = tuple.FieldDecls[0];     // declarations are for projections
            FuncDecl second = tuple.FieldDecls[1];
            Expr tup1 = ctx.MkConst("t1", tuple);
            Expr tup2 = ctx.MkConst("t2", tuple);

            Solver solver = ctx.MkSolver();

            /* assert tup1 != tup2 */
            solver.Assert(ctx.MkNot(ctx.MkEq(tup1, tup2)));
            /* assert first tup1 = first tup2 */
            solver.Assert(ctx.MkEq(ctx.MkApp(first, tup1), ctx.MkApp(first, tup2)));

            /* find model for the constraints above */
            Model model = null;
            if (Status.SATISFIABLE == solver.Check())
            {
                model = solver.Model;
                Console.WriteLine("{0}", model);
                Console.WriteLine("evaluating tup1 {0}", (model.Evaluate(tup1)));
                Console.WriteLine("evaluating tup2 {0}", (model.Evaluate(tup2)));
                Console.WriteLine("evaluating second(tup2) {0}",
                          (model.Evaluate(ctx.MkApp(second, tup2))));
            }
            else
            {
                Console.WriteLine("BUG, the constraints are satisfiable.");
            }
        }

        /// <summary>
        /// Demonstrate how to use <code>Push</code>and <code>Pop</code>to