You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
this unknown check-sat response "" may actually be in instance of clearInput not working. I added this remark/question to the source:
-- I THINK this will pull characters from the solver's output
-- (that we will ignore) until it blocks.
-- E.g., a solver may send newlines and comments (traces, timing)
-- The problem is that the solver may be slow in sending a comment
-- (temporarily blocking) so we assume it's done,
-- and mistake a slow comment for an actual response.
clearInput :: SMTPipe -> IO ()
clearInput pipe = do
let stdout = getStdout $ processHandle pipe
r <- hReady stdout
if r
then (do
_ <- BS.hGetSome stdout 1024
clearInput pipe)
else return ()
putRequest :: SMTPipe -> L.Lisp -> IO ()
putRequest pipe expr = do
clearInput pipe -- we pull the character stream until it blocks.
-- then we send the request. so we can be sure that the following characters
-- are indeed from the response to this request.
let stdin = getStdin $ processHandle pipe
toByteStringIO (BS.hPutStr stdin) (mappend (L.fromLispExpr expr) flush)
BS8.hPutStrLn stdin ""
hFlush stdin
I am getting spurious
smtlib2: unknown check-sat response: ""
might be solved with https://github.com/fpco/typed-process
e.g., I am doing this here https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/master/src/Ersatz/Solver/Pipe.hs
The text was updated successfully, but these errors were encountered: