This is an old revision of the document!

Regsy - Examples

Addition

# 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
 
var2 x,y,z;
plus(x,y,z);

Four-Weigths

unfold

# 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);
pred plusar5(var2 x1,x2,x3,x4,x5,x6) = ex2 c: plusar4(x1,x2,x3,x4,c) & plus(c,x5,x6);
 
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 time3(var2 p,q) =
  ex2 t: shift(p,t) & plus(p,t,q);
 
macro time9(var2 p,q) =
  ex2 t: shift3(p,t) & plus(p,t,q);
 
macro time27(var2 p,q) =
  ex2 t1,t2,t3: shift(p,t1) & shift2(t1,t2) & shift(t2,t3) & plusar4(p,t1,t2,t3,q);
 
macro weight(var2 w, w1, w2, w3, w4) =
  leq(w1,pconst(2)) &
  leq(w2,pconst(2)) &
  leq(w3,pconst(2)) &
  ex2 t2,t3,t4,s:
  time3(w2,t2)  &
  time9(w3,t3)  &
  time27(w4,t4) &
  plusar4(w1,t2,t3,t4,s) & plus(w,pconst(40),s);
 
var2 w,w1,w2,w3,w4;
weight(w, w1, w2, w3, w4);

Three-Weigths-Minimisation

unfold

# 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);
pred plusar5(var2 x1,x2,x3,x4,x5,x6) = ex2 c: plusar4(x1,x2,x3,x4,c) & plus(c,x5,x6);
pred plusar6(var2 x1,x2,x3,x4,x5,x6,x7) = ex2 c: plusar5(x1,x2,x3,x4,x5,c) & plus(c,x6,x7);
 
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 time3(var2 p,q) =
  ex2 t: shift(p,t) & plus(p,t,q);
 
macro time9(var2 p,q) =
  ex2 t: shift3(p,t) & plus(p,t,q);
 
macro time27(var2 p,q) =
  ex2 t1,t2,t3: shift(p,t1) & shift2(t1,t2) & shift(t2,t3) & plusar4(p,t1,t2,t3,q);
 
macro sumleq1(var2 wl, wr) =
  ex2 s: plus(wl,wr,s) & leq(s,pconst(1));
 
 
macro weight(var2 w, w1l, w2l, w3l, w1r, w2r, w3r) =
  ex2 l2,l3,r2,r3,s:
  time3(w2l,l2)   & time3(w2r,r2) &
  time9(w3l,l3)   & time9(w3r,r3) &
  plusar3(w1l,l2,l3,s) & plusar4(w1r,r2,r3,w,s);
 
macro mutualExclusion(var2 w1l, w2l, w3l, w1r, w2r, w3r) =
  (w1l = pconst(0) | w1r = pconst(0)) &
  (w2l = pconst(0) | w2r = pconst(0)) &
  (w3l = pconst(0) | w3r = pconst(0));
 
macro bounded(var2 w1l, w2l, w3l, w1r, w2r, w3r) =
  sumleq1(w1l,w1r) &
  sumleq1(w2l,w2r) &
  sumleq1(w3l,w3r);
 
macro minimize(var2 w, w1l, w2l, w3l, w1r, w2r, w3r) = 
  all2 v1l, v2l, v3l, v1r, v2r, v3r:
   ~weight(w,v1l, v2l, v3l, v1r, v2r, v3r) |
	~(ex2 sv,sw: plusar6(v1l, v2l, v3l, v1r, v2r, v3r, sv) &
	             plusar6(w1l, w2l, w3l, w1r, w2r, w3r, sw) &
                     less(sv,sw));
 
var2 w, w1l, w2l, w3l, w1r, w2r, w3r;
  true
# & bounded(w1l, w2l, w3l, w1r, w2r, w3r)
# & mutualExclusion(w1l, w2l, w3l, w1r, w2r, w3r)
  & minimize(w, w1l, w2l, w3l, w1r, w2r, w3r)
  & weight(w, w1l, w2l, w3l, w1r, w2r, w3r);

Approximation

unfold

# 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);
 
