var1 $;
# implicit constraints in every quantifier.
defaultwhere1(p) = p <= $;
defaultwhere2(P) = P sub {0,...,$};
pred at_least_two(var0 A,var0 B,var0 C) =
(A & B) | (A & C) | (B & C);
pred mod_two(var0 A,var0 B,var0 C,var0 @d) = (A <=> B <=> C <=> @d);
# "high-level" description of the addition of Cin (carry in) and vectors X
# and Y with result Z and Cout (carry out); all vectors have length $+1
# and LSB is in position 0 (so LSB is set in X iff 0 in X)
pred add(var2 X, var2 Y, var2 Result, var0 Cin, var0 Cout) =
ex2 C: (0 in C <=> Cin)
& (all1 i:
mod_two(i in X, i in Y, i in C, i in Result)
& (i < $ => ((i+1 in C)
<=> at_least_two(i in X, i in Y, i in C))))
& (Cout <=> at_least_two($ in X, $ in Y, $ in C));
# a "synchronous" adder where carry is computed independently. We get a
# carry at position i if either i=0 and Cin is asserted or else a carry
# was manifestly generated at some earlier position j and never swallowed
# in the meantime (k).
pred sync_add(var2 X, var2 Y, var2 Result, var0 Cin, Cout) =
ex2 C:
(all1 i:i in C <=> i=0 & Cin |
ex1 j: j* k in X | k in Y) &
at_least_two(j in X, j in Y, j=0&Cin)) &
(all1 p: mod_two(p in X, p in Y, p in C, p in Result)) &
(Cout <=> at_least_two($ in X, $ in Y, $ in C));
all2 X,Y,Z: all0 Cin, Cout:
add(X,Y,Z,Cin,Cout) <=> sync_add(X,Y,Z,Cin,Cout);
*