40 lines
1.8 KiB
MiniZinc
40 lines
1.8 KiB
MiniZinc
% 位 x 的的总和 = 二元表示的 s。
|
|
% s[0], s[1], ..., s[k] 其中 2^k >= length(x) > 2^(k-1)
|
|
predicate binary_sum(array[int] of var bool:x,
|
|
array[int] of var bool:s)=
|
|
let { int: l = length(x) } in
|
|
if l == 1 then s[0] = x[1]
|
|
elseif l == 2 then
|
|
s[0] = (x[1] xor x[2]) /\ s[1] = (x[1] /\ x[2])
|
|
else let { int: ll = (l div 2),
|
|
array[1..ll] of var bool: f = [ x[i] | i in 1..ll ],
|
|
array[1..ll] of var bool: t = [x[i]| i in ll+1..2*ll],
|
|
var bool: b = if ll*2 == l then false else x[l] endif,
|
|
int: cp = floor(log2(int2float(ll))),
|
|
array[0..cp] of var bool: fs,
|
|
array[0..cp] of var bool: ts } in
|
|
binary_sum(f, fs) /\ binary_sum(t, ts) /\
|
|
binary_add(fs, ts, b, s)
|
|
endif;
|
|
|
|
% 把两个二元数值 x 和 y 加起来，位 ci 用来表示进位，来得到二元 s
|
|
predicate binary_add(array[int] of var bool: x,
|
|
array[int] of var bool: y,
|
|
var bool: ci,
|
|
array[int] of var bool: s) =
|
|
let { int:l = length(x),
|
|
int:n = length(s), } in
|
|
assert(l == length(y),
|
|
"length of binary_add input args must be same",
|
|
assert(n == l \/ n == l+1, "length of binary_add output " ++
|
|
"must be equal or one more than inputs",
|
|
let { array[0..l] of var bool: c } in
|
|
full_adder(x[0], y[0], ci, s[0], c[0]) /\
|
|
forall(i in 1..l)(full_adder(x[i], y[i], c[i-1], s[i], c[i])) /\
|
|
if n > l then s[n] = c[l] else c[l] == false endif ));
|
|
|
|
predicate full_adder(var bool: x, var bool: y, var bool: ci,
|
|
var bool: s, var bool: co) =
|
|
let { var bool: xy = x xor y } in
|
|
s = (xy xor ci) /\ co = ((x /\ y) \/ (ci /\ xy));
|