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

{-# OPTIONS_GHC -Wno-name-shadowing #-}

-- | 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)
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 =
  forall a. Context -> [Char] -> IO a -> IO a
smtBracket Context
me [Char]
"checkValidWithContext" 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 -> [Char] -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid Config
cfg [Char]
f [(Symbol, Sort)]
xts Expr
p Expr
q = do
  Context
me <- Config -> [Char] -> IO Context
makeContext Config
cfg [Char]
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 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 -> [Char] -> [(Symbol, Sort)] -> ListNE Expr -> IO [Bool]
checkValids Config
cfg [Char]
f [(Symbol, Sort)]
xts ListNE Expr
ps
  = do Context
me <- Config -> [Char] -> IO Context
makeContext Config
cfg [Char]
f
       Context -> [(Symbol, Sort)] -> IO ()
smtDecls Context
me [(Symbol, Sort)]
xts
       forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ListNE Expr
ps forall a b. (a -> b) -> a -> b
$ \Expr
p ->
          forall a. Context -> [Char] -> IO a -> IO a
smtBracket Context
me [Char]
"checkValids" forall a b. (a -> b) -> a -> b
$
            Context -> Expr -> IO ()
smtAssert Context
me (Expr -> Expr
PNot Expr
p) 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 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 -> Text -> IO ()
smtWrite Context
me ({-# SCC "Command-runSmt2" #-} Builder -> Text
Builder.toLazyText (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
_            = 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 -> Text -> IO ()
smtWrite Context
me !Text
s = Context -> Text -> IO ()
smtWriteRaw Context
me Text
s

smtRead :: Context -> IO Response
smtRead :: Context -> IO Response
smtRead Context
me = {- SCC "smtRead" -} do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Context -> Bool
ctxVerbose Context
me) forall a b. (a -> b) -> a -> b
$ Text -> IO ()
LTIO.putStrLn Text
"SMT READ"
  Text
ln  <- Context -> IO Text
smtReadRaw Context
me
  Result Response
res <- forall (m :: * -> *) a.
Monad m =>
m Text -> Parser a -> Text -> m (Result a)
A.parseWith (Context -> IO Text
smtReadRaw Context
me) SmtParser Response
responseP Text
ln
  case forall r. Result r -> Either [Char] r
A.eitherResult Result Response
res of
    Left [Char]
e  -> forall a. (?callStack::CallStack) => [Char] -> a
Misc.errorstar forall a b. (a -> b) -> a -> b
$ [Char]
"SMTREAD:" forall a. [a] -> [a] -> [a]
++ [Char]
e
    Right Response
r -> do
      forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) (\Handle
h -> Handle -> Text -> IO ()
LTIO.hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ Builder -> Text
blt (Builder
"; SMT Says: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> Builder
bShow Response
r)) (Context -> Maybe Handle
ctxLog Context
me)
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Context -> Bool
ctxVerbose Context
me) forall a b. (a -> b) -> a -> b
$ Text -> IO ()
LTIO.putStrLn forall a b. (a -> b) -> a -> b
$ Builder -> Text
blt (Builder
"SMT Says: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> Builder
bShow Response
r)
      forall (m :: * -> *) a. Monad m => a -> m a
return Response
r



type SmtParser a = Parser T.Text a

responseP :: SmtParser Response
responseP :: SmtParser Response
responseP = {- SCC "responseP" -} Char -> Parser Char
A.char Char
'(' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SmtParser Response
sexpP
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text
A.string Text
"sat"     forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. Monad m => a -> m a
return Response
Sat
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text
A.string Text
"unsat"   forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. Monad m => a -> m a
return Response
Unsat
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text
A.string Text
"unknown" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. Monad m => a -> m a
return Response
Unknown

sexpP :: SmtParser Response
sexpP :: SmtParser Response
sexpP = {- SCC "sexpP" -} Text -> Parser Text
A.string Text
"error" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> Response
Error forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
errorP)
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [(Symbol, Text)] -> Response
Values forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SmtParser [(Symbol, Text)]
valuesP

