-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Core.AlgReals
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Algebraic reals in Haskell.
-----------------------------------------------------------------------------

{-# LANGUAGE FlexibleInstances #-}

{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

module Data.SBV.Core.AlgReals (
             AlgReal(..)
           , AlgRealPoly(..)
           , RationalCV(..)
           , RealPoint(..), realPoint
           , mkPolyReal
           , algRealToSMTLib2
           , algRealToHaskell
           , algRealToRational
           , mergeAlgReals
           , isExactRational
           , algRealStructuralEqual
           , algRealStructuralCompare
           )
   where

import Data.Char       (isDigit)

import Data.List       (sortBy, isPrefixOf, partition)
import Data.Ratio      ((%), numerator, denominator)
import Data.Function   (on)
import System.Random
import Test.QuickCheck (Arbitrary(..))

import Numeric (readSigned, readFloat)

import Text.Read(readMaybe)

-- | Is the endpoint included in the interval?
data RealPoint a = OpenPoint   a -- ^ open: i.e., doesn't include the point
                 | ClosedPoint a -- ^ closed: i.e., includes the point
                 deriving (Int -> RealPoint a -> ShowS
forall a. Show a => Int -> RealPoint a -> ShowS
forall a. Show a => [RealPoint a] -> ShowS
forall a. Show a => RealPoint a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RealPoint a] -> ShowS
$cshowList :: forall a. Show a => [RealPoint a] -> ShowS
show :: RealPoint a -> String
$cshow :: forall a. Show a => RealPoint a -> String
showsPrec :: Int -> RealPoint a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> RealPoint a -> ShowS
Show, RealPoint a -> RealPoint a -> Bool
forall a. Eq a => RealPoint a -> RealPoint a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RealPoint a -> RealPoint a -> Bool
$c/= :: forall a. Eq a => RealPoint a -> RealPoint a -> Bool
== :: RealPoint a -> RealPoint a -> Bool
$c== :: forall a. Eq a => RealPoint a -> RealPoint a -> Bool
Eq, RealPoint a -> RealPoint a -> Bool
RealPoint a -> RealPoint a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (RealPoint a)
forall a. Ord a => RealPoint a -> RealPoint a -> Bool
forall a. Ord a => RealPoint a -> RealPoint a -> Ordering
forall a. Ord a => RealPoint a -> RealPoint a -> RealPoint a
min :: RealPoint a -> RealPoint a -> RealPoint a
$cmin :: forall a. Ord a => RealPoint a -> RealPoint a -> RealPoint a
max :: RealPoint a -> RealPoint a -> RealPoint a
$cmax :: forall a. Ord a => RealPoint a -> RealPoint a -> RealPoint a
>= :: RealPoint a -> RealPoint a -> Bool
$c>= :: forall a. Ord a => RealPoint a -> RealPoint a -> Bool
> :: RealPoint a -> RealPoint a -> Bool
$c> :: forall a. Ord a => RealPoint a -> RealPoint a -> Bool
<= :: RealPoint a -> RealPoint a -> Bool
$c<= :: forall a. Ord a => RealPoint a -> RealPoint a -> Bool
< :: RealPoint a -> RealPoint a -> Bool
$c< :: forall a. Ord a => RealPoint a -> RealPoint a -> Bool
compare :: RealPoint a -> RealPoint a -> Ordering
$ccompare :: forall a. Ord a => RealPoint a -> RealPoint a -> Ordering
Ord)

-- | Extract the point associated with the open-closed point
realPoint :: RealPoint a -> a
realPoint :: forall a. RealPoint a -> a
realPoint (OpenPoint   a
a) = a
a
realPoint (ClosedPoint a
a) = a
a

-- | Algebraic reals. Note that the representation is left abstract. We represent
-- rational results explicitly, while the roots-of-polynomials are represented
-- implicitly by their defining equation
data AlgReal = AlgRational Bool Rational                             -- ^ bool says it's exact (i.e., SMT-solver did not return it with ? at the end.)
             | AlgPolyRoot (Integer,  AlgRealPoly) (Maybe String)    -- ^ which root of this polynomial and an approximate decimal representation with given precision, if available
             | AlgInterval (RealPoint Rational) (RealPoint Rational) -- ^ interval, with low and high bounds

-- | Check whether a given argument is an exact rational
isExactRational :: AlgReal -> Bool
isExactRational :: AlgReal -> Bool
isExactRational (AlgRational Bool
True Rational
_) = Bool
True
isExactRational AlgReal
_                    = Bool
False

-- | A univariate polynomial, represented simply as a
-- coefficient list. For instance, "5x^3 + 2x - 5" is
-- represented as [(5, 3), (2, 1), (-5, 0)]
newtype AlgRealPoly = AlgRealPoly [(Integer, Integer)]
                   deriving (AlgRealPoly -> AlgRealPoly -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AlgRealPoly -> AlgRealPoly -> Bool
$c/= :: AlgRealPoly -> AlgRealPoly -> Bool
== :: AlgRealPoly -> AlgRealPoly -> Bool
$c== :: AlgRealPoly -> AlgRealPoly -> Bool
Eq, Eq AlgRealPoly
AlgRealPoly -> AlgRealPoly -> Bool
AlgRealPoly -> AlgRealPoly -> Ordering
AlgRealPoly -> AlgRealPoly -> AlgRealPoly
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
$cmin :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
max :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
$cmax :: AlgRealPoly -> AlgRealPoly -> AlgRealPoly
>= :: AlgRealPoly -> AlgRealPoly -> Bool
$c>= :: AlgRealPoly -> AlgRealPoly -> Bool
> :: AlgRealPoly -> AlgRealPoly -> Bool
$c> :: AlgRealPoly -> AlgRealPoly -> Bool
<= :: AlgRealPoly -> AlgRealPoly -> Bool
$c<= :: AlgRealPoly -> AlgRealPoly -> Bool
< :: AlgRealPoly -> AlgRealPoly -> Bool
$c< :: AlgRealPoly -> AlgRealPoly -> Bool
compare :: AlgRealPoly -> AlgRealPoly -> Ordering
$ccompare :: AlgRealPoly -> AlgRealPoly -> Ordering
Ord)

-- | Construct a poly-root real with a given approximate value (either as a decimal, or polynomial-root)
mkPolyReal :: Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal :: Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal (Left (Bool
exact, String
str))
 = case (String
str, forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall a. Eq a => a -> a -> Bool
== Char
'.') String
str) of
      (String
"", (String, String)
_)                                -> Bool -> Rational -> AlgReal
AlgRational Bool
exact Rational
0
      (String
_, (String
x, Char
'.':String
y)) | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit (String
x forall a. [a] -> [a] -> [a]
++ String
y) -> Bool -> Rational -> AlgReal
AlgRational Bool
exact (forall a. Read a => String -> a
read (String
xforall a. [a] -> [a] -> [a]
++String
y) forall a. Integral a => a -> a -> Ratio a
% (Integer
10 forall a b. (Num a, Integral b) => a -> b -> a
^ forall (t :: * -> *) a. Foldable t => t a -> Int
length String
y))
      (String
_, (String
x, String
""))    | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
x        -> Bool -> Rational -> AlgReal
AlgRational Bool
exact (forall a. Read a => String -> a
read String
x forall a. Integral a => a -> a -> Ratio a
% Integer
1)
      (String, (String, String))
