Using "17-bit-vectors" in SBV

bitvec17.hs

import Control.Monad.Trans  (liftIO)
import Control.Monad.Reader (ask)

import Data.SBV.Dynamic

--------------------------------------------------------------------------------
-- I should really export the following four definitions from SBV.Dynamic
mkWordN :: Int -> String -> Symbolic SVal
mkWordN w nm = ask >>= liftIO . svMkSymVar Nothing (KBounded False w) (Just nm)

mkWordN_ :: Int -> Symbolic SVal
mkWordN_ w   = ask >>= liftIO . svMkSymVar Nothing (KBounded False w) Nothing

mkIntN :: Int -> String -> Symbolic SVal
mkIntN w nm = ask >>= liftIO . svMkSymVar Nothing (KBounded True w) (Just nm)

mkIntN_ :: Int -> Symbolic SVal
mkIntN_ w   = ask >>= liftIO . svMkSymVar Nothing (KBounded True w) Nothing
--------------------------------------------------------------------------------

-- proves (x-y)*(x+y) = x*x - y*y
good = proveWith z3{verbose=True} $ do
                         x <- mkWordN 17 "x"
                         y <- mkWordN 17 "y"
                         let lhs = (x `svMinus` y) `svTimes` (x `svPlus` y)
                             rhs = (x `svTimes` x) `svMinus` (y `svTimes` y)
                         return $ lhs `svEqual` rhs

-- shows that (x-y)-(x+y) = x*x - y*y does not hold!
bad = proveWith z3{verbose=True} $ do
                        x <- mkWordN 17 "x"
                        y <- mkWordN 17 "y"
                        let lhs = (x `svMinus` y) `svMinus` (x `svPlus` y)
                            rhs = (x `svTimes` x) `svMinus` (y `svTimes` y)
                        return $ lhs `svEqual` rhs