simple-smt 0.5.2 → 0.5.3

raw patch · 3 files changed

+15/−1 lines, 3 files

Files

• CHANGES +2/−0
• SimpleSMT.hs +12/−0
• simple-smt.cabal +1/−1

@@ -1,3 +1,5 @@+0.5.3: Add 'zeroExtend' and 'signExtend'+0.5.2: Fix right shift 0.5.1:  Add 'define' commands 0.5:    Adds more bit-wise operations 0.4:    Fixes definiiton of `geq`

@@ -106,6 +106,8 @@   , bvShl   , bvLShr   , bvAShr+  , signExtend+  , zeroExtend      -- ** Arrays   , select@@ -615,6 +617,15 @@ concat :: SExpr -> SExpr -> SExpr concat x y = fun "concat" [x,y] +-- | Extend to the signed equivalent bitvector by @i@ bits+signExtend :: Integer -> SExpr -> SExpr+signExtend i x = List [ fam "sign_extend" [i], x ]++-- | Extend with zeros to the unsigned equivalent bitvector+-- by @i@ bits+zeroExtend :: Integer -> SExpr -> SExpr+zeroExtend i x = List [ fam "zero_extend" [i], x ]+ -- | Extract a sub-sequence of a bit vector. extract :: SExpr -> Integer -> Integer -> SExpr extract x y z = List [ fam "extract" [y,z], x ]@@ -683,6 +694,7 @@ -- | 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.5.2+version:             0.5.3 synopsis:            A simple way to interact with an SMT solver process. description:         A simple way to interact with an SMT solver process. license:             BSD3