_                                      ->
        -- CVC5 prints in division-rational form:
        case forall a. Read a => String -> Maybe a
readMaybe (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Char
',') (forall a b. (a -> b) -> [a] -> [b]
map (\Char
c -> if Char
c forall a. Eq a => a -> a -> Bool
== Char
'/' then Char
'%' else Char
c) String
str)) :: Maybe Rational of
          Just Rational
r  -> Bool -> Rational -> AlgReal
AlgRational Bool
exact Rational
r
          Maybe Rational
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"*** Data.SBV.mkPolyReal: Unable to read a number from:"
                                     , String
"***"
                                     , String
"*** " forall a. [a] -> [a] -> [a]
++ String
str
                                     , String
"***"
                                     , String
"*** Please report this as a bug."
                                     ]
mkPolyReal (Right (Integer
k, [(Integer, Integer)]
coeffs))
 = (Integer, AlgRealPoly) -> Maybe String -> AlgReal
AlgPolyRoot (Integer
k, [(Integer, Integer)] -> AlgRealPoly
AlgRealPoly ([(Integer, Integer)] -> [(Integer, Integer)]
normalize [(Integer, Integer)]
coeffs)) forall a. Maybe a
Nothing
 where normalize :: [(Integer, Integer)] -> [(Integer, Integer)]
       normalize :: [(Integer, Integer)] -> [(Integer, Integer)]
normalize = forall {b} {a}. (Eq b, Num a) => [(a, b)] -> [(a, b)]
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> b
snd)
       merge :: [(a, b)] -> [(a, b)]
