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

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

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

    -- * Query API
    , smtDecl
    , smtDecls
    , smtDefineFunc
    , smtAssert
    , smtFuncDecl
    , smtAssertAxiom
    , smtCheckUnsat
    , smtCheckSat
    , smtBracket, smtBracketAt
    , smtDistinct
    , smtPush, smtPop

    -- * Check Validity
    , checkValid
    , checkValid'
    , checkValidWithContext
    , checkValids

    ) where

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.ByteString.Builder (Builder)
import qualified Data.ByteString.Builder as BS
import qualified Data.ByteString.Lazy as LBS
import qualified Data.ByteString.Lazy.Char8 as Char8
import           Data.Char
import qualified Data.HashMap.Strict      as M
import           Data.Maybe              (fromMaybe)
import qualified Data.Text                as T
import qualified Data.Text.Encoding       as TE
import qualified Data.Text.IO
-- import           Data.Text.Format
import qualified Data.Text.Lazy.IO        as LTIO
import           System.Directory
import           System.Console.CmdArgs.Verbosity
import           System.FilePath
import           System.IO
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)
import qualified SMTLIB.Backends
import qualified SMTLIB.Backends.Process as Process
import qualified Language.Fixpoint.Conditional.Z3 as Conditional.Z3
import Control.Concurrent.Async (async)

