hasmtlib 2.0.1 → 2.1.0

raw patch · 17 files changed

+163/−98 lines, 17 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +11/−0
• README.md +8/−8
• hasmtlib.cabal +2/−1
• src/Language/Hasmtlib.hs +2/−0
• src/Language/Hasmtlib/Counting.hs +5/−3
• src/Language/Hasmtlib/Solver/Bitwuzla.hs +19/−0
• src/Language/Hasmtlib/Solver/CVC5.hs +4/−5
• src/Language/Hasmtlib/Solver/Common.hs +20/−22
• src/Language/Hasmtlib/Solver/MathSAT.hs +7/−8
• src/Language/Hasmtlib/Solver/OpenSMT.hs +4/−5
• src/Language/Hasmtlib/Solver/Yices.hs +4/−5
• src/Language/Hasmtlib/Solver/Z3.hs +4/−5
• src/Language/Hasmtlib/Type/ArrayMap.hs +9/−9
• src/Language/Hasmtlib/Type/MonadSMT.hs +1/−3
• src/Language/Hasmtlib/Type/OMT.hs +1/−1
• src/Language/Hasmtlib/Type/Pipe.hs +43/−12
• src/Language/Hasmtlib/Type/Solver.hs +19/−11

@@ -6,6 +6,17 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [PVP versioning](https://pvp.haskell.org/). +## v2.1.0 _(2024-07-26)_++### Added+- Added solver Bitwuzla+- Added debugging capabilities for `Pipe` by introducing `debugInteractiveWith`++### Changed+- Yices now uses flag `--incremental` by default+- *(breaking change)* Removed functional dependency `m -> s` from `MonadIncrSMT s m`. This forces you to specify the underlying state when using `interactiveWith`. Therefore `interactiveWith cvc5Living $ do ...` now becomes `interactiveWith @Pipe cvc5Living $ do ...`.+- *(breaking change)* Removed `newtype ProcessSolver` and replaced it with underlying `SMTLIB.Backends.Process.Config`. This may only affect you if you instantiated custom solvers.+ ## v2.0.1 _(2024-07-23)_  ### Added

@@ -1,6 +1,6 @@ [![Hackage](https://img.shields.io/hackage/v/hasmtlib.svg)](https://hackage.haskell.org/package/hasmtlib) ![Static Badge](https://img.shields.io/badge/Lang-GHC2021-blue) [![Haskell-CI](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/bruderj15/Hasmtlib/actions/workflows/haskell-ci.yml) [![License: GPL v3](https://img.shields.io/badge/License-GPLv3-blue.svg)](https://www.gnu.org/licenses/gpl-3.0) -# Hasmtlib+# Hasmtlib - Haskell SMTLib MTL Library  Hasmtlib is a library for generating SMTLib2-problems using a monad. It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.@@ -41,7 +41,7 @@  main :: IO () main = do-  res <- solveWith (solver @SMT cvc5) $ do+  res <- solveWith @SMT (solver cvc5) $ do     setLogic "QF_NRA"      u :: V3 (Expr RealSort) <- variable@@ -71,7 +71,7 @@   ``` - [x] Pure API with Expression-instances for Num, Floating, Bounded, ...   ```haskell-    solveWith (solver @SMT yices) $ do+    solveWith @SMT (solver yices) $ do       setLogic "QF_BV"       x <- var @(BvSort 16)       y <- var@@ -83,16 +83,16 @@     -- | Function that turns a state (usually SMT or OMT) into a result and a solution     type Solver s m = s -> m (Result, Solution)   ```-- [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT & OpenSMT+- [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT, OpenSMT & Bitwuzla   ```haskell-    (result, solution) <- solveWith (solver @SMT mathsat) $ do+    (result, solution) <- solveWith @SMT (solver mathsat) $ do       setLogic "QF_LIA"       assert $ ...   ``` - [x] Incremental solving   ```haskell       cvc5Living <- interactiveSolver cvc5-      interactiveWith cvc5Living $ do+      interactiveWith @Pipe cvc5Living $ do         setLogic "QF_LIA"         setOption $ Incremental True         setOption $ ProduceModels True@@ -108,7 +108,7 @@   ``` - [x] Pure quantifiers `for_all` and `exists`   ```haskell-    solveWith (solver @SMT z3) $ do+    solveWith @SMT (solver z3) $ do       setLogic "LIA"       z <- var @IntSort       assert $ z === 0@@ -120,7 +120,7 @@   ``` - [x] Optimization Modulo Theories (OMT) / MaxSMT   ```haskell-    res <- solveWith (solver @OMT z3) $ do+    res <- solveWith @OMT (solver z3) $ do       setLogic "QF_LIA"       x <- var @IntSort 

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               2.0.1+version:               2.1.0 synopsis:              A monad for interfacing with external SMT solvers description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.@@ -38,6 +38,7 @@                      , Language.Hasmtlib.Internal.Bitvec                      , Language.Hasmtlib.Internal.Render                      , Language.Hasmtlib.Solver.Common+                     , Language.Hasmtlib.Solver.Bitwuzla                      , Language.Hasmtlib.Solver.CVC5                      , Language.Hasmtlib.Solver.MathSAT                      , Language.Hasmtlib.Solver.OpenSMT

@@ -19,6 +19,7 @@   , module Language.Hasmtlib.Counting   , module Language.Hasmtlib.Variable   , module Language.Hasmtlib.Solver.Common+  , module Language.Hasmtlib.Solver.Bitwuzla   , module Language.Hasmtlib.Solver.CVC5   , module Language.Hasmtlib.Solver.Z3   , module Language.Hasmtlib.Solver.Yices@@ -46,6 +47,7 @@ import Language.Hasmtlib.Counting import Language.Hasmtlib.Variable import Language.Hasmtlib.Solver.Common+import Language.Hasmtlib.Solver.Bitwuzla import Language.Hasmtlib.Solver.CVC5 import Language.Hasmtlib.Solver.Z3 import Language.Hasmtlib.Solver.Yices

@@ -9,25 +9,27 @@ import Language.Hasmtlib.Iteable import Data.Proxy +-- | Wrapper for 'count' which takes a 'Proxy'. count' :: forall t f. (Functor f, Foldable f, Num (Expr t)) => Proxy t -> f (Expr BoolSort) -> Expr t count' _ = sum . fmap (\b -> ite b 1 0) {-# INLINEABLE count' #-} +-- | Out of many bool-expressions build a formula which encodes how many of them are 'true'. count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t count = count' (Proxy @t) {-# INLINE count #-} --- | Out of many bool-expressions build a formula which encodes that __at most__ 'k' of them are 'true'+-- | Out of many bool-expressions build a formula which encodes that __at most__ 'k' of them are 'true'. atMost  :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort atMost  k = (<=? k) . count {-# INLINEABLE atMost #-} --- | Out of many bool-expressions build a formula which encodes that __at least__ 'k' of them are 'true'+-- | Out of many bool-expressions build a formula which encodes that __at least__ 'k' of them are 'true'. atLeast :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort atLeast k = (>=? k) . count {-# INLINEABLE atLeast #-} --- | Out of many bool-expressions build a formula which encodes that __exactly__ 'k' of them are 'true'+-- | Out of many bool-expressions build a formula which encodes that __exactly__ 'k' of them are 'true'. exactly :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort exactly k = (=== k) . count {-# INLINEABLE exactly #-}

@@ -0,0 +1,19 @@+module Language.Hasmtlib.Solver.Bitwuzla where++import SMTLIB.Backends.Process++-- | A 'Config' for Bitwuzla.+--   Requires binary @bitwuzla@ to be in path.+--+--   As of v0.5 Bitwuzla uses Cadical as SAT-Solver by default.+--   Make sure it's default SAT-Solver binary - probably @cadical@ - is in path too.+bitwuzla :: Config+bitwuzla = defaultConfig { exe = "bitwuzla", args = [] }++-- | A 'Config' for Bitwuzla which uses Kissat for SAT-Solving.+--   Requires binary @bitwuzla@ and @kissat@ to be in path.+--+-- Combination with Kissat currently behaves weirdly: https://github.com/bitwuzla/bitwuzla/issues/119+--+-- bitwuzlaWithKissat :: Config+-- bitwuzlaWithKissat = defaultConfig { exe = "bitwuzla", args = ["--sat-solver=kissat"] }

@@ -1,9 +1,8 @@ module Language.Hasmtlib.Solver.CVC5 where -import Language.Hasmtlib.Solver.Common-import qualified SMTLIB.Backends.Process as P+import SMTLIB.Backends.Process --- | A 'ProcessSolver' for CVC5.+-- | A 'Config' for CVC5. --   Requires binary @cvc5@ to be in path.-cvc5 :: ProcessSolver-cvc5 = ProcessSolver $ P.defaultConfig { P.exe = "cvc5", P.args = [] }+cvc5 :: Config+cvc5 = defaultConfig { exe = "cvc5", args = [] }

@@ -14,25 +14,23 @@ import Control.Lens import Control.Monad import Control.Monad.IO.Class-import qualified SMTLIB.Backends.Process as P-import qualified SMTLIB.Backends as B---- | A newtype-wrapper for 'P.Config' which configures a solver via external process.-newtype ProcessSolver = ProcessSolver { conf :: P.Config }+import qualified SMTLIB.Backends.Process as Process+import qualified SMTLIB.Backends as Backend --- | Creates a 'Solver' from a 'ProcessSolver'.-solver :: (RenderSeq s, MonadIO m) => ProcessSolver -> Solver s m-solver (ProcessSolver cfg) = processSolver cfg Nothing+-- | Creates a 'Solver' from a 'Process.Config'.+solver :: (RenderSeq s, MonadIO m) => Process.Config -> Solver s m+solver cfg = processSolver cfg Nothing --- | Creates a debugging 'Solver' from a 'ProcessSolver'.-debug :: (RenderSeq s, Default (Debugger s), MonadIO m) => ProcessSolver -> Solver s m-debug (ProcessSolver cfg) = processSolver cfg $ Just def+-- | Creates a debugging 'Solver' from a 'Process.Config'.+debug :: (RenderSeq s, MonadIO m) => Process.Config -> Debugger s -> Solver s m+debug cfg = processSolver cfg . Just --- | Creates an interactive session with a solver by creating and returning an alive process-handle 'P.Handle'.-interactiveSolver :: MonadIO m => ProcessSolver -> m (B.Solver, P.Handle)-interactiveSolver (ProcessSolver cfg) = liftIO $ do-  handle  <- P.new cfg-  liftM2 (,) (B.initSolver B.Queuing $ P.toBackend handle) (return handle)+-- | Creates an interactive session with a solver by creating and returning an alive process-handle 'Process.Handle'.+--   Queues commands by default, see 'Backend.Queuing'.+interactiveSolver :: MonadIO m => Process.Config -> m (Backend.Solver, Process.Handle)+interactiveSolver cfg = liftIO $ do+  handle  <- Process.new cfg+  liftM2 (,) (Backend.initSolver Backend.Queuing $ Process.toBackend handle) (return handle)  -- | A type holding actions for debugging states. data Debugger s = Debugger@@ -77,20 +75,20 @@ -- -- 5. close the process and clean up all resources. ---processSolver :: (RenderSeq s, MonadIO m) => P.Config -> Maybe (Debugger s) -> Solver s m+processSolver :: (RenderSeq s, MonadIO m) => Process.Config -> Maybe (Debugger s) -> Solver s m processSolver cfg debugger s = do-  liftIO $ P.with cfg $ \handle -> do+  liftIO $ Process.with cfg $ \handle -> do     maybe mempty (`debugState` s) debugger-    pSolver <- B.initSolver B.Queuing $ P.toBackend handle+    pSolver <- Backend.initSolver Backend.Queuing $ Process.toBackend handle      let problem = renderSeq s     maybe mempty (`debugProblem` problem) debugger -    forM_ problem (B.command_ pSolver)-    resultResponse <- B.command pSolver "(check-sat)"+    forM_ problem (Backend.command_ pSolver)+    resultResponse <- Backend.command pSolver "(check-sat)"     maybe mempty (`debugResultResponse` resultResponse) debugger -    modelResponse  <- B.command pSolver "(get-model)"+    modelResponse  <- Backend.command pSolver "(get-model)"     maybe mempty (`debugModelResponse` modelResponse) debugger      case parseOnly resultParser (toStrict resultResponse) of

@@ -1,14 +1,13 @@ module Language.Hasmtlib.Solver.MathSAT where -import Language.Hasmtlib.Solver.Common-import qualified SMTLIB.Backends.Process as P+import SMTLIB.Backends.Process --- | A 'ProcessSolver' for MathSAT.+-- | A 'Config' for MathSAT. --   Requires binary @mathsat@ to be in path.-mathsat :: ProcessSolver-mathsat = ProcessSolver $ P.defaultConfig { P.exe = "mathsat", P.args = [] }+mathsat :: Config+mathsat = defaultConfig { exe = "mathsat", args = [] } --- | A 'ProcessSolver' for OptiMathSAT.+-- | A 'Config' for OptiMathSAT. --   Requires binary @optimathsat@ to be in path.-optimathsat :: ProcessSolver-optimathsat = ProcessSolver $ P.defaultConfig { P.exe = "optimathsat", P.args = ["-optimization=true"] }+optimathsat :: Config+optimathsat = defaultConfig { exe = "optimathsat", args = ["-optimization=true"] }

@@ -1,9 +1,8 @@ module Language.Hasmtlib.Solver.OpenSMT where -import Language.Hasmtlib.Solver.Common-import qualified SMTLIB.Backends.Process as P+import SMTLIB.Backends.Process --- | A 'ProcessSolver' for OpenSMT.+-- | A 'Config' for OpenSMT. --   Requires binary @opensmt@ to be in path.-opensmt :: ProcessSolver-opensmt = ProcessSolver $ P.defaultConfig { P.exe = "opensmt", P.args = [] }+opensmt :: Config+opensmt = defaultConfig { exe = "opensmt", args = [] }

@@ -1,9 +1,8 @@ module Language.Hasmtlib.Solver.Yices where -import Language.Hasmtlib.Solver.Common-import qualified SMTLIB.Backends.Process as P+import SMTLIB.Backends.Process --- | A 'ProcessSolver' for Yices.+-- | A 'Config' for Yices. --   Requires binary @yices-smt2@ to be in path.-yices :: ProcessSolver-yices = ProcessSolver $ P.defaultConfig { P.exe = "yices-smt2", P.args = ["--smt2-model-format"] }+yices :: Config+yices = defaultConfig { exe = "yices-smt2", args = ["--smt2-model-format", "--incremental"] }

@@ -1,9 +1,8 @@ module Language.Hasmtlib.Solver.Z3 where -import Language.Hasmtlib.Solver.Common-import qualified SMTLIB.Backends.Process as P+import SMTLIB.Backends.Process --- | A 'ProcessSolver' for Z3.+-- | A 'Config' for Z3. --   Requires binary @z3@ to be in path.-z3 :: ProcessSolver-z3 = ProcessSolver P.defaultConfig+z3 :: Config+z3 = defaultConfig

@@ -4,22 +4,22 @@ module Language.Hasmtlib.Type.ArrayMap where  import Data.Proxy-import qualified Data.Map as Map  +import qualified Data.Map as Map import Control.Lens --- | Class that allows access to a map-like array where specific values are is the default value or overwritten values.+-- | Class that allows access to a map-like array where any value is either the default value or an overwritten values. --   Every index has a value by default. --   Values at indices can be overwritten manually.--- +-- --   Based on McCarthy`s basic array theory.--- +-- --   Therefore the following axioms must hold:--- +-- -- 1. forall A i x: arrSelect (store A i x) == x--- +-- -- 2. forall A i j x: i /= j ==> (arrSelect (arrStore A i x) j === arrSelect A j) class ArrayMap f k v where-  asConst'   :: Proxy f -> Proxy k -> v -> f k v +  asConst'   :: Proxy f -> Proxy k -> v -> f k v   viewConst  :: f k v -> v   arrSelect  :: f k v -> k -> v   arrStore   :: f k v -> k -> v -> f k v@@ -28,8 +28,8 @@ asConst :: forall f k v. ArrayMap f k v => v -> f k v asConst = asConst' (Proxy @f) (Proxy @k) --- | A map-like array with a default constant value and partially overwritten values.  -data ConstArray k v = ConstArray +-- | A map-like array with a default constant value and partially overwritten values.+data ConstArray k v = ConstArray   { _arrConst :: v   , _stored :: Map.Map k v   } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

@@ -1,5 +1,3 @@-{-# LANGUAGE FunctionalDependencies #-}- module Language.Hasmtlib.Type.MonadSMT where  import Language.Hasmtlib.Internal.Expr@@ -111,7 +109,7 @@ quantify expr = return expr  -- | A 'MonadSMT' that allows incremental solving.-class MonadSMT s m => MonadIncrSMT s m | m -> s where+class MonadSMT s m => MonadIncrSMT s m where   -- | Push a new context (one) to the solvers context-stack.   push :: m () 

@@ -34,7 +34,7 @@  -- | The state of the OMT-problem. data OMT = OMT-  { _smt            :: SMT                                  -- ^ The underlying 'SMT'-Problem+  { _smt            :: !SMT                                 -- ^ The underlying 'SMT'-Problem   , _targetMinimize :: !(Seq (SomeKnownSMTSort Minimize))   -- ^ All expressions to minimize   , _targetMaximize :: !(Seq (SomeKnownSMTSort Maximize))   -- ^ All expressions to maximize   , _softFormulas   :: !(Seq SoftFormula)                   -- ^ All soft assertions of boolean expressions

@@ -17,10 +17,12 @@ import Data.IntMap as IMap (singleton) import Data.Dependent.Map as DMap import Data.Coerce+import qualified Data.ByteString.Lazy.Char8 as ByteString.Char8 import Data.ByteString.Builder import Data.ByteString.Lazy hiding (filter, singleton, isPrefixOf) import Data.Attoparsec.ByteString hiding (Result) import Control.Monad.State+import Control.Monad import Control.Lens hiding (List)  -- | A pipe to the solver.@@ -31,6 +33,7 @@   { _lastPipeVarId :: {-# UNPACK #-} !Int              -- ^ Last Id assigned to a new var   , _mPipeLogic    :: Maybe String                     -- ^ Logic for the SMT-Solver   , _pipe          :: !B.Solver                        -- ^ Active pipe to the backend+  , _isDebugging   :: Bool                             -- ^ Flag if pipe shall debug   }  $(makeLenses ''Pipe)@@ -42,7 +45,9 @@   var' p = do     smt <- get     newVar <- smtvar' p-    liftIO $ B.command_ (smt^.pipe) $ renderDeclareVar newVar+    let cmd = renderDeclareVar newVar+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (smt^.pipe) cmd     return $ Var newVar   {-# INLINEABLE var' #-} @@ -51,32 +56,45 @@     qExpr <- case smt^.mPipeLogic of       Nothing    -> return expr       Just logic -> if "QF" `isPrefixOf` logic then return expr else quantify expr-    liftIO $ B.command_ (smt^.pipe) $ renderAssert qExpr+    let cmd = renderAssert qExpr+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (smt^.pipe) cmd   {-# INLINEABLE assert #-}    setOption opt = do     smt <- get-    liftIO $ B.command_ (smt^.pipe) $ render opt+    let cmd = render opt+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (smt^.pipe) cmd    setLogic l = do     mPipeLogic ?= l     smt <- get-    liftIO $ B.command_ (smt^.pipe) $ renderSetLogic (stringUtf8 l)+    let cmd = renderSetLogic (stringUtf8 l)+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (smt^.pipe) cmd  instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where   push = do     smt <- get-    liftIO $ B.command_ (smt^.pipe) "(push 1)"+    let cmd = "(push 1)"+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (smt^.pipe) cmd   {-# INLINE push #-}    pop = do     smt <- get-    liftIO $ B.command_ (smt^.pipe) "(pop 1)"+    let cmd = "(pop 1)"+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (smt^.pipe) cmd   {-# INLINE pop #-}    checkSat = do     smt <- get-    result <- liftIO $ B.command (smt^.pipe) "(check-sat)"+    let cmd = "(check-sat)"+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    result <- liftIO $ B.command (smt^.pipe) cmd+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn result     case parseOnly resultParser (toStrict result) of       Left e    -> liftIO $ do         print result@@ -85,7 +103,10 @@    getModel = do     smt   <- get-    model <- liftIO $ B.command (smt^.pipe) "(get-model)"+    let cmd = "(get-model)"+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    model <- liftIO $ B.command (smt^.pipe) cmd+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn model     case parseOnly anyModelParser (toStrict model) of       Left e    -> liftIO $ do         print model@@ -95,7 +116,10 @@   getValue :: forall t. KnownSMTSort t => Expr t -> m (Maybe (Decoded (Expr t)))   getValue v@(Var x) = do     smt   <- get-    model <- liftIO $ B.command (smt^.pipe) $ renderUnary "get-value" $ "(" <> render x <> ")"+    let cmd = renderUnary "get-value" $ "(" <> render x <> ")"+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    model <- liftIO $ B.command (smt^.pipe) cmd+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn model     case parseOnly (getValueParser @t x) (toStrict model) of       Left e    -> liftIO $ do         print model@@ -115,14 +139,21 @@ instance (MonadSMT Pipe m, MonadIO m) => MonadOMT Pipe m where   minimize expr = do     smt <- get-    liftIO $ B.command_ (smt^.pipe) $ render $ Minimize expr+    let cmd = render $ Minimize expr+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (smt^.pipe) cmd   {-# INLINEABLE minimize #-}    maximize expr = do     smt <- get-    liftIO $ B.command_ (smt^.pipe) $ render $ Maximize expr+    let cmd = render $ Maximize expr+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (smt^.pipe) cmd   {-# INLINEABLE maximize #-}    assertSoft expr w gid = do     smt <- get-    liftIO $ B.command_ (smt^.pipe) $ render $ SoftFormula expr w gid+    let cmd = render $ SoftFormula expr w gid+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (smt^.pipe) cmd+  {-# INLINEABLE assertSoft #-}

@@ -1,6 +1,7 @@ module Language.Hasmtlib.Type.Solver   ( WithSolver(..)-  , solveWith, interactiveWith+  , solveWith+  , interactiveWith, debugInteractiveWith   , solveMinimized, solveMinimizedDebug   , solveMaximized, solveMaximizedDebug   )@@ -13,14 +14,15 @@ import Language.Hasmtlib.Type.Pipe import Language.Hasmtlib.Orderable import Language.Hasmtlib.Codec-import qualified SMTLIB.Backends as B-import qualified SMTLIB.Backends.Process as P+import qualified SMTLIB.Backends as Backend+import qualified SMTLIB.Backends.Process as Process import Data.Default import Control.Monad.State --- | Data that can have a 'B.Solver'.+-- | Data that can have a 'Backend.Solver' which may be debugged. class WithSolver a where-  withSolver :: B.Solver -> a+  -- | Create a datum with a 'Backend.Solver' and a 'Bool for whether to debug the 'Backend.Solver'.+  withSolver :: Backend.Solver -> Bool -> a  instance WithSolver Pipe where   withSolver = Pipe 0 Nothing@@ -43,7 +45,7 @@ -- -- main :: IO () -- main = do---   res <- solveWith (solver cvc5) $ do+--   res <- solveWith @SMT (solver cvc5) $ do --     setLogic \"QF_LIA\" -- --     x <- var @IntSort@@ -54,7 +56,7 @@ -- --   print res -- @-solveWith :: (Monad m, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))+solveWith :: (Default s, Monad m, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a)) solveWith solver m = do   (a, problem) <- runStateT m def   (result, solution) <- solver problem@@ -72,7 +74,7 @@ -- main :: IO () -- main = do --   cvc5Living <- interactiveSolver cvc5---   interactiveWith cvc5Living $ do+--   interactiveWith @Pipe cvc5Living $ do --     setOption $ Incremental True --     setOption $ ProduceModels True --     setLogic \"QF_LIA\"@@ -100,10 +102,16 @@ -- --   return () -- @-interactiveWith :: (MonadIO m, WithSolver s) => (B.Solver, P.Handle) -> StateT s m () -> m ()+interactiveWith :: (WithSolver s, MonadIO m) => (Backend.Solver, Process.Handle) -> StateT s m () -> m () interactiveWith (solver, handle) m = do-   _ <- runStateT m $ withSolver solver-   liftIO $ P.close handle+  _ <- runStateT m $ withSolver solver False+  liftIO $ Process.close handle++-- | Like 'interactiveWith' but it prints all communication with the solver to console.+debugInteractiveWith :: (WithSolver s, MonadIO m) => (Backend.Solver, Process.Handle) -> StateT s m () -> m ()+debugInteractiveWith (solver, handle) m = do+  _ <- runStateT m $ withSolver solver True+  liftIO $ Process.close handle  -- | Solves the current problem with respect to a minimal solution for a given numerical expression. --