module Language.Fixpoint.Smt.Interface (
Command (..)
, Response (..)
, SMTLIB2 (..)
, Context (..)
, makeContext
, makeContextNoLog
, cleanupContext
, command
, smtWrite
, smtDecl
, smtAssert
, smtCheckUnsat
, smtBracket
, smtDistinct
, theorySymbols
) where
import Language.Fixpoint.Config (SMTSolver (..))
import Language.Fixpoint.Errors
import Language.Fixpoint.Files
import Language.Fixpoint.Types
import Language.Fixpoint.Smt.Types
import Language.Fixpoint.Smt.Theories
import Language.Fixpoint.Smt.Serialize
import Control.Applicative ((*>), (<$>), (<*), (<|>))
import Control.Monad
import Data.Char
import qualified Data.HashMap.Strict as M
import qualified Data.List as L
import Data.Monoid
import qualified Data.Text as T
import Data.Text.Format
import qualified Data.Text.IO as TIO
import qualified Data.Text.Lazy as LT
import qualified Data.Text.Lazy.IO as LTIO
import System.Directory
import System.Exit hiding (die)
import System.FilePath
import System.IO (Handle, IOMode (..), hClose, hFlush,
openFile)
import System.Process
import qualified Data.Attoparsec.Text as A
command :: Context -> Command -> IO Response
command me !cmd = say me cmd >> hear me cmd
where
say me = smtWrite me . smt2
hear me CheckSat = smtRead me
hear me (GetValue _) = smtRead me
hear me _ = return Ok
smtWrite :: Context -> LT.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 -> error e
Right r -> do
maybe (return ()) (\h -> hPutStrLnNow h $ format "; SMT Says: {}" (Only $ show r)) (cLog me)
when (verbose me) $
LTIO.putStrLn $ format "SMT Says: {}" (Only $ show r)
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 <> ")"
pairs :: [a] -> [(a,a)]
pairs !xs = case L.splitAt 2 xs of
([],b) -> []
([x,y], zs) -> (x,y) : pairs zs
smtWriteRaw :: Context -> LT.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 = LTIO.hPutStrLn h s >> hFlush h
makeContext :: SMTSolver -> FilePath -> IO Context
makeContext s f
= do me <- makeProcess s
pre <- smtPreamble 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
makeContextNoLog s
= do me <- makeProcess s
pre <- smtPreamble s me
mapM_ (smtWrite me) pre
return me
makeProcess s
= do (hOut, hIn, _ ,pid) <- runInteractiveCommand $ smtCmd s
return $ Ctx pid hIn hOut Nothing False
cleanupContext :: Context -> IO ExitCode
cleanupContext me@(Ctx {..})
= do smtWrite me "(exit)"
code <- waitForProcess pId
hClose cIn
hClose cOut
maybe (return ()) hClose cLog
return code
smtCmd Z3 = "z3 -smt2 -in"
smtCmd Mathsat = "mathsat -input=smt2"
smtCmd Cvc4 = "cvc4 --incremental -L smtlib2"
smtPreamble 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 ++ z3Preamble
else return $ z3_options ++ z3Preamble
smtPreamble _ _
= return smtlibPreamble
versionGreater (x:xs) (y:ys)
| x > y = True
| x == y = versionGreater xs ys
| x < y = False
versionGreater xs [] = True
versionGreater [] ys = False
smtPush, smtPop :: Context -> IO ()
smtPush me = interact' me Push
smtPop me = interact' me Pop
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 )
smtAssert :: Context -> Pred -> 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 $ "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)" ]