UnsatCoresDemo.cs

using System;
using System.Collections.Generic;
using Microsoft.Z3;

namespace unsat_cores_csharp
{
    class Program
    {
        public static void UnsatCoreAndProofExample(Context ctx)
        {
            Console.WriteLine("UnsatCoreAndProofExample");

            Solver solver = ctx.MkSolver();

            BoolExpr pa = ctx.MkBoolConst("PredA");
            BoolExpr pb = ctx.MkBoolConst("PredB");
            BoolExpr pc = ctx.MkBoolConst("PredC");
            BoolExpr pd = ctx.MkBoolConst("PredD");
            
            BoolExpr p1 = ctx.MkBoolConst("P1");
            BoolExpr p2 = ctx.MkBoolConst("P2");
            BoolExpr p3 = ctx.MkBoolConst("P3");
            BoolExpr p4 = ctx.MkBoolConst("P4");
            
            Expr[] assumptions = new Expr[] { ctx.MkNot(p1), ctx.MkNot(p2), ctx.MkNot(p3), ctx.MkNot(p4) };
            BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc });
            BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc });
            BoolExpr f3 = ctx.MkOr(ctx.MkNot(pa), ctx.MkNot(pc));
            BoolExpr f4 = pd;

            solver.Assert(ctx.MkOr(f1, p1));
            solver.Assert(ctx.MkOr(f2, p2));
            solver.Assert(ctx.MkOr(f3, p3));
            solver.Assert(ctx.MkOr(f4, p4));
            
            Status result = solver.Check(assumptions);

            if (result == Status.UNSATISFIABLE)
            {
                Console.WriteLine("unsat");
                Console.WriteLine("proof: {0}", solver.Proof);
                Console.WriteLine("core: ");
                foreach (Expr c in solver.UnsatCore)
                {
                    Console.WriteLine("{0}", c);
                }
            }
        }
        
        public static void UnsatCoreAndProofExample2(Context ctx)
        {
            Console.WriteLine("UnsatCoreAndProofExample2");

            Solver solver = ctx.MkSolver();

            BoolExpr pa = ctx.MkBoolConst("PredA");
            BoolExpr pb = ctx.MkBoolConst("PredB");
            BoolExpr pc = ctx.MkBoolConst("PredC");
            BoolExpr pd = ctx.MkBoolConst("PredD");

            BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc });
            BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc });
            BoolExpr f3 = ctx.MkOr(ctx.MkNot(pa), ctx.MkNot(pc));
            BoolExpr f4 = pd;

            BoolExpr p1 = ctx.MkBoolConst("P1");
            BoolExpr p2 = ctx.MkBoolConst("P2");
            BoolExpr p3 = ctx.MkBoolConst("P3");
            BoolExpr p4 = ctx.MkBoolConst("P4");

            solver.AssertAndTrack(f1, p1);
            solver.AssertAndTrack(f2, p2);
            solver.AssertAndTrack(f3, p3);
            solver.AssertAndTrack(f4, p4);
            Status result = solver.Check();

            if (result == Status.UNSATISFIABLE)
            {
                Console.WriteLine("unsat");
                Console.WriteLine("core: ");
                foreach (Expr c in solver.UnsatCore)
                {
                    Console.WriteLine("{0}", c);
                }
            }
        }
        
        static void Main(string[] args)
        {
            using (Context ctx = new Context(new Dictionary<string, string>() { { "proof", "true" } }))
            {
                UnsatCoreAndProofExample(ctx);
                UnsatCoreAndProofExample2(ctx);
            }
        }
    }
}