module Language.Fixpoint.SmtLib2 (
Command (..)
, Response (..)
, SMTLIB2 (..)
, Context (..)
, makeContext
, makeContextNoLog
, cleanupContext
, command
, smtWrite
, smt_set_funs
) where
import Language.Fixpoint.Config (SMTSolver (..))
import Language.Fixpoint.Files
import Language.Fixpoint.Types
import Control.Monad
import Data.Char
import qualified Data.List as L
import qualified Data.HashMap.Strict as M
import Data.Monoid
import Data.Text.Format
import qualified Data.Text as T
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
import System.FilePath
import System.Process
import System.IO (openFile, IOMode (..), Handle, hFlush, hClose)
import Control.Applicative ((<$>), (<|>), (*>), (<*))
import qualified Data.Attoparsec.Text as A
type Raw = T.Text
data Command = Push
| Pop
| CheckSat
| Declare Symbol [Sort] Sort
| Define Sort
| Assert (Maybe Int) Pred
| Distinct [Expr]
| GetValue [Symbol]
deriving (Eq, Show)
data Response = Ok
| Sat
| Unsat
| Unknown
| Values [(Symbol, Raw)]
| Error Raw
deriving (Eq, Show)
data Context = Ctx { pId :: ProcessHandle
, cIn :: Handle
, cOut :: Handle
, cLog :: Maybe Handle
, verbose :: Bool
}
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 ()) (\h -> hPutStrLnNow h s) (cLog me)
smtReadRaw :: Context -> IO Raw
smtReadRaw me = TIO.hGetLine (cIn me)
hPutStrLnNow h !s = LTIO.hPutStrLn h s >> hFlush h
makeContext :: SMTSolver -> IO Context
makeContext s
= 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'
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)"
r <- (!!1) . T.splitOn "\"" <$> smtReadRaw me
case T.words r of
"4.3.2" : _ -> return $ z3_432_options ++ z3Preamble
_ -> return $ z3_options ++ z3Preamble
smtPreamble _ _
= return smtlibPreamble
smtFile :: FilePath
smtFile = extFileName Smt2 "out"
smtDecl me x ts t = interact' me (Declare x ts t)
smtPush me = interact' me (Push)
smtPop me = interact' me (Pop)
smtAssert me p = interact' me (Assert Nothing p)
smtDistinct me az = interact' me (Distinct az)
smtCheckUnsat me = respSat <$> command me CheckSat
respSat Unsat = True
respSat Sat = False
respSat Unknown = False
respSat r = error "crash: SMTLIB2 respSat"
interact' me cmd = command me cmd >> return ()
elt, set :: Raw
elt = "Elt"
set = "Set"
map = "Map"
bit = "BitVec"
sz32 = "Size32"
sz64 = "Size64"
emp, add, cup, cap, mem, dif, sub, com :: Raw
emp = "smt_set_emp"
add = "smt_set_add"
cup = "smt_set_cup"
cap = "smt_set_cap"
mem = "smt_set_mem"
dif = "smt_set_dif"
sub = "smt_set_sub"
com = "smt_set_com"
sel = "smt_map_sel"
sto = "smt_map_sto"
smt_set_funs :: M.HashMap Symbol Raw
smt_set_funs = M.fromList [ ("Set_emp",emp),("Set_add",add),("Set_cup",cup)
, ("Set_cap",cap),("Set_mem",mem),("Set_dif",dif)
, ("Set_sub",sub),("Set_com",com)]
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)" ]
z3Preamble
= [ format "(define-sort {} () Int)"
(Only elt)
, format "(define-sort {} () (Array {} Bool))"
(set, elt)
, format "(define-fun {} () {} ((as const {}) false))"
(emp, set, set)
, format "(define-fun {} ((x {}) (s {})) Bool (select s x))"
(mem, elt, set)
, format "(define-fun {} ((s {}) (x {})) {} (store s x true))"
(add, set, elt, set)
, format "(define-fun {} ((s1 {}) (s2 {})) {} ((_ map or) s1 s2))"
(cup, set, set, set)
, format "(define-fun {} ((s1 {}) (s2 {})) {} ((_ map and) s1 s2))"
(cap, set, set, set)
, format "(define-fun {} ((s {})) {} ((_ map not) s))"
(com, set, set)
, format "(define-fun {} ((s1 {}) (s2 {})) {} ({} s1 ({} s2)))"
(dif, set, set, set, cap, com)
, format "(define-fun {} ((s1 {}) (s2 {})) Bool (= {} ({} s1 s2)))"
(sub, set, set, emp, dif)
]
smtlibPreamble
= [ "(set-logic QF_UFLIA)"
, format "(define-sort {} () Int)" (Only elt)
, format "(define-sort {} () Int)" (Only set)
, format "(declare-fun {} () {})" (emp, set)
, format "(declare-fun {} ({} {}) {})" (add, set, elt, set)
, format "(declare-fun {} ({} {}) {})" (cup, set, set, set)
, format "(declare-fun {} ({} {}) {})" (cap, set, set, set)
, format "(declare-fun {} ({} {}) {})" (dif, set, set, set)
, format "(declare-fun {} ({} {}) Bool)" (sub, set, set)
, format "(declare-fun {} ({} {}) Bool)" (mem, elt, set)
]
mkSetSort _ _ = set
mkEmptySet _ _ = emp
mkSetAdd _ s x = format "({} {} {})" (add, s, x)
mkSetMem _ x s = format "({} {} {})" (mem, x, s)
mkSetCup _ s t = format "({} {} {})" (cup, s, t)
mkSetCap _ s t = format "({} {} {})" (cap, s, t)
mkSetDif _ s t = format "({} {} {})" (dif, s, t)
mkSetSub _ s t = format "({} {} {})" (sub, s, t)
class SMTLIB2 a where
smt2 :: a -> LT.Text
instance SMTLIB2 Sort where
smt2 FInt = "Int"
smt2 (FApp t []) | t == intFTyCon = "Int"
smt2 (FApp t []) | t == boolFTyCon = "Bool"
smt2 (FApp t [FApp ts _,_]) | t == appFTyCon && fTyconSymbol ts == "Set_Set" = "Set"
smt2 (FObj s) = smt2 s
smt2 (FFunc _ _) = error "smt2 FFunc"
smt2 _ = "Int"
instance SMTLIB2 Symbol where
smt2 s | Just t <- M.lookup s smt_set_funs
= LT.fromStrict t
smt2 s = LT.fromStrict . encode . symbolText $ s
encode :: T.Text -> T.Text
encode t =
foldr (\(x,y) t -> T.replace x y t) t [("[", "ZM"), ("]", "ZN"), (":", "ZC")
,("(", "ZL"), (")", "ZR"), (",", "ZT")
,("|", "zb"), ("#", "zh"), ("\\","zr")
,("z", "zz"), ("Z", "ZZ"), ("%","zv")]
instance SMTLIB2 SymConst where
smt2 (SL s) = LT.fromStrict s
instance SMTLIB2 Constant where
smt2 (I n) = format "{}" (Only n)
instance SMTLIB2 LocSymbol where
smt2 = smt2 . val
instance SMTLIB2 Bop where
smt2 Plus = "+"
smt2 Minus = "-"
smt2 Times = "*"
smt2 Div = "/"
smt2 Mod = "mod"
instance SMTLIB2 Brel where
smt2 Eq = "="
smt2 Ueq = "="
smt2 Gt = ">"
smt2 Ge = ">="
smt2 Lt = "<"
smt2 Le = "<="
smt2 _ = error "SMTLIB2 Brel"
instance SMTLIB2 Expr where
smt2 (ESym z) = smt2 z
smt2 (ECon c) = smt2 c
smt2 (EVar x) = smt2 x
smt2 (ELit x _) = smt2 x
smt2 (EApp f []) = smt2 f
smt2 (EApp f [e]) | val f == "Set_emp"
= format "(= {} {})" (emp, smt2 e)
smt2 (EApp f [e]) | val f == "Set_sng"
= format "({} {} {})" (add, emp, smt2 e)
smt2 (EApp f es) = format "({} {})" (smt2 f, smt2s es)
smt2 (ENeg e) = format "(- {})" (Only $ smt2 e)
smt2 (EBin o e1 e2) = format "({} {} {})" (smt2 o, smt2 e1, smt2 e2)
smt2 (EIte e1 e2 e3) = format "(ite {} {} {})" (smt2 e1, smt2 e2, smt2 e3)
smt2 _ = error "TODO: SMTLIB2 Expr"
instance SMTLIB2 Pred where
smt2 (PTrue) = "true"
smt2 (PFalse) = "false"
smt2 (PAnd ps) = format "(and {})" (Only $ smt2s ps)
smt2 (POr ps) = format "(or {})" (Only $ smt2s ps)
smt2 (PNot p) = format "(not {})" (Only $ smt2 p)
smt2 (PImp p q) = format "(=> {} {})" (smt2 p, smt2 q)
smt2 (PIff p q) = format "(= {} {})" (smt2 p, smt2 q)
smt2 (PBexp e) = smt2 e
smt2 (PAtom r e1 e2) = mkRel r e1 e2
smt2 _ = error "smtlib2 Pred"
mkRel Ne e1 e2 = mkNe e1 e2
mkRel Une e1 e2 = mkNe e1 e2
mkRel r e1 e2 = format "({} {} {})" (smt2 r, smt2 e1, smt2 e2)
mkNe e1 e2 = format "(not (= {} {}))" (smt2 e1, smt2 e2)
instance SMTLIB2 Command where
smt2 (Declare x ts t) = format "(declare-fun {} ({}) {})" (smt2 x, smt2s ts, smt2 t)
smt2 (Define t) = format "(declare-sort {})" (Only $ smt2 t)
smt2 (Assert Nothing p) = format "(assert {})" (Only $ smt2 p)
smt2 (Assert (Just i) p) = format "(assert (! {} :named p-{}))" (smt2 p, i)
smt2 (Distinct az) = format "(assert (distinct {}))" (Only $ smt2s az)
smt2 (Push) = "(push 1)"
smt2 (Pop) = "(pop 1)"
smt2 (CheckSat) = "(check-sat)"
smt2 (GetValue xs) = LT.unwords $ ["(get-value ("] ++ fmap smt2 xs ++ ["))"]
smt2s = LT.intercalate " " . fmap smt2