Minizinc 按位运算符(或类似的高效运算)?

Minizinc bitwise operators (or similar efficient operation)?

我想约束一个整数变量,使其具有一些其他整数的按位异或值。 我知道我可以用布尔数组而不是整数对值进行编码,并且有类似 forall (i, j in 1..n) c[i] = a[i] xor b[i] 的东西,但我想要更有效的东西。

有没有办法在Minizinc(或直接Flatzinc)中使用按位运算符? 还是全局约束或我可以用来实现我想要的并确保它得到有效实施的东西?我正在使用 Gecode 作为求解器。

以下 MiniZinc 模型演示了计算两个整数变量的按位 XOR 的函数:

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)"];