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 不再接受此代码(“未知常量”)。
有没有办法恢复旧的行为?或者另一种方式如何在范围内声明符号,使得声明(并且只有声明,而不是假设)是全局的,即不弹出?
最佳答案
是的,在 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))
关于scope - 声明在其范围之外仍然有效的符号,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/7337783/