hasmtlib 2.7.1 → 2.7.2

raw patch · 12 files changed

+50/−53 lines, 12 filesdep +constrained-somePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: constrained-some

API changes (from Hackage documentation)

Files

• CHANGELOG.md +11/−0
• hasmtlib.cabal +2/−2
• src/Language/Hasmtlib/Internal/Constraint.hs +0/−14
• src/Language/Hasmtlib/Internal/Parser.hs +11/−10
• src/Language/Hasmtlib/Internal/Render.hs +4/−3
• src/Language/Hasmtlib/Internal/Sharing.hs +3/−2
• src/Language/Hasmtlib/Internal/Uniplate1.hs +1/−1
• src/Language/Hasmtlib/Type/Debugger.hs +7/−6
• src/Language/Hasmtlib/Type/OMT.hs +4/−3
• src/Language/Hasmtlib/Type/SMT.hs +2/−1
• src/Language/Hasmtlib/Type/SMTSort.hs +2/−9
• src/Language/Hasmtlib/Type/Solution.hs +3/−2

@@ -6,6 +6,17 @@ 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.7.2 _(2024-11-27)_++### Added+- Added dependency `constrained-some`++### Changed+- Replaced internal usages of custom existential `SomeSMTSort` with `Some1` from `constrained-some`++### Removed+- Removed module `Language.Hasmtlib.Internal.Constraint`+ ## v2.7.1 _(2024-10-05)_  ### Changed

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               2.7.1+version:               2.7.2 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.@@ -36,7 +36,6 @@                      , Language.Hasmtlib.Internal.Render                      , Language.Hasmtlib.Internal.Sharing                      , Language.Hasmtlib.Internal.Uniplate1-                     , Language.Hasmtlib.Internal.Constraint                      , Language.Hasmtlib.Solver.Bitwuzla                      , Language.Hasmtlib.Solver.CVC5                      , Language.Hasmtlib.Solver.MathSAT@@ -78,6 +77,7 @@                      , bitvec                       >= 1.1.5  && < 2                      , finite-typelits              >= 0.1.0  && < 1                      , vector-sized                 >= 1      && < 2+                     , constrained-some             >= 0.1    && < 0.2    ghc-options:       -O2                      -Wall

@@ -1,14 +0,0 @@-module Language.Hasmtlib.Internal.Constraint where--import Data.Kind---- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k------ @--- AllC '[]       k = ()--- AllC (c ': cs) k = (c k, AllC cs k)--- @-type AllC :: [k -> Constraint] -> k -> Constraint-type family AllC cs k :: Constraint where-  AllC '[]       k = ()-  AllC (c ': cs) k = (c k, AllC cs k)

@@ -13,6 +13,7 @@ import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Type.ArrayMap import Language.Hasmtlib.Type.Expr+import Data.Some.Constraint import Data.Bit import Data.Coerce import Data.Proxy@@ -66,23 +67,23 @@   _     <- string "var_"   vId   <- decimal @Int   _     <- skipSpace >> string "()" >> skipSpace-  (SomeSMTSort someSort) <- parseSomeSort+  (Some1 someSort) <- parseSomeSort   _     <- skipSpace   expr  <- parseExpr' someSort   _     <- skipSpace >> char ')'   case decode mempty expr of     Nothing    -> fail $ "Solver reponded with solution for var_" ++ show vId ++ " but it contains "                       ++ "another var. This cannot be parsed and evaluated currently."-    Just value -> return $ SomeSMTSort $ SMTVarSol (coerce vId) (wrapValue value)+    Just value -> return $ Some1 $ SMTVarSol (coerce vId) (wrapValue value) {-# INLINEABLE parseSomeSol #-}  parseSomeSort :: Parser (SomeKnownOrdSMTSort SSMTSort)-parseSomeSort = (string "Bool" *> pure (SomeSMTSort SBoolSort))-        <|> (string "Int"  *> pure (SomeSMTSort SIntSort))-        <|> (string "Real" *> pure (SomeSMTSort SRealSort))+parseSomeSort = (string "Bool" *> pure (Some1 SBoolSort))+        <|> (string "Int"  *> pure (Some1 SIntSort))+        <|> (string "Real" *> pure (Some1 SRealSort))         <|> parseSomeBitVecSort         <|> parseSomeArraySort-        <|> (string "String" *> pure (SomeSMTSort SStringSort))+        <|> (string "String" *> pure (Some1 SStringSort)) {-# INLINEABLE parseSomeSort #-}  parseSomeBitVecSort :: Parser (SomeKnownOrdSMTSort SSMTSort)@@ -95,18 +96,18 @@     -- SMTLib does not differentiate between signed and unsigned BitVec on the type-level     -- We do. So we always just put Unsigned here and in Codec (Expr t)     -- if (t ~ BvSort Signed _) we retrieve unsigned solution and flip type-level encoding-    SomeNat pn -> return $ SomeSMTSort $ SBvSort (Proxy @Unsigned) pn+    SomeNat pn -> return $ Some1 $ SBvSort (Proxy @Unsigned) pn {-# INLINEABLE parseSomeBitVecSort #-}  parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort) parseSomeArraySort = do   _ <- char '(' >> skipSpace   _ <- string "Array" >> skipSpace-  (SomeSMTSort keySort)   <- parseSomeSort+  (Some1 keySort)   <- parseSomeSort   _ <- skipSpace-  (SomeSMTSort valueSort) <- parseSomeSort+  (Some1 valueSort) <- parseSomeSort   _ <- skipSpace >> char ')'-  return $ SomeSMTSort $ SArraySort (goProxy keySort) (goProxy valueSort)+  return $ Some1 $ SArraySort (goProxy keySort) (goProxy valueSort)     where       goProxy :: forall t. SSMTSort t -> Proxy t       goProxy _ = Proxy @t

