Unsupported argument root when using AlgReal

[arrowd]

As a result of solving my problem I get an AlgReal, which, being printed, looks like

root(2, 2535301200456458802993406410752x^2 = 3342936855254052832178637801831666727317)

However, when trying to convert it to Double with fromRational . toRational, I get:

SBV.algRealToHaskell: Unsupported argument: root(2, 2535301200456458802993406410752x^2 = 3342936855254052832178637801831666727317)
CallStack (from HasCallStack):
  error, called at ./Data/SBV/Core/AlgReals.hs:190:41 in sbv-8.6-4S9z5R1TCJr59anjkda4w3:Data.SBV.Core.AlgReals

What does that error mean?

[LeventErkok]

A root object represents a real number that is not a rational. (For instance square-root of 2.) There is no underlying type in Haskell that can represent such a number. So, when SBV gets a model over Real's, it carefully tracks whether it is rational (i.e., one that can be converted using toRational) or one that cannot. In this case, you're getting an example that cannot be represented as a Rational Haskell value.

The error message can be improved though, and I just pushed a commit that improves it. If you try it now, it should say something like:

SBV.algRealToHaskell: Unsupported argument:

   root(1, x^2 = 2) = -1.414213562373095...

represents an irrational number, and cannot be converted to a Haskell value.

CallStack (from HasCallStack):
  error, called at /Users/leventerkok/Projects/sbv/Data/SBV/Core/AlgReals.hs:190:41 in main:Data.SBV.Core.AlgReals

Hopefully, that's a lot easier to read.

If you want to get an "approximate" value, you can do:

Prelude Data.SBV Data.SBV.Internals> Just x <- (extractModel `fmap` (sat $ \(x::SReal) -> x*x .== 2)) :: IO (Maybe AlgReal)
Prelude Data.SBV Data.SBV.Internals> AlgPolyRoot _ (Just approx) = x
Prelude Data.SBV Data.SBV.Internals> approx
"-1.414213562373095..."

(Don't forget to import Data.SBV.Internals. Note that in this case SBV adds the ... at the end to indicate this is an approximate representation. You can now take this string and turn it into some other kind of number if you want:

Prelude Data.SBV Data.SBV.Internals> read (reverse . drop 3 . reverse $ approx) :: Double
-1.414213562373095

but obviously now you're just getting an approximation as a Double in this case.

[arrowd]

Why not add a public function to get an approximation for AlgReal? Getting it by reading some internal value is a bit clunky. Or there is no binary representation of approximated value in first place?

[LeventErkok]

Sure. Added in commit: https://github.com/LeventErkok/sbv/commit/7152849ba150de23a537c075d9825f580c413982

From the commit message:

Add function 'algRealToRational' that can convert an algebraic-real to a Haskell rational. We get an either value: If the algebraic real is exact, then it returns a 'Left' value that represents the value precisely. Otherwise, it returns a 'Right' value, which is only an approximation. Note: Setting 'printRealPrec' in SMTConfig to a higher value will increase the precision at the cost of more computation by the SMT solver.

You get a Left value if the rational is exact, or a Right value if it is approximate. Compare:

Prelude Data.SBV> Just x <- (extractModel `fmap` (sat $ \(x::SReal) -> x*x .== 2)) :: IO (Maybe AlgReal)
Prelude Data.SBV> algRealToRational x
Right ((-282842712474619) % 200000000000000)

to:

Prelude Data.SBV> Just x <- (extractModel `fmap` (sat $ \(x::SReal) -> x*x .== 4)) :: IO (Maybe AlgReal)
Prelude Data.SBV> algRealToRational x
Left (2 % 1)

You can increase the "precision" by using:

satWith z3{printRealPrec = 20} ...

the higher the number, the more precise the approximation will be.

Does this help?

[arrowd]

Looks awesome, thanks! Will try this out as soon as I remember how to reference packages at the given commit in Stack.

[arrowd]

Unfortunately, I still get an error, which means that my value cannot be approximated. Do I have any options?

[arrowd]

By the way, using yices instead of z3 yields following error:

***    Sent      : (assert s18)
***    Expected  : success
***    Received  : (error "non-linear arithmetic is not allowed in logic ALL")

Not sure if it is another bug in SBV. Do I have to call setLogic myself?

[LeventErkok]

Irrational roots are only supported by z3.

Regarding the error you're getting; can you post a minimal repro? It should not happen with z3.

[arrowd]

Here it is: https://arrowd.name/emishield.zip

Let me know if it is still big and you want me to reduce it further.

[LeventErkok]

This is a problem with SBV. I'll push in a fix shortly.

[LeventErkok]

@arrowd Give the latest commit a try. I think it should work fine now.

[arrowd]

Yep, it is. Thank you for your support.