|
definition:
|
checkUnsatWithSMT :: Options -> QName -> String -> IORef ProgInfo
-> [(QName,ConsInfo)]
-> [(Int,TypeExpr)] -> [(Int,Sort)]
-> Term -> [QName] -> [QName] -> IO (Maybe Bool)
checkUnsatWithSMT opts qf title pistore consinfos vartypes
extravars -- variables representing h.o. subexps
assertion -- assertion to be checked
assertioncons -- constructors occurring in the assertion
assertfuncs = -- defined functions occurring in assertion
flip catch (\e -> print e >> return Nothing) $ do
--let allsyms = nub (catMaybes
-- (map (\n -> maybe Nothing Just (untransOpName n))
-- (map qidName (allQIdsOfTerm assertion))))
unless (null assertfuncs) $ printWhenDetails opts $
"Translating operations into SMT: " ++ unwords (map showQName assertfuncs)
fdecls0 <- getAllFunctions opts pistore assertfuncs
pinfos <- fmap progInfos $ readIORef pistore
let fdecls1 = addTypes2FuncDecls pinfos
(map (completeBranchesInFunc consinfos True) fdecls0)
-- reduce to functions reachable from assertion after eliminating h.o.:
fdecls = usedFunctions assertfuncs
(map (updFuncBody replaceHigherOrderInExp) fdecls1)
--printInfoLine $ "OPERATIONS TO BE TRANSLATED:\n" ++ unlines (map showFuncDecl fdecls)
let smtfuncs = maybe (Comment $ "ERROR translating " ++
show (map funcName fdecls))
(\fds -> DefineSigsRec fds)
(mapM fun2SMT fdecls)
fdecltvars = nub (concatMap allTVarsInFuncDecl fdecls)
--printInfoLine $ "TRANSLATED FUNCTIONS:\n" ++ pPrint (pretty smtfuncs)
--let title1 = title ++ "\nTRANSLATED FUNCTIONS:\n" ++ pPrint (pretty smtfuncs)
let vartypestcons = foldr union [] (map (tconsOfTypeExpr . snd) vartypes)
funcstcons = foldr union [] (map (tconsOfTypeExpr . funcType) fdecls)
asserttcons = map (\(ConsType _ tc _) -> tc)
(map (snd3 . infoOfCons consinfos) assertioncons)
(primtypes,usertypes) =
partition ((== "Prelude") . fst)
(union funcstcons (union vartypestcons asserttcons))
decls <- mapM (getTypeDeclOf pistore) usertypes
-- collect all type parameters in order to declare them as sorts:
let tvarsInVars = foldr union []
(map (typeParamsOfSort . type2sort)
(map snd vartypes ++ map TVar fdecltvars))
varsorts = map (\(i,te) -> (i, type2sort te)) vartypes ++ extravars
--printInfoLine $ "Assertion: " ++ pPrint (pretty assertion)
let smt = concatMap preludeType2SMT (map snd primtypes) ++
[ EmptyLine ] ++
(if null decls
then []
else [ Comment "User-defined datatypes:" ] ++
map tdecl2SMT decls) ++
(if null tvarsInVars
then []
else [ EmptyLine, Comment "Polymorphic sorts:" ] ++
map (\tv -> DeclareSort tv 0) tvarsInVars) ++
[ EmptyLine, smtfuncs, EmptyLine
, Comment "Free variables:" ] ++
map (\(i,s) -> DeclareVar (SV i s)) varsorts ++
[ EmptyLine
, Comment "Boolean formula of assertion (known properties):"
, sAssert assertion, EmptyLine
, Comment "check satisfiability:"
, CheckSat
]
--printInfoLine $ "SMT commands as Curry term:\n" ++ show smt
let preludesmt = if all ((`elem` defaultSMTTypes) . snd) primtypes
then "Prelude_min.smt"
else "Prelude.smt"
smtprelude <- readIncludeFile preludesmt
let scripttitle = unlines (map ("; "++) (lines title))
printWhenAll opts $
"RAW SMT SCRIPT:\n" ++ scripttitle ++ "\n\n" ++ showSMTRaw smt
let smtinput = scripttitle ++ "\n" ++ smtprelude ++ showSMT smt
printWhenDetails opts $ "SMT SCRIPT:\n" ++ showWithLineNums smtinput
let z3opts = ["-smt2", "-T:2"]
when (optStoreSMT opts) (storeSMT "SMT-" z3opts smtinput >> return ())
printWhenDetails opts $
"CALLING Z3 (with options: " ++ unwords z3opts ++ ")..."
(ecode,out,err) <- evalCmd "z3" ("-in" : z3opts) smtinput
when (ecode > 0) $ do
printWhenStatus opts $ "EXIT CODE: " ++ show ecode
outfile <- storeSMT "smterror-" z3opts smtinput
when (optVerb opts < 3) $ printWhenStatus opts $
"ERROR in SMT script (saved in '" ++ outfile ++ "'):\n" ++
out ++ "\n" ++ err
printWhenDetails opts $ "RESULT:\n" ++ out
unless (null err) $ printWhenDetails opts $ "ERROR:\n" ++ err
let pcvalid = let ls = lines out in not (null ls) && head ls == "unsat"
return (if ecode>0 then Nothing else Just pcvalid)
where
defaultSMTTypes = ["Int","Float","Bool", "Char", "[]"]
storeSMT fileprefix z3opts script = do
ctime <- getCPUTime
let outfile = fileprefix ++ transOpName qf ++ "-" ++ show ctime ++ ".smt"
execcmt = unwords $ ["; Run with: z3"] ++ z3opts ++ [outfile]
writeFile outfile (execcmt ++ "\n\n" ++ script)
return outfile
|
|
iotype:
|
{(_,_,_,_,_,_,_,_,_,_) |-> _}
|
|
signature:
|
Verify.Options.Options -> (String, String) -> String
-> Data.IORef.IORef Verify.ProgInfo.ProgInfo
-> [((String, String), (Prelude.Int, Verify.ProgInfo.ConsType, [((String, String), Prelude.Int)]))]
-> [(Prelude.Int, FlatCurry.Types.TypeExpr)]
-> [(Prelude.Int, Verify.ESMT.Sort)] -> Verify.ESMT.Term -> [(String, String)]
-> [(String, String)] -> Prelude.IO (Prelude.Maybe Prelude.Bool)
|