From 5e97c2ef9b8eb5b72f6a35ec724ebda18647e3e2 Mon Sep 17 00:00:00 2001 From: bruderj15 Date: Mon, 26 Aug 2024 13:37:41 +0200 Subject: [PATCH 1/3] 81-eq-sharing: Added SharingMode, defaults to StableNames --- src/Language/Hasmtlib.hs | 2 + src/Language/Hasmtlib/Example/Sharing.hs | 27 ++++++ src/Language/Hasmtlib/Internal/Sharing.hs | 19 +++- src/Language/Hasmtlib/Type/OMT.hs | 12 ++- src/Language/Hasmtlib/Type/Pipe.hs | 100 +++++++++++----------- src/Language/Hasmtlib/Type/SMT.hs | 6 +- src/Language/Hasmtlib/Type/Solver.hs | 3 +- 7 files changed, 111 insertions(+), 58 deletions(-) create mode 100644 src/Language/Hasmtlib/Example/Sharing.hs diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs index 2ea73f9..c3219c3 100644 --- a/src/Language/Hasmtlib.hs +++ b/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 diff --git a/src/Language/Hasmtlib/Example/Sharing.hs b/src/Language/Hasmtlib/Example/Sharing.hs new file mode 100644 index 0000000..f4b58aa --- /dev/null +++ b/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 diff --git a/src/Language/Hasmtlib/Internal/Sharing.hs b/src/Language/Hasmtlib/Internal/Sharing.hs index df8d365..a870504 100644 --- a/src/Language/Hasmtlib/Internal/Sharing.hs +++ b/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 diff --git a/src/Language/Hasmtlib/Type/OMT.hs b/src/Language/Hasmtlib/Type/OMT.hs index 744e5dd..1c05958 100644 --- a/src/Language/Hasmtlib/Type/OMT.hs +++ b/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 diff --git a/src/Language/Hasmtlib/Type/Pipe.hs b/src/Language/Hasmtlib/Type/Pipe.hs index 6658274..75822a3 100644 --- a/src/Language/Hasmtlib/Type/Pipe.hs +++ b/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,71 +49,72 @@ 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 @@ -120,11 +122,11 @@ instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where 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 #-} diff --git a/src/Language/Hasmtlib/Type/SMT.hs b/src/Language/Hasmtlib/Type/SMT.hs index 7ca7f1f..a836867 100644 --- a/src/Language/Hasmtlib/Type/SMT.hs +++ b/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 diff --git a/src/Language/Hasmtlib/Type/Solver.hs b/src/Language/Hasmtlib/Type/Solver.hs index 6325e42..990dc24 100644 --- a/src/Language/Hasmtlib/Type/Solver.hs +++ b/src/Language/Hasmtlib/Type/Solver.hs @@ -7,6 +7,7 @@ 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 @@ -24,7 +25,7 @@ class WithSolver a where 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: From a1e363856051231aa39056817bc30e25244097c8 Mon Sep 17 00:00:00 2001 From: bruderj15 Date: Mon, 26 Aug 2024 13:50:38 +0200 Subject: [PATCH 2/3] 81-eq-sharing: docu fix --- src/Language/Hasmtlib/Type/Expr.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs index 375a171..6bd830b 100644 --- a/src/Language/Hasmtlib/Type/Expr.hs +++ b/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 From 59bfbec4f47db5e89e9ba4943528e3cfc21b0014 Mon Sep 17 00:00:00 2001 From: bruderj15 Date: Mon, 26 Aug 2024 13:57:56 +0200 Subject: [PATCH 3/3] 81-eq-sharing: bump version --- CHANGELOG.md | 9 +++++++++ hasmtlib.cabal | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ffd36ef..88f94fd 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/hasmtlib.cabal b/hasmtlib.cabal index fc2e11e..ebe486f 100644 --- a/hasmtlib.cabal +++ b/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.