3

使用 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 吗？

4

1 回答 1

3

这是一个很好的问题。不幸的是，如果您将自己限制在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))

（您可能必须小心计算zIwhen z < 0，但想法是一样的。）

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

如果您有sin并且pi：

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

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

对有理数的限制

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

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

于 2017-02-09T21:52:07.363 回答