Minizinc位运算符(或类似的有效操作)？

Question

我希望约束一个整数变量，将其他整数的按位XOR作为值。我知道我可以用布尔数组而不是整数来编码这些值，并且有一些类似于forall (i, j in 1..n) c[i] = a[i] xor b[i]的东西，但是我想要更高效的东西。

在Minizinc (或直接使用Flatzinc)中有使用位运算符的方法吗？或者是一个全局约束或者我可以用来实现我想要的东西并确保它得到有效实现的东西？我在用壁虎来解决问题。

Answer 1

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