module Language.Fixpoint.Smt.Interface (
Command (..)
, Response (..)
, SMTLIB2 (..)
, Context (..)
, makeContext
, makeContextNoLog
, makeContextWithSEnv
, cleanupContext
, command
, smtWrite
, smtDecl
, smtAssert
, smtCheckUnsat
, smtCheckSat
, smtBracket
, smtDistinct
, checkValid, checkValidWithContext
, checkValids
, makeZ3Context
) where
import Language.Fixpoint.Types.Config (SMTSolver (..))
import Language.Fixpoint.Misc (errorstar)
import Language.Fixpoint.Types.Errors
import Language.Fixpoint.Utils.Files
import Language.Fixpoint.Types
import Language.Fixpoint.Smt.Types
import Language.Fixpoint.Smt.Theories (preamble)
import Language.Fixpoint.Smt.Serialize (initSMTEnv)
import Control.Applicative ((<|>))
import Control.Monad
import Data.Char
import Data.Monoid
import qualified Data.Text as T
import Data.Text.Format hiding (format)
import qualified Data.Text.IO as TIO
import System.Directory
import System.Console.CmdArgs.Verbosity
import System.Exit hiding (die)
import System.FilePath
import System.IO (IOMode (..), hClose, hFlush, openFile)
import System.Process
import qualified Data.Attoparsec.Text as A
import Text.PrettyPrint.HughesPJ (text)
makeZ3Context :: FilePath -> [(Symbol, Sort)] -> IO Context
makeZ3Context f xts
= do me <- makeContextWithSEnv False Z3 f $ fromListSEnv xts
smtDecls me (toListSEnv initSMTEnv)
smtDecls me xts
return me
checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValidWithContext me xts p q
= smtBracket me $ do smtDecls me xts
smtAssert me $ pAnd [p, PNot q]
smtCheckUnsat me
checkValid :: Bool -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid u f xts p q
= do me <- makeContext u Z3 f
smtDecls me xts
smtAssert me $ pAnd [p, PNot q]
smtCheckUnsat me
checkValids :: Bool -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]
checkValids u f xts ps
= do me <- makeContext u Z3 f
smtDecls me xts
forM ps $ \p ->
smtBracket me $
smtAssert me (PNot p) >> smtCheckUnsat me
command :: Context -> Command -> IO Response
command me !cmd = say cmd >> hear cmd
where
say = smtWrite me . runSmt2 (smtenv me)
hear CheckSat = smtRead me
hear (GetValue _) = smtRead me
hear _ = return Ok
smtWrite :: Context -> T.Text -> IO ()
smtWrite me !s = smtWriteRaw me s
smtRead :: Context -> IO Response
smtRead me =
do ln <- smtReadRaw me
res <- A.parseWith (smtReadRaw me) responseP ln
case A.eitherResult res of
Left e -> errorstar $ "SMTREAD:" ++ e
Right r -> do
maybe (return ()) (\h -> hPutStrLnNow h $ format "; SMT Says: {}" (Only $ show r)) (cLog me)
return r
responseP = A.char '(' *> sexpP
<|> A.string "sat" *> return Sat
<|> A.string "unsat" *> return Unsat
<|> A.string "unknown" *> return Unknown
sexpP = A.string "error" *> (Error <$> errorP)
<|> Values <$> valuesP
errorP = A.skipSpace *> A.char '"' *> A.takeWhile1 (/='"') <* A.string "\")"
valuesP = A.many1' pairP <* A.char ')'
pairP =
do A.skipSpace
A.char '('
!x <- symbolP
A.skipSpace
!v <- valueP
A.char ')'
return (x,v)
symbolP = symbol <$> A.takeWhile1 (not . isSpace)
valueP = negativeP
<|> A.takeWhile1 (\c -> not (c == ')' || isSpace c))
negativeP
= do v <- A.char '(' *> A.takeWhile1 (/=')') <* A.char ')'
return $ "(" <> v <> ")"
smtWriteRaw :: Context -> T.Text -> IO ()
smtWriteRaw me !s = do
hPutStrLnNow (cOut me) s
maybe (return ()) (`hPutStrLnNow` s) (cLog me)
smtReadRaw :: Context -> IO Raw
smtReadRaw me = TIO.hGetLine (cIn me)
hPutStrLnNow h !s = TIO.hPutStrLn h s >> hFlush h
makeContext :: Bool -> SMTSolver -> FilePath -> IO Context
makeContext u s f
= do me <- makeProcess s
pre <- smtPreamble u s me
createDirectoryIfMissing True $ takeDirectory smtFile
hLog <- openFile smtFile WriteMode
let me' = me { cLog = Just hLog }
mapM_ (smtWrite me') pre
return me'
where
smtFile = extFileName Smt2 f
makeContextWithSEnv :: Bool -> SMTSolver -> FilePath -> SMTEnv -> IO Context
makeContextWithSEnv u s f env
= (\cxt -> cxt {smtenv = env}) <$> makeContext u s f
makeContextNoLog :: Bool -> SMTSolver -> IO Context
makeContextNoLog u s
= do me <- makeProcess s
pre <- smtPreamble u s me
mapM_ (smtWrite me) pre
return me
makeProcess :: SMTSolver -> IO Context
makeProcess s
= do (hOut, hIn, _ ,pid) <- runInteractiveCommand $ smtCmd s
loud <- isLoud
return Ctx { pId = pid
, cIn = hIn
, cOut = hOut
, cLog = Nothing
, verbose = loud
, smtenv = initSMTEnv
}
cleanupContext :: Context -> IO ExitCode
cleanupContext (Ctx {..})
= do hClose cIn
hClose cOut
maybe (return ()) hClose cLog
waitForProcess pId
smtCmd Z3 = "z3 -smt2 -in"
smtCmd Mathsat = "mathsat -input=smt2"
smtCmd Cvc4 = "cvc4 --incremental -L smtlib2"
smtPreamble u Z3 me
= do smtWrite me "(get-info :version)"
v:_ <- T.words . (!!1) . T.splitOn "\"" <$> smtReadRaw me
if T.splitOn "." v `versionGreater` ["4", "3", "2"]
then return $ z3_432_options ++ preamble u Z3
else return $ z3_options ++ preamble u Z3
smtPreamble u s _
= return $ preamble u s
versionGreater (x:xs) (y:ys)
| x > y = True
| x == y = versionGreater xs ys
| x < y = False
versionGreater _ [] = True
versionGreater [] _ = False
versionGreater _ _ = errorstar "Interface.versionGreater called with bad arguments"
smtPush, smtPop :: Context -> IO ()
smtPush me = interact' me Push
smtPop me = interact' me Pop
smtDecls :: Context -> [(Symbol, Sort)] -> IO ()
smtDecls me xts = forM_ xts (\(x,t) -> smtDecl me x t)
smtDecl :: Context -> Symbol -> Sort -> IO ()
smtDecl me x t = interact' me (Declare x ins out)
where
(ins, out) = deconSort t
deconSort :: Sort -> ([Sort], Sort)
deconSort t = case functionSort t of
Just (_, ins, out) -> (ins, out)
Nothing -> ([] , t )
smtCheckSat :: Context -> Expr -> IO Bool
smtCheckSat me p
= smtAssert me p >> (ans <$> command me CheckSat)
where
ans Sat = True
ans _ = False
smtAssert :: Context -> Expr -> IO ()
smtAssert me p = interact' me (Assert Nothing p)
smtDistinct :: Context -> [Expr] -> IO ()
smtDistinct me az = interact' me (Distinct az)
smtCheckUnsat :: Context -> IO Bool
smtCheckUnsat me = respSat <$> command me CheckSat
smtBracket :: Context -> IO a -> IO a
smtBracket me a = do smtPush me
r <- a
smtPop me
return r
respSat Unsat = True
respSat Sat = False
respSat Unknown = False
respSat r = die $ err dummySpan $ text ("crash: SMTLIB2 respSat = " ++ show r)
interact' me cmd = void $ command me cmd
z3_432_options
= [ "(set-option :auto-config false)"
, "(set-option :model true)"
, "(set-option :model.partial false)"
, "(set-option :smt.mbqi false)" ]
z3_options
= [ "(set-option :auto-config false)"
, "(set-option :model true)"
, "(set-option :model-partial false)"
, "(set-option :mbqi false)" ]