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

{-# LANGUAGE FlexibleInstances #-}

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

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

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

-- | 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

-- | Check wheter a given argument is an exact rational
isExactRational :: AlgReal -> Bool
isExactRational :: AlgReal -> Bool
isExactRational (AlgRational True _) = Bool
True
isExactRational _                    = 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
(AlgRealPoly -> AlgRealPoly -> Bool)
-> (AlgRealPoly -> AlgRealPoly -> Bool) -> Eq AlgRealPoly
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
Eq AlgRealPoly =>
(AlgRealPoly -> AlgRealPoly -> Ordering)
-> (AlgRealPoly -> AlgRealPoly -> Bool)
-> (AlgRealPoly -> AlgRealPoly -> Bool)
-> (AlgRealPoly -> AlgRealPoly -> Bool)
-> (AlgRealPoly -> AlgRealPoly -> Bool)
-> (AlgRealPoly -> AlgRealPoly -> AlgRealPoly)
-> (AlgRealPoly -> AlgRealPoly -> AlgRealPoly)
-> Ord 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
$cp1Ord :: Eq AlgRealPoly
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 (exact :: Bool
exact, str :: String
str))
 = case (String
str, (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '.') String
str) of
      ("", (_, _))    -> Bool -> Rational -> AlgReal
AlgRational Bool
exact 0
      (_, (x :: String
x, '.':y :: String
y)) -> Bool -> Rational -> AlgReal
AlgRational Bool
exact (String -> Integer
forall a. Read a => String -> a
read (String
xString -> String -> String
forall a. [a] -> [a] -> [a]
++String
y) Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% (10 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
y))
      (_, (x :: String
x, _))     -> Bool -> Rational -> AlgReal
AlgRational Bool
exact (String -> Integer
forall a. Read a => String -> a
read String
x Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% 1)
mkPolyReal (Right (k :: Integer
k, coeffs :: [(Integer, Integer)]
coeffs))
 = (Integer, AlgRealPoly) -> Maybe String -> AlgReal
AlgPolyRoot (Integer
k, [(Integer, Integer)] -> AlgRealPoly
AlgRealPoly ([(Integer, Integer)] -> [(Integer, Integer)]
normalize [(Integer, Integer)]
coeffs)) Maybe String
forall a. Maybe a
Nothing
 where normalize :: [(Integer, Integer)] -> [(Integer, Integer)]
       normalize :: [(Integer, Integer)] -> [(Integer, Integer)]
normalize = [(Integer, Integer)] -> [(Integer, Integer)]
forall b a. (Eq b, Num a) => [(a, b)] -> [(a, b)]
merge ([(Integer, Integer)] -> [(Integer, Integer)])
-> ([(Integer, Integer)] -> [(Integer, Integer)])
-> [(Integer, Integer)]
-> [(Integer, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Integer, Integer) -> (Integer, Integer) -> Ordering)
-> [(Integer, Integer)] -> [(Integer, Integer)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Integer -> Integer -> Ordering) -> Integer -> Integer -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer -> Integer -> Ordering)
-> ((Integer, Integer) -> Integer)
-> (Integer, Integer)
-> (Integer, Integer)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Integer, Integer) -> Integer
forall a b. (a, b) -> b
snd)
       merge :: [(a, b)] -> [(a, b)]
merge []                     = []
       merge [x :: (a, b)
x]                    = [(a, b)
x]
       merge ((a :: a
a, b :: b
b):r :: [(a, b)]
r@((c :: a
c, d :: b
d):xs :: [(a, b)]
xs))
         | b
b b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
d                   = [(a, b)] -> [(a, b)]
merge ((a
aa -> a -> a
forall a. Num a => a -> a -> a
+a
c, b
b)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
xs)
         | Bool
True                     = (a
a, b
b) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)]
merge [(a, b)]
r

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

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

