Add bit-vector to integer conversions

LeventErkok · Jul 8, 2015 · 67e66dd · 67e66dd
1 parent 61687d0
commit 67e66dd
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 2 deletions.
diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs
@@ -610,10 +610,18 @@ handleIntCast kFrom kTo a
          | m == n = a
          | True   = extract (n - 1)
 
-        b2i s m = error "TBD: b2i_" ++ show (s, m)
         i2u n   = error $ "TBD: i2u_" ++ show n
         i2s n   = error $ "TBD: i2s_" ++ show n
 
+        b2i s m
+          | s    = "(- " ++ val ++ " " ++ valIf (2^m) sign ++ ")"
+          | True = val
+          where valIf v b = "(ite (= " ++ b ++ " #b1) " ++ show (v::Integer) ++ " 0)"
+                getBit i  = "((_ extract " ++ show i ++ " " ++ show i ++ ") " ++ a ++ ")"
+                bitVal i  = valIf (2^i) (getBit i)
+                val       = "(+ " ++ unwords (map bitVal [0 .. m-1]) ++ ")"
+                sign      = getBit (m-1)
+
         signExtend i = "((_ sign_extend " ++ show i ++  ") "  ++ a ++ ")"
         zeroExtend i = "((_ zero_extend " ++ show i ++  ") "  ++ a ++ ")"
         extract    i = "((_ extract "     ++ show i ++ " 0) " ++ a ++ ")"
diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs
@@ -2,4 +2,4 @@
 module SBVUnitTestBuildTime (buildTime) where
 
 buildTime :: String
-buildTime = "Tue Jul  7 21:12:15 PDT 2015"
+buildTime = "Tue Jul  7 22:12:36 PDT 2015"