[SMT-LIB] BitVectors32: DIV and MOD

[Domagoj Babic]

Vijay,

Since UDIV,SDIV (as well as UMOD,SMOD) must be distinguishable, there
are only two options:

1) Either define signed/unsigned types, and have a single DIV/MOD op,

2) or let integers be in 2's-complement and have both versions of the
operators.

I'd vote for (2):
* (2) is much more in the spirit of modular arithmetic, because modular
arithmetic really doesn't care about signs.
* That is how DIV/MOD are implemented on all the processors (at least
those I know of).
* Simpler type handling within theorem provers.
* Having a clean separation between SDIV/UDIV facilitates optimizations,
especially signed/unsigned division by a constant.


Once this is hammered down, the exact definition of UDIV/SDIV is given
by standard equations.

Domagoj