@@ -11,6 +11,7 @@ import Language.Hasmtlib.Type.Bitvec import Language.Hasmtlib.Type.ArrayMap import Data.Coerce+import Data.Some.Constraint import Data.Sequence import Data.Foldable (foldl') import Data.Map (size, minViewWithKey)@@ -292,7 +293,7 @@ instance RenderProblem SMT where   renderOptions = fromList . fmap render . view options   renderLogic = maybe mempty (renderSetLogic . stringUtf8) . view mlogic-  renderDeclareVars = fmap (\(SomeSMTSort v) -> renderDeclareVar v) . view vars+  renderDeclareVars = fmap (\(Some1 v) -> renderDeclareVar v) . view vars   renderAssertions = fmap renderAssert . view formulas   renderSoftAssertions _ = mempty   renderMinimizations _ = mempty@@ -304,5 +305,5 @@   renderDeclareVars = renderDeclareVars . view smt   renderAssertions = renderAssertions . view smt   renderSoftAssertions = fmap render . view softFormulas-  renderMinimizations = fmap (\case SomeSMTSort minExpr -> render minExpr) . view targetMinimize-  renderMaximizations = fmap (\case SomeSMTSort maxExpr -> render maxExpr) . view targetMaximize+  renderMinimizations = fmap (\case Some1 minExpr -> render minExpr) . view targetMinimize+  renderMaximizations = fmap (\case Some1 maxExpr -> render maxExpr) . view targetMaximize

@@ -12,6 +12,7 @@ import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Expr import Data.GADT.Compare+import Data.Some.Constraint import Data.HashMap.Lazy import Data.Default import Data.Kind@@ -72,7 +73,7 @@ share origExpr expr = do   let sn = unsafePerformIO (makeStableName' origExpr)    in use (stableMap.at sn) >>= \mexpr' -> case mexpr' of-        Just (SomeSMTSort expr') -> case geq (sortSing' origExpr) (sortSing' expr') of+        Just (Some1 expr') -> case geq (sortSing' origExpr) (sortSing' expr') of           Nothing -> expr >>= makeNode sn           Just Refl -> return expr'         Nothing -> expr >>= makeNode sn@@ -81,7 +82,7 @@ makeNode sn nodeExpr = do   nodeVar <- var   assertSharedNode sn $ nodeVar === nodeExpr-  stableMap.at sn ?= SomeSMTSort nodeVar+  stableMap.at sn ?= Some1 nodeVar   return nodeVar  makeStableName' :: a -> IO (StableName ())

@@ -2,8 +2,8 @@  module Language.Hasmtlib.Internal.Uniplate1 where -import Language.Hasmtlib.Internal.Constraint import Data.Functor.Identity+import Data.Some.Constraint import Data.Kind  type Uniplate1 :: (k -> Type) -> [k -> Constraint] -> Constraint

@@ -27,6 +27,7 @@ import Language.Hasmtlib.Type.OMT import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.SMTSort+import Data.Some.Constraint import Data.Sequence as Seq hiding ((|>)) import Data.ByteString.Lazy (ByteString, split) import Data.ByteString.Lazy.UTF8 (toString)@@ -160,8 +161,8 @@ instance StateDebugger SMT where   statistically = silently     { debugState = \s -> do-      putStrLn $ "Bool Vars:  " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> True ; _ -> False) $ s^.vars)-      putStrLn $ "Arith Vars: " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> False ; _ -> True) $ s^.vars)+      putStrLn $ "Bool Vars:  " ++ show (Seq.length $ Seq.filter (\(Some1 v) -> case sortSing' v of SBoolSort -> True ; _ -> False) $ s^.vars)+      putStrLn $ "Arith Vars: " ++ show (Seq.length $ Seq.filter (\(Some1 v) -> case sortSing' v of SBoolSort -> False ; _ -> True) $ s^.vars)       putStrLn $ "Assertions: " ++ show (Seq.length (s^.formulas))       putStrLn $ "Size:       " ++ show (sum $ fmap exprSize $ s^.formulas)     }@@ -169,14 +170,14 @@ instance StateDebugger OMT where   statistically = silently     { debugState = \omt -> do-      putStrLn $ "Bool Vars:       " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> True ; _ -> False) $ omt^.smt.vars)-      putStrLn $ "Arith Vars:      " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> False ; _ -> True) $ omt^.smt.vars)+      putStrLn $ "Bool Vars:       " ++ show (Seq.length $ Seq.filter (\(Some1 v) -> case sortSing' v of SBoolSort -> True ; _ -> False) $ omt^.smt.vars)+      putStrLn $ "Arith Vars:      " ++ show (Seq.length $ Seq.filter (\(Some1 v) -> case sortSing' v of SBoolSort -> False ; _ -> True) $ omt^.smt.vars)       putStrLn $ "Hard assertions: " ++ show (Seq.length (omt^.smt.formulas))       putStrLn $ "Soft assertions: " ++ show (Seq.length (omt^.softFormulas))       putStrLn $ "Optimizations:   " ++ show (Seq.length (omt^.targetMinimize) + Seq.length (omt^.targetMaximize))       let omtSize = sum (fmap exprSize $ omt^.smt.formulas)                   + sum (fmap (exprSize . view formula) $ omt^.softFormulas)-                  + sum (fmap (\(SomeSMTSort (Minimize expr)) -> exprSize expr) $ omt^.targetMinimize)-                  + sum (fmap (\(SomeSMTSort (Maximize expr)) -> exprSize expr) $ omt^.targetMaximize)+                  + sum (fmap (\(Some1 (Minimize expr)) -> exprSize expr) $ omt^.targetMinimize)+                  + sum (fmap (\(Some1 (Maximize expr)) -> exprSize expr) $ omt^.targetMaximize)       putStrLn $ "Size:            " ++ show omtSize     }