{-
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 Ctx {Bool
Maybe Handle
IO ()
Solver
SymEnv
ctxSymEnv :: Context -> SymEnv
ctxVerbose :: Context -> Bool
ctxLog :: Context -> Maybe Handle
ctxClose :: Context -> IO ()
ctxSolver :: Context -> Solver
ctxSymEnv :: SymEnv
ctxVerbose :: Bool
ctxLog :: Maybe Handle
ctxClose :: IO ()
ctxSolver :: Solver
..} !Command
cmd       = do
  -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
  --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe Handle
ctxLog forall a b. (a -> b) -> a -> b
$ \Handle
h -> do
    Handle -> Builder -> IO ()
BS.hPutBuilder Handle
h Builder
cmdBS
    Handle -> ByteString -> IO ()
LBS.hPutStr Handle
h ByteString
"\n"
  case Command
cmd of
    Command
CheckSat   -> IO Response
commandRaw
    GetValue [Symbol]
_ -> IO Response
commandRaw
    Command
_          -> Solver -> Builder -> IO ()
SMTLIB.Backends.command_ Solver
ctxSolver Builder
cmdBS forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Response
Ok
  where
    commandRaw :: IO Response
commandRaw      = do
      ByteString
resp <- Solver -> Builder -> IO ByteString
SMTLIB.Backends.command Solver
ctxSolver Builder
cmdBS
      let respTxt :: Text
respTxt =
            OnDecodeError -> ByteString -> Text
TE.decodeUtf8With (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Char
' ') forall a b. (a -> b) -> a -> b
$
            ByteString -> ByteString
LBS.toStrict ByteString
resp
      Text -> IO Response
parse Text
respTxt
    cmdBS :: Builder
cmdBS = {-# SCC "Command-runSmt2" #-} forall a. SMTLIB2 a => SymEnv -> a -> Builder
runSmt2 SymEnv
ctxSymEnv Command
cmd
    parse :: Text -> IO Response
parse Text
resp      = do
      case forall a. Parser a -> Text -> Either [Char] a
A.parseOnly SmtParser Response
responseP Text
resp of
        Left [Char]
e  -> forall a. HasCallStack => [Char] -> a
Misc.errorstar forall a b. (a -> b) -> a -> b
$ [Char]
"SMTREAD:" forall a. [a] -> [a] -> [a]
++ [Char]
e
        Right Response
r -> do
          let textResponse :: Text
textResponse = Text
"; SMT Says: " forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (forall a. Show a => a -> [Char]
show Response
r)
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe Handle
ctxLog forall a b. (a -> b) -> a -> b
$ \Handle
h ->
            Handle -> Text -> IO ()
Data.Text.IO.hPutStrLn Handle
h Text
textResponse
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ctxVerbose forall a b. (a -> b) -> a -> b
$
            Text -> IO ()
Data.Text.IO.putStrLn Text
textResponse
          forall (m :: * -> *) a. Monad m => a -> m a
return Response
r

smtSetMbqi :: Context -> IO ()
smtSetMbqi :: Context -> IO ()
smtSetMbqi Context
me = Context -> Command -> IO ()
interact' Context
me Command
SetMbqi

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

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

--------------------------------------------------------------------------
makeContext :: Config -> FilePath -> IO Context
--------------------------------------------------------------------------
makeContext :: Config -> [Char] -> IO Context
makeContext Config
cfg [Char]
f
  = do 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
1024 forall a. Num a => a -> a -> a
* Int
1024 forall a. Num a => a -> a -> a
* Int
64
       Context
me   <- Config -> Maybe Handle -> IO Context
makeContext' Config
cfg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Handle
hLog
       [Builder]
pre  <- Config -> SMTSolver -> Context -> IO [Builder]
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_ (Solver -> Builder -> IO ()
SMTLIB.Backends.command_ (Context -> Solver
ctxSolver Context
me)) [Builder]
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 -> Maybe Handle -> IO Context
makeContext' Config
cfg forall a. Maybe a
Nothing
       [Builder]
pre <- Config -> SMTSolver -> Context -> IO [Builder]
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_ (Solver -> Builder -> IO ()
SMTLIB.Backends.command_ (Context -> Solver
ctxSolver Context
me)) [Builder]
pre
       forall (m :: * -> *) a. Monad m => a -> m a
return Context
me

makeProcess
  :: Maybe Handle
  -> Process.Config
  -> IO (SMTLIB.Backends.Backend, IO ())
makeProcess :: Maybe Handle -> Config -> IO (Backend, IO ())
makeProcess Maybe Handle
ctxLog Config
cfg
  = do handle :: Handle
handle@Process.Handle {hMaybeErr :: Handle -> Maybe Handle
hMaybeErr = Just Handle
hErr, Handle
ProcessHandle
process :: Handle -> ProcessHandle
hIn :: Handle -> Handle
hOut :: Handle -> Handle
hOut :: Handle
hIn :: Handle
process :: ProcessHandle
..} <- Config -> IO Handle
Process.new Config
cfg
       case Maybe Handle
ctxLog of
         Maybe Handle
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
         Just Handle
hLog -> forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ 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
           (do Text
err <- Handle -> IO Text
LTIO.hGetLine Handle
hErr
               Handle -> Text -> IO ()
LTIO.hPutStrLn Handle
hLog forall a b. (a -> b) -> a -> b
$ Text
"OOPS, SMT solver error:" forall a. Semigroup a => a -> a -> a
<> Text
err
           ) forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` \ SomeException {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
       let backend :: Backend
backend = Handle -> Backend
Process.toBackend Handle
handle
       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
1024 forall a. Num a => a -> a -> a
* Int
1024 forall 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
1024 forall a. Num a => a -> a -> a
* Int
1024 forall a. Num a => a -> a -> a
* Int
64
       forall (m :: * -> *) a. Monad m => a -> m a
return (Backend
backend, Handle -> IO ()
Process.close Handle
handle)

makeContext' :: Config -> Maybe Handle -> IO Context
makeContext' :: Config -> Maybe Handle -> IO Context
makeContext' Config
cfg Maybe Handle
ctxLog
  = do (Backend
backend, IO ()
closeIO) <- case Config -> SMTSolver
solver Config
cfg of
         SMTSolver
Z3      ->
           {- "z3 -smt2 -in"                   -}
           {- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}
           {- "z3 -smtc -in MBQI=false"        -}
           Maybe Handle -> Config -> IO (Backend, IO ())
makeProcess Maybe Handle
ctxLog forall a b. (a -> b) -> a -> b
$ Config
Process.defaultConfig
                             { exe :: [Char]
Process.exe = [Char]
"z3"
                             , args :: [[Char]]
Process.args = [[Char]
"-smt2", [Char]
"-in"] }
         SMTSolver
Z3mem   -> forall a. IO a
Conditional.Z3.makeZ3
         SMTSolver
Mathsat -> Maybe Handle -> Config -> IO (Backend, IO ())
makeProcess Maybe Handle
ctxLog forall a b. (a -> b) -> a -> b
$ Config
Process.defaultConfig
                             { exe :: [Char]
Process.exe = [Char]
"mathsat"
                             , args :: [[Char]]
Process.args = [[Char]
"-input=smt2"] }
         SMTSolver
Cvc4    -> Maybe Handle -> Config -> IO (Backend, IO ())
makeProcess Maybe Handle
ctxLog forall a b. (a -> b) -> a -> b
$
                      Config
Process.defaultConfig
                             { exe :: [Char]
Process.exe = [Char]
"cvc4"
                             , args :: [[Char]]
Process.args = [[Char]
"--incremental", [Char]
"-L", [Char]
"smtlib2"] }
       Solver
solver <- QueuingFlag -> Backend -> IO Solver
SMTLIB.Backends.initSolver QueuingFlag
SMTLIB.Backends.Queuing Backend
backend
       Bool
loud <- IO Bool
isLoud
       forall (m :: * -> *) a. Monad m => a -> m a
return Ctx { ctxSolver :: Solver
ctxSolver  = Solver
solver
                  , ctxClose :: IO ()
ctxClose   = IO ()
closeIO
                  , ctxLog :: Maybe Handle
ctxLog     = Maybe Handle
ctxLog
                  , ctxVerbose :: Bool
ctxVerbose = Bool
loud
                  , ctxSymEnv :: SymEnv
ctxSymEnv  = forall a. Monoid a => a
mempty
                  }

-- | Close file handles and release the solver backend's resources.
cleanupContext :: Context -> IO ()
cleanupContext :: Context -> IO ()
cleanupContext Ctx {Bool
Maybe Handle
IO ()
Solver
SymEnv
ctxSymEnv :: SymEnv
ctxVerbose :: Bool
ctxLog :: Maybe Handle
ctxClose :: IO ()
ctxSolver :: Solver
ctxSymEnv :: Context -> SymEnv
ctxVerbose :: Context -> Bool
ctxLog :: Context -> Maybe Handle
ctxClose :: Context -> IO ()
ctxSolver :: Context -> Solver
..} = do
  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
  IO ()
ctxClose

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)

smtPreamble :: Config -> SMTSolver -> Context -> IO [Builder]
smtPreamble :: Config -> SMTSolver -> Context -> IO [Builder]
smtPreamble Config
cfg SMTSolver
s Context
me
  | SMTSolver
s forall a. Eq a => a -> a -> Bool
== SMTSolver
Z3 Bool -> Bool -> Bool
|| SMTSolver
s forall a. Eq a => a -> a -> Bool
== SMTSolver
Z3mem
    = 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
$ [Builder]
z3_options forall a. [a] -> [a] -> [a]
++ Config -> [Builder]
makeMbqi Config
cfg forall a. [a] -> [a] -> [a]
++ Config -> [Builder]
makeTimeout Config
cfg forall a. [a] -> [a] -> [a]
++ Config -> SMTSolver -> [Builder]
Thy.preamble Config
cfg SMTSolver
Z3
  | Bool
otherwise
    = 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 -> [Builder]
Thy.preamble Config
cfg SMTSolver
s)

getZ3Version :: Context -> IO [Int]
getZ3Version :: Context -> IO [Int]
getZ3Version Context
me
  = do -- resp is like (:version "4.8.15")
       ByteString
resp <- Solver -> Builder -> IO ByteString
SMTLIB.Backends.command (Context -> Solver
ctxSolver Context
me) Builder
"(get-info :version)"
       case Char -> ByteString -> [ByteString]
Char8.split Char
'"' ByteString
resp of
         ByteString
_:ByteString
rText:[ByteString]
_ -> do
           -- strip off potential " - build hashcode ..." suffix
           let vText :: ByteString
vText = (Char -> Bool) -> ByteString -> ByteString
Char8.takeWhile (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace) ByteString
rText
           let parsedComponents :: [[(a, [Char])]]
parsedComponents = [ forall a. Read a => ReadS a
reads (ByteString -> [Char]
Char8.unpack ByteString
cText) | ByteString
cText <- Char -> ByteString -> [ByteString]
Char8.split Char
'.' ByteString
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. HasCallStack => [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
             ]
         [ByteString]
xs -> forall a. HasCallStack => [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 [ByteString]
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

-----------------------------------------------------------------

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 -> [Builder]
makeTimeout :: Config -> [Builder]
makeTimeout Config
cfg
  | Just Int
i <- Config -> Maybe Int
smtTimeout Config
cfg = [ Builder
"\n(set-option :timeout " forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Int
i) forall a. Semigroup a => a -> a -> a
<> Builder
")\n"]
  | Bool
otherwise                = [Builder
""]


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

z3_options :: [Builder]
z3_options :: [Builder]
z3_options
  = [ Builder
"(set-option :auto-config false)"
    , Builder
"(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)