25 bool reportAllSolutions,
29 _maxSolutions(grader.getVarCount()),
30 _reportAllSolutions(reportAllSolutions),
31 _boundSetting(boundSetting),
33 _simplify_tmpDominator(grader.getVarCount()),
34 _simplify_tmpOldDominator(grader.getVarCount()),
35 _simplify_tmpOldDivisor(grader.getVarCount()),
36 _boundSimplify_tmpPivot(grader.getVarCount()) {
99 bool changedSlice =
false;
100 for (
bool firstLoop =
true; true ; firstLoop =
false) {
122 if (firstLoop && changed) {
126 return changedSlice || changed;
131 oldDominator = dominator;
138 (oldDivisor, oldDominator, slice.
getMultiply(), dominator))
148 (oldDivisor, oldDominator, slice.
getMultiply(), dominator))
160 (
const Term& oldDivisor,
const Term& oldDominator,
161 const Term& newDivisor,
const Term& newDominator)
const {
172 if (oldDivisor[var] == newDivisor[var] &&
173 oldDominator[var] == newDominator[var])
178 if (newDivisor[var] > oldDivisor[var])
181 ASSERT(newDivisor[var] == oldDivisor[var]);
182 ASSERT(newDominator[var] < oldDominator[var]);
186 }
else if (sign > 0) {
187 if (newDominator[var] < oldDominator[var]) {
191 ASSERT(newDominator[var] == oldDominator[var]);
192 ASSERT(newDivisor[var] > oldDivisor[var]);
193 if (newDivisor[var] == newDominator[var] &&
205 const Term& dominator,
206 const mpz_class& upperBound) {
221 (
const Term& divisor,
222 const Term& dominator,
223 const mpz_class& upperBound,
226 bool simplifiedAny =
false;
230 ASSERT(divisor[var] <= dominator[var]);
233 if (divisor[var] == dominator[var])
242 B = dominator[var] - 1;
243 if (divisor[var] == B)
252 (var, divisor[var], B - 1, tPrime,
_tmpC);
254 if (foundNonImproving) {
255 simplifiedAny =
true;
256 pivot[var] = tPrime - divisor[var] + 1;
259 }
else if (sign < 0) {
266 simplifiedAny =
true;
267 pivot[var] = dominator[var] - divisor[var];
274 return simplifiedAny;
278 (
const Term& divisor,
279 const Term& dominator,
280 const mpz_class& upperBound,
286 ASSERT(divisor[var] <= dominator[var]);
287 if (divisor[var] == dominator[var])
300 (var, divisor[var] + 1, dominator[var], tPrime,
_tmpC);
302 if (foundNonImproving) {
304 pivot[var] = tPrime - divisor[var];
309 }
else if (sign > 0) {
318 pivot[var] = dominator[var] - divisor[var];
338 for (
size_t var = 0; var < dominator.
getVarCount(); ++var) {
344 dominator[var] = multiply[var] +
lcm[var] - 1;
Represents a monomial ideal with int exponents.
size_t getGeneratorCount() const
void insert(const Exponent *term)
virtual void getPivot(Term &pivot, Slice &slice)
Used by pivotSplit to obtain a pivot.
bool getOuterSimplify(const Term &divisor, const Term &dominator, const mpz_class &upperBound, Term &pivot)
Find an inner slice that is non-improving, allowing us to replace the current slice with the outer sl...
Term _simplify_tmpOldDivisor
Temporary variable used in simplify.
const TermGrader & _grader
We use _grader to assign values to solutions.
BoundSetting
The values of BoundSetting indicate how to use the bound.
@ DoNotUseBound
Make no use of the bound.
@ UseBoundToEliminateAndSimplify
Eliminate non-improving slices and simplify slices by trying to generate non-improving slices that ar...
@ UseBoundToEliminate
Eliminate non-improving slices, achieving a branch-and-bound algorithm in place of the usual backtrac...
const Ideal & getMaximalSolutions()
Returns one of or all of the msm's with optimal value found so far, depending on the value of reportA...
OptimizeStrategy(TermGrader &grader, const SplitStrategy *splitStrategy, bool reportAllSolutions, BoundSetting boundSetting)
Construct an OptimizeStrategy.
bool boundSimplify(Slice &slice, const Term &dominator, const mpz_class &upperBound)
This method simplifies a slice based on generating non-improving outer and inner slices.
Ideal _maxSolutions
Stores the optimal solutions found so far, according to the best value found so far.
bool getDominator(Slice &slice, Term &dominator)
Sets dominator to be a term dominating every element of the content of slice.
virtual void getPivot(Term &pivot, Slice &slice)
Used by pivotSplit to obtain a pivot.
Term _boundSimplify_tmpPivot
Temporary variable used in simplify.
const mpz_class & getMaximalValue()
The optimal value associated to all entries from getMaximalSolutions().
mpz_class _simplify_tmpUpperBound
Temporary variable used in simplify.
mpz_class _maxValue
The best value of any solution found so far.
virtual void consume(const Term &term)
Consume a term.
Term _simplify_tmpOldDominator
Temporary variable used in simplify.
Term _simplify_tmpDominator
Temporary variable used in simplify.
bool _reportAllSolutions
Indicates whether to compute all optimal solutions, as opposed to computing just one (when there are ...
bool changedInWayRelevantToBound(const Term &oldDivisor, const Term &oldDominator, const Term &newDivisor, const Term &newDominator) const
Returns true if iterating bound-based simplification might do something.
virtual void beginConsuming()
Tell the consumer to begin consuming an ideal.
virtual void doneConsuming()
Must be called once after each time beginConsuming has been called.
virtual void setUseIndependence(bool use)
Independence splits are not supported, so calling this method does nothing.
size_t getVarCount() const
The number of varibles this object was initialized with.
mpz_class _maxValueToBeat
Is equal to _maxValue minus _reportAllSolutions, except when no solution has been found so far,...
virtual bool simplify(Slice &slice)
This method calls MsmStrategy::simplify to perform the usual simplification of slice,...
mpz_class _tmpC
Temporary variable used in getInnerSimplify and getOuterSimplify.
BoundSetting _boundSetting
Indicates how to use the bound.
mpz_class _consume_tmpDegree
Temporary variable used in consume.
bool getInnerSimplify(const Term &divisor, const Term &dominator, const mpz_class &upperBound, Term &pivot)
Find an outer slice that is non-improving, allowing us to replace the current slice with the inner sl...
virtual void setUseIndependence(bool use)
This method should only be called before calling run().
virtual bool simplify(Slice &slice)
Simplifies slice and returns true if it changed.
This class represents a slice, which is the central data structure of the Slice Algorithm.
virtual bool innerSlice(const Term &pivot)
Sets this object to the inner slice according to pivot.
virtual void outerSlice(const Term &pivot)
Sets this object to the outer slice according to pivot.
const Ideal & getIdeal() const
Returns for a slice .
void clearIdealAndSubtract()
Clears getIdeal() and getSubtract() and does not change getMultiply().
Term & getMultiply()
Returns for a slice .
const Term & getLcm() const
Returns the least common multiple of the generators of getIdeal().
size_t getVarCount() const
Returns the number of variables in the ambient ring.
A SplitStrategy is an implementation of a split selection strategy for the Slice Algorithm.
A TermGrader assigns a value, the degree, to each monomial.
mpz_class getDegree(const Term &term) const
Returns the degree of term.
size_t getVarCount() const
Exponent getMaxExponent(size_t var) const
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
Term represents a product of variables which does not include a coefficient.
size_t getVarCount() const
static bool isIdentity(const Exponent *a, size_t varCount)
Returns whether a is 1, i.e. whether all entries of a are 0.
static bool divides(const Exponent *a, const Exponent *b, size_t varCount)
Returns whether a divides b.
static void setToIdentity(Exponent *res, size_t varCount)
Set res equal to , i.e. set each entry of res equal to 0.
void lcm(Word *res, const Word *resEnd, const Word *a, const Word *b)