{-# LANGUAGE OverloadedStrings #-}
module SMTLIB.Backends (Backend (..), Solver, initSolver, command, command_) where
import Data.ByteString.Builder (Builder)
import qualified Data.ByteString.Lazy.Char8 as LBS
import Data.Char (isSpace)
import Data.IORef (IORef, atomicModifyIORef, newIORef)
import Data.List (intersperse)
import Prelude hiding (log)
data Backend = Backend
{
Backend -> Builder -> IO ByteString
send :: Builder -> IO LBS.ByteString
}
type Queue = IORef Builder
putQueue :: Queue -> Builder -> IO ()
putQueue :: Queue -> Builder -> IO ()
putQueue Queue
q Builder
cmd = Queue -> (Builder -> (Builder, ())) -> IO ()
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef Queue
q ((Builder -> (Builder, ())) -> IO ())
-> (Builder -> (Builder, ())) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Builder
cmds ->
(Builder
cmds Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cmd, ())
flushQueue :: Queue -> IO Builder
flushQueue :: Queue -> IO Builder
flushQueue Queue
q = Queue -> (Builder -> (Builder, Builder)) -> IO Builder
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef Queue
q ((Builder -> (Builder, Builder)) -> IO Builder)
-> (Builder -> (Builder, Builder)) -> IO Builder
forall a b. (a -> b) -> a -> b
$ \Builder
cmds ->
(Builder
forall a. Monoid a => a
mempty, Builder
cmds)
data Solver = Solver
{
Solver -> Backend
backend :: Backend,
Solver -> Maybe Queue
queue :: Maybe Queue
}
initSolver ::
Backend ->
Bool ->
IO Solver
initSolver :: Backend -> Bool -> IO Solver
initSolver Backend
solverBackend Bool
lazy = do
Maybe Queue
solverQueue <-
if Bool
lazy
then do
Queue
ref <- Builder -> IO Queue
forall a. a -> IO (IORef a)
newIORef Builder
forall a. Monoid a => a
mempty
Maybe Queue -> IO (Maybe Queue)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Queue -> IO (Maybe Queue))
-> Maybe Queue -> IO (Maybe Queue)
forall a b. (a -> b) -> a -> b
$ Queue -> Maybe Queue
forall a. a -> Maybe a
Just Queue
ref
else Maybe Queue -> IO (Maybe Queue)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Queue
forall a. Maybe a
Nothing
let solver :: Solver
solver = Backend -> Maybe Queue -> Solver
Solver Backend
solverBackend Maybe Queue
solverQueue
if Bool
lazy
then () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else
Solver -> Builder -> Builder -> IO ()
setOption Solver
solver Builder
"print-success" Builder
"true"
Solver -> Builder -> Builder -> IO ()
setOption Solver
solver Builder
"produce-models" Builder
"true"
Solver -> IO Solver
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
solver
command :: Solver -> Builder -> IO LBS.ByteString
command :: Solver -> Builder -> IO ByteString
command Solver
solver Builder
cmd = do
Backend -> Builder -> IO ByteString
send (Solver -> Backend
backend Solver
solver)
(Builder -> IO ByteString) -> IO Builder -> IO ByteString
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< case Solver -> Maybe Queue
queue Solver
solver of
Maybe Queue
Nothing -> Builder -> IO Builder
forall (m :: * -> *) a. Monad m => a -> m a
return (Builder -> IO Builder) -> Builder -> IO Builder
forall a b. (a -> b) -> a -> b
$ Builder
cmd
Just Queue
q -> (Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cmd) (Builder -> Builder) -> IO Builder -> IO Builder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Queue -> IO Builder
flushQueue Queue
q
command_ :: Solver -> Builder -> IO ()
command_ :: Solver -> Builder -> IO ()
command_ Solver
solver Builder
cmd =
case Solver -> Maybe Queue
queue Solver
solver of
Maybe Queue
Nothing -> do
ByteString
res <- Backend -> Builder -> IO ByteString
send (Solver -> Backend
backend Solver
solver) Builder
cmd
if ByteString -> ByteString
trim ByteString
res ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
"success"
then () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else
[Char] -> IO ()
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$
[[Char]] -> [Char]
unlines
[ [Char]
"Unexpected result from the SMT solver:",
[Char]
" Expected: success",
[Char]
" Got: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ByteString -> [Char]
forall a. Show a => a -> [Char]
show ByteString
res
]
Just Queue
q -> Queue -> Builder -> IO ()
putQueue Queue
q Builder
cmd
where
trim :: ByteString -> ByteString
trim = (Char -> Bool) -> ByteString -> ByteString
LBS.dropWhile Char -> Bool
isSpace (ByteString -> ByteString)
-> (ByteString -> ByteString) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
LBS.reverse (ByteString -> ByteString)
-> (ByteString -> ByteString) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ByteString -> ByteString
LBS.dropWhile Char -> Bool
isSpace (ByteString -> ByteString)
-> (ByteString -> ByteString) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
LBS.reverse
setOption :: Solver -> Builder -> Builder -> IO ()
setOption :: Solver -> Builder -> Builder -> IO ()
setOption Solver
solver Builder
name Builder
value = Solver -> Builder -> IO ()
command_ Solver
solver (Builder -> IO ()) -> Builder -> IO ()
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
list [Builder
"set-option", Builder
":" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
name, Builder
value]
list :: [Builder] -> Builder
list :: [Builder] -> Builder
list [Builder]
bs = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat (Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
intersperse Builder
" " [Builder]
bs) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"