@@ -31,6 +31,7 @@ import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.SMT+import Data.Some.Constraint import Data.List (isPrefixOf) import Data.Default import Data.Coerce@@ -76,7 +77,7 @@    var' p = do     newVar <- smtvar' p-    smt.vars %= (|> SomeSMTSort newVar)+    smt.vars %= (|> Some1 newVar)     return $ Var newVar   {-# INLINE var' #-} @@ -97,11 +98,11 @@   minimize expr = do     sm <- use (smt.sharingMode)     sExpr <- runSharing sm expr-    modifying targetMinimize (|> SomeSMTSort (Minimize sExpr))+    modifying targetMinimize (|> Some1 (Minimize sExpr))   maximize expr = do     sm <- use (smt.sharingMode)     sExpr <- runSharing sm expr-    modifying targetMaximize (|> SomeSMTSort (Maximize sExpr))+    modifying targetMaximize (|> Some1 (Maximize sExpr))   assertSoft expr w gid = do     sm <- use (smt.sharingMode)     sExpr <- runSharing sm expr

@@ -21,6 +21,7 @@ import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Option import Language.Hasmtlib.Type.Expr+import Data.Some.Constraint import Data.List (isPrefixOf) import Data.Default import Data.Coerce@@ -57,7 +58,7 @@    var' p = do     newVar <- smtvar' p-    vars %= (|> SomeSMTSort newVar)+    vars %= (|> Some1 newVar)     return $ Var newVar   {-# INLINEABLE var' #-} 

@@ -18,17 +18,16 @@ , KnownSMTSort(..), sortSing'    -- * Existential-, SomeSMTSort(..) , SomeKnownSMTSort ) where -import Language.Hasmtlib.Internal.Constraint import Language.Hasmtlib.Type.Bitvec import Language.Hasmtlib.Type.ArrayMap import Data.GADT.Compare import Data.Kind import Data.Proxy+import Data.Some.Constraint import qualified Data.Text as Text import Control.Lens import GHC.TypeLits@@ -125,11 +124,5 @@ sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t sortSing' _ = sortSing @t --- | An existential wrapper that hides some 'SMTSort' and a list of 'Constraint's holding for it.-data SomeSMTSort cs f where-  SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f--deriving instance (forall t. Show (f t)) => Show (SomeSMTSort cs f)- -- | An existential wrapper that hides some known 'SMTSort'.-type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f+type SomeKnownSMTSort f = Some1 ((~) f) KnownSMTSort

@@ -38,6 +38,7 @@ import Data.IntMap as IMap hiding (foldl) import Data.Dependent.Map as DMap import Data.Dependent.Map.Lens+import Data.Some.Constraint import Control.Lens  -- | Results of check-sat commands.@@ -64,12 +65,12 @@ instance Ord (HaskellType t) => OrdHaskellType t  -- | An existential wrapper that hides some known 'SMTSort' with an 'Ord' 'HaskellType'-type SomeKnownOrdSMTSort f = SomeSMTSort '[KnownSMTSort, OrdHaskellType] f+type SomeKnownOrdSMTSort f = Somes1 '[(~) f] '[KnownSMTSort, OrdHaskellType]  -- | Create a 'Solution' from some 'SMTVarSol's. fromSomeVarSols :: [SomeKnownOrdSMTSort SMTVarSol] -> Solution fromSomeVarSols = foldl-  (\dsol (SomeSMTSort s) -> let sSort = sortSing' s in+  (\dsol (Some1 s) -> let sSort = sortSing' s in     dsol & dmat sSort %~       (\case         Nothing -> Just $ IntValueMap $ IMap.singleton (s^.solVar.varId) (s^.solVal)