Updated remaining modules to work with updated LogData interface to what4 solvers

what4-abc/src/What4/Solver/ABC.hs

@@ -99,9 +99,9 @@ abcAdapter =
    SolverAdapter
    { solver_adapter_name = "abc"
    , solver_adapter_config_options = abcOptions
-   , solver_adapter_check_sat = \sym logLn rsn ps _auxOutput cont -> do
+   , solver_adapter_check_sat = \sym logData ps cont -> do
            p <- andAllOf sym folded ps
-           res <- checkSat sym logLn rsn p
+           res <- checkSat sym logData p
            cont . runIdentity . traverseSatResult (\x -> pure (x,Nothing)) pure $ res
    , solver_adapter_write_smt2 = \_ _ _ -> do
        fail "ABC backend does not support writing SMTLIB2 files."
@@ -123,14 +123,14 @@ genericSatAdapter =
    SolverAdapter
    { solver_adapter_name = "sat"
    , solver_adapter_config_options = genericSatOptions
-   , solver_adapter_check_sat = \sym logLn _rsn ps _auxOutput cont -> do
+   , solver_adapter_check_sat = \sym logData ps cont -> do
        let cfg = getConfiguration sym
        cmd <- T.unpack <$> (getOpt =<< getOptionSetting satCommand cfg)
        let mkCommand path = do
              let var_map = Map.fromList [("1",path)]
              Env.expandEnvironmentPath var_map cmd
        p <- andAllOf sym folded ps
-       mmdl <- runExternalDimacsSolver logLn mkCommand p
+       mmdl <- runExternalDimacsSolver (logCallbackVerbose logData) mkCommand p
        cont . runIdentity . traverseSatResult (\x -> pure (x,Nothing)) pure $ mmdl
    , solver_adapter_write_smt2 = \_ _ _ -> do
        fail "SAT backend does not support writing SMTLIB2 files."
@@ -657,11 +657,10 @@ recordBoundVar ntk info = do
 -- | Expression to check is satisfiable.
 checkSat :: IsExprBuilder sym
          => sym
-         -> (Int -> String -> IO ())
-         -> String
+         -> LogData
          -> BoolExpr t
          -> IO (SatResult (GroundEvalFn t) ())
-checkSat sym logLn rsn e = do
+checkSat sym logData e = do
   let cfg = getConfiguration sym
   -- Get variables in expression.
   let vars = predicateVarInfo e
@@ -671,7 +670,7 @@ checkSat sym logLn rsn e = do
   logSolverEvent sym
     SolverStartSATQuery
     { satQuerySolverName = "ABC"
-    , satQueryReason = rsn
+    , satQueryReason = logReason logData
     }
   withNetwork $ \ntk -> do
     -- Get network
@@ -709,11 +708,11 @@ checkSat sym logLn rsn e = do
     p <- foldM (GIA.and (gia ntk)) c preds
     -- Add bindings for uninterpreted bindings.
     res <- if Map.null a_quants then do
-             logLn 2 "Calling ABC's SAT solver"
+             logCallbackVerbose logData 2 "Calling ABC's SAT solver"
              r <- GIA.checkSat (gia ntk) p
              evaluateSatModel ntk [] r
            else do
-             logLn 2 "Calling ABC's QBF solver"
+             logCallbackVerbose logData 2 "Calling ABC's QBF solver"
              runQBF ntk exist_cnt p max_qbf_iter
     logSolverEvent sym
       SolverEndSATQuery

what4-blt/src/What4/Solver/BLT.hs

@@ -110,8 +110,8 @@ bltAdapter =
    SolverAdapter
    { solver_adapter_name = "blt"
    , solver_adapter_config_options = bltOptions
-   , solver_adapter_check_sat = \sym _ rsn ps _auxOutput cont ->
-           runBLTInOverride sym rsn ps
+   , solver_adapter_check_sat = \sym logData ps cont ->
+           runBLTInOverride sym logData ps
              (cont . runIdentity . traverseSatResult (\x -> pure (x,Nothing)) pure)
    , solver_adapter_write_smt2 = \_ _ _ -> do
        fail "BLT backend does not support writing SMTLIB2 files."
@@ -119,18 +119,18 @@ bltAdapter =
 
 runBLTInOverride :: IsExprBuilder sym
                  => sym
-                 -> String
+                 -> LogData
                  -> [BoolExpr t] -- ^ propositions to check
                  -> (SatResult (GroundEvalFn t) () -> IO a)
                  -> IO a
-runBLTInOverride sym rsn ps contFn = do
+runBLTInOverride sym logData ps contFn = do
   let cfg = getConfiguration sym
   epar <- parseBLTParams . T.unpack <$> (getOpt =<< getOptionSetting bltParams cfg)
   par  <- either fail return epar
   logSolverEvent sym
     SolverStartSATQuery
     { satQuerySolverName = "BLT"
-    , satQueryReason = rsn
+    , satQueryReason = logReason logData
     }
   withHandle par $ \h -> do
     forM_ ps (assume h)

what4/src/What4/Solver.hs

@@ -16,7 +16,7 @@ module What4.Solver
   , solverAdapterOptions
   , LogData(..)
   , logCallback
-
+  , defaultLogData
 
     -- * Boolector
   , boolectorAdapter