module Data.SBV.Provers.Prover (
SMTSolver(..), SMTConfig(..), Predicate, Provable(..)
, ThmResult(..), SatResult(..), SafeResult(..), AllSatResult(..), SMTResult(..)
, isSatisfiable, isSatisfiableWith, isTheorem, isTheoremWith
, prove, proveWith
, sat, satWith
, safe, safeWith, isSafe
, allSat, allSatWith
, isVacuous, isVacuousWith
, SatModel(..), Modelable(..), displayModels, extractModels
, getModelDictionaries, getModelValues, getModelUninterpretedValues
, boolector, cvc4, yices, z3, mathSAT, abc, defaultSMTCfg
, compileToSMTLib, generateSMTBenchmarks
, internalSATCheck
) where
import Control.Monad (when, unless)
import Data.List (intercalate)
import System.FilePath (addExtension, splitExtension)
import System.Time (getClockTime)
import System.IO.Unsafe (unsafeInterleaveIO)
import GHC.Stack.Compat
#if !MIN_VERSION_base(4,9,0)
import GHC.SrcLoc.Compat
#endif
import qualified Data.Set as Set (Set, toList)
import Data.SBV.BitVectors.Data
import Data.SBV.SMT.SMT
import Data.SBV.SMT.SMTLib
import Data.SBV.Utils.TDiff
import Control.DeepSeq (rnf)
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 qualified Data.SBV.Provers.ABC as ABC
mkConfig :: SMTSolver -> SMTLibVersion -> [String] -> SMTConfig
mkConfig s smtVersion tweaks = SMTConfig { verbose = False
, timing = NoTiming
, sBranchTimeOut = Nothing
, timeOut = Nothing
, printBase = 10
, printRealPrec = 16
, smtFile = Nothing
, solver = s
, solverTweaks = tweaks
, smtLibVersion = smtVersion
, satCmd = "(check-sat)"
, isNonModelVar = const False
, roundingMode = RoundNearestTiesToEven
, useLogic = Nothing
}
boolector :: SMTConfig
boolector = mkConfig Boolector.boolector SMTLib2 []
cvc4 :: SMTConfig
cvc4 = mkConfig CVC4.cvc4 SMTLib2 []
yices :: SMTConfig
yices = mkConfig Yices.yices SMTLib2 []
z3 :: SMTConfig
z3 = mkConfig Z3.z3 SMTLib2 ["(set-option :smt.mbqi true) ; use model based quantifier instantiation"]
mathSAT :: SMTConfig
mathSAT = mkConfig MathSAT.mathSAT SMTLib2 []
abc :: SMTConfig
abc = mkConfig ABC.abc SMTLib2 []
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, Provable p) => Provable (SArray a b -> p) where
forAll_ k = declNewSArray (\t -> "array_" ++ show t) Nothing >>= \a -> forAll_ $ k a
forAll (s:ss) k = declNewSArray (const 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 (HasKind a, HasKind b, Provable p) => Provable (SFunArray a b -> p) where
forAll_ k = declNewSFunArray Nothing >>= \a -> forAll_ $ k a
forAll (_:ss) k = declNewSFunArray 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 => SMTLibVersion
-> Bool
-> a
-> IO String
compileToSMTLib version isSat a = do
t <- getClockTime
let comments = ["Created on " ++ show t]
cvt = case version of
SMTLib2 -> toSMTLib2
(_, _, _, _, smtLibPgm) <- simulate cvt defaultSMTCfg isSat comments a
let out = show smtLibPgm
return $ out ++ "\n(check-sat)\n"
generateSMTBenchmarks :: Provable a => Bool -> FilePath -> a -> IO ()
generateSMTBenchmarks isSat f a = mapM_ gen [minBound .. maxBound]
where gen v = do s <- compileToSMTLib v isSat a
let fn = f `addExtension` smtLibVersionExtension v
writeFile fn s
putStrLn $ "Generated " ++ show v ++ " 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 = case smtLibVersion config of
SMTLib2 -> toSMTLib2
satWith :: Provable a => SMTConfig -> a -> IO SatResult
satWith config a = simulate cvt config True [] a >>= callSolver True "Checking Satisfiability.." SatResult config
where cvt = case smtLibVersion config of
SMTLib2 -> toSMTLib2
safeWith :: SExecutable a => SMTConfig -> a -> IO [SafeResult]
safeWith cfg a = do
res@Result{resAssertions=asserts} <- runSymbolic (True, cfg) $ sName_ a >>= output
mapM (verify res) asserts
where locInfo (Just ps) = Just $ let loc (f, sl) = concat [srcLocFile sl, ":", show (srcLocStartLine sl), ":", show (srcLocStartCol sl), ":", f]
in intercalate ",\n " (map loc ps)
locInfo _ = Nothing
verify res (msg, cs, cond) = do SatResult result <- runProofOn cvt cfg True [] pgm >>= callSolver True msg SatResult cfg
return $ SafeResult (locInfo (getCallStack `fmap` cs), msg, result)
where pgm = res { resInputs = [(EX, n) | (_, n) <- resInputs res]
, resOutputs = [cond]
}
cvt = case smtLibVersion cfg of
SMTLib2 -> toSMTLib2
isSafe :: SafeResult -> Bool
isSafe (SafeResult (_, _, result)) = case result of
Unsatisfiable{} -> True
Satisfiable{} -> False
Unknown{} -> False
ProofError{} -> False
TimeOut{} -> False
isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool
isVacuousWith config a = do
Result ki tr uic is cs ts as uis ax asgn cstr asserts _ <- runSymbolic (True, 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 asserts [trueSW]
cvt = case smtLibVersion config of
SMTLib2 -> toSMTLib2
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 = case smtLibVersion config of
SMTLib2 -> toSMTLib2
msg "Checking Satisfiability, all solutions.."
sbvPgm@(qinps, _, ki, _, _) <- simulate converter config True [] p
let usorts = [s | us@(KUserSort s _) <- Set.toList ki, isFree us]
where isFree (KUserSort _ (Left _)) = True
isFree _ = False
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 let modelOnlyAssocs = [v | v@(x, _) <- modelAssocs model, not (isNonModelVar config x)]
rest <- unsafeInterleaveIO $ loop (n+1) (modelOnlyAssocs : 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, 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 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)]
, [Either SW (SW, [SW])]
, Set.Set Kind
, [(String, Maybe CallStack, SW)]
, SMTLibPgm
)
callSolver :: Bool -> String -> (SMTResult -> b) -> SMTConfig -> SMTProblem -> IO b
callSolver isSat checkMsg wrap config (qinps, 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 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 ProblemConstruction $ runSymbolic (isSat, 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 assertions [o@(SW KBool _)] ->
timeIf isTiming Translation
$ let 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)
smtScript = converter (roundingMode config) (useLogic config) solverCaps ki isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o
result = (is, skolemMap, ki, assertions, smtScript)
in rnf smtScript `seq` return result
Result{resOutputs = 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!"
internalSATCheck :: SMTConfig -> SBool -> State -> String -> IO SatResult
internalSATCheck cfg condInPath st msg = do
sw <- sbvToSW st condInPath
() <- forceSWArg sw
Result ki tr uic is cs ts as uis ax asgn cstr assertions _ <- extractSymbolicSimulationState st
let
pgm = Result ki tr uic [(EX, n) | (_, n) <- is] cs ts as uis ax asgn cstr assertions [sw]
cvt = case smtLibVersion cfg of
SMTLib2 -> toSMTLib2
runProofOn cvt cfg True [] pgm >>= callSolver True msg SatResult cfg