{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
module Language.Fixpoint.Smt.Interface (
Command (..)
, Response (..)
, SMTLIB2 (..)
, Context (..)
, makeContext
, makeContextNoLog
, makeContextWithSEnv
, cleanupContext
, command
, smtExit
, smtSetMbqi
, smtDecl
, smtDecls
, smtDefineFunc
, smtAssert
, smtFuncDecl
, smtAssertAxiom
, smtCheckUnsat
, smtCheckSat
, smtBracket, smtBracketAt
, smtDistinct
, smtPush, smtPop
, smtAssertAsync
, smtCheckUnsatAsync
, readCheckUnsat
, smtBracketAsyncAt
, smtPushAsync
, smtPopAsync
, checkValid
, checkValid'
, checkValidWithContext
, checkValids
) where
import Control.Concurrent.Async (async, cancel)
import Control.Concurrent.STM
(TVar, atomically, modifyTVar, newTVarIO, readTVar, retry, writeTVar)
import Language.Fixpoint.Types.Config ( SMTSolver (..)
, Config
, solver
, smtTimeout
, gradual
, stringTheory)
import qualified Language.Fixpoint.Misc as Misc
import Language.Fixpoint.Types.Errors
import Language.Fixpoint.Utils.Files
import Language.Fixpoint.Types hiding (allowHO)
import qualified Language.Fixpoint.Types as F
import Language.Fixpoint.Smt.Types
import qualified Language.Fixpoint.Smt.Theories as Thy
import Language.Fixpoint.Smt.Serialize ()
import Control.Applicative ((<|>))
import Control.Monad
import Control.Exception
import Data.Char
import qualified Data.HashMap.Strict as M
import Data.Maybe (fromMaybe)
import qualified Data.Text as T
import qualified Data.Text.IO as TIO
import qualified Data.Text.Lazy as LT
import qualified Data.Text.Lazy.IO as LTIO
import System.Directory
import System.Console.CmdArgs.Verbosity
import System.Exit hiding (die)
import System.FilePath
import System.IO
import System.Process
import qualified Data.Attoparsec.Text as A
import Data.Attoparsec.Internal.Types (Parser)
import Text.PrettyPrint.HughesPJ (text)
import Language.Fixpoint.SortCheck
import Language.Fixpoint.Utils.Builder as Builder
checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValidWithContext :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValidWithContext Context
me [(Symbol, Sort)]
xts Expr
p Expr
q =
forall a. Context -> [Char] -> IO a -> IO a
smtBracket Context
me [Char]
"checkValidWithContext" forall a b. (a -> b) -> a -> b
$
Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' Context
me [(Symbol, Sort)]
xts Expr
p Expr
q
checkValid :: Config -> FilePath -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid :: Config -> [Char] -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid Config
cfg [Char]
f [(Symbol, Sort)]
xts Expr
p Expr
q = do
Context
me <- Config -> [Char] -> IO Context
makeContext Config
cfg [Char]
f
Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' Context
me [(Symbol, Sort)]
xts Expr
p Expr
q
checkValid' :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' :: Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
checkValid' Context
me [(Symbol, Sort)]
xts Expr
p Expr
q = do
Context -> [(Symbol, Sort)] -> IO ()
smtDecls Context
me [(Symbol, Sort)]
xts
Context -> Expr -> IO ()
smtAssert Context
me forall a b. (a -> b) -> a -> b
$ ListNE Expr -> Expr
pAnd [Expr
p, Expr -> Expr
PNot Expr
q]
Context -> IO Bool
smtCheckUnsat Context
me
checkValids :: Config -> FilePath -> [(Symbol, Sort)] -> [Expr] -> IO [Bool]
checkValids :: Config -> [Char] -> [(Symbol, Sort)] -> ListNE Expr -> IO [Bool]
checkValids Config
cfg [Char]
f [(Symbol, Sort)]
xts ListNE Expr
ps
= do Context
me <- Config -> [Char] -> IO Context
makeContext Config
cfg [Char]
f
Context -> [(Symbol, Sort)] -> IO ()
smtDecls Context
me [(Symbol, Sort)]
xts
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ListNE Expr
ps forall a b. (a -> b) -> a -> b
$ \Expr
p ->
forall a. Context -> [Char] -> IO a -> IO a
smtBracket Context
me [Char]
"checkValids" forall a b. (a -> b) -> a -> b
$
Context -> Expr -> IO ()
smtAssert Context
me (Expr -> Expr
PNot Expr
p) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Context -> IO Bool
smtCheckUnsat Context
me
{-# SCC command #-}
command :: Context -> Command -> IO Response
command :: Context -> Command -> IO Response
command Context
me !Command
cmd = IO ()
say forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> IO Response
hear Command
cmd
where
env :: SymEnv
env = Context -> SymEnv
ctxSymEnv Context
me
say :: IO ()
say = Context -> Text -> IO ()
smtWrite Context
me ({-# SCC "Command-runSmt2" #-} Builder -> Text
Builder.toLazyText (forall a. SMTLIB2 a => SymEnv -> a -> Builder
runSmt2 SymEnv
env Command
cmd))
hear :: Command -> IO Response
hear Command
CheckSat = Context -> IO Response
smtRead Context
me
hear (GetValue [Symbol]
_) = Context -> IO Response
smtRead Context
me
hear Command
_ = forall (m :: * -> *) a. Monad m => a -> m a
return Response
Ok
smtExit :: Context -> IO ()
smtExit :: Context -> IO ()
smtExit Context
me = Context -> Command -> IO ()
asyncCommand Context
me Command
Exit
smtSetMbqi :: Context -> IO ()
smtSetMbqi :: Context -> IO ()
smtSetMbqi Context
me = Context -> Command -> IO ()
asyncCommand Context
me Command
SetMbqi
smtWrite :: Context -> Raw -> IO ()
smtWrite :: Context -> Text -> IO ()
smtWrite Context
me !Text
s = Context -> Text -> IO ()
smtWriteRaw Context
me Text
s
smtRead :: Context -> IO Response
smtRead :: Context -> IO Response
smtRead Context
me = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Context -> Bool
ctxVerbose Context
me) forall a b. (a -> b) -> a -> b
$ Text -> IO ()
LTIO.putStrLn Text
"SMT READ"
Text
ln <- Context -> IO Text
smtReadRaw Context
me
Result Response
res <- forall (m :: * -> *) a.
Monad m =>
m Text -> Parser a -> Text -> m (Result a)
A.parseWith (Context -> IO Text
smtReadRaw Context
me) SmtParser Response
responseP Text
ln
case forall r. Result r -> Either [Char] r
A.eitherResult Result Response
res of
Left [Char]
e -> forall a. (?callStack::CallStack) => [Char] -> a
Misc.errorstar forall a b. (a -> b) -> a -> b
$ [Char]
"SMTREAD:" forall a. [a] -> [a] -> [a]
++ [Char]
e
Right Response
r -> do
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) (\Handle
h -> Handle -> Text -> IO ()
LTIO.hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ Builder -> Text
blt (Builder
"; SMT Says: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> Builder
bShow Response
r)) (Context -> Maybe Handle
ctxLog Context
me)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Context -> Bool
ctxVerbose Context
me) forall a b. (a -> b) -> a -> b
$ Text -> IO ()
LTIO.putStrLn forall a b. (a -> b) -> a -> b
$ Builder -> Text
blt (Builder
"SMT Says: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> Builder
bShow Response
r)
forall (m :: * -> *) a. Monad m => a -> m a
return Response
r
type SmtParser a = Parser T.Text a
responseP :: SmtParser Response
responseP :: SmtParser Response
responseP = Char -> Parser Char
A.char Char
'(' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SmtParser Response
sexpP
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text
A.string Text
"sat" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. Monad m => a -> m a
return Response
Sat
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text
A.string Text
"unsat" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. Monad m => a -> m a
return Response
Unsat
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text
A.string Text
"unknown" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. Monad m => a -> m a
return Response
Unknown
sexpP :: SmtParser Response
sexpP :: SmtParser Response
sexpP = Text -> Parser Text
A.string Text
"error" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> Response
Error forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
errorP)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [(Symbol, Text)] -> Response
Values forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SmtParser [(Symbol, Text)]
valuesP
errorP :: SmtParser T.Text
errorP :: Parser Text
errorP = Parser ()
A.skipSpace forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> Parser Char
A.char Char
'"' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Char -> Bool) -> Parser Text
A.takeWhile1 (forall a. Eq a => a -> a -> Bool
/=Char
'"') forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser Text
A.string Text
"\")"
valuesP :: SmtParser [(Symbol, T.Text)]
valuesP :: SmtParser [(Symbol, Text)]
valuesP = forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
A.many1' SmtParser (Symbol, Text)
pairP forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
A.char Char
')'
pairP :: SmtParser (Symbol, T.Text)
pairP :: SmtParser (Symbol, Text)
pairP =
do Parser ()
A.skipSpace
Char
_ <- Char -> Parser Char
A.char Char
'('
!Symbol
x <- SmtParser Symbol
symbolP
Parser ()
A.skipSpace
!Text
v <- Parser Text
valueP
Char
_ <- Char -> Parser Char
A.char Char
')'
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
x,Text
v)
symbolP :: SmtParser Symbol
symbolP :: SmtParser Symbol
symbolP = forall a. Symbolic a => a -> Symbol
symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> Parser Text
A.takeWhile1 (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace)
valueP :: SmtParser T.Text
valueP :: Parser Text
valueP = Parser Text
negativeP
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Char -> Bool) -> Parser Text
A.takeWhile1 (\Char
c -> Bool -> Bool
not (Char
c forall a. Eq a => a -> a -> Bool
== Char
')' Bool -> Bool -> Bool
|| Char -> Bool
isSpace Char
c))
negativeP :: SmtParser T.Text
negativeP :: Parser Text
negativeP
= do Text
v <- Char -> Parser Char
A.char Char
'(' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Char -> Bool) -> Parser Text
A.takeWhile1 (forall a. Eq a => a -> a -> Bool
/=Char
')') forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
A.char Char
')'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Text
"(" forall a. Semigroup a => a -> a -> a
<> Text
v forall a. Semigroup a => a -> a -> a
<> Text
")"
smtWriteRaw :: Context -> Raw -> IO ()
smtWriteRaw :: Context -> Text -> IO ()
smtWriteRaw Context
me !Text
s = do
Handle -> Text -> IO ()
hPutStrLnNow (Context -> Handle
ctxIn Context
me) Text
s
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> Text -> IO ()
`LTIO.hPutStrLn` Text
s) (Context -> Maybe Handle
ctxLog Context
me)
smtReadRaw :: Context -> IO T.Text
smtReadRaw :: Context -> IO Text
smtReadRaw Context
me = do
Bool
eof <- Handle -> IO Bool
hIsEOF (Context -> Handle
ctxOut Context
me)
if Bool
eof then forall a. (?callStack::CallStack) => [Char] -> a
Misc.errorstar [Char]
"SMT returned End of File" else
Handle -> IO Text
TIO.hGetLine (Context -> Handle
ctxOut Context
me)
{-# SCC smtReadRaw #-}
hPutStrLnNow :: Handle -> LT.Text -> IO ()
hPutStrLnNow :: Handle -> Text -> IO ()
hPutStrLnNow Handle
h !Text
s = Handle -> Text -> IO ()
LTIO.hPutStrLn Handle
h Text
s forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
h
{-# SCC hPutStrLnNow #-}
makeContext :: Config -> FilePath -> IO Context
makeContext :: Config -> [Char] -> IO Context
makeContext Config
cfg [Char]
f
= do Context
me <- Config -> IO Context
makeProcess Config
cfg
[Text]
pre <- Config -> SMTSolver -> Context -> IO [Text]
smtPreamble Config
cfg (Config -> SMTSolver
solver Config
cfg) Context
me
Bool -> [Char] -> IO ()
createDirectoryIfMissing Bool
True forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
takeDirectory [Char]
smtFile
Handle
hLog <- [Char] -> IOMode -> IO Handle
openFile [Char]
smtFile IOMode
WriteMode
Handle -> BufferMode -> IO ()
hSetBuffering Handle
hLog forall a b. (a -> b) -> a -> b
$ Maybe Int -> BufferMode
BlockBuffering forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int
1024forall a. Num a => a -> a -> a
*Int
1024forall a. Num a => a -> a -> a
*Int
64
let me' :: Context
me' = Context
me { ctxLog :: Maybe Handle
ctxLog = forall a. a -> Maybe a
Just Handle
hLog }
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Context -> Text -> IO ()
smtWrite Context
me') [Text]
pre
forall (m :: * -> *) a. Monad m => a -> m a
return Context
me'
where
smtFile :: [Char]
smtFile = Ext -> [Char] -> [Char]
extFileName Ext
Smt2 [Char]
f
makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context
makeContextWithSEnv :: Config -> [Char] -> SymEnv -> IO Context
makeContextWithSEnv Config
cfg [Char]
f SymEnv
env = do
Context
ctx <- Config -> [Char] -> IO Context
makeContext Config
cfg [Char]
f
let ctx' :: Context
ctx' = Context
ctx {ctxSymEnv :: SymEnv
ctxSymEnv = SymEnv
env}
Context -> IO ()
declare Context
ctx'
forall (m :: * -> *) a. Monad m => a -> m a
return Context
ctx'
makeContextNoLog :: Config -> IO Context
makeContextNoLog :: Config -> IO Context
makeContextNoLog Config
cfg
= do Context
me <- Config -> IO Context
makeProcess Config
cfg
[Text]
pre <- Config -> SMTSolver -> Context -> IO [Text]
smtPreamble Config
cfg (Config -> SMTSolver
solver Config
cfg) Context
me
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Context -> Text -> IO ()
smtWrite Context
me) [Text]
pre
forall (m :: * -> *) a. Monad m => a -> m a
return Context
me
makeProcess :: Config -> IO Context
makeProcess :: Config -> IO Context
makeProcess Config
cfg
= do (Handle
hIn, Handle
hOut, Handle
_ ,ProcessHandle
pid) <- [Char] -> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveCommand forall a b. (a -> b) -> a -> b
$ SMTSolver -> [Char]
smtCmd (Config -> SMTSolver
solver Config
cfg)
Bool
loud <- IO Bool
isLoud
Handle -> BufferMode -> IO ()
hSetBuffering Handle
hOut forall a b. (a -> b) -> a -> b
$ Maybe Int -> BufferMode
BlockBuffering forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int
1024forall a. Num a => a -> a -> a
*Int
1024forall a. Num a => a -> a -> a
*Int
64
Handle -> BufferMode -> IO ()
hSetBuffering Handle
hIn forall a b. (a -> b) -> a -> b
$ Maybe Int -> BufferMode
BlockBuffering forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int
1024forall a. Num a => a -> a -> a
*Int
1024forall a. Num a => a -> a -> a
*Int
64
TVar Builder
queueTVar <- forall a. a -> IO (TVar a)
newTVarIO forall a. Monoid a => a
mempty
Async ()
writerAsync <- forall a. IO a -> IO (Async a)
async forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Applicative f => f a -> f b
forever forall a b. (a -> b) -> a -> b
$ do
Text
t <- forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ do
Builder
builder <- forall a. TVar a -> STM a
readTVar TVar Builder
queueTVar
let t :: Text
t = Builder -> Text
Builder.toLazyText Builder
builder
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Text -> Bool
LT.null Text
t) forall a. STM a
retry
forall a. TVar a -> a -> STM ()
writeTVar TVar Builder
queueTVar forall a. Monoid a => a
mempty
forall (m :: * -> *) a. Monad m => a -> m a
return Text
t
Handle -> Text -> IO ()
LTIO.hPutStr Handle
hIn Text
t
Handle -> IO ()
hFlush Handle
hIn
forall (m :: * -> *) a. Monad m => a -> m a
return Ctx { ctxPid :: ProcessHandle
ctxPid = ProcessHandle
pid
, ctxIn :: Handle
ctxIn = Handle
hIn
, ctxOut :: Handle
ctxOut = Handle
hOut
, ctxLog :: Maybe Handle
ctxLog = forall a. Maybe a
Nothing
, ctxVerbose :: Bool
ctxVerbose = Bool
loud
, ctxSymEnv :: SymEnv
ctxSymEnv = forall a. Monoid a => a
mempty
, ctxAsync :: Async ()
ctxAsync = Async ()
writerAsync
, ctxTVar :: TVar Builder
ctxTVar = TVar Builder
queueTVar
}
cleanupContext :: Context -> IO ExitCode
cleanupContext :: Context -> IO ExitCode
cleanupContext Ctx{Bool
Maybe Handle
Handle
Async ()
TVar Builder
ProcessHandle
SymEnv
ctxTVar :: TVar Builder
ctxAsync :: Async ()
ctxSymEnv :: SymEnv
ctxVerbose :: Bool
ctxLog :: Maybe Handle
ctxOut :: Handle
ctxIn :: Handle
ctxPid :: ProcessHandle
ctxTVar :: Context -> TVar Builder
ctxAsync :: Context -> Async ()
ctxPid :: Context -> ProcessHandle
ctxOut :: Context -> Handle
ctxIn :: Context -> Handle
ctxLog :: Context -> Maybe Handle
ctxVerbose :: Context -> Bool
ctxSymEnv :: Context -> SymEnv
..} = do
forall a. Async a -> IO ()
cancel Async ()
ctxAsync
[Char] -> Handle -> IO ()
hCloseMe [Char]
"ctxIn" Handle
ctxIn
[Char] -> Handle -> IO ()
hCloseMe [Char]
"ctxOut" Handle
ctxOut
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) ([Char] -> Handle -> IO ()
hCloseMe [Char]
"ctxLog") Maybe Handle
ctxLog
ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ctxPid
hCloseMe :: String -> Handle -> IO ()
hCloseMe :: [Char] -> Handle -> IO ()
hCloseMe [Char]
msg Handle
h = Handle -> IO ()
hClose Handle
h forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(IOException
exn :: IOException) -> [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"OOPS, hClose breaks: " forall a. [a] -> [a] -> [a]
++ [Char]
msg forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show IOException
exn)
smtCmd :: SMTSolver -> String
smtCmd :: SMTSolver -> [Char]
smtCmd SMTSolver
Z3 = [Char]
"z3 -smt2 -in"
smtCmd SMTSolver
Mathsat = [Char]
"mathsat -input=smt2"
smtCmd SMTSolver
Cvc4 = [Char]
"cvc4 --incremental -L smtlib2"
smtPreamble :: Config -> SMTSolver -> Context -> IO [LT.Text]
smtPreamble :: Config -> SMTSolver -> Context -> IO [Text]
smtPreamble Config
cfg SMTSolver
Z3 Context
me
= do [Int]
v <- Context -> IO [Int]
getZ3Version Context
me
SMTSolver -> [Int] -> Config -> IO ()
checkValidStringFlag SMTSolver
Z3 [Int]
v Config
cfg
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Text]
z3_options forall a. [a] -> [a] -> [a]
++ Config -> [Text]
makeMbqi Config
cfg forall a. [a] -> [a] -> [a]
++ Config -> [Text]
makeTimeout Config
cfg forall a. [a] -> [a] -> [a]
++ Config -> SMTSolver -> [Text]
Thy.preamble Config
cfg SMTSolver
Z3
smtPreamble Config
cfg SMTSolver
s Context
_
= SMTSolver -> [Int] -> Config -> IO ()
checkValidStringFlag SMTSolver
s [] Config
cfg forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (Config -> SMTSolver -> [Text]
Thy.preamble Config
cfg SMTSolver
s)
getZ3Version :: Context -> IO [Int]
getZ3Version :: Context -> IO [Int]
getZ3Version Context
me
= do Context -> Text -> IO ()
smtWrite Context
me Text
"(get-info :version)"
Text
resp <- Context -> IO Text
smtReadRaw Context
me
case Text -> Text -> [Text]
T.splitOn Text
"\"" Text
resp of
Text
_:Text
vText:[Text]
_ -> do
let parsedComponents :: [[(a, [Char])]]
parsedComponents = [ forall a. Read a => ReadS a
reads (Text -> [Char]
T.unpack Text
cText) | Text
cText <- Text -> Text -> [Text]
T.splitOn Text
"." Text
vText ]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
[ case [(Int, [Char])]
pComponent of
[(Int
c, [Char]
"")] -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
c
[(Int, [Char])]
xs -> forall a. (?callStack::CallStack) => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Can't parse z3 version: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [(Int, [Char])]
xs
| [(Int, [Char])]
pComponent <- forall {a}. Read a => [[(a, [Char])]]
parsedComponents
]
[Text]
xs -> forall a. (?callStack::CallStack) => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Can't parse z3 (get-info :version): " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Text]
xs
checkValidStringFlag :: SMTSolver -> [Int] -> Config -> IO ()
checkValidStringFlag :: SMTSolver -> [Int] -> Config -> IO ()
checkValidStringFlag SMTSolver
smt [Int]
v Config
cfg
= forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTSolver -> [Int] -> Config -> Bool
noString SMTSolver
smt [Int]
v Config
cfg) forall a b. (a -> b) -> a -> b
$
forall a. Error -> a
die forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
dummySpan ([Char] -> Doc
text [Char]
"stringTheory is only supported by z3 version >=4.2.2")
noString :: SMTSolver -> [Int] -> Config -> Bool
noString :: SMTSolver -> [Int] -> Config -> Bool
noString SMTSolver
smt [Int]
v Config
cfg
= Config -> Bool
stringTheory Config
cfg
Bool -> Bool -> Bool
&& Bool -> Bool
not (SMTSolver
smt forall a. Eq a => a -> a -> Bool
== SMTSolver
Z3 Bool -> Bool -> Bool
&& ([Int]
v forall a. Ord a => a -> a -> Bool
>= [Int
4, Int
4, Int
2]))
smtPush, smtPop :: Context -> IO ()
smtPush :: Context -> IO ()
smtPush Context
me = Context -> Command -> IO ()
interact' Context
me Command
Push
smtPop :: Context -> IO ()
smtPop Context
me = Context -> Command -> IO ()
interact' Context
me Command
Pop
smtDecls :: Context -> [(Symbol, Sort)] -> IO ()
smtDecls :: Context -> [(Symbol, Sort)] -> IO ()
smtDecls = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Symbol -> Sort -> IO ()
smtDecl
smtDecl :: Context -> Symbol -> Sort -> IO ()
smtDecl :: Context -> Symbol -> Sort -> IO ()
smtDecl Context
me Symbol
x Sort
t = Context -> Command -> IO ()
interact' Context
me ( Text -> [SmtSort] -> SmtSort -> Command
Declare (Symbol -> Text
symbolSafeText Symbol
x) [SmtSort]
ins' SmtSort
out')
where
ins' :: [SmtSort]
ins' = Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ins
out' :: SmtSort
out' = Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env Sort
out
([Sort]
ins, Sort
out) = Sort -> ([Sort], Sort)
deconSort Sort
t
_msg :: [Char]
_msg = [Char]
"smtDecl: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp (Symbol
x, Sort
t, [Sort]
ins, Sort
out)
env :: SEnv DataDecl
env = SymEnv -> SEnv DataDecl
seData (Context -> SymEnv
ctxSymEnv Context
me)
smtFuncDecl :: Context -> T.Text -> ([SmtSort], SmtSort) -> IO ()
smtFuncDecl :: Context -> Text -> ([SmtSort], SmtSort) -> IO ()
smtFuncDecl Context
me Text
x ([SmtSort]
ts, SmtSort
t) = Context -> Command -> IO ()
interact' Context
me (Text -> [SmtSort] -> SmtSort -> Command
Declare Text
x [SmtSort]
ts SmtSort
t)
smtDataDecl :: Context -> [DataDecl] -> IO ()
smtDataDecl :: Context -> [DataDecl] -> IO ()
smtDataDecl Context
me [DataDecl]
ds = Context -> Command -> IO ()
interact' Context
me ([DataDecl] -> Command
DeclData [DataDecl]
ds)
deconSort :: Sort -> ([Sort], Sort)
deconSort :: Sort -> ([Sort], Sort)
deconSort Sort
t = case Sort -> Maybe ([Int], [Sort], Sort)
functionSort Sort
t of
Just ([Int]
_, [Sort]
ins, Sort
out) -> ([Sort]
ins, Sort
out)
Maybe ([Int], [Sort], Sort)
Nothing -> ([] , Sort
t )
smtCheckSat :: Context -> Expr -> IO Bool
smtCheckSat :: Context -> Expr -> IO Bool
smtCheckSat Context
me Expr
p
= Context -> Expr -> IO ()
smtAssert Context
me Expr
p forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Response -> Bool
ans forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> Command -> IO Response
command Context
me Command
CheckSat)
where
ans :: Response -> Bool
ans Response
Sat = Bool
True
ans Response
_ = Bool
False
smtAssert :: Context -> Expr -> IO ()
smtAssert :: Context -> Expr -> IO ()
smtAssert Context
me Expr
p = Context -> Command -> IO ()
interact' Context
me (Maybe Int -> Expr -> Command
Assert forall a. Maybe a
Nothing Expr
p)
smtDefineFunc :: Context -> Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> IO ()
smtDefineFunc :: Context -> Symbol -> [(Symbol, Sort)] -> Sort -> Expr -> IO ()
smtDefineFunc Context
me Symbol
name [(Symbol, Sort)]
params Sort
rsort Expr
e =
let env :: SEnv DataDecl
env = SymEnv -> SEnv DataDecl
seData (Context -> SymEnv
ctxSymEnv Context
me)
in Context -> Command -> IO ()
interact' Context
me forall a b. (a -> b) -> a -> b
$
Symbol -> [(Symbol, SmtSort)] -> SmtSort -> Expr -> Command
DefineFunc
Symbol
name
(forall a b. (a -> b) -> [a] -> [b]
map (Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) [(Symbol, Sort)]
params)
(Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False SEnv DataDecl
env Sort
rsort)
Expr
e
asyncCommand :: Context -> Command -> IO ()
asyncCommand :: Context -> Command -> IO ()
asyncCommand Context
me Command
cmd = do
let env :: SymEnv
env = Context -> SymEnv
ctxSymEnv Context
me
cmdText :: Text
cmdText = {-# SCC "asyncCommand-runSmt2" #-} Builder -> Text
Builder.toLazyText forall a b. (a -> b) -> a -> b
$ forall a. SMTLIB2 a => SymEnv -> a -> Builder
runSmt2 SymEnv
env Command
cmd
TVar Builder -> Text -> IO ()
asyncPutStrLn (Context -> TVar Builder
ctxTVar Context
me) Text
cmdText
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Handle -> Text -> IO ()
`LTIO.hPutStrLn` Text
cmdText) (Context -> Maybe Handle
ctxLog Context
me)
where
asyncPutStrLn :: TVar Builder.Builder -> LT.Text -> IO ()
asyncPutStrLn :: TVar Builder -> Text -> IO ()
asyncPutStrLn TVar Builder
tv Text
t = forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$
forall a. TVar a -> (a -> a) -> STM ()
modifyTVar TVar Builder
tv (forall a. Monoid a => a -> a -> a
`mappend` (Text -> Builder
Builder.fromLazyText Text
t forall a. Monoid a => a -> a -> a
`mappend` forall a. IsString a => [Char] -> a
Builder.fromString [Char]
"\n"))
smtAssertAsync :: Context -> Expr -> IO ()
smtAssertAsync :: Context -> Expr -> IO ()
smtAssertAsync Context
me Expr
p = Context -> Command -> IO ()
asyncCommand Context
me forall a b. (a -> b) -> a -> b
$ Maybe Int -> Expr -> Command
Assert forall a. Maybe a
Nothing Expr
p
smtCheckUnsatAsync :: Context -> IO ()
smtCheckUnsatAsync :: Context -> IO ()
smtCheckUnsatAsync Context
me = Context -> Command -> IO ()
asyncCommand Context
me Command
CheckSat
smtBracketAsyncAt :: SrcSpan -> Context -> String -> IO a -> IO a
smtBracketAsyncAt :: forall a. SrcSpan -> Context -> [Char] -> IO a -> IO a
smtBracketAsyncAt SrcSpan
sp Context
x [Char]
y IO a
z = forall a. Context -> [Char] -> IO a -> IO a
smtBracketAsync Context
x [Char]
y IO a
z forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` forall a. SrcSpan -> Error -> a
dieAt SrcSpan
sp
smtBracketAsync :: Context -> String -> IO a -> IO a
smtBracketAsync :: forall a. Context -> [Char] -> IO a -> IO a
smtBracketAsync Context
me [Char]
_msg IO a
a = do
Context -> IO ()
smtPushAsync Context
me
a
r <- IO a
a
Context -> IO ()
smtPopAsync Context
me
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
smtPushAsync, smtPopAsync :: Context -> IO ()
smtPushAsync :: Context -> IO ()
smtPushAsync Context
me = Context -> Command -> IO ()
asyncCommand Context
me Command
Push
smtPopAsync :: Context -> IO ()
smtPopAsync Context
me = Context -> Command -> IO ()
asyncCommand Context
me Command
Pop
{-# SCC readCheckUnsat #-}
readCheckUnsat :: Context -> IO Bool
readCheckUnsat :: Context -> IO Bool
readCheckUnsat Context
me = Response -> Bool
respSat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> IO Response
smtRead Context
me
smtAssertAxiom :: Context -> Triggered Expr -> IO ()
smtAssertAxiom :: Context -> Triggered Expr -> IO ()
smtAssertAxiom Context
me Triggered Expr
p = Context -> Command -> IO ()
interact' Context
me (Triggered Expr -> Command
AssertAx Triggered Expr
p)
smtDistinct :: Context -> [Expr] -> IO ()
smtDistinct :: Context -> ListNE Expr -> IO ()
smtDistinct Context
me ListNE Expr
az = Context -> Command -> IO ()
interact' Context
me (ListNE Expr -> Command
Distinct ListNE Expr
az)
smtCheckUnsat :: Context -> IO Bool
smtCheckUnsat :: Context -> IO Bool
smtCheckUnsat Context
me = Response -> Bool
respSat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> Command -> IO Response
command Context
me Command
CheckSat
smtBracketAt :: SrcSpan -> Context -> String -> IO a -> IO a
smtBracketAt :: forall a. SrcSpan -> Context -> [Char] -> IO a -> IO a
smtBracketAt SrcSpan
sp Context
x [Char]
y IO a
z = forall a. Context -> [Char] -> IO a -> IO a
smtBracket Context
x [Char]
y IO a
z forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` forall a. SrcSpan -> Error -> a
dieAt SrcSpan
sp
smtBracket :: Context -> String -> IO a -> IO a
smtBracket :: forall a. Context -> [Char] -> IO a -> IO a
smtBracket Context
me [Char]
_msg IO a
a = do
Context -> IO ()
smtPush Context
me
a
r <- IO a
a
Context -> IO ()
smtPop Context
me
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
respSat :: Response -> Bool
respSat :: Response -> Bool
respSat Response
Unsat = Bool
True
respSat Response
Sat = Bool
False
respSat Response
Unknown = Bool
False
respSat Response
r = forall a. Error -> a
die forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
dummySpan forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text ([Char]
"crash: SMTLIB2 respSat = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Response
r)
interact' :: Context -> Command -> IO ()
interact' :: Context -> Command -> IO ()
interact' Context
me Command
cmd = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ Context -> Command -> IO Response
command Context
me Command
cmd
makeTimeout :: Config -> [LT.Text]
makeTimeout :: Config -> [Text]
makeTimeout Config
cfg
| Just Int
i <- Config -> Maybe Int
smtTimeout Config
cfg = [ [Char] -> Text
LT.pack ([Char]
"\n(set-option :timeout " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i forall a. [a] -> [a] -> [a]
++ [Char]
")\n")]
| Bool
otherwise = [Text
""]
makeMbqi :: Config -> [LT.Text]
makeMbqi :: Config -> [Text]
makeMbqi Config
cfg
| Config -> Bool
gradual Config
cfg = [Text
""]
| Bool
otherwise = [Text
"\n(set-option :smt.mbqi false)"]
z3_options :: [LT.Text]
z3_options :: [Text]
z3_options
= [ Text
"(set-option :auto-config false)"
, Text
"(set-option :model true)" ]
declare :: Context -> IO ()
declare :: Context -> IO ()
declare Context
me = do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[DataDecl]]
dss forall a b. (a -> b) -> a -> b
$ Context -> [DataDecl] -> IO ()
smtDataDecl Context
me
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Symbol, Sort)]
thyXTs forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ Context -> Symbol -> Sort -> IO ()
smtDecl Context
me
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Symbol, Sort)]
qryXTs forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ Context -> Symbol -> Sort -> IO ()
smtDecl Context
me
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Text, ([SmtSort], SmtSort))]
ats forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ Context -> Text -> ([SmtSort], SmtSort) -> IO ()
smtFuncDecl Context
me
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ListNE Expr]
ess forall a b. (a -> b) -> a -> b
$ Context -> ListNE Expr -> IO ()
smtDistinct Context
me
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ListNE Expr
axs forall a b. (a -> b) -> a -> b
$ Context -> Expr -> IO ()
smtAssert Context
me
where
env :: SymEnv
env = Context -> SymEnv
ctxSymEnv Context
me
dss :: [[DataDecl]]
dss = SymEnv -> [[DataDecl]]
dataDeclarations SymEnv
env
lts :: [(Symbol, Sort)]
lts = forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> SEnv Sort
F.seLits forall a b. (a -> b) -> a -> b
$ SymEnv
env
ess :: [ListNE Expr]
ess = [(Symbol, Sort)] -> [ListNE Expr]
distinctLiterals [(Symbol, Sort)]
lts
axs :: ListNE Expr
axs = [(Symbol, Sort)] -> ListNE Expr
Thy.axiomLiterals [(Symbol, Sort)]
lts
thyXTs :: [(Symbol, Sort)]
thyXTs = forall a. (a -> Bool) -> [a] -> [a]
filter (forall {b}. Int -> (Symbol, b) -> Bool
isKind Int
1) [(Symbol, Sort)]
xts
qryXTs :: [(Symbol, Sort)]
qryXTs = forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd forall {a}. Elaborate a => a -> a
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter (forall {b}. Int -> (Symbol, b) -> Bool
isKind Int
2) [(Symbol, Sort)]
xts
isKind :: Int -> (Symbol, b) -> Bool
isKind Int
n = (Int
n forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> Symbol -> Int
symKind SymEnv
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst
xts :: [(Symbol, Sort)]
xts = SEnv Sort -> [(Symbol, Sort)]
symbolSorts (SymEnv -> SEnv Sort
F.seSort SymEnv
env)
tx :: a -> a
tx = forall a. Elaborate a => Located [Char] -> SymEnv -> a -> a
elaborate Located [Char]
"declare" SymEnv
env
ats :: [(Text, ([SmtSort], SmtSort))]
ats = SymEnv -> [(Text, ([SmtSort], SmtSort))]
funcSortVars SymEnv
env
symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)]
symbolSorts :: SEnv Sort -> [(Symbol, Sort)]
symbolSorts SEnv Sort
env = [(Symbol
x, Sort -> Sort
tx Sort
t) | (Symbol
x, Sort
t) <- forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv Sort
env ]
where
tx :: Sort -> Sort
tx t :: Sort
t@(FObj Symbol
a) = forall a. a -> Maybe a -> a
fromMaybe Sort
t (forall a. Symbol -> SEnv a -> Maybe a
F.lookupSEnv Symbol
a SEnv Sort
env)
tx Sort
t = Sort
t
dataDeclarations :: SymEnv -> [[DataDecl]]
dataDeclarations :: SymEnv -> [[DataDecl]]
dataDeclarations = [DataDecl] -> [[DataDecl]]
orderDeclarations forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> SEnv DataDecl
F.seData
funcSortVars :: F.SymEnv -> [(T.Text, ([F.SmtSort], F.SmtSort))]
funcSortVars :: SymEnv -> [(Text, ([SmtSort], SmtSort))]
funcSortVars SymEnv
env = [(Symbol -> FuncSort -> Text
var Symbol
applyName FuncSort
t , forall {b}. (SmtSort, b) -> ([SmtSort], b)
appSort FuncSort
t) | FuncSort
t <- [FuncSort]
ts]
forall a. [a] -> [a] -> [a]
++ [(Symbol -> FuncSort -> Text
var Symbol
coerceName FuncSort
t , ([SmtSort
t1],SmtSort
t2)) | t :: FuncSort
t@(SmtSort
t1, SmtSort
t2) <- [FuncSort]
ts]
forall a. [a] -> [a] -> [a]
++ [(Symbol -> FuncSort -> Text
var Symbol
lambdaName FuncSort
t , forall {a}. (a, a) -> ([a], SmtSort)
lamSort FuncSort
t) | FuncSort
t <- [FuncSort]
ts]
forall a. [a] -> [a] -> [a]
++ [(Symbol -> FuncSort -> Text
var (Int -> Symbol
lamArgSymbol Int
i) FuncSort
t , forall {b} {b} {a}. (b, b) -> ([a], b)
argSort FuncSort
t) | t :: FuncSort
t@(SmtSort
_,SmtSort
F.SInt) <- [FuncSort]
ts, Int
i <- [Int
1..Int
Thy.maxLamArg] ]
where
var :: Symbol -> FuncSort -> Text
var Symbol
n = forall a. PPrint a => Symbol -> SymEnv -> a -> FuncSort -> Text
F.symbolAtSmtName Symbol
n SymEnv
env ()
ts :: [FuncSort]
ts = forall k v. HashMap k v -> [k]
M.keys (SymEnv -> HashMap FuncSort Int
F.seAppls SymEnv
env)
appSort :: (SmtSort, b) -> ([SmtSort], b)
appSort (SmtSort
s,b
t) = ([SmtSort
F.SInt, SmtSort
s], b
t)
lamSort :: (a, a) -> ([a], SmtSort)
lamSort (a
s,a
t) = ([a
s, a
t], SmtSort
F.SInt)
argSort :: (b, b) -> ([a], b)
argSort (b
s,b
_) = ([] , b
s)
symKind :: F.SymEnv -> F.Symbol -> Int
symKind :: SymEnv -> Symbol -> Int
symKind SymEnv
env Symbol
x = case TheorySymbol -> Sem
F.tsInterp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> SymEnv -> Maybe TheorySymbol
F.symEnvTheory Symbol
x SymEnv
env of
Just Sem
F.Theory -> Int
0
Just Sem
F.Ctor -> Int
0
Just Sem
F.Test -> Int
0
Just Sem
F.Field -> Int
0
Just Sem
F.Uninterp -> Int
1
Maybe Sem
Nothing -> Int
2
distinctLiterals :: [(F.Symbol, F.Sort)] -> [[F.Expr]]
distinctLiterals :: [(Symbol, Sort)] -> [ListNE Expr]
distinctLiterals [(Symbol, Sort)]
xts = [ ListNE Expr
es | (Sort
_, ListNE Expr
es) <- [(Sort, ListNE Expr)]
tess ]
where
tess :: [(Sort, ListNE Expr)]
tess = forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Sort
t, forall a. Expression a => a -> Expr
F.expr Symbol
x) | (Symbol
x, Sort
t) <- [(Symbol, Sort)]
xts, Sort -> Bool
notFun Sort
t]
notFun :: Sort -> Bool
notFun = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Bool
F.isFunctionSortedReft forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> Reft -> SortedReft
`F.RR` Reft
F.trueReft)