26 _grades(varDegrees.size()) {
29 _signs.resize(varDegrees.size());
30 for (
size_t var = 0; var < varDegrees.size(); ++var) {
31 if (varDegrees[var] > 0)
33 else if (varDegrees[var] < 0)
38 for (
size_t var = 0; var < varDegrees.size(); ++var) {
39 size_t maxId = translator.
getMaxId(var);
42 for (
Exponent e = 0; e <= maxId; ++e)
56 for (
size_t var = 0; var < term.
getVarCount(); ++var)
62 mpz_class& degree)
const {
65 for (
size_t var = 0; var < term.
getVarCount(); ++var)
70 const Term& dominator,
71 mpz_class& bound)
const {
78 for (
size_t var = 0; var < varCount; ++var) {
88 optimalExponent = div;
98 optimalExponent = dom - 1;
100 optimalExponent = dom;
109 optimalExponent = dom;
111 optimalExponent = div;
114 bound +=
getGrade(var, optimalExponent);
119 const Term& dominator)
const {
130 const mpz_class& maxDegree)
const {
140 const mpz_class& exp =
_grades[var][e];
141 if (exp <= maxDegree) {
157 const mpz_class& maxDegree)
const {
167 const mpz_class& exp =
_grades[var][e];
168 if (exp <= maxDegree) {
180 (
size_t var,
const mpz_class& value,
bool strict)
const {
187 for (
size_t e = 1; e <
_grades[var].size(); ++e) {
188 const mpz_class& exp =
_grades[var][e];
190 if (exp <= value && (first || exp >
_grades[var][best])) {
200 const mpz_class& value,
bool strict)
const {
207 bool positive = sign > 0;
223 size_t gap = high - low;
231 if (lowDelta < gap) {
235 pivot = low + lowDelta + 1;
240 pivot = low + (gap + 1) / 2;
245 if (positive ?
getGrade(var, pivot) <= value :
getGrade(var, pivot) >= value) {
256 if (reference < from)
268 mpz_class& degree)
const {
271 for (
size_t var = 0; var < term.
getVarCount(); ++var)
284 return _grades[var].size() - 1;
292 out <<
"TermGrader (\n";
293 for (
size_t var = 0; var <
_grades.size(); ++var) {
294 out <<
" var " << var <<
':';
295 for (
size_t e = 0; e <
_grades[var].size(); ++e)
ostream & operator<<(ostream &out, const TermGrader &grader)
size_t inverseProjectVar(size_t rangeVar) const
size_t getRangeVarCount() const
A TermGrader assigns a value, the degree, to each monomial.
void getIncrementedDegree(const Term &term, const Projection &projection, mpz_class °ree) const
void print(ostream &out) const
Exponent getLargestLessThan2(size_t var, const mpz_class &value, bool strict=true) const
Returns the index of the largest stored exponent of var that is less than value.
mpz_class getDegree(const Term &term) const
Returns the degree of term.
size_t getVarCount() const
Exponent getMaxExponent(size_t var) const
TermGrader(const vector< mpz_class > &varDegrees, const TermTranslator &translator)
bool getMaxIndexLessThan(size_t var, Exponent from, Exponent to, Exponent &index, const mpz_class &maxDegree) const
Finds maximal index in [from, to] to such that degree(t) <= maxDegree.
void getUpperBound(const Term &divisor, const Term &dominator, mpz_class &bound) const
Assigns to bound the degree of the largest term v such that divisor divides v and v divides dominator...
bool getMinIndexLessThan(size_t var, Exponent from, Exponent to, Exponent &index, const mpz_class &maxDegree) const
Finds minimal index in [from, to] to such that degree(t) <= maxDegree.
int getGradeSign(size_t var) const
Returns 1 if the grade strictly increases with the exponent of var, returns -1 if it strictly decreas...
const mpz_class & getGrade(size_t var, Exponent exponent) const
vector< vector< mpz_class > > _grades
TermTranslator handles translation between terms whose exponents are infinite precision integers and ...
const mpz_class & getExponent(size_t variable, Exponent exponent) const
This method translates from IDs to arbitrary precision integers.
Exponent getMaxId(size_t variable) const
The assigned IDs are those in the range [0, getMaxId(var)].
Term represents a product of variables which does not include a coefficient.
size_t getVarCount() const
static bool divides(const Exponent *a, const Exponent *b, size_t varCount)
Returns whether a divides b.