{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Tools.BMC (
bmc, bmcWith
) where
import Data.SBV
import Data.SBV.Control
import Control.Monad (when)
bmc :: (EqSymbolic st, Queriable IO st, res ~ QueryResult st)
=> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmc :: forall st res.
(EqSymbolic st, Queriable IO st, res ~ QueryResult st) =>
Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmc = SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> (st -> SBool)
-> IO (Either String (Int, [res]))
forall st res.
(EqSymbolic st, Queriable IO st, res ~ QueryResult st) =>
SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcWith SMTConfig
defaultSMTCfg
bmcWith :: (EqSymbolic st, Queriable IO st, res ~ QueryResult st)
=> SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcWith :: forall st res.
(EqSymbolic st, Queriable IO st, res ~ QueryResult st) =>
SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcWith SMTConfig
cfg Maybe Int
mbLimit Bool
chatty Symbolic ()
setup st -> SBool
initial st -> [st]
trans st -> SBool
goal
= SMTConfig
-> Symbolic (Either String (Int, [res]))
-> IO (Either String (Int, [res]))
forall a. SMTConfig -> Symbolic a -> IO a
runSMTWith SMTConfig
cfg (Symbolic (Either String (Int, [res]))
-> IO (Either String (Int, [res])))
-> Symbolic (Either String (Int, [res]))
-> IO (Either String (Int, [res]))
forall a b. (a -> b) -> a -> b
$ do Symbolic ()
setup
Query (Either String (Int, [res]))
-> Symbolic (Either String (Int, [res]))
forall a. Query a -> Symbolic a
query (Query (Either String (Int, [res]))
-> Symbolic (Either String (Int, [res])))
-> Query (Either String (Int, [res]))
-> Symbolic (Either String (Int, [res]))
forall a b. (a -> b) -> a -> b
$ do st
state <- QueryT IO st
forall (m :: * -> *) a. Queriable m a => QueryT m a
create
SBool -> QueryT IO ()
forall a. QuantifiedBool a => a -> QueryT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ st -> SBool
initial st
state
Int -> st -> [st] -> Query (Either String (Int, [res]))
go Int
0 st
state []
where go :: Int -> st -> [st] -> Query (Either String (Int, [res]))
go Int
i st
_ [st]
_
| Just Int
l <- Maybe Int
mbLimit, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
l
= Either String (Int, [res]) -> Query (Either String (Int, [res]))
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String (Int, [res]) -> Query (Either String (Int, [res])))
-> Either String (Int, [res]) -> Query (Either String (Int, [res]))
forall a b. (a -> b) -> a -> b
$ String -> Either String (Int, [res])
forall a b. a -> Either a b
Left (String -> Either String (Int, [res]))
-> String -> Either String (Int, [res])
forall a b. (a -> b) -> a -> b
$ String
"BMC limit of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" reached"
go Int
i st
curState [st]
sofar = do Bool -> QueryT IO () -> QueryT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
chatty (QueryT IO () -> QueryT IO ()) -> QueryT IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> QueryT IO ()
forall a. IO a -> Query a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"BMC: Iteration: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
Int -> QueryT IO ()
push Int
1
SBool -> QueryT IO ()
forall a. QuantifiedBool a => a -> QueryT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ st -> SBool
goal st
curState
CheckSatResult
cs <- Query CheckSatResult
checkSat
case CheckSatResult
cs of
DSat{} -> String -> Query (Either String (Int, [res]))
forall a. HasCallStack => String -> a
error String
"BMC: Solver returned an unexpected delta-sat result."
CheckSatResult
Sat -> do Bool -> QueryT IO () -> QueryT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
chatty (QueryT IO () -> QueryT IO ()) -> QueryT IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> QueryT IO ()
forall a. IO a -> Query a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"BMC: Solution found at iteration " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
[res]
ms <- (st -> QueryT IO res) -> [st] -> QueryT IO [res]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM st -> QueryT IO res
st -> QueryT IO (QueryResult st)
forall (m :: * -> *) a.
Queriable m a =>
a -> QueryT m (QueryResult a)
project (st
curState st -> [st] -> [st]
forall a. a -> [a] -> [a]
: [st]
sofar)
Either String (Int, [res]) -> Query (Either String (Int, [res]))
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String (Int, [res]) -> Query (Either String (Int, [res])))
-> Either String (Int, [res]) -> Query (Either String (Int, [res]))
forall a b. (a -> b) -> a -> b
$ (Int, [res]) -> Either String (Int, [res])
forall a b. b -> Either a b
Right (Int
i, [res] -> [res]
forall a. [a] -> [a]
reverse [res]
ms)
CheckSatResult
Unk -> do Bool -> QueryT IO () -> QueryT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
chatty (QueryT IO () -> QueryT IO ()) -> QueryT IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> QueryT IO ()
forall a. IO a -> Query a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"BMC: Backend solver said unknown at iteration " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
Either String (Int, [res]) -> Query (Either String (Int, [res]))
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String (Int, [res]) -> Query (Either String (Int, [res])))
-> Either String (Int, [res]) -> Query (Either String (Int, [res]))
forall a b. (a -> b) -> a -> b
$ String -> Either String (Int, [res])
forall a b. a -> Either a b
Left (String -> Either String (Int, [res]))
-> String -> Either String (Int, [res])
forall a b. (a -> b) -> a -> b
$ String
"BMC: Solver said unknown in iteration " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
CheckSatResult
Unsat -> do Int -> QueryT IO ()
pop Int
1
st
nextState <- QueryT IO st
forall (m :: * -> *) a. Queriable m a => QueryT m a
create
SBool -> QueryT IO ()
forall a. QuantifiedBool a => a -> QueryT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ (st -> SBool) -> [st] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAny (st
nextState st -> st -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.==) (st -> [st]
trans st
curState)
Int -> st -> [st] -> Query (Either String (Int, [res]))
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) st
nextState (st
curState st -> [st] -> [st]
forall a. a -> [a] -> [a]
: [st]
sofar)