hasmtlib 2.0.0 → 2.0.1

raw patch · 5 files changed

+26/−15 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +9/−0
• hasmtlib.cabal +1/−1
• src/Language/Hasmtlib/Boolean.hs +7/−5
• src/Language/Hasmtlib/Solver/Common.hs +6/−6
• src/Language/Hasmtlib/Type/OMT.hs +3/−3

@@ -6,6 +6,15 @@ 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.0.1 _(2024-07-23)_++### Added+- Added more documentation++### Changed+- `(<==>)` now has `infixr 4`+- `(<==)` now has `infixl 0`+ ## v2.0.0 _(2024-07-23)_  ### Added

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

@@ -12,15 +12,15 @@ import GHC.TypeNats  class Boolean b where-  -- | Lift a 'Bool'+  -- | Lift a 'Bool'.   bool :: Bool -> b -  -- | The true constant+  -- | The true constant.   -- @'true' = 'bool' 'True'@   true :: b   true = bool True -  -- | The false constant+  -- | The false constant.   -- @'false' = 'bool' 'False'@   false :: b   false = bool False@@ -47,16 +47,18 @@   (<==>) :: b -> b -> b   x <==> y = (x ==> y) && (y ==> x) -  -- | Logical negation+  -- | Logical negation.   not :: b -> b -  -- | Exclusive-or+  -- | Exclusive-or.   xor :: b -> b -> b    infix 4 `xor`+  infixr 4 <==>   infixr 3 &&   infixr 2 ||   infixr 0 ==>+  infixl 0 <==  -- | The logical conjunction of several values. and :: (Foldable t, Boolean b) => t b -> b

@@ -20,11 +20,11 @@ -- | A newtype-wrapper for 'P.Config' which configures a solver via external process. newtype ProcessSolver = ProcessSolver { conf :: P.Config } --- | Creates a 'Solver' from a 'ProcessSolver'+-- | Creates a 'Solver' from a 'ProcessSolver'. solver :: (RenderSeq s, MonadIO m) => ProcessSolver -> Solver s m solver (ProcessSolver cfg) = processSolver cfg Nothing --- | Creates a debugging 'Solver' from a 'ProcessSolver'+-- | 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 @@ -36,10 +36,10 @@  -- | A type holding actions for debugging states. data Debugger s = Debugger-  { debugState          :: s -> IO ()-  , debugProblem        :: Seq Builder -> IO ()-  , debugResultResponse :: ByteString -> IO ()-  , debugModelResponse  :: ByteString -> IO ()+  { debugState          :: s -> IO ()               -- ^ Debug the entire state+  , debugProblem        :: Seq Builder -> IO ()     -- ^ Debug the linewise-rendered problem+  , debugResultResponse :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(check-sat)@+  , debugModelResponse  :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(get-model)@   }  instance Default (Debugger SMT) where

@@ -20,9 +20,9 @@  -- | An assertion of a booolean expression in OMT that may be weighted. data SoftFormula = SoftFormula-  { _formula  :: Expr BoolSort-  , _mWeight  :: Maybe Double-  , _mGroupId :: Maybe String+  { _formula  :: Expr BoolSort    -- ^ The underlying soft formula+  , _mWeight  :: Maybe Double     -- ^ Weight of the soft formula+  , _mGroupId :: Maybe String     -- ^ Group-Id of the soft formula   } deriving Show $(makeLenses ''SoftFormula)