z3與SMTlib2輸入

Question

我剛剛將z3從4.1升級到4.3.1，並且似乎smtlib2輸入已更改： 現在，函數/常量聲明不會被pop語句刪除。

以下是可以在z3 4.1（和其他SMT求解器...）下正常工作的SMTlib2輸入，但是返回的錯誤是z3 4.3.1：（錯誤「第19行第25列：無效聲明，常量'bs_2 「（蒙山給定的簽名）已聲明」）

(set-option :produce-models true) 
(set-option :produce-unsat-cores true) 
(set-option :interactive-mode true) 
(set-option :print-success false) 
(push 1) 
(declare-fun bs_1() Bool) 
(push 1) 
(declare-fun bs_2() Bool) 
(assert (and bs_1 (not bs_2))) 
(check-sat) 
(pop 1) 
(push 1) 
(declare-fun bs_2() Bool) 
(assert (and bs_1 (not bs_2))) 
(check-sat) 
(pop 1) 
(pop 1) 
(exit) 

刪除最後BS_2宣言正常工作與Z3 4.3.1，而不是Z3 4.1。 我使用push/pop錯誤嗎？

Answer 1

在Z3 4.3.1中，我們試圖放寬一些SMT-LIB 2.0的限制，以使Z3更便於使用。例如，當x是Real時，我們現在可以寫(+ x 2)而不是(+ x 2.0)。聲明是全局的，而不像Z3 4.1那樣。動機是讓用戶更簡潔地編碼問題。我們可以使用下面的選項來啓用範圍的聲明像Z3 4.1

(set-option :global-decls false) 

話雖這麼說，我理解這種變化是非常混亂，反直覺的用戶所使用到其他SMT求解器，或讀一本手冊描述SMT-LIB標準。因此，我們會將默認值更改回(set-option :global-decls false)。