1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
# 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);
# times-2 relation (p = q "*2")
pred times_two(var2 p,q) =
plus(q,q,p);
# export some automata
var2 p, q, r;
execute export("presburger_plus_012.dfa", plus(p,q,r)); # 012 denotes variable ordering
execute export("presburger_less_01.dfa", less(p,q));
execute export("presburger_timestwo_01.dfa", times_two(p,q));
execute export("presburger_const42.dfa", p = pconst(42));
|
