-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Rational
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Symbolic rationals, corresponds to Haskell's 'Rational' type
-----------------------------------------------------------------------------

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}

{-# OPTIONS_GHC -Wall -Werror -Wno-orphans #-}

module Data.SBV.Rational (
    -- * Constructing rationals
      (.%)
    -- * Rounding rationals
    , sRationalToSIntegerFloor, sRationalToSIntegerCeiling, sRationalToSIntegerTruncate
    , sRationalToSIntegerRoundAway, sRationalToSIntegerRoundToEven, sRationalToSIntegerRM
    -- * Converting between rationals and reals
    , sRationalToSReal, sRealToSRational
    ) where

import qualified Data.Ratio as R

import Data.SBV.Core.AlgReals (isExactRational)
import Data.SBV.Core.Data
import Data.SBV.Core.Model
import Data.SBV.Core.Symbolic (newInternalVariable)
import Data.SBV.Utils.Numeric (roundAway)

infixl 7 .%

-- | Construct a symbolic rational from a given numerator and denominator. Note that
-- it is not possible to deconstruct a rational by taking numerator and denominator
-- fields, since we do not represent them canonically. (This is due to the fact that
-- SMTLib has no functions to compute the GCD. While we can define a recursive function
-- to do so, it would almost always imply non-decidability for even the simplest queries.)
(.%) :: SInteger -> SInteger -> SRational
SInteger
top .% :: SInteger -> SInteger -> SRational
.% SInteger
bot
 | Just Integer
t <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
top
 , Just Integer
b <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
bot
 = Rational -> SRational
forall a. SymVal a => a -> SBV a
literal (Rational -> SRational) -> Rational -> SRational
forall a b. (a -> b) -> a -> b
$ Integer
t Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
R.% Integer
b
 | Bool
True
 = SVal -> SRational
forall a. SVal -> SBV a
SBV (SVal -> SRational) -> SVal -> SRational
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KRational (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
 where res :: State -> IO SV
res State
st = do SV
t <- State -> SInteger -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SInteger
top
                   SV
b <- State -> SInteger -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SInteger
bot
                   State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KRational (SBVExpr -> IO SV) -> SBVExpr -> IO SV
forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp Op
RationalConstructor [SV
t, SV
b]

-- | Convert an SRational to an SInteger, @floor@ version. That is, it computes
-- the largest integer @n@ that satisfies @(n .% 1) <= r@.
--
-- For instance, @1.3@ will be @1@, but @-1.3@ will be @-2@.
--
-- See 'sRationalToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.
sRationalToSIntegerFloor :: SRational -> SInteger
-- NB: We use @sDiv@ below because it implements division that truncates
-- towards negative infinity, which is exactly what @floor@ needs.
sRationalToSIntegerFloor :: SRational -> SInteger
sRationalToSIntegerFloor = (Rational -> Integer)
-> ((SInteger, SInteger) -> SInteger) -> SRational -> SInteger
forall t.
SymVal t =>
(Rational -> t)
-> ((SInteger, SInteger) -> SBV t) -> SRational -> SBV t
lift1 Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor ((SInteger -> SInteger -> SInteger)
-> (SInteger, SInteger) -> SInteger
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SInteger -> SInteger -> SInteger
forall a. SDivisible a => a -> a -> a
sDiv)

-- | Convert an SRational to an SInteger, @ceiling@ version. That is, it
-- computes the smallest integer @n@ that satisfies @r <= (n .% 1)@.
--
-- For instance, @1.3@ will be @2@, but @-1.3@ will be @-1@.
--
-- See 'sRationalToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.
sRationalToSIntegerCeiling :: SRational -> SInteger
sRationalToSIntegerCeiling :: SRational -> SInteger
sRationalToSIntegerCeiling SRational
x
  | Just Rational
i <- SRational -> Maybe Rational
forall a. SymVal a => SBV a -> Maybe a
unliteral SRational
x
  = Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal (Integer -> SInteger) -> Integer -> SInteger
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
i
  | Bool
True
  = - (SRational -> SInteger
sRationalToSIntegerFloor (- SRational
x))

-- | Convert an SRational to an SInteger, truncating version. Truncate simply
-- chops off the fractional part, essentially rounding towards zero.
--
-- For instance, @1.3@ will be @1@, and @-1.3@ will be @-1@.
--
-- See 'sRationalToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.
sRationalToSIntegerTruncate :: SRational -> SInteger
sRationalToSIntegerTruncate :: SRational -> SInteger
sRationalToSIntegerTruncate SRational
x
  | Just Rational
i <- SRational -> Maybe Rational
forall a. SymVal a => SBV a -> Maybe a
unliteral SRational
x
  = Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal (Integer -> SInteger) -> Integer -> SInteger
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
truncate Rational
i
  | Bool
True
  = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SRational
x SRational -> SRational -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SRational
0) (SRational -> SInteger
sRationalToSIntegerFloor SRational
x) (SRational -> SInteger
sRationalToSIntegerCeiling SRational
x)

-- | Convert an SRational to an SInteger by converting to the nearest integer.
-- If there is a tie (i.e., if the fractional component of the SRational is
-- equal to 0.5), then round away from zero.
--
-- For instance:
--
-- * @1.3@ will be @1@
-- * @1.5@ will be @2@ (because @abs 1 < abs 2@)
-- * @1.7@ will be @2@
-- * @2.3@ will be @2@
-- * @2.5@ will be @3@ (because @abs 2 < abs 3@)
-- * @2.7@ will be @3@
-- * @-1.3@ will be @-1@
-- * @-1.5@ will be @-2@ (because @abs (-1) < abs (-2)@)
-- * @-1.7@ will be @-2@
-- * @-2.3@ will be @-2@
-- * @-2.5@ will be @-3@ (because @abs (-2) < abs (-3)@)
-- * @-2.7@ will be @-3@
--
-- See 'sRationalToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.
sRationalToSIntegerRoundAway :: SRational -> SInteger
sRationalToSIntegerRoundAway :: SRational -> SInteger
sRationalToSIntegerRoundAway SRational
x
  | Just Rational
i <- SRational -> Maybe Rational
forall a. SymVal a => SBV a -> Maybe a
unliteral SRational
x
  = Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal (Integer -> SInteger) -> Integer -> SInteger
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
roundAway Rational
i
  | Bool
True
  = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite
      (SRational
x SRational -> SRational -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SRational
0)
      (SRational -> SInteger
sRationalToSIntegerFloor   (SRational
x SRational -> SRational -> SRational
forall a. Num a => a -> a -> a
+ SRational
half))
      (SRational -> SInteger
sRationalToSIntegerCeiling (SRational
x SRational -> SRational -> SRational
forall a. Num a => a -> a -> a
- SRational
half))
  where
    half :: SRational
    half :: SRational
half = SRational
0.5

-- | Convert an SRational to an SInteger by converting to the nearest integer.
-- If there is a tie (i.e., if the fractional component of the SRational is
-- equal to 0.5), then round to the nearest even integer.
--
-- For instance:
--
-- * @1.3@ will be @1@
-- * @1.5@ will be @2@ (because @2@ is even)
-- * @1.7@ will be @2@
-- * @2.3@ will be @2@
-- * @2.5@ will be @2@ (because @2@ is even)
-- * @2.7@ will be @3@
-- * @-1.3@ will be @-1@
-- * @-1.5@ will be @-2@ (because @-2@ is even)
-- * @-1.7@ will be @-2@
-- * @-2.3@ will be @-2@
-- * @-2.5@ will be @-2@ (because @-2@ is even)
-- * @-2.7@ will be @-3@
--
-- See 'sRationalToSIntegerRM' to select the rounding mode with a symbolic 'SRoundingMode'.
sRationalToSIntegerRoundToEven :: SRational -> SInteger
sRationalToSIntegerRoundToEven :: SRational -> SInteger
sRationalToSIntegerRoundToEven SRational
x
  | Just Rational
i <- SRational -> Maybe Rational
forall a. SymVal a => SBV a -> Maybe a
unliteral SRational
x
  = Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal (Integer -> SInteger) -> Integer -> SInteger
forall a b. (a -> b) -> a -> b
$ Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
round Rational
i
  | Bool
True
  = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SRational
diff SRational -> SRational -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SRational
half) SInteger
lo (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$
    SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SRational
diff SRational -> SRational -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SRational
half) SInteger
hi (SInteger -> SInteger) -> SInteger -> SInteger
forall a b. (a -> b) -> a -> b
$
    SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (Integer -> SInteger -> SBool
sDivides Integer
2 SInteger
lo) SInteger
lo SInteger
hi
  where
    half :: SRational
    half :: SRational
