Merge pull request #86 from bruderj15/develop

Publish v2.5.1

CHANGELOG.md

@@ -6,6 +6,15 @@ 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.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

hasmtlib.cabal

@@ -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.

src/Language/Hasmtlib.hs

@@ -22,6 +22,7 @@ module Language.Hasmtlib
   , 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.Z3
 import Language.Hasmtlib.Solver.Yices
 import Language.Hasmtlib.Solver.OpenSMT
 import Language.Hasmtlib.Solver.MathSAT
+import Language.Hasmtlib.Internal.Sharing

src/Language/Hasmtlib/Example/Sharing.hs

@@ -0,0 +1,27 @@
+module Language.Hasmtlib.Example.Arith where
+
+import Prelude hiding ((&&))
+import Language.Hasmtlib
+import Data.Default
+
+main :: IO ()
+main = do
+  res <- solveWith @SMT (debug cvc5 def) $ do
+    setLogic "QF_LIA"
+
+    x <- var @IntSort
+
+    let a1 = x + x
+        a2 = a1 + a1
+
+    assert $ a2 === a2
+
+    setSharingMode None
+    assert $ a2 === a2
+
+    setSharingMode StableNames
+    assert $ a2 === a2
+
+    return x
+
+  print res

src/Language/Hasmtlib/Internal/Sharing.hs

@@ -2,6 +2,7 @@
 
 module Language.Hasmtlib.Internal.Sharing
   ( Sharing(..)
+  , SharingMode(..)
   , runSharing, share
   )
 where
@@ -12,6 +13,7 @@ import Language.Hasmtlib.Type.SMTSort
 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 Unsafe.Coerce
 
 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 @@ class Sharing s where
   --   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

src/Language/Hasmtlib/Type/Expr.hs

@@ -715,7 +715,7 @@ instance Real (Expr IntSort) where
   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 @@ instance Real (Expr RealSort) where
   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 @@ instance KnownNat n => Real (Expr (BvSort n)) where
   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

src/Language/Hasmtlib/Type/OMT.hs

@@ -49,6 +49,7 @@ instance Sharing OMT where
   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 @@ instance MonadState OMT m => MonadSMT OMT m where
 
   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 MonadState OMT m => MonadSMT OMT m where
 
 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

src/Language/Hasmtlib/Type/Pipe.hs

@@ -37,9 +37,10 @@ import System.Mem.StableName
 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,83 +49,84 @@ instance Sharing Pipe where
   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
         error e
       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 @@ instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where
 
   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 (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where
 
 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 #-}

src/Language/Hasmtlib/Type/SMT.hs

@@ -27,17 +27,19 @@ data SMT = SMT
   , _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 @@ instance MonadState SMT m => MonadSMT SMT m where
 
   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