Method EvalExample1

examples/dotnet/Program.cs:1739–1776

Demonstrate how to use #Eval.

(Context ctx)

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

            IntExpr x = ctx.MkIntConst("x");
            IntExpr y = ctx.MkIntConst("y");
            IntExpr two = ctx.MkInt(2);

            Solver solver = ctx.MkSolver();

            /* assert x < y */
            solver.Assert(ctx.MkLt(x, y));

            /* assert x > 2 */
            solver.Assert(ctx.MkGt(x, two));

            /* find model for the constraints above */
            Model model = null;
            if (Status.SATISFIABLE == solver.Check())
            {
                model = solver.Model;
                Console.WriteLine("{0}", model);
                Console.WriteLine("\nevaluating x+y");
                Expr v = model.Evaluate(ctx.MkAdd(x, y));
                if (v != null)
                {
                    Console.WriteLine("result = {0}", (v));
                }
                else
                {
                    Console.WriteLine("Failed to evaluate: x+y");
                }
            }
            else
            {
                Console.WriteLine("BUG, the constraints are satisfiable.");
            }
        }

        /// <summary>
        /// Demonstrate how to use #Eval on tuples.