errorP :: SmtParser T.Text
errorP :: Parser Text
errorP = Parser ()
A.skipSpace forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> Parser Char
A.char Char
'"' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Char -> Bool) -> Parser Text
A.takeWhile1 (forall a. Eq a => a -> a -> Bool
/=Char
'"') forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser Text
A.string Text
"\")"

valuesP :: SmtParser [(Symbol, T.Text)]
valuesP :: SmtParser [(Symbol, Text)]
valuesP = forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
A.many1' SmtParser (Symbol, Text)
pairP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
A.char Char
')'

pairP :: SmtParser (Symbol, T.Text)
pairP :: SmtParser (Symbol, Text)
pairP = {- SCC "pairP" -}
  do Parser ()
A.skipSpace
     Char
_ <- Char -> Parser Char
A.char Char
'('
     !Symbol
x <- SmtParser Symbol
symbolP
     Parser ()
A.skipSpace
     !Text
v <- Parser Text
valueP
     Char
_ <- Char -> Parser Char
A.char Char
')'
     forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
x,Text
v)

symbolP :: SmtParser Symbol
symbolP :: SmtParser Symbol
symbolP = {- SCC "symbolP" -} forall a. Symbolic a => a -> Symbol
symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> Parser Text
A.takeWhile1 (Bool -> Bool
not 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
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Char -> Bool) -> Parser Text
A.takeWhile1 (\Char
c -> Bool -> Bool
not (Char
c 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
'(' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Char -> Bool) -> Parser Text
A.takeWhile1 (forall a. Eq a => a -> a -> Bool
/=Char
')') forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
A.char Char
')'
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Text
"(" forall a. Semigroup a => a -> a -> a
<> Text
v forall a. Semigroup a => a -> a -> a
<> Text
")"

-- | Writes a line of input for the SMT solver and to the log if there is one.
smtWriteRaw :: Context -> Raw -> IO ()
smtWriteRaw :: Context -> Text -> IO ()
smtWriteRaw Context
me !Text
s = {- SCC "smtWriteRaw" -} do
  -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
  --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
  Handle -> Text -> IO ()
hPutStrLnNow (Context -> Handle
ctxIn Context
me) Text
s
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> Text -> IO ()
`LTIO.hPutStrLn` Text
s) (Context -> Maybe Handle
ctxLog Context
me)

-- | Reads a line of output from the SMT solver.
smtReadRaw :: Context -> IO T.Text
smtReadRaw :: Context -> IO Text
smtReadRaw Context
me = do
  Bool
eof <- Handle -> IO Bool
hIsEOF (Context -> Handle
ctxOut Context
me)
  if Bool
eof then forall a. (?callStack::CallStack) => [Char] -> a
Misc.errorstar [Char]
"SMT returned End of File" else
    Handle -> IO Text
TIO.hGetLine (Context -> Handle
ctxOut Context
me)
{-# SCC smtReadRaw  #-}

hPutStrLnNow :: Handle -> LT.Text -> IO ()
hPutStrLnNow :: Handle -> Text -> IO ()
hPutStrLnNow Handle
h !Text
s = Handle -> Text -> IO ()
LTIO.hPutStrLn Handle
h Text
s 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 -> [Char] -> IO Context
makeContext Config
cfg [Char]
f
  = do Context
me   <- Config -> IO Context
makeProcess Config
cfg
       [Text]
pre  <- Config -> SMTSolver -> Context -> IO [Text]
smtPreamble Config
cfg (Config -> SMTSolver
solver Config
cfg) Context
me
       Bool -> [Char] -> IO ()
createDirectoryIfMissing Bool
True forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
takeDirectory [Char]
smtFile
       Handle
hLog <- [Char] -> IOMode -> IO Handle
openFile [Char]
smtFile IOMode
WriteMode
       Handle -> BufferMode -> IO ()
hSetBuffering Handle
hLog forall a b. (a -> b) -> a -> b
$ Maybe Int -> BufferMode
BlockBuffering forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int
1024forall a. Num a => a -> a -> a
*Int
1024forall a. Num a => a -> a -> a
*Int
64
       let me' :: Context
me' = Context
me { ctxLog :: Maybe Handle
ctxLog = forall a. a -> Maybe a
Just Handle
hLog }
       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Context -> Text -> IO ()
smtWrite Context
me') [Text]
pre
       forall (m :: * -> *) a. Monad m => a -> m a
return Context
me'
    where
       smtFile :: [Char]
smtFile = Ext -> [Char] -> [Char]
extFileName Ext
Smt2 [Char]
f

makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context
makeContextWithSEnv :: Config -> [Char] -> SymEnv -> IO Context
makeContextWithSEnv Config
cfg [Char]
f SymEnv
env = do
  Context
ctx     <- Config -> [Char] -> IO Context
makeContext Config
cfg [Char]
f
  let ctx' :: Context
ctx' = Context
ctx {ctxSymEnv :: SymEnv
ctxSymEnv = SymEnv
env}
  Context -> IO ()
declare Context
ctx'
  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
       [Text]
pre <- Config -> SMTSolver -> Context -> IO [Text]
smtPreamble Config
cfg (Config -> SMTSolver
solver Config
cfg) Context
me
       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Context -> Text -> IO ()
smtWrite Context
me) [Text]
pre
       forall (m :: * -> *) a. Monad m => a -> m a
