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

-- | This module contains an SMTLIB2 interface for
--   1. checking the validity, and,
--   2. computing satisfying assignments
--   for formulas.
--   By implementing a binary interface over the SMTLIB2 format defined at
--   http://www.smt-lib.org/
--   http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf

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

    -- * Query API
    , smtDecl
    , smtDecls
    , 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 qualified Language.Fixpoint.Types.Visitor as Vis
import           Language.Fixpoint.Types.Errors
import           Language.Fixpoint.Utils.Files
import           Language.Fixpoint.Types         hiding (allowHO)
import qualified Language.Fixpoint.Types         as F
import           Language.Fixpoint.Smt.Types
import qualified Language.Fixpoint.Smt.Theories as Thy
import           Language.Fixpoint.Smt.Serialize ()
import           Control.Applicative      ((<|>))
import           Control.Monad
import           Control.Exception
import           Data.Char
import qualified Data.HashMap.Strict      as M
import           Data.Maybe              (fromMaybe)
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup          (Semigroup (..))
#endif

import qualified Data.Text                as T
import           Data.Text.Format
import qualified Data.Text.IO             as TIO
import qualified Data.Text.Lazy           as LT
import qualified Data.Text.Lazy.Builder   as Builder
import qualified Data.Text.Lazy.IO        as LTIO
import           System.Directory
import           System.Console.CmdArgs.Verbosity
import           System.Exit              hiding (die)
import           System.FilePath
import           System.IO                (Handle, IOMode (..), hClose, hFlush, openFile)
import           System.Process
import qualified Data.Attoparsec.Text     as A
-- import qualified Data.HashMap.Strict      as M
import           Data.Attoparsec.Internal.Types (Parser)
import           Text.PrettyPrint.HughesPJ (text)
import           Language.Fixpoint.SortCheck
-- import qualified Language.Fixpoint.Types as F
-- import           Language.Fixpoint.Types.PrettyPrint (tracepp)

{-
runFile f
  = readFile f >>= runString

runString str
  = runCommands $ rr str

runCommands cmds
  = do me   <- makeContext Z3
       mapM_ (T.putStrLn . smt2) cmds
       zs   <- mapM (command me) cmds
       return zs
-}

checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValidWithContext Context
me [(Symbol, Sort)]
xts Expr
p Expr
q =
  Context -> String -> IO Bool -> IO Bool
forall a. Context -> String -> IO a -> IO a
smtBracket Context
me String
"checkValidWithContext" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$
    Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' Context
me [(Symbol, Sort)]
xts Expr
p Expr
q

-- | type ClosedPred E = {v:Pred | subset (vars v) (keys E) }
-- checkValid :: e:Env -> ClosedPred e -> ClosedPred e -> IO Bool
checkValid :: Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid :: Config -> String -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid Config
cfg String
f [(Symbol, Sort)]
xts Expr
p Expr
q = do
  Context
me <- Config -> String -> IO Context
makeContext Config
cfg String
f
  Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' Context
me [(Symbol, Sort)]
xts Expr
p Expr
q

checkValid' :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' Context
me [(Symbol, Sort)]
xts Expr
p Expr
q = do
  Context -> [(Symbol, Sort)] -> IO ()
smtDecls Context
me [(Symbol, Sort)]
xts
  Context -> Expr -> IO ()
smtAssert Context
me (Expr -> IO ()) -> Expr -> IO ()
forall a b. (a -> b) -> a -> b
$ ListNE Expr -> Expr
pAnd [Expr
p, Expr -> Expr
PNot Expr
q]
  Context -> IO Bool
smtCheckUnsat Context
me

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

-- checkValid :: e:Env -> [ClosedPred e] -> IO [Bool]
checkValids :: Config -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]
checkValids :: Config -> String -> [(Symbol, Sort)] -> ListNE Expr -> IO [Bool]
checkValids Config
cfg String
f [(Symbol, Sort)]
xts ListNE Expr
ps
  = do Context
me <- Config -> String -> IO Context
makeContext Config
cfg String
f
       Context -> [(Symbol, Sort)] -> IO ()
