聲明在其範圍外仍然有效的符號

Question

Z3 2.x具有符號聲明未被彈出的特徵（很好，可能相當於錯誤），例如，以下代碼被Z3 2.x接受：

(push) 
(declare-fun x() Int) 
; Assumptions made in this scope will be popped correctly 
(pop) 
(assert (= x x)) 

Z3 3.x不再接受此代碼（「未知常量」）。

有沒有辦法恢復舊的行爲？或者，另一種方式是如何在範圍內聲明符號，使得聲明（以及只有聲明，而不是假設）是全局的，即沒有彈出？

Answer 1

是的，在Z3 2.x中所有的聲明都是全局的。我們在Z3 3.x中改變了這種行爲，因爲SMT-LIB 2.0標準規定所有聲明都應該被限定範圍。 您可以使用選項:global-decls恢復舊行爲。

(set-option :global-decls true) 
(push) 
(declare-fun x() Int) 
(pop) 
(assert (= x x))