module Data.SBV.Provers.Prover (
SMTSolver(..), SMTConfig(..), Predicate, Provable(..)
, ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..)
, isSatisfiable, isTheorem
, isSatisfiableWithin, isTheoremWithin
, numberOfModels
, Equality(..)
, prove, proveWith
, sat, satWith
, allSat, allSatWith
, SatModel(..), getModel, displayModels
, defaultSMTCfg, verboseSMTCfg, timingSMTCfg, verboseTimingSMTCfg
, Yices.yices
, timeout
) where
import Control.Monad(when)
import Control.Concurrent(forkIO)
import Control.Concurrent.Chan.Strict
import Data.Maybe(fromJust, isJust)
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.Model
import Data.SBV.SMT.SMT
import Data.SBV.SMT.SMTLib
import qualified Data.SBV.Provers.Yices as Yices
import Data.SBV.Utils.TDiff
defaultSMTCfg :: SMTConfig
defaultSMTCfg = SMTConfig {verbose = False, timing = False, printBase = 10, solver = Yices.yices}
verboseSMTCfg :: SMTConfig
verboseSMTCfg = defaultSMTCfg {verbose=True}
timingSMTCfg :: SMTConfig
timingSMTCfg = defaultSMTCfg {timing=True}
verboseTimingSMTCfg :: SMTConfig
verboseTimingSMTCfg = timingSMTCfg {verbose=True}
timeout :: Int -> SMTConfig -> SMTConfig
timeout n s
| nm == name Yices.yices = s{solver = Yices.timeout n (solver s)}
| True = error $ "SBV.Prover.timeout: Solver " ++ show nm ++ " does not support time-outs"
where nm = name (solver s)
type Predicate = Symbolic SBool
class Provable a where
forAll_ :: a -> Predicate
forAll :: [String] -> a -> Predicate
instance Provable Predicate where
forAll_ = id
forAll _ = id
instance Provable SBool where
forAll_ = output
forAll _ = output
instance (SymWord a, Provable p) => Provable (SBV a -> p) where
forAll_ k = free_ >>= \a -> forAll_ $ k a
forAll (s:ss) k = free s >>= \a -> forAll ss $ k a
forAll [] k = forAll_ k
instance (HasSignAndSize a, HasSignAndSize b, SymArray array, Provable p) => Provable (array a b -> p) where
forAll_ k = newArray_ Nothing >>= \a -> forAll_ $ k a
forAll (s:ss) k = newArray s Nothing >>= \a -> forAll ss $ k a
forAll [] k = forAll_ k
instance (SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) where
forAll_ k = free_ >>= \a -> forAll_ $ \b -> k (a, b)
forAll (s:ss) k = free s >>= \a -> forAll ss $ \b -> k (a, b)
forAll [] k = forAll_ k
instance (SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) where
forAll_ k = free_ >>= \a -> forAll_ $ \b c -> k (a, b, c)
forAll (s:ss) k = free s >>= \a -> forAll ss $ \b c -> k (a, b, c)
forAll [] k = forAll_ k
instance (SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) where
forAll_ k = free_ >>= \a -> forAll_ $ \b c d -> k (a, b, c, d)
forAll (s:ss) k = free s >>= \a -> forAll ss $ \b c d -> k (a, b, c, d)
forAll [] k = forAll_ k
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
forAll_ k = free_ >>= \a -> forAll_ $ \b c d e -> k (a, b, c, d, e)
forAll (s:ss) k = free s >>= \a -> forAll ss $ \b c d e -> k (a, b, c, d, e)
forAll [] k = forAll_ k
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
forAll_ k = free_ >>= \a -> forAll_ $ \b c d e f -> k (a, b, c, d, e, f)
forAll (s:ss) k = free s >>= \a -> forAll ss $ \b c d e f -> k (a, b, c, d, e, f)
forAll [] k = forAll_ k
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
forAll_ k = free_ >>= \a -> forAll_ $ \b c d e f g -> k (a, b, c, d, e, f, g)
forAll (s:ss) k = free s >>= \a -> forAll ss $ \b c d e f g -> k (a, b, c, d, e, f, g)
forAll [] k = forAll_ k
prove :: Provable a => a -> IO ThmResult
prove = proveWith defaultSMTCfg
sat :: Provable a => a -> IO SatResult
sat = satWith defaultSMTCfg
allSat :: Provable a => a -> IO AllSatResult
allSat = allSatWith defaultSMTCfg
checkTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
checkTheorem mbTo p = do r <- pr p
case r of
ThmResult (Unsatisfiable _) -> return $ Just True
ThmResult (Satisfiable _ _) -> return $ Just False
ThmResult (TimeOut _) -> return Nothing
_ -> error $ "SBV.isTheorem: Received:\n" ++ show r
where pr = maybe prove (\i -> proveWith (timeout i defaultSMTCfg)) mbTo
checkSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
checkSatisfiable mbTo p = do r <- s p
case r of
SatResult (Satisfiable _ _) -> return $ Just True
SatResult (Unsatisfiable _) -> return $ Just False
SatResult (TimeOut _) -> return Nothing
_ -> error $ "SBV.isSatisfiable: Received: " ++ show r
where s = maybe sat (\i -> satWith (timeout i defaultSMTCfg)) mbTo
isTheoremWithin :: Provable a => Int -> a -> IO (Maybe Bool)
isTheoremWithin i = checkTheorem (Just i)
isSatisfiableWithin :: Provable a => Int -> a -> IO (Maybe Bool)
isSatisfiableWithin i = checkSatisfiable (Just i)
isTheorem :: Provable a => a -> IO Bool
isTheorem p = fromJust `fmap` checkTheorem Nothing p
isSatisfiable :: Provable a => a -> IO Bool
isSatisfiable p = fromJust `fmap` checkSatisfiable Nothing p
numberOfModels :: Provable a => a -> IO Int
numberOfModels p = do AllSatResult rs <- allSat p
return $ sum $ map walk rs
where walk (Satisfiable{}) = 1
walk r = error $ "numberOfModels: Unexpected result from an allSat check: " ++ show (AllSatResult [r])
proveWith :: Provable a => SMTConfig -> a -> IO ThmResult
proveWith config a = generateTrace config False a >>= callSolver [] "Checking Theoremhood.." ThmResult config
satWith :: Provable a => SMTConfig -> a -> IO SatResult
satWith config a = generateTrace config True a >>= callSolver [] "Checking Satisfiability.." SatResult config
allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult
allSatWith config p = do when (verbose config) $ putStrLn "** Checking Satisfiability, all solutions.."
sbvPgm <- generateTrace config True p
resChan <- newChan
let add = writeChan resChan . Just
stop = writeChan resChan Nothing
final r = add r >> stop
fork io = if verbose config then io else forkIO io >> return ()
fork $ go sbvPgm add stop final (1::Int) []
results <- getChanContents resChan
return $ AllSatResult $ map fromJust $ takeWhile isJust results
where go sbvPgm add stop final = loop
where loop !n nonEqConsts = do
SatResult r <- callSolver nonEqConsts ("Looking for solution " ++ show n) SatResult config sbvPgm
case r of
Satisfiable _ [] -> final r
Unknown _ [] -> final r
ProofError _ _ -> final r
TimeOut _ -> stop
Unsatisfiable _ -> stop
Satisfiable _ model -> add r >> loop (n+1) (model : nonEqConsts)
Unknown _ model -> add r >> loop (n+1) (model : nonEqConsts)
callSolver :: [[(String, CW)]] -> String -> (SMTResult -> b) -> SMTConfig -> ([NamedSymVar], SMTLibPgm) -> IO b
callSolver nonEqConstraints checkMsg wrap config (inps, smtLibPgm) = do
let msg = when (verbose config) . putStrLn . ("** " ++)
msg checkMsg
let finalPgm = addNonEqConstraints nonEqConstraints smtLibPgm
msg $ "Generated SMTLib program:\n" ++ finalPgm
smtAnswer <- engine (solver config) config inps finalPgm
msg "Done.."
return $ wrap smtAnswer
generateTrace :: Provable a => SMTConfig -> Bool -> a -> IO ([NamedSymVar], SMTLibPgm)
generateTrace config isSat predicate = do
let msg = when (verbose config) . putStrLn . ("** " ++)
isTiming = timing config
msg "Generating a symbolic trace.."
res <- timeIf isTiming "problem construction" $ runSymbolic $ forAll_ predicate
msg $ "Generated symbolic trace:\n" ++ show res
msg "Translating to SMT-Lib.."
case res of
Result is consts tbls arrs pgm [o@(SW{})] -> timeIf isTiming "translation" $ return (is, toSMTLib isSat is consts tbls arrs pgm o)
_ -> error $ "SBVProver.callSolver: Impossible happened: " ++ show res
infix 4 ===
class Equality a where
(===) :: a -> a -> IO ThmResult
instance (SymWord a, EqSymbolic z) => Equality (SBV a -> z) where
k === l = prove $ \a -> k a .== l a
instance (SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) where
k === l = prove $ \a b -> k a b .== l a b
instance (SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) where
k === l = prove $ \a b -> k (a, b) .== l (a, b)
instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) where
k === l = prove $ \a b c -> k a b c .== l a b c
instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) where
k === l = prove $ \a b c -> k (a, b, c) .== l (a, b, c)
instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) where
k === l = prove $ \a b c d -> k a b c d .== l a b c d
instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) where
k === l = prove $ \a b c d -> k (a, b, c, d) .== l (a, b, c, d)
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) where
k === l = prove $ \a b c d e -> k a b c d e .== l a b c d e
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) where
k === l = prove $ \a b c d e -> k (a, b, c, d, e) .== l (a, b, c, d, e)
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) where
k === l = prove $ \a b c d e f -> k a b c d e f .== l a b c d e f
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) where
k === l = prove $ \a b c d e f -> k (a, b, c, d, e, f) .== l (a, b, c, d, e, f)
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) where
k === l = prove $ \a b c d e f g -> k a b c d e f g .== l a b c d e f g
instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) where
k === l = prove $ \a b c d e f g -> k (a, b, c, d, e, f, g) .== l (a, b, c, d, e, f, g)