1 #include "math/dd/dd_pdd.h"
2
3 namespace dd {
4
5 class test {
6 public :
7
hello_world()8 static void hello_world() {
9 pdd_manager m(3);
10 pdd v0 = m.mk_var(0);
11 pdd v1 = m.mk_var(1);
12 pdd v2 = m.mk_var(2);
13 std::cout << v0 << "\n";
14 std::cout << v1 << "\n";
15 std::cout << v2 << "\n";
16 pdd c1 = v0 * v1 * v2;
17 pdd c2 = v2 * v0 * v1;
18 std::cout << c1 << "\n";
19 VERIFY(c1 == c2);
20
21 c1 = v0 + v1 + v2;
22 c2 = v2 + v1 + v0;
23 std::cout << c1 << "\n";
24 VERIFY(c1 == c2);
25
26 c1 = (v0+v1) * v2;
27 c2 = (v0*v2) + (v1*v2);
28 std::cout << c1 << "\n";
29 VERIFY(c1 == c2);
30 c1 = (c1 + 3) + 1;
31 c2 = (c2 + 1) + 3;
32 std::cout << c1 << "\n";
33 VERIFY(c1 == c2);
34 c1 = v0 - v1;
35 c2 = v1 - v0;
36 std::cout << c1 << " " << c2 << "\n";
37
38 c1 = v1*v2;
39 c2 = (v0*v2) + (v2*v2);
40 pdd c3 = m.zero();
41 VERIFY(m.try_spoly(c1, c2, c3));
42 std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
43
44 c1 = v1*v2;
45 c2 = (v0*v2) + (v1*v1);
46 VERIFY(m.try_spoly(c1, c2, c3));
47 std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
48
49 c1 = (v0*v1) - (v0*v0);
50 c2 = (v0*v1*(v2 + v0)) + v2;
51 c3 = c2.reduce(c1);
52 std::cout << c1 << " " << c2 << " reduce: " << c3 << "\n";
53 VERIFY(c3 == c3.reduce(c1));
54 }
55
reduce()56 static void reduce() {
57 std::cout << "\nreduce\n";
58 // a(b^2)cd + abc + bcd + bc + cd + 3 reduce by bc
59 pdd_manager m(4);
60 pdd a = m.mk_var(0);
61 pdd b = m.mk_var(1);
62 pdd c = m.mk_var(2);
63 pdd d = m.mk_var(3);
64 pdd e = (a * b * b * c * d) + (2*a*b*c) + (b*c*d) + (b*c) + (c*d) + 3;
65 std::cout << e << "\n";
66 pdd f = b * c;
67 pdd r_ef = m.reduce(e, f);
68 m.display(std::cout);
69 std::cout << "result of reduce " << e << " by " << f << " is " << r_ef << "\n";
70 VERIFY(r_ef == (c*d) + 3);
71 pdd r_fe = m.reduce(f, e);
72 std::cout << "result of reduce " << f << " by " << e << " is " << r_fe << "\n" ;
73 VERIFY(r_fe == f);
74
75 // test that b*c*d is treated as the leading monomial
76 f = b*c*d - d*d;
77 r_ef = m.reduce(e, f);
78 std::cout << "result of reduce " << e << " by " << f << " is " << r_ef << "\n";
79 VERIFY(r_ef == (a*b*d*d) + (2*a*b*c) + (d*d) + (b*c) + (c*d) + 3);
80
81 pdd k = d*d + 3*b;
82 VERIFY(m.reduce(f, k) == b*c*d + 3*b);
83
84 }
85
86
87
large_product()88 static void large_product() {
89 std::cout << "\nlarge_product\n";
90 pdd_manager m(4);
91 pdd a = m.mk_var(0);
92 pdd b = m.mk_var(1);
93 pdd c = m.mk_var(2);
94 pdd d = m.mk_var(3);
95
96 pdd e = a + c;
97 for (unsigned i = 0; i < 5; i++) {
98 e = e * e;
99 }
100 e = e * b;
101 std::cout << e << "\n";
102 }
103
reset()104 static void reset() {
105 std::cout << "\ntest reset\n";
106 pdd_manager m(4);
107 pdd a = m.mk_var(0);
108 pdd b = m.mk_var(1);
109 pdd c = m.mk_var(2);
110 pdd d = m.mk_var(3);
111 std::cout << (a + b)*(c + d) << "\n";
112
113 unsigned_vector l2v;
114 for (unsigned i = 0; i < 4; ++i)
115 l2v.push_back(3 - i);
116 m.reset(l2v);
117 a = m.mk_var(0);
118 b = m.mk_var(1);
119 c = m.mk_var(2);
120 d = m.mk_var(3);
121 std::cout << (a + b)*(c + d) << "\n";
122 }
123
canonize()124 static void canonize() {
125 std::cout << "\ncanonize\n";
126 pdd_manager m(2);
127 pdd a = m.mk_var(0);
128 pdd b = m.mk_var(1);
129
130 pdd e = (a - b) * ( a + b);
131 pdd f = a * a - b * b;
132 VERIFY(e == f);
133
134 e = (a - b)* (a - b);
135 f = a * a - 2 * a * b + b * b;
136 VERIFY(e == f);
137 e = a - 3;
138 e = e * e;
139 f = a * a - 6 * a + 9;
140 VERIFY(e == f);
141 e = 2 * a - 3;
142 e = e * e;
143 f = 4 * a * a - 12 * a + 9;
144 VERIFY(e == f);
145 }
146
147
iterator()148 static void iterator() {
149 std::cout << "test iterator\n";
150 pdd_manager m(4);
151 pdd a = m.mk_var(0);
152 pdd b = m.mk_var(1);
153 pdd c = m.mk_var(2);
154 pdd d = m.mk_var(3);
155 pdd p = (a + b)*(c + 3*d) + 2;
156 std::cout << p << "\n";
157 for (auto const& m : p) {
158 std::cout << m << "\n";
159 }
160 }
order()161 static void order() {
162 std::cout << "order\n";
163 pdd_manager m(4);
164 unsigned va = 0;
165 unsigned vb = 1;
166 unsigned vc = 2;
167 unsigned vd = 3;
168 pdd a = m.mk_var(va);
169 pdd b = m.mk_var(vb);
170 pdd c = m.mk_var(vc);
171 pdd d = m.mk_var(vd);
172 pdd p = a + b;
173 std::cout << p << "\n";
174 unsigned i = 0;
175 for (auto const& m : p) {
176 std::cout << m << "\n";
177 VERIFY(i != 0 ||( m.vars.size() == 1 && m.vars[0] == vb));
178 VERIFY(i != 1 ||( m.vars.size() == 1 && m.vars[0] == va));
179 i++;
180 }
181 pdd ccbbaa = c*c*b*b*a*a;
182 pdd ccbbba = c*c*b*b*b*a;
183 p = ccbbaa + ccbbba;
184
185 i = 0;
186 std::cout << "p = " << p << "\n";
187 for (auto const& m : p) {
188 std::cout << m << "\n";
189 VERIFY(i != 0 ||( m.vars.size() == 6 && m.vars[4] == vb)); // the first one has to be ccbbba
190 VERIFY(i != 1 ||( m.vars.size() == 6 && m.vars[4] == va)); // the second one has to be ccbbaa
191 i++;
192 }
193 pdd dcbba = d*c*b*b*a;
194 pdd dd = d * d;
195 p = dcbba + ccbbba + dd;
196 vector<unsigned> v;
197 std::cout << "p = " << p << "\n";
198 unsigned k = p.index();
199 std::cout << "pdd(k) = " << pdd(k, m) << "\n";
200 k = m.first_leading(k);
201 do {
202 if (m.is_val(k)) {
203 VERIFY(m.val(k).is_one());
204 break;
205 }
206 v.push_back(m.var(k));
207 std::cout << "pdd(k) = " << pdd(k, m) << "\n";
208 std::cout << "push v" << m.var(k) << "\n";
209 k = m.next_leading(k);
210 } while(true);
211 auto it = v.begin();
212 std::cout << "v" << *it;
213 it++;
214 for( ; it != v.end(); it ++) {
215 std::cout << "*v" << *it;
216 }
217 VERIFY(v.size() == 6);
218 VERIFY(v[0] == vc);
219 std::cout << "\n";
220 v.reset();
221 p = d*c*c*d + b*c*c*b + d*d*d;
222 k = p.index();
223 std::cout << "pdd(k) = " << pdd(k, m) << "\n";
224 k = m.first_leading(k);
225 do {
226 if (m.is_val(k)) {
227 VERIFY(m.val(k).is_one());
228 break;
229 }
230 v.push_back(m.var(k));
231 std::cout << "pdd(k) = " << pdd(k, m) << "\n";
232 std::cout << "push v" << m.var(k) << "\n";
233 k = m.next_leading(k);
234 } while(true);
235 it = v.begin();
236 std::cout << "v" << *it;
237 it++;
238 for( ; it != v.end(); it ++) {
239 std::cout << "*v" << *it;
240 }
241 VERIFY(v.size() == 4);
242 VERIFY(v[0] == vd);
243 std::cout << "\n";
244
245 }
order_lm()246 static void order_lm() {
247 std::cout << "order_lm\n";
248 pdd_manager m(4);
249 unsigned va = 0;
250 unsigned vb = 1;
251 unsigned vc = 2;
252 unsigned vd = 3;
253 pdd a = m.mk_var(va);
254 pdd b = m.mk_var(vb);
255 pdd c = m.mk_var(vc);
256 pdd d = m.mk_var(vd);
257 pdd p = a + b;
258 std::cout << p << "\n";
259 unsigned i = 0;
260 for (auto const& m : p) {
261 std::cout << m << "\n";
262 VERIFY(i != 0 ||( m.vars.size() == 1 && m.vars[0] == vb));
263 VERIFY(i != 1 ||( m.vars.size() == 1 && m.vars[0] == va));
264 i++;
265 }
266 pdd ccbbaa = c*c*b*b*a*a;
267 pdd ccbbba = c*c*b*b*b*a;
268 p = ccbbaa + ccbbba;
269
270 i = 0;
271 std::cout << "p = " << p << "\n";
272 for (auto const& m : p) {
273 std::cout << m << "\n";
274 VERIFY(i != 0 ||( m.vars.size() == 6 && m.vars[4] == vb)); // the first one has to be ccbbba
275 VERIFY(i != 1 ||( m.vars.size() == 6 && m.vars[4] == va)); // the second one has to be ccbbaa
276 i++;
277 }
278 pdd dcbba = d*c*b*b*a;
279 pdd dd = d * d;
280 pdd p0 = p + dd;
281 std::cout << p0 << " > " << p << "\n";
282 VERIFY(m.lm_lt(p, p0));
283 VERIFY(m.lm_lt(p0 + a * b, p0 + b * b));
284
285 }
286
287 };
288
289 }
290
tst_pdd()291 void tst_pdd() {
292 dd::test::hello_world();
293 dd::test::reduce();
294 dd::test::large_product();
295 dd::test::canonize();
296 dd::test::reset();
297 dd::test::iterator();
298 dd::test::order();
299 dd::test::order_lm();
300 }
301