haskell - 如何在 SBV 中获得符号平方根和对数函数？

Question

我能找到的唯一解决方案是做一个平方根近似，但这并不象征性地起作用，所以我不能用它来证明。

score 3 · Accepted Answer

SBV 已经支持浮点类型的平方根：

单精度：

Prelude Data.SBV> sat $ \x -> x .== fpSqrt sRNE (4.2::SFloat)
Satisfiable. Model:
  s0 = 2.04939 :: Float

双精度：

Prelude Data.SBV> sat $ \x -> x .== fpSqrt sRNE (4.2::SDouble)
Satisfiable. Model:
  s0 = 2.04939015319192 :: Double

请注意，您需要提供一个舍入模式，在上面我使用sRNE的代表round-nearest-towards-even是 Haskell 中使用的默认舍入模式。如果需要，SBV 支持所有 5 种 IEEE 舍入模式。

您还可以使用 reals（任意精度代数实数）：

Prelude Data.SBV> sat $ \x -> x * x .==  (4.2::SReal)
Satisfiable. Model:
  s0 = root(1, 5x^2 = 21) = -2.0493901531919196... :: Real

在这种情况下，您会得到一个代数方程和实际结果的近似值。（注意上面x*x == 4.2与相同5*x^2 = 21）。这两种形式都可以从程序化 API 获得。

整数平方根没有单一的函数。也不是对数。后者可以使用量词来表示，但 SMT 求解器不太可能为它们产生好的结果，因为它们将涉及非线性算术和量化。

通常请注意，SBV 和 SMT 求解器都不适用于“简化”符号表达式。您将始终得到查询的具体答案：如果您要求sqrt 50，您将得到7.07106（以正确的类型/精度），而不是诸如之类的东西5 * sqrt 2。

1 回答 1