在 QF_UFNRA 中获取实数的小数部分
Get fractional part of real in QF_UFNRA
使用 smtlib 我想使用 QF_UFNRA 制作类似 modulo 的东西。这使我无法使用 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 吗？
这是一个很好的问题。不幸的是，如果您将自己限制在 QF_UFNRA.
，您想要做的通常是 不可能的
如果你能编码这样的功能，那么你就可以决定任意的丢番图方程。您只需将给定的丢番图方程投射到实数上，使用这种所谓的方法计算实数解的 "fraction"，并断言分数为 0。由于实数是可判定的，这将为您提供丢番图方程的判定程序，从而完成不可能的事情。 （这被称为希尔伯特第十问题。）
因此，尽管任务看起来很简单，但实际上是无法完成的。但这并不意味着你不能用一些扩展来编码它，并且可能让求解器成功地决定它的实例。
如果允许量词和递归函数
如果你允许自己使用量词和recursive-functions，那么你可以这样写：
(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 手册。）这实际上是您尝试在问题中编码的内容，而是使用 recursive-function-definition 工具而不是隐式编码。然而，在 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))
（当z < 0计算zI时，你可能需要小心计算，但思路是一样的。）
请注意，编码简单并不意味着 z3 总能成功回答查询。由于 Real 和 Integer 的混合，如前所述，问题仍然无法确定。如果您对 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 片段的情况：求解器通常可能会放弃，但它采用的启发式算法可能会解决具有实际意义的问题。
有理数限制
除了理论之外，事实证明，如果您只使用有理数（而不是实际的实数），那么您确实可以编写 first-order 公式来识别整数。编码不适合胆小的人，但是：http://math.mit.edu/~poonen/papers/ae.pdf。此外，由于编码涉及量词，SMT 求解器不太可能很好地处理基于此想法的公式。
[顺便感谢一下我的同事们；这个问题引发了一场精彩的 lunch-time 对话！]
使用 smtlib 我想使用 QF_UFNRA 制作类似 modulo 的东西。这使我无法使用 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 吗？
这是一个很好的问题。不幸的是，如果您将自己限制在 QF_UFNRA.
如果你能编码这样的功能，那么你就可以决定任意的丢番图方程。您只需将给定的丢番图方程投射到实数上，使用这种所谓的方法计算实数解的 "fraction"，并断言分数为 0。由于实数是可判定的，这将为您提供丢番图方程的判定程序，从而完成不可能的事情。 （这被称为希尔伯特第十问题。）
因此，尽管任务看起来很简单，但实际上是无法完成的。但这并不意味着你不能用一些扩展来编码它，并且可能让求解器成功地决定它的实例。
如果允许量词和递归函数
如果你允许自己使用量词和recursive-functions，那么你可以这样写：
(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 手册。）这实际上是您尝试在问题中编码的内容，而是使用 recursive-function-definition 工具而不是隐式编码。然而，在 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))
（当z < 0计算zI时，你可能需要小心计算，但思路是一样的。）
请注意，编码简单并不意味着 z3 总能成功回答查询。由于 Real 和 Integer 的混合，如前所述，问题仍然无法确定。如果您对 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 片段的情况：求解器通常可能会放弃，但它采用的启发式算法可能会解决具有实际意义的问题。
有理数限制
除了理论之外，事实证明，如果您只使用有理数（而不是实际的实数），那么您确实可以编写 first-order 公式来识别整数。编码不适合胆小的人，但是：http://math.mit.edu/~poonen/papers/ae.pdf。此外，由于编码涉及量词，SMT 求解器不太可能很好地处理基于此想法的公式。
[顺便感谢一下我的同事们；这个问题引发了一场精彩的 lunch-time 对话！]