Z3 2.x具有不弹出符号声明的功能(嗯,可能是bug),例如Z3 2.x接受以下代码:

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

Z3 3.x不再接受此代码(“未知常数”)。

有办法恢复旧的行为吗?或者以另一种方式如何在范围内声明符号,以使声明(并且仅声明,而不是假设)是全局的,即不弹出?

最佳答案

是的,在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))

07-24 09:37
查看更多