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

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

(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) и sat на втором (check-sat), но я не знаю.

Подскажите, пожалуйста, в чем проблема. Я использую windows 7, jSMTLIB, используя cygwin

Спасибо, Саиф


z3 smt
person Saif    schedule 22.02.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Я не знаю, какой бэкэнд в 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 в их документации.

person pad    schedule 23.02.2012