merge []                     = []
       merge [(a, b)
x]                    = [(a, b)
x]
       merge ((a
a, b
b):r :: [(a, b)]
r@((a
c, b
d):[(a, b)]
xs))
         | b
b forall a. Eq a => a -> a -> Bool
== b
d                   = [(a, b)] -> [(a, b)]
merge ((a
aforall a. Num a => a -> a -> a
+a
c, b
b)forall a. a -> [a] -> [a]
:[(a, b)]
xs)
         | Bool
True                     = (a
a, b
b) forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)]
merge [(a, b)]
r

instance Show AlgRealPoly where
  show :: AlgRealPoly -> String
show (AlgRealPoly [(Integer, Integer)]
xs) = ShowS
chkEmpty ([String] -> String
join (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [forall {a} {a}.
(Eq a, Eq a, Num a, Num a, Show a, Show a) =>
(a, a) -> [String]
term (Integer, Integer)
p | p :: (Integer, Integer)
p@(Integer
_, Integer
x) <- [(Integer, Integer)]
xs, Integer
x forall a. Eq a => a -> a -> Bool
/= Integer
0])) forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
c
     where c :: Integer
c  = -Integer
1 forall a. Num a => a -> a -> a
* forall a. [a] -> a
head ([Integer
k | (Integer
k, Integer
0) <- [(Integer, Integer)]
xs] forall a. [a] -> [a] -> [a]
++ [Integer
0])
           term :: (a, a) -> [String]
term ( a
0, a
_) = []
           term ( a
1, a
1) = [ String
"x"]
           term ( a
1, a
p) = [ String
"x^" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
p]
           term (-1, a
1) = [String
"-x"]
           term (-1, a
p) = [String
"-x^" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
p]
           term (a
k,  a
1) = [forall a. Show a => a -> String
show a
k forall a. [a] -> [a] -> [a]
++ String
"x"]
           term (a
k,  a
p) = [forall a. Show a => a -> String
show a
k forall a. [a] -> [a] -> [a]
++ String
"x^" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
p]
           join :: [String] -> String
join []      = String
""
           join (String
k:[String]
ks) = String
k forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ [String] -> String
join [String]
ks
             where s :: String
s = case [String]
ks of
                        []    -> String
""
                        (String
y:[String]
_) | String
"-" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
y -> String
""
                              | String
"+" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
y -> String
""
                              | Bool
True               -> String
"+"
           chkEmpty :: ShowS
chkEmpty String
s = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s then String
"0" else String
s

instance Show AlgReal where
  show :: AlgReal -> String
show (AlgRational Bool
exact Rational
a)         = Bool -> Rational -> String
showRat Bool
exact Rational
a
  show (AlgPolyRoot (Integer
i, AlgRealPoly
p) Maybe String
mbApprox) = String
"root(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
i forall a. [a] -> [a] -> [a]
++ String
", " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AlgRealPoly
p forall a. [a] -> [a] -> [a]
++ String
")" forall a. [a] -> [a] -> [a]
++ forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" ShowS
app Maybe String
mbApprox
     where app :: ShowS
app String
v | forall a. [a] -> a
last String
v forall a. Eq a => a -> a -> Bool
== Char
'?' = String
" = " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [a]
init String
v forall a. [a] -> [a] -> [a]
++ String
"..."
                 | Bool
True          = String
" = " forall a. [a] -> [a] -> [a]
++ String
v
  show (AlgInterval RealPoint Rational
a RealPoint Rational
b)         = case (RealPoint Rational
a, RealPoint Rational
b) of
                                     (OpenPoint   Rational
l, OpenPoint   Rational
h) -> String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rational
l forall a. [a] -> [a] -> [a]
++ String
", " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rational
h forall a. [a] -> [a] -> [a]
++ String
")"
                                     (OpenPoint   Rational
l, ClosedPoint Rational
h) -> String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rational
l forall a. [a] -> [a] -> [a]
++ String
", " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rational
h forall a. [a] -> [a] -> [a]
++ String
"]"
                                     (ClosedPoint Rational
l, OpenPoint   Rational
h) -> String
"[" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rational
l forall a. [a] -> [a] -> [a]
++ String
", " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rational
h forall a. [a] -> [a] -> [a]
++ String
")"
                                     (ClosedPoint Rational
l, ClosedPoint Rational
h) -> String
"[" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rational
l forall a. [a] -> [a] -> [a]
++ String
", " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rational
h forall a. [a] -> [a] -> [a]
++ String
"]"

