Method LogicExample

examples/dotnet/Program.cs:1023–1051

Shows how to use Solver(logic)

(Context ctx)

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

            Microsoft.Z3.Global.ToggleWarningMessages(true);

            BitVecSort bvs = ctx.MkBitVecSort(32);
            Expr x = ctx.MkConst("x", bvs);
            Expr y = ctx.MkConst("y", bvs);
            BoolExpr eq = ctx.MkEq(x, y);

            // Use a solver for QF_BV
            Solver s = ctx.MkSolver("QF_BV");
            s.Assert(eq);
            Status res = s.Check();
            Console.WriteLine("solver result: " + res);


            // Or perhaps a tactic for QF_BV
            Goal g = ctx.MkGoal(true);
            g.Assert(eq);

            Tactic t = ctx.MkTactic("qfbv");
            ApplyResult ar = t.Apply(g);
            Console.WriteLine("tactic result: " + ar);

            if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedSat)
                throw new TestFailedException();
        }

        /// <summary>
        /// Demonstrates how to use the ParOr tactic.