Getting Unsat core examples using Z3 and c#

Question

I am trying to use the Z3 sat solver in an C# implementation. This code is very close to the example given by Microsoft itself in "http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs". My code is:

using (Context ctx = new Context(new Dictionary<string, string>() { { "proof", "true" } }))
{
...
Expr x = ctx.MkConst("x", ctx.MkIntSort());
Expr y = ctx.MkConst("y", ctx.MkIntSort());
Expr zero = ctx.MkNumeral(0, ctx.MkIntSort());
Expr one = ctx.MkNumeral(1, ctx.MkIntSort());
Expr five = ctx.MkNumeral(5, ctx.MkIntSort());

Solver s = ctx.MkSolver();

s.Assert(ctx.MkGt((ArithExpr)x, (ArithExpr)zero)); // x > 0
s.Assert(ctx.MkLt((ArithExpr)y, (ArithExpr)five)); // y < 5
s.Assert(ctx.MkLt((ArithExpr)x, (ArithExpr)zero)); // x < 0
s.Assert(ctx.MkEq((ArithExpr)y, ctx.MkAdd((ArithExpr)x, (ArithExpr)one))); // y = x + 1

 Status result = s.Check();

 if (result == Status.UNSATISFIABLE)
 {
     Console.WriteLine("unsat");
     Console.WriteLine("proof: {0}", s.Proof);
     Console.WriteLine("core: ");
     foreach (Expr c in s.UnsatCore)
     {
         Console.WriteLine("{0}", c);
     }
 }

But still when I reach the "s.UnsatCore" for this model it is empty.

I have also tried to enter in the assertions like this:

BoolExpr constraint1 = ctx.MkBoolConst("Constraint1");
s.AssertAndTrack(ctx.MkGt((ArithExpr)x, (ArithExpr)zero), constraint1);
BoolExpr constraint2 = ctx.MkBoolConst("Constraint2");
s.AssertAndTrack(ctx.MkLt((ArithExpr)y, (ArithExpr)five), constraint2);
BoolExpr constraint3 = ctx.MkBoolConst("Constraint3");
s.AssertAndTrack(ctx.MkLt((ArithExpr)x, (ArithExpr)zero), constraint3);
BoolExpr constraint4 = ctx.MkBoolConst("Constraint4");
s.AssertAndTrack(ctx.MkEq((ArithExpr)y, ctx.MkAdd((ArithExpr)x, (ArithExpr)one)), constraint4);

I would want the UnsatCore to return "constraint1, constrint3". Can anyone help me on what I am doing wrong?

Please add what output get and what output you would expect. — Sebastian Stigler
I would expect to return the first and last constraint. I also wrote it like this: — Amir Ebrahimi
BoolExpr constraint1 = ctx.MkBoolConst("Constraint1"); s.AssertAndTrack(ctx.MkGt((ArithExpr)x, (ArithExpr)zero), constraint1); BoolExpr constraint2 = ctx.MkBoolConst("Constraint2"); s.AssertAndTrack(ctx.MkLt((ArithExpr)y, (ArithExpr)five), constraint2); BoolExpr constraint3 = ctx.MkBoolConst("Constraint3"); s.AssertAndTrack(ctx.MkLt((ArithExpr)x, (ArithExpr)zero), constraint3); — Amir Ebrahimi
BoolExpr constraint4 = ctx.MkBoolConst("Constraint4"); s.AssertAndTrack(ctx.MkEq((ArithExpr)y, ctx.MkAdd((ArithExpr)x, (ArithExpr)one)), constraint4); But still the s.UnsatCore is empty — Amir Ebrahimi
Don't use comment to provide useful information regarding the question : edit your post. — AFract

Jörg Pfähler Jörg Pfähler · Accepted Answer · 2015-02-11T16:50:42

Did you enable proof generation when creating ctx (the documentation of Solver.UnsatCore states that the result is empty if it is disabled)? You need to pass the Dictionary ("proof -> "true") to the constructor of Context to do so.

Getting Unsat core examples using Z3 and c#

1 Answers