-- lift unary op through an exact rational, otherwise bail
lift1 :: String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 :: String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 String
_  Rational -> Rational
o (AlgRational Bool
e Rational
a) = Bool -> Rational -> AlgReal
AlgRational Bool
e (Rational -> Rational
o Rational
a)
lift1 String
nm Rational -> Rational
_ AlgReal
a                 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"AlgReal." forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
": unsupported argument: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AlgReal
a

-- lift binary op through exact rationals, otherwise bail
lift2 :: String -> (Rational -> Rational -> Rational) -> AlgReal -> AlgReal -> AlgReal
lift2 :: String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 String
_  Rational -> Rational -> Rational
o (AlgRational Bool
True Rational
a) (AlgRational Bool
True Rational
b) = Bool -> Rational -> AlgReal
AlgRational Bool
True (Rational
a Rational -> Rational -> Rational
`o` Rational
b)
lift2 String
nm Rational -> Rational -> Rational
_ AlgReal
a                    AlgReal
b                    = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"AlgReal." forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
": unsupported arguments: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (AlgReal
a, AlgReal
b)

-- The idea in the instances below is that we will fully support operations
-- on "AlgRational" AlgReals, but leave everything else undefined. When we are
-- on the Haskell side, the AlgReal's are *not* reachable. They only represent
-- return values from SMT solvers, which we should *not* need to manipulate.
instance Eq AlgReal where
  AlgRational Bool
True Rational
a == :: AlgReal -> AlgReal -> Bool
== AlgRational Bool
True Rational
b = Rational
a forall a. Eq a => a -> a -> Bool
== Rational
b
  AlgReal
a                  == AlgReal
b                  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"AlgReal.==: unsupported arguments: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (AlgReal
a, AlgReal
b)

instance Ord AlgReal where
  AlgRational Bool
True Rational
a compare :: AlgReal -> AlgReal -> Ordering
`compare` AlgRational Bool
True Rational
b = Rational
a forall a. Ord a => a -> a -> Ordering
`compare` Rational
b
  AlgReal
a                  `compare` AlgReal
b                  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"AlgReal.compare: unsupported arguments: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (AlgReal
a, AlgReal
b)

-- | Structural equality for AlgReal; used when constants are Map keys
algRealStructuralEqual   :: AlgReal -> AlgReal -> Bool
AlgRational Bool
a Rational
b algRealStructuralEqual :: AlgReal -> AlgReal -> Bool
`algRealStructuralEqual` AlgRational Bool
c Rational
d = (Bool
a, Rational
b) forall a. Eq a => a -> a -> Bool
== (Bool
c, Rational
d)
AlgPolyRoot (Integer, AlgRealPoly)
a Maybe String
b `algRealStructuralEqual` AlgPolyRoot (Integer, AlgRealPoly)
c Maybe String
d = ((Integer, AlgRealPoly)
a, Maybe String
b) forall a. Eq a => a -> a -> Bool
== ((Integer, AlgRealPoly)
c, Maybe String
d)
AlgReal
_               `algRealStructuralEqual` AlgReal
_               = Bool
False

-- | Structural comparisons for AlgReal; used when constants are Map keys
algRealStructuralCompare :: AlgReal -> AlgReal -> Ordering
AlgRational Bool
a Rational
b algRealStructuralCompare :: AlgReal -> AlgReal -> Ordering
`algRealStructuralCompare` AlgRational Bool
c Rational
d = (Bool
a, Rational
b) forall a. Ord a => a -> a -> Ordering
`compare` (Bool
c, Rational
d)
AlgRational Bool
_ Rational
_ `algRealStructuralCompare` AlgPolyRoot (Integer, AlgRealPoly)
_ Maybe String
_ = Ordering
LT
AlgRational Bool
_ Rational
_ `algRealStructuralCompare` AlgInterval RealPoint Rational
_ RealPoint Rational
_ = Ordering
LT
AlgPolyRoot (Integer, AlgRealPoly)
_ Maybe String
_ `algRealStructuralCompare` AlgRational Bool
_ Rational
_ = Ordering
GT
AlgPolyRoot (Integer, AlgRealPoly)
a Maybe String
b `algRealStructuralCompare` AlgPolyRoot (Integer, AlgRealPoly)
c Maybe String
d = ((Integer, AlgRealPoly)
a, Maybe String
b) forall a. Ord a => a -> a -> Ordering
`compare` ((Integer, AlgRealPoly)
c, Maybe String
d)
AlgPolyRoot (Integer, AlgRealPoly)
_ Maybe String
_ `algRealStructuralCompare` AlgInterval RealPoint Rational
_ RealPoint Rational
_ = Ordering
LT
AlgInterval RealPoint Rational
_ RealPoint Rational
_ `algRealStructuralCompare` AlgRational Bool
_ Rational
_ = Ordering
GT
AlgInterval RealPoint Rational
_ RealPoint Rational
_ `algRealStructuralCompare` AlgPolyRoot (Integer, AlgRealPoly)
_ Maybe String
_ = Ordering
GT
AlgInterval RealPoint Rational
a RealPoint Rational
b `algRealStructuralCompare` AlgInterval RealPoint Rational
c RealPoint Rational
d = (RealPoint Rational
a, RealPoint Rational
b) forall a. Ord a => a -> a -> Ordering
`compare` (RealPoint Rational
c, RealPoint Rational
d)

