module Language.Fixpoint.Smt.Interface (
Command (..)
, Response (..)
, SMTLIB2 (..)
, Context (..)
, makeContext
, makeContextNoLog
, makeContextWithSEnv
, cleanupContext
, command
, smtWrite
, smtDecl
, smtDecls
, smtAssert
, smtAssertAxiom
, smtCheckUnsat
, smtCheckSat
, smtBracket
, smtDistinct
, smtPush, smtPop
, checkValid
, checkValid'
, checkValidWithContext
, checkValids
, makeSmtContext
) where
import Language.Fixpoint.Types.Config ( SMTSolver (..)
, Config
, solver
, extensionality
, alphaEquivalence
, betaEquivalence
, normalForm
, stringTheory)
import Language.Fixpoint.Misc (errorstar)
import Language.Fixpoint.Types.Errors
import Language.Fixpoint.Utils.Files
import Language.Fixpoint.Types hiding (allowHO)
import Language.Fixpoint.Smt.Types
import qualified Language.Fixpoint.Smt.Theories as Thy
import Language.Fixpoint.Smt.Serialize ()
import Control.Applicative ((<|>))
import Control.Monad
import Control.Exception
import Data.Char
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.Builder as Builder
import qualified Data.Text.Lazy.IO as LTIO
import System.Directory
import System.Console.CmdArgs.Verbosity
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
import qualified Data.HashMap.Strict as M
import Data.Attoparsec.Internal.Types (Parser)
import Text.PrettyPrint.HughesPJ (text)
makeSmtContext :: Config -> FilePath -> [(Symbol, Sort)] -> IO Context
makeSmtContext cfg f xts = do
me <- makeContextWithSEnv cfg f $ fromListSEnv xts
smtDecls me theoryDecls
smtDecls me xts
return me
theoryDecls :: [(Symbol, Sort)]
theoryDecls = [ (x, tsSort ty) | (x, ty) <- M.toList Thy.theorySymbols, not (tsInterp ty)]
checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValidWithContext me xts p q =
smtBracket me "checkValidWithContext" $
checkValid' me xts p q
checkValid :: Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid cfg f xts p q = do
me <- makeContext cfg f
checkValid' me xts p q
checkValid' :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' me xts p q = do
smtDecls me xts
smtAssert me $ pAnd [p, PNot q]
smtCheckUnsat me
checkValids :: Config -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]
checkValids cfg f xts ps
= do me <- makeContext cfg f
smtDecls me xts
forM ps $ \p ->
smtBracket me "checkValids" $
smtAssert me (PNot p) >> smtCheckUnsat me
command :: Context -> Command -> IO Response
command me !cmd = say cmd >> hear cmd
where
say = smtWrite me . Builder.toLazyText . runSmt2
hear CheckSat = smtRead me
hear (GetValue _) = smtRead me
hear _ = return Ok
smtWrite :: Context -> Raw -> 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)) (ctxLog me)
return r
type SmtParser a = Parser T.Text a
responseP :: SmtParser Response
responseP = A.char '(' *> sexpP
<|> A.string "sat" *> return Sat
<|> A.string "unsat" *> return Unsat
<|> A.string "unknown" *> return Unknown
sexpP :: SmtParser Response
sexpP = A.string "error" *> (Error <$> errorP)
<|> Values <$> valuesP
errorP :: SmtParser T.Text
errorP = A.skipSpace *> A.char '"' *> A.takeWhile1 (/='"') <* A.string "\")"
valuesP :: SmtParser [(Symbol, T.Text)]
valuesP = A.many1' pairP <* A.char ')'
pairP :: SmtParser (Symbol, T.Text)
pairP =
do A.skipSpace
A.char '('
!x <- symbolP
A.skipSpace
!v <- valueP
A.char ')'
return (x,v)
symbolP :: SmtParser Symbol
symbolP = symbol <$> A.takeWhile1 (not . isSpace)
valueP :: SmtParser T.Text
valueP = negativeP
<|> A.takeWhile1 (\c -> not (c == ')' || isSpace c))
negativeP :: SmtParser T.Text
negativeP
= do v <- A.char '(' *> A.takeWhile1 (/=')') <* A.char ')'
return $ "(" <> v <> ")"
smtWriteRaw :: Context -> Raw -> IO ()
smtWriteRaw me !s = do
hPutStrLnNow (ctxCout me) s
maybe (return ()) (`hPutStrLnNow` s) (ctxLog me)
smtReadRaw :: Context -> IO T.Text
smtReadRaw me = TIO.hGetLine (ctxCin me)
hPutStrLnNow :: Handle -> LT.Text -> IO ()
hPutStrLnNow h !s = LTIO.hPutStrLn h s >> hFlush h
makeContext :: Config -> FilePath -> IO Context
makeContext cfg f
= do me <- makeProcess cfg
pre <- smtPreamble cfg (solver cfg) me
createDirectoryIfMissing True $ takeDirectory smtFile
hLog <- openFile smtFile WriteMode
let me' = me { ctxLog = Just hLog }
mapM_ (smtWrite me') pre
return me'
where
smtFile = extFileName Smt2 f
makeContextWithSEnv :: Config -> FilePath -> SMTEnv -> IO Context
makeContextWithSEnv cfg f env
= (\cxt -> cxt {ctxSmtEnv = env}) <$> makeContext cfg f
makeContextNoLog :: Config -> IO Context
makeContextNoLog cfg
= do me <- makeProcess cfg
pre <- smtPreamble cfg (solver cfg) me
mapM_ (smtWrite me) pre
return me
makeProcess :: Config -> IO Context
makeProcess cfg
= do (hOut, hIn, _ ,pid) <- runInteractiveCommand $ smtCmd (solver cfg)
loud <- isLoud
return Ctx { ctxPid = pid
, ctxCin = hIn
, ctxCout = hOut
, ctxLog = Nothing
, ctxVerbose = loud
, ctxExt = extensionality cfg
, ctxAeq = alphaEquivalence cfg
, ctxBeq = betaEquivalence cfg
, ctxNorm = normalForm cfg
, ctxSmtEnv = Thy.theorySEnv
}
cleanupContext :: Context -> IO ExitCode
cleanupContext (Ctx {..}) = do
hCloseMe "ctxCin" ctxCin
hCloseMe "ctxCout" ctxCout
maybe (return ()) (hCloseMe "ctxLog") ctxLog
waitForProcess ctxPid
hCloseMe :: String -> Handle -> IO ()
hCloseMe msg h = hClose h `catch` (\(exn :: IOException) -> putStrLn $ "OOPS, hClose breaks: " ++ msg ++ show exn)
smtCmd :: SMTSolver -> String
smtCmd Z3 = "z3 -smt2 -in"
smtCmd Mathsat = "mathsat -input=smt2"
smtCmd Cvc4 = "cvc4 --incremental -L smtlib2"
smtPreamble :: Config -> SMTSolver -> Context -> IO [LT.Text]
smtPreamble cfg Z3 me
= do smtWrite me "(get-info :version)"
v:_ <- T.words . (!!1) . T.splitOn "\"" <$> smtReadRaw me
checkValidStringFlag Z3 v cfg
if T.splitOn "." v `versionGreaterEq` ["4", "3", "2"]
then return $ z3_432_options ++ makeMbqi cfg ++ Thy.preamble cfg Z3
else return $ z3_options ++ makeMbqi cfg ++ Thy.preamble cfg Z3
smtPreamble cfg s _
= checkValidStringFlag s "" cfg >> return (Thy.preamble cfg s)
checkValidStringFlag :: SMTSolver -> T.Text -> Config -> IO ()
checkValidStringFlag smt v cfg
= when (noString smt v cfg) $
die $ err dummySpan (text "stringTheory is only supported by z3 version >=4.2.2")
noString :: SMTSolver -> T.Text -> Config -> Bool
noString smt v cfg
= stringTheory cfg
&& not (smt == Z3 && (T.splitOn "." v `versionGreaterEq` ["4", "4", "2"]))
versionGreaterEq :: Ord a => [a] -> [a] -> Bool
versionGreaterEq (x:xs) (y:ys)
| x > y = True
| x == y = versionGreaterEq xs ys
| x < y = False
versionGreaterEq _ [] = True
versionGreaterEq [] _ = False
versionGreaterEq _ _ = 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 = mapM_ . uncurry . smtDecl
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)
smtAssertAxiom :: Context -> Triggered Expr -> IO ()
smtAssertAxiom me p = interact' me (AssertAxiom p)
smtDistinct :: Context -> [Expr] -> IO ()
smtDistinct me az = interact' me (Distinct az)
smtCheckUnsat :: Context -> IO Bool
smtCheckUnsat me = respSat <$> command me CheckSat
smtBracket :: Context -> String -> IO a -> IO a
smtBracket me _msg a = do
smtPush me
r <- a
smtPop me
return r
respSat :: Response -> Bool
respSat Unsat = True
respSat Sat = False
respSat Unknown = False
respSat r = die $ err dummySpan $ text ("crash: SMTLIB2 respSat = " ++ show r)
interact' :: Context -> Command -> IO ()
interact' me cmd = void $ command me cmd
makeMbqi :: Config -> [LT.Text]
makeMbqi cfg
| extensionality cfg = [""]
| otherwise = ["\n(set-option :smt.mbqi false)"]
z3_432_options :: [LT.Text]
z3_432_options
= [ "(set-option :auto-config false)"
, "(set-option :model true)"
, "(set-option :model.partial false)"]
z3_options :: [LT.Text]
z3_options
= [ "(set-option :auto-config false)"
, "(set-option :model true)"
, "(set-option :model-partial false)"]