结合非线性 Real 和线性 Int [英] Combining nonlinear Real with linear Int

问题描述

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

I've read the posts about nonlinear arithmetic and uninterpreted functions. I'm still very new to SMT world, so apologies if I'm not using the right vocabulary or this is a bad question.

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

For the following code, there are asserts put onto the stack above an unrelated top-level assert, (assert (> i 10)). However, Z3 returns unsat for the case with Reals (the first push to the first pop). I think this has something to do with an attempt by Z3 to use an Int solver since the first assertion was on an Int, and Z3 assigns e1 to (/ 1.0 2.0), a number with no Int representation, because of the constraint (assert (< e3 1)) (if I remove this constraint, it works). Using (check-sat-using qfnra-nlsat) solves the problem for Reals, but returns unknown for the case of Ints, However, I can still get model for the Int case that satisfies the constraints.

(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 ...) 取决于断言的类型?

Is there single call to check that I can use in all cases, or will I need to use (check-sat-using ...) depending on the types that were asserted on?

推荐答案

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

Since you are mixing real and integer sorts, I think you'll need to use check-sat-using. From How does Z3 handle non-linear integer arithmetic?:

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

"the nonlinear real arithmetic (NLSat) solver is not used by default for nonlinear integer problems. It is usually very ineffective on integer problems. Nonetheless, we can force Z3 to use NLSat even for integer problems."

您强制 Z3 使用 (check-sat-using qfnra-nlsat) 在整数约束上使用非线性实数算术求解器.以下是如何使用 z3py 在 Python 中执行此操作:z3 失败这个方程组

You're forcing Z3 to use the nonlinear real arithmetic solver on the integer constraints with the (check-sat-using qfnra-nlsat). Here's also how to do it in Python with z3py: z3 fails with this system of equations

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

I imagine at some point in the future (although devs can confirm) you will not have to do this, but the last I heard (see e.g., mixing reals and bit-vectors and Using Z3Py online to prove that n^5 <= 5 ^n for n >= 5), the nonlinear real arithmetic solver tactic is not fully integrated with the other solvers yet.

这篇关于结合非线性 Real 和线性 Int的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！