将非线性 Real 与线性 Int 相结合

Question

我已阅读有关非线性算术和未解释函数的帖子。我对 SMT 世界还是很陌生，所以如果我没有使用正确的词汇或者这是一个糟糕的问题，我深表歉意。

对于以下代码，在堆栈中放置了一些断言，位于不相关的顶级断言(assert (> i 10)) 之上。但是，对于 Reals 的情况，Z3 返回 unsat（第一次推送到第一次弹出）。我认为这与 Z3 尝试使用 Int 求解器有关，因为第一个断言是在 Int 上，并且 Z3 将 e1 分配给 (/ 1.0 2.0)，这是一个没有 Int 表示的数字，因为约束 (assert (< e3 1)) (如果我删除这个约束，它会起作用）。使用(check-sat-using qfnra-nlsat) 解决了Reals 的问题，但对于Ints 的情况返回unknown，但是，我仍然可以获得满足约束的Int 情况的模型。

(set-option :global-decls false)

(declare-const i Int)
(assert (> i 10))

(push)
  (declare-const e1 Real)
  (declare-const e2 Real)

  (define-fun e3 () Real (/ e1 e2))
  (assert (> e1 0))
  (assert (> e2 0))
  (assert (< e3 1))

  ;(check-sat-using qfnra-nlsat)
  (check-sat)
(pop)
(push)
  (declare-const e1 Int)
  (declare-const e2 Int)

  (define-fun e3 () Int (div e1 e2))
  (assert (> e2 0))
  (assert (> e3 0))

  ;(check-sat-using qfnra-nlsat)
  (check-sat)
(pop)

是否有一次调用来检查我是否可以在所有情况下使用，或者我是否需要根据断言的类型使用(check-sat-using ...)？

Answer 1

由于您混合了实数和整数排序，我认为您需要使用check-sat-using。来自How does Z3 handle non-linear integer arithmetic?：

“非线性实数算术 (NLSat) 求解器默认情况下不用于非线性整数问题。它通常对整数问题非常无效。尽管如此，我们可以强制 Z3 使用 NLSat，即使是整数问题。”

您正在强制 Z3 对带有 (check-sat-using qfnra-nlsat) 的整数约束使用非线性实数算术求解器。这也是在 Python 中使用 z3py 的方法：z3 fails with this system of equations

我想在未来的某个时候（尽管开发人员可以确认）你不必这样做，但我听说的最后一次（参见例如，mixing reals and bit-vectors 和Using Z3Py online to prove that n^5 <= 5 ^n for n >= 5），非线性实数算术求解器策略是尚未与其他求解器完全集成。