CODEWITHSUNDEEP
c#z3smt
Amir Ebrahimi
Amir Ebrahimi

Reputation: 115

Modeling constraints in Z3 and Unsat core cases

I am using the Z3 solver and implementing in C#. I have used the example given by Microsoft in the description of their .Net API (http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs). In this example I have tried to replace the model in function "UnsatCoreAndProofExample" with my own model which is:

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());

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

Status result = solver.Check();

The result which I am expecting is to say that Constraint1 and Constraint4 are returned in the Unsat Code. I know that the setting for returning the Unsatcore are correct because when I run the original "UnsatCoreAndProofExample" function the unsat Core is returned. But when I JUST change the model to the model above although the result is Unsat but no Unsatcore is returned. So my question is, could it be because of the way I am writing my model or is there another mistake I am making?

Upvotes: 3

Views: 212

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

There was indeed a bug in the infrastructure which made it very hard to use AssertAndTrack correctly. This is now fixed in the unstable branch (fix is here). I've also added another example to the .NET and Java examples that uses AssertAndTrack to get a core.

Upvotes: 2

Related Questions