Z3 和 Unsat 核心案例中的建模约束

Question

我正在使用 Z3 求解器并在 C# 中实现。我在他们的 .Net API (http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs) 描述中使用了 Microsoft 给出的示例。在此示例中，我尝试将函数“UnsatCoreAndProofExample”中的模型替换为我自己的模型：

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

我期望的结果是在 Unsat 代码中返回 Constraint1 和 Constraint4。我知道返回 Unsatcore 的设置是正确的，因为当我运行原始的“UnsatCoreAndProofExample”函数时，会返回 unsat Core。但是当我只是将模型更改为上面的模型时，虽然结果是 Unsat 但没有返回 Unsatcore。 所以我的问题是，可能是因为我编写模型的方式，还是我犯了另一个错误？

Answer 1

基础架构中确实存在一个错误，导致很难正确使用 AssertAndTrack。这现在已在不稳定分支中修复（修复为 here）。我还在使用 AssertAndTrack 获取核心的 .NET 和 Java 示例中添加了另一个示例。