# 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

# less-than relation (p "<" q)
pred less(var2 p,q) =
   ex2 t: t ~= empty & plus(p,t,q);
pred leq(var2 p,q) =
   ex2 t: plus(p,t,q);


pred plusar3(var2 x1,x2,x3,x4) = ex2 c: plus(x1,x2,c) & plus(c,x3,x4);
pred plusar4(var2 x1,x2,x3,x4,x5) = ex2 c: plusar3(x1,x2,x3,c) & plus(c,x4,x5);

macro shift(var2 p,q) = plus(p,p,q);
macro shift2(var2 p,q) = ex2 t: shift(p,t) & shift(t,q);
macro shift3(var2 p,q) = ex2 t: shift2(p,t) & shift(t,q);

macro time7(var2 p,q) =
   ex2 t1,t2: shift(p,t1) & shift(t1,t2) & plusar3(p,t1,t2,q);
macro time8(var2 p,q) = shift3(p,q);

macro christmas(var2 elines, ilines, isyls, nsyls, line7, line8,
nslines, nlines, tlines) =
   plus(elines,nlines,tlines) &
   plus(ilines,nslines,nlines) &
   plus(line7,line8,nlines) &
   (ex2 t7,t8,s: time7(line7,t7) & time8(line8,t8) &
plus(nsyls,isyls,s) & plus(t7,t8,s)) &
   (ex2 tlinesfact: shift2(tlinesfact,tlines)) &
   leq(pconst(0),line8) &
   leq(pconst(0),line7) &
   leq(pconst(0), tlines);

ex2 elines, ilines, isyls, nsyls, line7, line8: ex2 nslines, nlines, tlines: christmas(elines, ilines, isyls, nsyls, line7, line8, nslines, nlines, tlines);