Много благодаря на Джош и Леонардо за отговора на предишния въпрос.
Имам още няколко въпроса.
‹1> Помислете за друг пример.
(exists k) i * k > = 4 and k > 1.
Това има просто решение i > 0. (както за Int, така и за Real случай)
Въпреки това, когато се опитах да следвам,
(declare-const i Int)
(assert (exists ((k Int)) (and (>= (* i k) 4) (> k 1))))
(apply (using-params qe :qe-nonlinear true))
Z3 Не може да елиминира квантификатора тук.
Въпреки това, това може да елиминира за истински случай. (когато i и k са реални) Елиминирането на квантора по-трудно ли е за цели числа?
‹2> Използвам Z3 C API в моята система. Добавям някои нелинейни ограничения за цели числа с квантори в моята система. Z3 в момента проверява за задоволимост и ми дава правилен модел, когато системата е задоволителна.
Знам, че след елиминирането на квантора тези ограничения се редуцират до линейни ограничения.
Мислех, че z3 автоматично елиминира квантора, преди да провери задоволимостта. Но тъй като не можеше да направи това в случай 1 по-горе, сега мисля, че обикновено намира модел без елиминиране на квантификатор. Прав ли съм?
В момента z3 може да разреши ограниченията в моята система. Но може да се провали при сложни системи. В такъв случай, добра идея ли е да се направи елиминиране на квантора по някакъв друг метод без z3 и да се добавят ограничения към z3 по-късно?
‹3> Мога да се сетя да добавя реални нелинейни ограничения вместо целочислени нелинейни ограничения в моята система. В такъв случай, как мога да наложа z3 да извършва Quantifier Elimination с помощта на C-API?
‹4> И накрая, това добра идея ли е да наложите z3 да извършва Quantifier Elimination? Или обикновено намира модел по-интелигентно, без да прави Quantifier Elimination?
Благодаря.
