Ограничения моделирования в случаях ядра Z3 и Unsat

Question

Я использую решатель Z3 и реализую в C#. Я использовал пример, предоставленный Microsoft, в описании их .Net API (http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs). В этом примере я попытался заменить модель в функции «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(); 

Результат, который я ожидаю, чтобы сказать, что Constraint1 и Constraint4 возвращаются в Unsat Кодекса. Я знаю, что настройка для возврата Unsatcore верна, потому что, когда я запускаю исходную функцию UnsatCoreAndProofExample, возвращается unsat Core. Но когда я просто меняю модель на модель выше, хотя результатом является Unsat, но не возвращается Unsatcore. Итак, мой вопрос: может ли это быть из-за того, как я пишу свою модель или есть другая ошибка, которую я делаю?

Answer 1

В инфраструктуре действительно была ошибка, из-за которой было очень сложно правильно использовать AssertAndTrack. Теперь это исправлено в нестабильной ветке (исправление here). Я также добавил еще один пример примеров .NET и Java, которые используют AssertAndTrack для получения ядра.