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

[Clark Barrett]

Domagoj,

I think the mod vs rem issue is nicely summarized in the following article:

http://en.wikipedia.org/wiki/Modulo_operation

A couple of things I notice here:

- Older languages typically have only one modulo operator, called "%" or mod.
  (Fortran and Pascal for example).
- If a language has more than one version of this operator, they are called rem
  and mod and have the semantics you have described.

With regard to the "%" operator, it is called the modulus operator in the
original K&R C book, and it is also called the same thing in some Java books I
have, but you are correct that some recent treatments (i.e. C99) seem to favor
calling it the remainder operataor.

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.

I hope to have the new theory specification ready in the next couple of days.

-Clark

> 
> Hi Clark,
> 
> On 5/2/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> > I respectfully disagree.  The "%" operator is called the modulus operator in C.
> > "mod" may mean different things in other languages or contexts, but using
> > "bvmod" for an operator whose semantics are the same as the C *modulus* operator
> > certainly makes sense in benchmarks derived from C programs (of which we have
> > many).  So you can justly accuse us of being C-centric in our nomenclature, but
> > saying it is outright wrong is overstating the issue.
> 
> 
> C standard: ISO/IEC 9899:1999 Sec. 6.5.5:
> 5 The result of the / operator is the quotient from the division of
> the first operand by the
> second; the result of the % operator is the remainder.
> 
> - There exists no 'modulus operator' in the index - 'remainder
>   operator' refers the reader to 6.5.5
> 
> C++ standard: ISO/IEC 14882:1998 Sec. 5.6 contains pretty much the same
> sentence as the C standard, BUT the index lumps both 'remainder
> operator' and 'modulus operator' to 'modulus operator', giving some
> justification for your statement.
> 
> VHDL standard: IEEE Std 1076 2000 Sec. 7.2.5:
> 
> Operator    Operation
> mod         Modulus
> rem         Remainder
> 
> A = (A/B) * B + (A rem B)
> A = B * N +     (A mod B)
> 
> As far as I understand, ADA has mod/rem defined in the same way, but
> couldn't get my hands on a copy of the standard unfortunately.
> 
> What I've seen in other sources is that rem/mod operator is frequently
> distinguished, and 'modulus' is used for the second operand of the
> rem/mod operation (like divisor for division), which certainly promotes
> the confusion.
> 
> 
> I'd also like to suggest thinking a little bit beyond the current state of
> the SMT-LIB:
> 
> Once you can handle all the modular arithmetic operators, floating point
> is not that far out of reach. For the floating point, ISO/IEC
> 9899:1999 clearly distinguishes FREM and FMOD (Sec. 7.12.10). For
> symmetricity, REM and MOD should be distinguished for integers as well.
> 
> Regards,
>     Domagoj Babic
>