带 SMTlib2 输入的 z3

【问题标题】：z3 with SMTlib2 input带 SMTlib2 输入的 z3
【发布时间】：2012-11-20 13:03:52
【问题描述】：

我刚刚将 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。我是否使用了 push/pop 错误？

【问题讨论】：

标签： z3

【解决方案1】：

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

(set-option :global-decls false)

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

【讨论】：