声明在其范围之外仍然有效的符号答案

【问题标题】：Declare symbols that remain valid outside their scope声明在其范围之外仍然有效的符号
【发布时间】：2011-09-07 17:07:58
【问题描述】：

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 不再接受此代码（“未知常量”）。

有没有办法恢复旧的行为？或者另一种方式，如何在范围内声明符号，使得声明（并且只有声明，而不是假设）是全局的，即不弹出？

【问题讨论】：

【解决方案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))

【讨论】：