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

Question

The only solution I can find is to do a square root approximation, but this doesn't work symbolically so I can't use it for proving.

Answer 1

SBV already supports square-root for the floating-point types:

Single precision:

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

Double precision:

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

Note that you need to provide a rounding-mode, in the above I used sRNE which stands for round-nearest-towards-even which is the default rounding-mode used in Haskell. SBV supports all 5 IEEE rounding modes, if needed.

You can also use reals (arbitrary-precision algebraic real numbers):

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

In this case, you get an algebraic equation, and an approximation of the real-result. (Note in the above that x*x == 4.2 is the same as 5*x^2 = 21). Both forms are available from the programmatic API.

There's no single function for integer-square-roots; nor for logarithms. These latter ones can be expressed using quantifiers, but SMT solvers are unlikely to produce good results for them since they will involve both non-linear arithmetic and quantification.

Note in general that neither SBV nor SMT solvers are good for "simplifying" symbolic expressions. You will always get a concrete answer for your query: If you ask for sqrt 50, you will get 7.07106 (in the correct type/precision), instead of things like 5 * sqrt 2, for instance.