[SMT-LIB] Bool as alias for BitVec[1]

[Clark Barrett]

Right.  The difference between mod and rem only matters in the case of signed
arithmetic.  What I meant (but did not say) in my last email was that we will
distinguish between the two in the signed case.

Thus, the new operators will be bvurem, bvsrem, and bvsmod.  I will send new
theory and logic files soon.

-Clark

> 
> Hi Clark,
> 
> On 5/7/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> > As a compromise and in recognition of the fact that recent languages include
> > both, I propose to include both bvmod and bvrem in the new theory.  The
> > "standard" operator with C semantics will be called bvrem.
> 
> If your goal is to fully support C semantics, you still haven't achieved
> it.
> 
> 
> To understand why, you need to look deeper in the standard, more
> precisely into the (horrible) type system. All the compilers I know of
> (including GCC) reduce operations on signed and unsigned types to either
> operations on signed or operations on unsigned types (according to C
> casting mechanism). For most operators, this difference doesn't matter
> because of the properties of the 2's complement. BUT, for division and
> remainder, the difference matters.
> 
> For instance, urem is performed through truncating division (explained
> on the page to which you sent me the link
> [http://en.wikipedia.org/wiki/Modulo_operation]), while srem is
> performed through Euclidian division.
> 
> If you want to support the full semantics of C, you need both versions.
> Mod operator is, however, optional.
> 
> 
> Example:
> 
> -7 mod -4 = -3
> -7 srem -4 = -3
> -7 urem -4 = 4294967289 urem 4294967292 = 4294967289 (-7)
> 
> But,
> 
> -7 mod 4 = 1
> -7 srem 4 = -3
> -7 urem 4 = 1
> 
> So, you can clearly see that mod != srem != urem.
> 
> That's why Spear format (check my web page) clearly separates urem and
> srem, and defines them both. This approach also nicely matches how most
> processors implement (un)singed remainder - through (un)signed division
> - on x86 DIV is unsigned, and IDIV is signed division.
> 
> What I'd suggest is that you support urem and srem.
> 
> Regards,
>     Domagoj Babic
>