instance Num AlgReal where
  + :: AlgReal -> AlgReal -> AlgReal
(+)         = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 String
"+"      forall a. Num a => a -> a -> a
(+)
  * :: AlgReal -> AlgReal -> AlgReal
(*)         = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 String
"*"      forall a. Num a => a -> a -> a
(*)
  (-)         = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 String
"-"      (-)
  negate :: AlgReal -> AlgReal
negate      = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 String
"negate" forall a. Num a => a -> a
negate
  abs :: AlgReal -> AlgReal
abs         = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 String
"abs"    forall a. Num a => a -> a
abs
  signum :: AlgReal -> AlgReal
signum      = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 String
"signum" forall a. Num a => a -> a
signum
  fromInteger :: Integer -> AlgReal
fromInteger = Bool -> Rational -> AlgReal
AlgRational Bool
True forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger

-- |  NB: Following the other types we have, we require `a/0` to be `0` for all a.
instance Fractional AlgReal where
  (AlgRational Bool
True Rational
_) / :: AlgReal -> AlgReal -> AlgReal
/ (AlgRational Bool
True Rational
b) | Rational
b forall a. Eq a => a -> a -> Bool
== Rational
0 = AlgReal
0
  AlgReal
a                    / AlgReal
b                             = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 String
"/" forall a. Fractional a => a -> a -> a
(/) AlgReal
a AlgReal
b
  fromRational :: Rational -> AlgReal
fromRational = Bool -> Rational -> AlgReal
AlgRational Bool
True

instance Real AlgReal where
  toRational :: AlgReal -> Rational
toRational (AlgRational Bool
True Rational
v) = Rational
v
  toRational AlgReal
x                    = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"AlgReal.toRational: Argument cannot be represented as a rational value: " forall a. [a] -> [a] -> [a]
++ AlgReal -> String
algRealToHaskell AlgReal
x

instance Random Rational where
  random :: forall g. RandomGen g => g -> (Rational, g)