smtDecls Context
me [(Symbol, Sort)]
xts
       ListNE Expr -> (Expr -> IO Bool) -> IO [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ListNE Expr
ps ((Expr -> IO Bool) -> IO [Bool]) -> (Expr -> IO Bool) -> IO [Bool]
forall a b. (a -> b) -> a -> b
$ \Expr
p ->
          Context -> String -> IO Bool -> IO Bool
forall a. Context -> String -> IO a -> IO a
smtBracket Context
me String
"checkValids" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$
            Context -> Expr -> IO ()
smtAssert Context
me (Expr -> Expr
PNot Expr
p) IO () -> IO Bool -> IO Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Context -> IO Bool
smtCheckUnsat Context
me

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

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

--------------------------------------------------------------------------------
command              :: Context -> Command -> IO Response
--------------------------------------------------------------------------------
command :: Context -> Command -> IO Response
command Context
me !Command
cmd       = Command -> IO ()
forall a. SMTLIB2 a => a -> IO ()
say Command
cmd IO () -> IO Response -> IO Response
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> IO Response
hear Command
cmd
  where
    env :: SymEnv
env               = Context -> SymEnv
ctxSymEnv Context
me
    say :: a -> IO ()
say               = Context -> Raw -> IO ()
smtWrite Context
me (Raw -> IO ()) -> (a -> Raw) -> a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> Raw
Builder.toLazyText (Builder -> Raw) -> (a -> Builder) -> a -> Raw
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> a -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
runSmt2 SymEnv
env
    hear :: Command -> IO Response
hear Command
CheckSat     = Context -> IO Response
smtRead Context
me
    hear (GetValue [Symbol]
_) = Context -> IO Response
smtRead Context
me
    hear Command
_            = Response -> IO Response
forall (m :: * -> *) a. Monad m => a -> m a
return Response
Ok


smtWrite :: Context -> Raw -> IO ()
smtWrite :: Context -> Raw -> IO ()
smtWrite Context
me !Raw
s = Context -> Raw -> IO ()
smtWriteRaw Context
me Raw
s

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

type SmtParser a = Parser T.Text a

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

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

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

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

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

symbolP :: SmtParser Symbol
symbolP :: SmtParser Symbol
symbolP = {-# SCC "symbolP" #-} Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> Parser Text -> SmtParser Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> Parser Text
A.takeWhile1 (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace)

valueP :: SmtParser T.Text
valueP :: Parser Text
valueP = {-# SCC "valueP" #-} Parser Text
negativeP
      Parser Text -> Parser Text -> Parser Text
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Char -> Bool) -> Parser Text
A.takeWhile1 (\Char
c -> Bool -> Bool
not (Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')' Bool -> Bool -> Bool
|| Char -> Bool
isSpace Char
c))

negativeP :: SmtParser T.Text
negativeP :: Parser Text
negativeP
  = do Text
v <- Char -> Parser Char
A.char Char
'(' Parser Char -> Parser Text -> Parser Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Char -> Bool) -> Parser Text
A.takeWhile1 (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/=Char
')') Parser Text -> Parser Char -> Parser Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
A.char Char
')'
       Text -> Parser Text
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> Parser Text) -> Text -> Parser Text
forall a b. (a -> b) -> a -> b
$ Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
v Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

smtWriteRaw      :: Context -> Raw -> IO ()
smtWriteRaw :: Context -> Raw -> IO ()
smtWriteRaw Context
me !Raw
s = {-# SCC "smtWriteRaw" #-} do
  -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
  --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
  Handle -> Raw -> IO ()
hPutStrLnNow (Context -> Handle
ctxCout Context
me) Raw
s
  IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> Raw -> IO ()
`hPutStrLnNow` Raw
s) (Context -> Maybe Handle
ctxLog Context
me)

smtReadRaw       :: Context -> IO T.Text
smtReadRaw :: Context -> IO Text
smtReadRaw Context
me    = {-# SCC "smtReadRaw" #-} Handle -> IO Text
TIO.hGetLine (Context -> Handle
ctxCin Context
me)

hPutStrLnNow     :: Handle -> LT.Text -> IO ()
hPutStrLnNow :: Handle -> Raw -> IO ()
hPutStrLnNow Handle
h !Raw
s = Handle -> Raw -> IO ()
LTIO.hPutStrLn Handle
h Raw
s IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
h

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

--------------------------------------------------------------------------
makeContext   :: Config -> FilePath -> IO Context
--------------------------------------------------------------------------
makeContext :: Config -> String -> IO Context
makeContext Config
cfg String
f
  = do Context
me   <- Config -> IO Context
makeProcess Config
cfg
       [Raw]
pre  <- Config -> SMTSolver -> Context -> IO [Raw]
smtPreamble Config
cfg (Config -> SMTSolver
solver Config
cfg) Context
me
       Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String
takeDirectory String
smtFile
       Handle
hLog <- String -> IOMode -> IO Handle
openFile String
smtFile IOMode
WriteMode
       let me' :: Context
me' = Context
me { ctxLog :: Maybe Handle
ctxLog = Handle -> Maybe Handle
forall a. a -> Maybe a
Just Handle
hLog }
       (Raw -> IO ()) -> [Raw] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Context -> Raw -> IO ()
smtWrite Context
me') [Raw]
pre
       Context -> IO Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
me'
    where
       smtFile :: String
smtFile = Ext -> String -> String
extFileName Ext
Smt2 String
f

makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context
makeContextWithSEnv :: Config -> String -> SymEnv -> IO Context
makeContextWithSEnv Config
cfg String
f SymEnv
env = do
  Context
ctx     <- Config -> String -> IO Context
makeContext Config
cfg String
f
  let ctx' :: Context
ctx' = Context
ctx {ctxSymEnv :: SymEnv
ctxSymEnv = SymEnv
env}
  Context -> IO ()
declare Context
ctx'
  Context -> IO Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
ctx'
  -- where msg = "makeContextWithSEnv" ++ show env

makeContextNoLog :: Config -> IO Context
makeContextNoLog :: Config -> IO Context
makeContextNoLog Config
cfg
  = do Context
me  <- Config -> IO Context
makeProcess Config
cfg
       [Raw]
pre <- Config -> SMTSolver -> Context -> IO [Raw]
smtPreamble Config
cfg (Config -> SMTSolver
solver Config
cfg) Context
me
       (Raw -> IO ()) -> [Raw] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Context -> Raw -> IO ()
smtWrite Context
me) [Raw]
pre
       Context -> IO Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
