Smtlib麻煩代碼

Question

我有這個下面的代碼

(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 

代碼應在第一（檢查-SAT）返回不飽和度，坐在第二（檢查-SAT），但我得到未知。

有人可以告訴我什麼是問題。我使用Windows 7，jSMTLIB使用cygwin的

感謝 賽義夫

Answer 1

我不知道你是用來解決此其後端的jSMTLIB。但是，在SMT-LIB v2中，(check-sat (= x w))甚至不合法。

當我改變該行：

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

我得到unsat和Z3 web界面，這是我們期待的sat。

請注意(get-info :statistics)也是不正確的;正確的選項是(get-info :all-statistics)。您可以在their documentation中閱讀更多關於SMT-LIB v2標準的信息。