-----------------------------------------------------------------------------
-- |
-- 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_)

-- Doctest only
-- $setup
-- >>> :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 :: Boundary a -> Bool
isClosed Unbounded  = Bool
False
isClosed (Open   _) = Bool
False
isClosed (Closed _) = 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 l :: Boundary a
l u :: 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 -> 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 onLeft :: Bool
onLeft b :: Boundary a
b = case Boundary a
b of
                           Unbounded | Bool
onLeft -> "(-oo"
                                     | Bool
True   -> "oo)"
                           Open   v :: a
v  | Bool
onLeft -> "(" 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]
++ ")"
                           Closed v :: a
v  | Bool
onLeft -> "[" 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]
++ "]"

-- | 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! 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 .> 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 :: forall a. (Ord a, Num a, SymVal a,  SMTValue a, SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => (SBV a -> SBool) -> IO [Range a]
ranges :: (SBV a -> SBool) -> IO [Range a]
ranges = SMTConfig -> (SBV a -> SBool) -> IO [Range a]
forall a.
(Ord a, Num a, SymVal a, SMTValue 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,  SMTValue a, SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => SMTConfig -> (SBV a -> SBool) -> IO [Range a]
rangesWith :: SMTConfig -> (SBV a -> SBool) -> IO [Range a]
rangesWith cfg :: SMTConfig
cfg prop :: SBV a -> SBool
prop = do Maybe (Range a)
mbBounds <- IO (Maybe (Range a))
getInitialBounds
                         case Maybe (Range a)
mbBounds of
                           Nothing -> [Range a] -> IO [Range a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                           Just r :: 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
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 ecv :: ExtCV
ecv) = ExtCV -> Boundary a
getExtVal ExtCV
ecv

                getExtVal :: ExtCV -> Boundary a
                getExtVal :: ExtCV -> Boundary a
getExtVal (Infinite _) = Boundary a
forall a. Boundary a
Unbounded
                getExtVal (Epsilon  k :: 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 (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 [ "*** Data.SBV.ranges.getExtVal: Unexpected interval bounds!"
                                                         , "***"
                                                         , "*** Found bound: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExtCV -> String
forall a. Show a => a -> String
show ExtCV
i
                                                         , "*** Please report this as a bug!"
                                                         ]
                getExtVal (BoundedCV cv :: 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 a :: ExtCV
a b :: ExtCV
b) = ExtCV -> Boundary a
getExtVal ExtCV
a Boundary a -> Boundary a -> Boundary a
`addBound` ExtCV -> Boundary a
getExtVal ExtCV
b
                getExtVal (MulExtCV a :: ExtCV
a b :: 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 f :: a -> a -> a
f x :: Boundary a
x y :: 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
a, Just b :: a
b, 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
a, Just b :: a
b, 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
                                  _                       -> Boundary a
forall a. Boundary a
Unbounded
                  where fromBound :: Boundary a -> Maybe a
fromBound Unbounded  = Maybe a
forall a. Maybe a
Nothing
                        fromBound (Open   a :: a
a) = a -> Maybe a
forall a. a -> Maybe a
Just a
a
                        fromBound (Closed a :: 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
cv = case [CV] -> Maybe (MetricSpace a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV
cv] of
                                 Just (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
                                                                    Nothing -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "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 r :: a
r  -> a
r
                                 _                             -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "Data.SBV.ranges.getRegVal: Cannot parse " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
cv

            IndependentResult m :: [(String, SMTResult)]
m <- SMTConfig -> OptimizeStyle -> SymbolicT IO () -> IO OptimizeResult
forall a.
Provable a =>
SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
optimizeWith SMTConfig
cfg OptimizeStyle
Independent (SymbolicT IO () -> IO OptimizeResult)
-> SymbolicT IO () -> 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 (m :: * -> *). SolverContext m => SBool -> 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 ()
forall a. Metric a => String -> SBV a -> SymbolicT IO ()
minimize "min" SBV a
x
                                                                     String -> SBV a -> SymbolicT IO ()
forall a. Metric a => String -> SBV a -> SymbolicT IO ()
maximize "max" SBV a
x
            case [SMTResult] -> SMTResult
forall a. [a] -> a
head (((String, SMTResult) -> SMTResult)
-> [(String, SMTResult)] -> [SMTResult]
forall a b. (a -> b) -> [a] -> [b]
map (String, SMTResult) -> SMTResult
forall a b. (a, b) -> b
snd [(String, SMTResult)]
m) of
              Unsatisfiable{} -> Maybe (Range a) -> IO (Maybe (Range a))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Range a)
forall a. Maybe a
Nothing
              Unknown{}       -> String -> IO (Maybe (Range a))
forall a. HasCallStack => String -> a
error "Solver said Unknown!"
              ProofError{}    -> String -> IO (Maybe (Range a))
forall a. HasCallStack => String -> a
error (OptimizeResult -> String
forall a. Show a => a -> String
show ([(String, SMTResult)] -> OptimizeResult
IndependentResult [(String, SMTResult)]
m))
              _               -> let Just (Just mi :: GeneralizedCV
mi) = String -> SMTResult -> Maybe GeneralizedCV
forall a. Modelable a => String -> a -> Maybe GeneralizedCV
getModelObjectiveValue "min" (SMTResult -> Maybe GeneralizedCV)
-> Maybe SMTResult -> Maybe (Maybe GeneralizedCV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ("min" String -> [(String, SMTResult)] -> Maybe SMTResult
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, SMTResult)]
m)
                                     Just (Just ma :: GeneralizedCV
ma) = String -> SMTResult -> Maybe GeneralizedCV
forall a. Modelable a => String -> a -> Maybe GeneralizedCV
getModelObjectiveValue "max" (SMTResult -> Maybe GeneralizedCV)
-> Maybe SMTResult -> Maybe (Maybe GeneralizedCV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ("max" String -> [(String, SMTResult)] -> Maybe SMTResult
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, SMTResult)]
m)
                                 in Maybe (Range a) -> IO (Maybe (Range 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
mi) (GeneralizedCV -> Boundary a
getGenVal GeneralizedCV
ma)


        bisect :: Range a -> IO (Maybe [Range a])
        bisect :: Range a -> IO (Maybe [Range a])
bisect (Range lo :: Boundary a
lo hi :: 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 <- 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 v :: Boundary a
v open :: SBV a -> SBV a -> SBool
open closed :: SBV a -> SBV a -> SBool
closed = case Boundary a
v of
                                                                    Unbounded -> SBool
sTrue
                                                                    Open   a :: 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
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 (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBool
lower SBool -> SBool -> SBool
.&& SBool
upper SBool -> SBool -> SBool
.&& 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
                                                  Unsat -> Maybe [Range a] -> Query (Maybe [Range a])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Range a]
forall a. Maybe a
Nothing
                                                  Unk   -> String -> Query (Maybe [Range a])
forall a. HasCallStack => String -> a
error "Data.SBV.interval.bisect: Solver said unknown!"
                                                  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. SMTValue a => SBV a -> Query a
getValue SBV a
x
                                                              Maybe [Range a] -> Query (Maybe [Range 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 []     sofar :: [Range a]
sofar = [Range a] -> IO [Range 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 (c :: Range a
c:cs :: [Range a]
cs) sofar :: [Range a]
sofar = do Maybe [Range a]
mbCS <- Range a -> IO (Maybe [Range a])
bisect Range a
c
                                 case Maybe [Range a]
mbCS of
                                   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 xss :: [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

{-# ANN rangesWith ("HLint: ignore Replace case with fromMaybe" :: String) #-}