hasmtlib 1.1.2 → 1.2.0

raw patch · 10 files changed

+150/−100 lines, 10 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−0
• hasmtlib.cabal +1/−1
• src/Language/Hasmtlib/Boolean.hs +6/−6
• src/Language/Hasmtlib/Codec.hs +17/−7
• src/Language/Hasmtlib/Equatable.hs +9/−8
• src/Language/Hasmtlib/Internal/Expr.hs +16/−13
• src/Language/Hasmtlib/Internal/Expr/Num.hs +9/−35
• src/Language/Hasmtlib/Internal/Render.hs +8/−1
• src/Language/Hasmtlib/Type/Expr.hs +60/−11
• src/Language/Hasmtlib/Type/Solver.hs +16/−18

@@ -6,6 +6,14 @@ 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/). +## v1.2.0 _(2024-07-11)_++### Added+- Added n-ary comparisons `distinct` & `equal`++### Changed+- *(breaking change)* When using `interactiveWith` the `SMTOption` `Incremental` is no longer set by default anymore+ ## v1.1.2 _(2024-07-02)_  ### Changed

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

@@ -2,7 +2,7 @@  module Language.Hasmtlib.Boolean where -import Prelude (Bool(..), (.), id, Eq(..))  +import Prelude (Bool(..), (.), id, Eq(..)) import qualified Prelude as P import Data.Bit import Data.Coerce@@ -10,7 +10,7 @@ import Data.Foldable hiding (and, or) import qualified Data.Vector.Unboxed.Sized as V import GHC.TypeNats-  + class Boolean b where   -- | Lift a 'Bool'   bool :: Bool -> b@@ -40,7 +40,7 @@    -- | Exclusive-or   xor :: b -> b -> b- +   infixr 3 &&   infixr 2 ||   infixr 0 ==>@@ -81,11 +81,11 @@   (||)  = (P.||)   not   = P.not   xor   = (/=)-  + instance Boolean Bit where   bool = Bit-  (&&) = (.&.) -  (||) = (.|.) +  (&&) = (.&.)+  (||) = (.|.)   not  = complement   xor  = Bits.xor 