half = SRational
0.5

    lo, hi :: SInteger
    lo :: SInteger
lo = SRational -> SInteger
sRationalToSIntegerFloor SRational
x
    hi :: SInteger
hi = SInteger
loSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1

    diff :: SRational
    diff :: SRational
diff = SRational
x SRational -> SRational -> SRational
forall a. Num a => a -> a -> a
- (SInteger
lo SInteger -> SInteger -> SRational
.% SInteger
1)

-- | Convert an 'SRational' to an 'SInteger' according to the supplied
-- 'SRoundingMode'. This dispatches to 'sRationalToSIntegerRoundToEven',
-- 'sRationalToSIntegerRoundAway', 'sRationalToSIntegerCeiling',
-- 'sRationalToSIntegerFloor', and 'sRationalToSIntegerTruncate' for the
-- round-nearest-even, round-nearest-away, round-toward-positive,
-- round-toward-negative, and round-toward-zero modes respectively.
--
-- Note that we re-use the 'SRoundingMode' type here, even though
-- 'SRoundingMode' is normally associated with floating-point operations. The
-- floating-point resemblance is superficial, as this function does not use any
-- floating-point functionality behind the scenes.
sRationalToSIntegerRM :: SRoundingMode -> SRational -> SInteger
sRationalToSIntegerRM :: SRoundingMode -> SRational -> SInteger
sRationalToSIntegerRM SRoundingMode
rm SRational
x =
  SInteger
