Твърдения за именуване на Microsoft Z3

Трябва да назова някои твърдения в моя модел z3, така че да може да генерира ненаситени ядра.

Мога да направя това ръчно по следния начин:

(assert (! (assertion) :named x))

Просто трябва да го направя с помощта на .NET API директно.

някаква помощ?


person Daniel    schedule 22.04.2013    source източник


Отговори (1)


Z3 не поддържа това директно чрез .NET API. Вместо това трябва да се създаде булева константа (името, напр. x), която след това може да се използва за налагане на условни ограничения, напр.

solver.AssertAndTrack(constraint, x);

След това ограничението се нарича x и тази константа се използва за позоваване на него в ненаситените ядра. За пример в Python вижте и този друг въпрос; стратегията е същата в .NET API, само имената на функциите се различават леко.

person Christoph Wintersteiger    schedule 23.04.2013
comment
Кристоф: методът съществува и извикването му работи добре. Въпреки това, когато е ненаситено, все още не се генерира ненаситено ядро - person Cristiano Sousa; 24.04.2013
comment
Предполагам, че тогава не сте активирали unsat core генериране. Имайте предвид, че MkGoal приема булеви параметри, които позволяват модели, ненаситени ядра или доказателства. Освен това глобалната опция unsat_core трябва да бъде активирана. - person Christoph Wintersteiger; 29.04.2013
comment
Кристоф: опцията е активирана. проблемът е в самия JAVA API, той е малко непостоянен. Понякога генерира unsatcore, а понякога не - person Cristiano Sousa; 15.05.2013
comment
Виждам. Не знам как може да се случи това. Имате ли пример, който показва това непостоянно поведение? - person Christoph Wintersteiger; 17.05.2013