hasmtlib 2.6.2 → 2.6.3

raw patch · 6 files changed

+123/−40 lines, 6 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +14/−0
• hasmtlib.cabal +1/−1
• src/Language/Hasmtlib/Internal/Sharing.hs +1/−1
• src/Language/Hasmtlib/Solver/Bitwuzla.hs +10/−0
• src/Language/Hasmtlib/Type/MonadSMT.hs +7/−3
• src/Language/Hasmtlib/Type/Solver.hs +90/−35

@@ -6,6 +6,20 @@ 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.6.3 _(2024-09-07)_++### Added+- Added a solver configuration `bitwuzlaKissat` for `Bitwuzla` with underlying SAT-Solver `Kissat`.++### Changed+- Removed `solveMinimizedDebug` & `solveMaximizedDebug`. Use the modified `solveMinimized` & `solveMaximized` instead.+You can also provide a step-size now.+- Fixed a bug where `MonadOMT#solve` would run `get-model` although the solver did not necessarily respond with `Sat`.+- `SharingMode` for sharing common (sub-)expressions now defaults to `None`.+The previous default `StableNames` in general is only worth using, when your program can benefit a lot from sharing.+Otherwise it may drastically downgrade solver performance due to abundance of sharing-variables.+If you still want to use it, run `setSharingMode StableNames` within the problems monad.+ ## v2.6.2 _(2024-09-04)_  ### Changed

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               2.6.2+version:               2.6.3 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.

@@ -28,7 +28,7 @@   deriving Show  instance Default SharingMode where-  def = StableNames+  def = None  -- | States that can share expressions by comparing their 'StableName's. class Sharing s where

@@ -9,3 +9,13 @@ --   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 with Kissat as underlying sat-solver.+--+--   Requires binary @bitwuzla@ and to be in path.+--   Will use the @kissat@ shipped with @bitwuzla@.+--+--   It is recommended to build @bitwuzla@ from source for this to work as expected.+bitwuzlaKissat :: Config+bitwuzlaKissat = defaultConfig { exe = "bitwuzla", args = ["--sat-solver=kissat"] }

@@ -36,7 +36,6 @@ import Language.Hasmtlib.Codec import Data.Proxy import Control.Lens-import Control.Monad import Control.Monad.State  -- | A 'MonadState' that holds an SMT-Problem.@@ -235,12 +234,17 @@ -- (res, sol) <- solve -- case res of --   Sat -> do---     x' <- getValue x --     liftIO $ print $ decode sol x --   r -> print r -- @ solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution)-solve = liftM2 (,) checkSat getModel+solve = do+  res <- checkSat+  case res of+    Sat -> do+      sol <- getModel+      return (Sat, sol)+    r -> return (r, mempty)  -- | A 'MonadSMT' that addtionally allows optimization targets. --

