differential-datalog
differential-datalog copied to clipboard
Type constraints for right-hand operand of shift operators
The following program:
input relation X(x: bit<16>, y: bit<16>)
output relation Y(x: bit<16>, y: bit<16>, z: bit<16>)
Y(x, y, x << y) :- X(x, y).
yields the following compiler error that I don't expect (with release v1.2.3 and earlier releases):
error: /home/blp/nerpa/nerpa/ofp4/test.dl:3.6-3.7: Unsatisfiable bit-width constraint '16 = 0' in
expected type: bit<16>
actual type: bit<32>
in
expression 'y'
Y(x, y, x << y) :- X(x, y).
^
I can fix it by casting y
to u32
in the shift expression, like this:
Y(x, y, x << (y as u32)) :- X(x, y).
I would prefer that <<
(and presumably >>
) accept any integer type as its right-hand operand.
Probably any unsigned integer type only could work. Signed values introduce additional complications.
That's reasonable.
If https://github.com/vmware/differential-datalog/pull/1159 gets merged, and this bug gets fixed, then the documentation added by the PR should be updated as well.