{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}
module Language.Fixpoint.Smt.Interface (
Command (..)
, Response (..)
, SMTLIB2 (..)
, Context (..)
, makeContext
, makeContextNoLog
, makeContextWithSEnv
, cleanupContext
, command
, smtExit
, smtSetMbqi
, smtDecl
, smtDecls
, smtDefineFunc
, smtAssert
, smtFuncDecl
, smtAssertAxiom
, smtCheckUnsat
, smtCheckSat
, smtBracket, smtBracketAt
, smtDistinct
, smtPush, smtPop
, smtAssertAsync
, smtCheckUnsatAsync
, readCheckUnsat
, smtBracketAsyncAt
, smtPushAsync
, smtPopAsync
, checkValid
, checkValid'
, checkValidWithContext
, checkValids
) where
import Control.Concurrent.Async (async, cancel)
import Control.Concurrent.STM
(TVar, atomically, modifyTVar, newTVarIO, readTVar, retry, writeTVar)
import Language.Fixpoint.Types.Config ( SMTSolver (..)
, Config
, solver
, smtTimeout
, gradual
, stringTheory)
import qualified Language.Fixpoint.Misc as Misc
import Language.Fixpoint.Types.Errors
import Language.Fixpoint.Utils.Files
import Language.Fixpoint.Types hiding (allowHO)
import qualified Language.Fixpoint.Types as F
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 qualified Data.HashMap.Strict as M
import Data.Maybe (fromMaybe)
#if !MIN_VERSION_base(4,14,0)
import Data.Semigroup (Semigroup (..))
#endif
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.Console.CmdArgs.Verbosity
import System.Exit hiding (die)
import System.FilePath
import System.IO
import System.Process
import qualified Data.Attoparsec.Text as A
import Data.Attoparsec.Internal.Types (Parser)
import Text.PrettyPrint.HughesPJ (text)
import Language.Fixpoint.SortCheck
import Language.Fixpoint.Utils.Builder as Builder
checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValidWithContext Context
me [(Symbol, Sort)]
xts Expr
p Expr
q =
Context -> String -> IO Bool -> IO Bool
forall a. Context -> String -> IO a -> IO a
smtBracket Context
me String
"checkValidWithContext" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$
Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' Context
me [(Symbol, Sort)]
xts Expr
p Expr
q
checkValid :: Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid :: Config -> String -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid Config
cfg String
f [(Symbol, Sort)]
xts Expr
p Expr
q = do
Context
me <- Config -> String -> IO Context
makeContext Config
cfg String
f
Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' Context
me [(Symbol, Sort)]
xts Expr
p Expr
q
checkValid' :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' Context
me [(Symbol, Sort)]
xts Expr
p Expr
q = do
Context -> [(Symbol, Sort)] -> IO ()
smtDecls Context
me [(Symbol, Sort)]
xts
Context -> Expr -> IO ()
smtAssert Context
me (Expr -> IO ()) -> Expr -> IO ()
forall a b. (a -> b) -> a -> b
$ ListNE Expr -> Expr
pAnd [Expr
p, Expr -> Expr
PNot Expr
q]
Context -> IO Bool
smtCheckUnsat Context
me
checkValids :: Config -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]
checkValids :: Config -> String -> [(Symbol, Sort)] -> ListNE Expr -> IO [Bool]
checkValids Config
cfg String
f [(Symbol, Sort)]
xts ListNE Expr
ps
= do Context
me <- Config -> String -> IO Context
makeContext Config
cfg String
f
Context -> [(Symbol, Sort)] -> IO ()
smtDecls Context
me [(Symbol, Sort)]
xts
ListNE Expr -> (Expr -> IO Bool) -> IO [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ListNE Expr
ps ((Expr -> IO Bool) -> IO [Bool]) -> (Expr -> IO Bool) -> IO [Bool]
forall a b. (a -> b) -> a -> b
$ \Expr
p ->
Context -> String -> IO Bool -> IO Bool
forall a. Context -> String -> IO a -> IO a
smtBracket Context
me String
"checkValids" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$
Context -> Expr -> IO ()
smtAssert Context
me (Expr -> Expr
PNot Expr
p) IO () -> IO Bool -> IO Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Context -> IO Bool
smtCheckUnsat Context
me
{-# SCC command #-}
command :: Context -> Command -> IO Response
command :: Context -> Command -> IO Response
command Context
me !Command
cmd = IO ()
say IO () -> IO Response -> IO Response
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> IO Response
hear Command
cmd
where
env :: SymEnv
env = Context -> SymEnv
ctxSymEnv Context
me
say :: IO ()
say = Context -> Raw -> IO ()
smtWrite Context
me ({-# SCC "Command-runSmt2" #-} Builder -> Raw
Builder.toLazyText (SymEnv -> Command -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
runSmt2 SymEnv
env Command
cmd))
hear :: Command -> IO Response
hear Command
CheckSat = Context -> IO Response
smtRead Context
me
hear (GetValue [Symbol]
_) = Context -> IO Response
smtRead Context
me
hear Command
_ = Response -> IO Response
forall (m :: * -> *) a. Monad m => a -> m a
return Response
Ok
smtExit :: Context -> IO ()
smtExit :: Context -> IO ()
smtExit Context
me = Context -> Command -> IO ()
asyncCommand Context
me Command
Exit
smtSetMbqi :: Context -> IO ()
smtSetMbqi :: Context -> IO ()
smtSetMbqi Context
me = Context -> Command -> IO ()
asyncCommand Context
me Command
SetMbqi
smtWrite :: Context -> Raw -> IO ()
smtWrite :: Context -> Raw -> IO ()
smtWrite Context
me !Raw
s = Context -> Raw -> IO ()
smtWriteRaw Context
me Raw
s
smtRead :: Context -> IO Response
smtRead :: Context -> IO Response
smtRead Context
me = do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Context -> Bool
ctxVerbose Context
me) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Raw -> IO ()
LTIO.putStrLn Raw
"SMT READ"
Text
ln <- Context -> IO Text
smtReadRaw Context
me
Result Response
res <- IO Text -> Parser Response -> Text -> IO (Result Response)
forall (m :: * -> *) a.
Monad m =>
m Text -> Parser a -> Text -> m (Result a)
A.parseWith (Context -> IO Text
smtReadRaw Context
me) Parser Response
responseP Text
ln
case Result Response -> Either String Response
forall r. Result r -> Either String r
A.eitherResult Result Response
res of
Left String
e -> String -> IO Response
forall a. (?callStack::CallStack) => String -> a
Misc.errorstar (String -> IO Response) -> String -> IO Response
forall a b. (a -> b) -> a -> b
$ String
"SMTREAD:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e
Right Response
r -> do
IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (\Handle
h -> Handle -> Raw -> IO ()
LTIO.hPutStrLn Handle
h (Raw -> IO ()) -> Raw -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> Raw
blt (Builder
"; SMT Says: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (Response -> Builder
forall a. Show a => a -> Builder
bShow Response
r))) (Context -> Maybe Handle
ctxLog Context
me)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Context -> Bool
ctxVerbose Context
me) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Raw -> IO ()
LTIO.putStrLn (Raw -> IO ()) -> Raw -> IO ()
forall a b. (a -> b) -> a -> b
$ Builder -> Raw
blt (Builder
"SMT Says: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Response -> Builder
forall a. Show a => a -> Builder
bShow Response
r)
Response -> IO Response
forall (m :: * -> *) a. Monad m => a -> m a
return Response
r
type SmtParser a = Parser T.Text a
responseP :: SmtParser Response
responseP :: Parser Response
responseP = Char -> Parser Char
A.char Char
'(' Parser Char -> Parser Response -> Parser Response
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Response
sexpP
Parser Response -> Parser Response -> Parser Response
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text
A.string Text
"sat" Parser Text -> Parser Response -> Parser Response
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Response -> Parser Response
forall (m :: * -> *) a. Monad m => a -> m a
return Response
Sat
Parser Response -> Parser Response -> Parser Response
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text
A.string Text
"unsat" Parser Text -> Parser Response -> Parser Response
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Response -> Parser Response
forall (m :: * -> *) a. Monad m => a -> m a
return Response
Unsat
Parser Response -> Parser Response -> Parser Response
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text
A.string Text
"unknown" Parser Text -> Parser Response -> Parser Response
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Response -> Parser Response
forall (m :: * -> *) a. Monad m => a -> m a
return Response
Unknown
sexpP :: SmtParser Response
sexpP :: Parser Response
sexpP = Text -> Parser Text
A.string Text
"error" Parser Text -> Parser Response -> Parser Response
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> Response
Error (Text -> Response) -> Parser Text -> Parser Response
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
errorP)
Parser Response -> Parser Response -> Parser Response
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [(Symbol, Text)] -> Response
Values ([(Symbol, Text)] -> Response)
-> Parser Text [(Symbol, Text)] -> Parser Response
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text [(Symbol, Text)]
valuesP
errorP :: SmtParser T.Text
errorP :: Parser Text
errorP = Parser ()
A.skipSpace Parser () -> Parser Char -> Parser Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> Parser Char
A.char Char
'"' Parser Char -> Parser Text -> Parser Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Char -> Bool) -> Parser Text
A.takeWhile1 (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/=Char
'"') Parser Text -> Parser Text -> Parser Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser Text
A.string Text
"\")"
valuesP :: SmtParser [(Symbol, T.Text)]
valuesP :: Parser Text [(Symbol, Text)]
valuesP = Parser Text (Symbol, Text) -> Parser Text [(Symbol, Text)]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
A.many1' Parser Text (Symbol, Text)
pairP Parser Text [(Symbol, Text)]
-> Parser Char -> Parser Text [(Symbol, Text)]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
A.char Char
')'
pairP :: SmtParser (Symbol, T.Text)
pairP :: Parser Text (Symbol, Text)
pairP =
do Parser ()
A.skipSpace
Char -> Parser Char
A.char Char
'('
!Symbol
x <- SmtParser Symbol
symbolP
Parser ()
A.skipSpace
!Text
v <- Parser Text
valueP
Char -> Parser Char
A.char Char
')'
(Symbol, Text) -> Parser Text (Symbol, Text)
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
x,Text
v)
symbolP :: SmtParser Symbol
symbolP :: SmtParser Symbol
symbolP = Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> Parser Text -> SmtParser Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> Parser Text
A.takeWhile1 (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace)
valueP :: SmtParser T.Text
valueP :: Parser Text
valueP = Parser Text
negativeP
Parser Text -> Parser Text -> Parser Text
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Char -> Bool) -> Parser Text
A.takeWhile1 (\Char
c -> Bool -> Bool
not (Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')' Bool -> Bool -> Bool
|| Char -> Bool
isSpace Char
c))
negativeP :: SmtParser T.Text
negativeP :: Parser Text
negativeP
= do Text
v <- Char -> Parser Char
A.char Char
'(' Parser Char -> Parser Text -> Parser Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Char -> Bool) -> Parser Text
A.takeWhile1 (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/=Char
')') Parser Text -> Parser Char -> Parser Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
A.char Char
')'
Text -> Parser Text
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> Parser Text) -> Text -> Parser Text
forall a b. (a -> b) -> a -> b
$ Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
v Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
smtWriteRaw :: Context -> Raw -> IO ()
smtWriteRaw :: Context -> Raw -> IO ()
smtWriteRaw Context
me !Raw
s = do
Handle -> Raw -> IO ()
hPutStrLnNow (Context -> Handle
ctxCout Context
me) Raw
s
IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> Raw -> IO ()
`LTIO.hPutStrLn` Raw
s) (Context -> Maybe Handle
ctxLog Context
me)
smtReadRaw :: Context -> IO T.Text
smtReadRaw :: Context -> IO Text
smtReadRaw Context
me = Handle -> IO Text
TIO.hGetLine (Context -> Handle
ctxCin Context
me)
{-# SCC smtReadRaw #-}
hPutStrLnNow :: Handle -> LT.Text -> IO ()
hPutStrLnNow :: Handle -> Raw -> IO ()
hPutStrLnNow Handle
h !Raw
s = Handle -> Raw -> IO ()
LTIO.hPutStrLn Handle
h Raw
s IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
h
{-# SCC hPutStrLnNow #-}
makeContext :: Config -> FilePath -> IO Context
makeContext :: Config -> String -> IO Context
makeContext Config
cfg String
f
= do Context
me <- Config -> IO Context
makeProcess Config
cfg
[Raw]
pre <- Config -> SMTSolver -> Context -> IO [Raw]
smtPreamble Config
cfg (Config -> SMTSolver
solver Config
cfg) Context
me
Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String
takeDirectory String
smtFile
Handle
hLog <- String -> IOMode -> IO Handle
openFile String
smtFile IOMode
WriteMode
Handle -> BufferMode -> IO ()
hSetBuffering Handle
hLog (BufferMode -> IO ()) -> BufferMode -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe Int -> BufferMode
BlockBuffering (Maybe Int -> BufferMode) -> Maybe Int -> BufferMode
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Int
1024Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
1024Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
64
let me' :: Context
me' = Context
me { ctxLog :: Maybe Handle
ctxLog = Handle -> Maybe Handle
forall a. a -> Maybe a
Just Handle
hLog }
(Raw -> IO ()) -> [Raw] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Context -> Raw -> IO ()
smtWrite Context
me') [Raw]
pre
Context -> IO Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
me'
where
smtFile :: String
smtFile = Ext -> String -> String
extFileName Ext
Smt2 String
f
makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context
makeContextWithSEnv :: Config -> String -> SymEnv -> IO Context
makeContextWithSEnv Config
cfg String
f SymEnv
env = do
Context
ctx <- Config -> String -> IO Context
makeContext Config
cfg String
f
let ctx' :: Context
ctx' = Context
ctx {ctxSymEnv :: SymEnv
ctxSymEnv = SymEnv
env}
Context -> IO ()
declare Context
ctx'
Context -> IO Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
ctx'
makeContextNoLog :: Config -> IO Context
makeContextNoLog :: Config -> IO Context
makeContextNoLog Config
cfg
= do Context
me <- Config -> IO Context
makeProcess Config
cfg
[Raw]
pre <- Config -> SMTSolver -> Context -> IO [Raw]
smtPreamble Config
cfg (Config -> SMTSolver
solver Config
cfg) Context
me
(Raw -> IO ()) -> [Raw] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Context -> Raw -> IO ()
smtWrite Context
me) [Raw]
pre
Context -> IO Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
me
makeProcess :: Config -> IO Context
makeProcess :: Config -> IO Context
makeProcess Config
cfg
= do (Handle
hOut, Handle
hIn, Handle
_ ,ProcessHandle
pid) <- String -> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveCommand (String -> IO (Handle, Handle, Handle, ProcessHandle))
-> String -> IO (Handle, Handle, Handle, ProcessHandle)
forall a b. (a -> b) -> a -> b
$ SMTSolver -> String
smtCmd (Config -> SMTSolver
solver Config
cfg)
Bool
loud <- IO Bool
isLoud
Handle -> BufferMode -> IO ()
hSetBuffering Handle
hOut (BufferMode -> IO ()) -> BufferMode -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe Int -> BufferMode
BlockBuffering (Maybe Int -> BufferMode) -> Maybe Int -> BufferMode
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Int
1024Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
1024Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
64
Handle -> BufferMode -> IO ()
hSetBuffering Handle
hIn (BufferMode -> IO ()) -> BufferMode -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe Int -> BufferMode
BlockBuffering (Maybe Int -> BufferMode) -> Maybe Int -> BufferMode
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Int
1024Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
1024Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
64
TVar Builder
queueTVar <- Builder -> IO (TVar Builder)
forall a. a -> IO (TVar a)
newTVarIO Builder
forall a. Monoid a => a
mempty
Async ()
writerAsync <- IO () -> IO (Async ())
forall a. IO a -> IO (Async a)
async (IO () -> IO (Async ())) -> IO () -> IO (Async ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
forall (f :: * -> *) a b. Applicative f => f a -> f b
forever (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
Raw
t <- STM Raw -> IO Raw
forall a. STM a -> IO a
atomically (STM Raw -> IO Raw) -> STM Raw -> IO Raw
forall a b. (a -> b) -> a -> b
$ do
Builder
builder <- TVar Builder -> STM Builder
forall a. TVar a -> STM a
readTVar TVar Builder
queueTVar
let t :: Raw
t = Builder -> Raw
Builder.toLazyText Builder
builder
Bool -> STM () -> STM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Raw -> Bool
LT.null Raw
t) STM ()
forall a. STM a
retry
TVar Builder -> Builder -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar TVar Builder
queueTVar Builder
forall a. Monoid a => a
mempty
Raw -> STM Raw
forall (m :: * -> *) a. Monad m => a -> m a
return Raw
t
Handle -> Raw -> IO ()
LTIO.hPutStr Handle
hOut Raw
t
Handle -> IO ()
hFlush Handle
hOut
Context -> IO Context
forall (m :: * -> *) a. Monad m => a -> m a
return Ctx :: ProcessHandle
-> Handle
-> Handle
-> Maybe Handle
-> Bool
-> SymEnv
-> Async ()
-> TVar Builder
-> Context
Ctx { ctxPid :: ProcessHandle
ctxPid = ProcessHandle
pid
, ctxCin :: Handle
ctxCin = Handle
hIn
, ctxCout :: Handle
ctxCout = Handle
hOut
, ctxLog :: Maybe Handle
ctxLog = Maybe Handle
forall a. Maybe a
Nothing
, ctxVerbose :: Bool
ctxVerbose = Bool
loud
, ctxSymEnv :: SymEnv
ctxSymEnv = SymEnv
forall a. Monoid a => a
mempty
, ctxAsync :: Async ()
ctxAsync = Async ()
writerAsync
, ctxTVar :: TVar Builder
ctxTVar = TVar Builder
queueTVar
}
cleanupContext :: Context -> IO ExitCode
cleanupContext :: Context -> IO ExitCode
cleanupContext (Ctx {Bool
Maybe Handle
Handle
Async ()
TVar Builder
ProcessHandle
SymEnv
ctxTVar :: TVar Builder
ctxAsync :: Async ()
ctxSymEnv :: SymEnv
ctxVerbose :: Bool
ctxLog :: Maybe Handle
ctxCout :: Handle
ctxCin :: Handle
ctxPid :: ProcessHandle
ctxTVar :: Context -> TVar Builder
ctxAsync :: Context -> Async ()
ctxPid :: Context -> ProcessHandle
ctxCin :: Context -> Handle
ctxCout :: Context -> Handle
ctxLog :: Context -> Maybe Handle
ctxVerbose :: Context -> Bool
ctxSymEnv :: Context -> SymEnv
..}) = do
Async () -> IO ()
forall a. Async a -> IO ()
cancel Async ()
ctxAsync
String -> Handle -> IO ()
hCloseMe String
"ctxCin" Handle
ctxCin
String -> Handle -> IO ()
hCloseMe String
"ctxCout" Handle
ctxCout
IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (String -> Handle -> IO ()
hCloseMe String
"ctxLog") Maybe Handle
ctxLog
ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ctxPid
hCloseMe :: String -> Handle -> IO ()
hCloseMe :: String -> Handle -> IO ()
hCloseMe String
msg Handle
h = Handle -> IO ()
hClose Handle
h IO () -> (IOException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(IOException
exn :: IOException) -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"OOPS, hClose breaks: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ IOException -> String
forall a. Show a => a -> String
show IOException
exn)
smtCmd :: SMTSolver -> String
smtCmd :: SMTSolver -> String
smtCmd SMTSolver
Z3 = String
"z3 -smt2 -in"
smtCmd SMTSolver
Mathsat = String
"mathsat -input=smt2"
smtCmd SMTSolver
Cvc4 = String
"cvc4 --incremental -L smtlib2"
smtPreamble :: Config -> SMTSolver -> Context -> IO [LT.Text]
smtPreamble :: Config -> SMTSolver -> Context -> IO [Raw]
smtPreamble Config
cfg SMTSolver
Z3 Context
me
= do Context -> Raw -> IO ()
smtWrite Context
me Raw
"(get-info :version)"
Text
v:[Text]
_ <- Text -> [Text]
T.words (Text -> [Text]) -> (Text -> Text) -> Text -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Text] -> Int -> Text
forall a. [a] -> Int -> a
!!Int
1) ([Text] -> Text) -> (Text -> [Text]) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> [Text]
T.splitOn Text
"\"" (Text -> [Text]) -> IO Text -> IO [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> IO Text
smtReadRaw Context
me
SMTSolver -> Text -> Config -> IO ()
checkValidStringFlag SMTSolver
Z3 Text
v Config
cfg
if Text -> Text -> [Text]
T.splitOn Text
"." Text
v [Text] -> [Text] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
`versionGreaterEq` [Text
"4", Text
"3", Text
"2"]
then [Raw] -> IO [Raw]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Raw] -> IO [Raw]) -> [Raw] -> IO [Raw]
forall a b. (a -> b) -> a -> b
$ [Raw]
z3_432_options [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
makeMbqi Config
cfg [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
makeTimeout Config
cfg [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> SMTSolver -> [Raw]
Thy.preamble Config
cfg SMTSolver
Z3
else [Raw] -> IO [Raw]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Raw] -> IO [Raw]) -> [Raw] -> IO [Raw]
forall a b. (a -> b) -> a -> b
$ [Raw]
z3_options [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
makeMbqi Config
cfg [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
makeTimeout Config
cfg [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> SMTSolver -> [Raw]
Thy.preamble Config
cfg SMTSolver
Z3
smtPreamble Config
cfg SMTSolver
s Context
_
= SMTSolver -> Text -> Config -> IO ()
checkValidStringFlag SMTSolver
s Text
"" Config
cfg IO () -> IO [Raw] -> IO [Raw]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Raw] -> IO [Raw]
forall (m :: * -> *) a. Monad m => a -> m a
return (Config -> SMTSolver -> [Raw]
Thy.preamble Config
cfg SMTSolver
s)
checkValidStringFlag :: SMTSolver -> T.Text -> Config -> IO ()
checkValidStringFlag :: SMTSolver -> Text -> Config -> IO ()
checkValidStringFlag SMTSolver
smt Text
v Config
cfg
= Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTSolver -> Text -> Config -> Bool
noString SMTSolver
smt Text
v Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
Error -> IO ()
forall a. Error -> a
die (Error -> IO ()) -> Error -> IO ()
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
dummySpan (String -> Doc
text String
"stringTheory is only supported by z3 version >=4.2.2")
noString :: SMTSolver -> T.Text -> Config -> Bool
noString :: SMTSolver -> Text -> Config -> Bool
noString SMTSolver
smt Text
v Config
cfg
= Config -> Bool
stringTheory Config
cfg
Bool -> Bool -> Bool
&& Bool -> Bool
not (SMTSolver
smt SMTSolver -> SMTSolver -> Bool
forall a. Eq a => a -> a -> Bool
== SMTSolver
Z3 Bool -> Bool -> Bool
&& (Text -> Text -> [Text]
T.splitOn Text
"." Text
v [Text] -> [Text] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
`versionGreaterEq` [Text
"4", Text
"4", Text
"2"]))
versionGreaterEq :: Ord a => [a] -> [a] -> Bool
versionGreaterEq :: [a] -> [a] -> Bool
versionGreaterEq (a
x:[a]
xs) (a
y:[a]
ys)
| a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
y = Bool
True
| a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = [a] -> [a] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
versionGreaterEq [a]
xs [a]
ys
| a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y = Bool
False
versionGreaterEq [a]
_ [] = Bool
True
versionGreaterEq [] [a]
_ = Bool
False
versionGreaterEq [a]
_ [a]
_ = String -> Bool
forall a. (?callStack::CallStack) => String -> a
Misc.errorstar String
"Interface.versionGreater called with bad arguments"
smtPush, smtPop :: Context -> IO ()
smtPush :: Context -> IO ()
smtPush Context
me = Context -> Command -> IO ()
interact' Context
me Command
Push
smtPop :: Context -> IO ()
smtPop Context
me = Context -> Command -> IO ()
interact' Context
me Command
Pop
smtDecls :: Context -> [(Symbol, Sort)] -> IO ()
smtDecls :: Context -> [(Symbol, Sort)] -> IO ()
smtDecls = ((Symbol, Sort) -> IO ()) -> [(Symbol, Sort)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((Symbol, Sort) -> IO ()) -> [(Symbol, Sort)] -> IO ())
-> (Context -> (Symbol, Sort) -> IO ())
-> Context
-> [(Symbol, Sort)]
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ())
-> (Context -> Symbol -> Sort -> IO ())
-> Context
-> (Symbol, Sort)
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Symbol -> Sort -> IO ()
smtDecl
smtDecl :: Context -> Symbol -> Sort -> IO ()
smtDecl :: Context -> Symbol -> Sort -> IO ()
smtDecl Context
me Symbol
x Sort
t = Context -> Command -> IO ()
interact' Context
me ( Text -> [SmtSort] -> SmtSort -> Command
Declare (Symbol -> Text
symbolSafeText Symbol
x) [SmtSort]
ins' SmtSort
out')
where
ins' :: [SmtSort]
ins' = Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env (Sort -> SmtSort) -> [Sort] -> [SmtSort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ins
out' :: SmtSort
out' = Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env Sort
out
([Sort]
ins, Sort
out) = Sort -> ([Sort], Sort)
deconSort Sort
t
_msg :: String
_msg = String
"smtDecl: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Symbol, Sort, [Sort], Sort) -> String
forall a. PPrint a => a -> String
showpp (Symbol
x, Sort
t, [Sort]
ins, Sort
out)
env :: SEnv DataDecl
env = SymEnv -> SEnv DataDecl
seData (Context -> SymEnv
ctxSymEnv Context
me)
smtFuncDecl :: Context -> T.Text -> ([SmtSort], SmtSort) -> IO ()
smtFuncDecl :: Context -> Text -> ([SmtSort], SmtSort) -> IO ()
smtFuncDecl Context
me Text
x ([SmtSort]
ts, SmtSort
t) = Context -> Command -> IO ()
interact' Context
me (Text -> [SmtSort] -> SmtSort -> Command
Declare Text
x [SmtSort]
ts SmtSort
t)
smtDataDecl :: Context -> [DataDecl] -> IO ()
smtDataDecl :: Context -> [DataDecl] -> IO ()
smtDataDecl Context
me [DataDecl]
ds = Context -> Command -> IO ()
interact' Context
me ([DataDecl] -> Command
DeclData [DataDecl]
ds)
deconSort :: Sort -> ([Sort], Sort)
deconSort :: Sort -> ([Sort], Sort)
deconSort Sort
t = case Sort -> Maybe ([Int], [Sort], Sort)
functionSort Sort
t of
Just ([Int]
_, [Sort]
ins, Sort
out) -> ([Sort]
ins, Sort
out)
Maybe ([Int], [Sort], Sort)
Nothing -> ([] , Sort
t )
smtCheckSat :: Context -> Expr -> IO Bool
smtCheckSat :: Context -> Expr -> IO Bool
smtCheckSat Context
me Expr
p
= Context -> Expr -> IO ()
smtAssert Context
me Expr
p IO () -> IO Bool -> IO Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Response -> Bool
ans (Response -> Bool) -> IO Response -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> Command -> IO Response
command Context
me Command
CheckSat)
where
ans :: Response -> Bool
ans Response
Sat = Bool
True
ans Response
_ = Bool
False
smtAssert :: Context -> Expr -> IO ()
smtAssert :: Context -> Expr -> IO ()
smtAssert Context
me Expr
p = Context -> Command -> IO ()
interact' Context
me (Maybe Int -> Expr -> Command
Assert Maybe Int
forall a. Maybe a
Nothing Expr
p)
smtDefineFunc :: Context -> Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> IO ()
smtDefineFunc :: Context -> Symbol -> [(Symbol, Sort)] -> Sort -> Expr -> IO ()
smtDefineFunc Context
me Symbol
name [(Symbol, Sort)]
params Sort
rsort Expr
e =
let env :: SEnv DataDecl
env = SymEnv -> SEnv DataDecl
seData (Context -> SymEnv
ctxSymEnv Context
me)
in Context -> Command -> IO ()
interact' Context
me (Command -> IO ()) -> Command -> IO ()
forall a b. (a -> b) -> a -> b
$
Symbol -> [(Symbol, SmtSort)] -> SmtSort -> Expr -> Command
DefineFunc
Symbol
name
(((Symbol, Sort) -> (Symbol, SmtSort))
-> [(Symbol, Sort)] -> [(Symbol, SmtSort)]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env (Sort -> SmtSort) -> (Symbol, Sort) -> (Symbol, SmtSort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) [(Symbol, Sort)]
params)
(Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env Sort
rsort)
Expr
e
asyncCommand :: Context -> Command -> IO ()
asyncCommand :: Context -> Command -> IO ()
asyncCommand Context
me Command
cmd = do
let env :: SymEnv
env = Context -> SymEnv
ctxSymEnv Context
me
cmdText :: Raw
cmdText = {-# SCC "asyncCommand-runSmt2" #-} Builder -> Raw
Builder.toLazyText (Builder -> Raw) -> Builder -> Raw
forall a b. (a -> b) -> a -> b
$ SymEnv -> Command -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
runSmt2 SymEnv
env Command
cmd
TVar Builder -> Raw -> IO ()
asyncPutStrLn (Context -> TVar Builder
ctxTVar Context
me) Raw
cmdText
IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> Raw -> IO ()
`LTIO.hPutStrLn` Raw
cmdText) (Context -> Maybe Handle
ctxLog Context
me)
where
asyncPutStrLn :: TVar Builder.Builder -> LT.Text -> IO ()
asyncPutStrLn :: TVar Builder -> Raw -> IO ()
asyncPutStrLn TVar Builder
tv Raw
t = STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$
TVar Builder -> (Builder -> Builder) -> STM ()
forall a. TVar a -> (a -> a) -> STM ()
modifyTVar TVar Builder
tv (Builder -> Builder -> Builder
forall a. Monoid a => a -> a -> a
`mappend` (Raw -> Builder
Builder.fromLazyText Raw
t Builder -> Builder -> Builder
forall a. Monoid a => a -> a -> a
`mappend` String -> Builder
forall a. IsString a => String -> a
Builder.fromString String
"\n"))
smtAssertAsync :: Context -> Expr -> IO ()
smtAssertAsync :: Context -> Expr -> IO ()
smtAssertAsync Context
me Expr
p = Context -> Command -> IO ()
asyncCommand Context
me (Command -> IO ()) -> Command -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Expr -> Command
Assert Maybe Int
forall a. Maybe a
Nothing Expr
p
smtCheckUnsatAsync :: Context -> IO ()
smtCheckUnsatAsync :: Context -> IO ()
smtCheckUnsatAsync Context
me = Context -> Command -> IO ()
asyncCommand Context
me Command
CheckSat
smtBracketAsyncAt :: SrcSpan -> Context -> String -> IO a -> IO a
smtBracketAsyncAt :: SrcSpan -> Context -> String -> IO a -> IO a
smtBracketAsyncAt SrcSpan
sp Context
x String
y IO a
z = Context -> String -> IO a -> IO a
forall a. Context -> String -> IO a -> IO a
smtBracketAsync Context
x String
y IO a
z IO a -> (Error -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` SrcSpan -> Error -> IO a
forall a. SrcSpan -> Error -> a
dieAt SrcSpan
sp
smtBracketAsync :: Context -> String -> IO a -> IO a
smtBracketAsync :: Context -> String -> IO a -> IO a
smtBracketAsync Context
me String
_msg IO a
a = do
Context -> IO ()
smtPushAsync Context
me
a
r <- IO a
a
Context -> IO ()
smtPopAsync Context
me
a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
smtPushAsync, smtPopAsync :: Context -> IO ()
smtPushAsync :: Context -> IO ()
smtPushAsync Context
me = Context -> Command -> IO ()
asyncCommand Context
me Command
Push
smtPopAsync :: Context -> IO ()
smtPopAsync Context
me = Context -> Command -> IO ()
asyncCommand Context
me Command
Pop
{-# SCC readCheckUnsat #-}
readCheckUnsat :: Context -> IO Bool
readCheckUnsat :: Context -> IO Bool
readCheckUnsat Context
me = Response -> Bool
respSat (Response -> Bool) -> IO Response -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> IO Response
smtRead Context
me
smtAssertAxiom :: Context -> Triggered Expr -> IO ()
smtAssertAxiom :: Context -> Triggered Expr -> IO ()
smtAssertAxiom Context
me Triggered Expr
p = Context -> Command -> IO ()
interact' Context
me (Triggered Expr -> Command
AssertAx Triggered Expr
p)
smtDistinct :: Context -> [Expr] -> IO ()
smtDistinct :: Context -> ListNE Expr -> IO ()
smtDistinct Context
me ListNE Expr
az = Context -> Command -> IO ()
interact' Context
me (ListNE Expr -> Command
Distinct ListNE Expr
az)
smtCheckUnsat :: Context -> IO Bool
smtCheckUnsat :: Context -> IO Bool
smtCheckUnsat Context
me = Response -> Bool
respSat (Response -> Bool) -> IO Response -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> Command -> IO Response
command Context
me Command
CheckSat
smtBracketAt :: SrcSpan -> Context -> String -> IO a -> IO a
smtBracketAt :: SrcSpan -> Context -> String -> IO a -> IO a
smtBracketAt SrcSpan
sp Context
x String
y IO a
z = Context -> String -> IO a -> IO a
forall a. Context -> String -> IO a -> IO a
smtBracket Context
x String
y IO a
z IO a -> (Error -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` SrcSpan -> Error -> IO a
forall a. SrcSpan -> Error -> a
dieAt SrcSpan
sp
smtBracket :: Context -> String -> IO a -> IO a
smtBracket :: Context -> String -> IO a -> IO a
smtBracket Context
me String
_msg IO a
a = do
Context -> IO ()
smtPush Context
me
a
r <- IO a
a
Context -> IO ()
smtPop Context
me
a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
respSat :: Response -> Bool
respSat :: Response -> Bool
respSat Response
Unsat = Bool
True
respSat Response
Sat = Bool
False
respSat Response
Unknown = Bool
False
respSat Response
r = Error -> Bool
forall a. Error -> a
die (Error -> Bool) -> Error -> Bool
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
dummySpan (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String
"crash: SMTLIB2 respSat = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Response -> String
forall a. Show a => a -> String
show Response
r)
interact' :: Context -> Command -> IO ()
interact' :: Context -> Command -> IO ()
interact' Context
me Command
cmd = IO Response -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO Response -> IO ()) -> IO Response -> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Command -> IO Response
command Context
me Command
cmd
makeTimeout :: Config -> [LT.Text]
makeTimeout :: Config -> [Raw]
makeTimeout Config
cfg
| Just Int
i <- Config -> Maybe Int
smtTimeout Config
cfg = [ String -> Raw
LT.pack (String
"\n(set-option :timeout " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int -> String
forall a. Show a => a -> String
show Int
i) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")\n")]
| Bool
otherwise = [Raw
""]
makeMbqi :: Config -> [LT.Text]
makeMbqi :: Config -> [Raw]
makeMbqi Config
cfg
| Config -> Bool
gradual Config
cfg = [Raw
""]
| Bool
otherwise = [Raw
"\n(set-option :smt.mbqi false)"]
z3_432_options :: [LT.Text]
z3_432_options :: [Raw]
z3_432_options
= [ Raw
"(set-option :auto-config false)"
, Raw
"(set-option :model true)"
, Raw
"(set-option :model.partial false)"]
z3_options :: [LT.Text]
z3_options :: [Raw]
z3_options
= [ Raw
"(set-option :auto-config false)"
, Raw
"(set-option :model true)"
, Raw
"(set-option :model-partial false)"]
declare :: Context -> IO ()
declare :: Context -> IO ()
declare Context
me = do
[[DataDecl]] -> ([DataDecl] -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[DataDecl]]
dss (([DataDecl] -> IO ()) -> IO ()) -> ([DataDecl] -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> [DataDecl] -> IO ()
smtDataDecl Context
me
[(Symbol, Sort)] -> ((Symbol, Sort) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Symbol, Sort)]
thyXTs (((Symbol, Sort) -> IO ()) -> IO ())
-> ((Symbol, Sort) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ())
-> (Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Symbol -> Sort -> IO ()
smtDecl Context
me
[(Symbol, Sort)] -> ((Symbol, Sort) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Symbol, Sort)]
qryXTs (((Symbol, Sort) -> IO ()) -> IO ())
-> ((Symbol, Sort) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ())
-> (Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Symbol -> Sort -> IO ()
smtDecl Context
me
[(Text, ([SmtSort], SmtSort))]
-> ((Text, ([SmtSort], SmtSort)) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Text, ([SmtSort], SmtSort))]
ats (((Text, ([SmtSort], SmtSort)) -> IO ()) -> IO ())
-> ((Text, ([SmtSort], SmtSort)) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Text -> ([SmtSort], SmtSort) -> IO ())
-> (Text, ([SmtSort], SmtSort)) -> IO ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Text -> ([SmtSort], SmtSort) -> IO ())
-> (Text, ([SmtSort], SmtSort)) -> IO ())
-> (Text -> ([SmtSort], SmtSort) -> IO ())
-> (Text, ([SmtSort], SmtSort))
-> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Text -> ([SmtSort], SmtSort) -> IO ()
smtFuncDecl Context
me
[ListNE Expr] -> (ListNE Expr -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ListNE Expr]
ess ((ListNE Expr -> IO ()) -> IO ())
-> (ListNE Expr -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> ListNE Expr -> IO ()
smtDistinct Context
me
ListNE Expr -> (Expr -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ListNE Expr
axs ((Expr -> IO ()) -> IO ()) -> (Expr -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Expr -> IO ()
smtAssert Context
me
where
env :: SymEnv
env = Context -> SymEnv
ctxSymEnv Context
me
dss :: [[DataDecl]]
dss = SymEnv -> [[DataDecl]]
dataDeclarations SymEnv
env
lts :: [(Symbol, Sort)]
lts = SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv (SEnv Sort -> [(Symbol, Sort)])
-> (SymEnv -> SEnv Sort) -> SymEnv -> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> SEnv Sort
F.seLits (SymEnv -> [(Symbol, Sort)]) -> SymEnv -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ SymEnv
env
ess :: [ListNE Expr]
ess = [(Symbol, Sort)] -> [ListNE Expr]
distinctLiterals [(Symbol, Sort)]
lts
axs :: ListNE Expr
axs = [(Symbol, Sort)] -> ListNE Expr
Thy.axiomLiterals [(Symbol, Sort)]
lts
thyXTs :: [(Symbol, Sort)]
thyXTs = ((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> (Symbol, Sort) -> Bool
forall b. Int -> (Symbol, b) -> Bool
isKind Int
1) [(Symbol, Sort)]
xts
qryXTs :: [(Symbol, Sort)]
qryXTs = (Sort -> Sort) -> (Symbol, Sort) -> (Symbol, Sort)
forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd Sort -> Sort
forall a. Elaborate a => a -> a
tx ((Symbol, Sort) -> (Symbol, Sort))
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> (Symbol, Sort) -> Bool
forall b. Int -> (Symbol, b) -> Bool
isKind Int
2) [(Symbol, Sort)]
xts
isKind :: Int -> (Symbol, b) -> Bool
isKind Int
n = (Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool) -> ((Symbol, b) -> Int) -> (Symbol, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> Symbol -> Int
symKind SymEnv
env (Symbol -> Int) -> ((Symbol, b) -> Symbol) -> (Symbol, b) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, b) -> Symbol
forall a b. (a, b) -> a
fst
xts :: [(Symbol, Sort)]
xts = SEnv Sort -> [(Symbol, Sort)]
symbolSorts (SymEnv -> SEnv Sort
F.seSort SymEnv
env)
tx :: a -> a
tx = Located String -> SymEnv -> a -> a
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
"declare" SymEnv
env
ats :: [(Text, ([SmtSort], SmtSort))]
ats = SymEnv -> [(Text, ([SmtSort], SmtSort))]
funcSortVars SymEnv
env
symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)]
symbolSorts :: SEnv Sort -> [(Symbol, Sort)]
symbolSorts SEnv Sort
env = [(Symbol
x, Sort -> Sort
tx Sort
t) | (Symbol
x, Sort
t) <- SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv Sort
env ]
where
tx :: Sort -> Sort
tx t :: Sort
t@(FObj Symbol
a) = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe Sort
t (Symbol -> SEnv Sort -> Maybe Sort
forall a. Symbol -> SEnv a -> Maybe a
F.lookupSEnv Symbol
a SEnv Sort
env)
tx Sort
t = Sort
t
dataDeclarations :: SymEnv -> [[DataDecl]]
dataDeclarations :: SymEnv -> [[DataDecl]]
dataDeclarations = [DataDecl] -> [[DataDecl]]
orderDeclarations ([DataDecl] -> [[DataDecl]])
-> (SymEnv -> [DataDecl]) -> SymEnv -> [[DataDecl]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, DataDecl) -> DataDecl)
-> [(Symbol, DataDecl)] -> [DataDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, DataDecl) -> DataDecl
forall a b. (a, b) -> b
snd ([(Symbol, DataDecl)] -> [DataDecl])
-> (SymEnv -> [(Symbol, DataDecl)]) -> SymEnv -> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEnv DataDecl -> [(Symbol, DataDecl)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv (SEnv DataDecl -> [(Symbol, DataDecl)])
-> (SymEnv -> SEnv DataDecl) -> SymEnv -> [(Symbol, DataDecl)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> SEnv DataDecl
F.seData
funcSortVars :: F.SymEnv -> [(T.Text, ([F.SmtSort], F.SmtSort))]
funcSortVars :: SymEnv -> [(Text, ([SmtSort], SmtSort))]
funcSortVars SymEnv
env = [(Symbol -> FuncSort -> Text
var Symbol
applyName FuncSort
t , FuncSort -> ([SmtSort], SmtSort)
forall b. (SmtSort, b) -> ([SmtSort], b)
appSort FuncSort
t) | FuncSort
t <- [FuncSort]
ts]
[(Text, ([SmtSort], SmtSort))]
-> [(Text, ([SmtSort], SmtSort))] -> [(Text, ([SmtSort], SmtSort))]
forall a. [a] -> [a] -> [a]
++ [(Symbol -> FuncSort -> Text
var Symbol
coerceName FuncSort
t , ([SmtSort
t1],SmtSort
t2)) | t :: FuncSort
t@(SmtSort
t1, SmtSort
t2) <- [FuncSort]
ts]
[(Text, ([SmtSort], SmtSort))]
-> [(Text, ([SmtSort], SmtSort))] -> [(Text, ([SmtSort], SmtSort))]
forall a. [a] -> [a] -> [a]
++ [(Symbol -> FuncSort -> Text
var Symbol
lambdaName FuncSort
t , FuncSort -> ([SmtSort], SmtSort)
forall a. (a, a) -> ([a], SmtSort)
lamSort FuncSort
t) | FuncSort
t <- [FuncSort]
ts]
[(Text, ([SmtSort], SmtSort))]
-> [(Text, ([SmtSort], SmtSort))] -> [(Text, ([SmtSort], SmtSort))]
forall a. [a] -> [a] -> [a]
++ [(Symbol -> FuncSort -> Text
var (Int -> Symbol
lamArgSymbol Int
i) FuncSort
t , FuncSort -> ([SmtSort], SmtSort)
forall b b a. (b, b) -> ([a], b)
argSort FuncSort
t) | t :: FuncSort
t@(SmtSort
_,SmtSort
F.SInt) <- [FuncSort]
ts, Int
i <- [Int
1..Int
Thy.maxLamArg] ]
where
var :: Symbol -> FuncSort -> Text
var Symbol
n = Symbol -> SymEnv -> () -> FuncSort -> Text
forall a. PPrint a => Symbol -> SymEnv -> a -> FuncSort -> Text
F.symbolAtSmtName Symbol
n SymEnv
env ()
ts :: [FuncSort]
ts = HashMap FuncSort Int -> [FuncSort]
forall k v. HashMap k v -> [k]
M.keys (SymEnv -> HashMap FuncSort Int
F.seAppls SymEnv
env)
appSort :: (SmtSort, b) -> ([SmtSort], b)
appSort (SmtSort
s,b
t) = ([SmtSort
F.SInt, SmtSort
s], b
t)
lamSort :: (a, a) -> ([a], SmtSort)
lamSort (a
s,a
t) = ([a
s, a
t], SmtSort
F.SInt)
argSort :: (b, b) -> ([a], b)
argSort (b
s,b
_) = ([] , b
s)
symKind :: F.SymEnv -> F.Symbol -> Int
symKind :: SymEnv -> Symbol -> Int
symKind SymEnv
env Symbol
x = case TheorySymbol -> Sem
F.tsInterp (TheorySymbol -> Sem) -> Maybe TheorySymbol -> Maybe Sem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> SymEnv -> Maybe TheorySymbol
F.symEnvTheory Symbol
x SymEnv
env of
Just Sem
F.Theory -> Int
0
Just Sem
F.Ctor -> Int
0
Just Sem
F.Test -> Int
0
Just Sem
F.Field -> Int
0
Just Sem
F.Uninterp -> Int
1
Maybe Sem
Nothing -> Int
2
distinctLiterals :: [(F.Symbol, F.Sort)] -> [[F.Expr]]
distinctLiterals :: [(Symbol, Sort)] -> [ListNE Expr]
distinctLiterals [(Symbol, Sort)]
xts = [ ListNE Expr
es | (Sort
_, ListNE Expr
es) <- [(Sort, ListNE Expr)]
tess ]
where
tess :: [(Sort, ListNE Expr)]
tess = [(Sort, Expr)] -> [(Sort, ListNE Expr)]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Sort
t, Symbol -> Expr
forall a. Expression a => a -> Expr
F.expr Symbol
x) | (Symbol
x, Sort
t) <- [(Symbol, Sort)]
xts, Sort -> Bool
notFun Sort
t]
notFun :: Sort -> Bool
notFun = Bool -> Bool
not (Bool -> Bool) -> (Sort -> Bool) -> Sort -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Bool
F.isFunctionSortedReft (SortedReft -> Bool) -> (Sort -> SortedReft) -> Sort -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> Reft -> SortedReft
`F.RR` Reft
F.trueReft)