    -----------------------------------------------------------------------------
    -- |
    -- 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
               , algRealToRational
               , 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(..))

    import Numeric (readSigned, readFloat)

    -- | 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
    $ [String] -> String
    unlines [ ""
                                                            , "SBV.algRealToHaskell: Unsupported argument:"
                                                            , ""
                                                            , "   " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ AlgReal -> String
    forall a. Show a => a -> String
    show AlgReal
    r
                                                            , ""
                                                            , "represents an irrational number, and cannot be converted to a Haskell value."
                                                            ]

    -- | 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 -> Either Rational Rational
    algRealToRational :: AlgReal -> Either Rational Rational
    algRealToRational a :: AlgReal
    a = case AlgReal
    a of
                            AlgRational True  r :: Rational
    r        -> Rational -> Either Rational Rational
    forall a b. a -> Either a b
    Left Rational
    r
                            AlgRational False r :: Rational
    r        -> Rational -> Either Rational Rational
    forall a b. a -> Either a b
    Left Rational
    r
                            AlgPolyRoot _     Nothing  -> Either Rational Rational
    forall a. a
    bad
                            AlgPolyRoot _     (Just s :: String
    s) -> let trimmed :: String
    trimmed = case String -> String
    forall a. [a] -> [a]
    reverse String
    s of
                                                                         '.':'.':'.':rest :: String
    rest -> String -> String
    forall a. [a] -> [a]
    reverse String
    rest
                                                                         _                -> String
    s
                                                          in case ReadS Rational -> ReadS Rational
    forall a. Real a => ReadS a -> ReadS a
    readSigned ReadS Rational
    forall a. RealFrac a => ReadS a
    readFloat String
    trimmed of
                                                               [(v :: Rational
    v, "")] -> Rational -> Either Rational Rational
    forall a b. b -> Either a b
    Right Rational
    v
                                                               _         -> Either Rational Rational
    forall a. a
    bad
       where bad :: a
    bad = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                   , "SBV.algRealToRational: Unsupported argument:"
                                   , ""
                                   , "   " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ AlgReal -> String
    forall a. Show a => a -> String
    show AlgReal
    a
                                   , ""
                                   , "represents an irrational number that cannot be approximated."
                                   ]

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