me

makeProcess :: Config -> IO Context
makeProcess :: Config -> IO Context
makeProcess Config
cfg
  = do (Handle
hOut, Handle
hIn, Handle
_ ,ProcessHandle
pid) <- String -> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveCommand (String -> IO (Handle, Handle, Handle, ProcessHandle))
-> String -> IO (Handle, Handle, Handle, ProcessHandle)
forall a b. (a -> b) -> a -> b
$ SMTSolver -> String
smtCmd (Config -> SMTSolver
solver Config
cfg)
       Bool
loud <- IO Bool
isLoud
       Context -> IO Context
forall (m :: * -> *) a. Monad m => a -> m a
return Ctx :: ProcessHandle
-> Handle -> Handle -> Maybe Handle -> Bool -> SymEnv -> Context
Ctx { ctxPid :: ProcessHandle
ctxPid     = ProcessHandle
pid
                  , ctxCin :: Handle
ctxCin     = Handle
hIn
                  , ctxCout :: Handle
ctxCout    = Handle
hOut
                  , ctxLog :: Maybe Handle
ctxLog     = Maybe Handle
forall a. Maybe a
Nothing
                  , ctxVerbose :: Bool
ctxVerbose = Bool
loud
                  , ctxSymEnv :: SymEnv
ctxSymEnv  = SymEnv
forall a. Monoid a => a
mempty
                  }

--------------------------------------------------------------------------
cleanupContext :: Context -> IO ExitCode
--------------------------------------------------------------------------
cleanupContext :: Context -> IO ExitCode
cleanupContext (Ctx {Bool
Maybe Handle
Handle
ProcessHandle
SymEnv
ctxSymEnv :: SymEnv
ctxVerbose :: Bool
ctxLog :: Maybe Handle
ctxCout :: Handle
ctxCin :: Handle
ctxPid :: ProcessHandle
ctxPid :: Context -> ProcessHandle
ctxCin :: Context -> Handle
ctxCout :: Context -> Handle
ctxLog :: Context -> Maybe Handle
ctxVerbose :: Context -> Bool
ctxSymEnv :: Context -> SymEnv
..}) = do
  String -> Handle -> IO ()
hCloseMe String
"ctxCin"  Handle
ctxCin
  String -> Handle -> IO ()
hCloseMe String
"ctxCout" Handle
ctxCout
  IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (String -> Handle -> IO ()
hCloseMe String
"ctxLog") Maybe Handle
ctxLog
  ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ctxPid

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

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

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

-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...
smtPreamble :: Config -> SMTSolver -> Context -> IO [LT.Text]
smtPreamble :: Config -> SMTSolver -> Context -> IO [Raw]
smtPreamble Config
cfg SMTSolver
Z3 Context
me
  = do Context -> Raw -> IO ()
smtWrite Context
me Raw
"(get-info :version)"
       Text
v:[Text]
_ <- Text -> [Text]
T.words (Text -> [Text]) -> (Text -> Text) -> Text -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Text] -> Int -> Text
forall a. [a] -> Int -> a
!!Int
1) ([Text] -> Text) -> (Text -> [Text]) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> [Text]
T.splitOn Text
"\"" (Text -> [Text]) -> IO Text -> IO [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> IO Text
smtReadRaw Context
me
       SMTSolver -> Text -> Config -> IO ()
checkValidStringFlag SMTSolver
Z3 Text
v Config
cfg
       if Text -> Text -> [Text]
T.splitOn Text
"." Text
v [Text] -> [Text] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
`versionGreaterEq` [Text
"4", Text
"3", Text
"2"]
         then [Raw] -> IO [Raw]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Raw] -> IO [Raw]) -> [Raw] -> IO [Raw]
