simple-smt 0.4.0 → 0.5.0

raw patch · 2 files changed

+49/−2 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• SimpleSMT.hs +48/−1
• simple-smt.cabal +1/−1

@@ -71,6 +71,9 @@   , geq   , leq   , bvULt+  , bvULeq+  , bvSLt+  , bvSLeq      -- ** Arithmetic   , add@@ -89,13 +92,18 @@   , bvNot   , bvNeg   , bvAnd+  , bvXOr   , bvOr   , bvAdd+  , bvSub   , bvMul   , bvUDiv   , bvURem+  , bvSDiv+  , bvSRem   , bvShl   , bvLShr+  , bvAShr      -- ** Arrays   , select@@ -446,7 +454,9 @@ --      up so that it is. --    * The width should be strictly positive. bvHex :: Int {- ^ Width, in bits -} -> Integer {- ^ Value -} -> SExpr-bvHex w v = const ("#x" ++ padding ++ hex)+bvHex w v+  | v >= 0    = const ("#x" ++ padding ++ hex)+  | otherwise = bvHex w (2^w + v)   where   hex     = showHex v ""   padding = replicate (P.div (w + 3) 4 - length hex) '0'@@ -522,9 +532,21 @@ bvULt :: SExpr -> SExpr -> SExpr bvULt x y = fun "bvult" [x,y] +-- | Unsigned less-than-or-equal on bit-vectors.+bvULeq :: SExpr -> SExpr -> SExpr+bvULeq x y = fun "bvule" [x,y] +-- | Signed less-than on bit-vectors.+bvSLt :: SExpr -> SExpr -> SExpr+bvSLt x y = fun "bvslt" [x,y] +-- | Signed less-than-or-equal on bit-vectors.+bvSLeq :: SExpr -> SExpr -> SExpr+bvSLeq x y = fun "bvsle" [x,y] +++ -- | Addition. -- See also 'bvAdd' add :: SExpr -> SExpr -> SExpr@@ -583,6 +605,10 @@ bvOr :: SExpr -> SExpr -> SExpr bvOr x y = fun "bvor" [x,y] +-- | Bitwsie exclusive or.+bvXOr :: SExpr -> SExpr -> SExpr+bvXOr x y = fun "bvxor" [x,y]+ -- | Bit vector arithmetic negation. bvNeg :: SExpr -> SExpr bvNeg x = fun "bvneg" [x]@@ -591,6 +617,12 @@ bvAdd :: SExpr -> SExpr -> SExpr bvAdd x y = fun "bvadd" [x,y] +-- | Subtraction of bit vectors.+bvSub :: SExpr -> SExpr -> SExpr+bvSub x y = fun "bvsub" [x,y]+++ -- | Multiplication of bit vectors. bvMul :: SExpr -> SExpr -> SExpr bvMul x y = fun "bvmul" [x,y]@@ -603,6 +635,17 @@ bvURem :: SExpr -> SExpr -> SExpr bvURem x y = fun "bvurem" [x,y] +-- | Bit vector signed division.+bvSDiv :: SExpr -> SExpr -> SExpr+bvSDiv x y = fun "bvsdiv" [x,y]++-- | Bit vector signed reminder.+bvSRem :: SExpr -> SExpr -> SExpr+bvSRem x y = fun "bvsrem" [x,y]++++ -- | Shift left. bvShl :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr bvShl x y = fun "bvshl" [x,y]@@ -610,6 +653,10 @@ -- | Logical shift right. bvLShr :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr bvLShr x y = fun "bvshr" [x,y]++-- | Arithemti shift right (copies most significant bit).+bvAShr :: SExpr {- ^ value -} -> SExpr {- ^ shift amount -} -> SExpr+bvAShr x y = fun "bvashr" [x,y]  -- | Get an elemeent of an array. select :: SExpr {- ^ array -} -> SExpr {- ^ index -} -> SExpr

@@ -1,5 +1,5 @@ name:                simple-smt-version:             0.4.0+version:             0.5.0 synopsis:            A simple way to interact with an SMT solver process. description:         A simple way to interact with an SMT solver process. license:             BSD3