1

我已阅读有关非线性算术和未解释函数的帖子。我对 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 的问题，但返回unknown了 Ints 的情况，但是，我仍然可以获得满足约束的 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 ...)根据断言的类型使用？

4

1 回答 1

3

由于您混合了实数和整数排序，我认为您需要使用check-sat-using. 从Z3 如何处理非线性整数算术？：

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

您正在强制 Z3 在整数约束上使用非线性实数算术求解器(check-sat-using qfnra-nlsat)。这也是如何在 Python 中使用 z3py 进行操作的方法：z3 在这个方程组中失败

我想在未来的某个时候（尽管开发人员可以确认）你不必这样做，但我听到的最后一次（参见例如混合实数和位向量以及在线使用 Z3Py 来证明 n^5 <= 5 ^n for n >= 5 )，非线性实数算术求解器策略尚未与其他求解器完全集成。

于 2013-10-29T15:19:28.923 回答