-- lift unary op through an exact rational, otherwise bail
lift1 :: String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 :: String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 _  o :: Rational -> Rational
o (AlgRational e :: Bool
e a :: Rational
a) = Bool -> Rational -> AlgReal
AlgRational Bool
e (Rational -> Rational
o Rational
a)
lift1 nm :: String
nm _ a :: AlgReal
a                 = String -> AlgReal
forall a. HasCallStack => String -> a
error (String -> AlgReal) -> String -> AlgReal
forall a b. (a -> b) -> a -> b
$ "AlgReal." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": unsupported argument: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
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 _  o :: Rational -> Rational -> Rational
o (AlgRational True a :: Rational
a) (AlgRational True b :: Rational
b) = Bool -> Rational -> AlgReal
AlgRational Bool
True (Rational
a Rational -> Rational -> Rational
`o` Rational
b)
lift2 nm :: String
nm _ a :: AlgReal
a                    b :: AlgReal
b                    = String -> AlgReal
forall a. HasCallStack => String -> a
error (String -> AlgReal) -> String -> AlgReal
forall a b. (a -> b) -> a -> b
$ "AlgReal." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": unsupported arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
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 True a :: Rational
a == :: AlgReal -> AlgReal -> Bool
== AlgRational True b :: Rational
b = Rational
a Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
b
  a :: AlgReal
a                  == b :: AlgReal
b                  = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "AlgReal.==: unsupported arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
forall a. Show a => a -> String
show (AlgReal
a, AlgReal
b)

instance Ord AlgReal where
  AlgRational True a :: Rational
a compare :: AlgReal -> AlgReal -> Ordering
`compare` AlgRational True b :: Rational
b = Rational
a Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Rational
b
  a :: AlgReal
a                  `compare` b :: AlgReal
b                  = String -> Ordering
forall a. HasCallStack => String -> a
error (String -> Ordering) -> String -> Ordering
forall a b. (a -> b) -> a -> b
$ "AlgReal.compare: unsupported arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
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 a :: Bool
a b :: Rational
b algRealStructuralEqual :: AlgReal -> AlgReal -> Bool
`algRealStructuralEqual` AlgRational c :: Bool
c d :: Rational
d = (Bool
a, Rational
b) (Bool, Rational) -> (Bool, Rational) -> Bool
forall a. Eq a => a -> a -> Bool
== (Bool
c, Rational
d)
AlgPolyRoot a :: (Integer, AlgRealPoly)
a b :: Maybe String
b `algRealStructuralEqual` AlgPolyRoot c :: (Integer, AlgRealPoly)
c d :: Maybe String
d = ((Integer, AlgRealPoly)
a, Maybe String
b) ((Integer, AlgRealPoly), Maybe String)
-> ((Integer, AlgRealPoly), Maybe String) -> Bool
forall a. Eq a => a -> a -> Bool
== ((Integer, AlgRealPoly)
c, Maybe String
d)
_               `algRealStructuralEqual` _               = Bool
False

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

instance Num AlgReal where
  + :: AlgReal -> AlgReal -> AlgReal
(+)         = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 "+"      Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(+)
  * :: AlgReal -> AlgReal -> AlgReal
(*)         = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 "*"      Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(*)
  (-)         = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 "-"      (-)
  negate :: AlgReal -> AlgReal
negate      = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 "negate" Rational -> Rational
forall a. Num a => a -> a
negate
  abs :: AlgReal -> AlgReal
abs         = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 "abs"    Rational -> Rational
forall a. Num a => a -> a
abs
  signum :: AlgReal -> AlgReal
signum      = String -> (Rational -> Rational) -> AlgReal -> AlgReal
lift1 "signum" Rational -> Rational
forall a. Num a => a -> a
signum
  fromInteger :: Integer -> AlgReal
fromInteger = Bool -> Rational -> AlgReal
AlgRational Bool
True (Rational -> AlgReal)
-> (Integer -> Rational) -> Integer -> AlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Rational
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 True _) / :: AlgReal -> AlgReal -> AlgReal
/ (AlgRational True b :: Rational
b) | Rational
b Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = 0
  a :: AlgReal
a                    / b :: AlgReal
b                             = String
-> (Rational -> Rational -> Rational)
-> AlgReal
-> AlgReal
-> AlgReal
lift2 "/" Rational -> Rational -> Rational
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 True v :: Rational
v) = Rational
v
  toRational x :: AlgReal
