GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 13:01:31 +03:00
Code Issues Projects Releases Wiki Activity

Pass 'verbose' flag through to SBV for :prove and :sat

Browse Source 
This addresses issue #17.
This commit is contained in:
Brian Huffman 2014-09-26 11:56:32 -07:00
parent e9642e5809
commit 840e99f563
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/Cryptol/Symbolic.hs
View File

@ -86,12 +86,13 @@ satProve isSat (proverName, useSolverIte, verbose) edecls mfile (expr, schema) =
case proverName of case proverName of
"any" -> SBV.sbvAvailableSolvers "any" -> SBV.sbvAvailableSolvers
_ -> return [(lookupProver proverName) { smtFile = mfile }] _ -> return [(lookupProver proverName) { smtFile = mfile }]
let provers' = [ p { SBV.timing = verbose, SBV.verbose = verbose } | p <- provers ]
let tyFn = if isSat then existsFinType else forallFinType let tyFn = if isSat then existsFinType else forallFinType
let runProver fn tag e = do let runProver fn tag e = do
when verbose $ liftIO $ when verbose $ liftIO $
putStrLn $ "Trying proof with " ++ putStrLn $ "Trying proof with " ++
intercalate ", " (map show provers) intercalate ", " (map show provers)
(firstProver, res) <- fn provers e (firstProver, res) <- fn provers' e
when verbose $ liftIO $ when verbose $ liftIO $
putStrLn $ "Got result from " ++ show firstProver putStrLn $ "Got result from " ++ show firstProver
return (tag res) return (tag res)