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

[Domagoj Babic]

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