generated from tweag/project
/
Backends.hs
162 lines (148 loc) · 6.4 KB
/
Backends.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
{-# LANGUAGE OverloadedStrings #-}
module SMTLIB.Backends
( Backend (..),
QueuingFlag (..),
Solver,
initSolver,
command,
command_,
flushQueue,
)
where
import Control.Monad ((<=<))
import Data.ByteString.Builder (Builder)
import qualified Data.ByteString.Lazy.Char8 as LBS
import Data.Char (isSpace)
import Data.IORef (IORef, modifyIORef, newIORef, readIORef, writeIORef)
import Data.List (intersperse)
import Prelude hiding (log)
-- | The type of solver backends. SMTLib2 commands are sent to a backend which
-- processes them and outputs the solver's response.
data Backend = Backend
{ -- | Send a command to the backend.
-- While the implementation depends on the backend, this function is usually
-- *not* thread-safe.
send :: Builder -> IO LBS.ByteString,
-- | Send a command that doesn't produce any response to the backend.
-- The backend may implement this by not reading the output and leaving it
-- for a later read, or reading the output and discarding it immediately.
-- Hence this method should only be used when the command does not produce
-- any response to be outputted.
-- Again, this function may not be thread-safe.
send_ :: Builder -> IO ()
}
type Queue = IORef Builder
-- | A boolean-equivalent datatype indicating whether to enable queuing.
data QueuingFlag = Queuing | NoQueuing
-- | Push a command on the solver's queue of commands to evaluate.
-- The command must not produce any output when evaluated, unless it is the last
-- command added before the queue is flushed.
-- For a fixed queue, this function is *not* thread-safe.
put :: Queue -> Builder -> IO ()
put q cmd = modifyIORef q (<> cmd)
-- | Empty the queue of commands to evaluate and return its content as a bytestring
-- builder.
-- For a fixed queue, this function is *not* thread-safe.
flush :: Queue -> IO Builder
flush q = do
cmds <- readIORef q
writeIORef q mempty
return cmds
-- | A solver is essentially a wrapper around a solver backend. It also comes an
-- optional queue of commands to send to the backend.
--
-- A solver can either be in 'Queuing' mode or 'NoQueuing' mode. In 'NoQueuing'
-- mode, the queue of commands isn't used and the commands are sent to the
-- backend immediately. In 'Queuing' mode, commands whose output are not
-- strictly necessary for the rest of the computation (typically the ones whose
-- output should just be @success@) and that are sent through 'command_' are not
-- sent to the backend immediately, but rather written on the solver's queue.
-- When a command whose output is actually necessary needs to be sent, the queue
-- is flushed and sent as a batch to the backend.
--
-- 'Queuing' mode should be faster as there usually is a non-negligible constant
-- overhead in sending a command to the backend. But since the commands are sent
-- by batches, a command sent to the solver will only produce an error when the
-- queue is flushed, i.e. when a command with interesting output is sent. You
-- thus probably want to stick with 'NoQueuing' mode when debugging. Moreover,
-- when commands are sent by batches, only the last command in the batch may
-- produce an output for parsing to work properly. Hence the @:print-success@
-- option is disabled in 'Queuing' mode, and this should not be overriden
-- manually.
data Solver = Solver
{ -- | The backend processing the commands.
backend :: Backend,
-- | An optional queue to write commands that are to be sent to the solver lazily.
queue :: Maybe Queue
}
-- | Create a new solver and initialize it with some options so that it behaves
-- correctly for our use.
-- In particular, the "print-success" option is disabled in 'Queuing' mode. This
-- should not be overriden manually.
initSolver ::
-- | whether to enable 'Queuing' mode (see 'Solver' for the meaning of this
-- flag)
QueuingFlag ->
-- | the solver backend
Backend ->
IO Solver
initSolver queuing solverBackend = do
solverQueue <- case queuing of
Queuing -> do
ref <- newIORef mempty
return $ Just ref
NoQueuing -> return Nothing
let solver = Solver solverBackend solverQueue
case queuing of
Queuing -> return ()
NoQueuing ->
-- this should not be enabled when the queue is used, as it messes with parsing
-- the outputs of commands that are actually interesting
-- TODO checking for correctness and enabling laziness can be made compatible
-- but it would require the solver backends to return several outputs at once
-- alternatively, we may consider that the user wanting both features should
-- implement their own backend that deals with this
setOption solver "print-success" "true"
setOption solver "produce-models" "true"
return solver
-- | Have the solver evaluate a SMT-LIB command.
-- This forces the queued commands to be evaluated as well, but their results are
-- *not* checked for correctness.
-- For a fixed backend, this function is *not* thread-safe.
command :: Solver -> Builder -> IO LBS.ByteString
command solver cmd = do
send (backend solver)
=<< case queue solver of
Nothing -> return cmd
Just q -> (<> cmd) <$> flush q
-- | A command with no interesting result.
-- In 'NoQueuing' mode, the result is checked for correctness. In 'Queuing'
-- mode, (unless the queue is flushed and evaluated right after) the command
-- must not produce any output when evaluated, and its output is thus in
-- particular not checked for correctness. For a fixed backend, this function is
-- *not* thread-safe.
command_ :: Solver -> Builder -> IO ()
command_ solver cmd =
case queue solver of
Nothing -> do
res <- send (backend solver) cmd
if trim res == "success"
then return ()
else
fail $
unlines
[ "Unexpected result from the SMT solver:",
" Expected: success",
" Got: " ++ show res
]
Just q -> put q cmd
where
trim = LBS.dropWhile isSpace . LBS.reverse . LBS.dropWhile isSpace . LBS.reverse
-- | Force the content of the queue to be sent to the solver.
-- Only useful in queuing mode, does nothing in non-queuing mode.
flushQueue :: Solver -> IO ()
flushQueue solver = maybe (return ()) (send_ (backend solver) <=< flush) $ queue solver
setOption :: Solver -> Builder -> Builder -> IO ()
setOption solver name value = command_ solver $ list ["set-option", ":" <> name, value]
list :: [Builder] -> Builder
list bs = "(" <> mconcat (intersperse " " bs) <> ")"