# MONA Presburger predicates

# auxiliary predicates
pred xor(var0 x,y) = x&~y | ~x&y;
pred at_least_two(var0 x,y,z) = x&y | x&z | y&z;

# addition relation (p "+" q = r)
pred plus(var2 p,q,r) =
 ex2 c:                                                  # carry track
   0 notin c                                             # no carry-in
 & all1 t:
     (t+1 in c <=> at_least_two(t in p, t in q, t in c)) # propagate carry
   & (t in r <=> xor(xor(t in p, t in q), t in c));      # calculate result

ex2 x, y, z: plus(x,y,z);