hasmtlib 2.5.0 → 2.5.1

raw patch · 9 files changed

+97/−62 lines, 9 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +9/−0
• hasmtlib.cabal +1/−1
• src/Language/Hasmtlib.hs +2/−0
• src/Language/Hasmtlib/Internal/Sharing.hs +17/−2
• src/Language/Hasmtlib/Type/Expr.hs +3/−3
• src/Language/Hasmtlib/Type/OMT.hs +8/−4
• src/Language/Hasmtlib/Type/Pipe.hs +51/−49
• src/Language/Hasmtlib/Type/SMT.hs +4/−2
• src/Language/Hasmtlib/Type/Solver.hs +2/−1

@@ -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.5.1 _(2024-08-26)_++### Added+- Added `SharingMode = None | StableNames` in `Language.Hasmtlib.Internal.Sharing`. Defaults to `StableNames`.+- Added function `setSharingMode` which allows you to change the `SharingMode`.++### Changed+- `runSharing` in `Language.Hasmtlib.Internal.Sharing` now differentiates sharing behavior based on newly given argument of type `SharingMode`+ ## v2.5.0 _(2024-08-25)_  ### Added

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

@@ -22,6 +22,7 @@   , module Language.Hasmtlib.Solver.Yices   , module Language.Hasmtlib.Solver.OpenSMT   , module Language.Hasmtlib.Solver.MathSAT+  , SharingMode(..), setSharingMode   )   where @@ -47,3 +48,4 @@ import Language.Hasmtlib.Solver.Yices import Language.Hasmtlib.Solver.OpenSMT import Language.Hasmtlib.Solver.MathSAT+import Language.Hasmtlib.Internal.Sharing