return Context
me

makeProcess :: Config -> IO Context
makeProcess :: Config -> IO Context
makeProcess Config
cfg
  = do (Handle
hIn, Handle
hOut, Handle
_ ,ProcessHandle
pid) <- [Char] -> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveCommand forall a b. (a -> b) -> a -> b
$ SMTSolver -> [Char]
smtCmd (Config -> SMTSolver
solver Config
cfg)
       Bool
loud <- IO Bool
isLoud
       Handle -> BufferMode -> IO ()
hSetBuffering Handle
hOut forall a b. (a -> b) -> a -> b
$ Maybe Int -> BufferMode
BlockBuffering forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int
1024forall a. Num a => a -> a -> a
*Int
1024forall a. Num a => a -> a -> a
*Int
64
       Handle -> BufferMode -> IO ()
hSetBuffering Handle
hIn forall a b. (a -> b) -> a -> b
$ Maybe Int -> BufferMode
BlockBuffering forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int
1024forall a. Num a => a -> a -> a
*Int
1024forall a. Num a => a -> a -> a
*Int
64
       -- See Note [Async SMT API]
       TVar Builder
queueTVar <- forall a. a -> IO (TVar a)
newTVarIO forall a. Monoid a => a
mempty
       Async ()
writerAsync <- forall a. IO a -> IO (Async a)
async forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Applicative f => f a -> f b
forever forall a b. (a -> b) -> a -> b
$ do
         Text
t <- forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ do
           Builder
builder <- forall a. TVar a -> STM a
readTVar TVar Builder
queueTVar
           let t :: Text
t = Builder -> Text
Builder.toLazyText Builder
builder
           forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Text -> Bool
LT.null Text
t) forall a. STM a
retry
           forall a. TVar a -> a -> STM ()
writeTVar TVar Builder
queueTVar forall a. Monoid a => a
mempty
           forall (m :: * -> *) a. Monad m => a -> m a
return Text
t
         Handle -> Text -> IO ()
LTIO.hPutStr Handle
hIn Text
t
         Handle -> IO ()
hFlush Handle
hIn
       forall (m :: * -> *) a. Monad m => a -> m a
return Ctx { ctxPid :: ProcessHandle
ctxPid     = ProcessHandle
pid
                  , ctxIn :: Handle
ctxIn      = Handle
hIn
                  , ctxOut :: Handle
ctxOut     = Handle
hOut
                  , ctxLog :: Maybe Handle
ctxLog     = forall a. Maybe a
Nothing
                  , ctxVerbose :: Bool
ctxVerbose = Bool
loud
                  , ctxSymEnv :: SymEnv
ctxSymEnv  = forall a. Monoid a => a
mempty
                  , ctxAsync :: Async ()
ctxAsync   = Async ()
writerAsync
                  , ctxTVar :: TVar Builder
ctxTVar    = TVar Builder
queueTVar
                  }

-- | Close file handles and wait for the solver process to terminate.
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
ctxOut :: Handle
ctxIn :: Handle
ctxPid :: ProcessHandle
ctxTVar :: Context -> TVar Builder
ctxAsync :: Context -> Async ()
ctxPid :: Context -> ProcessHandle
ctxOut :: Context -> Handle
ctxIn :: Context -> Handle
ctxLog :: Context -> Maybe Handle
ctxVerbose :: Context -> Bool
ctxSymEnv :: Context -> SymEnv
..} = do
  forall a. Async a -> IO ()
cancel Async ()
ctxAsync
  [Char] -> Handle -> IO ()
hCloseMe [Char]
"ctxIn" Handle
ctxIn
  [Char] -> Handle -> IO ()
hCloseMe [Char]
"ctxOut"  Handle
ctxOut
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) ([Char] -> Handle -> IO ()
hCloseMe [Char]
"ctxLog") Maybe Handle
ctxLog
  ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ctxPid

hCloseMe :: String -> Handle -> IO ()
hCloseMe :: [Char] -> Handle -> IO ()
hCloseMe [Char]
msg Handle
h = Handle -> IO ()
hClose Handle
h forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(IOException
exn :: IOException) -> [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"OOPS, hClose breaks: " forall a. [a] -> [a] -> [a]
++ [Char]
msg forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show IOException
exn)

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

smtCmd         :: SMTSolver -> String --  T.Text
smtCmd :: SMTSolver -> [Char]
smtCmd SMTSolver
Z3      = [Char]
"z3 -smt2 -in"
smtCmd SMTSolver
Mathsat = [Char]
"mathsat -input=smt2"
smtCmd SMTSolver
Cvc4    = [Char]
"cvc4 --incremental -L smtlib2"

smtPreamble :: Config -> SMTSolver -> Context -> IO [LT.Text]
smtPreamble :: Config -> SMTSolver -> Context -> IO [Text]
smtPreamble Config
cfg SMTSolver
Z3 Context
me
  = do [Int]
v <- Context -> IO [Int]
getZ3Version Context
me
       SMTSolver -> [Int] -> Config -> IO ()
checkValidStringFlag SMTSolver
Z3 [Int]
v Config
cfg
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Text]
z3_options forall a. [a] -> [a] -> [a]
++ Config -> [Text]
makeMbqi Config
cfg forall a. [a] -> [a] -> [a]
++ Config -> [Text]
makeTimeout Config
cfg forall a. [a] -> [a] -> [a]
++ Config -> SMTSolver -> [Text]
Thy.preamble Config
cfg SMTSolver
Z3
smtPreamble Config
cfg SMTSolver
s Context
_
  = SMTSolver -> [Int] -> Config -> IO ()
checkValidStringFlag SMTSolver
s [] Config
cfg forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Config -> SMTSolver -> [Text]
Thy.preamble Config
cfg SMTSolver
s)

getZ3Version :: Context -> IO [Int]
getZ3Version :: Context -> IO [Int]
getZ3Version Context
me
  = do Context -> Text -> IO ()
smtWrite Context
me Text
"(get-info :version)"
       -- resp is like (:version "4.8.15")
       Text
resp <- Context -> IO Text
smtReadRaw Context
me
       case Text -> Text -> [Text]
T.splitOn Text
"\"" Text
resp of
         Text
_:Text
vText:[Text]
_ -> do
           let parsedComponents :: [[(a, [Char])]]
parsedComponents = [ forall a. Read a => ReadS a
reads (Text -> [Char]
T.unpack Text
cText) | Text
cText <- Text -> Text -> [Text]
T.splitOn Text
"." Text
vText ]
           forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
             [ case [(Int, [Char])]
pComponent of
                 [(Int
c, [Char]
"")] -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
c
                 [(Int, [Char])]
xs -> forall a. (?callStack::CallStack) => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Can't parse z3 version: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [(Int, [Char])]
xs
             | [(Int, [Char])]
pComponent <- forall {a}. Read a => [[(a, [Char])]]
parsedComponents
             ]
         [Text]
xs -> forall a. (?callStack::CallStack) => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Can't parse z3 (get-info :version): " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Text]
xs

checkValidStringFlag :: SMTSolver -> [Int] -> Config -> IO ()
checkValidStringFlag :: SMTSolver -> [Int] -> Config -> IO ()
checkValidStringFlag SMTSolver
smt [Int]
v Config
cfg
  = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTSolver -> [Int] -> Config -> Bool
