liquid-fixpoint-0.4.0.0: src/Language/Fixpoint/Smt/Interface.hs
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE UndecidableInstances #-}
-- | This module contains an SMTLIB2 interface for
-- 1. checking the validity, and,
-- 2. computing satisfying assignments
-- for formulas.
-- By implementing a binary interface over the SMTLIB2 format defined at
-- http://www.smt-lib.org/
-- http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf
module Language.Fixpoint.Smt.Interface (
-- * Commands
Command (..)
-- * Responses
, Response (..)
-- * Typeclass for SMTLIB2 conversion
, SMTLIB2 (..)
-- * Creating and killing SMTLIB2 Process
, Context (..)
, makeContext
, makeContextNoLog
, cleanupContext
-- * Execute Queries
, command
, smtWrite
-- * Query API
, smtDecl
, smtAssert
, smtCheckUnsat
, smtBracket
, smtDistinct
-- * Theory Symbols
, theorySymbols
-- smt_set_funs
) 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
{- Usage:
runFile f
= readFile f >>= runString
runString str
= runCommands $ rr str
runCommands cmds
= do me <- makeContext Z3
mapM_ (T.putStrLn . smt2) cmds
zs <- mapM (command me) cmds
return zs
-}
--------------------------------------------------------------------------
-- | SMT IO --------------------------------------------------------------
--------------------------------------------------------------------------
--------------------------------------------------------------------------
command :: Context -> Command -> IO Response
--------------------------------------------------------------------------
command me !cmd = {-# SCC "command" #-} 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 = {-# SCC "smtRead" #-}
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 = {-# SCC "responseP" #-} A.char '(' *> sexpP
<|> A.string "sat" *> return Sat
<|> A.string "unsat" *> return Unsat
<|> A.string "unknown" *> return Unknown
sexpP = {-# SCC "sexpP" #-} A.string "error" *> (Error <$> errorP)
<|> Values <$> valuesP
errorP = A.skipSpace *> A.char '"' *> A.takeWhile1 (/='"') <* A.string "\")"
valuesP = A.many1' pairP <* (A.char ')')
pairP = {-# SCC "pairP" #-}
do A.skipSpace
A.char '('
!x <- symbolP
A.skipSpace
!v <- valueP
A.char ')'
return (x,v)
symbolP = {-# SCC "symbolP" #-} symbol <$> A.takeWhile1 (not . isSpace)
valueP = {-# SCC "valueP" #-} negativeP
<|> A.takeWhile1 (\c -> not (c == ')' || isSpace c))
negativeP
= do v <- A.char '(' *> A.takeWhile1 (/=')') <* A.char ')'
return $ "(" <> v <> ")"
{-@ pairs :: {v:[a] | (len v) mod 2 = 0} -> [(a,a)] @-}
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 = {-# SCC "smtWriteRaw" #-} do
hPutStrLnNow (cOut me) s
maybe (return ()) (`hPutStrLnNow` s) (cLog me)
smtReadRaw :: Context -> IO Raw
smtReadRaw me = {-# SCC "smtReadRaw" #-} TIO.hGetLine (cIn me)
hPutStrLnNow h !s = LTIO.hPutStrLn h s >> hFlush h
--------------------------------------------------------------------------
-- | SMT Context ---------------------------------------------------------
--------------------------------------------------------------------------
--------------------------------------------------------------------------
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
{- "z3 -smt2 -in" -}
{- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}
{- "z3 -smtc -in MBQI=false" -}
smtCmd Z3 = "z3 -smt2 -in"
smtCmd Mathsat = "mathsat -input=smt2"
smtCmd Cvc4 = "cvc4 --incremental -L smtlib2"
-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...
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
-----------------------------------------------------------------------------
-- | SMT Commands -----------------------------------------------------------
-----------------------------------------------------------------------------
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
-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...
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)" ]