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