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

{-# OPTIONS_GHC -Wall -Werror #-}

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

import qualified Data.Ratio as R

import Data.SBV.Core.Data
import Data.SBV.Core.Model () -- instances only

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. One can use the maximization engine
-- to compute the GCD of numbers, but not as a function.)
(.%) :: 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
 = Ratio Integer -> SRational
forall a. SymVal a => a -> SBV a
literal (Ratio Integer -> SRational) -> Ratio Integer -> SRational
forall a b. (a -> b) -> a -> b
$ Integer
t Integer -> Integer -> Ratio Integer
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]