random g
g = (Integer
a forall a. Integral a => a -> a -> Ratio a
% Integer
b', g
g'')
     where (Integer
a, g
g')  = forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
           (Integer
b, g
g'') = forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g'
           b' :: Integer
b'       = if Integer
0 forall a. Ord a => a -> a -> Bool
< Integer
b then Integer
b else Integer
1 forall a. Num a => a -> a -> a
- Integer
b -- ensures 0 < b

  randomR :: forall g. RandomGen g => (Rational, Rational) -> g -> (Rational, g)
randomR (Rational
l, Rational
h) g
g = (Rational
r forall a. Num a => a -> a -> a
* Rational
d forall a. Num a => a -> a -> a
+ Rational
l, g
g'')
     where (Integer
b, g
g')  = forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g
           b' :: Integer
b'       = if Integer
0 forall a. Ord a => a -> a -> Bool
< Integer
b then Integer
b else Integer
1 forall a. Num a => a -> a -> a
- Integer
b -- ensures 0 < b
           (Integer
a, g
g'') = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Integer
0, Integer
b') g
g'

           r :: Rational
r = Integer
a forall a. Integral a => a -> a -> Ratio a
% Integer
b'
           d :: Rational
d = Rational
h forall a. Num a => a -> a -> a
- Rational
l

instance Random AlgReal where
  random :: forall g. RandomGen g => g -> (AlgReal, g)
random g
g = let (Rational
a, g
g') = forall a g. (Random a, RandomGen g) => g -> (a, g)
random g
g in (Bool -> Rational -> AlgReal
AlgRational Bool
True Rational
a, g
g')
  randomR :: forall g. RandomGen g => (AlgReal, AlgReal) -> g -> (AlgReal, g)
randomR (AlgRational Bool
True Rational
l, AlgRational Bool
True Rational
h) g
g = let (Rational
a, g
g') = forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Rational
l, Rational
h) g
g in (Bool -> Rational -> AlgReal
AlgRational Bool
True Rational
a, g
g')
  randomR (AlgReal, AlgReal)
lh                                       g
_ = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"AlgReal.randomR: unsupported bounds: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (AlgReal, AlgReal)
lh

-- | Render an 'AlgReal' as an SMTLib2 value. Only supports rationals for the time being.
algRealToSMTLib2 :: AlgReal -> String
algRealToSMTLib2 :: AlgReal -> String
algRealToSMTLib2 (AlgRational Bool
True Rational
r)
   | Integer
m forall a. Eq a => a -> a -> Bool
== Integer
0 = String
"0.0"
   | Integer
m forall a. Ord a => a -> a -> Bool
< Integer
0  = String
"(- (/ "  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Num a => a -> a
abs Integer
m) forall a. [a] -> [a] -> [a]
++ String
".0 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n forall a. [a] -> [a] -> [a]
++ String
".0))"
   | Bool
True   =    String
"(/ "  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
m       forall a. [a] -> [a] -> [a]
++ String
".0 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n forall a. [a] -> [a] -> [a]
++ String
".0)"
  where (Integer
m, Integer
n) = (forall a. Ratio a -> a
numerator Rational
r, forall a. Ratio a -> a
denominator Rational
r)
algRealToSMTLib2 r :: AlgReal
r@(AlgRational Bool
False Rational
_)
   = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV: Unexpected inexact rational to be converted to SMTLib2: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AlgReal
r
algRealToSMTLib2 (AlgPolyRoot (Integer
i, AlgRealPoly [(Integer, Integer)]
xs) Maybe String
_) = String
"(root-obj (+ " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a} {a}.
(Eq a, Num a, Num a, Ord a, Show a, Show a) =>
(a, a) -> [String]
term [(Integer, Integer)]
xs) forall a. [a] -> [a] -> [a]
++ String
") " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
i forall a. [a] -> [a] -> [a]
++ String
")"
  where term :: (a, a) -> [String]
term (a
0, a
_) = []
        term (a
k, a
0) = [forall {a}. (Ord a, Num a, Show a) => a -> String
coeff a
k]
        term (a
1, a
1) = [String
"x"]
        term (a
1, a
p) = [String
"(^ x " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
p forall a. [a] -> [a] -> [a]
++ String
")"]
        term (a
k, a
1) = [String
"(* " forall a. [a] -> [a] -> [a]
++ forall {a}. (Ord a, Num a, Show a) => a -> String
coeff a
k forall a. [a] -> [a] -> [a]
++ String
" x)"]
        term (a
k, a
p) = [String
"(* " forall a. [a] -> [a] -> [a]
++ forall {a}. (Ord a, Num a, Show a) => a -> String
coeff a
k forall a. [a] -> [a] -> [a]
++ String
" (^ x " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
p forall a. [a] -> [a] -> [a]
++ String
"))"]
        coeff :: a -> String
coeff a
n | a
n forall a. Ord a => a -> a -> Bool
< a
0 = String
"(- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Num a => a -> a
abs a
n) forall a. [a] -> [a] -> [a]
++ String
")"
                | Bool
True  = forall a. Show a => a -> String
show a
n
algRealToSMTLib2 r :: AlgReal
r@AlgInterval{}
   = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV: Unexpected inexact rational to be converted to SMTLib2: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AlgReal
r

-- | Render an 'AlgReal' as a Haskell value. Only supports rationals, since there is no corresponding
-- standard Haskell type that can represent root-of-polynomial variety.
algRealToHaskell :: AlgReal -> String
algRealToHaskell :: AlgReal -> String
algRealToHaskell (AlgRational Bool
True Rational
r) = String
"((" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rational
r forall a. [a] -> [a] -> [a]
++ String
") :: Rational)"
algRealToHaskell AlgReal
r                    = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                        , String
"SBV.algRealToHaskell: Unsupported argument:"
                                                        , String
""
                                                        , String
"   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AlgReal
r
                                                        , String
""
                                                        , String
"represents an irrational number, and cannot be converted to a Haskell value."
                                                        ]

-- | Conversion from internal rationals to Haskell values
data RationalCV = RatIrreducible AlgReal                                   -- ^ Root of a polynomial, cannot be reduced
                | RatExact       Rational                                  -- ^ An exact rational
                | RatApprox      Rational                                  -- ^ An approximated value
                | RatInterval    (RealPoint Rational) (RealPoint Rational) -- ^ Interval. Can be open/closed on both ends.
                deriving Int -> RationalCV -> ShowS