-> SInteger
-> SInteger
-> SInteger
-> SInteger
-> SRoundingMode
-> SInteger
forall r.
Mergeable r =>
r -> r -> r -> r -> r -> SRoundingMode -> r
sCaseRoundingMode
    (SRational -> SInteger
sRationalToSIntegerRoundToEven SRational
x)
    (SRational -> SInteger
sRationalToSIntegerRoundAway SRational
x)
    (SRational -> SInteger
sRationalToSIntegerCeiling SRational
x)
    (SRational -> SInteger
sRationalToSIntegerFloor SRational
x)
    (SRational -> SInteger
sRationalToSIntegerTruncate SRational
x)
    SRoundingMode
rm

-- | Convert an 'SRational' to an 'SReal'. This conversion is always exact: the
-- rational @t .% b@ maps to the real @t \/ b@. (Recall that denominators are
-- always positive, so no division-by-zero can arise here.)
sRationalToSReal :: SRational -> SReal
sRationalToSReal :: SRational -> SBV AlgReal
sRationalToSReal = (Rational -> AlgReal)
-> ((SInteger, SInteger) -> SBV AlgReal)
-> SRational
-> SBV AlgReal
forall t.
SymVal t =>
(Rational -> t)
-> ((SInteger, SInteger) -> SBV t) -> SRational -> SBV t
lift1 Rational -> AlgReal
forall a. Fractional a => Rational -> a
fromRational (\(SInteger
t, SInteger
b) -> SInteger -> SBV AlgReal
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SInteger
t SBV AlgReal -> SBV AlgReal -> SBV AlgReal
forall a. Fractional a => a -> a -> a
/ SInteger -> SBV AlgReal
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SInteger
b)

-- | Convert an 'SReal' to an 'SRational'. The conversion is /exact/ for reals
-- that are rational: a concrete rational is converted directly, while a
-- symbolic (or non-literal) real is handled by introducing a fresh symbolic
-- rational @r@ and constraining @'sRationalToSReal' r '.==' x@. Thus, whenever
-- the input real is representable as the ratio of two integers, the result
-- denotes exactly that same value---no precision is lost.
--
-- Note the caveat implied by this encoding: if the input real is /irrational/
-- (i.e., not expressible as a ratio of two integers), then the introduced
-- equality constraint is unsatisfiable, which renders the entire problem
-- @UNSAT@. In other words, using this function is an implicit assertion that
-- its argument is a rational number.
sRealToSRational :: SReal -> SRational
sRealToSRational :: SBV AlgReal -> SRational
sRealToSRational SBV AlgReal
x
  | Just AlgReal
v <- SBV AlgReal -> Maybe AlgReal
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV AlgReal
x, AlgReal -> Bool
isExactRational AlgReal
v
  = Rational -> SRational
forall a. SymVal a => a -> SBV a
literal (AlgReal -> Rational
forall a. Real a => a -> Rational
toRational AlgReal
v)
  | Bool
True
  = SVal -> SRational
