Very imprecise sqrt computation for rational numbers

[tquatmann]

As observed in #868, carl::sqrt might be very imprecise.
For example, I get sqrt(2)=3/2 in [1, 2] when executing

    std::cout << "sqrt(2)="
                    << carl::sqrt(GmpRationalNumber(2))
                    << " in [" << carl::sqrt_safe(GmpRationalNumber(2)).first << ", "  << carl::sqrt_safe(GmpRationalNumber(2)).second << "]\n";

I believe the carl implementation is optimised towards efficiency and not blowing up the number representation. However, I believe within the Storm context, its reasonable to require that

• carl::sqrt(GmpRationalNumber ..) is always at least as precise as std::sqrt(double ...)
• if the square root of the given number is rational, carl::sqrt(...) yields the exact result.

As far as I did the math, the current implementation (which relies on sqrt_safe satisfies the second requirement, but obviously not the former.

I propose a simple solution that computes the square root using carl::sqrt_safe(..). If that is not exact, we try a conversion to double and (if possible) use those results to improve the bounds of sqrt_safe.

Any opinion on whether such a solution should be integrated in carl-srotm or storm?

[volkm]

I would lean towards implementing this solution in carl, because all other parts are located there anyways.
I like the fallback solution via double, maybe we can also try to use a higher precision for sqrt_safe in the first place.

By the way, is the issue only for Gmp or also for Cln?