Minizinc bitwise operators (or similar efficient operation)?

Question

I would like to constrain an integer variable to have as value the bitwise XOR of some other integers. I know I can encode the values in boolean arrays instead of integers and have something like forall (i, j in 1..n) c[i] = a[i] xor b[i] but I would like something more efficient.

Is there any way to use bitwise operators in Minizinc (or directly Flatzinc)? Or alternatively a global constraint or something I can use to achieve what I want and make sure it is implemented efficiently? I am using Gecode as solver.

Answer 1

The following MiniZinc model demonstrates a function to compute the bitwise XOR of two integer variables:

include "globals.mzn";

int: bits = 15;
set of int: Bits = 0 .. bits-1;
set of int: Domain = 0 .. pow(2, bits) - 1;

var Domain: x;
var Domain: y;

%  pre-calculate powers of 2: 1, 2, 4, ...
array[Bits] of Domain: twopow = array1d(Bits, [pow(2, i) | i in Bits]);

%  test bit in int
function var int: bit_of(var int: num, Bits: idx) = 
  ((num div twopow[idx]) mod 2);

%  function to calculate the bitwise XOR of two ints
function var int: bitxor(var int: x, var int: y) =
  sum([twopow[i] * ((bit_of(x, i) + bit_of(y, i)) mod 2) | i in Bits]);

constraint y = 0x05;

constraint bitxor(x, y) = 0xA5;

solve satisfy;

output ["\(x) \(y)"];