forall a b. (a -> b) -> a -> b
$ [Raw]
z3_432_options [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
makeMbqi Config
cfg [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
makeTimeout Config
cfg [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> SMTSolver -> [Raw]
Thy.preamble Config
cfg SMTSolver
Z3
         else [Raw] -> IO [Raw]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Raw] -> IO [Raw]) -> [Raw] -> IO [Raw]
forall a b. (a -> b) -> a -> b
$ [Raw]
z3_options     [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
makeMbqi Config
cfg [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
makeTimeout Config
cfg [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> SMTSolver -> [Raw]
Thy.preamble Config
cfg SMTSolver
Z3
smtPreamble Config
cfg SMTSolver
s Context
_
  = SMTSolver -> Text -> Config -> IO ()
checkValidStringFlag SMTSolver
s Text
"" Config
cfg IO () -> IO [Raw] -> IO [Raw]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Raw] -> IO [Raw]
forall (m :: * -> *) a. Monad m => a -> m a
return (Config -> SMTSolver -> [Raw]
Thy.preamble Config
cfg SMTSolver
s)

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

noString :: SMTSolver -> T.Text -> Config -> Bool
noString :: SMTSolver -> Text -> Config -> Bool
noString SMTSolver
smt Text
v Config
cfg
  =  Config -> Bool
stringTheory Config
cfg
  Bool -> Bool -> Bool
&& Bool -> Bool
not (SMTSolver
smt SMTSolver -> SMTSolver -> Bool
forall a. Eq a => a -> a -> Bool
== SMTSolver
Z3 Bool -> Bool -> Bool
&& (Text -> Text -> [Text]
T.splitOn Text
"." Text
v [Text] -> [Text] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
`versionGreaterEq` [Text
"4", Text
"4", Text
"2"]))


versionGreaterEq :: Ord a => [a] -> [a] -> Bool
versionGreaterEq :: [a] -> [a] -> Bool
versionGreaterEq (a
x:[a]
xs) (a
y:[a]
ys)
  | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>  a
y = Bool
True
  | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = [a] -> [a] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
versionGreaterEq [a]
xs [a]
ys
  | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<  a
y = Bool
False
versionGreaterEq [a]
_  [] = Bool
True
versionGreaterEq [] [a]
_  = Bool
False
versionGreaterEq [a]
_ [a]
_ = String -> Bool
forall a. (?callStack::CallStack) => String -> a
Misc.errorstar String
"Interface.versionGreater called with bad arguments"

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

smtPush, smtPop   :: Context -> IO ()
smtPush :: Context -> IO ()
smtPush Context
me        = Context -> Command -> IO ()
interact' Context
me Command
Push
smtPop :: Context -> IO ()
smtPop Context
me         = Context -> Command -> IO ()
interact' Context
me Command
Pop

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

smtDecl :: Context -> Symbol -> Sort -> IO ()
smtDecl :: Context -> Symbol -> Sort -> IO ()
smtDecl Context
me Symbol
x Sort
t = Context -> Command -> IO ()
interact' Context
me ({- notracepp msg $ -} Symbol -> [SmtSort] -> SmtSort -> Command
Declare Symbol
x [SmtSort]
ins' SmtSort
out')
  where
    ins' :: [SmtSort]
ins'       = Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env (Sort -> SmtSort) -> [Sort] -> [SmtSort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ins
    out' :: SmtSort
out'       = Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env     Sort
out
    ([Sort]
ins, Sort
out) = Sort -> ([Sort], Sort)
deconSort Sort
t
    _msg :: String
_msg        = String
"smtDecl: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Symbol, Sort, [Sort], Sort) -> String
forall a. PPrint a => a -> String
showpp (Symbol
x, Sort
t, [Sort]
ins, Sort
out)
    env :: SEnv DataDecl
env        = SymEnv -> SEnv DataDecl
seData (Context -> SymEnv
ctxSymEnv Context
me)

smtFuncDecl :: Context -> Symbol -> ([SmtSort],  SmtSort) -> IO ()
smtFuncDecl :: Context -> Symbol -> ([SmtSort], SmtSort) -> IO ()
smtFuncDecl Context
me Symbol
x ([SmtSort]
ts, SmtSort
t) = Context -> Command -> IO ()
interact' Context
me (Symbol -> [SmtSort] -> SmtSort -> Command
Declare Symbol
x [SmtSort]
ts SmtSort
t)

smtDataDecl :: Context -> [DataDecl] -> IO ()
smtDataDecl :: Context -> [DataDecl] -> IO ()
smtDataDecl Context
me [DataDecl]
ds = Context -> Command -> IO ()
interact' Context
me ([DataDecl] -> Command
DeclData [DataDecl]
ds)

deconSort :: Sort -> ([Sort], Sort)
deconSort :: Sort -> ([Sort], Sort)
deconSort Sort
t = case Sort -> Maybe ([Int], [Sort], Sort)
functionSort Sort
t of
                Just ([Int]
_, [Sort]
ins, Sort
out) -> ([Sort]
ins, Sort
out)
                Maybe ([Int], [Sort], Sort)
Nothing            -> ([] , Sort
t  )

-- hack now this is used only for checking gradual condition.
smtCheckSat :: Context -> Expr -> IO Bool
smtCheckSat :: Context -> Expr -> IO Bool
smtCheckSat Context
me Expr
p
 = Context -> Expr -> IO ()
smtAssert Context
me Expr
p IO () -> IO Bool -> IO Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Response -> Bool
ans (Response -> Bool) -> IO Response -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> Command -> IO Response
command Context
me Command
CheckSat)
 where
   ans :: Response -> Bool
ans Response
Sat = Bool
True
   ans Response
_   = Bool
False

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

smtAssertAxiom :: Context -> Triggered Expr -> IO ()
smtAssertAxiom :: Context -> Triggered Expr -> IO ()
smtAssertAxiom Context
me Triggered Expr
p  = Context -> Command -> IO ()
interact' Context
me (Triggered Expr -> Command
AssertAx Triggered Expr
p)

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

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

smtBracketAt :: SrcSpan -> Context -> String -> IO a -> IO a
smtBracketAt :: SrcSpan -> Context -> String -> IO a -> IO a
smtBracketAt SrcSpan
sp Context
x String
y IO a
z = Context -> String -> IO a -> IO a
forall a. Context -> String -> IO a -> IO a
smtBracket Context
x String
y IO a
z IO a -> (Error -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` SrcSpan -> Error -> IO a
forall a. SrcSpan -> Error -> a
dieAt SrcSpan
sp

smtBracket :: Context -> String -> IO a -> IO a
smtBracket :: Context -> String -> IO a -> IO a
smtBracket Context
me String
_msg IO a
a   = do
  Context -> IO ()
smtPush Context
me
  a
r <- IO a
a
  Context -> IO ()
smtPop Context
me
  a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r

respSat :: Response -> Bool
respSat :: Response -> Bool
respSat Response
Unsat   = Bool
True
respSat Response
Sat     = Bool
False
respSat Response
Unknown = Bool
False
respSat Response
r       = Error -> Bool
forall a. Error -> a
die (Error -> Bool) -> Error -> Bool
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
dummySpan (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String
"crash: SMTLIB2 respSat = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Response -> String
forall a. Show a => a -> String
show Response
r)

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


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


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

-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...
z3_432_options :: [LT.Text]
z3_432_options :: [Raw]
z3_432_options
  = [ Raw
"(set-option :auto-config false)"
    , Raw
"(set-option :model true)"
    , Raw
"(set-option :model.partial false)"]

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



--------------------------------------------------------------------------------
declare :: Context -> IO () -- SolveM ()
--------------------------------------------------------------------------------
declare :: Context -> IO ()
declare Context
me = do
  [[DataDecl]] -> ([DataDecl] -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[DataDecl]]
dss    (([DataDecl] -> IO ()) -> IO ()) -> ([DataDecl] -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$           Context -> [DataDecl] -> IO ()
smtDataDecl Context
me
  [(Symbol, Sort)] -> ((Symbol, Sort) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Symbol, Sort)]
thyXTs (((Symbol, Sort) -> IO ()) -> IO ())
-> ((Symbol, Sort) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ())
-> (Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Symbol -> Sort -> IO ()
smtDecl     Context
me
  [(Symbol, Sort)] -> ((Symbol, Sort) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Symbol, Sort)]
qryXTs (((Symbol, Sort) -> IO ()) -> IO ())
-> ((Symbol, Sort) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ())
-> (Symbol -> Sort -> IO ()) -> (Symbol, Sort) -> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Symbol -> Sort -> IO ()
smtDecl     Context
me
  [(Symbol, ([SmtSort], SmtSort))]
-> ((Symbol, ([SmtSort], SmtSort)) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Symbol, ([SmtSort], SmtSort))]
ats    (((Symbol, ([SmtSort], SmtSort)) -> IO ()) -> IO ())
-> ((Symbol, ([SmtSort], SmtSort)) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Symbol -> ([SmtSort], SmtSort) -> IO ())
-> (Symbol, ([SmtSort], SmtSort)) -> IO ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Symbol -> ([SmtSort], SmtSort) -> IO ())
 -> (Symbol, ([SmtSort], SmtSort)) -> IO ())
-> (Symbol -> ([SmtSort], SmtSort) -> IO ())
-> (Symbol, ([SmtSort], SmtSort))
-> IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Symbol -> ([SmtSort], SmtSort) -> IO ()
smtFuncDecl Context
me
  [ListNE Expr] -> (ListNE Expr -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ListNE Expr]
ess    ((ListNE Expr -> IO ()) -> IO ())
-> (ListNE Expr -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$           Context -> ListNE Expr -> IO ()
smtDistinct Context
me
  ListNE Expr -> (Expr -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ListNE Expr
axs    ((Expr -> IO ()) -> IO ()) -> (Expr -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$           Context -> Expr -> IO ()
smtAssert   Context
me
  where
    env :: SymEnv
env        = Context -> SymEnv
ctxSymEnv Context
me
    dss :: [[DataDecl]]
dss        = SymEnv -> [[DataDecl]]
dataDeclarations          SymEnv
env
    lts :: [(Symbol, Sort)]
lts        = SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv (SEnv Sort -> [(Symbol, Sort)])
-> (SymEnv -> SEnv Sort) -> SymEnv -> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> SEnv Sort
F.seLits (SymEnv -> [(Symbol, Sort)]) -> SymEnv -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ SymEnv
env
    ess :: [ListNE Expr]
ess        = [(Symbol, Sort)] -> [ListNE Expr]
distinctLiterals  [(Symbol, Sort)]
lts
    axs :: ListNE Expr
axs        = [(Symbol, Sort)] -> ListNE Expr
Thy.axiomLiterals [(Symbol, Sort)]
lts
    thyXTs :: [(Symbol, Sort)]
thyXTs     =                    ((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> (Symbol, Sort) -> Bool
forall b. Int -> (Symbol, b) -> Bool
isKind Int
1) [(Symbol, Sort)]
xts
    qryXTs :: [(Symbol, Sort)]
qryXTs     = (Sort -> Sort) -> (Symbol, Sort) -> (Symbol, Sort)
forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd Sort -> Sort
forall a. Elaborate a => a -> a
tx ((Symbol, Sort) -> (Symbol, Sort))
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> (Symbol, Sort) -> Bool
forall b. Int -> (Symbol, b) -> Bool
isKind Int
2) [(Symbol, Sort)]
xts
    isKind :: Int -> (Symbol, b) -> Bool
isKind Int
n   = (Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==)  (Int -> Bool) -> ((Symbol, b) -> Int) -> (Symbol, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> Symbol -> Int
symKind SymEnv
env (Symbol -> Int) -> ((Symbol, b) -> Symbol) -> (Symbol, b) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, b) -> Symbol
forall a b. (a, b) -> a
fst
    xts :: [(Symbol, Sort)]
xts        = {- tracepp "symbolSorts" $ -} SEnv Sort -> [(Symbol, Sort)]
symbolSorts (SymEnv -> SEnv Sort
F.seSort SymEnv
env) 
    tx :: a -> a
tx         = Located String -> SymEnv -> a -> a
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate    Located String
"declare" SymEnv
env
    ats :: [(Symbol, ([SmtSort], SmtSort))]
ats        = SymEnv -> [(Symbol, ([SmtSort], SmtSort))]
funcSortVars SymEnv
env

symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)]
symbolSorts :: SEnv Sort -> [(Symbol, Sort)]
symbolSorts SEnv Sort
env = [(Symbol
x, Sort -> Sort
tx Sort
t) | (Symbol
x, Sort
t) <- SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv Sort
env ]
 where
  tx :: Sort -> Sort
tx t :: Sort
t@(FObj Symbol
a) = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe Sort
t (Symbol -> SEnv Sort -> Maybe Sort
forall a. Symbol -> SEnv a -> Maybe a
F.lookupSEnv Symbol
a SEnv Sort
env)
  tx Sort
t          = Sort
t

dataDeclarations :: SymEnv -> [[DataDecl]]
dataDeclarations :: SymEnv -> [[DataDecl]]
dataDeclarations = [DataDecl] -> [[DataDecl]]
orderDeclarations ([DataDecl] -> [[DataDecl]])
-> (SymEnv -> [DataDecl]) -> SymEnv -> [[DataDecl]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, DataDecl) -> DataDecl)
-> [(Symbol, DataDecl)] -> [DataDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, DataDecl) -> DataDecl
forall a b. (a, b) -> b
snd ([(Symbol, DataDecl)] -> [DataDecl])
-> (SymEnv -> [(Symbol, DataDecl)]) -> SymEnv -> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEnv DataDecl -> [(Symbol, DataDecl)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv (SEnv DataDecl -> [(Symbol, DataDecl)])
-> (SymEnv -> SEnv DataDecl) -> SymEnv -> [(Symbol, DataDecl)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> SEnv DataDecl
F.seData

funcSortVars :: F.SymEnv -> [(F.Symbol, ([F.SmtSort], F.SmtSort))]
funcSortVars :: SymEnv -> [(Symbol, ([SmtSort], SmtSort))]
funcSortVars SymEnv
env  = [(Symbol -> FuncSort -> Symbol
var Symbol
applyName  FuncSort
t       , FuncSort -> ([SmtSort], SmtSort)
forall b. (SmtSort, b) -> ([SmtSort], b)
appSort FuncSort
t) | FuncSort
t <- [FuncSort]
ts]
                 [(Symbol, ([SmtSort], SmtSort))]
-> [(Symbol, ([SmtSort], SmtSort))]
-> [(Symbol, ([SmtSort], SmtSort))]
forall a. [a] -> [a] -> [a]
++ [(Symbol -> FuncSort -> Symbol
var Symbol
coerceName FuncSort
t       , ([SmtSort
t1],SmtSort
t2)) | t :: FuncSort
t@(SmtSort
t1, SmtSort
t2) <- [FuncSort]
ts]
                 [(Symbol, ([SmtSort], SmtSort))]
-> [(Symbol, ([SmtSort], SmtSort))]
-> [(Symbol, ([SmtSort], SmtSort))]
forall a. [a] -> [a] -> [a]
++ [(Symbol -> FuncSort -> Symbol
var Symbol
lambdaName FuncSort
t       , FuncSort -> ([SmtSort], SmtSort)
forall a. (a, a) -> ([a], SmtSort)
lamSort FuncSort
t) | FuncSort
t <- [FuncSort]
ts]
                 [(Symbol, ([SmtSort], SmtSort))]
-> [(Symbol, ([SmtSort], SmtSort))]
-> [(Symbol, ([SmtSort], SmtSort))]
forall a. [a] -> [a] -> [a]
++ [(Symbol -> FuncSort -> Symbol
var (Int -> Symbol
lamArgSymbol Int
i) FuncSort
t , FuncSort -> ([SmtSort], SmtSort)
forall b b a. (b, b) -> ([a], b)
argSort FuncSort
t) | t :: FuncSort
t@(SmtSort
_,SmtSort
F.SInt) <- [FuncSort]
ts, Int
i <- [Int
1..Int
Thy.maxLamArg] ]
  where
    var :: Symbol -> FuncSort -> Symbol
var Symbol
n         = Symbol -> SymEnv -> () -> FuncSort -> Symbol
forall a. PPrint a => Symbol -> SymEnv -> a -> FuncSort -> Symbol
F.symbolAtSmtName Symbol
n SymEnv
env ()
    ts :: [FuncSort]
ts            = HashMap FuncSort Int -> [FuncSort]
forall k v. HashMap k v -> [k]
M.keys (SymEnv -> HashMap FuncSort Int
F.seAppls SymEnv
env)
    appSort :: (SmtSort, b) -> ([SmtSort], b)
appSort (SmtSort
s,b
t) = ([SmtSort
F.SInt, SmtSort
s], b
t)
    lamSort :: (a, a) -> ([a], SmtSort)
lamSort (a
s,a
t) = ([a
s, a
t], SmtSort
F.SInt)
    argSort :: (b, b) -> ([a], b)
argSort (b
s,b
_) = ([]    , b
s)

-- | 'symKind' returns {0, 1, 2} where:
--   0 = Theory-Definition,
--   1 = Theory-Declaration,
--   2 = Query-Binder

symKind :: F.SymEnv -> F.Symbol -> Int
symKind :: SymEnv -> Symbol -> Int
symKind SymEnv
env Symbol
x = case TheorySymbol -> Sem
F.tsInterp (TheorySymbol -> Sem) -> Maybe TheorySymbol -> Maybe Sem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> SymEnv -> Maybe TheorySymbol
F.symEnvTheory Symbol
x SymEnv
env of
                  Just Sem
F.Theory   -> Int
0
                  Just Sem
F.Ctor     -> Int
0
                  Just Sem
F.Test     -> Int
0
                  Just Sem
F.Field    -> Int
0
                  Just Sem
F.Uninterp -> Int
1
                  Maybe Sem
Nothing         -> Int
2
              -- Just t  -> if tsInterp t then 0 else 1


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

-- | `distinctLiterals` is used solely to determine the set of literals
--   (of each sort) that are *disequal* to each other, e.g. EQ, LT, GT,
--   or string literals "cat", "dog", "mouse". These should only include
--   non-function sorted values.
distinctLiterals :: [(F.Symbol, F.Sort)] -> [[F.Expr]]
distinctLiterals :: [(Symbol, Sort)] -> [ListNE Expr]
distinctLiterals [(Symbol, Sort)]
xts = [ ListNE Expr
es | (Sort
_, ListNE Expr
es) <- [(Sort, ListNE Expr)]
tess ]
   where
    tess :: [(Sort, ListNE Expr)]
tess             = [(Sort, Expr)] -> [(Sort, ListNE Expr)]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Sort
t, Symbol -> Expr
forall a. Expression a => a -> Expr
F.expr Symbol
x) | (Symbol
x, Sort
t) <- [(Symbol, Sort)]
xts, Sort -> Bool
notFun Sort
t]
    notFun :: Sort -> Bool
notFun           = Bool -> Bool
not (Bool -> Bool) -> (Sort -> Bool) -> Sort -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Bool
F.isFunctionSortedReft (SortedReft -> Bool) -> (Sort -> SortedReft) -> Sort -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> Reft -> SortedReft
`F.RR` Reft
F.trueReft)
    -- _notStr          = not . (F.strSort ==) . F.sr_sort . (`F.RR` F.trueReft)

--------------------------------------------------------------------------------
-- | 'orderDeclarations' sorts the data declarations such that each declarations
--   only refers to preceding ones.
--------------------------------------------------------------------------------
orderDeclarations :: [F.DataDecl] -> [[F.DataDecl]]
--------------------------------------------------------------------------------
orderDeclarations :: [DataDecl] -> [[DataDecl]]
orderDeclarations [DataDecl]
ds = {- reverse -} ((DataDecl -> (FTycon, [FTycon])) -> [DataDecl] -> [[DataDecl]]
forall v a. Ord v => (a -> (v, [v])) -> [a] -> [[a]]
Misc.sccsWith DataDecl -> (FTycon, [FTycon])
f [DataDecl]
ds)
  where
    dM :: HashMap FTycon DataDecl
dM               = [(FTycon, DataDecl)] -> HashMap FTycon DataDecl
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(DataDecl -> FTycon
F.ddTyCon DataDecl
d, DataDecl
d) | DataDecl
d <- [DataDecl]
ds]
    f :: DataDecl -> (FTycon, [FTycon])
f DataDecl
d              = (DataDecl -> FTycon
F.ddTyCon DataDecl
d, HashMap FTycon DataDecl -> DataDecl -> [FTycon]
dataDeclDeps HashMap FTycon DataDecl
dM DataDecl
d)

dataDeclDeps :: M.HashMap F.FTycon F.DataDecl -> F.DataDecl -> [F.FTycon]
dataDeclDeps :: HashMap FTycon DataDecl -> DataDecl -> [FTycon]
dataDeclDeps HashMap FTycon DataDecl
dM = (FTycon -> Bool) -> [FTycon] -> [FTycon]
forall a. (a -> Bool) -> [a] -> [a]
filter (FTycon -> HashMap FTycon DataDecl -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
`M.member` HashMap FTycon DataDecl
dM) ([FTycon] -> [FTycon])
-> (DataDecl -> [FTycon]) -> DataDecl -> [FTycon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FTycon] -> [FTycon]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([FTycon] -> [FTycon])
-> (DataDecl -> [FTycon]) -> DataDecl -> [FTycon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> [FTycon]
dataDeclFTycons

dataDeclFTycons :: F.DataDecl -> [F.FTycon]
dataDeclFTycons :: DataDecl -> [FTycon]
dataDeclFTycons = (DataCtor -> [FTycon]) -> [DataCtor] -> [FTycon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataCtor -> [FTycon]
dataCtorFTycons ([DataCtor] -> [FTycon])
-> (DataDecl -> [DataCtor]) -> DataDecl -> [FTycon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> [DataCtor]
F.ddCtors

dataCtorFTycons :: F.DataCtor -> [F.FTycon]
dataCtorFTycons :: DataCtor -> [FTycon]
dataCtorFTycons = (DataField -> [FTycon]) -> [DataField] -> [FTycon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataField -> [FTycon]
dataFieldFTycons ([DataField] -> [FTycon])
-> (DataCtor -> [DataField]) -> DataCtor -> [FTycon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtor -> [DataField]
F.dcFields

dataFieldFTycons :: F.DataField -> [F.FTycon]
dataFieldFTycons :: DataField -> [FTycon]
dataFieldFTycons = Sort -> [FTycon]
sortFTycons (Sort -> [FTycon]) -> (DataField -> Sort) -> DataField -> [FTycon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataField -> Sort
F.dfSort

sortFTycons :: Sort -> [FTycon]
sortFTycons :: Sort -> [FTycon]
sortFTycons = ([FTycon] -> Sort -> [FTycon]) -> [FTycon] -> Sort -> [FTycon]
forall a. (a -> Sort -> a) -> a -> Sort -> a
Vis.foldSort [FTycon] -> Sort -> [FTycon]
go []
  where
    go :: [FTycon] -> Sort -> [FTycon]
go [FTycon]
cs (FTC FTycon
c) = FTycon
c FTycon -> [FTycon] -> [FTycon]
forall a. a -> [a] -> [a]
: [FTycon]
cs
    go [FTycon]
cs Sort
_       = [FTycon]
cs