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

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

module Data.SBV.Rational (
    -- * Constructing rationals
      (.%)
  ) where

import qualified Data.Ratio as R

import Data.SBV.Core.Data
import Data.SBV.Core.Model

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]

-- | 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 (String -> Op
Uninterpreted String
"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 (String -> Op
Uninterpreted String
"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

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