@@ -2,6 +2,7 @@  module Language.Hasmtlib.Internal.Sharing   ( Sharing(..)+  , SharingMode(..)   , runSharing, share   ) where@@ -12,6 +13,7 @@ import Language.Hasmtlib.Type.Expr import Data.GADT.Compare import Data.HashMap.Lazy+import Data.Default import Control.Monad.State import Control.Lens import System.Mem.StableName@@ -20,6 +22,15 @@  import Data.Kind +-- | Mode used for sharing.+data SharingMode =+    None            -- ^ Common expressions are not shared at all+  | StableNames     -- ^ Expressions that resolve to the same 'StableName' are shared+  deriving Show++instance Default SharingMode where+  def = StableNames+ -- | States that can share expressions by comparing their 'StableName's. class Sharing s where   -- | A constraint on the monad used when asserting the shared node in 'assertSharedNode'.@@ -32,12 +43,16 @@   --   Also gives access to the 'StableName' of the original expression.   assertSharedNode :: (MonadState s m, SharingMonad s m) => StableName () -> Expr BoolSort -> m () +  -- | Sets the mode used for sharing common expressions. Defaults to 'StableNames'.+  setSharingMode :: MonadState s m => SharingMode -> m ()+ -- | Shares all possible sub-expressions in given expression. --   Replaces each node in the expression-tree with an auxiliary variable. --   All nodes @x@ @y@ where @makeStableName x == makeStableName y@ are replaced with the same auxiliary variable. --   Therefore this creates a DAG.-runSharing :: (KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) => Expr t -> m (Expr t)-runSharing = lazyParaM1 (+runSharing :: (KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) => SharingMode -> Expr t -> m (Expr t)+runSharing None = return+runSharing StableNames = lazyParaM1 (     \origExpr expr ->       if isLeaf origExpr       then return origExpr

@@ -715,7 +715,7 @@   toRational x = error $ "Real#toRational[Expr IntSort] only supported for constants. But given: " <> show x   {-# INLINE toRational #-} --- | This instance is __partial__ for 'toEnum', it's only intended for use with constants ('Constant').+-- | This instance is __partial__ for 'fromEnum', it's only intended for use with constants ('Constant'). instance Enum (Expr IntSort) where   fromEnum (Constant (IntValue x)) = fromIntegral x   fromEnum x = error $ "Enum#fromEnum[Expr IntSort] only supported for constants. But given: " <> show x@@ -747,7 +747,7 @@   toRational x = error $ "Real#toRational[Expr RealSort] only supported for constants. But given: " <> show x   {-# INLINE toRational #-} --- | This instance is __partial__ for 'toEnum', it's only intended for use with constants ('Constant').+-- | This instance is __partial__ for 'fromEnum', it's only intended for use with constants ('Constant'). instance Enum (Expr RealSort) where   fromEnum (Constant (RealValue x)) = fromEnum x   fromEnum x = error $ "Enum#fromEnum[Expr RealSort] only supported for constants. But given: " <> show x@@ -761,7 +761,7 @@   toRational x = error $ "Real#toRational[Expr BvSort] only supported for constants. But given: " <> show x   {-# INLINE toRational #-} --- | This instance is __partial__ for 'toEnum', it's only intended for use with constants ('Constant').+-- | This instance is __partial__ for 'fromEnum', it's only intended for use with constants ('Constant'). instance KnownNat n => Enum (Expr (BvSort n)) where   fromEnum (Constant (BvValue x)) = fromIntegral x   fromEnum x = error $ "Enum#fromEnum[Expr BvSort] only supported for constants. But given: " <> show x

@@ -49,6 +49,7 @@   type SharingMonad OMT = Monad   stableMap = smt.Language.Hasmtlib.Type.SMT.stableMap   assertSharedNode _ expr = modifying (smt.formulas) (|> expr)+  setSharingMode sm = smt.sharingMode .= sm  instance MonadState OMT m => MonadSMT OMT m where   smtvar' _ = fmap coerce $ (smt.lastVarId) <+= 1@@ -62,7 +63,7 @@    assert expr = do     omt <- get-    sExpr <- runSharing expr+    sExpr <- runSharing (omt^.smt.sharingMode) expr     qExpr <- case omt^.smt.mlogic of       Nothing    -> return sExpr       Just logic -> if "QF" `isPrefixOf` logic then return sExpr else quantify sExpr@@ -78,13 +79,16 @@  instance MonadSMT OMT m => MonadOMT OMT m where   minimize expr = do-    sExpr <- runSharing expr+    sm <- use (smt.sharingMode)+    sExpr <- runSharing sm expr     modifying targetMinimize (|> SomeSMTSort (Minimize sExpr))   maximize expr = do-    sExpr <- runSharing expr+    sm <- use (smt.sharingMode)+    sExpr <- runSharing sm expr     modifying targetMaximize (|> SomeSMTSort (Maximize sExpr))   assertSoft expr w gid = do-    sExpr <- runSharing expr+    sm <- use (smt.sharingMode)+    sExpr <- runSharing sm expr     modifying softFormulas (|> SoftFormula sExpr w gid)  instance Render SoftFormula where

@@ -37,9 +37,10 @@ data Pipe = Pipe   { _lastPipeVarId     :: {-# UNPACK #-} !Int                                 -- ^ Last Id assigned to a new var   , _mPipeLogic        :: Maybe String                                        -- ^ Logic for the SMT-Solver+  , _pipeSharingMode   :: !SharingMode                                         -- ^ How to share common expressions   , _pipeStableMap     :: !(HashMap (StableName ()) (SomeKnownSMTSort Expr))  -- ^ Mapping between a 'StableName' and it's 'Expr' we may share   , _incrSharedAuxs    :: !(Seq (Seq (StableName ())))                        -- ^ Index of each 'Seq' ('StableName' ()) is incremental stack height where 'StableName' representing auxiliary var that has been shared-  , _pipe              :: !B.Solver                                           -- ^ Active pipe to the backend+  , _pipeSolver        :: !B.Solver                                           -- ^ Active pipe to the backend   , _isDebugging       :: !Bool                                               -- ^ Flag if pipe shall debug   } $(makeLenses ''Pipe)@@ -48,71 +49,72 @@   type SharingMonad Pipe = MonadIO   stableMap = pipeStableMap   assertSharedNode sn expr = do-    smt <- get+    pipe <- get     modifying (incrSharedAuxs._last) (|> sn)     let cmd = renderAssert expr-    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd-    liftIO $ B.command_ (smt^.pipe) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (pipe^.pipeSolver) cmd+  setSharingMode sm = pipeSharingMode .= sm  instance (MonadState Pipe m, MonadIO m) => MonadSMT Pipe m where   smtvar' _ = fmap coerce $ lastPipeVarId <+= 1   {-# INLINE smtvar' #-}    var' p = do-    smt <- get+    pipe <- get     newVar <- smtvar' p     let cmd = renderDeclareVar newVar-    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd-    liftIO $ B.command_ (smt^.pipe) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (pipe^.pipeSolver) cmd     return $ Var newVar   {-# INLINEABLE var' #-}    assert expr = do-    smt <- get-    sExpr <- runSharing expr-    qExpr <- case smt^.mPipeLogic of+    pipe <- get+    sExpr <- runSharing (pipe^.pipeSharingMode) expr+    qExpr <- case pipe^.mPipeLogic of       Nothing    -> return sExpr       Just logic -> if "QF" `isPrefixOf` logic then return sExpr else quantify sExpr     let cmd = renderAssert qExpr-    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd-    liftIO $ B.command_ (smt^.pipe) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (pipe^.pipeSolver) cmd   {-# INLINEABLE assert #-}    setOption opt = do-    smt <- get+    pipe <- get     let cmd = render opt-    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd-    liftIO $ B.command_ (smt^.pipe) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (pipe^.pipeSolver) cmd    setLogic l = do     mPipeLogic ?= l-    smt <- get+    pipe <- get     let cmd = renderSetLogic (stringUtf8 l)-    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd-    liftIO $ B.command_ (smt^.pipe) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (pipe^.pipeSolver) cmd  instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where   push = do-    smt <- get+    pipe <- get     let cmd = "(push 1)"-    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd-    liftIO $ B.command_ (smt^.pipe) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (pipe^.pipeSolver) cmd     incrSharedAuxs <>= mempty    pop = do-    smt <- get+    pipe <- get     let cmd = "(pop 1)"-    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd-    liftIO $ B.command_ (smt^.pipe) cmd-    forMOf_ (incrSharedAuxs._last.folded) smt (\sn -> pipeStableMap.at sn .= Nothing)+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (pipe^.pipeSolver) cmd+    forMOf_ (incrSharedAuxs._last.folded) pipe (\sn -> pipeStableMap.at sn .= Nothing)     modifying incrSharedAuxs $ \case (auxs:>_) -> auxs ; auxs -> auxs    checkSat = do-    smt <- get+    pipe <- get     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+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    result <- liftIO $ B.command (pipe^.pipeSolver) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn result     case parseOnly resultParser (toStrict result) of       Left e    -> liftIO $ do         print result@@ -120,11 +122,11 @@       Right res -> return res    getModel = do-    smt   <- get+    pipe   <- get     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+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    model <- liftIO $ B.command (pipe^.pipeSolver) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn model     case parseOnly anyModelParser (toStrict model) of       Left e    -> liftIO $ do         print model@@ -133,11 +135,11 @@    getValue :: forall t. KnownSMTSort t => Expr t -> m (Maybe (Decoded (Expr t)))   getValue v@(Var x) = do-    smt   <- get+    pipe   <- get     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+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    model <- liftIO $ B.command (pipe^.pipeSolver) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn model     case parseOnly (getValueParser @t x) (toStrict model) of       Left e    -> liftIO $ do         print model@@ -155,25 +157,25 @@  instance (MonadSMT Pipe m, MonadIO m) => MonadOMT Pipe m where   minimize expr = do-    smt <- get-    sExpr <- runSharing expr+    pipe <- get+    sExpr <- runSharing (pipe^.pipeSharingMode) expr     let cmd = render $ Minimize sExpr-    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd-    liftIO $ B.command_ (smt^.pipe) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (pipe^.pipeSolver) cmd   {-# INLINEABLE minimize #-}    maximize expr = do-    smt <- get-    sExpr <- runSharing expr+    pipe <- get+    sExpr <- runSharing (pipe^.pipeSharingMode) expr     let cmd = render $ Maximize sExpr-    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd-    liftIO $ B.command_ (smt^.pipe) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (pipe^.pipeSolver) cmd   {-# INLINEABLE maximize #-}    assertSoft expr w gid = do-    smt <- get-    sExpr <- runSharing expr+    pipe <- get+    sExpr <- runSharing (pipe^.pipeSharingMode) expr     let cmd = render $ SoftFormula sExpr w gid-    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd-    liftIO $ B.command_ (smt^.pipe) cmd+    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (pipe^.pipeSolver) cmd   {-# INLINEABLE assertSoft #-}

@@ -27,17 +27,19 @@   , _formulas  :: !(Seq (Expr BoolSort))                              -- ^ All asserted formulas   , _mlogic    :: Maybe String                                        -- ^ Logic for the SMT-Solver   , _options   :: [SMTOption]                                         -- ^ All manually configured SMT-Solver-Options+  , _sharingMode :: !SharingMode                                       -- ^ How to share common expressions   , _stableMap :: !(HashMap (StableName ()) (SomeKnownSMTSort Expr))  -- ^ Mapping between a 'StableName' and it's 'Expr' we may share   } $(makeLenses ''SMT)  instance Default SMT where-  def = SMT 0 mempty mempty mempty [ProduceModels True] mempty+  def = SMT 0 mempty mempty mempty [ProduceModels True] def mempty  instance Sharing SMT where   type SharingMonad SMT = Monad   stableMap = Language.Hasmtlib.Type.SMT.stableMap   assertSharedNode _ expr = modifying formulas (|> expr)+  setSharingMode sm = sharingMode .= sm  instance MonadState SMT m => MonadSMT SMT m where   smtvar' _ = fmap coerce $ lastVarId <+= 1@@ -51,7 +53,7 @@    assert expr = do     smt <- get-    sExpr <- runSharing expr+    sExpr <- runSharing (smt^.sharingMode) expr     qExpr <- case smt^.mlogic of       Nothing    -> return sExpr       Just logic -> if "QF" `isPrefixOf` logic then return sExpr else quantify sExpr

@@ -7,6 +7,7 @@   ) where +import Language.Hasmtlib.Internal.Sharing import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.SMTSort@@ -24,7 +25,7 @@   withSolver :: Backend.Solver -> Bool -> a  instance WithSolver Pipe where-  withSolver = Pipe 0 Nothing mempty mempty+  withSolver = Pipe 0 Nothing StableNames mempty mempty  -- | @'solveWith' solver prob@ solves a SMT problem @prob@ with the given -- @solver@. It returns a pair consisting of: