带SMTlib2输入的z3

Question

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

下面是SMTlib2输入，它在SMT4.1(和其他z3解算器...)中工作得很好，但在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)

在z3 4.3.1中删除最后一个bs_2声明效果很好，但在z3 4.1中就不行了。我是不是用错了推送/弹出？

Answer 1

在SMT4.3.1中，我们试图放松Z3 -LIB2.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)。