x                    = String -> Rational
forall a. HasCallStack => String -> a
error (String -> Rational) -> String -> Rational
forall a b. (a -> b) -> a -> b
$ "AlgReal.toRational: Argument cannot be represented as a rational value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
algRealToHaskell AlgReal
x

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

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

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

instance Random AlgReal where
  random :: g -> (AlgReal, g)
random g :: g
g = let (a :: Rational
a, g' :: g
g') = g -> (Rational, 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 :: (AlgReal, AlgReal) -> g -> (AlgReal, g)
randomR (AlgRational True l :: Rational
l, AlgRational True h :: Rational
h) g :: g
g = let (a :: Rational
a, g' :: g
g') = (Rational, Rational) -> g -> (Rational, 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 lh :: (AlgReal, AlgReal)
lh                                       _ = String -> (AlgReal, g)
forall a. HasCallStack => String -> a
error (String -> (AlgReal, g)) -> String -> (AlgReal, g)
forall a b. (a -> b) -> a -> b
$ "AlgReal.randomR: unsupported bounds: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (AlgReal, AlgReal) -> String
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 True r :: Rational
r)
   | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = "0.0"
   | Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0  = "(- (/ "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Integer -> Integer
forall a. Num a => a -> a
abs Integer
m) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0))"
   | Bool
True   =    "(/ "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
m       String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".0)"
  where (m :: Integer
m, n :: Integer
n) = (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r, Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r)
algRealToSMTLib2 r :: AlgReal
r@(AlgRational False _)
   = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "SBV: Unexpected inexact rational to be converted to SMTLib2: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
algRealToSMTLib2 (AlgPolyRoot (i :: Integer
i, AlgRealPoly xs :: [(Integer, Integer)]
xs) _) = "(root-obj (+ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (((Integer, Integer) -> [String])
-> [(Integer, Integer)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Integer, Integer) -> [String]
forall a a.
(Eq a, Num a, Num a, Ord a, Show a, Show a) =>
(a, a) -> [String]
term [(Integer, Integer)]
xs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
  where term :: (a, a) -> [String]
term (0, _) = []
        term (k :: a
k, 0) = [a -> String
forall a. (Ord a, Num a, Show a) => a -> String
coeff a
k]
        term (1, 1) = ["x"]
        term (1, p :: a
p) = ["(^ x " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"]
        term (k :: a
k, 1) = ["(* " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. (Ord a, Num a, Show a) => a -> String
coeff a
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ " x)"]
        term (k :: a
k, p :: a
p) = ["(* " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. (Ord a, Num a, Show a) => a -> String
coeff a
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (^ x " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"]
        coeff :: a -> String
coeff n :: a
n | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = "(- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (a -> a
forall a. Num a => a -> a
abs a
n) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                | Bool
True  = a -> String
forall a. Show a => a -> String
show a
n

-- | 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 True r :: Rational
r) = "((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall a. Show a => a -> String
show Rational
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") :: Rational)"
algRealToHaskell r :: AlgReal
r                    = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "SBV.algRealToHaskell: Unsupported argument: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r

-- 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 exact :: Bool
exact r :: Rational
r = String -> String
p (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ case Integer -> [Integer] -> Maybe (Int, String)
f25 (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r) [] of
                       Nothing               -> Rational -> String
forall a. Show a => a -> String
show Rational
r   -- bail out, not precisely representable with finite digits
                       Just (noOfZeros :: Int
noOfZeros, num :: String
num) -> let present :: Int
present = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
num
                                                in String -> String
neg (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ case Int
noOfZeros Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
present of
                                                           LT -> let (b :: String
b, a :: String
a) = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
present Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
noOfZeros) String
num in String
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ "." String -> String -> String
forall a. [a] -> [a] -> [a]
++ if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
a then "0" else String
a
                                                           EQ -> "0." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
num
                                                           GT -> "0." String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
noOfZeros Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
present) '0' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
num
  where p :: String -> String
