From 279e9c89ab7eba64269d14b0eb0488f58d2f9e01 Mon Sep 17 00:00:00 2001 From: bruderj15 Date: Sat, 7 Sep 2024 10:06:39 +0200 Subject: [PATCH 1/4] clean: added #100 --- src/Language/Hasmtlib/Solver/Bitwuzla.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/Language/Hasmtlib/Solver/Bitwuzla.hs b/src/Language/Hasmtlib/Solver/Bitwuzla.hs index a40c8f8..e7bbe20 100644 --- a/src/Language/Hasmtlib/Solver/Bitwuzla.hs +++ b/src/Language/Hasmtlib/Solver/Bitwuzla.hs @@ -9,3 +9,13 @@ import SMTLIB.Backends.Process -- 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"] } From 4d7afc8bc3857d87d77f05dd941ea2699a91c8f3 Mon Sep 17 00:00:00 2001 From: bruderj15 Date: Sat, 7 Sep 2024 10:07:13 +0200 Subject: [PATCH 2/4] clean: fix #97 --- src/Language/Hasmtlib/Internal/Sharing.hs | 2 +- src/Language/Hasmtlib/Type/Solver.hs | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Language/Hasmtlib/Internal/Sharing.hs b/src/Language/Hasmtlib/Internal/Sharing.hs index f9a7cca..edfe744 100644 --- a/src/Language/Hasmtlib/Internal/Sharing.hs +++ b/src/Language/Hasmtlib/Internal/Sharing.hs @@ -28,7 +28,7 @@ data SharingMode = deriving Show instance Default SharingMode where - def = StableNames + def = None -- | States that can share expressions by comparing their 'StableName's. class Sharing s where diff --git a/src/Language/Hasmtlib/Type/Solver.hs b/src/Language/Hasmtlib/Type/Solver.hs index 9ccd68f..278cfe4 100644 --- a/src/Language/Hasmtlib/Type/Solver.hs +++ b/src/Language/Hasmtlib/Type/Solver.hs @@ -20,7 +20,6 @@ module Language.Hasmtlib.Type.Solver ) where -import Language.Hasmtlib.Internal.Sharing import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.SMTSort @@ -38,7 +37,7 @@ class WithSolver a where 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: From 3ea8b20913d5139e15d89a95cd88e38ab48f2231 Mon Sep 17 00:00:00 2001 From: bruderj15 Date: Sat, 7 Sep 2024 16:45:07 +0200 Subject: [PATCH 3/4] clean: fix #99 --- .../Example/IncrementalOptimization.hs | 15 +-- src/Language/Hasmtlib/Type/MonadSMT.hs | 10 +- src/Language/Hasmtlib/Type/Solver.hs | 122 +++++++++++++----- 3 files changed, 102 insertions(+), 45 deletions(-) diff --git a/src/Language/Hasmtlib/Example/IncrementalOptimization.hs b/src/Language/Hasmtlib/Example/IncrementalOptimization.hs index 437b141..484629d 100644 --- a/src/Language/Hasmtlib/Example/IncrementalOptimization.hs +++ b/src/Language/Hasmtlib/Example/IncrementalOptimization.hs @@ -5,19 +5,16 @@ import Control.Monad.IO.Class main :: IO () main = do - iSolver <- interactiveSolver z3 - interactiveWith @Pipe iSolver $ do + iz3 <- interactiveSolver z3 + debugInteractiveWith @Pipe iz3 $ do setOption $ ProduceModels True setLogic "QF_LIA" x <- var @IntSort - assert $ x >? -2 - assertSoftWeighted (x >? -1) 5.0 + assert $ x ? 0 - minimize x - - (_, sol) <- solve + (res, sol) <- solveMaximized x (Just (+2)) Nothing + liftIO $ print res liftIO $ print $ decode sol x - - return () diff --git a/src/Language/Hasmtlib/Type/MonadSMT.hs b/src/Language/Hasmtlib/Type/MonadSMT.hs index c42d7eb..54e7dff 100644 --- a/src/Language/Hasmtlib/Type/MonadSMT.hs +++ b/src/Language/Hasmtlib/Type/MonadSMT.hs @@ -36,7 +36,6 @@ import Language.Hasmtlib.Type.Solution 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 @@ class MonadSMT s m => MonadIncrSMT s m where -- (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. -- diff --git a/src/Language/Hasmtlib/Type/Solver.hs b/src/Language/Hasmtlib/Type/Solver.hs index 278cfe4..6d100cf 100644 --- a/src/Language/Hasmtlib/Type/Solver.hs +++ b/src/Language/Hasmtlib/Type/Solver.hs @@ -13,10 +13,10 @@ module Language.Hasmtlib.Type.Solver , interactiveWith, debugInteractiveWith -- ** Minimzation - , solveMinimized, solveMinimizedDebug + , solveMinimized -- ** Maximization - , solveMaximized, solveMaximizedDebug + , solveMaximized ) where @@ -29,6 +29,7 @@ import Language.Hasmtlib.Codec 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. @@ -129,56 +130,111 @@ debugInteractiveWith (solver, handle) m = do -- | 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 ( (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) ( 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 From 5bae8cd8f67510d75f57859822f09a2d94f0dd49 Mon Sep 17 00:00:00 2001 From: bruderj15 Date: Sat, 7 Sep 2024 16:57:09 +0200 Subject: [PATCH 4/4] clean: bump version --- CHANGELOG.md | 14 ++++++++++++++ hasmtlib.cabal | 2 +- 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a6640a8..8edade4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,20 @@ file. 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 diff --git a/hasmtlib.cabal b/hasmtlib.cabal index b482a31..298ba71 100644 --- a/hasmtlib.cabal +++ b/hasmtlib.cabal @@ -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.