在 QF_UFNRA 中获取实数的小数部分答案

【问题标题】：Get fractional part of real in QF_UFNRA在 QF_UFNRA 中获取实数的小数部分
【发布时间】：2017-06-27 06:49:10
【问题描述】：

使用 smtlib 我想使用 QF_UFNRA 进行模运算。这使我无法使用 mod、to_int、to_real 之类的东西。

最后我想在下面的代码中得到z的小数部分：

(set-logic QF_UFNRA)

(declare-fun z () Real)
(declare-fun z1 () Real)
(define-fun zval_1 ((x Real)) Real
         x
)
(declare-fun zval (Real) Real)

(assert (= z 1.5));
(assert (=> (and (<= 0.0 z) (< z 1.0)) (= (zval z) (zval_1 z))))
(assert (=> (>= z 1.0) (= (zval z) (zval (- z 1.0)))))
(assert (= z1 (zval z)))

当然，正如我在这里提出的这个问题，暗示它没有成功。

有人知道如何使用逻辑 QF_UFNRA 将 z 的小数部分转换为 z1 吗？

【问题讨论】：

标签： z3 smt cvc4

【解决方案1】：

这是一个很好的问题。不幸的是，如果您将自己限制在QF_UFNRA，您想要做的事情通常不可能。

如果您可以对此类功能进行编码，那么您可以决定任意丢番图方程。您只需将给定的丢番图方程转换为实数，使用这种所谓的方法计算实数解的“分数”，并断言该分数是0。由于实数是可判定的，这将为您提供丢番图方程的判定程序，完成不可能的事情。（这被称为希尔伯特第十问题。）

因此，尽管任务看起来很无辜，但实际上是不可行的。但这并不意味着您不能使用某些扩展对其进行编码，并且可能让求解器成功决定它的实例。

如果你允许量词和递归函数

如果你允许自己使用量词和递归函数，那么你可以这样写：

(set-logic UFNRA)

(define-fun-rec frac ((x Real)) Real (ite (< x 1) x (frac (- x 1))))

(declare-fun res () Real)
(assert (= (frac 1.5) res))

(check-sat)
(get-value (res))

z3 的回应：

sat
((res (/ 1.0 2.0)))

请注意，我们使用了允许量化的 UFNRA 逻辑，由于使用了 define-fun-rec 构造，此处隐含地需要量化。（有关详细信息，请参阅 SMTLib 手册。）这基本上是您在问题中尝试编码的内容，而是使用递归函数定义工具而不是隐式编码。然而，在 SMTLib 中使用递归函数有几个注意事项：特别是，您可以编写使系统变得不一致的函数，这很容易。有关详细信息，请参阅http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-draft.pdf 的第 4.2.3 节。

如果你可以使用 QF_UFNIRA

如果你转移到QF_UFNIRA，即允许混合实数和整数，编码很容易：

(set-logic QF_UFNIRA)

(declare-fun z  () Real)
(declare-fun zF () Real)
(declare-fun zI () Int)

(assert (= z (+ zF zI)))
(assert (<= 0 zF))
(assert (< zF 1))

(assert (= z 1.5))
(check-sat)
(get-value (zF zI))

z3 回应：

sat
((zF (/ 1.0 2.0))
 (zI 1))

（zI和z < 0的计算可能要小心，但思路是一样的。）

请注意，仅仅因为编码简单并不意味着 z3 总是能够成功回答查询。由于Real's 和Integer's 的混合，问题仍然无法确定，如前所述。如果您对z 有其他限制，z3 可能会很好地响应unknown 这种编码。在这种特殊情况下，它恰好足够简单，因此 z3 能够找到模型。

如果你有`sin` 和`pi`：

这更像是一个思想实验，而不是真正的替代方案。如果 SMTLib 允许 sin 和 pi，那么您可以检查 sin (zI * pi) 是否为 0，以获得适当约束的 zI。此查询的任何令人满意的模型都将确保zI 是整数。然后，您可以使用此值通过从 z 中减去 zI 来提取小数部分。

但这是徒劳的，因为 SMTLib 既不允许 sin 也不允许 pi。并且有充分的理由：可判定性将丢失。话虽如此，也许一些勇敢的灵魂可以设计一个支持sin、pi 等的逻辑，并成功正确回答您的查询，同时在问题变得难以解决时返回unknown。这已经是非线性算术和QF_UFNIRA 片段的情况：求解器通常可能会放弃，但它采用的启发式方法可能会解决实际感兴趣的问题。

对 Rationals 的限制

撇开理论不谈，事实证明，如果您只使用有理数（而不是实际实数），那么您确实可以编写一个一阶公式来识别整数。但是，编码不适合胆小的人：http://math.mit.edu/~poonen/papers/ae.pdf。此外，由于编码涉及量词，因此 SMT 求解器不太可能很好地使用基于此想法的公式。

[顺便说一句，我应该感谢我的工作同事；这个问题促成了一次很棒的午餐时间谈话！]

【讨论】：

感谢您的回答！实际上，我的问题是（并且是）将 sin（和其他三角函数）近似为 SMT 问题。为此，我想将传入变量计算为 0
酷。你应该结帐dReal:cs.cmu.edu/~sicung/papers/dReal.pdf。我自己没有使用过它，但它声称使用 δ-可满足性的概念来支持三角函数。（这个问题一般来说是不可判定的，但是如果你允许一定的精度损失，可以检查可满足性。）
另外：如果你可以转移到定理证明环境，MetiTarski 是一个支持超越的强大工具：cl.cam.ac.uk/~lp15/papers/Arith
我试过 dReal3。非常好，但缺少模型和 UNSAT 核心。只是为了让您知道。

如果你允许量词和递归函数

如果你可以使用 QF_UFNIRA

如果你有sin 和pi：

对 Rationals 的限制

如果你有`sin` 和`pi`：