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
, yices, z3
, compileToSMTLib
) where
import qualified Control.Exception as E
import Control.Concurrent (forkIO)
import Control.Concurrent.Chan.Strict (newChan, writeChan, getChanContents)
import Control.Monad (when)
import Data.List (intercalate)
import Data.Maybe (fromJust, isJust, catMaybes)
import System.Time (getClockTime)
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 qualified Data.SBV.Provers.Z3 as Z3
import Data.SBV.Utils.TDiff
yices :: SMTConfig
yices = SMTConfig {verbose = False, timing = False, timeOut = Nothing, printBase = 10, smtFile = Nothing, solver = Yices.yices, useSMTLib2 = False}
z3 :: SMTConfig
z3 = yices { solver = Z3.z3, useSMTLib2 = True }
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_ = return
forAll _ = return
instance (SymWord a, Provable p) => Provable (SBV a -> p) where
forAll_ k = forall_ >>= \a -> forAll_ $ k a
forAll (s:ss) k = forall 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 = forall_ >>= \a -> forAll_ $ \b -> k (a, b)
forAll (s:ss) k = forall 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 = forall_ >>= \a -> forAll_ $ \b c -> k (a, b, c)
forAll (s:ss) k = forall 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 = forall_ >>= \a -> forAll_ $ \b c d -> k (a, b, c, d)
forAll (s:ss) k = forall 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 = forall_ >>= \a -> forAll_ $ \b c d e -> k (a, b, c, d, e)
forAll (s:ss) k = forall 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 = forall_ >>= \a -> forAll_ $ \b c d e f -> k (a, b, c, d, e, f)
forAll (s:ss) k = forall 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 = forall_ >>= \a -> forAll_ $ \b c d e f g -> k (a, b, c, d, e, f, g)
forAll (s:ss) k = forall 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 yices
sat :: Provable a => a -> IO SatResult
sat = satWith yices
allSat :: Provable a => a -> IO AllSatResult
allSat = allSatWith yices
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 (yices{timeOut = Just i})) 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 yices{timeOut = Just i}) 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 $ length rs
compileToSMTLib :: Provable a => Bool -> a -> IO String
compileToSMTLib smtLib2 a = do
t <- getClockTime
let comments = ["Created on " ++ show t]
cvt = if smtLib2 then toSMTLib2 else toSMTLib1
(_, _, _, smtLibPgm) <- simulate cvt yices False comments a
return $ show smtLibPgm ++ "\n"
proveWith :: Provable a => SMTConfig -> a -> IO ThmResult
proveWith config a = simulate cvt config False [] a >>= callSolver False "Checking Theoremhood.." ThmResult config
where cvt = if useSMTLib2 config then toSMTLib2 else toSMTLib1
satWith :: Provable a => SMTConfig -> a -> IO SatResult
satWith config a = simulate cvt config True [] a >>= callSolver True "Checking Satisfiability.." SatResult config
where cvt = if useSMTLib2 config then toSMTLib2 else toSMTLib1
allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult
allSatWith config p = do
let converter = if useSMTLib2 config then toSMTLib2 else toSMTLib1
msg "Checking Satisfiability, all solutions.."
sbvPgm@(qinps, _, _, _) <- simulate converter config True [] p
resChan <- newChan
let add = writeChan resChan . Just
stop = writeChan resChan Nothing
final r = add r >> stop
die m = final (ProofError config [m])
fork io = if verbose config then io else forkIO io >> return ()
fork $ E.catch (go sbvPgm add stop final (1::Int) [])
(\e -> die (show (e::E.SomeException)))
results <- getChanContents resChan
let w = ALL `elem` map fst qinps
return $ AllSatResult (w, map fromJust (takeWhile isJust results))
where msg = when (verbose config) . putStrLn . ("** " ++)
go sbvPgm add stop final = loop
where loop !n nonEqConsts = do
curResult <- invoke nonEqConsts n sbvPgm
case curResult of
Nothing -> stop
Just (SatResult r) -> case r of
Satisfiable _ (SMTModel [] _ _) -> final r
Unknown _ (SMTModel [] _ _) -> final r
ProofError _ _ -> final r
TimeOut _ -> stop
Unsatisfiable _ -> stop
Satisfiable _ model -> add r >> loop (n+1) (modelAssocs model : nonEqConsts)
Unknown _ model -> add r >> loop (n+1) (modelAssocs model : nonEqConsts)
invoke nonEqConsts n (qinps, modelMap, skolemMap, smtLibPgm) = do
msg $ "Looking for solution " ++ show n
case addNonEqConstraints qinps nonEqConsts smtLibPgm of
Nothing ->
return Nothing
Just finalPgm -> do msg $ "Generated SMTLib program:\n" ++ finalPgm
smtAnswer <- engine (solver config) config True qinps modelMap skolemMap finalPgm
msg "Done.."
return $ Just $ SatResult smtAnswer
callSolver :: Bool -> String -> (SMTResult -> b) -> SMTConfig -> ([(Quantifier, NamedSymVar)], [(String, UnintKind)], [Either SW (SW, [SW])], SMTLibPgm) -> IO b
callSolver isSat checkMsg wrap config (qinps, modelMap, skolemMap, smtLibPgm) = do
let msg = when (verbose config) . putStrLn . ("** " ++)
msg checkMsg
let finalPgm = intercalate "\n" (pre ++ post) where SMTLibPgm _ (_, pre, post) = smtLibPgm
msg $ "Generated SMTLib program:\n" ++ finalPgm
smtAnswer <- engine (solver config) config isSat qinps modelMap skolemMap finalPgm
msg "Done.."
return $ wrap smtAnswer
simulate :: Provable a => SMTLibConverter -> SMTConfig -> Bool -> [String] -> a -> IO ([(Quantifier, NamedSymVar)], [(String, UnintKind)], [Either SW (SW, [SW])], SMTLibPgm)
simulate converter config isSat comments predicate = do
let msg = when (verbose config) . putStrLn . ("** " ++)
isTiming = timing config
msg "Starting symbolic simulation.."
res <- timeIf isTiming "problem construction" $ runSymbolic $ forAll_ predicate >>= output
msg $ "Generated symbolic trace:\n" ++ show res
msg "Translating to SMT-Lib.."
case res of
Result hasInfPrec _codeSegs is consts tbls arrs uis axs pgm [o@(SW (False, Size (Just 1)) _)] ->
timeIf isTiming "translation" $ do let uiMap = catMaybes (map arrayUIKind arrs) ++ map unintFnUIKind uis
skolemMap = skolemize (if isSat then is else map flipQ is)
where flipQ (ALL, x) = (EX, x)
flipQ (EX, x) = (ALL, x)
skolemize :: [(Quantifier, NamedSymVar)] -> [Either SW (SW, [SW])]
skolemize qinps = go qinps ([], [])
where go [] (_, sofar) = reverse sofar
go ((ALL, (v, _)):rest) (us, sofar) = go rest (v:us, Left v : sofar)
go ((EX, (v, _)):rest) (us, sofar) = go rest (us, Right (v, reverse us) : sofar)
return (is, uiMap, skolemMap, converter hasInfPrec isSat comments is skolemMap consts tbls arrs uis axs pgm o)
Result _hasInfPrec _codeSegs _is _consts _tbls _arrs _uis _axs _pgm os -> case length os of
0 -> error $ "Impossible happened, unexpected non-outputting result\n" ++ show res
1 -> error $ "Impossible happened, non-boolean output in " ++ show os
++ "\nDetected while generating the trace:\n" ++ show res
_ -> error $ "User error: Multiple output values detected: " ++ show os
++ "\nDetected while generating the trace:\n" ++ show res
++ "\n*** Check calls to \"output\", they are typically not needed!"
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)