# multiplication with constants
pred times1(var2 p,q) = (p=q);
pred times2(var2 p,q) = plus(p,p,q);
pred times3(var2 p,q) = ex2 t: times2(p,t) & plus(p,t,q);
pred times4(var2 p,q) = ex2 t: times3(p,t) & plus(p,t,q);
pred times5(var2 p,q) = ex2 t: times4(p,t) & plus(p,t,q);
pred times6(var2 p,q) = ex2 t: times5(p,t) & plus(p,t,q);
pred times7(var2 p,q) = ex2 t: times6(p,t) & plus(p,t,q);
pred times8(var2 p,q) = ex2 t: times7(p,t) & plus(p,t,q);
pred times9(var2 p,q) = ex2 t: times8(p,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 approxEq(var2 x,y,err) = plus(x,err,y) | plus(y,err,x);
 
macro spec(var2 x,y,z,err)=
  ex2 xtimes6,ytimes9: 
    times6(x,xtimes6) & 
    times9(y,ytimes9) & 
    ex2 s: plus(xtimes6,ytimes9,s) & approxEq(s,z,err);
 
macro minispecZ(var2 x,y,z,err) =
  spec(x,y,z,err) &
  all2 err',x',y':  ~spec(x',y',z,err') | leq(err,err');
 
var2 x,y,z,err;
minispecZ(x,y,z,err);

Syracuse unfolding

unfold

# 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;
 
pred even(var2 x) = (0 notin x);
 
# 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 shiftl(var2 p,q) =
  all1 t: ((t+1 in p) <=> (t in q));
 
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);
 
pred times1(var2 p,q) = (p=q);
pred times2(var2 p,q) = shift(p,q);
pred times3(var2 p,q) = ex2 t: times2(p,t) & plus(p,t,q);
 
macro step(var2 x,y) = 
  (even(x) & shiftl(x,y)) |
  (~even(x) & (ex2 x3: times3(x,x3) & plus(x3,pconst(1),y)));
 
macro step2(var2 x,y) =
  ex2 z: step(x,z) & step(z,y);
 
macro step3(var2 x,y) =
  ex2 z: step2(x,z) & step(z,y);
 
macro step6(var2 x,y) =
  ex2 z: step3(x,z) & step3(z,y);
 
var2 x,y;
step6(x,y);

Smoothing

unfold

# 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);
 
pred shiftback(var2 x,y) =
  all1 i: i in y <=> (i + 2) in x;
 
pred closed(var2 s) = all1 x: (x + 4) in s => x in s;
pred divisibleBy4(var1 i) = all2 s: (i in s & closed(s)) => 0 in s;
pred createNumber(var0 b0,b1,b2,b3, var2 n) =
  (b0 <=> 0 in n) &
  (b1 <=> 1 in n) &
  (b2 <=> 2 in n) &
  (b3 <=> 3 in n) &
  all1 i: i > 3 => i notin n;
 
pred smoothing(var2 a,b) =
  0 notin b & 1 notin b & 2 notin b & 3 notin b &
  all1 i: divisibleBy4(i) => (
    ex2 x,y,z,t,tDiv4:
    ex0 x0,x1,x2,x3,y0,y1,y2,y3,z0,z1,z2,z3,t0,t1,t2,t3:
      (x0 <=> i in a) &
      (x1 <=> (i+1) in a) &
      (x2 <=> (i+2) in a) &
      (x3 <=> (i+3) in a) &
      (y0 <=> (i+4) in a) &
      (y1 <=> (i+5) in a) &
      (y2 <=> (i+6) in a) &
      (y3 <=> (i+7) in a) &
      (z0 <=> (i+8) in a) &
      (z1 <=> (i+9) in a) &
      (z2 <=> (i+10) in a) &
      (z3 <=> (i+11) in a) &
      createNumber(x0,x1,x2,x3,x) &
      createNumber(y0,y1,y2,y3,y) &
      createNumber(z0,z1,z2,z3,z) &
      plusar4(x,y,y,z,t) &
      shiftback(t,tDiv4) &
      createNumber(t0,t1,t2,t3,tDiv4) &
      (t0 <=> (i+4) in b) &
      (t1 <=> (i+5) in b) &
      (t2 <=> (i+6) in b) &
      (t3 <=> (i+7) in b)
  );
 
var2 a,b;
smoothing(a,b);