module Data.SBV.Provers.Prover (
SMTSolver(..), SMTConfig(..), Predicate, Provable(..)
, ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..), SafeResult(..)
, isSatisfiable, isSatisfiableWith, isTheorem, isTheoremWith
, prove, proveWith
, sat, satWith
, safe, safeWith
, allSat, allSatWith
, isVacuous, isVacuousWith
, SatModel(..), Modelable(..), displayModels, extractModels
, getModelDictionaries, getModelValues, getModelUninterpretedValues
, boolector, cvc4, yices, z3, mathSAT, defaultSMTCfg
, compileToSMTLib, generateSMTBenchmarks
, isSBranchFeasibleInState
, isConditionSatisfiable
) where
import Control.Monad (when, unless)
import Control.Monad.Trans (liftIO)
import Data.List (intercalate)
import Data.Maybe (mapMaybe, fromMaybe, isJust)
import System.FilePath (addExtension, splitExtension)
import System.Time (getClockTime)
import System.IO.Unsafe (unsafeInterleaveIO)
import qualified Data.Set as Set (Set, toList)
import qualified Control.Exception as C
import Data.SBV.BitVectors.Data
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 qualified Data.SBV.Provers.MathSAT as MathSAT
import Data.SBV.Utils.TDiff
mkConfig :: SMTSolver -> Bool -> [String] -> SMTConfig
mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False
, timing = False
, sBranchTimeOut = Nothing
, timeOut = Nothing
, printBase = 10
, printRealPrec = 16
, smtFile = Nothing
, solver = s
, solverTweaks = tweaks
, useSMTLib2 = isSMTLib2
, satCmd = "(check-sat)"
, roundingMode = RoundNearestTiesToEven
, useLogic = Nothing
}
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"]
mathSAT :: SMTConfig
mathSAT = mkConfig MathSAT.mathSAT True []
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
safe :: SExecutable a => a -> IO SafeResult
safe = safeWith defaultSMTCfg
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
safeWith :: SExecutable a => SMTConfig -> a -> IO SafeResult
safeWith config a = C.catchJust choose checkSafe return
where checkSafe = do let msg = when (verbose config) . putStrLn . ("** " ++)
isTiming = timing config
msg "Starting safety checking symbolic simulation.."
res <- timeIf isTiming "problem construction" $ runSymbolic (False, Just config) $ sName_ a >>= output
msg $ "Generated symbolic trace:\n" ++ show res
return SafeNeverFails
choose e@(SafeNeverFails{}) = Just e
choose e@(SafeAlwaysFails{}) = Just e
choose e@(SafeFailsInModel{}) = Just e
isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool
isVacuousWith config a = do
Result ki tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic (True, Just config) $ forAll_ a >>= output
case cstr of
[] -> return False
_ -> do let is' = [(EX, i) | (_, i) <- is]
res' = Result ki 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, _, _, ki, _) <- simulate converter config True [] p
let usorts = [s | KUninterpreted s <- Set.toList ki]
unless (null usorts) $ msg $ "SBV.allSat: Uninterpreted sorts present: " ++ unwords usorts
++ "\n SBV will use equivalence classes to generate all-satisfying instances."
results <- unsafeInterleaveIO $ go sbvPgm (1::Int) []
let w = ALL `elem` map fst qinps
return $ AllSatResult (w, results)
where msg = when (verbose config) . putStrLn . ("** " ++)
go sbvPgm = loop
where loop !n nonEqConsts = do
curResult <- invoke nonEqConsts n sbvPgm
case curResult of
Nothing -> return []
Just (SatResult r) -> let cont model = do rest <- unsafeInterleaveIO $ loop (n+1) (modelAssocs model : nonEqConsts)
return (r : rest)
in case r of
Satisfiable _ (SMTModel [] _ _) -> return [r]
Unknown _ (SMTModel [] _ _) -> return [r]
ProofError _ _ -> return [r]
TimeOut _ -> return []
Unsatisfiable _ -> return []
Satisfiable _ model -> cont model
Unknown _ model -> cont model
invoke nonEqConsts n (qinps, modelMap, skolemMap, _, smtLibPgm) = do
msg $ "Looking for solution " ++ show n
case addNonEqConstraints (roundingMode config) qinps nonEqConsts smtLibPgm of
Nothing ->
return Nothing
Just finalPgm -> do msg $ "Generated SMTLib program:\n" ++ finalPgm
smtAnswer <- engine (solver config) (updateName (n1) config) True qinps modelMap skolemMap finalPgm
msg "Done.."
return $ Just $ SatResult smtAnswer
updateName i cfg = cfg{smtFile = upd `fmap` smtFile cfg}
where upd nm = let (b, e) = splitExtension nm in b ++ "_allSat_" ++ show i ++ e
type SMTProblem = ( [(Quantifier, NamedSymVar)]
, [(String, UnintKind)]
, [Either SW (SW, [SW])]
, Set.Set Kind
, 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, Just config) $ (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 ki _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW KBool _)] ->
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, ki, converter (roundingMode config) (useLogic config) solverCaps ki isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o)
Result _kindInfo _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!"
isSBranchFeasibleInState :: State -> String -> SBool -> IO Bool
isSBranchFeasibleInState st branch cond = do
let cfg = let pickedConfig = fromMaybe defaultSMTCfg (getSBranchRunConfig st)
in pickedConfig { timeOut = sBranchTimeOut pickedConfig }
msg = when (verbose cfg) . putStrLn . ("** " ++)
check <- internalSATCheck cfg st cond ("sBranch: Checking " ++ show branch ++ " feasibility")
res <- case check of
SatResult (Unsatisfiable _) -> return False
_ -> return True
msg $ "sBranch: Conclusion: " ++ if res then "Feasible" else "Unfeasible"
return res
isConditionSatisfiable :: State -> SBool -> IO (Maybe SatResult)
isConditionSatisfiable st cond = do
let cfg = fromMaybe defaultSMTCfg (getSBranchRunConfig st)
msg = when (verbose cfg) . putStrLn . ("** " ++)
check <- internalSATCheck cfg st cond "sAssert: Checking satisfiability"
res <- case check of
r@(SatResult (Satisfiable{})) -> return $ Just r
SatResult (Unsatisfiable _) -> return Nothing
_ -> error $ "sAssert: Unexpected external result: " ++ show check
msg $ "sAssert: Conclusion: " ++ if isJust res then "Satisfiable" else "Unsatisfiable"
return res
internalSATCheck :: SMTConfig -> State -> SBool -> String -> IO SatResult
internalSATCheck cfg st cond msg = do
sw <- sbvToSW st cond
() <- forceSWArg sw
Result ki tr uic is cs ts as uis ax asgn cstr _ <- liftIO $ extractSymbolicSimulationState st
let
pgm = Result ki tr uic [(EX, n) | (_, n) <- is] cs ts as uis ax asgn cstr [sw]
cvt = if useSMTLib2 cfg then toSMTLib2 else toSMTLib1
runProofOn cvt cfg True [] pgm >>= callSolver True msg SatResult cfg