1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 grobner.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2008-12-04.
15
16 Revision History:
17
18 --*/
19 #include "math/grobner/grobner.h"
20 #include "ast/ast_pp.h"
21 #include "ast/ast_ll_pp.h"
22 #include "util/ref_util.h"
23
24 // #define PROFILE_GB
25
grobner(ast_manager & m,v_dependency_manager & d)26 grobner::grobner(ast_manager & m, v_dependency_manager & d):
27 m_manager(m),
28 m_dep_manager(d),
29 m_util(m),
30 m_var_lt(m_var2weight),
31 m_monomial_lt(m_var_lt),
32 m_changed_leading_term(false),
33 m_unsat(nullptr) {
34 }
35
~grobner()36 grobner::~grobner() {
37 flush();
38 }
39
flush()40 void grobner::flush() {
41 dec_ref_map_keys(m_manager, m_var2weight);
42 del_equations(0);
43 }
44
del_equations(unsigned old_size)45 void grobner::del_equations(unsigned old_size) {
46 SASSERT(m_equations_to_delete.size() >= old_size);
47 equation_vector::iterator it = m_equations_to_delete.begin();
48 equation_vector::iterator end = m_equations_to_delete.end();
49 it += old_size;
50 for (; it != end; ++it) {
51 equation * eq = *it;
52 if (eq)
53 del_equation(eq);
54 }
55 m_equations_to_delete.shrink(old_size);
56 }
57
del_equation(equation * eq)58 void grobner::del_equation(equation * eq) {
59 m_processed.erase(eq);
60 m_to_process.erase(eq);
61 SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
62 m_equations_to_delete[eq->m_bidx] = 0;
63 del_monomials(eq->m_monomials);
64 dealloc(eq);
65 }
66
del_monomials(ptr_vector<monomial> & ms)67 void grobner::del_monomials(ptr_vector<monomial>& ms) {
68 for (auto& m : ms) {
69 del_monomial(m);
70 }
71 ms.reset();
72 }
73
del_monomial(monomial * m)74 void grobner::del_monomial(monomial * m) {
75 for (expr * v : m->m_vars) {
76 m_manager.dec_ref(v);
77 }
78 dealloc(m);
79 }
80
unfreeze_equations(unsigned old_size)81 void grobner::unfreeze_equations(unsigned old_size) {
82 SASSERT(m_equations_to_unfreeze.size() >= old_size);
83 equation_vector::iterator it = m_equations_to_unfreeze.begin();
84 equation_vector::iterator end = m_equations_to_unfreeze.end();
85 it += old_size;
86 for (; it != end; ++it) {
87 equation * eq = *it;
88 m_to_process.insert(eq);
89 }
90 m_equations_to_unfreeze.shrink(old_size);
91 }
92
push_scope()93 void grobner::push_scope() {
94 m_scopes.push_back(scope());
95 scope & s = m_scopes.back();
96 s.m_equations_to_unfreeze_lim = m_equations_to_unfreeze.size();
97 s.m_equations_to_delete_lim = m_equations_to_delete.size();
98 }
99
pop_scope(unsigned num_scopes)100 void grobner::pop_scope(unsigned num_scopes) {
101 SASSERT(num_scopes >= get_scope_level());
102 unsigned new_lvl = get_scope_level() - num_scopes;
103 scope & s = m_scopes[new_lvl];
104 unfreeze_equations(s.m_equations_to_unfreeze_lim);
105 del_equations(s.m_equations_to_delete_lim);
106 m_scopes.shrink(new_lvl);
107 }
108
reset()109 void grobner::reset() {
110 flush();
111 m_processed.reset();
112 m_to_process.reset();
113 m_equations_to_unfreeze.reset();
114 m_equations_to_delete.reset();
115 m_unsat = nullptr;
116 }
117
display_var(std::ostream & out,expr * var) const118 void grobner::display_var(std::ostream & out, expr * var) const {
119 if (is_app(var) && to_app(var)->get_num_args() > 0)
120 out << mk_bounded_pp(var, m_manager);
121 else
122 out << mk_pp(var, m_manager);
123 }
124
display_vars(std::ostream & out,unsigned num_vars,expr * const * vars) const125 void grobner::display_vars(std::ostream & out, unsigned num_vars, expr * const * vars) const {
126 for (unsigned i = 0; i < num_vars; i++) {
127 display_var(out, vars[i]);
128 out << " ";
129 }
130 }
131
display_monomial(std::ostream & out,monomial const & m) const132 void grobner::display_monomial(std::ostream & out, monomial const & m) const {
133 if (!m.m_coeff.is_one() || m.m_vars.empty()) {
134 out << m.m_coeff;
135 if (!m.m_vars.empty())
136 out << "*";
137 }
138
139 if (!m.m_vars.empty()) {
140 ptr_vector<expr>::const_iterator it = m.m_vars.begin();
141 ptr_vector<expr>::const_iterator end = m.m_vars.end();
142 unsigned power = 1;
143 expr * prev = *it;
144 it++;
145 for (; it != end; ++it) {
146 expr * curr = *it;
147 if (curr == prev) {
148 power++;
149 }
150 else {
151 display_var(out, prev);
152 if (power > 1)
153 out << "^" << power;
154 power = 1;
155 prev = curr;
156 out << "*";
157 }
158 }
159 display_var(out, prev);
160 if (power > 1)
161 out << "^" << power;
162 }
163 }
164
display_monomials(std::ostream & out,unsigned num_monomials,monomial * const * monomials) const165 void grobner::display_monomials(std::ostream & out, unsigned num_monomials, monomial * const * monomials) const {
166 bool first = true;
167 for (unsigned i = 0; i < num_monomials; i++) {
168 monomial const * m = monomials[i];
169 if (first)
170 first = false;
171 else
172 out << " + ";
173 display_monomial(out, *m);
174 }
175 }
176
display_equation(std::ostream & out,equation const & eq) const177 void grobner::display_equation(std::ostream & out, equation const & eq) const {
178 display_monomials(out, eq.m_monomials.size(), eq.m_monomials.data());
179 out << " = 0\n";
180 }
181
display_equations(std::ostream & out,equation_set const & v,char const * header) const182 void grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const {
183 if (!v.empty()) {
184 out << header << "\n";
185 for (equation const* eq : v)
186 display_equation(out, *eq);
187 }
188 }
189
display(std::ostream & out) const190 void grobner::display(std::ostream & out) const {
191 display_equations(out, m_processed, "processed:");
192 display_equations(out, m_to_process, "to process:");
193 }
194
set_weight(expr * n,int weight)195 void grobner::set_weight(expr * n, int weight) {
196 if (weight == 0)
197 return;
198 if (!m_var2weight.contains(n))
199 m_manager.inc_ref(n);
200 m_var2weight.insert(n, weight);
201 }
202
203 /**
204 \brief Update equation using the new variable order.
205 Return true if the leading term was modified.
206 */
update_order(equation * eq)207 bool grobner::update_order(equation * eq) {
208 if (eq->get_num_monomials() == 0)
209 return false;
210 monomial * first = eq->m_monomials[0];
211 for (monomial* m : eq->m_monomials) {
212 std::stable_sort(m->m_vars.begin(), m->m_vars.end(), m_var_lt);
213 }
214 std::stable_sort(eq->m_monomials.begin(), eq->m_monomials.end(), m_monomial_lt);
215 return eq->m_monomials[0] != first;
216 }
217
update_order(equation_set & s,bool processed)218 void grobner::update_order(equation_set & s, bool processed) {
219 ptr_buffer<equation> to_remove;
220 for (equation * eq : s) {
221 if (update_order(eq)) {
222 if (processed) {
223 to_remove.push_back(eq);
224 m_to_process.insert(eq);
225 }
226 }
227 }
228 for (equation* e : to_remove)
229 s.erase(e);
230 }
231
update_order()232 void grobner::update_order() {
233 update_order(m_to_process, false);
234 update_order(m_processed, true);
235 }
236
operator ()(expr * v1,expr * v2) const237 bool grobner::var_lt::operator()(expr * v1, expr * v2) const {
238 if (v1 == v2) return false;
239 int w1 = 0;
240 int w2 = 0;
241 m_var2weight.find(v1, w1);
242 m_var2weight.find(v2, w2);
243 return (w1 > w2) || (w1 == w2 && v1->get_id() < v2->get_id());
244 }
245
operator ()(monomial * m1,monomial * m2) const246 bool grobner::monomial_lt::operator()(monomial * m1, monomial * m2) const {
247 // Using graded lex order.
248 if (m1->get_degree() > m2->get_degree())
249 return true;
250 if (m1->get_degree() < m2->get_degree())
251 return false;
252 ptr_vector<expr>::iterator it1 = m1->m_vars.begin();
253 ptr_vector<expr>::iterator it2 = m2->m_vars.begin();
254 ptr_vector<expr>::iterator end1 = m1->m_vars.end();
255 for (; it1 != end1; ++it1, ++it2) {
256 expr * v1 = *it1;
257 expr * v2 = *it2;
258 if (v1 == v2)
259 continue;
260 if (m_var_lt(v1, v2))
261 return true;
262 if (v1 != v2)
263 return false;
264 }
265 return false;
266 }
267
add_var(monomial * m,expr * v)268 inline void grobner::add_var(monomial * m, expr * v) {
269 SASSERT(!m_util.is_numeral(v));
270 m_manager.inc_ref(v);
271 m->m_vars.push_back(v);
272 }
273
mk_monomial(rational const & coeff,unsigned num_vars,expr * const * vars)274 grobner::monomial * grobner::mk_monomial(rational const & coeff, unsigned num_vars, expr * const * vars) {
275 monomial * r = alloc(monomial);
276 r->m_coeff = coeff;
277 for (unsigned i = 0; i < num_vars; i++)
278 add_var(r, vars[i]);
279 std::stable_sort(r->m_vars.begin(), r->m_vars.end(), m_var_lt);
280 return r;
281 }
282
mk_monomial(rational const & coeff,expr * m)283 grobner::monomial * grobner::mk_monomial(rational const & coeff, expr * m) {
284 monomial * r = alloc(monomial);
285 if (m_util.is_numeral(m, r->m_coeff)) {
286 r->m_coeff *= coeff;
287 return r;
288 }
289 if (m_util.is_mul(m)) {
290 expr * body = m;
291 SASSERT(!m_util.is_numeral(to_app(m)->get_arg(1))); // monomial is in normal form
292 if (m_util.is_numeral(to_app(m)->get_arg(0), r->m_coeff)) {
293 r->m_coeff *= coeff;
294 body = to_app(m)->get_arg(1);
295 }
296 else {
297 r->m_coeff = coeff;
298 }
299 while (m_util.is_mul(body)) {
300 add_var(r, to_app(body)->get_arg(0));
301 body = to_app(body)->get_arg(1);
302 }
303 add_var(r, body);
304 std::stable_sort(r->m_vars.begin(), r->m_vars.end(), m_var_lt);
305 }
306 else {
307 r->m_coeff = coeff;
308 r->m_vars.push_back(m);
309 m_manager.inc_ref(m);
310 }
311 return r;
312 }
313
init_equation(equation * eq,v_dependency * d)314 void grobner::init_equation(equation * eq, v_dependency * d) {
315 eq->m_scope_lvl = get_scope_level();
316 unsigned bidx = m_equations_to_delete.size();
317 eq->m_bidx = bidx;
318 eq->m_dep = d;
319 eq->m_lc = true;
320 m_equations_to_delete.push_back(eq);
321 SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
322 }
323
assert_eq_0(unsigned num_monomials,monomial * const * monomials,v_dependency * ex)324 void grobner::assert_eq_0(unsigned num_monomials, monomial * const * monomials, v_dependency * ex) {
325 ptr_vector<monomial> ms;
326 ms.append(num_monomials, monomials);
327 std::stable_sort(ms.begin(), ms.end(), m_monomial_lt);
328 merge_monomials(ms);
329 if (!ms.empty()) {
330 normalize_coeff(ms);
331 equation * eq = alloc(equation);
332 eq->m_monomials.swap(ms);
333 init_equation(eq, ex);
334 m_to_process.insert(eq);
335 }
336 }
337
assert_eq_0(unsigned num_monomials,rational const * coeffs,expr * const * monomials,v_dependency * ex)338 void grobner::assert_eq_0(unsigned num_monomials, rational const * coeffs, expr * const * monomials, v_dependency * ex) {
339 #define MK_EQ(COEFF) \
340 ptr_vector<monomial> ms; \
341 for (unsigned i = 0; i < num_monomials; i++) \
342 ms.push_back(mk_monomial(COEFF, monomials[i])); \
343 std::stable_sort(ms.begin(), ms.end(), m_monomial_lt); \
344 merge_monomials(ms); \
345 if (!ms.empty()) { \
346 equation * eq = alloc(equation); \
347 normalize_coeff(ms); \
348 eq->m_monomials.swap(ms); \
349 init_equation(eq, ex); \
350 m_to_process.insert(eq); \
351 }
352
353 MK_EQ(coeffs[i]);
354 }
355
assert_eq_0(unsigned num_monomials,expr * const * monomials,v_dependency * ex)356 void grobner::assert_eq_0(unsigned num_monomials, expr * const * monomials, v_dependency * ex) {
357 rational one(1);
358 MK_EQ(one);
359 }
360
extract_monomials(expr * lhs,ptr_buffer<expr> & monomials)361 void grobner::extract_monomials(expr * lhs, ptr_buffer<expr> & monomials) {
362 while (m_util.is_add(lhs)) {
363 SASSERT(!m_util.is_add(to_app(lhs)->get_arg(0)));
364 monomials.push_back(to_app(lhs)->get_arg(0));
365 lhs = to_app(lhs)->get_arg(1);
366 }
367 monomials.push_back(lhs);
368 }
369
assert_eq(expr * eq,v_dependency * ex)370 void grobner::assert_eq(expr * eq, v_dependency * ex) {
371 SASSERT(m_manager.is_eq(eq));
372 expr * lhs = to_app(eq)->get_arg(0);
373 expr * rhs = to_app(eq)->get_arg(1);
374 SASSERT(m_util.is_numeral(rhs));
375 ptr_buffer<expr> monomials;
376 extract_monomials(lhs, monomials);
377 rational c;
378 bool is_int = false;
379 m_util.is_numeral(rhs, c, is_int);
380 expr_ref new_c(m_manager);
381 if (!c.is_zero()) {
382 c.neg();
383 new_c = m_util.mk_numeral(c, is_int);
384 monomials.push_back(new_c);
385 }
386 assert_eq_0(monomials.size(), monomials.data(), ex);
387 }
388
assert_monomial_tautology(expr * m)389 void grobner::assert_monomial_tautology(expr * m) {
390 equation * eq = alloc(equation);
391 eq->m_monomials.push_back(mk_monomial(rational(1), m));
392 // create (quote m)
393 monomial * m1 = alloc(monomial);
394 m1->m_coeff = rational(-1);
395 m_manager.inc_ref(m);
396 m1->m_vars.push_back(m);
397 eq->m_monomials.push_back(m1);
398 normalize_coeff(eq->m_monomials);
399 init_equation(eq, static_cast<v_dependency*>(nullptr)); \
400 m_to_process.insert(eq);
401 }
402
403 /**
404 \brief Return true if the body of m1 and m2 are equal
405 */
is_eq_monomial_body(monomial const * m1,monomial const * m2)406 bool grobner::is_eq_monomial_body(monomial const * m1, monomial const * m2) {
407 if (m1->get_degree() != m2->get_degree())
408 return false;
409 ptr_vector<expr>::const_iterator it1 = m1->m_vars.begin();
410 ptr_vector<expr>::const_iterator it2 = m2->m_vars.begin();
411 ptr_vector<expr>::const_iterator end1 = m1->m_vars.end();
412 for (; it1 != end1; ++it1, ++it2) {
413 expr * v1 = *it1;
414 expr * v2 = *it2;
415 if (v1 != v2)
416 return false;
417 }
418 return true;
419 }
420
421 /**
422 \brief Merge monomials (* c1 m) (* c2 m).
423
424 \remark This method assumes the monomials are sorted.
425 */
merge_monomials(ptr_vector<monomial> & monomials)426 void grobner::merge_monomials(ptr_vector<monomial> & monomials) {
427 TRACE("grobner", tout << "before merging monomials:\n"; display_monomials(tout, monomials.size(), monomials.data()); tout << "\n";);
428 unsigned j = 0;
429 unsigned sz = monomials.size();
430 if (sz == 0)
431 return;
432 SASSERT(&m_del_monomials != &monomials);
433 ptr_vector<monomial>& to_delete = m_del_monomials;
434 to_delete.reset();
435 m_manager.limit().inc(sz);
436 for (unsigned i = 1; i < sz; ++i) {
437 monomial * m1 = monomials[j];
438 monomial * m2 = monomials[i];
439 if (is_eq_monomial_body(m1, m2)) {
440 m1->m_coeff += m2->m_coeff;
441 to_delete.push_back(m2);
442 }
443 else {
444 if (m1->m_coeff.is_zero())
445 to_delete.push_back(m1);
446 else
447 j++;
448 monomials[j] = m2;
449 }
450 }
451 SASSERT(j < sz);
452 monomial * m1 = monomials[j];
453 if (m1->m_coeff.is_zero())
454 to_delete.push_back(m1);
455 else
456 j++;
457 monomials.shrink(j);
458 del_monomials(to_delete);
459 TRACE("grobner", tout << "after merging monomials:\n"; display_monomials(tout, monomials.size(), monomials.data()); tout << "\n";);
460 }
461
462 /**
463 \brief Divide the coefficients by the coefficient of the leading term.
464 */
normalize_coeff(ptr_vector<monomial> & monomials)465 void grobner::normalize_coeff(ptr_vector<monomial> & monomials) {
466 if (monomials.empty())
467 return;
468 rational c = monomials[0]->m_coeff;
469 if (c.is_one())
470 return;
471 unsigned sz = monomials.size();
472 for (unsigned i = 0; i < sz; i++)
473 monomials[i]->m_coeff /= c;
474 }
475
476 /**
477 \brief Simplify the given monomials
478 */
simplify(ptr_vector<monomial> & monomials)479 void grobner::simplify(ptr_vector<monomial> & monomials) {
480 std::stable_sort(monomials.begin(), monomials.end(), m_monomial_lt);
481 merge_monomials(monomials);
482 normalize_coeff(monomials);
483 }
484
485 /**
486 \brief Return true if the equation is of the form k = 0, where k is a numeral different from zero.
487
488 \remark This method assumes the equation is simplified.
489 */
is_inconsistent(equation * eq) const490 inline bool grobner::is_inconsistent(equation * eq) const {
491 SASSERT(!(eq->m_monomials.size() == 1 && eq->m_monomials[0]->get_degree() == 0) || !eq->m_monomials[0]->m_coeff.is_zero());
492 return eq->m_monomials.size() == 1 && eq->m_monomials[0]->get_degree() == 0;
493 }
494
495 /**
496 \brief Return true if the equation is of the form 0 = 0.
497 */
is_trivial(equation * eq) const498 inline bool grobner::is_trivial(equation * eq) const {
499 return eq->m_monomials.empty();
500 }
501
502 /**
503 \brief Sort monomials, and merge monomials with the same body.
504 */
simplify(equation * eq)505 void grobner::simplify(equation * eq) {
506 simplify(eq->m_monomials);
507 if (is_inconsistent(eq) && !m_unsat)
508 m_unsat = eq;
509 }
510
511 /**
512 \brief Return true if monomial m1 is (* c1 M) and m2 is (* c2 M M').
513 Store M' in rest.
514
515 \remark This method assumes the variables of m1 and m2 are sorted.
516 */
is_subset(monomial const * m1,monomial const * m2,ptr_vector<expr> & rest) const517 bool grobner::is_subset(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest) const {
518 unsigned i1 = 0;
519 unsigned i2 = 0;
520 unsigned sz1 = m1->m_vars.size();
521 unsigned sz2 = m2->m_vars.size();
522 if (sz1 <= sz2) {
523 while (true) {
524 if (i1 >= sz1) {
525 for (; i2 < sz2; i2++)
526 rest.push_back(m2->m_vars[i2]);
527 TRACE("grobner",
528 tout << "monomail: "; display_monomial(tout, *m1); tout << " is a subset of ";
529 display_monomial(tout, *m2); tout << "\n";
530 tout << "rest: "; display_vars(tout, rest.size(), rest.data()); tout << "\n";);
531 return true;
532 }
533 if (i2 >= sz2)
534 break;
535 expr * var1 = m1->m_vars[i1];
536 expr * var2 = m2->m_vars[i2];
537 if (var1 == var2) {
538 i1++;
539 i2++;
540 continue;
541 }
542 if (m_var_lt(var2, var1)) {
543 i2++;
544 rest.push_back(var2);
545 continue;
546 }
547 SASSERT(m_var_lt(var1, var2));
548 break;
549 }
550 }
551 // is not subset
552 TRACE("grobner", tout << "monomail: "; display_monomial(tout, *m1); tout << " is not a subset of ";
553 display_monomial(tout, *m2); tout << "\n";);
554 return false;
555 }
556
557 /**
558 \brief Multiply the monomials of source starting at position start_idx by (coeff * vars), and store the resultant monomials
559 at result.
560 */
mul_append(unsigned start_idx,equation const * source,rational const & coeff,ptr_vector<expr> const & vars,ptr_vector<monomial> & result)561 void grobner::mul_append(unsigned start_idx, equation const * source, rational const & coeff, ptr_vector<expr> const & vars, ptr_vector<monomial> & result) {
562 unsigned sz = source->get_num_monomials();
563 for (unsigned i = start_idx; i < sz; i++) {
564 monomial const * m = source->get_monomial(i);
565 monomial * new_m = alloc(monomial);
566 new_m->m_coeff = m->m_coeff;
567 new_m->m_coeff *= coeff;
568 new_m->m_vars.append(m->m_vars.size(), m->m_vars.data());
569 new_m->m_vars.append(vars.size(), vars.data());
570 for (expr* e : new_m->m_vars)
571 m_manager.inc_ref(e);
572 std::stable_sort(new_m->m_vars.begin(), new_m->m_vars.end(), m_var_lt);
573 result.push_back(new_m);
574 }
575 }
576
577 /**
578 \brief Copy the given monomial.
579 */
copy_monomial(monomial const * m)580 grobner::monomial * grobner::copy_monomial(monomial const * m) {
581 monomial * r = alloc(monomial);
582 r->m_coeff = m->m_coeff;
583 for (expr* e : m->m_vars)
584 add_var(r, e);
585 return r;
586 }
587
588 /**
589 \brief Copy the given equation.
590 */
copy_equation(equation const * eq)591 grobner::equation * grobner::copy_equation(equation const * eq) {
592 equation * r = alloc(equation);
593 unsigned sz = eq->get_num_monomials();
594 for (unsigned i = 0; i < sz; i++)
595 r->m_monomials.push_back(copy_monomial(eq->get_monomial(i)));
596 init_equation(r, eq->m_dep);
597 r->m_lc = eq->m_lc;
598 return r;
599 }
600
601 /**
602 \brief Simplify the target equation using the source as a rewrite rule.
603 Return 0 if target was not simplified.
604 Return target if target was simplified but source->m_scope_lvl <= target->m_scope_lvl.
605 Return new_equation if source->m_scope_lvl > target->m_scope_lvl, moreover target is freezed, and new_equation contains the result.
606 */
simplify(equation const * source,equation * target)607 grobner::equation * grobner::simplify(equation const * source, equation * target) {
608 TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source););
609 if (source->get_num_monomials() == 0)
610 return nullptr;
611 m_stats.m_simplify++;
612 bool result = false;
613 bool simplified;
614 do {
615 simplified = false;
616 unsigned i = 0;
617 unsigned j = 0;
618 unsigned sz = target->m_monomials.size();
619 monomial const * LT = source->get_monomial(0);
620 ptr_vector<monomial> & new_monomials = m_tmp_monomials;
621 new_monomials.reset();
622 ptr_vector<expr> & rest = m_tmp_vars1;
623 for (; i < sz; i++) {
624 monomial * curr = target->m_monomials[i];
625 rest.reset();
626 if (is_subset(LT, curr, rest)) {
627 if (i == 0)
628 m_changed_leading_term = true;
629 if (source->m_scope_lvl > target->m_scope_lvl) {
630 target = copy_equation(target);
631 SASSERT(target->m_scope_lvl >= source->m_scope_lvl);
632 }
633 if (!result) {
634 // first time that source is being applied.
635 target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
636 }
637 simplified = true;
638 result = true;
639 rational coeff = curr->m_coeff;
640 coeff /= LT->m_coeff;
641 coeff.neg();
642 if (!rest.empty())
643 target->m_lc = false;
644 mul_append(1, source, coeff, rest, new_monomials);
645 del_monomial(curr);
646 target->m_monomials[i] = 0;
647 }
648 else {
649 target->m_monomials[j] = curr;
650 j++;
651 }
652 }
653 if (simplified) {
654 target->m_monomials.shrink(j);
655 target->m_monomials.append(new_monomials.size(), new_monomials.data());
656 simplify(target);
657 }
658 }
659 while (simplified && m_manager.inc());
660 TRACE("grobner", tout << "result: "; display_equation(tout, *target););
661 return result ? target : nullptr;
662 }
663
664 /**
665 \brief Simplify given equation using processed equalities.
666 Return 0, if the equation was not simplified.
667 Return eq, if the equation was simplified using destructive updates.
668 Return new_eq otherwise.
669 */
simplify_using_processed(equation * eq)670 grobner::equation * grobner::simplify_using_processed(equation * eq) {
671 bool result = false;
672 bool simplified;
673 TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities\n";);
674 do {
675 simplified = false;
676 for (equation const* p : m_processed) {
677 equation * new_eq = simplify(p, eq);
678 if (new_eq) {
679 result = true;
680 simplified = true;
681 eq = new_eq;
682 }
683 if (!m_manager.inc()) {
684 return nullptr;
685 }
686 }
687 }
688 while (simplified);
689 TRACE("grobner", tout << "simplification result: "; display_equation(tout, *eq););
690 return result ? eq : nullptr;
691 }
692
693 /**
694 \brief Return true if eq1 is a better than e2, for being the next equation to be processed.
695 */
is_better_choice(equation * eq1,equation * eq2)696 bool grobner::is_better_choice(equation * eq1, equation * eq2) {
697 if (!eq2)
698 return true;
699 if (eq1->m_monomials.empty())
700 return true;
701 if (eq2->m_monomials.empty())
702 return false;
703 if (eq1->m_monomials[0]->get_degree() < eq2->m_monomials[0]->get_degree())
704 return true;
705 if (eq1->m_monomials[0]->get_degree() > eq2->m_monomials[0]->get_degree())
706 return false;
707 return eq1->m_monomials.size() < eq2->m_monomials.size();
708 }
709
710 /**
711 \brief Pick next unprocessed equation
712 */
pick_next()713 grobner::equation * grobner::pick_next() {
714 equation * r = nullptr;
715 ptr_buffer<equation> to_delete;
716 for (equation * curr : m_to_process) {
717 if (is_trivial(curr))
718 to_delete.push_back(curr);
719 else if (is_better_choice(curr, r))
720 r = curr;
721 }
722 for (equation * e : to_delete)
723 del_equation(e);
724 if (r)
725 m_to_process.erase(r);
726 TRACE("grobner", tout << "selected equation: "; if (!r) tout << "<null>\n"; else display_equation(tout, *r););
727 return r;
728 }
729
730 /**
731 \brief Use the given equation to simplify processed terms.
732 */
simplify_processed(equation * eq)733 bool grobner::simplify_processed(equation * eq) {
734 ptr_buffer<equation> to_insert;
735 ptr_buffer<equation> to_remove;
736 ptr_buffer<equation> to_delete;
737 equation_set::iterator it = m_processed.begin();
738 equation_set::iterator end = m_processed.end();
739 for (; it != end && m_manager.inc(); ++it) {
740 equation * curr = *it;
741 m_changed_leading_term = false;
742 // if the leading term is simplified, then the equation has to be moved to m_to_process
743 equation * new_curr = simplify(eq, curr);
744 if (new_curr != nullptr) {
745 if (new_curr != curr) {
746 m_equations_to_unfreeze.push_back(curr);
747 to_remove.push_back(curr);
748 if (m_changed_leading_term) {
749 m_to_process.insert(new_curr);
750 to_remove.push_back(curr);
751 }
752 else {
753 to_insert.push_back(new_curr);
754 }
755 curr = new_curr;
756 }
757 else {
758 if (m_changed_leading_term) {
759 m_to_process.insert(curr);
760 to_remove.push_back(curr);
761 }
762 }
763 }
764 if (is_trivial(curr))
765 to_delete.push_back(curr);
766 }
767 for (equation* eq : to_insert)
768 m_processed.insert(eq);
769 for (equation* eq : to_remove)
770 m_processed.erase(eq);
771 for (equation* eq : to_delete)
772 del_equation(eq);
773 return m_manager.inc();
774 }
775
776 /**
777 \brief Use the given equation to simplify to-process terms.
778 */
simplify_to_process(equation * eq)779 void grobner::simplify_to_process(equation * eq) {
780 ptr_buffer<equation> to_insert;
781 ptr_buffer<equation> to_remove;
782 ptr_buffer<equation> to_delete;
783 for (equation* curr : m_to_process) {
784 equation * new_curr = simplify(eq, curr);
785 if (new_curr != nullptr && new_curr != curr) {
786 m_equations_to_unfreeze.push_back(curr);
787 to_insert.push_back(new_curr);
788 to_remove.push_back(curr);
789 curr = new_curr;
790 }
791 if (is_trivial(curr))
792 to_delete.push_back(curr);
793 }
794 for (equation* eq : to_insert)
795 m_to_process.insert(eq);
796 for (equation* eq : to_remove)
797 m_to_process.erase(eq);
798 for (equation* eq : to_delete)
799 del_equation(eq);
800 }
801
802 /**
803 \brief If m1 = (* c M M1) and m2 = (* d M M2) and M is non empty, then return true and store M1 in rest1 and M2 in rest2.
804 */
unify(monomial const * m1,monomial const * m2,ptr_vector<expr> & rest1,ptr_vector<expr> & rest2)805 bool grobner::unify(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest1, ptr_vector<expr> & rest2) {
806 TRACE("grobner", tout << "unifying: "; display_monomial(tout, *m1); tout << " "; display_monomial(tout, *m2); tout << "\n";);
807 bool found_M = false;
808 unsigned i1 = 0;
809 unsigned i2 = 0;
810 unsigned sz1 = m1->m_vars.size();
811 unsigned sz2 = m2->m_vars.size();
812 while (true) {
813 if (i1 >= sz1) {
814 if (found_M) {
815 for (; i2 < sz2; i2++)
816 rest2.push_back(m2->m_vars[i2]);
817 return true;
818 }
819 return false;
820 }
821 if (i2 >= sz2) {
822 if (found_M) {
823 for (; i1 < sz1; i1++)
824 rest1.push_back(m1->m_vars[i1]);
825 return true;
826 }
827 return false;
828 }
829 expr * var1 = m1->m_vars[i1];
830 expr * var2 = m2->m_vars[i2];
831 if (var1 == var2) {
832 found_M = true;
833 i1++;
834 i2++;
835 }
836 else if (m_var_lt(var2, var1)) {
837 i2++;
838 rest2.push_back(var2);
839 }
840 else {
841 i1++;
842 rest1.push_back(var1);
843 }
844 }
845 }
846
847 /**
848 \brief Superpose the given two equations.
849 */
superpose(equation * eq1,equation * eq2)850 void grobner::superpose(equation * eq1, equation * eq2) {
851 if (eq1->m_monomials.empty() || eq2->m_monomials.empty())
852 return;
853 m_stats.m_superpose++;
854 ptr_vector<expr> & rest1 = m_tmp_vars1;
855 rest1.reset();
856 ptr_vector<expr> & rest2 = m_tmp_vars2;
857 rest2.reset();
858 if (unify(eq1->m_monomials[0], eq2->m_monomials[0], rest1, rest2)) {
859 TRACE("grobner", tout << "superposing:\n"; display_equation(tout, *eq1); display_equation(tout, *eq2);
860 tout << "rest1: "; display_vars(tout, rest1.size(), rest1.data()); tout << "\n";
861 tout << "rest2: "; display_vars(tout, rest2.size(), rest2.data()); tout << "\n";);
862 ptr_vector<monomial> & new_monomials = m_tmp_monomials;
863 new_monomials.reset();
864 mul_append(1, eq1, eq2->m_monomials[0]->m_coeff, rest2, new_monomials);
865 rational c = eq1->m_monomials[0]->m_coeff;
866 c.neg();
867 mul_append(1, eq2, c, rest1, new_monomials);
868 simplify(new_monomials);
869 TRACE("grobner", tout << "resulting monomials: "; display_monomials(tout, new_monomials.size(), new_monomials.data()); tout << "\n";);
870 if (new_monomials.empty())
871 return;
872 m_num_new_equations++;
873 equation * new_eq = alloc(equation);
874 new_eq->m_monomials.swap(new_monomials);
875 init_equation(new_eq, m_dep_manager.mk_join(eq1->m_dep, eq2->m_dep));
876 new_eq->m_lc = false;
877 m_to_process.insert(new_eq);
878 }
879 }
880
881 /**
882 \brief Superpose the given equations with the equations in m_processed.
883 */
superpose(equation * eq)884 void grobner::superpose(equation * eq) {
885 for (equation * curr : m_processed) {
886 superpose(eq, curr);
887 }
888 }
889
compute_basis_init()890 void grobner::compute_basis_init() {
891 m_stats.m_compute_basis++;
892 m_num_new_equations = 0;
893 }
894
compute_basis_step()895 bool grobner::compute_basis_step() {
896 equation * eq = pick_next();
897 if (!eq)
898 return true;
899 m_stats.m_num_processed++;
900 #ifdef PROFILE_GB
901 if (m_stats.m_num_processed % 100 == 0) {
902 verbose_stream() << "[grobner] " << m_processed.size() << " " << m_to_process.size() << "\n";
903 }
904 #endif
905 equation * new_eq = simplify_using_processed(eq);
906 if (new_eq != nullptr && eq != new_eq) {
907 // equation was updated using non destructive updates
908 m_equations_to_unfreeze.push_back(eq);
909 eq = new_eq;
910 }
911 if (!m_manager.inc()) return false;
912 if (!simplify_processed(eq)) return false;
913 superpose(eq);
914 m_processed.insert(eq);
915 simplify_to_process(eq);
916 TRACE("grobner", tout << "end of iteration:\n"; display(tout););
917 return false;
918 }
919
compute_basis(unsigned threshold)920 bool grobner::compute_basis(unsigned threshold) {
921 compute_basis_init();
922 while (m_num_new_equations < threshold && m_manager.inc()) {
923 if (compute_basis_step()) return true;
924 }
925 return false;
926 }
927
copy_to(equation_set const & s,ptr_vector<equation> & result) const928 void grobner::copy_to(equation_set const & s, ptr_vector<equation> & result) const {
929 for (equation * e : s)
930 result.push_back(e);
931 }
932
933 /**
934 \brief Copy the equations in m_processed and m_to_process to result.
935
936 \warning This equations can be deleted when compute_basis is invoked.
937 */
get_equations(ptr_vector<equation> & result) const938 void grobner::get_equations(ptr_vector<equation> & result) const {
939 copy_to(m_processed, result);
940 copy_to(m_to_process, result);
941 }
942
943