3

我刚刚将 z3 从 4.1 升级到 4.3.1，似乎 smtlib2 输入发生了变化：现在，pop 语句不会删除函数/常量声明。

这是与 z3 4.1（和其他 SMT 求解器...）一起正常工作的 SMTlib2 输入，但在 z3 4.3.1 中返回错误：（错误“第 19 行第 25 列：无效声明，常量 'bs_2'（其中给定签名）已经声明“）

(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(set-option :interactive-mode true)
(set-option :print-success false)
(push 1)
(declare-fun bs_1 () Bool)
(push 1)
(declare-fun bs_2 () Bool)
(assert (and  bs_1 (not bs_2)))
(check-sat)
(pop 1)
(push 1)
(declare-fun bs_2 () Bool)
(assert (and  bs_1 (not bs_2)))
(check-sat)
(pop 1)
(pop 1)
(exit)

删除最后一个 bs_2 声明适用于 z3 4.3.1，但不适用于 z3 4.1。我使用推送/弹出错误吗？

4

1 回答 1

4

在 Z3 4.3.1 中，我们尝试放宽了 SMT-LIB 2.0 的一些限制，让 Z3 使用起来更方便。例如，我们现在可以写(+ x 2)而不是(+ x 2.0)when xis Real。声明是全局的，而不是像 Z3 4.1 中的范围。其动机是允许用户更简洁地编码问题。我们可以使用以下选项来启用范围声明，如 Z3 4.1

(set-option :global-decls false)

话虽如此，我知道这种变化对于习惯于其他 SMT 求解器或阅读描述 SMT-LIB 标准的手册的用户来说是非常令人困惑和违反直觉的。因此，我们将默认更改回(set-option :global-decls false).

于 2012-11-20T15:11:03.213 回答