@@ -1,10 +1,11 @@ {-# LANGUAGE DefaultSignatures #-} -- required for DefaultEncoded a-{-# LANGUAGE UndecidableInstances #-}  +{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE LambdaCase #-}  module Language.Hasmtlib.Codec where -import Prelude hiding (not, (&&), (||))+import Prelude hiding (not, (&&), (||), all, and) import Language.Hasmtlib.Internal.Bitvec import Language.Hasmtlib.Internal.Expr import Language.Hasmtlib.Type.Solution@@ -12,11 +13,13 @@ import Language.Hasmtlib.Boolean import Data.Kind import Data.Coerce+import qualified Data.List as List import Data.Map (Map) import Data.Sequence (Seq)-import Data.IntMap as IM+import Data.IntMap as IM hiding (foldl) import Data.Dependent.Map as DMap import Data.Tree (Tree)+import qualified Data.Vector.Sized as V import Control.Monad  -- | Compute the default 'Decoded' 'Type' for every functor-wrapper.@@ -56,8 +59,15 @@   decode sol (Div x y)          = liftA2 (/)   (decode sol x) (decode sol y)   decode sol (LTH x y)          = liftA2 (<)   (decode sol x) (decode sol y)   decode sol (LTHE x y)         = liftA2 (<=)  (decode sol x) (decode sol y)-  decode sol (EQU x y)          = liftA2 (==)  (decode sol x) (decode sol y)-  decode sol (Distinct x y)     = liftA2 (/=)  (decode sol x) (decode sol y)+  decode sol (EQU xs)           = do+    xs' <- decode sol (V.toList xs)+    case xs' of+      []   -> return true+      (x:xs'') -> return $ all (x ==) xs''+  decode sol (Distinct xs)      = do+    xs' <- decode sol (V.toList xs)+    let xss = List.filter ((==2) . length) $ List.permutations xs'+    return $ all (\case (a:b:_) -> a /= b ; _ -> true) xss   decode sol (GTHE x y)         = liftA2 (>=)  (decode sol x) (decode sol y)   decode sol (GTH x y)          = liftA2 (>)   (decode sol x) (decode sol y)   decode sol (Not x)            = fmap   not  (decode sol x)@@ -77,7 +87,7 @@   decode sol (ToReal x)         = fmap realToFrac (decode sol x)   decode sol (ToInt x)          = fmap truncate   (decode sol x)   decode sol (IsInt x)          = fmap ((0 ==) . snd . properFraction) (decode sol x)-  decode sol (Ite p t f)        = liftM3 (\p' t' f' -> if p' then t' else f') (decode sol p) (decode sol t) (decode sol f) +  decode sol (Ite p t f)        = liftM3 (\p' t' f' -> if p' then t' else f') (decode sol p) (decode sol t) (decode sol f)   decode sol (BvNot x)          = fmap not (decode sol x)   decode sol (BvAnd x y)        = liftA2 (&&) (decode sol x) (decode sol y)   decode sol (BvOr x y)         = liftA2 (||) (decode sol x) (decode sol y)@@ -103,7 +113,7 @@   decode sol (ArrStore i x arr) = liftM3 arrStore (decode sol i) (decode sol x) (decode sol arr)   decode _ (ForAll _ _)         = Nothing   decode _ (Exists _ _)         = Nothing-  +   encode = Constant . wrapValue  instance Codec () where

@@ -7,20 +7,21 @@ import Prelude hiding (not, (&&)) import Language.Hasmtlib.Internal.Expr import Language.Hasmtlib.Boolean-import GHC.Generics-import Numeric.Natural import Data.Int import Data.Word import Data.Void+import qualified Data.Vector.Sized as V+import Numeric.Natural+import GHC.Generics  -- | Test two as on equality as SMT-Expression.--- +-- -- @ --     x <- var @RealType---     y <- var +--     y <- var --     assert $ y === x && not (y /== x) -- @--- +-- class Equatable a where   -- | Test whether two values are equal in the SMT-Problem.   (===) :: a -> a -> Expr BoolSort@@ -34,9 +35,9 @@ infix 4 ===, /==  instance (KnownSMTSort t, Eq (HaskellType t)) => Equatable (Expr t) where-  (===) = EQU-  {-# INLINE (===) #-}  -  (/==) = Distinct+  x === y = EQU $ V.fromTuple (x,y)+  {-# INLINE (===) #-}+  x /== y = Distinct $ V.fromTuple (x,y)   {-# INLINE (/==) #-}  class GEquatable f where

@@ -11,11 +11,14 @@ import Language.Hasmtlib.Type.ArrayMap import Language.Hasmtlib.Boolean import Data.GADT.Compare-import Data.Map+import Data.Map hiding (toList)+import Data.List (intercalate) import Data.Kind import Data.Proxy import Data.Coerce+import Data.Foldable (toList) import Data.ByteString.Builder+import qualified Data.Vector.Sized as V import Control.Lens import GHC.TypeLits @@ -126,11 +129,11 @@ sortSing' _ = sortSing @t  -- | 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 = ()@@ -141,7 +144,7 @@   SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f  -- | An existential wrapper that hides some known 'SMTSort'.-type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f +type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f  -- | A SMT expression. --   For internal use only.@@ -160,8 +163,8 @@    LTH       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort   LTHE      :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort-  EQU       :: (Eq  (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort-  Distinct  :: (Eq  (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort+  EQU       :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => V.Vector (n + 2) (Expr t) -> Expr BoolSort+  Distinct  :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => V.Vector (n + 2) (Expr t) -> Expr BoolSort   GTHE      :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort   GTH       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort @@ -227,7 +230,7 @@   {-# INLINE not #-}   xor  = Xor   {-# INLINE xor #-}-  + instance KnownNat n => Boolean (Expr (BvSort n)) where   bool = Constant . BvValue . bool   {-# INLINE bool #-}@@ -239,11 +242,11 @@   {-# INLINE not #-}   xor  = BvXor   {-# INLINE xor #-}-  + instance Bounded (Expr BoolSort) where   minBound = false   maxBound = true-  + instance KnownNat n => Bounded (Expr (BvSort n)) where   minBound = Constant $ BvValue minBound   maxBound = Constant $ BvValue maxBound@@ -289,8 +292,8 @@    render (LTH x y)    = renderBinary "<" x y   render (LTHE x y)   = renderBinary "<=" x y-  render (EQU x y)    = renderBinary "=" x y-  render (Distinct x y) = renderBinary "distinct" x y+  render (EQU xs)     = renderNary "=" $ V.toList xs+  render (Distinct xs)= renderNary "distinct" $ V.toList xs   render (GTHE x y)   = renderBinary ">=" x y   render (GTH x y)    = renderBinary ">" x y @@ -373,8 +376,8 @@   show (Div x y)            = "(" ++ show x ++ " / " ++ show y ++ ")"   show (LTH x y)            = "(" ++ show x ++ " < " ++ show y ++ ")"   show (LTHE x y)           = "(" ++ show x ++ " <= " ++ show y ++ ")"-  show (EQU x y)            = "(" ++ show x ++ " == " ++ show y ++ ")"-  show (Distinct x y)       = "(" ++ show x ++ " /= " ++ show y ++ ")"+  show (EQU xs)             = "(= " ++ intercalate " " (show <$> toList xs) ++ ")"+  show (Distinct xs)        = "(distinct " ++ intercalate " " (show <$> toList xs) ++ ")"   show (GTHE x y)           = "(" ++ show x ++ " >= " ++ show y ++ ")"   show (GTH x y)            = "(" ++ show x ++ " > " ++ show y ++ ")"   show (Not x)              = "(not " ++ show x ++ ")"

@@ -5,10 +5,9 @@ import Language.Hasmtlib.Integraled import Language.Hasmtlib.Iteable import Language.Hasmtlib.Equatable-import Language.Hasmtlib.Orderable  -import Data.Proxy+import Language.Hasmtlib.Orderable import GHC.TypeNats-  + instance Num (Expr IntSort) where    fromInteger = Constant . IntValue    {-# INLINE fromInteger #-}@@ -42,7 +41,7 @@    {-# INLINE signum #-}  instance KnownNat n => Num (Expr (BvSort n)) where-   fromInteger = Constant . BvValue . fromInteger +   fromInteger = Constant . BvValue . fromInteger    {-# INLINE fromInteger #-}    (+)         = BvAdd    {-# INLINE (+) #-}@@ -54,7 +53,7 @@    {-# INLINE abs #-}    signum _    = 0    {-# INLINE signum #-}-   + instance Fractional (Expr RealSort) where   fromRational = Constant . RealValue . fromRational   {-# INLINE fromRational #-}@@ -90,15 +89,15 @@  instance Integraled (Expr IntSort) where   quot = IDiv-  {-# INLINE quot #-}  +  {-# INLINE quot #-}   rem  = Mod-  {-# INLINE rem #-}  +  {-# INLINE rem #-}   div  = IDiv-  {-# INLINE div #-}  +  {-# INLINE div #-}   mod  = Mod-  {-# INLINE mod #-}  +  {-# INLINE mod #-}   quotRem x y = (quot x y, rem x y)-  {-# INLINE quotRem #-}  +  {-# INLINE quotRem #-}   divMod x y  = (div x y, mod x y)   {-# INLINE divMod #-} @@ -115,28 +114,3 @@   {-# INLINE quotRem #-}   divMod x y  = (div x y, mod x y)   {-# INLINE divMod #-}---- | Bitvector shift left-bvShL    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-bvShL    = BvShL-{-# INLINE bvShL #-}---- | Bitvector logical shift right-bvLShR   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-bvLShR   = BvLShR-{-# INLINE bvLShR #-}---- | Concat two bitvectors-bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))-bvConcat = BvConcat-{-# INLINE bvConcat #-}---- | Rotate bitvector left-bvRotL   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)-bvRotL   = BvRotL-{-# INLINE bvRotL #-}---- | Rotate bitvector right-bvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)-bvRotR   = BvRotR-{-# INLINE bvRotR #-}

@@ -1,12 +1,13 @@ module Language.Hasmtlib.Internal.Render where  import Data.ByteString.Builder+import Data.Foldable (foldl') import GHC.TypeNats  -- | Render values to their SMTLib2-Lisp form, represented as @Builder@. class Render a where   render :: a -> Builder-   + instance Render Bool where   render b = if b then "true" else "false"   {-# INLINEABLE render #-}@@ -42,3 +43,9 @@ renderTernary :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder renderTernary op x y z = "(" <> op <> " " <> render x <> " " <> render y <> " " <> render z <> ")" {-# INLINEABLE renderTernary #-}++renderNary :: Render a => Builder -> [a] -> Builder+renderNary op xs = "(" <> op <> renderedXs <> ")"+  where+    renderedXs = foldl' (\s x -> s <> " " <> render x) mempty xs+{-# INLINEABLE renderNary #-}

@@ -1,4 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ViewPatterns #-}  module Language.Hasmtlib.Type.Expr  ( SMTSort(..)@@ -7,27 +8,50 @@  , Value(..), unwrapValue, wrapValue  , SSMTSort(..), KnownSMTSort(..), sortSing', SomeSMTSort(..), SomeKnownSMTSort, AllC  , Expr+ , equal, distinct+ , bvShL, bvLShR, bvConcat, bvRotL, bvRotR  , for_all , exists  , select, store- , module Language.Hasmtlib.Internal.Expr.Num  ) where  import Language.Hasmtlib.Internal.Expr-import Language.Hasmtlib.Internal.Expr.Num+import Language.Hasmtlib.Internal.Expr.Num ()+import Language.Hasmtlib.Boolean+import Data.Proxy+import Data.List (genericLength)+import Data.Foldable (toList)+import qualified Data.Vector.Sized as V+import GHC.TypeNats +-- | Test multiple expressions on equality within in the 'SMT'-Problem.+equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort+equal (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of+  SomeNat n -> case V.fromListN' n xs of+    Nothing  -> EQU $ V.fromTuple (a,b)+    Just xs' -> EQU $ xs' V.++ V.fromTuple (a,b)+equal (toList -> _)        = true++-- | Test multiple expressions on distinctness within in the 'SMT'-Problem.+distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort+distinct (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of+  SomeNat n -> case V.fromListN' n xs of+    Nothing  -> Distinct $ V.fromTuple (a,b)+    Just xs' -> Distinct $ xs' V.++ V.fromTuple (a,b)+distinct (toList -> _)        = true+ -- | A universal quantification for any specific 'SMTSort'. --   If the type cannot be inferred, apply a type-annotation. --   Nested quantifiers are also supported.--- +-- --   Usage: -- --   @ --   assert $ --      for_all @IntSort $ \x ->---         x + 0 === x && 0 + x === x ---   @   --- +--         x + 0 === x && 0 + x === x+--   @+-- --   The lambdas 'x' is all-quantified here. --   It will only be scoped for the lambdas body. for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort@@ -36,16 +60,16 @@ -- | An existential quantification for any specific 'SMTSort' --   If the type cannot be inferred, apply a type-annotation. --   Nested quantifiers are also supported.--- +-- --   Usage:--- +-- --   @ --   assert $ --      for_all @(BvSort 8) $ \x -> --          exists $ \y ->---            x - y === 0 ---   @   --- +--            x - y === 0+--   @+-- --   The lambdas 'y' is existentially quantified here. --   It will only be scoped for the lambdas body. exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort@@ -58,3 +82,28 @@ -- | Store a value in an array. store :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v) store = ArrStore++-- | Bitvector shift left+bvShL    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)+bvShL    = BvShL+{-# INLINE bvShL #-}++-- | Bitvector logical shift right+bvLShR   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)+bvLShR   = BvLShR+{-# INLINE bvLShR #-}++-- | Concat two bitvectors+bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))+bvConcat = BvConcat+{-# INLINE bvConcat #-}++-- | Rotate bitvector left+bvRotL   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)+bvRotL   = BvRotL+{-# INLINE bvRotL #-}++-- | Rotate bitvector right+bvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)+bvRotR   = BvRotR+{-# INLINE bvRotR #-}

@@ -1,9 +1,7 @@ module Language.Hasmtlib.Type.Solver where  import Language.Hasmtlib.Type.Pipe-import Language.Hasmtlib.Type.Option import Language.Hasmtlib.Type.Solution-import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Codec import qualified SMTLIB.Backends as B import qualified SMTLIB.Backends.Process as P@@ -37,62 +35,62 @@ -- main = do --   res <- solveWith (solver cvc5) $ do --     setLogic \"QF_LIA\"--- +-- --     x <- var @IntSort--- +-- --     assert $ x >? 0---     +-- --     return x--- +-- --   print res -- @ solveWith :: (Monad m, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a)) solveWith solver m = do   (a, problem) <- runStateT m def   (result, solution) <- solver problem-    +   return (result, decode solution a)  -- | Pipes an SMT-problem interactively to the solver. --   Enables incremental solving by default. --   Here is a small example of how to use it for solving a problem utilizing the solvers incremental stack:--- +-- -- @ -- import Language.Hasmtlib -- import Control.Monad.IO.Class--- +-- -- main :: IO () -- main = do --   cvc5Living <- interactiveSolver cvc5 --   interactiveWith cvc5Living $ do+--     setOption $ Incremental True --     setOption $ ProduceModels True --     setLogic \"QF_LIA\"--- +-- --     x <- var @IntSort--- +-- --     assert $ x >? 0--- +-- --     (res, sol) <- solve --     liftIO $ print res --     liftIO $ print $ decode sol x--- +-- --     push --     y <- var @IntSort--- +-- --     assert $ y <? 0 --     assert $ x === y--- +-- --     res' <- checkSat --     liftIO $ print res' --     pop--- +-- --     res'' <- checkSat --     liftIO $ print res''--- +-- --   return () -- @ interactiveWith :: (MonadIO m, WithSolver s) => (B.Solver, P.Handle) -> StateT s m () -> m () interactiveWith (solver, handle) m = do-   liftIO $ B.command_ solver $ render (Incremental True)    _ <- runStateT m $ withSolver solver    liftIO $ P.close handle