[RationalCV] -> ShowS
RationalCV -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RationalCV] -> ShowS
$cshowList :: [RationalCV] -> ShowS
show :: RationalCV -> String
$cshow :: RationalCV -> String
showsPrec :: Int -> RationalCV -> ShowS
$cshowsPrec :: Int -> RationalCV -> ShowS
Show

-- | Convert an 'AlgReal' to a 'Rational'. If the 'AlgReal' is exact, then you get a 'Left' value. Otherwise,
-- you get a 'Right' value which is simply an approximation.
algRealToRational :: AlgReal -> RationalCV
algRealToRational :: AlgReal -> RationalCV
algRealToRational AlgReal
a = case AlgReal
a of
                        AlgRational Bool
True  Rational
r        -> Rational -> RationalCV
RatExact Rational
r
                        AlgRational Bool
False Rational
r        -> Rational -> RationalCV
RatExact Rational
r
                        AlgPolyRoot (Integer, AlgRealPoly)
_     Maybe String
Nothing  -> AlgReal -> RationalCV
RatIrreducible AlgReal
a
                        AlgPolyRoot (Integer, AlgRealPoly)
_     (Just String
s) -> let trimmed :: String
trimmed = case forall a. [a] -> [a]
reverse String
s of
                                                                     Char
'.':Char
'.':Char
'.':String
rest -> forall a. [a] -> [a]
reverse String
rest
                                                                     String
_                -> String
s
                                                      in case forall a. Real a => ReadS a -> ReadS a
readSigned forall a. RealFrac a => ReadS a
readFloat String
trimmed of
                                                           [(Rational
v, String
"")] -> Rational -> RationalCV
RatApprox Rational
v
                                                           [(Rational, String)]
_         -> forall {a}. String -> a
bad String
"represents a value that cannot be converted to a rational"
                        AlgInterval RealPoint Rational
lo RealPoint Rational
hi          -> RealPoint Rational -> RealPoint Rational -> RationalCV
RatInterval RealPoint Rational
lo RealPoint Rational
hi
   where bad :: String -> a
bad String
w = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                 , String
"SBV.algRealToRational: Unsupported argument:"
                                 , String
""
                                 , String
"   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AlgReal
a
                                 , String
""
                                 , String
w
                                 ]

-- Try to show a rational precisely if we can, with finite number of
-- digits. Otherwise, show it as a rational value.
showRat :: Bool -> Rational -> String
showRat :: Bool -> Rational -> String
showRat Bool
exact Rational
r = ShowS
p forall a b. (a -> b) -> a -> b
$ case Integer -> [Integer] -> Maybe (Int, String)
f25 (forall a. Ratio a -> a
denominator Rational
r) [] of
                       Maybe (Int, String)
Nothing               -> forall a. Show a => a -> String
show Rational
r   -- bail out, not precisely representable with finite digits
                       Just (Int
noOfZeros, String
num) -> let present :: Int
present = forall (t :: * -> *) a. Foldable t => t a -> Int
length String
num
                                                in ShowS
neg forall a b. (a -> b) -> a -> b
$ case Int
noOfZeros forall a. Ord a => a -> a -> Ordering
`compare` Int
present of
                                                           Ordering
LT -> let (String
b, String
a) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
present forall a. Num a => a -> a -> a
- Int
noOfZeros) String
num in String
b forall a. [a] -> [a] -> [a]
++ String
"." forall a. [a] -> [a] -> [a]
++ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
a then String
"0" else String
a
                                                           Ordering
EQ -> String
"0." forall a. [a] -> [a] -> [a]
++ String
num
                                                           Ordering
GT -> String
"0." forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (Int
noOfZeros forall a. Num a => a -> a -> a
- Int
present) Char
'0' forall a. [a] -> [a] -> [a]
++ String
num
  where p :: ShowS
p   = if Bool
exact then forall a. a -> a
id else (forall a. [a] -> [a] -> [a]
++ String
"...")
        neg :: ShowS
neg = if Rational
r forall a. Ord a => a -> a -> Bool
< Rational
0 then (Char
'-'forall a. a -> [a] -> [a]
:) else forall a. a -> a
id
        -- factor a number in 2's and 5's if possible
        -- If so, it'll return the number of digits after the zero
        -- to reach the next power of 10, and the numerator value scaled
        -- appropriately and shown as a string
        f25 :: Integer -> [Integer] -> Maybe (Int, String)
        f25 :: Integer -> [Integer] -> Maybe (Int, String)
