module Data.SBV.Provers.Prover (
SMTSolver(..), SMTConfig(..), Predicate, Provable(..)
, ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..)
, isSatisfiable, isSatisfiableWith, isTheorem, isTheoremWith
, Equality(..)
, prove, proveWith
, sat, satWith
, allSat, allSatWith
, isVacuous, isVacuousWith
, solve
, SatModel(..), Modelable(..), displayModels, extractModels
, boolector, cvc4, yices, z3, defaultSMTCfg
, compileToSMTLib, generateSMTBenchmarks
, sbvCheckSolverInstallation
) where
import qualified Control.Exception as E
import Control.Concurrent (forkIO, newChan, writeChan, getChanContents)
import Control.Monad (when, unless, void)
import Data.List (intercalate)
import Data.Maybe (fromJust, isJust, mapMaybe)
import System.FilePath (addExtension)
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.Boolector as Boolector
import qualified Data.SBV.Provers.CVC4 as CVC4
import qualified Data.SBV.Provers.Yices as Yices
import qualified Data.SBV.Provers.Z3 as Z3
import Data.SBV.Utils.TDiff
import Data.SBV.Utils.Boolean
mkConfig :: SMTSolver -> Bool -> [String] -> SMTConfig
mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False
, timing = False
, timeOut = Nothing
, printBase = 10
, printRealPrec = 16
, smtFile = Nothing
, solver = s
, solverTweaks = tweaks
, useSMTLib2 = isSMTLib2
, satCmd = "(check-sat)"
}
boolector :: SMTConfig
boolector = mkConfig Boolector.boolector True []
cvc4 :: SMTConfig
cvc4 = mkConfig CVC4.cvc4 True []
yices :: SMTConfig
yices = mkConfig Yices.yices False []
z3 :: SMTConfig
z3 = mkConfig Z3.z3 True ["(set-option :smt.mbqi true) ; use model based quantifier instantiation"]
defaultSMTCfg :: SMTConfig
defaultSMTCfg = z3
type Predicate = Symbolic SBool
class Provable a where
forAll_ :: a -> Predicate
forAll :: [String] -> a -> Predicate
forSome_ :: a -> Predicate
forSome :: [String] -> a -> Predicate
instance Provable Predicate where
forAll_ = id
forAll [] = id
forAll xs = error $ "SBV.forAll: Extra unmapped name(s) in predicate construction: " ++ intercalate ", " xs
forSome_ = id
forSome [] = id
forSome xs = error $ "SBV.forSome: Extra unmapped name(s) in predicate construction: " ++ intercalate ", " xs
instance Provable SBool where
forAll_ = return
forAll _ = return
forSome_ = return
forSome _ = 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
forSome_ k = exists_ >>= \a -> forSome_ $ k a
forSome (s:ss) k = exists s >>= \a -> forSome ss $ k a
forSome [] k = forSome_ k
instance (HasKind a, HasKind 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
forSome_ _ = error "SBV.forSome: Existential arrays are not currently supported."
forSome _ _ = error "SBV.forSome: Existential arrays are not currently supported."
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
forSome_ k = exists_ >>= \a -> forSome_ $ \b -> k (a, b)
forSome (s:ss) k = exists s >>= \a -> forSome ss $ \b -> k (a, b)
forSome [] k = forSome_ 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
forSome_ k = exists_ >>= \a -> forSome_ $ \b c -> k (a, b, c)
forSome (s:ss) k = exists s >>= \a -> forSome ss $ \b c -> k (a, b, c)
forSome [] k = forSome_ 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
forSome_ k = exists_ >>= \a -> forSome_ $ \b c d -> k (a, b, c, d)
forSome (s:ss) k = exists s >>= \a -> forSome ss $ \b c d -> k (a, b, c, d)
forSome [] k = forSome_ 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
forSome_ k = exists_ >>= \a -> forSome_ $ \b c d e -> k (a, b, c, d, e)
forSome (s:ss) k = exists s >>= \a -> forSome ss $ \b c d e -> k (a, b, c, d, e)
forSome [] k = forSome_ 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
forSome_ k = exists_ >>= \a -> forSome_ $ \b c d e f -> k (a, b, c, d, e, f)
forSome (s:ss) k = exists s >>= \a -> forSome ss $ \b c d e f -> k (a, b, c, d, e, f)
forSome [] k = forSome_ 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
forSome_ k = exists_ >>= \a -> forSome_ $ \b c d e f g -> k (a, b, c, d, e, f, g)
forSome (s:ss) k = exists s >>= \a -> forSome ss $ \b c d e f g -> k (a, b, c, d, e, f, g)
forSome [] k = forSome_ k
prove :: Provable a => a -> IO ThmResult
prove = proveWith defaultSMTCfg
sat :: Provable a => a -> IO SatResult
sat = satWith defaultSMTCfg
solve :: [SBool] -> Symbolic SBool
solve = return . bAnd
allSat :: Provable a => a -> IO AllSatResult
allSat = allSatWith defaultSMTCfg
isVacuous :: Provable a => a -> IO Bool
isVacuous = isVacuousWith defaultSMTCfg
isTheoremWith :: Provable a => SMTConfig -> Maybe Int -> a -> IO (Maybe Bool)
isTheoremWith cfg mbTo p = do r <- proveWith cfg{timeOut = mbTo} 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
isSatisfiableWith :: Provable a => SMTConfig -> Maybe Int -> a -> IO (Maybe Bool)
isSatisfiableWith cfg mbTo p = do r <- satWith cfg{timeOut = mbTo} p
case r of
SatResult (Satisfiable _ _) -> return $ Just True
SatResult (Unsatisfiable _) -> return $ Just False
SatResult (TimeOut _) -> return Nothing
_ -> error $ "SBV.isSatisfiable: Received: " ++ show r
isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
isTheorem = isTheoremWith defaultSMTCfg
isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)
isSatisfiable = isSatisfiableWith defaultSMTCfg
compileToSMTLib :: Provable a => Bool
-> Bool
-> a
-> IO String
compileToSMTLib smtLib2 isSat a = do
t <- getClockTime
let comments = ["Created on " ++ show t]
cvt = if smtLib2 then toSMTLib2 else toSMTLib1
(_, _, _, _, smtLibPgm) <- simulate cvt defaultSMTCfg isSat comments a
let out = show smtLibPgm
return $ out ++ if smtLib2
then "\n(check-sat)\n"
else "\n"
generateSMTBenchmarks :: Provable a => Bool -> FilePath -> a -> IO ()
generateSMTBenchmarks isSat f a = gen False smt1 >> gen True smt2
where smt1 = addExtension f "smt1"
smt2 = addExtension f "smt2"
gen b fn = do s <- compileToSMTLib b isSat a
writeFile fn s
putStrLn $ "Generated SMT benchmark " ++ show fn ++ "."
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
isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool
isVacuousWith config a = do
Result ub us tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic True $ forAll_ a >>= output
case cstr of
[] -> return False
_ -> do let is' = [(EX, i) | (_, i) <- is]
res' = Result ub us tr uic is' cs ts as uis ax asgn cstr [trueSW]
cvt = if useSMTLib2 config then toSMTLib2 else toSMTLib1
SatResult result <- runProofOn cvt config True [] res' >>= callSolver True "Checking Satisfiability.." SatResult config
case result of
Unsatisfiable{} -> return True
Satisfiable{} -> return False
Unknown{} -> error "SBV: isVacuous: Solver returned unknown!"
ProofError _ ls -> error $ "SBV: isVacuous: error encountered:\n" ++ unlines ls
TimeOut _ -> error "SBV: isVacuous: time-out."
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, _, _, usorts, _) <- simulate converter config True [] p
unless (null usorts) $ error $ "SBV.allSat: All-sat calls are not supported in the presence of uninterpreted sorts: " ++ unwords usorts
++ "\n Only 'sat' and 'prove' calls are available when uninterpreted sorts are used."
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 void (forkIO io)
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
type SMTProblem = ( [(Quantifier, NamedSymVar)]
, [(String, UnintKind)]
, [Either SW (SW, [SW])]
, [String]
, SMTLibPgm
)
callSolver :: Bool -> String -> (SMTResult -> b) -> SMTConfig -> SMTProblem -> 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 SMTProblem
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 isSat $ (if isSat then forSome_ else forAll_) predicate >>= output
msg $ "Generated symbolic trace:\n" ++ show res
msg "Translating to SMT-Lib.."
runProofOn converter config isSat comments res
runProofOn :: SMTLibConverter -> SMTConfig -> Bool -> [String] -> Result -> IO SMTProblem
runProofOn converter config isSat comments res =
let isTiming = timing config
solverCaps = capabilities (solver config)
in case res of
Result boundInfo usorts _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW (KBounded False 1) _)] ->
timeIf isTiming "translation" $ let uiMap = mapMaybe 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)
in return (is, uiMap, skolemMap, usorts, converter solverCaps boundInfo isSat comments usorts is skolemMap consts tbls arrs uis axs pgm cstrs o)
Result _boundInfo _us _qcInfo _codeSegs _is _consts _tbls _arrs _uis _axs _pgm _cstrs 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!"
sbvCheckSolverInstallation :: SMTConfig -> IO Bool
sbvCheckSolverInstallation cfg = do ThmResult r <- proveWith cfg $ \x -> (x+x) .== ((x*2) :: SWord8)
case r of
Unsatisfiable _ -> return True
_ -> return False
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)