forall a. SVal -> SBV a
SBV (SVal -> SRational) -> SVal -> SRational
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KRational (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
  where res :: State -> IO SV
res State
st = do SV
n <- State -> Kind -> IO SV
newInternalVariable State
st Kind
KRational
                    let r :: SRational
r = SVal -> SRational
forall a. SVal -> SBV a
SBV (Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KRational (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache (IO SV -> State -> IO SV
forall a b. a -> b -> a
const (SV -> IO SV
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SV
n))))) :: SRational
                    State -> Bool -> [(String, String)] -> SVal -> IO ()
internalConstraint State
st Bool
False [] (SVal -> IO ()) -> SVal -> IO ()
forall a b. (a -> b) -> a -> b
$ SBool -> SVal
forall a. SBV a -> SVal
unSBV (SBool -> SVal) -> SBool -> SVal
forall a b. (a -> b) -> a -> b
$ SRational -> SBV AlgReal
sRationalToSReal SRational
r SBV AlgReal -> SBV AlgReal -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV AlgReal
x
                    SV -> IO SV
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SV
n

-- | Get the numerator. Note that this is always symbolic since we don't have a concrete representation.
-- Furthermore this is only used internally and is not exported to the user, since it is not canonical.
doNotExport_numerator :: SRational -> SInteger
doNotExport_numerator :: SRational -> SInteger
doNotExport_numerator SRational
x = SVal -> SInteger
forall a. SVal -> SBV a
SBV (SVal -> SInteger) -> SVal -> SInteger
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KUnbounded (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
  where res :: State -> IO SV
res State
st = do SV
xv <- State -> SRational -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SRational
x
                    State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KUnbounded (SBVExpr -> IO SV) -> SBVExpr -> IO SV
forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (Text -> Op
Uninterpreted Text
"sbv.rat.numerator") [SV
xv]

-- | Get the numerator. Note that this is always symbolic since we don't have a concrete representation.
-- Furthermore this is only used internally and is not exported to the user, since it is not canonical.
doNotExport_denominator :: SRational -> SInteger
doNotExport_denominator :: SRational -> SInteger
doNotExport_denominator SRational
x = SVal -> SInteger
forall a. SVal -> SBV a
SBV (SVal -> SInteger) -> SVal -> SInteger
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KUnbounded (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
  where res :: State -> IO SV
res State
st = do SV
xv <- State -> SRational -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SRational
x
                    State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KUnbounded (SBVExpr -> IO SV) -> SBVExpr -> IO SV
forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (Text -> Op
Uninterpreted Text
"sbv.rat.denominator") [SV
xv]

-- | Num instance for SRational. Note that denominators are always positive.
instance Num SRational where
  fromInteger :: Integer -> SRational
fromInteger Integer
i  = SVal -> SRational
forall a. SVal -> SBV a
SBV (SVal -> SRational) -> SVal -> SRational
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KRational (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV)) -> CV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
KRational (Integer -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i :: Integer)
  + :: SRational -> SRational -> SRational
(+)            = (Rational -> Rational -> Rational)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SRational)
-> SRational
-> SRational
-> SRational
forall t.
SymVal t =>
(Rational -> Rational -> t)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBV t)
-> SRational
-> SRational
-> SBV t
lift2 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(+)    (\(SInteger
t1, SInteger
b1) (SInteger
t2, SInteger
b2) -> (SInteger
t1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
t2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b1) SInteger -> SInteger -> SRational
.% (SInteger
b1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b2))
  (-)            = (Rational -> Rational -> Rational)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SRational)
-> SRational
-> SRational
-> SRational
forall t.
SymVal t =>
(Rational -> Rational -> t)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBV t)
-> SRational
-> SRational
-> SBV t
lift2 (-)    (\(SInteger
t1, SInteger
b1) (SInteger
t2, SInteger
b2) -> (SInteger
t1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
t2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b1) SInteger -> SInteger -> SRational
.% (SInteger
b1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b2))
  * :: SRational -> SRational -> SRational
(*)            = (Rational -> Rational -> Rational)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SRational)
-> SRational
-> SRational
-> SRational
forall t.
SymVal t =>
(Rational -> Rational -> t)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBV t)
-> SRational
-> SRational
-> SBV t
lift2 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
(*)    (\(SInteger
t1, SInteger
b1) (SInteger
t2, SInteger
b2) -> (SInteger
t1      SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
t2     ) SInteger -> SInteger -> SRational
.% (SInteger
b1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b2))
  abs :: SRational -> SRational
