1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 polynomial.h
7
8 Abstract:
9
10 Goodies for creating and handling polynomials.
11
12 Author:
13
14 Leonardo (leonardo) 2011-11-15
15
16 Notes:
17
18 --*/
19 #pragma once
20
21 #include "util/mpz.h"
22 #include "util/rational.h"
23 #include "util/obj_ref.h"
24 #include "util/ref_vector.h"
25 #include "util/z3_exception.h"
26 #include "util/scoped_numeral.h"
27 #include "util/scoped_numeral_vector.h"
28 #include "util/params.h"
29 #include "util/mpbqi.h"
30 #include "util/rlimit.h"
31 #include "util/lbool.h"
32 #include "util/sign.h"
33
34 class small_object_allocator;
35
36 namespace algebraic_numbers {
37 class anum;
38 class manager;
39 };
40
41 namespace polynomial {
42 typedef unsigned var;
43 const var null_var = UINT_MAX;
44 typedef svector<var> var_vector;
45 class monomial;
46
47 int lex_compare(monomial const * m1, monomial const * m2);
48 int lex_compare2(monomial const * m1, monomial const * m2, var min_var);
49 int graded_lex_compare(monomial const * m1, monomial const * m2);
50 int rev_lex_compare(monomial const * m1, monomial const * m2);
51 int graded_rev_lex_compare(monomial const * m1, monomial const * m2);
52
53 // It is used only for signing cancellation.
54 class polynomial_exception : public default_exception {
55 public:
polynomial_exception(char const * msg)56 polynomial_exception(char const * msg):default_exception(msg) {}
57 };
58
59 /**
60 \brief A mapping from variables to degree
61 */
62 class var2degree {
63 unsigned_vector m_var2degree;
64 public:
set_degree(var x,unsigned d)65 void set_degree(var x, unsigned d) { m_var2degree.setx(x, d, 0); }
degree(var x)66 unsigned degree(var x) const { return m_var2degree.get(x, 0); }
67 void display(std::ostream & out) const;
68 friend std::ostream & operator<<(std::ostream & out, var2degree const & ideal) { ideal.display(out); return out; }
69 };
70
71 template<typename ValManager, typename Value = typename ValManager::numeral>
72 class var2value {
73 public:
74 virtual ValManager & m() const = 0;
75 virtual bool contains(var x) const = 0;
76 virtual Value const & operator()(var x) const = 0;
77 };
78
79 typedef var2value<unsynch_mpq_manager> var2mpq;
80 typedef var2value<mpbqi_manager> var2mpbqi;
81 typedef var2value<algebraic_numbers::manager, algebraic_numbers::anum> var2anum;
82
83 class monomial_manager;
84
85 /**
86 \brief Parameters for polynomial factorization.
87 */
88 struct factor_params {
89 unsigned m_max_p; //!< factor in GF_p using primes p <= m_max_p (default UINT_MAX)
90 unsigned m_p_trials; //!< Number of different finite factorizations: G_p1 ... G_pk, where k < m_p_trials
91 unsigned m_max_search_size; //!< Threshold on the search space.
92 factor_params();
93 factor_params(unsigned max_p, unsigned p_trials, unsigned max_search_size);
94 void updt_params(params_ref const & p);
95 /*
96 REG_MODULE_PARAMS('factor', polynomial::factor_params::get_param_descrs')
97 */
98 static void get_param_descrs(param_descrs & r);
99 };
100
101 struct display_var_proc {
operatordisplay_var_proc102 virtual std::ostream& operator()(std::ostream & out, var x) const { return out << "x" << x; }
103 };
104
105 class polynomial;
106 class manager;
107 typedef obj_ref<monomial, manager> monomial_ref;
108 typedef obj_ref<polynomial, manager> polynomial_ref;
109 typedef ref_vector<polynomial, manager> polynomial_ref_vector;
110 typedef ptr_vector<polynomial> polynomial_vector;
111
112 class manager {
113 public:
114 typedef unsynch_mpz_manager numeral_manager;
115 typedef numeral_manager::numeral numeral;
116 typedef svector<numeral> numeral_vector;
117 typedef _scoped_numeral<numeral_manager> scoped_numeral;
118 typedef _scoped_numeral_vector<numeral_manager> scoped_numeral_vector;
119
120 /**
121 \brief Contains a factorization of a polynomial of the form c * (f_1)^k_1 * ... (f_n)^k_n
122 */
123 class factors {
124 vector<polynomial *> m_factors;
125 svector<unsigned> m_degrees;
126 manager & m_manager;
127 numeral m_constant;
128 unsigned m_total_factors;
129 public:
130 factors(manager & m);
131 ~factors();
132
133 /**
134 \brief Number of distinct factors (not counting multiplicities).
135 */
distinct_factors()136 unsigned distinct_factors() const { return m_factors.size(); }
137
138 /**
139 \brief Number of distinct factors (counting multiplicities).
140 */
total_factors()141 unsigned total_factors() const { return m_total_factors; }
142
143 /**
144 \brief Returns the factor at given position.
145 */
146 polynomial_ref operator[](unsigned i) const;
147
148 /**
149 \brief Returns the constant (c above).
150 */
get_constant()151 numeral const & get_constant() const { return m_constant; }
152
153 /**
154 \brief Sets the constant.
155 */
156 void set_constant(numeral const & constant);
157
158 /**
159 \brief Returns the degree of a factor (k_i above).
160 */
get_degree(unsigned i)161 unsigned get_degree(unsigned i) const { return m_degrees[i]; }
162
163 /**
164 \brief Sets the degree of a factor.
165 */
166 void set_degree(unsigned i, unsigned degree);
167
168 /**
169 \brief Adds a polynomial to the factorization.
170 */
171 void push_back(polynomial * p, unsigned degree);
172
173 /**
174 \brief Returns the polynomial that this factorization represents.
175 */
176 void multiply(polynomial_ref & out) const;
177
m()178 manager & m() const { return m_manager; }
pm()179 manager & pm() const { return m_manager; }
180
181 void display(std::ostream& out) const;
182
183 void reset();
184
185 friend std::ostream & operator<<(std::ostream & out, factors const & f) {
186 f.display(out);
187 return out;
188 }
189 };
190
191 struct imp;
192 private:
193 imp * m_imp;
194 public:
195 manager(reslimit& lim, numeral_manager & m, monomial_manager * mm = nullptr);
196 manager(reslimit& lim, numeral_manager & m, small_object_allocator * a);
197 ~manager();
198
199 numeral_manager & m() const;
200 monomial_manager & mm() const;
201 small_object_allocator & allocator() const;
202
203 /**
204 \brief Return true if Z_p[X1, ..., Xn]
205 */
206 bool modular() const;
207 /**
208 \brief Return p in Z_p[X1, ..., Xn]
209 \pre modular
210 */
211 numeral const & p() const;
212
213 /**
214 \brief Set manager as Z[X1, ..., Xn]
215 */
216 void set_z();
217 /**
218 \brief Set manager as Z_p[X1, ..., Xn]
219 */
220 void set_zp(numeral const & p);
221 void set_zp(uint64_t p);
222
223 /**
224 \brief Abstract event handler.
225 */
226 class del_eh {
227 friend class manager;
228 del_eh * m_next;
229 public:
del_eh()230 del_eh():m_next(nullptr) {}
231 virtual void operator()(polynomial * p) = 0;
232 };
233
234 /**
235 \brief Install a "delete polynomial" event handler.
236 The event handler is not owned by the polynomial manager.
237 If eh = 0, then it uninstall the event handler.
238 */
239 void add_del_eh(del_eh * eh);
240 void remove_del_eh(del_eh * eh);
241
242 /**
243 \brief Create a new variable.
244 */
245 var mk_var();
246
247 /**
248 \brief Return the number of variables in the manager.
249 */
250 unsigned num_vars() const;
251
252 /**
253 \brief Return true if x is a valid variable in this manager.
254 */
is_valid(var x)255 bool is_valid(var x) const { return x < num_vars(); }
256
257 /**
258 \brief Increment reference counter.
259 */
260 void inc_ref(polynomial * p);
261 void inc_ref(monomial * m);
262
263 /**
264 \brief Decrement reference counter.
265 */
266 void dec_ref(polynomial * p);
267 void dec_ref(monomial * m);
268
269 /**
270 \brief Return an unique id associated with \c m.
271 This id can be used to implement efficient mappings from monomial to data.
272 */
273 static unsigned id(monomial const * m);
274
275 /**
276 \brief Return an unique id associated with \c m.
277 This id can be used to implement efficient mappings from polynomial to data.
278 */
279 static unsigned id(polynomial const * p);
280
281
282 /**
283 \brief Normalize coefficients by dividing by their gcd
284 */
285 void gcd_simplify(polynomial* p);
286
287 /**
288 \brief Return true if \c m is the unit monomial.
289 */
290 static bool is_unit(monomial const * m);
291
292 /**
293 \brief Return true if \c p is the zero polynomial.
294 */
295 static bool is_zero(polynomial const * p);
296
297 /**
298 \brief Return true if \c p is the constant polynomial.
299 */
300 static bool is_const(polynomial const * p);
301
302 /**
303 \brief Return true if \c m is univariate.
304 */
305 static bool is_univariate(monomial const * m);
306
307 /**
308 \brief Return true if \c p is an univariate polynomial.
309 */
310 static bool is_univariate(polynomial const * p);
311
312 /**
313 \brief Return true if m is linear (i.e., it is of the form 1 or x).
314 */
315 static bool is_linear(monomial const * m);
316
317 /**
318 \brief Return true if all monomials in p are linear.
319 */
320 static bool is_linear(polynomial const * p);
321
322 /**
323 \brief Return true if the monomial is a variable.
324 */
325 static bool is_var(monomial const* p, var& v);
326
327 /**
328 \brief Return true if the polynomial is a variable.
329 */
330 bool is_var(polynomial const* p, var& v);
331
332 /**
333 \brief Return true if the polynomial is of the form x + k
334 */
335 bool is_var_num(polynomial const* p, var& v, scoped_numeral& n);
336
337 /**
338 \brief Return the degree of variable x in p.
339 */
340 static unsigned degree(polynomial const * p, var x);
341
342 /**
343 \brief Return the polynomial total degree. That is,
344 the degree of the monomial of maximal degree in p.
345 */
346 static unsigned total_degree(polynomial const * p);
347
348 /**
349 \brief Return the number of monomials in p.
350 */
351 static unsigned size(polynomial const * p);
352
353 /**
354 \brief Return the maximal variable occurring in p.
355
356 Return null_var if p is a constant polynomial.
357 */
358 static var max_var(polynomial const * p);
359
360 /**
361 \brief Return the coefficient of the i-th monomial in p.
362
363 \pre i < size(p)
364 */
365 static numeral const & coeff(polynomial const * p, unsigned i);
366
367 /**
368 \brief Given an univariate polynomial, return the coefficient of x_k
369 */
370 static numeral const & univ_coeff(polynomial const * p, unsigned k);
371
372 /**
373 \brief Return a polynomial h that is the coefficient of x^k in p.
374 if p does not contain any monomial containing x^k, then return 0.
375 */
376 polynomial * coeff(polynomial const * p, var x, unsigned k);
377
378 polynomial * coeff(polynomial const * p, var x, unsigned k, polynomial_ref & reduct);
379
380 /**
381 \brief Return true if the coefficient of x^k in p is an integer != 0.
382 */
383 bool nonzero_const_coeff(polynomial const * p, var x, unsigned k);
384
385 /**
386 \brief Return true if the coefficient of x^k in p is an integer, and store it in c.
387 */
388 bool const_coeff(polynomial const * p, var x, unsigned k, numeral & c);
389
390 /**
391 \brief Store in c the integer content of p.
392 */
393 void int_content(polynomial const * p, numeral & c);
394
395 /**
396 \brief Returns sum of the absolute value of the coefficients.
397 */
398 void abs_norm(polynomial const * p, numeral & norm);
399
400 /**
401 \brief Return the leading integer coefficient (among the loeding power of x, one is picked arbitrary).
402 */
403 numeral const & numeral_lc(polynomial const * p, var x);
404
405 /**
406 \brief Return the trailing integer coefficient (i.e. the constant term).
407 */
408 numeral const & numeral_tc(polynomial const * p);
409
410 /**
411 \brief Return the content i*c of p with respect to variable x.
412 If p is a polynomial in Z[y_1, ..., y_k, x], then c is a polynomial in Z[y_1, ..., y_k]
413 */
414 void content(polynomial const * p, var x, numeral & i, polynomial_ref & c);
415 void content(polynomial const * p, var x, polynomial_ref & c);
416
417 /**
418 \brief Return the primitive polynomial of p with respect to variable x.
419 If p is a polynomial in Z[y_1, ..., y_k, x], then pp is a polynomial in Z[y_1, ..., y_k, x]
420 */
421 void primitive(polynomial const * p, var x, polynomial_ref & pp);
422
423 /**
424 \brief Return the integer content, content, and primitive polynomials of p with respect to x.
425 i*c*pp = p
426 If p is a polynomial in Z[y_1, ..., y_k, x], then
427 c is a polynomial in Z[y_1, ..., y_k]
428 pp is a polynomial in Z[y_1, ..., y_k, x]
429 */
430 void icpp(polynomial const * p, var x, numeral & i, polynomial_ref & c, polynomial_ref & pp);
431
432 polynomial * flip_sign_if_lm_neg(polynomial const * p);
433
434 /**
435 \brief Return the gcd g of p and q.
436 */
437 void gcd(polynomial const * p, polynomial const * q, polynomial_ref & g);
438
439 /**
440 \brief Return the i-th monomial of p.
441 */
442 static monomial * get_monomial(polynomial const * p, unsigned i);
443
444 /**
445 \brief Return the total degree of the given monomial.
446 */
447 static unsigned total_degree(monomial const * m);
448
449 /**
450 \brief Return the size (number of variables) of the given monomial.
451 */
452 static unsigned size(monomial const * m);
453
454 /**
455 \brief Convert a monomial created in a different manager.
456 */
457 monomial * convert(monomial const * m);
458
459 /**
460 \brief Return the i-th variable in the given monomial.
461
462 \pre i < size(m)
463 */
464 static var get_var(monomial const * m, unsigned i);
465
466 /**
467 \brief Return the degree of the i-th variable in the given monomial.
468
469 \pre i < size(m)
470 */
471 static unsigned degree(monomial const * m, unsigned i);
472
473 /**
474 \brief Return the degree of x in the given monomial.
475 */
476 static unsigned degree_of(monomial const * m, var x);
477
478 /**
479 \brief Return hash code for the given monomial.
480 */
481 static unsigned hash(monomial const * m);
482
483 /**
484 \brief Return hash code for the given polynomial.
485 */
486 unsigned hash(polynomial const * p);
487
488 /**
489 \brief Create the unit monomial. That is, the monomial of size zero.
490 */
491 monomial * mk_unit();
492
493 /**
494 \brief Create the zero polynomial. That is, the polynomial of size zero.
495 */
496 polynomial * mk_zero();
497
498 /**
499 \brief Create the constant polynomial \c r.
500
501 \warning r is a number managed by the numeral_manager in the polynomial manager
502
503 \warning r is reset.
504 */
505 polynomial * mk_const(numeral & r);
506
507 /**
508 \brief Create the constant polynomial \c r.
509
510 \pre r must be an integer
511 */
512 polynomial * mk_const(rational const & r);
513
514 /**
515 \brief Create an univariate monomial.
516 */
517 monomial * mk_monomial(var x);
518
519 /**
520 \brief Create an univariate monomial.
521 */
522 monomial * mk_monomial(var x, unsigned k);
523
524 /**
525 \brief Create the monomial
526
527 xs[0]*...*xs[sz-1]
528
529 Remark: xs may contain duplicate variables.
530
531 \warning The elements of xs will be reordered.
532 */
533 monomial * mk_monomial(unsigned sz, var * xs);
534
535 /**
536 \brief Create the polynomial x^k
537 */
538 polynomial * mk_polynomial(var x, unsigned k = 1);
539
540 /**
541 \brief Create the polynomial
542
543 as[0]*ms[0] + ... + as[sz-1]*ms[sz - 1]
544
545 \pre as's must be integers
546 */
547 polynomial * mk_polynomial(unsigned sz, rational const * as, monomial * const * ms);
548
549 /**
550 \brief Create the polynomial
551
552 as[0]*ms[0] + ... + as[sz-1]*ms[sz - 1]
553
554 \warning as's are numbers managed by mpq_manager in the polynomial manager
555
556 \warning the numerals in as are reset.
557 */
558 polynomial * mk_polynomial(unsigned sz, numeral * as, monomial * const * ms);
559
560 /**
561 \brief Create the linear polynomial
562
563 as[0]*xs[0] + ... + as[sz-1]*xs[sz-1] + c
564
565 \pre as's must be integers
566 */
567 polynomial * mk_linear(unsigned sz, rational const * as, var const * xs, rational const & c);
568
569 /**
570 \brief Create the linear polynomial
571
572 as[0]*xs[0] + ... + as[sz-1]*xs[sz-1] + c
573
574 \warning as's are numbers managed by mpq_manager in the polynomial manager
575
576 \warning the numerals in as are reset.
577 */
578 polynomial * mk_linear(unsigned sz, numeral * as, var const * xs, numeral & c);
579
580 /**
581 \brief Create an univariate polynomial of degree n
582
583 as[0] + as[1]*x + as[2]*x^2 + ... + as[n]*x^n
584
585 \warning \c as must contain n+1 elements.
586 */
587 polynomial * mk_univariate(var x, unsigned n, numeral * as);
588
589 /**
590 \brief Return -p
591 */
592 polynomial * neg(polynomial const * p);
593
594 /**
595 \brief Return p1 + p2
596 */
597 polynomial * add(polynomial const * p1, polynomial const * p2);
598
599 /**
600 \brief Return p1 - p2
601 */
602 polynomial * sub(polynomial const * p1, polynomial const * p2);
603
604 /**
605 \brief Return a1*m1*p1 + a2*m2*p2
606 */
607 polynomial * addmul(numeral const & a1, monomial const * m1, polynomial const * p1, numeral const & a2, monomial const * m2, polynomial const * p2);
608
609 /**
610 \brief Return p1 + a2*m2*p2
611 */
612 polynomial * addmul(polynomial const * p1, numeral const & a2, monomial const * m2, polynomial const * p2);
613
614 /**
615 \brief Return p1 + a2*p2
616 */
617 polynomial * addmul(polynomial const * p1, numeral const & a2, polynomial const * p2);
618
619 /**
620 \brief Return a * p
621 */
622 polynomial * mul(numeral const & a, polynomial const * p);
623 polynomial * mul(rational const & a, polynomial const * p);
624
625 /**
626 \brief Return p1 * p2
627 */
628 polynomial * mul(polynomial const * p1, polynomial const * p2);
629
630 /**
631 \brief Return m1 * m2
632 */
633 monomial * mul(monomial const * m1, monomial const * m2);
634
635 /**
636 \brief Return a * m * p
637 */
638 polynomial * mul(numeral const & a, monomial const * m, polynomial const * p);
639
640 /**
641 \brief Return m * p
642 */
643 polynomial * mul(monomial const * m, polynomial const * p);
644
645 /**
646 \brief Return true if m2 divides m1
647 */
648 bool div(monomial const * m1, monomial const * m2);
649
650 /**
651 \brief Return true if m2 divides m1, and store the result in r.
652 */
653 bool div(monomial const * m1, monomial const * m2, monomial_ref & r);
654
655 /**
656 \brief Newton interpolation algorithm for multivariate polynomials.
657 */
658 void newton_interpolation(var x, unsigned d, numeral const * inputs, polynomial * const * outputs, polynomial_ref & r);
659
660 /**
661 \brief Return the GCD of m1 and m2.
662 Store in q1 and q2 monomials s.t.
663 m1 = gcd * q1
664 m2 = gcd * q2
665 */
666 monomial * gcd(monomial const * m1, monomial const * m2, monomial * & q1, monomial * & q2);
667
668 /**
669 \brief Return true if the gcd of m1 and m2 is not 1.
670 In that case, store in q1 and q2 monomials s.t.
671 m1 = gcd * q1
672 m2 = gcd * q2
673 */
674 bool unify(monomial const * m1, monomial const * m2, monomial * & q1, monomial * & q2);
675
676 /**
677 \brief Return m^k
678 */
679 monomial * pw(monomial const * m, unsigned k);
680
681 /**
682 \brief Return the polynomial p^k
683 */
684 void pw(polynomial const * p, unsigned k, polynomial_ref & r);
685
686 /**
687 \brief Return dp/dx
688 */
689 polynomial * derivative(polynomial const * p, var x);
690
691 /**
692 \brief r := square free part of p with respect to x
693 */
694 void square_free(polynomial const * p, var x, polynomial_ref & r);
695
696 /**
697 \brief Return true if p is square free with respect to x
698 */
699 bool is_square_free(polynomial const * p, var x);
700
701 /**
702 \brief r := square free part of p
703 */
704 void square_free(polynomial const * p, polynomial_ref & r);
705
706 /**
707 \brief Return true if p is square free
708 */
709 bool is_square_free(polynomial const * p);
710
711 /**
712 \brief Return true if p1 == p2.
713 */
714 bool eq(polynomial const * p1, polynomial const * p2);
715
716 /**
717 \brief Rename variables using the given permutation.
718
719 sz must be num_vars()
720 */
721 void rename(unsigned sz, var const * xs);
722
723 /**
724 \brief Given an univariate polynomial p(x),
725 return the polynomial x^n * p(1/x), where n = degree(p)
726
727 If u is a nonzero root of p, then 1/u is a root the resultant polynomial.
728 */
729 polynomial * compose_1_div_x(polynomial const * p);
730
731 /**
732 \brief Given an univariate polynomial p(x),
733 return the polynomial y^n * p(x/y), where n = degree(p)
734 */
735 polynomial * compose_x_div_y(polynomial const * p, var y);
736
737 /**
738 \brief Given an univariate polynomial p(x), return p(-x)
739 */
740 polynomial * compose_minus_x(polynomial const * p);
741
742 /**
743 \brief Given an univariate polynomial p(x) and a polynomial q(y_1, ..., y_n),
744 return a polynomial r(y_1, ..., y_n) = p(q(y_1, ..., y_n)).
745 */
746 void compose(polynomial const * p, polynomial const * q, polynomial_ref & r);
747
748 /**
749 \brief Given an univariate polynomial p(x), return the polynomial r(y) = p(y)
750 */
751 polynomial * compose_y(polynomial const * p, var y);
752
753 /**
754 \brief Given an univariate polynomial p(x), return the polynomial r(x, y) = p(x - y).
755 The result is stored in r.
756 */
757 void compose_x_minus_y(polynomial const * p, var y, polynomial_ref & r);
758
759 /**
760 \brief Given an univariate polynomial p(x), return the polynomial r(x, y) = p(x + y).
761 The result is stored in r.
762 */
763 void compose_x_plus_y(polynomial const * p, var y, polynomial_ref & r);
764
765 /**
766 \brief Given an univariate polynomial p(x), return the polynomial r(x) = p(x - c).
767 The result is stored in r.
768 */
769 void compose_x_minus_c(polynomial const * p, numeral const & c, polynomial_ref & r);
770
771 /**
772 \brief Return the exact pseudo remainder of p by q, assuming x is the maximal variable.
773
774 See comments at pseudo_division_core at polynomial.cpp for a description of exact pseudo division.
775 */
776 void exact_pseudo_remainder(polynomial const * p, polynomial const * q, var x, polynomial_ref & R);
777
exact_pseudo_remainder(polynomial const * p,polynomial const * q,polynomial_ref & R)778 void exact_pseudo_remainder(polynomial const * p, polynomial const * q, polynomial_ref & R) {
779 exact_pseudo_remainder(p, q, max_var(q), R);
780 }
781
782 /**
783 \brief Return the pseudo remainder of p by q, assuming x is the maximal variable.
784
785 See comments at pseudo_division_core at polynomial.cpp for a description of exact pseudo division.
786 */
787 void pseudo_remainder(polynomial const * p, polynomial const * q, var x, unsigned & d, polynomial_ref & R);
788
pseudo_remainder(polynomial const * p,polynomial const * q,unsigned & d,polynomial_ref & R)789 void pseudo_remainder(polynomial const * p, polynomial const * q, unsigned & d, polynomial_ref & R) {
790 pseudo_remainder(p, q, max_var(q), d, R);
791 }
792
793 /**
794 \brief Return the exact pseudo division quotient and remainder.
795
796 See comments at pseudo_division_core at polynomial.cpp for a description of exact pseudo division.
797 */
798 void exact_pseudo_division(polynomial const * p, polynomial const * q, var x, polynomial_ref & Q, polynomial_ref & R);
799
exact_pseudo_division(polynomial const * p,polynomial const * q,polynomial_ref & Q,polynomial_ref & R)800 void exact_pseudo_division(polynomial const * p, polynomial const * q, polynomial_ref & Q, polynomial_ref & R) {
801 exact_pseudo_division(p, q, max_var(q), Q, R);
802 }
803
804 /**
805 \brief Return the pseudo division quotient and remainder.
806
807 See comments at pseudo_division_core at polynomial.cpp for a description of exact pseudo division.
808 */
809 void pseudo_division(polynomial const * p, polynomial const * q, var x, unsigned & d, polynomial_ref & Q, polynomial_ref & R);
810
pseudo_division(polynomial const * p,polynomial const * q,unsigned & d,polynomial_ref & Q,polynomial_ref & R)811 void pseudo_division(polynomial const * p, polynomial const * q, unsigned & d, polynomial_ref & Q, polynomial_ref & R) {
812 pseudo_division(p, q, max_var(q), d, Q, R);
813 }
814
815 /**
816 \brief Return p/q if q divides p.
817
818 \pre q divides p.
819
820 \remark p and q may be multivariate polynomials.
821 */
822 polynomial * exact_div(polynomial const * p, polynomial const * q);
823
824 /**
825 \brief Return true if q divides p.
826 */
827 bool divides(polynomial const * q, polynomial const * p);
828
829 /**
830 \brief Return p/c if c divides p.
831
832 \pre c divides p.
833
834 \remark p may be multivariate polynomial.
835 */
836 polynomial * exact_div(polynomial const * p, numeral const & c);
837
838 /**
839 \brief Store in r the quasi-resultant of p and q with respect to variable x.
840
841 Assume p and q are polynomials in Q[y_1, ..., y_n, x].
842 Then r is a polynomial in Q[y_1, ..., y_n].
843 Moreover, Forall a_1, ..., a_n, b,
844 if p(a_1, ..., a_n, b) = q(a_1, ..., a_n, b) = 0
845 then r(a_1, ..., a_n) = 0
846
847 \pre p and q must contain x.
848
849 \remark if r is the zero polynomial, then for any complex numbers a_1, ..., a_n,
850 the univariate polynomials p(a_1, ..., a_n, x) and q(a_1, ..., a_n, x) in C[x] have
851 a common root. C is the field of the complex numbers.
852 */
853 void quasi_resultant(polynomial const * p, polynomial const * q, var x, polynomial_ref & r);
854
855 /**
856 \brief Store in r the resultant of p and q with respect to variable x.
857 See comments in polynomial.cpp for more details
858 */
859 void resultant(polynomial const * p, polynomial const * q, var x, polynomial_ref & r);
860
861 /**
862 \brief Store in r the discriminant of p with respect to variable x.
863 discriminant(p, x, r) == resultant(p, derivative(p, x), x, r)
864 */
865 void discriminant(polynomial const * p, var x, polynomial_ref & r);
866
867 /**
868 \brief Store in S the principal subresultant coefficients for p and q.
869 */
870 void psc_chain(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S);
871
872 /**
873 \brief Make sure the GCD of the coefficients is one.
874
875 Make sure that the polynomial is a member of the polynomial ring of this manager.
876 If manager is Z_p[X1, ..., Xn], and polynomial is in Z[X1, ..., Xn] return a new
877 one where all coefficients are in Z_p
878 */
879 polynomial * normalize(polynomial const * p);
880
881 /**
882 \brief Return true if p is a square, and store its square root in r.
883 */
884 bool sqrt(polynomial const * p, polynomial_ref & r);
885
886
887 /**
888 \brief obtain the sign of the polynomial given sign of variables.
889 */
890 lbool sign(polynomial const* p, svector<lbool> const& sign_of_vars);
891
892 /**
893 \brief Return true if p is always positive for any assignment of its variables.
894
895 This is an incomplete check. This method just check if all monomials are powers of two,
896 and the coefficients are positive.
897 */
898 bool is_pos(polynomial const * p);
899
900 /**
901 \brief Return true if p is always negative for any assignment of its variables.
902
903 This is an incomplete check.
904 */
905 bool is_neg(polynomial const * p);
906
907 /**
908 \brief Return true if p is always non-positive for any assignment of its variables.
909
910 This is an incomplete check.
911 */
912 bool is_nonpos(polynomial const * p);
913
914 /**
915 \brief Return true if p is always non-negative for any assignment of its variables.
916
917 This is an incomplete check.
918 */
919 bool is_nonneg(polynomial const * p);
920
921 /**
922 \brief Make sure the monomials in p are sorted using lexicographical order.
923 Remark: the maximal monomial is at position 0.
924 */
925 void lex_sort(polynomial * p);
926
927 /**
928 \brief Collect variables that occur in p into xs
929 */
930 void vars(polynomial const * p, var_vector & xs);
931
932 /**
933 \brief Evaluate polynomial p using the assignment [x_1 -> v_1, ..., x_n -> v_n].
934 The result is store in r.
935 All variables occurring in p must be in xs.
936 */
937 void eval(polynomial const * p, var2mpbqi const & x2v, mpbqi & r);
938 void eval(polynomial const * p, var2mpq const & x2v, mpq & r);
939 void eval(polynomial const * p, var2anum const & x2v, algebraic_numbers::anum & r);
940
941 /**
942 \brief Apply substitution [x_1 -> v_1, ..., x_n -> v_n].
943 That is, given p \in Z[x_1, ..., x_n, y_1, ..., y_m] return a polynomial
944 r \in Z[y_1, ..., y_m].
945 Moreover forall a_1, ..., a_m in Q
946 sign(r(a_1, ..., a_m)) == sign(p(v_1, ..., v_n, a_1, ..., a_m))
947 */
948 polynomial * substitute(polynomial const * p, var2mpq const & x2v);
949 polynomial * substitute(polynomial const * p, unsigned xs_sz, var const * xs, mpq const * vs);
950
951 /**
952 \brief Apply substitution [x_1 -> v_1, ..., x_n -> v_n].
953 That is, given p \in Z[x_1, ..., x_n, y_1, ..., y_m] return
954 polynomial r(y_1, ..., y_m) = p(v_1, ..., v_n, y_1, ..., y_m) in Z[y_1, ..., y_m].
955 */
956 polynomial * substitute(polynomial const * p, unsigned xs_sz, var const * xs, numeral const * vs);
957
958 /**
959 \brief Apply substitution [x -> v].
960 That is, given p \in Z[x, y_1, ..., y_m] return
961 polynomial r(y_1, ..., y_m) = p(v, y_1, ..., y_m) in Z[y_1, ..., y_m].
962 */
substitute(polynomial const * p,var x,numeral const & v)963 polynomial * substitute(polynomial const * p, var x, numeral const & v) {
964 return substitute(p, 1, &x, &v);
965 }
966
967 /**
968 \brief Apply substitution [x -> p/q] in r.
969 That is, given r \in Z[x, y_1, .., y_m] return
970 polynomial q^k * r(p/q, y_1, .., y_m), where k is the maximal degree of x in r.
971 */
972 void substitute(polynomial const* r, var x, polynomial const* p, polynomial const* q, polynomial_ref& result);
973
974 /**
975 \brief Factorize the given polynomial p and store its factors in r.
976 */
977 void factor(polynomial const * p, factors & r, factor_params const & params = factor_params());
978
979 /**
980 \brief Dense univariate polynomial to sparse polynomial.
981 */
982 polynomial * to_polynomial(unsigned sz, numeral const * p, var x);
to_polynomial(numeral_vector const & p,var x)983 polynomial * to_polynomial(numeral_vector const & p, var x) {
984 return to_polynomial(p.size(), p.c_ptr(), x);
985 }
986
987 /**
988 \brief Make the leading monomial (with respect to graded lexicographical order) monic.
989
990 \pre numeral_manager must be a field.
991 */
992 polynomial * mk_glex_monic(polynomial const * p);
993
994 /**
995 \brief Return p'(y_1, ..., y_n, x) = p(y_1, ..., y_n, x + v)
996 */
997 polynomial * translate(polynomial const * p, var x, numeral const & v);
998
999 /**
1000 \brief Store p'(y_1, ..., y_n, x_1, ..., x_m) = p(y_1, ..., y_n, x_1 + v_1, ..., x_m + v_m)
1001 into r.
1002 */
1003 void translate(polynomial const * p, unsigned xs_sz, var const * xs, numeral const * vs, polynomial_ref & r);
translate(polynomial const * p,var_vector const & xs,numeral_vector const & vs,polynomial_ref & r)1004 void translate(polynomial const * p, var_vector const & xs, numeral_vector const & vs, polynomial_ref & r) {
1005 SASSERT(xs.size() == vs.size());
1006 translate(p, xs.size(), xs.c_ptr(), vs.c_ptr(), r);
1007 }
1008
1009 /**
1010 \brief Remove monomials m if it contains x^k and x2d[x] >= k
1011 */
1012 polynomial * mod_d(polynomial const * p, var2degree const & x2d);
1013
1014 /**
1015 \brief (exact) Pseudo division modulo var->degree mapping.
1016 */
1017 void exact_pseudo_division_mod_d(polynomial const * p, polynomial const * q, var x, var2degree const & x2d, polynomial_ref & Q, polynomial_ref & R);
1018
1019 void display(std::ostream & out, monomial const * m, display_var_proc const & proc = display_var_proc(), bool use_star = true) const;
1020
1021 void display(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc(), bool use_star = false) const;
1022
1023 void display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc()) const;
1024
1025 friend std::ostream & operator<<(std::ostream & out, polynomial_ref const & p) {
1026 p.m().display(out, p);
1027 return out;
1028 }
1029 };
1030
1031 typedef manager::factors factors;
1032 typedef manager::numeral numeral;
1033 typedef manager::numeral_manager numeral_manager;
1034 typedef manager::scoped_numeral scoped_numeral;
1035 typedef manager::scoped_numeral_vector scoped_numeral_vector;
1036
1037 class scoped_set_z {
1038 manager & m;
1039 bool m_modular;
1040 scoped_numeral m_p;
1041 public:
scoped_set_z(manager & _m)1042 scoped_set_z(manager & _m):m(_m), m_modular(m.modular()), m_p(m.m()) { m_p = m.p(); m.set_z(); }
~scoped_set_z()1043 ~scoped_set_z() { if (m_modular) m.set_zp(m_p); }
1044 };
1045
1046 class scoped_set_zp {
1047 manager & m;
1048 bool m_modular;
1049 scoped_numeral m_p;
1050 public:
scoped_set_zp(manager & _m,numeral const & p)1051 scoped_set_zp(manager & _m, numeral const & p):m(_m), m_modular(m.modular()), m_p(m.m()) { m_p = m.p(); m.set_zp(p); }
scoped_set_zp(manager & _m,uint64_t p)1052 scoped_set_zp(manager & _m, uint64_t p):m(_m), m_modular(m.modular()), m_p(m.m()) { m_p = m.p(); m.set_zp(p); }
~scoped_set_zp()1053 ~scoped_set_zp() { if (m_modular) m.set_zp(m_p); else m.set_z(); }
1054 };
1055 };
1056
1057 typedef polynomial::polynomial_ref polynomial_ref;
1058 typedef polynomial::polynomial_ref_vector polynomial_ref_vector;
1059
1060 polynomial::polynomial * convert(polynomial::manager & sm, polynomial::polynomial * p, polynomial::manager & tm,
1061 polynomial::var x = polynomial::null_var, unsigned max_d = UINT_MAX);
1062
convert(polynomial::manager & sm,polynomial_ref const & p,polynomial::manager & tm)1063 inline polynomial::polynomial * convert(polynomial::manager & sm, polynomial_ref const & p, polynomial::manager & tm) {
1064 SASSERT(&sm == &(p.m()));
1065 return convert(sm, p.get(), tm);
1066 }
1067
neg(polynomial_ref const & p)1068 inline polynomial_ref neg(polynomial_ref const & p) {
1069 polynomial::manager & m = p.m();
1070 return polynomial_ref(m.neg(p), m);
1071 }
1072
1073 inline polynomial_ref operator-(polynomial_ref const & p) {
1074 polynomial::manager & m = p.m();
1075 return polynomial_ref(m.neg(p), m);
1076 }
1077
1078 inline polynomial_ref operator+(polynomial_ref const & p1, polynomial_ref const & p2) {
1079 polynomial::manager & m = p1.m();
1080 return polynomial_ref(m.add(p1, p2), m);
1081 }
1082
1083 inline polynomial_ref operator+(polynomial_ref const & p1, int n) {
1084 polynomial::manager & m = p1.m();
1085 polynomial_ref tmp(m.mk_const(rational(n)), m);
1086 return p1 + tmp;
1087 }
1088
1089 inline polynomial_ref operator+(polynomial_ref const & p1, rational const & n) {
1090 polynomial::manager & m = p1.m();
1091 polynomial_ref tmp(m.mk_const(n), m);
1092 return p1 + tmp;
1093 }
1094
1095 inline polynomial_ref operator+(polynomial::numeral const & n, polynomial_ref const & p) {
1096 polynomial::manager & m = p.m();
1097 polynomial_ref tmp(m.mk_const(n), m);
1098 return p + tmp;
1099 }
1100
1101 inline polynomial_ref operator+(polynomial_ref const & p, polynomial::numeral const & n) {
1102 return operator+(n, p);
1103 }
1104
1105 inline polynomial_ref operator-(polynomial_ref const & p1, polynomial_ref const & p2) {
1106 polynomial::manager & m = p1.m();
1107 return polynomial_ref(m.sub(p1, p2), m);
1108 }
1109
1110 inline polynomial_ref operator-(polynomial_ref const & p1, int n) {
1111 polynomial::manager & m = p1.m();
1112 polynomial_ref tmp(m.mk_const(rational(n)), m);
1113 return p1 - tmp;
1114 }
1115
1116 inline polynomial_ref operator-(polynomial_ref const & p1, rational const & n) {
1117 polynomial::manager & m = p1.m();
1118 polynomial_ref tmp(m.mk_const(n), m);
1119 return p1 - tmp;
1120 }
1121
1122 inline polynomial_ref operator-(polynomial::numeral const & n, polynomial_ref const & p) {
1123 polynomial::manager & m = p.m();
1124 polynomial_ref tmp(m.mk_const(n), m);
1125 return p - tmp;
1126 }
1127
1128 inline polynomial_ref operator-(polynomial_ref const & p, polynomial::numeral const & n) {
1129 return operator-(n, p);
1130 }
1131
1132 inline polynomial_ref operator*(polynomial_ref const & p1, polynomial_ref const & p2) {
1133 polynomial::manager & m = p1.m();
1134 return polynomial_ref(m.mul(p1, p2), m);
1135 }
1136
1137 inline polynomial_ref operator*(rational const & n, polynomial_ref const & p) {
1138 polynomial::manager & m = p.m();
1139 return polynomial_ref(m.mul(n, p), m);
1140 }
1141
1142 inline polynomial_ref operator*(int n, polynomial_ref const & p) {
1143 polynomial::manager & m = p.m();
1144 return polynomial_ref(m.mul(rational(n), p), m);
1145 }
1146
1147 inline polynomial_ref operator*(polynomial::numeral const & n, polynomial_ref const & p) {
1148 polynomial::manager & m = p.m();
1149 return polynomial_ref(m.mul(n, p), m);
1150 }
1151
1152 inline polynomial_ref operator*(polynomial_ref const & p, polynomial::numeral const & n) {
1153 return operator*(n, p);
1154 }
1155
eq(polynomial_ref const & p1,polynomial_ref const & p2)1156 inline bool eq(polynomial_ref const & p1, polynomial_ref const & p2) {
1157 polynomial::manager & m = p1.m();
1158 return m.eq(p1, p2);
1159 }
1160
1161 inline polynomial_ref operator^(polynomial_ref const & p, int k) {
1162 SASSERT(k > 0);
1163 polynomial::manager & m = p.m();
1164 polynomial_ref r(m);
1165 m.pw(p, k, r);
1166 return polynomial_ref(r);
1167 }
1168
1169 inline polynomial_ref operator^(polynomial_ref const & p, unsigned k) {
1170 return operator^(p, static_cast<int>(k));
1171 }
1172
derivative(polynomial_ref const & p,polynomial::var x)1173 inline polynomial_ref derivative(polynomial_ref const & p, polynomial::var x) {
1174 polynomial::manager & m = p.m();
1175 return polynomial_ref(m.derivative(p, x), m);
1176 }
1177
is_zero(polynomial_ref const & p)1178 inline bool is_zero(polynomial_ref const & p) {
1179 return p.m().is_zero(p);
1180 }
1181
is_const(polynomial_ref const & p)1182 inline bool is_const(polynomial_ref const & p) {
1183 return p.m().is_const(p);
1184 }
1185
is_linear(polynomial_ref const & p)1186 inline bool is_linear(polynomial_ref const & p) {
1187 return p.m().is_linear(p);
1188 }
1189
is_univariate(polynomial_ref const & p)1190 inline bool is_univariate(polynomial_ref const & p) {
1191 return p.m().is_univariate(p);
1192 }
1193
total_degree(polynomial_ref const & p)1194 inline unsigned total_degree(polynomial_ref const & p) {
1195 return p.m().total_degree(p);
1196 }
1197
max_var(polynomial_ref const & p)1198 inline polynomial::var max_var(polynomial_ref const & p) {
1199 return p.m().max_var(p);
1200 }
1201
degree(polynomial_ref const & p,polynomial::var x)1202 inline unsigned degree(polynomial_ref const & p, polynomial::var x) {
1203 return p.m().degree(p, x);
1204 }
1205
size(polynomial_ref const & p)1206 inline unsigned size(polynomial_ref const & p) {
1207 return p.m().size(p);
1208 }
1209
coeff(polynomial_ref const & p,polynomial::var x,unsigned k)1210 inline polynomial_ref coeff(polynomial_ref const & p, polynomial::var x, unsigned k) {
1211 polynomial::manager & m = p.m();
1212 return polynomial_ref(m.coeff(p, x, k), m);
1213 }
1214
lc(polynomial_ref const & p,polynomial::var x)1215 inline polynomial_ref lc(polynomial_ref const & p, polynomial::var x) {
1216 polynomial::manager & m = p.m();
1217 return polynomial_ref(m.coeff(p, x, degree(p, x)), m);
1218 }
1219
univ_coeff(polynomial_ref const & p,unsigned k)1220 inline polynomial::numeral const & univ_coeff(polynomial_ref const & p, unsigned k) {
1221 return p.m().univ_coeff(p, k);
1222 }
1223
content(polynomial_ref const & p,polynomial::var x)1224 inline polynomial_ref content(polynomial_ref const & p, polynomial::var x) {
1225 polynomial::manager & m = p.m();
1226 polynomial_ref r(m);
1227 m.content(p, x, r);
1228 return r;
1229 }
1230
primitive(polynomial_ref const & p,polynomial::var x)1231 inline polynomial_ref primitive(polynomial_ref const & p, polynomial::var x) {
1232 polynomial::manager & m = p.m();
1233 polynomial_ref r(m);
1234 m.primitive(p, x, r);
1235 return r;
1236 }
1237
gcd(polynomial_ref const & p,polynomial_ref const & q)1238 inline polynomial_ref gcd(polynomial_ref const & p, polynomial_ref const & q) {
1239 polynomial::manager & m = p.m();
1240 polynomial_ref r(m);
1241 m.gcd(p, q, r);
1242 return r;
1243 }
1244
is_square_free(polynomial_ref const & p,polynomial::var x)1245 inline bool is_square_free(polynomial_ref const & p, polynomial::var x) {
1246 return p.m().is_square_free(p, x);
1247 }
1248
square_free(polynomial_ref const & p,polynomial::var x)1249 inline polynomial_ref square_free(polynomial_ref const & p, polynomial::var x) {
1250 polynomial::manager & m = p.m();
1251 polynomial_ref r(m);
1252 m.square_free(p, x, r);
1253 return r;
1254 }
1255
is_square_free(polynomial_ref const & p)1256 inline bool is_square_free(polynomial_ref const & p) {
1257 return p.m().is_square_free(p);
1258 }
1259
square_free(polynomial_ref const & p)1260 inline polynomial_ref square_free(polynomial_ref const & p) {
1261 polynomial::manager & m = p.m();
1262 polynomial_ref r(m);
1263 m.square_free(p, r);
1264 return r;
1265 }
1266
compose_y(polynomial_ref const & p,polynomial::var y)1267 inline polynomial_ref compose_y(polynomial_ref const & p, polynomial::var y) {
1268 polynomial::manager & m = p.m();
1269 return polynomial_ref(m.compose_y(p, y), m);
1270 }
1271
compose_1_div_x(polynomial_ref const & p)1272 inline polynomial_ref compose_1_div_x(polynomial_ref const & p) {
1273 polynomial::manager & m = p.m();
1274 return polynomial_ref(m.compose_1_div_x(p), m);
1275 }
1276
compose_x_div_y(polynomial_ref const & p,polynomial::var y)1277 inline polynomial_ref compose_x_div_y(polynomial_ref const & p, polynomial::var y) {
1278 polynomial::manager & m = p.m();
1279 return polynomial_ref(m.compose_x_div_y(p, y), m);
1280 }
1281
compose_minus_x(polynomial_ref const & p)1282 inline polynomial_ref compose_minus_x(polynomial_ref const & p) {
1283 polynomial::manager & m = p.m();
1284 return polynomial_ref(m.compose_minus_x(p), m);
1285 }
1286
compose(polynomial_ref const & p,polynomial_ref const & g)1287 inline polynomial_ref compose(polynomial_ref const & p, polynomial_ref const & g) {
1288 polynomial::manager & m = p.m();
1289 polynomial_ref r(m);
1290 m.compose(p, g, r);
1291 return polynomial_ref(r);
1292 }
1293
compose_x_minus_y(polynomial_ref const & p,polynomial::var y)1294 inline polynomial_ref compose_x_minus_y(polynomial_ref const & p, polynomial::var y) {
1295 polynomial::manager & m = p.m();
1296 polynomial_ref r(m);
1297 m.compose_x_minus_y(p, y, r);
1298 return polynomial_ref(r);
1299 }
1300
compose_x_plus_y(polynomial_ref const & p,polynomial::var y)1301 inline polynomial_ref compose_x_plus_y(polynomial_ref const & p, polynomial::var y) {
1302 polynomial::manager & m = p.m();
1303 polynomial_ref r(m);
1304 m.compose_x_plus_y(p, y, r);
1305 return polynomial_ref(r);
1306 }
1307
compose_x_minus_c(polynomial_ref const & p,polynomial::numeral const & c)1308 inline polynomial_ref compose_x_minus_c(polynomial_ref const & p, polynomial::numeral const & c) {
1309 polynomial::manager & m = p.m();
1310 polynomial_ref r(m);
1311 m.compose_x_minus_c(p, c, r);
1312 return polynomial_ref(r);
1313 }
1314
exact_div(polynomial_ref const & p,polynomial_ref const & q)1315 inline polynomial_ref exact_div(polynomial_ref const & p, polynomial_ref const & q) {
1316 polynomial::manager & m = p.m();
1317 return polynomial_ref(m.exact_div(p, q), m);
1318 }
1319
normalize(polynomial_ref const & p)1320 inline polynomial_ref normalize(polynomial_ref const & p) {
1321 polynomial::manager & m = p.m();
1322 return polynomial_ref(m.normalize(p), m);
1323 }
1324
sqrt(polynomial_ref const & p,polynomial_ref & r)1325 inline bool sqrt(polynomial_ref const & p, polynomial_ref & r) {
1326 return p.m().sqrt(p, r);
1327 }
1328
exact_pseudo_remainder(polynomial_ref const & p,polynomial_ref const & q,polynomial::var x)1329 inline polynomial_ref exact_pseudo_remainder(polynomial_ref const & p, polynomial_ref const & q, polynomial::var x) {
1330 polynomial::manager & m = p.m();
1331 polynomial_ref r(m);
1332 m.exact_pseudo_remainder(p, q, x, r);
1333 return polynomial_ref(r);
1334 }
1335
exact_pseudo_remainder(polynomial_ref const & p,polynomial_ref const & q)1336 inline polynomial_ref exact_pseudo_remainder(polynomial_ref const & p, polynomial_ref const & q) {
1337 return exact_pseudo_remainder(p, q, max_var(q));
1338 }
1339
pseudo_remainder(polynomial_ref const & p,polynomial_ref const & q,polynomial::var x,unsigned & d)1340 inline polynomial_ref pseudo_remainder(polynomial_ref const & p, polynomial_ref const & q, polynomial::var x, unsigned & d) {
1341 polynomial::manager & m = p.m();
1342 polynomial_ref r(m);
1343 m.pseudo_remainder(p, q, x, d, r);
1344 return polynomial_ref(r);
1345 }
1346
pseudo_remainder(polynomial_ref const & p,polynomial_ref const & q,unsigned & d)1347 inline polynomial_ref pseudo_remainder(polynomial_ref const & p, polynomial_ref const & q, unsigned & d) {
1348 return pseudo_remainder(p, q, max_var(q), d);
1349 }
1350
exact_pseudo_division(polynomial_ref const & p,polynomial_ref const & q,polynomial::var x,polynomial_ref & R)1351 inline polynomial_ref exact_pseudo_division(polynomial_ref const & p, polynomial_ref const & q, polynomial::var x,
1352 polynomial_ref & R) {
1353 polynomial::manager & m = p.m();
1354 polynomial_ref Q(m);
1355 m.exact_pseudo_division(p, q, x, Q, R);
1356 return polynomial_ref(Q);
1357 }
1358
exact_pseudo_division(polynomial_ref const & p,polynomial_ref const & q,polynomial_ref & R)1359 inline polynomial_ref exact_pseudo_division(polynomial_ref const & p, polynomial_ref const & q, polynomial_ref & R) {
1360 return exact_pseudo_division(p, q, max_var(q), R);
1361 }
1362
pseudo_division(polynomial_ref const & p,polynomial_ref const & q,polynomial::var x,unsigned & d,polynomial_ref & R)1363 inline polynomial_ref pseudo_division(polynomial_ref const & p, polynomial_ref const & q, polynomial::var x, unsigned & d, polynomial_ref & R) {
1364 polynomial::manager & m = p.m();
1365 polynomial_ref Q(m);
1366 m.pseudo_division(p, q, x, d, Q, R);
1367 return polynomial_ref(Q);
1368 }
1369
pseudo_division(polynomial_ref const & p,polynomial_ref const & q,unsigned & d,polynomial_ref & R)1370 inline polynomial_ref pseudo_division(polynomial_ref const & p, polynomial_ref const & q, unsigned & d, polynomial_ref & R) {
1371 return pseudo_division(p, q, max_var(q), d, R);
1372 }
1373
quasi_resultant(polynomial_ref const & p,polynomial_ref const & q,unsigned x)1374 inline polynomial_ref quasi_resultant(polynomial_ref const & p, polynomial_ref const & q, unsigned x) {
1375 polynomial::manager & m = p.m();
1376 polynomial_ref r(m);
1377 m.quasi_resultant(p, q, x, r);
1378 return polynomial_ref(r);
1379 }
1380
resultant(polynomial_ref const & p,polynomial_ref const & q,unsigned x)1381 inline polynomial_ref resultant(polynomial_ref const & p, polynomial_ref const & q, unsigned x) {
1382 polynomial::manager & m = p.m();
1383 polynomial_ref r(m);
1384 m.resultant(p, q, x, r);
1385 return polynomial_ref(r);
1386 }
1387
discriminant(polynomial_ref const & p,unsigned x)1388 inline polynomial_ref discriminant(polynomial_ref const & p, unsigned x) {
1389 polynomial::manager & m = p.m();
1390 polynomial_ref r(m);
1391 m.discriminant(p, x, r);
1392 return polynomial_ref(r);
1393 }
1394
is_pos(polynomial_ref const & p)1395 inline bool is_pos(polynomial_ref const & p) {
1396 return p.m().is_pos(p);
1397 }
1398
is_neg(polynomial_ref const & p)1399 inline bool is_neg(polynomial_ref const & p) {
1400 return p.m().is_neg(p);
1401 }
1402
is_nonpos(polynomial_ref const & p)1403 inline bool is_nonpos(polynomial_ref const & p) {
1404 return p.m().is_nonpos(p);
1405 }
1406
is_nonneg(polynomial_ref const & p)1407 inline bool is_nonneg(polynomial_ref const & p) {
1408 return p.m().is_nonneg(p);
1409 }
1410
1411 inline void factor(polynomial_ref const & p, polynomial::factors & r, polynomial::factor_params const & params = polynomial::factor_params()) {
1412 p.m().factor(p, r, params);
1413 }
1414
1415 std::ostream & operator<<(std::ostream & out, polynomial_ref_vector const & seq);
1416
1417