I’m having trouble getting my point across, so let me try and tackle it from a different perspective.
The fundamental problem is that integers are not closed under division, i.e., dividing two integers does not always produce an integer result - see Division (mathematics) - Wikipedia. The Wikipedia article offers five alternatives when the result of division is not an integer.
Now the “domain of discourse” for clpfd
is the set of integers, including infinity values. This reduces the set of possible alternatives when dividing two integers to 1. (partial function) and 5. (integer division). clpfd
made the decision to only support 5. and uses the integer divide operator //
rather than the division operator /
(and rightly so).
Most programming languages (and computers) also support IEEE floating point arithmetic. This extends the “domain of discourse” to a subset of real numbers (actually rational numbers), and, although floating point arithmetic is notoriously unsound, it’s adequate for most practical purposes. This domain extension to a subset of reals opens up the possibility of alternative 2., i.e., dividing two integers can yield a floating point value as an approximation to the real result. But since, in most cases, they also want 5. as an option, they end up with two integer division operations.
The “domain of discourse” for clpBNR
is the entire set of reals, and reals are closed under division - dividing a real by a real always produces a real. This only requires one division operator/function. So a clpBNR
integer is not a separate domain with a different set of operators. Instead it’s a constraint on the possible values of a real. The reason why clpBNR
" … blends and allows using constraints in the boolean, real and integer domains " is that, in fact, they’re not really separate domains at all; they’re all reals.
So clpBNR
currently supports alternatives 1. and 2. depending on how the result is constrained, e.g., [A,B,C]::integer, {A==B/C}
corresponds to option 1. and [B,C]::integer, {A==B/C}
corresponds to option 2. (or 3. under most circumstances).
The question I would like to answer is, given the above, whether there is a need to support 5. and why? Do we have any examples of real problems to which clpBNR
can be applied and can only be done with 5. ? I need an explanation for two divide operations in clpBNR
beyond “lots/most of other arithmetic systems have it”. I see no point in adding “features” that nobody is going to use.
And these are the people I’d like to hear from, surely they have relevant examples. (On the other hand, I’m not sure why anyone would port a working clpfd
program to clpBNR
, so that would be a useful discussion as well.)
Note that I’m not questioning the usefulness of integer division in general, just in a clpBNR
context. It’s not hard to think of useful examples using standard functional arithmetic; converting numeric values to strings comes to mind. But why would I use clpBNR
for that?
And I’m not questioning it on the basis of any practical implementation/maintenance considerations. I’d be all over it if I could figure out a good reason for doing it, because then I could explain it.