    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Tools.Range
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Single variable valid range detection.
    -----------------------------------------------------------------------------

    {-# LANGUAGE FlexibleContexts    #-}
    {-# LANGUAGE ScopedTypeVariables #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Tools.Range (

             -- * Boundaries and ranges
             Boundary(..), Range(..)

             -- * Computing valid ranges
           , ranges, rangesWith

           ) where

    import Data.SBV
    import Data.SBV.Control

    import Data.SBV.Internals hiding (Range, free_)

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> import Data.SBV
    -- >>> :set -XScopedTypeVariables

    -- | A boundary value
    data Boundary a = Unbounded -- ^ Unbounded
                    | Open   a  -- ^ Exclusive of the point
                    | Closed a  -- ^ Inclusive of the point

    -- | Is this a closed value?
    isClosed :: Boundary a -> Bool
    isClosed :: forall a. Boundary a -> Bool
    isClosed Boundary a
    Unbounded  = Bool
    False
    isClosed (Open   a
    _) = Bool
    False
    isClosed (Closed a
    _) = Bool
    True

    -- | A range is a pair of boundaries: Lower and upper bounds
    data Range a = Range (Boundary a) (Boundary a)

    -- | Show instance for 'Range'
    instance Show a => Show (Range a) where
       show :: Range a -> String
    show (Range Boundary a
    l Boundary a
    u) = Bool -> Boundary a -> String
    forall {a}. Show a => Bool -> Boundary a -> String
    sh Bool
    True Boundary a
    l String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "," String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Bool -> Boundary a -> String
    forall {a}. Show a => Bool -> Boundary a -> String
    sh Bool
    False Boundary a
    u
         where sh :: Bool -> Boundary a -> String
    sh Bool
    onLeft Boundary a
    b = case Boundary a
    b of
                               Boundary a
    Unbounded | Bool
    onLeft -> String
    "(-oo"
                                         | Bool
    True   -> String
    "oo)"
                               Open   a
    v  | Bool
    onLeft -> String
    "(" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    v
                                         | Bool
    True   -> a -> String
    forall a. Show a => a -> String
    show a
    v String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                               Closed a
    v  | Bool
    onLeft -> String
    "[" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    v
                                         | Bool
    True   -> a -> String
    forall a. Show a => a -> String
    show a
    v String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "]"

    -- | Given a single predicate over a single variable, find the contiguous ranges over which the predicate
    -- is satisfied. SBV will make one call to the optimizer, and then as many calls to the solver as there are
    -- disjoint ranges that the predicate is satisfied over. (Linear in the number of ranges.) Note that the
    -- number of ranges is large, this can take a long time!
    --
    -- Beware that, as of June 2021, z3 no longer supports optimization with 'SReal' in the presence of
    -- strict inequalities. See <https://github.com/Z3Prover/z3/issues/5314> for details. So, if you
    -- have 'SReal' variables, it is important that you do /not/ use a strict inequality, i.e., '.>', '.<', './=' etc.
    -- Inequalities of the form '.<=', '.>=' should be OK. Please report if you see any fishy
    -- behavior due to this change in z3's behavior.
    --
    -- Some examples:
    --
    -- >>> ranges (\(_ :: SInteger) -> sFalse)
    -- []
    -- >>> ranges (\(_ :: SInteger) -> sTrue)
    -- [(-oo,oo)]
    -- >>> ranges (\(x :: SInteger) -> sAnd [x .<= 120, x .>= -12, x ./= 3])
    -- [[-12,3),(3,120]]
    -- >>> ranges (\(x :: SInteger) -> sAnd [x .<= 75, x .>= 5, x ./= 6, x ./= 67])
    -- [[5,6),(6,67),(67,75]]
    -- >>> ranges (\(x :: SInteger) -> sAnd [x .<= 75, x ./= 3, x ./= 67])
    -- [(-oo,3),(3,67),(67,75]]
    -- >>> ranges (\(x :: SReal) -> sAnd [x .>= 3.2, x .<= 12.7])
    -- [[3.2,12.7]]
    -- >>> ranges (\(x :: SReal) -> sAnd [x .<= 12.7, x ./= 8])
    -- [(-oo,8.0),(8.0,12.7]]
    -- >>> ranges (\(x :: SReal) -> sAnd [x .>= 12.7, x ./= 15])
    -- [[12.7,15.0),(15.0,oo)]
    -- >>> ranges (\(x :: SInt8) -> sAnd [x .<= 7, x ./= 6])
    -- [[-128,6),(6,7]]
    -- >>> ranges $ \x -> x .>= (0::SReal)
    -- [[0.0,oo)]
    -- >>> ranges $ \x -> x .<= (0::SReal)
    -- [(-oo,0.0]]
    -- >>> ranges $ \(x :: SWord8) -> 2*x .== 4
    -- [[2,3),(129,130]]
    ranges :: forall a. (Ord a, Num a, SymVal a,  SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => (SBV a -> SBool) -> IO [Range a]
    ranges :: forall a.
    (Ord a, Num a, SymVal a, SatModel a, Metric a,
     SymVal (MetricSpace a), SatModel (MetricSpace a)) =>
    (SBV a -> SBool) -> IO [Range a]
    ranges = SMTConfig -> (SBV a -> SBool) -> IO [Range a]
    forall a.
    (Ord a, Num a, SymVal a, SatModel a, Metric a,
     SymVal (MetricSpace a), SatModel (MetricSpace a)) =>
    SMTConfig -> (SBV a -> SBool) -> IO [Range a]
    rangesWith SMTConfig
    defaultSMTCfg

    -- | Compute ranges, using the given solver configuration.
    rangesWith :: forall a. (Ord a, Num a, SymVal a,  SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => SMTConfig -> (SBV a -> SBool) -> IO [Range a]
    rangesWith :: forall a.
    (Ord a, Num a, SymVal a, SatModel a, Metric a,
     SymVal (MetricSpace a), SatModel (MetricSpace a)) =>
    SMTConfig -> (SBV a -> SBool) -> IO [Range a]
    rangesWith SMTConfig
    cfg SBV a -> SBool
    prop = do Maybe (Range a)
    mbBounds <- IO (Maybe (Range a))
    getInitialBounds
                             case Maybe (Range a)
    mbBounds of
                               Maybe (Range a)
    Nothing -> [Range a] -> IO [Range a]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
                               Just Range a
    r  -> [Range a] -> [Range a] -> IO [Range a]
    search [Range a
    r] []

      where getInitialBounds :: IO (Maybe (Range a))
            getInitialBounds :: IO (Maybe (Range a))
    getInitialBounds = do
                let getGenVal :: GeneralizedCV -> Boundary a
                    getGenVal :: GeneralizedCV -> Boundary a
    getGenVal (RegularCV  CV
    cv)  = a -> Boundary a
    forall a. a -> Boundary a
    Closed (a -> Boundary a) -> a -> Boundary a
    forall a b. (a -> b) -> a -> b
    $ CV -> a
    getRegVal CV
    cv
                    getGenVal (ExtendedCV ExtCV
    ecv) = ExtCV -> Boundary a
    getExtVal ExtCV
    ecv

                    getExtVal :: ExtCV -> Boundary a
                    getExtVal :: ExtCV -> Boundary a
    getExtVal (Infinite Kind
    _) = Boundary a
    forall a. Boundary a
    Unbounded
                    getExtVal (Epsilon  Kind
    k) = a -> Boundary a
    forall a. a -> Boundary a
    Open (a -> Boundary a) -> a -> Boundary a
    forall a b. (a -> b) -> a -> b
    $ CV -> a
    getRegVal (Kind -> Integer -> CV
    forall a. Integral a => Kind -> a -> CV
    mkConstCV Kind
    k (Integer
    0::Integer))
                    getExtVal i :: ExtCV
    i@Interval{} = String -> Boundary a
    forall a. HasCallStack => String -> a
    error (String -> Boundary a) -> String -> Boundary a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "*** Data.SBV.ranges.getExtVal: Unexpected interval bounds!"
                                                             , String
    "***"
                                                             , String
    "*** Found bound: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ExtCV -> String
    forall a. Show a => a -> String
    show ExtCV
    i
                                                             , String
    "*** Please report this as a bug!"
                                                             ]
                    getExtVal (BoundedCV CV
    cv) = a -> Boundary a
    forall a. a -> Boundary a
    Closed (a -> Boundary a) -> a -> Boundary a
    forall a b. (a -> b) -> a -> b
    $ CV -> a
    getRegVal CV
    cv
                    getExtVal (AddExtCV ExtCV
    a ExtCV
    b) = ExtCV -> Boundary a
    getExtVal ExtCV
    a Boundary a -> Boundary a -> Boundary a
    `addBound` ExtCV -> Boundary a
    getExtVal ExtCV
    b
                    getExtVal (MulExtCV ExtCV
    a ExtCV
    b) = ExtCV -> Boundary a
    getExtVal ExtCV
    a Boundary a -> Boundary a -> Boundary a
    `mulBound` ExtCV -> Boundary a
    getExtVal ExtCV
    b

                    opBound :: (a -> a -> a) -> Boundary a -> Boundary a -> Boundary a
                    opBound :: (a -> a -> a) -> Boundary a -> Boundary a -> Boundary a
    opBound a -> a -> a
    f Boundary a
    x Boundary a
    y = case (Boundary a -> Maybe a
    forall {a}. Boundary a -> Maybe a
    fromBound Boundary a
    x, Boundary a -> Maybe a
    forall {a}. Boundary a -> Maybe a
    fromBound Boundary a
    y, Boundary a -> Bool
    forall a. Boundary a -> Bool
    isClosed Boundary a
    x Bool -> Bool -> Bool
    && Boundary a -> Bool
    forall a. Boundary a -> Bool
    isClosed Boundary a
    y) of
                                      (Just a
    a, Just a
    b, Bool
    True)  -> a -> Boundary a
    forall a. a -> Boundary a
    Closed (a -> Boundary a) -> a -> Boundary a
    forall a b. (a -> b) -> a -> b
    $ a
    a a -> a -> a
    `f` a
    b
                                      (Just a
    a, Just a
    b, Bool
    False) -> a -> Boundary a
    forall a. a -> Boundary a
    Open   (a -> Boundary a) -> a -> Boundary a
    forall a b. (a -> b) -> a -> b
    $ a
    a a -> a -> a
    `f` a
    b
                                      (Maybe a, Maybe a, Bool)
    _                       -> Boundary a
    forall a. Boundary a
    Unbounded
                      where fromBound :: Boundary a -> Maybe a
    fromBound Boundary a
    Unbounded  = Maybe a
    forall a. Maybe a
    Nothing
                            fromBound (Open   a
    a) = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    a
                            fromBound (Closed a
    a) = a -> Maybe a
    forall a. a -> Maybe a
    Just a
    a

                    addBound, mulBound :: Boundary a -> Boundary a -> Boundary a
                    addBound :: Boundary a -> Boundary a -> Boundary a
    addBound = (a -> a -> a) -> Boundary a -> Boundary a -> Boundary a
    opBound a -> a -> a
    forall a. Num a => a -> a -> a
    (+)
                    mulBound :: Boundary a -> Boundary a -> Boundary a
    mulBound = (a -> a -> a) -> Boundary a -> Boundary a -> Boundary a
    opBound a -> a -> a
    forall a. Num a => a -> a -> a
    (*)

                    getRegVal :: CV -> a
                    getRegVal :: CV -> a
    getRegVal CV
    cv = case [CV] -> Maybe (MetricSpace a, [CV])
    forall a. SatModel a => [CV] -> Maybe (a, [CV])
    parseCVs [CV
    cv] of
                                     Just (MetricSpace a
    v :: MetricSpace a, []) -> case SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral (SBV (MetricSpace a) -> SBV a
    forall a. Metric a => SBV (MetricSpace a) -> SBV a
    fromMetricSpace (MetricSpace a -> SBV (MetricSpace a)
    forall a. SymVal a => a -> SBV a
    literal MetricSpace a
    v)) of
                                                                        Maybe a
    Nothing -> String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.ranges.getRegVal: Cannot extract value from metric space equivalent: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ CV -> String
    forall a. Show a => a -> String
    show CV
    cv
                                                                        Just a
    r  -> a
    r
                                     Maybe (MetricSpace a, [CV])
    _                             -> String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.ranges.getRegVal: Cannot parse " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ CV -> String
    forall a. Show a => a -> String
    show CV
    cv

                    getBound :: (String -> SBV a -> SymbolicT IO b) -> IO (Maybe GeneralizedCV)
    getBound String -> SBV a -> SymbolicT IO b
    cstr = do let objName :: String
    objName = String
    "boundValue"
                                       res :: OptimizeResult
    res@(LexicographicResult SMTResult
    m) <- SMTConfig -> OptimizeStyle -> SymbolicT IO b -> IO OptimizeResult
    forall a.
    Satisfiable a =>
    SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
    optimizeWith SMTConfig
    cfg OptimizeStyle
    Lexicographic (SymbolicT IO b -> IO OptimizeResult)
    -> SymbolicT IO b -> IO OptimizeResult
    forall a b. (a -> b) -> a -> b
    $ do SBV a
    x <- Symbolic (SBV a)
    forall a. SymVal a => Symbolic (SBV a)
    free_
                                                                                                          SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBV a -> SBool
    prop SBV a
    x
                                                                                                          String -> SBV a -> SymbolicT IO b
    cstr String
    objName SBV a
    x
                                       case SMTResult
    m of
                                         Unsatisfiable{} -> Maybe GeneralizedCV -> IO (Maybe GeneralizedCV)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe GeneralizedCV
    forall a. Maybe a
    Nothing
                                         Unknown{}       -> String -> IO (Maybe GeneralizedCV)
    forall a. HasCallStack => String -> a
    error String
    "Solver said Unknown!"
                                         ProofError{}    -> String -> IO (Maybe GeneralizedCV)
    forall a. HasCallStack => String -> a
    error (OptimizeResult -> String
    forall a. Show a => a -> String
    show OptimizeResult
    res)
                                         SMTResult
    _               -> Maybe GeneralizedCV -> IO (Maybe GeneralizedCV)
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe GeneralizedCV -> IO (Maybe GeneralizedCV))
    -> Maybe GeneralizedCV -> IO (Maybe GeneralizedCV)
    forall a b. (a -> b) -> a -> b
    $ String -> SMTResult -> Maybe GeneralizedCV
    forall a. Modelable a => String -> a -> Maybe GeneralizedCV
    getModelObjectiveValue String
    objName SMTResult
    m

                Maybe GeneralizedCV
    mi <- (String -> SBV a -> SymbolicT IO ()) -> IO (Maybe GeneralizedCV)
    forall {b}.
    SatisfiableM IO (SymbolicT IO b) =>
    (String -> SBV a -> SymbolicT IO b) -> IO (Maybe GeneralizedCV)
    getBound String -> SBV a -> SymbolicT IO ()
    forall a. Metric a => String -> SBV a -> SymbolicT IO ()
    minimize
                Maybe GeneralizedCV
    ma <- (String -> SBV a -> SymbolicT IO ()) -> IO (Maybe GeneralizedCV)
    forall {b}.
    SatisfiableM IO (SymbolicT IO b) =>
    (String -> SBV a -> SymbolicT IO b) -> IO (Maybe GeneralizedCV)
    getBound String -> SBV a -> SymbolicT IO ()
    forall a. Metric a => String -> SBV a -> SymbolicT IO ()
    maximize
                case (Maybe GeneralizedCV
    mi, Maybe GeneralizedCV
    ma) of
                  (Just GeneralizedCV
    minV, Just GeneralizedCV
    maxV) -> Maybe (Range a) -> IO (Maybe (Range a))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Range a) -> IO (Maybe (Range a)))
    -> Maybe (Range a) -> IO (Maybe (Range a))
    forall a b. (a -> b) -> a -> b
    $ Range a -> Maybe (Range a)
    forall a. a -> Maybe a
    Just (Range a -> Maybe (Range a)) -> Range a -> Maybe (Range a)
    forall a b. (a -> b) -> a -> b
    $ Boundary a -> Boundary a -> Range a
    forall a. Boundary a -> Boundary a -> Range a
    Range (GeneralizedCV -> Boundary a
    getGenVal GeneralizedCV
    minV) (GeneralizedCV -> Boundary a
    getGenVal GeneralizedCV
    maxV)
                  (Maybe GeneralizedCV, Maybe GeneralizedCV)
    _                      -> Maybe (Range a) -> IO (Maybe (Range a))
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Range a)
    forall a. Maybe a
    Nothing

            -- Is this range satisfiable? Returns a witness to it.
            witness :: Range a -> Symbolic (SBV a)
            witness :: Range a -> Symbolic (SBV a)
    witness (Range Boundary a
    lo Boundary a
    hi) = do SBV a
    x :: SBV a <- Symbolic (SBV a)
    forall a. SymVal a => Symbolic (SBV a)
    free_

                                       let restrict :: Boundary a
    -> (SBV a -> SBV a -> SBool) -> (SBV a -> SBV a -> SBool) -> SBool
    restrict Boundary a
    v SBV a -> SBV a -> SBool
    open SBV a -> SBV a -> SBool
    closed = case Boundary a
    v of
                                                                      Boundary a
    Unbounded -> SBool
    sTrue
                                                                      Open   a
    a  -> SBV a
    x SBV a -> SBV a -> SBool
    `open`   a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    a
                                                                      Closed a
    a  -> SBV a
    x SBV a -> SBV a -> SBool
    `closed` a -> SBV a
    forall a. SymVal a => a -> SBV a
    literal a
    a

                                           lower :: SBool
    lower = Boundary a
    -> (SBV a -> SBV a -> SBool) -> (SBV a -> SBV a -> SBool) -> SBool
    forall {a}.
    SymVal a =>
    Boundary a
    -> (SBV a -> SBV a -> SBool) -> (SBV a -> SBV a -> SBool) -> SBool
    restrict Boundary a
    lo SBV a -> SBV a -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    (.>) SBV a -> SBV a -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    (.>=)
                                           upper :: SBool
    upper = Boundary a
    -> (SBV a -> SBV a -> SBool) -> (SBV a -> SBV a -> SBool) -> SBool
    forall {a}.
    SymVal a =>
    Boundary a
    -> (SBV a -> SBV a -> SBool) -> (SBV a -> SBV a -> SBool) -> SBool
    restrict Boundary a
    hi SBV a -> SBV a -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    (.<) SBV a -> SBV a -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    (.<=)

                                       SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBool
    lower SBool -> SBool -> SBool
    .&& SBool
    upper

                                       SBV a -> Symbolic (SBV a)
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBV a
    x

            isFeasible :: Range a -> IO Bool
            isFeasible :: Range a -> IO Bool
    isFeasible Range a
    r = SMTConfig -> Symbolic Bool -> IO Bool
    forall a. SMTConfig -> Symbolic a -> IO a
    runSMTWith SMTConfig
    cfg (Symbolic Bool -> IO Bool) -> Symbolic Bool -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ do SBV a
    _ <- Range a -> Symbolic (SBV a)
    witness Range a
    r

                                               Query Bool -> Symbolic Bool
    forall a. Query a -> Symbolic a
    query (Query Bool -> Symbolic Bool) -> Query Bool -> Symbolic Bool
    forall a b. (a -> b) -> a -> b
    $ do CheckSatResult
    cs <- Query CheckSatResult
    checkSat
                                                          case CheckSatResult
    cs of
                                                            CheckSatResult
    Unsat  -> Bool -> Query Bool
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                                                            DSat{} -> String -> Query Bool
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.interval.isFeasible: Solver returned a delta-satisfiable result!"
                                                            CheckSatResult
    Unk    -> String -> Query Bool
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.interval.isFeasible: Solver said unknown!"
                                                            CheckSatResult
    Sat    -> Bool -> Query Bool
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True

            bisect :: Range a -> IO (Maybe [Range a])
            bisect :: Range a -> IO (Maybe [Range a])
    bisect r :: Range a
    r@(Range Boundary a
    lo Boundary a
    hi) = SMTConfig -> Symbolic (Maybe [Range a]) -> IO (Maybe [Range a])
    forall a. SMTConfig -> Symbolic a -> IO a
    runSMTWith SMTConfig
    cfg (Symbolic (Maybe [Range a]) -> IO (Maybe [Range a]))
    -> Symbolic (Maybe [Range a]) -> IO (Maybe [Range a])
    forall a b. (a -> b) -> a -> b
    $ do SBV a
    x <- Range a -> Symbolic (SBV a)
    witness Range a
    r

                                                         SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot (SBV a -> SBool
    prop SBV a
    x)

                                                         Query (Maybe [Range a]) -> Symbolic (Maybe [Range a])
    forall a. Query a -> Symbolic a
    query (Query (Maybe [Range a]) -> Symbolic (Maybe [Range a]))
    -> Query (Maybe [Range a]) -> Symbolic (Maybe [Range a])
    forall a b. (a -> b) -> a -> b
    $ do CheckSatResult
    cs <- Query CheckSatResult
    checkSat
                                                                    case CheckSatResult
    cs of
                                                                      CheckSatResult
    Unsat  -> Maybe [Range a] -> Query (Maybe [Range a])
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [Range a]
    forall a. Maybe a
    Nothing
                                                                      DSat{} -> String -> Query (Maybe [Range a])
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.interval.bisect: Solver returned a delta-satisfiable result!"
                                                                      CheckSatResult
    Unk    -> String -> Query (Maybe [Range a])
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.interval.bisect: Solver said unknown!"
                                                                      CheckSatResult
    Sat    -> do Boundary a
    midV <- a -> Boundary a
    forall a. a -> Boundary a
    Open (a -> Boundary a) -> QueryT IO a -> QueryT IO (Boundary a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SBV a -> QueryT IO a
    forall a. SymVal a => SBV a -> Query a
    getValue SBV a
    x
                                                                                   Maybe [Range a] -> Query (Maybe [Range a])
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [Range a] -> Query (Maybe [Range a]))
    -> Maybe [Range a] -> Query (Maybe [Range a])
    forall a b. (a -> b) -> a -> b
    $ [Range a] -> Maybe [Range a]
    forall a. a -> Maybe a
    Just [Boundary a -> Boundary a -> Range a
    forall a. Boundary a -> Boundary a -> Range a
    Range Boundary a
    lo Boundary a
    midV, Boundary a -> Boundary a -> Range a
    forall a. Boundary a -> Boundary a -> Range a
    Range Boundary a
    midV Boundary a
    hi]

            search :: [Range a] -> [Range a] -> IO [Range a]
            search :: [Range a] -> [Range a] -> IO [Range a]
    search []     [Range a]
    sofar = [Range a] -> IO [Range a]
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range a] -> IO [Range a]) -> [Range a] -> IO [Range a]
    forall a b. (a -> b) -> a -> b
    $ [Range a] -> [Range a]
    forall a. [a] -> [a]
    reverse [Range a]
    sofar
            search (Range a
    c:[Range a]
    cs) [Range a]
    sofar = do Bool
    feasible <- Range a -> IO Bool
    isFeasible Range a
    c
                                     if Bool
    feasible
                                        then do Maybe [Range a]
    mbCS <- Range a -> IO (Maybe [Range a])
    bisect Range a
    c
                                                case Maybe [Range a]
    mbCS of
                                                  Maybe [Range a]
    Nothing  -> [Range a] -> [Range a] -> IO [Range a]
    search [Range a]
    cs          (Range a
    cRange a -> [Range a] -> [Range a]
    forall a. a -> [a] -> [a]
    :[Range a]
    sofar)
                                                  Just [Range a]
    xss -> [Range a] -> [Range a] -> IO [Range a]
    search ([Range a]
    xss [Range a] -> [Range a] -> [Range a]
    forall a. [a] -> [a] -> [a]
    ++ [Range a]
    cs) [Range a]
    sofar
                                        else [Range a] -> [Range a] -> IO [Range a]
    search [Range a]
    cs [Range a]
    sofar

    {- HLint ignore rangesWith "Use fromMaybe" -}