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
var2 x,y,z;
plus(x,y,z);
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);
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);
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);
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);
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);
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);
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);
var2 elines, ilines, isyls, nsyls, line7, line8;
ex2 nslines, nlines, tlines:
christmas(elines, ilines, isyls, nsyls, line7, line8, nslines, nlines, tlines);
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);
macro shift(var2 p,q) = plus(p,p,q);
macro time6(var2 p,q) =
ex2 t1,t2: shift(p,t1) & shift(t1,t2) & plus(t1,t2,q);
macro decomp(var2 n,k) =
plus(k,k,n) | plusar3(k,k,k,n) | ex2 t: time6(k,t) & (plus(t,pconst(1),n) | plus(t,pconst(5),n));
var2 n,k;
decomp(n,k);
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);
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 plusleq(var2 p,q,r) = ex2 t: plus(p,q,t) & leq(t,r);
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);
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 times10(var2 p,q) = ex2 t: times9(p,t) & plus(p,t,q);
#-------------------------------------------
# 5*x1 + 3*x2 <= food1
# 2*x1 + 3*x2 <= food2
# price x1 = 8
# price x2 = 4
#-------------------------------------------
macro constraints(var2 x1,x2,food1,food2) =
ex2 x1times2, x1times5, x2times3:
times2(x1,x1times2) & times3(x2,x2times3) & times5(x1, x1times5) &
plusleq(x1times5, x2times3, food1) &
plusleq(x1times2, x2times3, food2);
macro cost(var2 x1, x2, c) =
ex2 x1times8, x2times4:
times8(x1,x1times8) & times4(x2,x2times4) & plus(x1times8,x2times4,c);
macro maximize(var2 x1,x2,food1,food2) =
all2 y1, y2:
~constraints(y1,y2,food1,food2) |
(ex2 cx,cy: cost(x1,x2,cx) & cost(y1,y2,cy) & leq(cy,cx));
#var2 food1,food2,x1,x2;
#constraints(x1,x2,food1,food2) & maximize(x1,x2,food1,food2);
#-------------------------------------------
# 2*x1 + x2 <= food1
# x1 + x2 <= food2
# price x1 = 4
# price x2 = 3
#-------------------------------------------
macro constraints2(var2 x1,x2,food1,food2) =
ex2 x1times2:
times2(x1,x1times2) &
plusleq(x1times2,x2,food1) &
plusleq(x1,x2,food2);
macro cost2(var2 x1,x2,c) =
ex2 x1times4,x2times3:
times4(x1,x1times4) &
times3(x2,x2times3) &
plus(x1times4,x2times3,c);
macro maximize2(var2 x1,x2,food1,food2) =
all2 y1, y2: ~constraints2(y1,y2,food1,food2) |
(ex2 cx,cy: cost2(x1,x2,cx) & cost2(y1,y2,cy) & leq(cy,cx));
#var2 food1,food2,x1,x2;
#constraints2(x1,x2,food1,food2) & maximize2(x1,x2,food1,food2);
#-------------------------------------------
# 4*x1 + 1*x2 <= food1
# 2*x1 + 3*x2 <= food2 3*x1 + 3*x2 <= food2
# price x1 = 8 or 6 or 9
# price x2 = 6 or 4 or 6
# out of memory on prime numbers, e.g, (5,3)
# (1000,9000,0,1000)
# (2000,8000,0,2000)
# (3000,7000,200,2200)
# (4000,6000,600,1600)
# (5000,5000,1000,1000)
# (6000,4000,1400,400)
# (7000,3000,1500,0)
# (8000,2000,1000,0)
# (9000,1000,500,0)
#-------------------------------------------
#-------------------------------------------
# 4*x1 + 1*x2 <= food1
# 3*x1 + 3*x2 <= food2
# price x1 = 9
# price x2 = 6
# (1000,9000,0,1000)
# (2000,8000,0,2000)
# (3000,7000,222,2111)
# (4000,6000,666,1334)
# (5000,5000,1111,555)
# (6000,4000,1333,0)
# (7000,3000,1000,0)
# (8000,2000,666,0)
# (9000,1000,333,0)
#-------------------------------------------
pred constraints3(var2 x1,x2,food1,food2) =
ex2 x1food1, x1food2, x2food2:
times4(x1,x1food1) &
times2(x1,x1food2) &
times3(x2,x2food2) &
plusleq(x1food1, x2, food1) &
plusleq(x1food2, x2food2, food2);
pred cost3(var2 x1, x2, c) =
ex2 x1price, x2price:
times9(x1,x1price) &
times6(x2,x2price) & plus(x1price,x2price,c);
macro maximize3(var2 x1,x2,food1,food2) =
all2 y1, y2:
~constraints3(y1,y2,food1,food2) |
(ex2 cx,cy: cost3(x1,x2,cx) & cost3(y1,y2,cy) & leq(cy,cx));
var2 food1,food2,x1,x2;
constraints3(x1,x2,food1,food2) & maximize3(x1,x2,food1,food2);
