Method ModelConverterTest

examples/dotnet/Program.cs:300–327

(Context ctx)

        }

        static void ModelConverterTest(Context ctx)
        {
            Console.WriteLine("ModelConverterTest");

            ArithExpr xr = (ArithExpr)ctx.MkConst(ctx.MkSymbol("x"), ctx.MkRealSort());
            ArithExpr yr = (ArithExpr)ctx.MkConst(ctx.MkSymbol("y"), ctx.MkRealSort());
            Goal g4 = ctx.MkGoal(true);
            g4.Assert(ctx.MkGt(xr, ctx.MkReal(10, 1)));
            g4.Assert(ctx.MkEq(yr, ctx.MkAdd(xr, ctx.MkReal(1, 1))));
            g4.Assert(ctx.MkGt(yr, ctx.MkReal(1, 1)));

            ApplyResult ar = ApplyTactic(ctx, ctx.MkTactic("simplify"), g4);
            if (ar.NumSubgoals == 1 && (ar.Subgoals[0].IsDecidedSat || ar.Subgoals[0].IsDecidedUnsat))
                throw new TestFailedException();

            ar = ApplyTactic(ctx, ctx.AndThen(ctx.MkTactic("simplify"), ctx.MkTactic("solve-eqs")), g4);
            if (ar.NumSubgoals == 1 && (ar.Subgoals[0].IsDecidedSat || ar.Subgoals[0].IsDecidedUnsat))
                throw new TestFailedException();

            Solver s = ctx.MkSolver();
            foreach (BoolExpr e in ar.Subgoals[0].Formulas)
                s.Assert(e);
            Status q = s.Check();
            Console.WriteLine("Solver says: " + q);
            Console.WriteLine("Model: \n" + s.Model);
            if (q != Status.SATISFIABLE)
                throw new TestFailedException();
        }

        /// <summary>
        /// A simple array example.