-----------------------------------------------------------------------------
-- |
-- 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 #-}
{-# LANGUAGE TypeApplications    #-}

{-# 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.Proxy

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

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

-- | 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 t'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 :: SWord 4) -> 2*x .== 4
-- [[2,3),(9,10]]
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 mbBounds <- IO (Maybe (Range a))
getInitialBounds
                         case 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@(LexicographicResult 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 x <- Symbolic (SBV a)
forall a. SymVal a => Symbolic (SBV a)
free_
                                                                                                      constrain $ prop x
                                                                                                      cstr objName x
                                   case 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 (Proxy a -> ShowS
forall a. Metric a => Proxy a -> ShowS
annotateForMS (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a) String
objName) SMTResult
m

            mi <- (String -> SBV a -> SymbolicT IO ()) -> IO (Maybe GeneralizedCV)
forall {b}.
Satisfiable (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
            ma <- getBound maximize
            case (mi, 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 x :: SBV a <- Symbolic (SBV a)
forall a. SymVal a => Symbolic (SBV a)
free_

                                   let 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 = 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 = 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
(.<=)

                                   constrain $ lower .&& upper

                                   return 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 _ <- Range a -> Symbolic (SBV a)
witness Range a
r

                                           query $ do cs <- checkSat
                                                      case 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 x <- Range a -> Symbolic (SBV a)
witness Range a
r

                                                     constrain $ sNot (prop x)

                                                     query $ do cs <- checkSat
                                                                case 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 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
                                                                               return $ Just [Range lo midV, Range midV 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 feasible <- Range a -> IO Bool
isFeasible Range a
c
                                 if feasible
                                    then do mbCS <- bisect c
                                            case 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 search cs sofar

{- HLint ignore rangesWith "Use fromMaybe" -}