abs            = (Rational -> Rational)
-> ((SInteger, SInteger) -> SRational) -> SRational -> SRational
forall t.
SymVal t =>
(Rational -> t)
-> ((SInteger, SInteger) -> SBV t) -> SRational -> SBV t
lift1 Rational -> Rational
forall a. Num a => a -> a
abs    (\(SInteger
t, SInteger
b) -> SInteger -> SInteger
forall a. Num a => a -> a
abs    SInteger
t SInteger -> SInteger -> SRational
.% SInteger
b)
  negate :: SRational -> SRational
negate         = (Rational -> Rational)
-> ((SInteger, SInteger) -> SRational) -> SRational -> SRational
forall t.
SymVal t =>
(Rational -> t)
-> ((SInteger, SInteger) -> SBV t) -> SRational -> SBV t
lift1 Rational -> Rational
forall a. Num a => a -> a
negate (\(SInteger
t, SInteger
b) -> SInteger -> SInteger
forall a. Num a => a -> a
negate SInteger
t SInteger -> SInteger -> SRational
.% SInteger
b)
  signum :: SRational -> SRational
signum SRational
a       = SBool -> SRational -> SRational -> SRational
forall a. Mergeable a => SBool -> a -> a -> a
ite (SRational
a SRational -> SRational -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SRational
0) SRational
1 (SRational -> SRational) -> SRational -> SRational
forall a b. (a -> b) -> a -> b
$ SBool -> SRational -> SRational -> SRational
forall a. Mergeable a => SBool -> a -> a -> a
ite (SRational
a SRational -> SRational -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SRational
0) (-SRational
1) SRational
0

-- | Fractional instance for SRational. Just like the 'Num' instance, division is
-- implemented at the SBV level via cross-multiplication, since SMTLib has no direct
-- support for our rational representation. Note that we keep the denominator positive:
-- dividing by @t2 .% b2@ multiplies the denominator by @t2@, which may be negative, so
-- we flip the signs of both parts when needed. Following the SBV convention for reals,
-- division by zero is defined to be zero.
--
-- We mark this @OVERLAPPING@ as it takes precedence over the generic instance in "Data.SBV.Core.Model",
-- which would otherwise try to translate rational division as an SMTLib @Quot@ (which doesn't exist for our rationals).
instance {-# OVERLAPPING #-} Fractional SRational where
  fromRational :: Rational -> SRational
fromRational = Rational -> SRational
forall a. SymVal a => a -> SBV a
literal (Rational -> SRational)
-> (Rational -> Rational) -> Rational -> SRational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Fractional a => Rational -> a
fromRational
  SRational
a / :: SRational -> SRational -> SRational
/ SRational
b        = SBool -> SRational -> SRational -> SRational
forall a. Mergeable a => SBool -> a -> a -> a
ite (SRational
b SRational -> SRational -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SRational
0) SRational
0 ((Rational -> Rational -> Rational)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SRational)
-> SRational
-> SRational
-> SRational
forall t.
SymVal t =>
(Rational -> Rational -> t)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBV t)
-> SRational
-> SRational
-> SBV t
lift2 Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
(/) (SInteger, SInteger) -> (SInteger, SInteger) -> SRational
divRat SRational
a SRational
b)
    where divRat :: (SInteger, SInteger) -> (SInteger, SInteger) -> SRational
divRat (SInteger
t1, SInteger
b1) (SInteger
t2, SInteger
b2) = SBool -> SRational -> SRational -> SRational
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
t2 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0) (        SInteger
num SInteger -> SInteger -> SRational
.%         SInteger
den)
                                                   (SInteger -> SInteger
forall a. Num a => a -> a
negate  SInteger
num SInteger -> SInteger -> SRational
.% SInteger -> SInteger
forall a. Num a => a -> a
negate  SInteger
den)
             where num :: SInteger
num = SInteger
t1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b2
                   den :: SInteger
den = SInteger
b1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
t2

-- | Symbolic ordering for SRational. Note that denominators are always positive.
instance OrdSymbolic SRational where
   .< :: SRational -> SRational -> SBool
