Smtlib проблемы с кодом - PullRequest
Новая
       8

Smtlib проблемы с кодом

1 голос
/ 23 февраля 2012

У меня есть следующий код 

(set-logic QF_LIA)
(declare-fun w () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (> x y))
(assert (> y z))
(push 1)
(assert (> z x))
(check-sat) ; unsat
(get-info :statistics)
(pop 1)
(push 1)
(check-sat (= x w)) ; sat

Код должен возвращать unsat на первом (check-sat) и сидеть на втором (check-sat), но я не знаю.Может кто-нибудь подскажите пожалуйста в чем проблема.Я использую Windows 7, jSMTLIB с помощью Cygwin

Спасибо Saif

1 Ответ

3 голосов
/ 23 февраля 2012

Я не знаю, какой бэкэнд в jSMTLIB вы использовали для решения этой проблемы.Однако (check-sat (= x w)) недопустимо даже в SMT-LIB v2.

Когда я изменяю эту строку на: 

(assert (= x w))
(check-sat)

Я получаю unsat и sat из веб-интерфейса Z3, что является нашим ожиданием.

Обратите внимание, что (get-info :statistics) также неверно;правильный вариант - (get-info :all-statistics).Вы можете прочитать больше о стандарте SMT-LIB v2 в их документации .

...