noString SMTSolver
smt [Int]
v Config
cfg) forall a b. (a -> b) -> a -> b
$
      forall a. Error -> a
die forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
dummySpan ([Char] -> Doc
text [Char]
"stringTheory is only supported by z3 version >=4.2.2")

noString :: SMTSolver -> [Int] -> Config -> Bool
noString :: SMTSolver -> [Int] -> Config -> Bool
noString SMTSolver
smt [Int]
v Config
cfg
  =  Config -> Bool
stringTheory Config
cfg
  Bool -> Bool -> Bool
&& Bool -> Bool
not (SMTSolver
smt forall a. Eq a => a -> a -> Bool
== SMTSolver
Z3 Bool -> Bool -> Bool
&& ([Int]
v forall a. Ord a => a -> a -> Bool
>= [Int
4, Int
4, Int
2]))

-----------------------------------------------------------------------------
-- | 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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 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 :: [Char]
_msg        = [Char]
"smtDecl: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Response -> Bool
ans 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 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 forall a b. (a -> b) -> a -> b
$
        Symbol -> [(Symbol, SmtSort)] -> SmtSort -> Expr -> Command
DefineFunc
          Symbol
name
          (forall a b. (a -> b) -> [a] -> [b]
map (Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env 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 :: Text
cmdText = {-# SCC "asyncCommand-runSmt2" #-} Builder -> Text
Builder.toLazyText forall a b. (a -> b) -> a -> b
$ forall a. SMTLIB2 a => SymEnv -> a -> Builder
runSmt2 SymEnv
env Command
cmd
  TVar Builder -> Text -> IO ()
asyncPutStrLn (Context -> TVar Builder
ctxTVar Context
me) Text
cmdText
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> Text -> IO ()
`LTIO.hPutStrLn` Text
cmdText) (Context -> Maybe Handle
ctxLog Context
me)
  where
    asyncPutStrLn :: TVar Builder.Builder -> LT.Text -> IO ()
    asyncPutStrLn :: TVar Builder -> Text -> IO ()
asyncPutStrLn TVar Builder
tv Text
t = forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$
      forall a. TVar a -> (a -> a) -> STM ()
modifyTVar TVar Builder
tv (forall a. Monoid a => a -> a -> a
`mappend` (Text -> Builder
Builder.fromLazyText Text
t forall a. Monoid a => a -> a -> a
`mappend` forall a. IsString a => [Char] -> a
Builder.fromString [Char]
"\n"))

smtAssertAsync :: Context -> Expr -> IO ()
smtAssertAsync :: Context -> Expr -> IO ()
smtAssertAsync Context
me Expr
p  = Context -> Command -> IO ()
asyncCommand Context
me forall a b. (a -> b) -> a -> b
$ Maybe Int -> Expr -> Command
Assert 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 :: forall a. SrcSpan -> Context -> [Char] -> IO a -> IO a
smtBracketAsyncAt SrcSpan
sp Context
x [Char]
y IO a
z = forall a. Context -> [Char] -> IO a -> IO a
smtBracketAsync Context
x [Char]
y IO a
z forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` forall a. SrcSpan -> Error -> a
dieAt SrcSpan
sp

smtBracketAsync :: Context -> String -> IO a -> IO a
smtBracketAsync :: forall a. Context -> [Char] -> IO a -> IO a
smtBracketAsync Context
me [Char]
_msg IO a
a   = do
  Context -> IO ()
smtPushAsync Context
me
  a
r <- IO a
a
  Context -> IO ()
smtPopAsync Context
me
  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 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 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 :: forall a. SrcSpan -> Context -> [Char] -> IO a -> IO a
smtBracketAt SrcSpan
sp Context
x [Char]
y IO a
z = forall a. Context -> [Char] -> IO a -> IO a
smtBracket Context
x [Char]
y IO a
z forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` forall a. SrcSpan -> Error -> a
dieAt SrcSpan
sp

smtBracket :: Context -> String -> IO a -> IO a
smtBracket :: forall a. Context -> [Char] -> IO a -> IO a
smtBracket Context
me [Char]
_msg IO a
a   = do
  Context -> IO ()
smtPush Context
me
  a
r <- IO a
a
  Context -> IO ()
smtPop Context
me
  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       = forall a. Error -> a
die forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
dummySpan forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text ([Char]
"crash: SMTLIB2 respSat = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Response
r)

interact' :: Context -> Command -> IO ()
interact' :: Context -> Command -> IO ()
interact' Context
me Command
cmd  = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ Context -> Command -> IO Response
command Context
me Command
cmd


makeTimeout :: Config -> [LT.Text]
makeTimeout :: Config -> [Text]
makeTimeout Config
cfg
  | Just Int
i <- Config -> Maybe Int
smtTimeout Config
cfg = [ [Char] -> Text
LT.pack ([Char]
"\n(set-option :timeout " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i forall a. [a] -> [a] -> [a]
++ [Char]
")\n")]
  | Bool
otherwise                = [Text
""]


makeMbqi :: Config -> [LT.Text]
makeMbqi :: Config -> [Text]
makeMbqi Config
cfg
  | Config -> Bool
gradual Config
cfg = [Text
""]
  | Bool
otherwise   = [Text
"\n(set-option :smt.mbqi false)"]

z3_options :: [LT.Text]
z3_options :: [Text]
z3_options
  = [ Text
"(set-option :auto-config false)"
    , Text
"(set-option :model true)" ]



--------------------------------------------------------------------------------
declare :: Context -> IO ()
--------------------------------------------------------------------------------
declare :: Context -> IO ()
declare Context
me = do
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[DataDecl]]
dss    forall a b. (a -> b) -> a -> b
$           Context -> [DataDecl] -> IO ()
smtDataDecl Context
me
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Symbol, Sort)]
thyXTs forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ Context -> Symbol -> Sort -> IO ()
smtDecl     Context
me
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Symbol, Sort)]
qryXTs forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ Context -> Symbol -> Sort -> IO ()
smtDecl     Context
me
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Text, ([SmtSort], SmtSort))]
ats    forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ Context -> Text -> ([SmtSort], SmtSort) -> IO ()
smtFuncDecl Context
me
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ListNE Expr]
ess    forall a b. (a -> b) -> a -> b
$           Context -> ListNE Expr -> IO ()
smtDistinct Context
me
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ListNE Expr
axs    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        = forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> SEnv Sort
F.seLits 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     =                    forall a. (a -> Bool) -> [a] -> [a]
filter (forall {b}. Int -> (Symbol, b) -> Bool
isKind Int
1) [(Symbol, Sort)]
xts
    qryXTs :: [(Symbol, Sort)]
