|
definition:
|
checkImplicationWithSMT :: Options -> IORef VState -> String -> [(Int,TypeExpr)]
-> Term -> Term -> Term -> IO (Maybe Bool)
checkImplicationWithSMT opts vstref scripttitle vartypes
assertion impbindings imp = do
let (pretypes,usertypes) =
partition ((== "Prelude") . fst)
(foldr union [] (map (tconsOfTypeExpr . snd) vartypes))
vst <- readIORef vstref
let allsyms = catMaybes
(map (\n -> maybe Nothing Just (untransOpName n))
(map qidName
(allQIdsOfTerm (tConj [assertion, impbindings, imp]))))
unless (null allsyms) $ printWhenIntermediate opts $
"Translating operations into SMT: " ++
unwords (map showQName allsyms)
smtfuncs <- funcs2SMT vstref allsyms
let decls = map (maybe (error "Internal error: some datatype not found!") id)
(map (tdeclOf vst) usertypes)
smt = concatMap preludeType2SMT (map snd pretypes) ++
[ EmptyLine ] ++
(if null decls
then []
else [ Comment "User-defined datatypes:" ] ++
map tdecl2SMT decls) ++
[ EmptyLine, smtfuncs, EmptyLine
, Comment "Free variables:" ] ++
map typedVar2SMT vartypes ++
[ EmptyLine
, Comment "Boolean formula of assertion (known properties):"
, sAssert assertion, EmptyLine
, Comment "Bindings of implication:"
, sAssert impbindings, EmptyLine
, Comment "Assert negated implication:"
, sAssert (tNot imp), EmptyLine
, Comment "check satisfiability:"
, CheckSat
, Comment "if unsat, the implication is valid"
]
--putStrLn $ "SMT commands as Curry term:\n" ++ show smt
smtprelude <- readFile (packagePath </> "include" </> "Prelude.smt")
let smtinput = "; " ++ scripttitle ++ "\n\n" ++ smtprelude ++ showSMT smt
printWhenAll opts $ "SMT SCRIPT:\n" ++ showWithLineNums smtinput
printWhenAll opts $ "CALLING Z3 (with options: -smt2 -T:5)..."
(ecode,out,err) <- evalCmd "z3" ["-smt2", "-in", "-T:5"] smtinput
when (ecode>0) $ do printWhenAll opts $ "EXIT CODE: " ++ show ecode
writeFile "error.smt" smtinput
printWhenAll opts $ "RESULT:\n" ++ out
unless (null err) $ printWhenAll 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)
|