Remove stdin/stdout duplicate from Solver; use values from WriterConn.

what4/src/What4/Protocol/Online.hs

@@ -18,6 +18,8 @@ module What4.Protocol.Online
   ( OnlineSolver(..)
   , AnOnlineSolver(..)
   , SolverProcess(..)
+  , solverStdin
+  , solverResponse
   , SolverGoalTimeout(..)
   , getGoalTimeoutInSeconds
   , ErrorBehavior(..)
@@ -134,12 +136,6 @@ data SolverProcess scope solver = SolverProcess
   , solverHandle :: !ProcessHandle
     -- ^ Handle to the solver process
 
-  , solverStdin :: !(Streams.OutputStream Text)
-    -- ^ Standard in for the solver process.
-
-  , solverResponse :: !(Streams.InputStream Text)
-    -- ^ Wrap the solver's stdout, for easier parsing of responses.
-
   , solverErrorBehavior :: !ErrorBehavior
     -- ^ Indicate this solver's behavior following an error response
 
@@ -176,6 +172,15 @@ data SolverProcess scope solver = SolverProcess
   }
 
 
+-- | Standard input stream for the solver process.
+solverStdin :: (SolverProcess t solver) -> (Streams.OutputStream Text)
+solverStdin = connHandle . solverConn
+
+-- | The solver's stdout, for easier parsing of responses.
+solverResponse :: (SolverProcess t solver) -> (Streams.InputStream Text)
+solverResponse = connInputHandle . solverConn
+
+
 -- | An impolite way to shut down a solver.  Prefer to use
 --   `shutdownSolverProcess`, unless the solver is unresponsive
 --   or in some unrecoverable error state.

what4/src/What4/Protocol/SMTLib2.hs

@@ -1076,11 +1076,9 @@ startSolver solver ack setup feats auxOutput sym = do
   return $! SolverProcess
             { solverConn     = writer
             , solverCleanupCallback = cleanupProcess hdls
-            , solverStdin    = in_stream
             , solverStderr   = err_reader
             , solverHandle   = ph
             , solverErrorBehavior = errBeh
-            , solverResponse = out_stream
             , solverEvalFuns = smtEvalFuns writer out_stream
             , solverLogFn    = I.logSolverEvent sym
             , solverName     = show solver

what4/src/What4/Protocol/SMTWriter.hs

@@ -591,6 +591,7 @@ data StackEntry t (h :: Type) = StackEntry
 data WriterConn t (h :: Type) =
   WriterConn { smtWriterName :: !String
                -- ^ Name of writer for error reporting purposes.
+
              , connHandle :: !(OutputStream Text)
                -- ^ Handle to write to
 

what4/src/What4/Solver/Yices.hs

@@ -693,10 +693,8 @@ yicesStartSolver features auxOutput sym = do -- FIXME
 
   return $! SolverProcess { solverConn   = conn
                           , solverCleanupCallback = cleanupProcess hdls
-                          , solverStdin  = in_stream'
                           , solverStderr = err_reader
                           , solverHandle = ph
-                          , solverResponse = out_stream
                           , solverErrorBehavior = ContinueOnError
                           , solverEvalFuns = smtEvalFuns conn out_stream
                           , solverLogFn = logSolverEvent sym
@@ -1155,8 +1153,6 @@ runYicesInOverride sym logData conditions resultFn = do
       let yp = SolverProcess { solverConn = c
                              , solverCleanupCallback = cleanupProcess hdls
                              , solverHandle = ph
-                             , solverStdin  = in_stream
-                             , solverResponse = out_stream
                              , solverErrorBehavior = ImmediateExit
                              , solverStderr = err_reader
                              , solverEvalFuns = smtEvalFuns c out_stream