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

[Domagoj Babic]

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