声明在其范围之外仍然有效的符号 [英] Declare symbols that remain valid outside their scope

问题描述

Z3 2.x具有不弹出符号声明的功能（很可能是错误）。 Z3 2.x接受以下代码：

Z3 2.x had the feature (well, probably rather the bug) that symbol declarations were not popped away, e.g. the following code is accepted by 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 3.x no longer accepts this code ("unknown constant").

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

Is there a way to restore the old behaviour? Or another way how one could declare symbols inside scopes such that the declaration (and only the declaration, not the assumptions) is global, i.e. not popped?

推荐答案

是的，在Z3 2.x中，所有声明都是全局的。我们在Z3 3.x中更改了此行为，因为SMT-LIB 2.0标准指出所有声明都应具有作用域。
您可以使用选项：global-decls 恢复旧的行为。

Yes, in Z3 2.x all declarations were global. We changed this behavior in Z3 3.x because the SMT-LIB 2.0 standard states that all declarations should be scoped. You can restore the old behavior using the option :global-decls.

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

这篇关于声明在其范围之外仍然有效的符号的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！