{-# LANGUAGE BangPatterns              #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE RecordWildCards           #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE PatternGuards             #-}
{-# LANGUAGE DoAndIfThenElse           #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use isNothing" #-}

-- | 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
    , smtAssertDecl
    , smtFuncDecl
    , smtAssertAxiom
    , smtCheckUnsat
    , smtBracket, smtBracketAt
    , smtDistinct
    , smtPush, smtPop
    , smtComment

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

    , funcSortVars

    ) where

import           Language.Fixpoint.Types.Config ( SMTSolver (..), solverFlags
                                                , Config (solver, smtTimeout, noStringTheory, save, allowHO))
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.Monad.State
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.List                (uncons)
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)
import GHC.Stack (HasCallStack)

{-
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
  :: HasCallStack => [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
checkValidWithContext :: HasCallStack => [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
checkValidWithContext [(Symbol, Sort)]
xts Expr
p Expr
q =
  String -> SmtM Bool -> SmtM Bool
forall a. String -> SmtM a -> SmtM a
smtBracket String
"checkValidWithContext" (SmtM Bool -> SmtM Bool) -> SmtM Bool -> SmtM Bool
forall a b. (a -> b) -> a -> b
$
    HasCallStack => [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
[(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
checkValid' [(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
  :: HasCallStack
  => Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid :: HasCallStack =>
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
  SmtM Bool -> Context -> IO Bool
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (HasCallStack => [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
[(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
checkValid' [(Symbol, Sort)]
xts Expr
p Expr
q) Context
me

checkValid' :: HasCallStack => [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
checkValid' :: HasCallStack => [(Symbol, Sort)] -> Expr -> Expr -> SmtM Bool
checkValid' [(Symbol, Sort)]
xts Expr
p Expr
q = do
  [(Symbol, Sort)] -> SmtM ()
smtDecls [(Symbol, Sort)]
xts
  HasCallStack => Expr -> SmtM ()
Expr -> SmtM ()
smtAssertDecl (Expr -> SmtM ()) -> Expr -> SmtM ()
forall a b. (a -> b) -> a -> b
$ ListNE Expr -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd [Expr
p, Expr -> Expr
forall v. ExprV v -> ExprV v
PNot Expr
q]
  SmtM Bool
HasCallStack => SmtM Bool
smtCheckUnsat

-- | 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
  StateT Context IO [Bool] -> Context -> IO [Bool]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ([(Symbol, Sort)] -> ListNE Expr -> StateT Context IO [Bool]
checkValids' [(Symbol, Sort)]
xts ListNE Expr
ps) Context
me

checkValids' :: [(Symbol, Sort)] -> [Expr] -> SmtM [Bool]
checkValids' :: [(Symbol, Sort)] -> ListNE Expr -> StateT Context IO [Bool]
checkValids' [(Symbol, Sort)]
xts ListNE Expr
ps = do
  [(Symbol, Sort)] -> SmtM ()
smtDecls [(Symbol, Sort)]
xts
  ListNE Expr -> (Expr -> SmtM Bool) -> StateT Context IO [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ListNE Expr
ps ((Expr -> SmtM Bool) -> StateT Context IO [Bool])
-> (Expr -> SmtM Bool) -> StateT Context IO [Bool]
forall a b. (a -> b) -> a -> b
$ \Expr
p ->
     String -> SmtM Bool -> SmtM Bool
forall a. String -> SmtM a -> SmtM a
smtBracket String
"checkValids" (SmtM Bool -> SmtM Bool) -> SmtM Bool -> SmtM Bool
forall a b. (a -> b) -> a -> b
$
       Expr -> SmtM ()
smtAssert (Expr -> Expr
forall v. ExprV v -> ExprV v
PNot Expr
p) SmtM () -> SmtM Bool -> SmtM Bool
forall a b.
StateT Context IO a -> StateT Context IO b -> StateT Context IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SmtM Bool
HasCallStack => SmtM Bool
smtCheckUnsat

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

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

commandRaw :: Maybe Handle -> SMTLIB.Backends.Solver -> Bool -> Builder -> IO Response
commandRaw :: Maybe Handle -> Solver -> Bool -> Builder -> IO Response
commandRaw Maybe Handle
ctxLog Solver
ctxSolver Bool
ctxVerbose Builder
cmdBS = do
  ByteString
resp <- Solver -> Builder -> IO ByteString
SMTLIB.Backends.command Solver
ctxSolver Builder
cmdBS
  let respTxt :: Text
respTxt =
        OnDecodeError -> ByteString -> Text
TE.decodeUtf8With ((Maybe Word8 -> Maybe Char) -> OnDecodeError
forall a b. a -> b -> a
const ((Maybe Word8 -> Maybe Char) -> OnDecodeError)
-> (Maybe Word8 -> Maybe Char) -> OnDecodeError
forall a b. (a -> b) -> a -> b
$ Maybe Char -> Maybe Word8 -> Maybe Char
forall a b. a -> b -> a
const (Maybe Char -> Maybe Word8 -> Maybe Char)
-> Maybe Char -> Maybe Word8 -> Maybe Char
forall a b. (a -> b) -> a -> b
$ Char -> Maybe Char
forall a. a -> Maybe a
Just Char
' ') (ByteString -> Text) -> ByteString -> Text
forall a b. (a -> b) -> a -> b
$
        ByteString -> ByteString
LBS.toStrict ByteString
resp
  case Parser Response -> Text -> Either String Response
forall a. Parser a -> Text -> Either String a
A.parseOnly Parser Response
responseP Text
respTxt of
    Left String
e  -> String -> IO Response
forall a. HasCallStack => 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
      let textResponse :: Text
textResponse = Text
"; SMT Says: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Response -> String
forall a. Show a => a -> String
show Response
r)
      Maybe Handle -> (Handle -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe Handle
ctxLog ((Handle -> IO ()) -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle
h ->
        Handle -> Text -> IO ()
Data.Text.IO.hPutStrLn Handle
h Text
textResponse
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ctxVerbose (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
        Text -> IO ()
Data.Text.IO.putStrLn Text
textResponse
      Response -> IO Response
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Response
r

--------------------------------------------------------------------------------
{-# SCC command #-}
command  :: HasCallStack => Command -> SmtM Response
--------------------------------------------------------------------------------
command :: HasCallStack => Command -> SmtM Response
command !Command
cmd       = do
  -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
  --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
  Maybe Handle
ctxLog <- (Context -> Maybe Handle) -> StateT Context IO (Maybe Handle)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> Maybe Handle
ctxLog
  Solver
ctxSolver <- (Context -> Solver) -> StateT Context IO Solver
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> Solver
ctxSolver
  Bool
ctxVerbose <- (Context -> Bool) -> SmtM Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> Bool
ctxVerbose
  Builder
cmdBS <- SymM Builder -> SmtM Builder
forall a. SymM a -> SmtM a
liftSym (SymM Builder -> SmtM Builder) -> SymM Builder -> SmtM Builder
forall a b. (a -> b) -> a -> b
$ Command -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
runSmt2 Command
cmd
  Maybe Handle -> (Handle -> SmtM ()) -> SmtM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe Handle
ctxLog ((Handle -> SmtM ()) -> SmtM ()) -> (Handle -> SmtM ()) -> SmtM ()
forall a b. (a -> b) -> a -> b
$ \Handle
h -> IO () -> SmtM ()
forall (m :: * -> *) a. Monad m => m a -> StateT Context m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> SmtM ()) -> IO () -> SmtM ()
forall a b. (a -> b) -> a -> b
$ do
    Handle -> Builder -> IO ()
BS.hPutBuilder Handle
h Builder
cmdBS
    Handle -> ByteString -> IO ()
LBS.hPutStr Handle
h ByteString
"\n"
  IO Response -> SmtM Response
forall (m :: * -> *) a. Monad m => m a -> StateT Context m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Response -> SmtM Response) -> IO Response -> SmtM Response
forall a b. (a -> b) -> a -> b
$ case Command
cmd of
    Command
CheckSat   -> Maybe Handle -> Solver -> Bool -> Builder -> IO Response
commandRaw Maybe Handle
ctxLog Solver
ctxSolver Bool
ctxVerbose Builder
cmdBS
    GetValue [Symbol]
_ -> Maybe Handle -> Solver -> Bool -> Builder -> IO Response
commandRaw Maybe Handle
ctxLog Solver
ctxSolver Bool
ctxVerbose Builder
cmdBS
    Command
_          -> Solver -> Builder -> IO ()
SMTLIB.Backends.command_ Solver
ctxSolver Builder
cmdBS IO () -> IO Response -> IO Response
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Response -> IO Response
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Response
Ok

-- | A variant of `command` that accepts a pre-built command
commandB :: Builder -> SmtM Response
--------------------------------------------------------------------------------
commandB :: Builder -> SmtM Response
commandB Builder
cmdBS       = do
  Maybe Handle
ctxLog <- (Context -> Maybe Handle) -> StateT Context IO (Maybe Handle)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> Maybe Handle
ctxLog
  Solver
ctxSolver <- (Context -> Solver) -> StateT Context IO Solver
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Context -> Solver
ctxSolver
  Maybe Handle -> (Handle -> SmtM ()) -> SmtM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe Handle
ctxLog ((Handle -> SmtM ()) -> SmtM ()) -> (Handle -> SmtM ()) -> SmtM ()
forall a b. (a -> b) -> a -> b
$ \Handle
h -> IO () -> SmtM ()
forall (m :: * -> *) a. Monad m => m a -> StateT Context m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> SmtM ()) -> IO () -> SmtM ()
forall a b. (a -> b) -> a -> b
$ do
    Handle -> Builder -> IO ()
BS.hPutBuilder Handle
h Builder
cmdBS
    Handle -> ByteString -> IO ()
LBS.hPutStr Handle
h ByteString
"\n"
  IO Response -> SmtM Response
forall (m :: * -> *) a. Monad m => m a -> StateT Context m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Response -> SmtM Response) -> IO Response -> SmtM Response
forall a b. (a -> b) -> a -> b
$ Solver -> Builder -> IO ()
SMTLIB.Backends.command_ Solver
ctxSolver Builder
cmdBS IO () -> IO Response -> IO Response
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Response -> IO Response
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Response
Ok

smtSetMbqi :: SmtM ()
smtSetMbqi :: SmtM ()
smtSetMbqi = Command -> SmtM ()
interact' Command
SetMbqi

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 a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Response
sexpP
         Parser Response -> Parser Response -> Parser Response
forall a. Parser Text a -> Parser Text a -> Parser Text a
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 a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Response -> Parser Response
forall a. a -> Parser Text a
forall (m :: * -> *) a. Monad m => a -> m a
return Response
Sat
         Parser Response -> Parser Response -> Parser Response
forall a. Parser Text a -> Parser Text a -> Parser Text a
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 a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Response -> Parser Response
forall a. a -> Parser Text a
forall (m :: * -> *) a. Monad m => a -> m a
return Response
Unsat
         Parser Response -> Parser Response -> Parser Response
forall a. Parser Text a -> Parser Text a -> Parser Text a
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 a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Response -> Parser Response
forall a. a -> Parser Text a
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 a b. Parser Text a -> Parser Text b -> Parser Text b
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 a. Parser Text a -> Parser Text a -> Parser Text a
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 a b. Parser Text a -> Parser Text b -> Parser Text b
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 a b. Parser Text a -> Parser Text b -> Parser Text b
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 a b. Parser Text a -> Parser Text b -> Parser Text a
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 a b. Parser Text a -> Parser Text b -> Parser Text a
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
_ <- 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
')'
     (Symbol, Text) -> Parser Text (Symbol, Text)
forall a. a -> Parser Text a
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 a. Parser Text a -> Parser Text a -> Parser Text a
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 a b. Parser Text a -> Parser Text b -> Parser Text b
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 a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
A.char Char
')'
       Text -> Parser Text
forall a. a -> Parser Text a
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
")"

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

--------------------------------------------------------------------------
makeContext :: Config -> FilePath -> IO Context
--------------------------------------------------------------------------
makeContext :: Config -> String -> IO Context
makeContext Config
cfg String
f
  = do Maybe Handle
mb_hLog <- if Bool -> Bool
not (Config -> Bool
save Config
cfg) then Maybe Handle -> IO (Maybe Handle)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Handle
forall a. Maybe a
Nothing else do
           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
1024 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
1024 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
64
           Maybe Handle -> IO (Maybe Handle)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Handle -> IO (Maybe Handle))
-> Maybe Handle -> IO (Maybe Handle)
forall a b. (a -> b) -> a -> b
$ Handle -> Maybe Handle
forall a. a -> Maybe a
Just Handle
hLog
       Context
me   <- Config -> Maybe Handle -> IO Context
makeContext' Config
cfg Maybe Handle
mb_hLog
       [Builder]
pre  <- Config -> SMTSolver -> Context -> IO [Builder]
smtPreamble Config
cfg (Config -> SMTSolver
solver Config
cfg) Context
me
       [Builder] -> (Builder -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Builder]
pre ((Builder -> IO ()) -> IO ()) -> (Builder -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Builder
line -> do
           Solver -> Builder -> IO ()
SMTLIB.Backends.command_ (Context -> Solver
ctxSolver Context
me) Builder
line
           Maybe Handle -> (Handle -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe Handle
mb_hLog ((Handle -> IO ()) -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle
hLog -> do
               Handle -> Builder -> IO ()
BS.hPutBuilder Handle
hLog Builder
line
               Handle -> ByteString -> IO ()
LBS.hPutStr Handle
hLog ByteString
"\n"
       Context -> IO Context
forall a. a -> IO a
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 -> DefinedFuns -> IO Context
makeContextWithSEnv :: Config -> String -> SymEnv -> DefinedFuns -> IO Context
makeContextWithSEnv Config
cfg String
f SymEnv
env DefinedFuns
defns = do
  Context
ctx      <- Config -> String -> IO Context
makeContext Config
cfg String
f
  let ctx' :: Context
ctx' = Context
ctx {ctxSymEnv = env, ctxDefines = defns}
  SmtM () -> Context -> IO Context
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT SmtM ()
declare Context
ctx'

makeContextNoLog :: Config -> IO Context
makeContextNoLog :: Config -> IO Context
makeContextNoLog Config
cfg = do
  Context
me  <- Config -> Maybe Handle -> IO Context
makeContext' Config
cfg Maybe Handle
forall a. Maybe a
Nothing
  [Builder]
pre <- Config -> SMTSolver -> Context -> IO [Builder]
smtPreamble Config
cfg (Config -> SMTSolver
solver Config
cfg) Context
me
  (Builder -> IO ()) -> [Builder] -> IO ()
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
  Context -> IO Context
forall a. a -> IO a
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 handl :: Handle
handl@Process.Handle {hMaybeErr :: Handle -> Maybe Handle
hMaybeErr = Just Handle
hErr, Handle
ProcessHandle
process :: ProcessHandle
hIn :: Handle
hOut :: Handle
hOut :: Handle -> Handle
hIn :: Handle -> Handle
process :: Handle -> ProcessHandle
..} <- Config -> IO Handle
Process.new Config
cfg
       case Maybe Handle
ctxLog of
         Maybe Handle
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         Just Handle
hLog -> IO (Async ()) -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO (Async ()) -> IO ()) -> IO (Async ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ 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
           (do Text
errTxt <- Handle -> IO Text
LTIO.hGetLine Handle
hErr
               Handle -> Text -> IO ()
LTIO.hPutStrLn Handle
hLog (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Text
"OOPS, SMT solver error:" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
errTxt
           ) IO () -> (SomeException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` \ SomeException {} -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       let backend :: Backend
backend = Handle -> Backend
Process.toBackend Handle
handl
       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
1024 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
1024 Int -> 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
1024 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
1024 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
64
       (Backend, IO ()) -> IO (Backend, IO ())
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Backend
backend, Handle -> IO ()
Process.close Handle
handl)

makeContext' :: Config -> Maybe Handle -> IO Context
makeContext' :: Config -> Maybe Handle -> IO Context
makeContext' Config
cfg Maybe Handle
ctxLog
  = do let slv :: SMTSolver
slv = Config -> SMTSolver
solver Config
cfg
       (Backend
backend, IO ()
closeIO) <- case SMTSolver
slv 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 (Config -> IO (Backend, IO ())) -> Config -> IO (Backend, IO ())
forall a b. (a -> b) -> a -> b
$ Config
Process.defaultConfig
                             { Process.exe = "z3"
                             , Process.args = ["-smt2", "-in"] }
         SMTSolver
Z3mem   -> IO (Backend, IO ())
forall a. IO a
Conditional.Z3.makeZ3
         SMTSolver
Mathsat -> Maybe Handle -> Config -> IO (Backend, IO ())
makeProcess Maybe Handle
ctxLog (Config -> IO (Backend, IO ())) -> Config -> IO (Backend, IO ())
forall a b. (a -> b) -> a -> b
$ Config
Process.defaultConfig
                             { Process.exe = "mathsat"
                             , Process.args = ["-input=smt2"] }
         SMTSolver
Cvc4    -> Maybe Handle -> Config -> IO (Backend, IO ())
makeProcess Maybe Handle
ctxLog (Config -> IO (Backend, IO ())) -> Config -> IO (Backend, IO ())
forall a b. (a -> b) -> a -> b
$
                      Config
Process.defaultConfig
                             { Process.exe = "cvc4"
                             , Process.args = ["-L", "smtlib2"] }
         SMTSolver
Cvc5    -> Maybe Handle -> Config -> IO (Backend, IO ())
makeProcess Maybe Handle
ctxLog (Config -> IO (Backend, IO ())) -> Config -> IO (Backend, IO ())
forall a b. (a -> b) -> a -> b
$
                      Config
Process.defaultConfig
                             { Process.exe = "cvc5"
                             , Process.args = ["-L", "smtlib2", "--arrays-exp"] }
       Solver
solver <- QueuingFlag -> Backend -> IO Solver
SMTLIB.Backends.initSolver QueuingFlag
SMTLIB.Backends.Queuing Backend
backend
       Bool
loud <- IO Bool
isLoud
       Context -> IO Context
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Ctx { ctxSolver :: Solver
ctxSolver    = Solver
solver
                  , ctxElabF :: ElabFlags
ctxElabF     = Config -> ElabFlags
solverFlags Config
cfg
                  , ctxClose :: IO ()
ctxClose     = IO ()
closeIO
                  , ctxLog :: Maybe Handle
ctxLog       = Maybe Handle
ctxLog
                  , ctxVerbose :: Bool
ctxVerbose   = Bool
loud
                  , ctxSymEnv :: SymEnv
ctxSymEnv    = SymEnv
forall a. Monoid a => a
mempty
                  , ctxIxs :: [Int]
ctxIxs       = []
                  , ctxDefines :: DefinedFuns
ctxDefines   = DefinedFuns
forall a. Monoid a => a
mempty
                  -- This is a heurstic to avoid generating large sequences of unused `lam_arg` symbols
                  -- when there's no higher-order reasoning. It might require some tuning on larger codebases
                  -- if `unknown function/constant lam_arg$XXX` errors are encountered.
                  , ctxLams :: Bool
ctxLams      = Config -> Bool
allowHO Config
cfg
                  , config :: Config
config       = Config
cfg
                  }

-- | Close file handles and release the solver backend's resources.
cleanupContext :: Context -> IO ()
cleanupContext :: Context -> IO ()
cleanupContext Ctx {Bool
[Int]
Maybe Handle
IO ()
Solver
ElabFlags
Config
SymEnv
DefinedFuns
ctxLog :: Context -> Maybe Handle
ctxSolver :: Context -> Solver
ctxVerbose :: Context -> Bool
ctxSymEnv :: Context -> SymEnv
ctxDefines :: Context -> DefinedFuns
ctxElabF :: Context -> ElabFlags
ctxClose :: Context -> IO ()
ctxIxs :: Context -> [Int]
ctxLams :: Context -> Bool
config :: Context -> Config
ctxSolver :: Solver
ctxElabF :: ElabFlags
ctxClose :: IO ()
ctxLog :: Maybe Handle
ctxVerbose :: Bool
ctxSymEnv :: SymEnv
ctxIxs :: [Int]
ctxDefines :: DefinedFuns
ctxLams :: Bool
config :: Config
..} = do
  IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (String -> Handle -> IO ()
hCloseMe String
"ctxLog") Maybe Handle
ctxLog
  IO ()
ctxClose

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)

smtPreamble :: Config -> SMTSolver -> Context -> IO [Builder]
smtPreamble :: Config -> SMTSolver -> Context -> IO [Builder]
smtPreamble Config
cfg SMTSolver
s Context
me
  | SMTSolver
s SMTSolver -> SMTSolver -> Bool
forall a. Eq a => a -> a -> Bool
== SMTSolver
Z3 Bool -> Bool -> Bool
|| SMTSolver
s SMTSolver -> SMTSolver -> Bool
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
         [Builder] -> IO [Builder]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Builder] -> IO [Builder]) -> [Builder] -> IO [Builder]
forall a b. (a -> b) -> a -> b
$ [Builder]
forall {a}. IsString a => [a]
makeMbqi [Builder] -> [Builder] -> [Builder]
forall a. [a] -> [a] -> [a]
++ Config -> [Builder]
makeTimeout Config
cfg [Builder] -> [Builder] -> [Builder]
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 IO () -> IO [Builder] -> IO [Builder]
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Builder] -> IO [Builder]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Config -> SMTSolver -> [Builder]
Thy.preamble Config
cfg SMTSolver
s)
  where
    makeMbqi :: [a]
makeMbqi = [a
"\n(set-option :smt.mbqi false)"]

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 (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace) ByteString
rText
           let parsedComponents :: [[(a, String)]]
parsedComponents = [ ReadS a
forall a. Read a => ReadS a
reads (ByteString -> String
Char8.unpack ByteString
cText) | ByteString
cText <- Char -> ByteString -> [ByteString]
Char8.split Char
'.' ByteString
vText ]
           [IO Int] -> IO [Int]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
             [ case [(Int, String)]
pComponent of
                 [(Int
c, String
"")] -> Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
c
                 [(Int, String)]
xs -> String -> IO Int
forall a. HasCallStack => String -> a
error (String -> IO Int) -> String -> IO Int
forall a b. (a -> b) -> a -> b
$ String
"Can't parse z3 version: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, String)] -> String
forall a. Show a => a -> String
show [(Int, String)]
xs
             | [(Int, String)]
pComponent <- [[(Int, String)]]
forall {a}. Read a => [[(a, String)]]
parsedComponents
             ]
         [ByteString]
xs -> String -> IO [Int]
forall a. HasCallStack => String -> a
error (String -> IO [Int]) -> String -> IO [Int]
forall a b. (a -> b) -> a -> b
$ String
"Can't parse z3 (get-info :version): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [ByteString] -> String
forall a. Show a => a -> String
show [ByteString]
xs

checkValidStringFlag :: SMTSolver -> [Int] -> Config -> IO ()
checkValidStringFlag :: SMTSolver -> [Int] -> Config -> IO ()
checkValidStringFlag SMTSolver
smt [Int]
v Config
cfg
  = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTSolver -> [Int] -> Config -> Bool
noString SMTSolver
smt [Int]
v Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
      Error -> IO ()
forall a. HasCallStack => 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 -> [Int] -> Config -> Bool
noString :: SMTSolver -> [Int] -> Config -> Bool
noString SMTSolver
smt [Int]
v Config
cfg
  =  Bool -> Bool
not (Config -> Bool
noStringTheory Config
cfg)
  Bool -> Bool -> Bool
&& Bool -> Bool
not (SMTSolver
smt SMTSolver -> SMTSolver -> Bool
forall a. Eq a => a -> a -> Bool
== SMTSolver
Cvc5 Bool -> Bool -> Bool
|| (SMTSolver
smt SMTSolver -> SMTSolver -> Bool
forall a. Eq a => a -> a -> Bool
== SMTSolver
Z3 Bool -> Bool -> Bool
&& ([Int]
v [Int] -> [Int] -> Bool
forall a. Ord a => a -> a -> Bool
>= [Int
4, Int
4, Int
2])))
-----------------------------------------------------------------------------
-- | SMT Commands -----------------------------------------------------------
-----------------------------------------------------------------------------

smtPush, smtPop :: SmtM ()
smtPush :: SmtM ()
smtPush = Command -> SmtM ()
interact' Command
Push
smtPop :: SmtM ()
smtPop  = Command -> SmtM ()
interact' Command
Pop

smtComment :: T.Text -> SmtM ()
smtComment :: Text -> SmtM ()
smtComment Text
t = Command -> SmtM ()
interact' (Text -> Command
Comment Text
t)

smtDecls :: [(Symbol, Sort)] -> SmtM ()
smtDecls :: [(Symbol, Sort)] -> SmtM ()
smtDecls = ((Symbol, Sort) -> SmtM ()) -> [(Symbol, Sort)] -> SmtM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((Symbol, Sort) -> SmtM ()) -> [(Symbol, Sort)] -> SmtM ())
-> ((Symbol, Sort) -> SmtM ()) -> [(Symbol, Sort)] -> SmtM ()
forall a b. (a -> b) -> a -> b
$ (Symbol -> Sort -> SmtM ()) -> (Symbol, Sort) -> SmtM ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Sort -> SmtM ()
smtDecl

smtDecl :: Symbol -> Sort -> SmtM ()
smtDecl :: Symbol -> Sort -> SmtM ()
smtDecl Symbol
x Sort
t = do
  Context
me <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  let env :: SEnv DataDecl
env = SymEnv -> SEnv DataDecl
seData (Context -> SymEnv
ctxSymEnv Context
me)
  let 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
  let out' :: SmtSort
out' = Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env     Sort
out
  Command -> SmtM ()
interact' (String -> Command -> Command
forall a. PPrint a => String -> a -> a
notracepp String
_msg (Command -> Command) -> Command -> Command
forall a b. (a -> b) -> a -> b
$ Text -> [SmtSort] -> SmtSort -> Command
Declare (Symbol -> Text
symbolSafeText Symbol
x) [SmtSort]
ins' SmtSort
out')
  where
    ([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)

smtFuncDecl :: T.Text -> ([SmtSort],  SmtSort) -> SmtM ()
smtFuncDecl :: Text -> ([SmtSort], SmtSort) -> SmtM ()
smtFuncDecl Text
x ([SmtSort]
ts, SmtSort
t) = Command -> SmtM ()
interact' (Text -> [SmtSort] -> SmtSort -> Command
Declare Text
x [SmtSort]
ts SmtSort
t)

smtDataDecl :: [DataDecl] -> SmtM ()
smtDataDecl :: [DataDecl] -> SmtM ()
smtDataDecl [DataDecl]
ds = Command -> SmtM ()
interact' ([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)

smtAssert :: Expr -> SmtM ()
smtAssert :: Expr -> SmtM ()
smtAssert Expr
p = Command -> SmtM ()
interact' (Maybe Int -> Expr -> Command
Assert Maybe Int
forall a. Maybe a
Nothing Expr
p)

-- the following three functions will emit additional `apply`,
-- `coerce`, and `lambda` symbols for fresh function sorts as needed
smtAssertDecl :: HasCallStack => Expr -> SmtM ()
smtAssertDecl :: HasCallStack => Expr -> SmtM ()
smtAssertDecl Expr
p = HasCallStack => Command -> SmtM ()
Command -> SmtM ()
interactDecl' (Maybe Int -> Expr -> Command
Assert Maybe Int
forall a. Maybe a
Nothing Expr
p)

smtDefineEqn :: Equation -> SmtM ()
smtDefineEqn :: Equation -> SmtM ()
smtDefineEqn Equ {Bool
[(Symbol, Sort)]
Symbol
Sort
Expr
eqName :: Symbol
eqArgs :: [(Symbol, Sort)]
eqBody :: Expr
eqSort :: Sort
eqRec :: Bool
eqRec :: forall v. EquationV v -> Bool
eqSort :: forall v. EquationV v -> Sort
eqBody :: forall v. EquationV v -> ExprV v
eqArgs :: forall v. EquationV v -> [(Symbol, Sort)]
eqName :: forall v. EquationV v -> Symbol
..} = Symbol -> [(Symbol, Sort)] -> Sort -> Expr -> SmtM ()
smtDefineFunc Symbol
eqName [(Symbol, Sort)]
eqArgs Sort
eqSort Expr
eqBody

smtDefineFunc :: Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> SmtM ()
smtDefineFunc :: Symbol -> [(Symbol, Sort)] -> Sort -> Expr -> SmtM ()
smtDefineFunc Symbol
name [(Symbol, Sort)]
symList Sort
rsort Expr
e =
  do SEnv DataDecl
env <- (Context -> SEnv DataDecl) -> StateT Context IO (SEnv DataDecl)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SymEnv -> SEnv DataDecl
seData (SymEnv -> SEnv DataDecl)
-> (Context -> SymEnv) -> Context -> SEnv DataDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> SymEnv
ctxSymEnv)
     HasCallStack => Command -> SmtM ()
Command -> SmtM ()
interactDecl' (Command -> SmtM ()) -> Command -> SmtM ()
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)]
symList)
          (Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env Sort
rsort)
          Expr
e

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

smtAssertAxiom :: Triggered Expr -> SmtM ()
smtAssertAxiom :: Triggered Expr -> SmtM ()
smtAssertAxiom Triggered Expr
p  = Command -> SmtM ()
interact' (Triggered Expr -> Command
AssertAx Triggered Expr
p)

smtDistinct :: [Expr] -> SmtM ()
smtDistinct :: ListNE Expr -> SmtM ()
smtDistinct ListNE Expr
az = Command -> SmtM ()
interact' (ListNE Expr -> Command
Distinct ListNE Expr
az)

smtCheckUnsat :: HasCallStack => SmtM Bool
smtCheckUnsat :: HasCallStack => SmtM Bool
smtCheckUnsat = HasCallStack => Response -> Bool
Response -> Bool
respSat (Response -> Bool) -> SmtM Response -> SmtM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack => Command -> SmtM Response
Command -> SmtM Response
command Command
CheckSat

smtBracketAt :: SrcSpan -> String -> SmtM a -> SmtM a
smtBracketAt :: forall a. SrcSpan -> String -> SmtM a -> SmtM a
smtBracketAt SrcSpan
sp String
_msg SmtM a
a =
  String -> SmtM a -> SmtM a
forall a. String -> SmtM a -> SmtM a
smtBracket String
_msg SmtM a
a SmtM a -> (Error -> IO a) -> SmtM a
forall e a. Exception e => SmtM a -> (e -> IO a) -> SmtM a
`catchSMT` SrcSpan -> Error -> IO a
forall a. SrcSpan -> Error -> a
dieAt SrcSpan
sp

-- | `smtBracket` adds a new level to the apply stack and saves the last fresh index
--   on the index stack before the action, and reverts these changes after the action.
smtBracket :: String -> SmtM a -> SmtM a
smtBracket :: forall a. String -> SmtM a -> SmtM a
smtBracket String
msg SmtM a
a = do
  Text -> SmtM ()
smtComment (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
"smtBracket - start: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg)
  SmtM ()
smtPush
  (Context -> Context) -> SmtM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> SmtM ())
-> (Context -> Context) -> SmtM ()
forall a b. (a -> b) -> a -> b
$ \Context
ctx ->
    let env :: SymEnv
env = Context -> SymEnv
ctxSymEnv Context
ctx in
    Context
ctx { ctxSymEnv = env { seAppls = pushAppls (seAppls env) }
        , ctxIxs = seIx env : ctxIxs ctx}
  a
r <- SmtM a
a
  SmtM ()
smtPop
  Text -> SmtM ()
smtComment (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
"smtBracket - end: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg)
  (Context -> Context) -> SmtM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Context -> Context) -> SmtM ())
-> (Context -> Context) -> SmtM ()
forall a b. (a -> b) -> a -> b
$ \Context
ctx ->
    let env :: SymEnv
env = Context -> SymEnv
ctxSymEnv Context
ctx
        (Int
i , [Int]
is) = (Int, [Int]) -> Maybe (Int, [Int]) -> (Int, [Int])
forall a. a -> Maybe a -> a
fromMaybe (Int
0, []) ([Int] -> Maybe (Int, [Int])
forall a. [a] -> Maybe (a, [a])
uncons ([Int] -> Maybe (Int, [Int])) -> [Int] -> Maybe (Int, [Int])
forall a b. (a -> b) -> a -> b
$ Context -> [Int]
ctxIxs Context
ctx)
      in
    Context
ctx { ctxSymEnv = env {seAppls = popAppls (seAppls env) , seIx = i}
        , ctxIxs = is}
  a -> SmtM a
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r

respSat :: HasCallStack => Response -> Bool
respSat :: HasCallStack => Response -> Bool
respSat Response
Unsat   = Bool
True
respSat Response
Sat     = Bool
False
respSat Response
Unknown = Bool
False
respSat Response
r       = Error -> Bool
forall a. HasCallStack => 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' :: Command -> SmtM ()
interact' :: Command -> SmtM ()
interact' Command
cmd  = SmtM Response -> SmtM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (SmtM Response -> SmtM ()) -> SmtM Response -> SmtM ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => Command -> SmtM Response
Command -> SmtM Response
command Command
cmd

-- | a variant of `interact'` which also emits fresh
--   `apply`, `coerce`, and `lambda` symbols
interactDecl' :: HasCallStack => Command -> SmtM ()
interactDecl' :: HasCallStack => Command -> SmtM ()
interactDecl' Command
cmd  = do
  Builder
cmdBS <- SymM Builder -> SmtM Builder
forall a. SymM a -> SmtM a
liftSym (SymM Builder -> SmtM Builder) -> SymM Builder -> SmtM Builder
forall a b. (a -> b) -> a -> b
$ Command -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
runSmt2 Command
cmd
  Context
ctx <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  let env :: SymEnv
env = Context -> SymEnv
ctxSymEnv Context
ctx
  let ats :: [(Text, ([SmtSort], SmtSort))]
ats = Bool -> SymEnv -> [(Text, ([SmtSort], SmtSort))]
funcSortVars (Context -> Bool
ctxLams Context
ctx) SymEnv
env
  [(Text, ([SmtSort], SmtSort))]
-> ((Text, ([SmtSort], SmtSort)) -> SmtM ()) -> SmtM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Text, ([SmtSort], SmtSort))]
ats (((Text, ([SmtSort], SmtSort)) -> SmtM ()) -> SmtM ())
-> ((Text, ([SmtSort], SmtSort)) -> SmtM ()) -> SmtM ()
forall a b. (a -> b) -> a -> b
$ (Text -> ([SmtSort], SmtSort) -> SmtM ())
-> (Text, ([SmtSort], SmtSort)) -> SmtM ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> ([SmtSort], SmtSort) -> SmtM ()
smtFuncDecl
  Context -> SmtM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Context
ctx {ctxSymEnv = env {seAppls = mergeTopAppls (seApplsCur env) (seAppls env), seApplsCur = M.empty} })
  SmtM Response -> SmtM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (SmtM Response -> SmtM ()) -> SmtM Response -> SmtM ()
forall a b. (a -> b) -> a -> b
$ Builder -> SmtM Response
commandB Builder
cmdBS

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


--------------------------------------------------------------------------------
declare :: SmtM ()
--------------------------------------------------------------------------------
declare :: SmtM ()
declare = do
  Context
me <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  let env :: SymEnv
env        = Context -> SymEnv
ctxSymEnv Context
me
  let xts :: [(Symbol, Sort)]
xts        = SEnv Sort -> [(Symbol, Sort)]
symbolSorts (SymEnv -> SEnv Sort
F.seSort SymEnv
env)
  let tx :: a -> a
tx         = ElabParam -> a -> a
forall a. (Elaborate a, HasCallStack) => ElabParam -> a -> a
elaborate (ElabFlags -> Located String -> SymEnv -> ElabParam
ElabParam (Context -> ElabFlags
ctxElabF Context
me) Located String
"declare" SymEnv
env)
  let 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
  let dss :: [[DataDecl]]
dss        = SymEnv -> [[DataDecl]]
dataDeclarations          SymEnv
env
  let thyXTs :: [(Symbol, Sort)]
thyXTs     =             [ (Symbol
x, Sort
t) | (Symbol
x, Sort
t) <- [(Symbol, Sort)]
xts, SymEnv -> Symbol -> Maybe Sem
symKind SymEnv
env Symbol
x Maybe Sem -> Maybe Sem -> Bool
forall a. Eq a => a -> a -> Bool
== Sem -> Maybe Sem
forall a. a -> Maybe a
Just Sem
F.Uninterp ]
  let qryXTs :: [(Symbol, Sort)]
qryXTs     = (Sort -> Sort) -> (Symbol, Sort) -> (Symbol, Sort)
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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
x, Sort
t) | (Symbol
x, Sort
t) <- [(Symbol, Sort)]
xts, SymEnv -> Symbol -> Maybe Sem
symKind SymEnv
env Symbol
x Maybe Sem -> Maybe Sem -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Sem
forall a. Maybe a
Nothing ]
  -- let isKind n   = (n ==)  . symKind env . fst
  let MkDefinedFuns [Equation]
defs = Context -> DefinedFuns
ctxDefines Context
me
  let ess :: [ListNE Expr]
ess        = [(Symbol, Sort)] -> [ListNE Expr]
distinctLiterals  [(Symbol, Sort)]
lts
  let axs :: ListNE Expr
axs        = Config -> [(Symbol, Sort)] -> ListNE Expr
Thy.axiomLiterals (Context -> Config
config Context
me) [(Symbol, Sort)]
lts
  [[DataDecl]] -> ([DataDecl] -> SmtM ()) -> SmtM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[DataDecl]]
dss              [DataDecl] -> SmtM ()
smtDataDecl
  [(Symbol, Sort)] -> ((Symbol, Sort) -> SmtM ()) -> SmtM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Symbol, Sort)]
thyXTs (((Symbol, Sort) -> SmtM ()) -> SmtM ())
-> ((Symbol, Sort) -> SmtM ()) -> SmtM ()
forall a b. (a -> b) -> a -> b
$ (Symbol -> Sort -> SmtM ()) -> (Symbol, Sort) -> SmtM ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Sort -> SmtM ()
smtDecl
  [(Symbol, Sort)] -> ((Symbol, Sort) -> SmtM ()) -> SmtM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Symbol, Sort)]
qryXTs (((Symbol, Sort) -> SmtM ()) -> SmtM ())
-> ((Symbol, Sort) -> SmtM ()) -> SmtM ()
forall a b. (a -> b) -> a -> b
$ (Symbol -> Sort -> SmtM ()) -> (Symbol, Sort) -> SmtM ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Sort -> SmtM ()
smtDecl
  [Equation] -> (Equation -> SmtM ()) -> SmtM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Equation]
defs             Equation -> SmtM ()
smtDefineEqn
  [ListNE Expr] -> (ListNE Expr -> SmtM ()) -> SmtM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ListNE Expr]
ess              ListNE Expr -> SmtM ()
smtDistinct
  ListNE Expr -> (Expr -> SmtM ()) -> SmtM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ListNE Expr
axs              Expr -> SmtM ()
smtAssert

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

-- | See 'F.seApplsCur' for explanation.
funcSortVars :: Bool -> F.SymEnv -> [(T.Text, ([F.SmtSort], F.SmtSort))]
funcSortVars :: Bool -> SymEnv -> [(Text, ([SmtSort], SmtSort))]
funcSortVars Bool
lams SymEnv
env =
    ((FuncSort, Int) -> [(Text, ([SmtSort], SmtSort))])
-> [(FuncSort, Int)] -> [(Text, ([SmtSort], SmtSort))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FuncSort, Int) -> [(Text, ([SmtSort], SmtSort))]
symbolsForTag ([(FuncSort, Int)] -> [(Text, ([SmtSort], SmtSort))])
-> [(FuncSort, Int)] -> [(Text, ([SmtSort], SmtSort))]
forall a b. (a -> b) -> a -> b
$ HashMap FuncSort Int -> [(FuncSort, Int)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap FuncSort Int -> [(FuncSort, Int)])
-> HashMap FuncSort Int -> [(FuncSort, Int)]
forall a b. (a -> b) -> a -> b
$ SymEnv -> HashMap FuncSort Int
F.seApplsCur SymEnv
env
  where
    symbolsForTag :: (FuncSort, Int) -> [(Text, ([SmtSort], SmtSort))]
symbolsForTag (FuncSort
t, Int
i) =
      let applySym :: Text
applySym  = Symbol -> Int -> Text
symbolAtSortIndex Symbol
applyName Int
i
          coerceSym :: Text
coerceSym = Symbol -> Int -> Text
symbolAtSortIndex Symbol
coerceName Int
i
          lamSym :: Text
lamSym    = Symbol -> Int -> Text
symbolAtSortIndex Symbol
lambdaName Int
i
          argSyms :: [(Text, ([a], SmtSort))]
argSyms   = if Bool
lams Bool -> Bool -> Bool
&& FuncSort -> SmtSort
forall a b. (a, b) -> b
snd FuncSort
t SmtSort -> SmtSort -> Bool
forall a. Eq a => a -> a -> Bool
== SmtSort
F.SInt
                        then [ (Symbol -> Int -> Text
symbolAtSortIndex (Int -> Symbol
lamArgSymbol Int
j) Int
i, FuncSort -> ([a], SmtSort)
forall {b} {b} {a}. (b, b) -> ([a], b)
argSort FuncSort
t)
                             | Int
j <- [Int
1..Int
Thy.maxLamArg] ]
                        else []
      in  (Text
applySym, FuncSort -> ([SmtSort], SmtSort)
forall {b}. (SmtSort, b) -> ([SmtSort], b)
appSort FuncSort
t)
        (Text, ([SmtSort], SmtSort))
-> [(Text, ([SmtSort], SmtSort))] -> [(Text, ([SmtSort], SmtSort))]
forall a. a -> [a] -> [a]
: (Text
coerceSym, ([FuncSort -> SmtSort
forall a b. (a, b) -> a
fst FuncSort
t], FuncSort -> SmtSort
forall a b. (a, b) -> b
snd FuncSort
t))
        (Text, ([SmtSort], SmtSort))
-> [(Text, ([SmtSort], SmtSort))] -> [(Text, ([SmtSort], SmtSort))]
forall a. a -> [a] -> [a]
: (Text
lamSym, FuncSort -> ([SmtSort], SmtSort)
forall {a}. (a, a) -> ([a], SmtSort)
lamSort FuncSort
t)
        (Text, ([SmtSort], SmtSort))
-> [(Text, ([SmtSort], SmtSort))] -> [(Text, ([SmtSort], SmtSort))]
forall a. a -> [a] -> [a]
: [(Text, ([SmtSort], SmtSort))]
forall {a}. [(Text, ([a], SmtSort))]
argSyms

    appSort :: (SmtSort, b) -> ([SmtSort], b)
appSort (SmtSort
s,b
t) = ([SmtSort
F.SInt, SmtSort
s], b
t)
    lamSort :: (a, a) -> ([a], SmtSort)
lamSort (a
s,a
t) = ([a
s, a
t], SmtSort
F.SInt)
    argSort :: (b, b) -> ([a], b)
argSort (b
s,b
_) = ([]    , b
s)

symKind :: F.SymEnv -> F.Symbol -> Maybe Sem
symKind :: SymEnv -> Symbol -> Maybe Sem
symKind SymEnv
env Symbol
x = 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

-- | `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
forall v. ReftV v
F.trueReft)
    -- _notStr          = not . (F.strSort ==) . F.sr_sort . (`F.RR` F.trueReft)