3

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

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

4

1 回答 1

0

是的,在 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))
于 2011-09-07T17:23:04.363 回答