Search code examples
constraint-programmingeclipse-clp

ECLiPSe CLP produces variable with unexpected range


I have a question regarding the following code:

:-lib(ic).

buggy_pred(Result, In0, In1, In2, In3, In4, In5, In6, In7) :-

    Args = [In0, In1, In2, In3, In4, In5, In6, In7],
    Args :: [0..255],

    Result :: [0..18446744073709551615],    % 64bits wide

    % put 8 bytes together to form a 64-bit value
    Result #= (In0 + (In1 * 256) + (In2 * 65536) + (In3 * 16777216) + (In4 * 4294967296) +
        (In5 * 1099511627776) + (In6 * 281474976710656) + (In7 * 72057594037927936)).


buggy_pred_test :-
    buggy_pred(Result, 56, 8, 0, 0, 16, 0, 0, 1),
    get_bounds(Result, Lo, Hi),

    write(Lo), nl,
    write(Hi).

Should not the above code (predicate buggy_pred_test) print two same numbers? In this case it yields two numbers (Lo and Hi respectively) which are different:

72057662757406720
72057662757406800

I cannot figure out what is the cause of that behaviour. I am using ECLiPSE 6.1 #194, x86_64 for linux. Your help is greatly appreciated.


Solution

  • ECLiPSe's lib(ic) constraint solver is designed for handling mixtures of real- and integer-valued variables/constraints. All computations are performed using double floats to represent upper and lower bounds, even integer operations (integrality is simply treated as an additional constraint).

    Because double floats have 53 bits of precision, only integers in the range -9007199254740991..9007199254740991 can be represented precisely. Larger integers are approximated by a floating point interval that encloses the true value. This is why you get a non-zero-width interval as a result.

    This may sound unsatisfactory, but in practice models involving huge integer domains are rarely efficiently solvable, and are therefore less useful than they may seem. So, the advice would be to model the problem differently, see here for an example of modeling a problem in two ways.