@@ -13,14 +13,13 @@   , interactiveWith, debugInteractiveWith    -- ** Minimzation-  , solveMinimized, solveMinimizedDebug+  , solveMinimized    -- ** Maximization-  , solveMaximized, solveMaximizedDebug+  , solveMaximized   ) where -import Language.Hasmtlib.Internal.Sharing import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.SMTSort@@ -30,6 +29,7 @@ import qualified SMTLIB.Backends as Backend import qualified SMTLIB.Backends.Process as Process import Data.Default+import Data.Maybe import Control.Monad.State  -- | Data that can have a 'Backend.Solver' which may be debugged.@@ -38,7 +38,7 @@   withSolver :: Backend.Solver -> Bool -> a  instance WithSolver Pipe where-  withSolver = Pipe 0 Nothing StableNames mempty mempty+  withSolver = Pipe 0 Nothing def mempty mempty  -- | @'solveWith' solver prob@ solves a SMT problem @prob@ with the given -- @solver@. It returns a pair consisting of:@@ -130,56 +130,111 @@  -- | Solves the current problem with respect to a minimal solution for a given numerical expression. -----   Uses iterative refinement.+--   This is done by incrementally refining the upper bound for a given target.+--   Terminates, when setting the last intermediate result as new upper bound results in 'Unsat'.+--   Then removes that last assertion and returns the previous (now confirmed minimal) result. -----   If you want access to intermediate results, use 'solveMinimizedDebug' instead.+--   You can also provide a step-size. You do not have to worry about stepping over the optimal result.+--   This implementation takes care of it.+--+--   Access to intermediate results is also possible via an 'IO'-Action.+--+-- ==== __Examples__+--+-- @+-- x <- var \@IntSort+-- assert $ x >? 4+-- solveMinimized x Nothing Nothing+-- @+--+-- The solver will return @x := 5@.+--+-- The first 'Nothing' indicates that each intermediate result will be set as next upper bound.+-- The second 'Nothing' shows that we do not care about intermediate, but only the final (minimal) result.+--+-- @+-- x <- var \@IntSort+-- assert $ x >? 4+-- solveMinimized x (Just (\\r -> r-1)) (Just print)+-- @+--+-- The solver will still return @x := 5@.+--+-- However, here we want the next bound of each refinement to be @lastResult - 1@.+-- Also, every intermediate result is printed. solveMinimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))-  => Expr t-  -> m (Result, Solution)-solveMinimized = solveOptimized Nothing (<?)---- | Like 'solveMinimized' but with access to intermediate results.-solveMinimizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))-  => (Solution -> IO ())-  -> Expr t+  => Expr t                             -- ^ Target to minimize+  -> Maybe (Expr t -> Expr t)           -- ^ Step-size: Lambda is given last result as argument, producing the next upper bound+  -> Maybe (Solution -> IO ())          -- ^ Accessor to intermediate results   -> m (Result, Solution)-solveMinimizedDebug debug = solveOptimized (Just debug) (<?)+solveMinimized = solveOptimized (<?)  -- | Solves the current problem with respect to a maximal solution for a given numerical expression. -----   Uses iterative refinement.+--   This is done by incrementally refining the lower bound for a given target.+--   Terminates, when setting the last intermediate result as new lower bound results in 'Unsat'.+--   Then removes that last assertion and returns the previous (now confirmed maximal) result. -----   If you want access to intermediate results, use 'solveMaximizedDebug' instead.+--   You can also provide a step-size. You do not have to worry about stepping over the optimal result.+--   This implementation takes care of it.+--+--   Access to intermediate results is also possible via an 'IO'-Action.+--+-- ==== __Examples__+--+-- @+-- x <- var \@IntSort+-- assert $ x <? 4+-- solveMaximized x Nothing Nothing+-- @+--+-- The solver will return @x := 3@.+--+-- The first 'Nothing' indicates that each intermediate result will be set as next lower bound.+-- The second 'Nothing' shows that we do not care about intermediate, but only the final (maximal) result.+--+-- @+-- x <- var \@IntSort+-- assert $ x <? 4+-- solveMinimized x (Just (+1)) (Just print)+-- @+--+-- The solver will still return @x := 3@.+--+-- However, here we want the next bound of each refinement to be @lastResult + 1@.+-- Also, every intermediate result is printed. solveMaximized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))-  => Expr t-  -> m (Result, Solution)-solveMaximized = solveOptimized Nothing (>?)---- | Like 'solveMaximized' but with access to intermediate results.-solveMaximizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))-  => (Solution -> IO ())-  -> Expr t+  => Expr t                             -- ^ Target to maximize+  -> Maybe (Expr t -> Expr t)           -- ^ Step-size: Lambda is given last result as argument, producing the next lower bound+  -> Maybe (Solution -> IO ())          -- ^ Accessor to intermediate results   -> m (Result, Solution)-solveMaximizedDebug debug = solveOptimized (Just debug) (>?)+solveMaximized = solveOptimized (>?)  solveOptimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t)-  => Maybe (Solution -> IO ())-  -> (Expr t -> Expr t -> Expr BoolSort)+  => (Expr t -> Expr t -> Expr BoolSort)   -> Expr t+  -> Maybe (Expr t -> Expr t)+  -> Maybe (Solution -> IO ())   -> m (Result, Solution)-solveOptimized mDebug op = go Unknown mempty+solveOptimized op goal mStep mDebug = refine Unknown mempty goal   where-    go oldRes oldSol target = do-      push-      (res, sol) <- solve+    refine oldRes oldSol target = do+      res <- checkSat       case res of         Sat   -> do+          sol <- getModel           case decode sol target of             Nothing        -> return (Sat, mempty)             Just targetSol -> do               case mDebug of                 Nothing    -> pure ()                 Just debug -> liftIO $ debug sol-              assert $ target `op` encode targetSol-              go res sol target-        _ -> pop >> return (oldRes, oldSol)+              push+              let step = fromMaybe id mStep+              assert $ target `op` step (encode targetSol)+              refine res sol target+        _ -> do+          pop+          case mStep of+            Nothing -> return (oldRes, oldSol)+            Just _  -> solveOptimized op goal Nothing mDebug -- make sure the very last step did not skip the optimal result