qryXTs     = forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd forall {a}. Elaborate a => a -> a
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter (forall {b}. Int -> (Symbol, b) -> Bool
isKind Int
2) [(Symbol, Sort)]
xts
    isKind :: Int -> (Symbol, b) -> Bool
isKind Int
n   = (Int
n forall a. Eq a => a -> a -> Bool
==)  forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> Symbol -> Int
symKind SymEnv
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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         = forall a. Elaborate a => Located [Char] -> SymEnv -> a -> a
elaborate    Located [Char]
"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) <- forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv Sort
env ]
 where
  tx :: Sort -> Sort
tx t :: Sort
t@(FObj Symbol
a) = forall a. a -> Maybe a -> a
fromMaybe Sort
t (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv 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       , forall {b}. (SmtSort, b) -> ([SmtSort], b)
appSort FuncSort
t) | FuncSort
t <- [FuncSort]
ts]
                 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]
                 forall a. [a] -> [a] -> [a]
++ [(Symbol -> FuncSort -> Text
var Symbol
lambdaName FuncSort
t       , forall {a}. (a, a) -> ([a], SmtSort)
lamSort FuncSort
t) | FuncSort
t <- [FuncSort]
ts]
                 forall a. [a] -> [a] -> [a]
++ [(Symbol -> FuncSort -> Text
var (Int -> Symbol
lamArgSymbol Int
i) FuncSort
t , 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         = forall a. PPrint a => Symbol -> SymEnv -> a -> FuncSort -> Text
F.symbolAtSmtName Symbol
n SymEnv
env ()
    ts :: [FuncSort]
ts            = 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 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             = forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Sort
t, 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Bool
F.isFunctionSortedReft 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)