ekmett / ersatz

A monad for interfacing with external SAT solvers
Other
62 stars 15 forks source link

strange result bit width for multiplication in type Bits #20

Closed jwaldmann closed 8 years ago

jwaldmann commented 8 years ago

following code should print number of bits used for result of multiplication:

ghci -isrc Ersatz
import Control.Monad
 ( solveWith minisat $ do x  <- Bits <$> replicateM 1000 exists ; let {y @(Bits bs) = x*x}  ; return (encode (fromIntegral (length bs))::Bits) ) :: IO (Result, Maybe Integer)

Strangely, it says 2007. Here is an actual table of values

width(x)       1 2 3  4  10  100  1000
width(x*x)    1 4 6  9  21  203  2007

Except for the first entry, we should always have width(x_x) == 2_width(x).

The extra bits are caused by intermediate additions (I guess).