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

Question

我能找到的唯一解决方案是求平方根近似值，但这在符号上不起作用，所以我不能用它来证明。

Answer 1

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 舍入模式。

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

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 求解器都不适合 "simplifying" 符号表达式。您将始终为您的查询得到一个具体的答案：如果您要求 sqrt 50，您将得到 7.07106（正确的 type/precision），而不是 5 * sqrt 2，例如。

How do I get symbolic square root and logarithm functions in SBV?