p   = if Bool
exact then String -> String
forall a. a -> a
id else (String -> String -> String
forall a. [a] -> [a] -> [a]
++ "...")
        neg :: String -> String
neg = if Rational
r Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then ('-'Char -> String -> String
forall a. a -> [a] -> [a]
:) else String -> String
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 1 sofar :: [Integer]
sofar = let (ts :: [Integer]
ts, fs :: [Integer]
fs)   = (Integer -> Bool) -> [Integer] -> ([Integer], [Integer])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 2) [Integer]
sofar
                          [lts :: Int
lts, lfs :: Int
lfs] = ([Integer] -> Int) -> [[Integer]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map [Integer] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Integer]
ts, [Integer]
fs]
                          noOfZeros :: Int
noOfZeros  = Int
lts Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` Int
lfs
                      in (Int, String) -> Maybe (Int, String)
forall a. a -> Maybe a
Just (Int
noOfZeros, Integer -> String
forall a. Show a => a -> String
show (Integer -> Integer
forall a. Num a => a -> a
abs (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r)  Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* [Integer] -> [Integer] -> Integer
forall p t t. Num p => [t] -> [t] -> p
factor [Integer]
ts [Integer]
fs))
        f25 v :: Integer
v sofar :: [Integer]
sofar = let (q2 :: Integer
q2, r2 :: Integer
r2) = Integer
v Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`quotRem` 2
                          (q5 :: Integer
q5, r5 :: Integer
r5) = Integer
v Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`quotRem` 5
                      in case (Integer
r2, Integer
r5) of
                           (0, _) -> Integer -> [Integer] -> Maybe (Int, String)
f25 Integer
q2 (2 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
sofar)
                           (_, 0) -> Integer -> [Integer] -> Maybe (Int, String)
f25 Integer
q5 (5 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
sofar)
                           _      -> Maybe (Int, String)
forall a. Maybe a
Nothing
        -- compute the next power of 10 we need to get to
        factor :: [t] -> [t] -> p
factor []     fs :: [t]
fs     = [p] -> p
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [2 | t
_ <- [t]
fs]
        factor ts :: [t]
ts     []     = [p] -> p
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [5 | t
_ <- [t]
ts]
        factor (_:ts :: [t]
ts) (_:fs :: [t]
fs) = [t] -> [t] -> p
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 _ f :: AlgReal
f@(AlgRational exact :: Bool
exact r :: Rational
r) (AlgPolyRoot kp :: (Integer, AlgRealPoly)
kp Nothing)
  | Bool
exact = AlgReal
f
  | Bool
True  = (Integer, AlgRealPoly) -> Maybe String -> AlgReal
AlgPolyRoot (Integer, AlgRealPoly)
kp (String -> Maybe String
forall a. a -> Maybe a
Just (Bool -> Rational -> String
showRat Bool
False Rational
r))
mergeAlgReals _ (AlgPolyRoot kp :: (Integer, AlgRealPoly)
kp Nothing) f :: AlgReal
f@(AlgRational exact :: Bool
exact r :: Rational
r)
  | Bool
exact = AlgReal
f
  | Bool
True  = (Integer, AlgRealPoly) -> Maybe String -> AlgReal
AlgPolyRoot (Integer, AlgRealPoly)
kp (String -> Maybe String
forall a. a -> Maybe a
Just (Bool -> Rational -> String
showRat Bool
False Rational
r))
mergeAlgReals _ f :: AlgReal
f@(AlgRational e1 :: Bool
e1 r1 :: Rational
r1) s :: AlgReal
s@(AlgRational e2 :: Bool
e2 r2 :: Rational
r2)
  | (Bool
e1, Rational
r1) (Bool, Rational) -> (Bool, Rational) -> Bool
forall a. Eq a => a -> a -> Bool
== (Bool
e2, Rational
r2) = AlgReal
f
  | Bool
e1                   = AlgReal
f
  | Bool
e2                   = AlgReal
s
mergeAlgReals m :: String
m _ _ = String -> 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 (Rational -> AlgReal) -> Gen Rational -> Gen AlgReal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Gen Rational
forall a. Arbitrary a => Gen a
arbitrary