f25 Integer
1 [Integer]
sofar = let ([Integer]
ts, [Integer]
fs)   = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall a. Eq a => a -> a -> Bool
== Integer
2) [Integer]
sofar
                          lts :: Int
lts        = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Integer]
ts
                          lfs :: Int
lfs        = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Integer]
fs
                          noOfZeros :: Int
noOfZeros  = Int
lts forall a. Ord a => a -> a -> a
`max` Int
lfs
                      in forall a. a -> Maybe a
Just (Int
noOfZeros, forall a. Show a => a -> String
show (forall a. Num a => a -> a
abs (forall a. Ratio a -> a
numerator Rational
r)  forall a. Num a => a -> a -> a
* forall {a} {t} {t}. Num a => [t] -> [t] -> a
factor [Integer]
ts [Integer]
fs))
        f25 Integer
v [Integer]
sofar = let (Integer
q2, Integer
r2) = Integer
v forall a. Integral a => a -> a -> (a, a)
`quotRem` Integer
2
                          (Integer
q5, Integer
r5) = Integer
v forall a. Integral a => a -> a -> (a, a)
`quotRem` Integer
5
                      in case (Integer
r2, Integer
r5) of
                           (Integer
0, Integer
_) -> Integer -> [Integer] -> Maybe (Int, String)
f25 Integer
q2 (Integer
2 forall a. a -> [a] -> [a]
: [Integer]
sofar)
                           (Integer
_, Integer
0) -> Integer -> [Integer] -> Maybe (Int, String)
f25 Integer
q5 (Integer
5 forall a. a -> [a] -> [a]
: [Integer]
sofar)
                           (Integer, Integer)
_      -> forall a. Maybe a
Nothing
        -- compute the next power of 10 we need to get to
        factor :: [t] -> [t] -> a
factor []     [t]
fs     = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [a
2 | t
_ <- [t]
fs]
        factor [t]
ts     []     = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [a
5 | t
_ <- [t]
ts]
        factor (t
_:[t]
ts) (t
_:[t]
fs) = [t] -> [t] -> a
factor [t]
ts [t]
fs

-- | Merge the representation of two algebraic reals, one assumed to be
-- in polynomial form, the other in decimal. Arguments can be the same
-- kind, so long as they are both rationals and equivalent; if not there
-- must be one that is precise. It's an error to pass anything
-- else to this function! (Used in reconstructing SMT counter-example values with reals).
mergeAlgReals :: String -> AlgReal -> AlgReal -> AlgReal
mergeAlgReals :: String -> AlgReal -> AlgReal -> AlgReal
mergeAlgReals String
_ f :: AlgReal
f@(AlgRational Bool
exact Rational
r) (AlgPolyRoot (Integer, AlgRealPoly)
kp Maybe String
Nothing)
  | Bool
exact = AlgReal
f
  | Bool
True  = (Integer, AlgRealPoly) -> Maybe String -> AlgReal
AlgPolyRoot (Integer, AlgRealPoly)
kp (forall a. a -> Maybe a
Just (Bool -> Rational -> String
showRat Bool
False Rational
r))
mergeAlgReals String
_ (AlgPolyRoot (Integer, AlgRealPoly)
kp Maybe String
Nothing) f :: AlgReal
f@(AlgRational Bool
exact Rational
r)
  | Bool
exact = AlgReal
f
  | Bool
True  = (Integer, AlgRealPoly) -> Maybe String -> AlgReal
AlgPolyRoot (Integer, AlgRealPoly)
kp (forall a. a -> Maybe a
Just (Bool -> Rational -> String
showRat Bool
False Rational
r))
mergeAlgReals String
_ f :: AlgReal
f@(AlgRational Bool
e1 Rational
r1) s :: AlgReal
s@(AlgRational Bool
e2 Rational
r2)
  | (Bool
e1, Rational
r1) forall a. Eq a => a -> a -> Bool
== (Bool
e2, Rational
r2) = AlgReal
f
  | Bool
e1                   = AlgReal
f
  | Bool
e2                   = AlgReal
s
mergeAlgReals String
m AlgReal
_ AlgReal
_ = forall a. HasCallStack => String -> a
error String
m

-- Quickcheck instance
instance Arbitrary AlgReal where
  arbitrary :: Gen AlgReal
arbitrary = Bool -> Rational -> AlgReal
AlgRational Bool
True forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. Arbitrary a => Gen a
arbitrary