(.<)  = (Rational -> Rational -> Bool)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBool)
-> SRational
-> SRational
-> SBool
forall t.
SymVal t =>
(Rational -> Rational -> t)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBV t)
-> SRational
-> SRational
-> SBV t
lift2 Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
(<)  (\(SInteger
t1, SInteger
b1) (SInteger
t2, SInteger
b2) -> (SInteger
t1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b2) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<  (SInteger
b1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
t2))
   .<= :: SRational -> SRational -> SBool
(.<=) = (Rational -> Rational -> Bool)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBool)
-> SRational
-> SRational
-> SBool
forall t.
SymVal t =>
(Rational -> Rational -> t)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBV t)
-> SRational
-> SRational
-> SBV t
lift2 Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
(<=) (\(SInteger
t1, SInteger
b1) (SInteger
t2, SInteger
b2) -> (SInteger
t1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b2) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= (SInteger
b1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
t2))
   .> :: SRational -> SRational -> SBool
(.>)  = (Rational -> Rational -> Bool)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBool)
-> SRational
-> SRational
-> SBool
forall t.
SymVal t =>
(Rational -> Rational -> t)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBV t)
-> SRational
-> SRational
-> SBV t
lift2 Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
(>)  (\(SInteger
t1, SInteger
b1) (SInteger
t2, SInteger
b2) -> (SInteger
t1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b2) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>  (SInteger
b1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
t2))
   .>= :: SRational -> SRational -> SBool
(.>=) = (Rational -> Rational -> Bool)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBool)
-> SRational
-> SRational
-> SBool
forall t.
SymVal t =>
(Rational -> Rational -> t)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBV t)
-> SRational
-> SRational
-> SBV t
lift2 Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
(>=) (\(SInteger
t1, SInteger
b1) (SInteger
t2, SInteger
b2) -> (SInteger
t1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
b2) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= (SInteger
b1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
t2))

-- | Get the top and bottom parts. Internal only; do not export!
doNotExport_getTB :: SRational -> (SInteger, SInteger)
doNotExport_getTB :: SRational -> (SInteger, SInteger)
doNotExport_getTB SRational
a = (SRational -> SInteger
doNotExport_numerator SRational
a, SRational -> SInteger
doNotExport_denominator SRational
a)

-- | Lift a function over one rational
lift1 :: SymVal t => (Rational -> t) -> ((SInteger,  SInteger) -> SBV t) -> SRational -> SBV t
lift1 :: forall t.
SymVal t =>
(Rational -> t)
-> ((SInteger, SInteger) -> SBV t) -> SRational -> SBV t
lift1 Rational -> t
cf (SInteger, SInteger) -> SBV t
f SRational
a
 | Just Rational
va <- SRational -> Maybe Rational
forall a. SymVal a => SBV a -> Maybe a
unliteral SRational
a
 = t -> SBV t
forall a. SymVal a => a -> SBV a
literal (Rational -> t
cf Rational
va)
 | Bool
True
 = (SInteger, SInteger) -> SBV t
f (SRational -> (SInteger, SInteger)
doNotExport_getTB SRational
a)

-- | Lift a function over two rationals
lift2 :: SymVal t => (Rational -> Rational -> t) -> ((SInteger,  SInteger) -> (SInteger,  SInteger) -> SBV t) -> SRational -> SRational -> SBV t
lift2 :: forall t.
SymVal t =>
(Rational -> Rational -> t)
-> ((SInteger, SInteger) -> (SInteger, SInteger) -> SBV t)
-> SRational
-> SRational
-> SBV t
lift2 Rational -> Rational -> t
cf (SInteger, SInteger) -> (SInteger, SInteger) -> SBV t
f SRational
a SRational
b
 | Just Rational
va <- SRational -> Maybe Rational
forall a. SymVal a => SBV a -> Maybe a
unliteral SRational
a, Just Rational
vb <- SRational -> Maybe Rational
forall a. SymVal a => SBV a -> Maybe a
unliteral SRational
b
 = t -> SBV t
forall a. SymVal a => a -> SBV a
literal (Rational
va Rational -> Rational -> t
`cf` Rational
vb)
 | Bool
True
 = (SInteger, SInteger) -> (SInteger, SInteger) -> SBV t
f (SRational -> (SInteger, SInteger)
doNotExport_getTB SRational
a) (SRational -> (SInteger, SInteger)
doNotExport_getTB SRational
b)

{- HLint ignore type doNotExport_numerator   "Use camelCase" -}
{- HLint ignore type doNotExport_denominator "Use camelCase" -}
{- HLint ignore type doNotExport_getTB       "Use camelCase" -}