{-# LANGUAGE CPP                       #-}
{-# LANGUAGE BangPatterns              #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE RecordWildCards           #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE PatternGuards             #-}

-- | 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

-- Note [Async SMT API]
--
-- The SMT solver is started in a separate process and liquid-fixpoint
-- communicates with it via pipes. This mechanism introduces some latency
-- since the queries need to reach the buffers in a separate process and
-- the OS has to switch contexts.
--
-- A remedy we currently try for this is to send multiple queries
-- together without waiting for the reply to each one, i.e. asynchronously.
-- We then collect the multiple answers after sending all of the queries.
--
-- The functions named @smt*Async@ implement this scheme.
--
-- An asynchronous thread is used to write the queries to prevent the
-- caller from blocking on IO, should the write buffer be full or should
-- an 'hFlush' call be necessary.

module Language.Fixpoint.Smt.Interface (

    -- * Commands
      Command  (..)

    -- * Responses
    , Response (..)

    -- * Typeclass for SMTLIB2 conversion
    , SMTLIB2 (..)

    -- * Creating and killing SMTLIB2 Process
    , Context (..)
    , makeContext
    , makeContextNoLog
    , makeContextWithSEnv
    , cleanupContext

    -- * Execute Queries
    , command
    , smtExit
    , smtSetMbqi

    -- * Query API
    , smtDecl
    , smtDecls
    , smtDefineFunc
    , smtAssert
    , smtFuncDecl
    , smtAssertAxiom
    , smtCheckUnsat
    , smtCheckSat
    , smtBracket, smtBracketAt
    , smtDistinct
    , smtPush, smtPop
    , smtAssertAsync
    , smtCheckUnsatAsync
    , readCheckUnsat
    , smtBracketAsyncAt
    , smtPushAsync
    , smtPopAsync

    -- * Check Validity
    , 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           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.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 qualified Data.HashMap.Strict      as M
import           Data.Attoparsec.Internal.Types (Parser)
import           Text.PrettyPrint.HughesPJ (text)
import           Language.Fixpoint.SortCheck
import           Language.Fixpoint.Utils.Builder as Builder
-- import qualified Language.Fixpoint.Types as F
-- import           Language.Fixpoint.Types.PrettyPrint (tracepp)

{-
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
-}

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

-- | type ClosedPred E = {v:Pred | subset (vars v) (keys E) }
-- checkValid :: e:Env -> ClosedPred e -> ClosedPred e -> IO Bool
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

-- | If you already HAVE a context, where all the variables have declared types
--   (e.g. if you want to make MANY repeated Queries)

-- checkValid :: e:Env -> [ClosedPred e] -> IO [Bool]
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

-- debugFile :: FilePath
-- debugFile = "DEBUG.smt2"

--------------------------------------------------------------------------------
-- | SMT IO --------------------------------------------------------------------
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
{-# 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 = {- SCC "smtRead" #-} 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 = {- SCC "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 = {- SCC "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 = {- SCC "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 = {- SCC "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 = {- SCC "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 = {- SCC "smtWriteRaw" #-} do
  -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
  --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
  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    = {- SCC "smtReadRaw" #-} 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 #-}

--------------------------------------------------------------------------
-- | SMT Context ---------------------------------------------------------
--------------------------------------------------------------------------

--------------------------------------------------------------------------
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'
  -- where msg = "makeContextWithSEnv" ++ show env

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
       -- See Note [Async SMT API]
       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)

{- "z3 -smt2 -in"                   -}
{- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}
{- "z3 -smtc -in MBQI=false"        -}

smtCmd         :: SMTSolver -> String --  T.Text
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"

-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...
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"

-----------------------------------------------------------------------------
-- | SMT Commands -----------------------------------------------------------
-----------------------------------------------------------------------------

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 ({- notracepp msg $ -} 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  )

-- hack now this is used only for checking gradual condition.
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

-----------------------------------------------------------------
-- Async calls to the smt
--
-- See Note [Async SMT API]
-----------------------------------------------------------------

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)"]

-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...
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 () -- SolveM ()
--------------------------------------------------------------------------------
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        = {- tracepp "symbolSorts" $ -} 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' returns {0, 1, 2} where:
--   0 = Theory-Definition,
--   1 = Theory-Declaration,
--   2 = Query-Binder

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
              -- Just t  -> if tsInterp t then 0 else 1


-- assumes :: [F.Expr] -> SolveM ()
-- assumes es = withContext $ \me -> forM_  es $ smtAssert me

-- | `distinctLiterals` is used solely to determine the set of literals
--   (of each sort) that are *disequal* to each other, e.g. EQ, LT, GT,
--   or string literals "cat", "dog", "mouse". These should only include
--   non-function sorted values.
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)
    -- _notStr          = not . (F.strSort ==) . F.sr_sort . (`F.RR` F.trueReft)