Z3 中的增量输入和断言集

Question

我有一个运行 Z3 版本 4.8.8 - 64 位的程序，带有增量输入：程序启动 Z3 一次，对 Z3 执行多轮输入输出，然后停止 Z3。出于性能原因，在没有增量输入的情况下运行 Z3 不是一种选择。

每一轮，程序向Z3输入一些(assert ...)语句，向Z3输入(check-sat)，然后从Z3获取(check-sat)的输出。

我有两轮输入输出：第一轮输入如z3.sat：

(declare-fun f () Int)
(declare-fun n () Int)
(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not false))
(check-sat)

这意味着：f 是偶数 Int 大于或等于 2。

第二轮输入如z3.unsat：

(declare-fun f () Int)
(declare-fun n () Int)
(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not (exists ((alpha Int)) (= (* 2 alpha) f))))
(check-sat)

这意味着：如果f 是偶数Int 大于或等于2，则存在alpha 其中alpha=f/2。

我假设使用增量输入运行 Z3 类似于将两轮输入 z3.sat 和 z3.unsat 连接到一个输入中，如 z3.combined：

(declare-fun f () Int)
(declare-fun n () Int)
(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not false))
(check-sat)
(declare-fun f () Int)
(declare-fun n () Int)
(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not (exists ((alpha Int)) (= (* 2 alpha) f))))
(check-sat)

跑步：

• z3 -smt2 z3.sat 输出 sat
• z3 -smt2 z3.unsat 输出 unsat
• z3 -smt2 z3.combined 输出错误，因为第一轮的 (assert ...) 语句不会消失：

  sat
  (error "line 8 column 21: invalid declaration, constant 'f' (with the given signature) already declared")
  (error "line 9 column 21: invalid declaration, constant 'n' (with the given signature) already declared")
  unknown
  

所以Z3似乎需要(push 1)和(pop 1)语句来忘记之前的断言集，所以我在z3.sat和z3.unsat的开头和结尾添加了这些语句，并重新连接了z3.pushpop.sat和z3.pushpop.unsat 得到z3.pushpop.combined。

• z3.pushpop.sat:

  (push 1)
  (declare-fun f () Int)
  (declare-fun n () Int)
  (assert (< 1 n))
  (assert (<= 2 f))
  (assert (= (+ (+ 1 f) 1) (+ n n)))
  (assert (not false))
  (check-sat)
  (pop 1)
  

• z3.pushpop.unsat:

  (push 1)
  (declare-fun f () Int)
  (declare-fun n () Int)
  (assert (< 1 n))
  (assert (<= 2 f))
  (assert (= (+ (+ 1 f) 1) (+ n n)))
  (assert (not (exists ((alpha Int)) (= (* 2 alpha) f))))
  (check-sat)
  (pop 1)
  

• z3.pushpop.combined:

  (push 1)
  (declare-fun f () Int)
  (declare-fun n () Int)
  (assert (< 1 n))
  (assert (<= 2 f))
  (assert (= (+ (+ 1 f) 1) (+ n n)))
  (assert (not false))
  (check-sat)
  (pop 1)
  (push 1)
  (declare-fun f () Int)
  (declare-fun n () Int)
  (assert (< 1 n))
  (assert (<= 2 f))
  (assert (= (+ (+ 1 f) 1) (+ n n)))
  (assert (not (exists ((alpha Int)) (= (* 2 alpha) f))))
  (check-sat)
  (pop 1)
  

但是，现在正在运行：

• z3 -smt2 z3.pushpop.sat 输出 sat
• z3 -smt2 z3.pushpop.unsat 输出 unknown
• z3 -smt2 z3.pushpop.combined 输出：

  sat
  unknown
  

为什么z3 -smt2 z3.pushpop.unsat 输出unknown？

Answer 1

正如 Malte 所提到的，pus/pop 的存在会在 z3 中触发“较弱”的求解器。 （这有很多技术原因，但我同意从最终用户的角度来看，行为的变化是不幸的，并且可能相当混乱。）

但是有些命令可以让你做你想做的事，而无需诉诸 push 和 pop。而不是它，只需插入：

(reset)

当您想“开始”一个新会话时，这将确保一切正常。也就是说，删除push/pop，并在连接时在其间插入(reset)。

稍微好一点的方法

虽然上述方法可行，但通常您只想忘记断言，而不是定义。也就是说，您要“记住”您在环境中有一个f 和一个n。如果这是您的用例，请将以下内容放在脚本的顶部：

(set-option :global-declarations true)

当你想“切换”到一个新问题时，发出：

(reset-assertions)

这样，您就不必每次都“重复”声明。也就是说，您的整个交互应该如下所示：

(set-option :global-declarations true)

(declare-fun f () Int)
(declare-fun n () Int)

(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not false))
(check-sat)

(reset-assertions)

(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not (exists ((alpha Int)) (= (* 2 alpha) f))))
(check-sat)

产生：

sat
unsat

参考

所有这些都记录在官方SMTLib document 中。见第 3.9 节，第 1 页。 44，对于global-declarations 的描述，以及第 4.2.2 节，第 4 页。 59，对于(reset-assertions)的描述。

Answer 2

增量模式强制 Z3 使用不同的理论子求解器，正如 this SO answer 中的一位开发人员所解释的那样。这些“增量模式”子求解器通常不如“常规”子求解器有效，或者至少可能表现不同。据我所知，只要 SMT 程序包含 push-pop 范围或多个 check-sat，Z3 就会切换到增量模式。

您最初说不使用增量模式不是一种选择，但至少您的文件z3.pushpop.combined 看起来很容易拆分。另一种选择可能是在两者之间重置 Z3（我认为 SMT 命令 (reset) 存在用于此目的），而不是使用 push-pop 块。但是，如果我上面所说的是正确的，这不会阻止 Z3 保持非增量模式。您可以考虑通过 Z3 问题跟踪器上的“问题问题”询问开发人员。