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))
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) {
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;
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;
Term _simplify_tmpOldDominator
Temporary variable used in simplify.
void clearIdealAndSubtract()
Clears getIdeal() and getSubtract() and does not change getMultiply().
int getGradeSign(size_t var) const
Returns 1 if the grade strictly increases with the exponent of var, returns -1 if it strictly decreas...
Eliminate non-improving slices, achieving a branch-and-bound algorithm in place of the usual backtrac...
static bool isIdentity(const Exponent *a, size_t varCount)
Returns whether a is 1, i.e. whether all entries of a are 0.
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.
const Ideal & getMaximalSolutions()
Returns one of or all of the msm's with optimal value found so far, depending on the value of reportA...
size_t getVarCount() const
size_t getVarCount() const
Returns the number of variables in the ambient ring.
virtual void setUseIndependence(bool use)
This method should only be called before calling run().
A SplitStrategy is an implementation of a split selection strategy for the Slice Algorithm.
Term _boundSimplify_tmpPivot
Temporary variable used in simplify.
mpz_class _consume_tmpDegree
Temporary variable used in consume.
const Term & getLcm() const
Returns the least common multiple of the generators of getIdeal().
virtual void outerSlice(const Term &pivot)
Sets this object to the outer slice according to pivot.
virtual bool innerSlice(const Term &pivot)
Sets this object to the inner slice according to pivot.
This class represents a slice, which is the central data structure of the Slice Algorithm.
virtual void getPivot(Term &pivot, Slice &slice)
Used by pivotSplit to obtain a pivot.
Exponent getMaxExponent(size_t var) const
size_t getVarCount() const
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.
mpz_class getDegree(const Term &term) const
Returns the degree of term.
const mpz_class & getMaximalValue()
The optimal value associated to all entries from getMaximalSolutions().
virtual void consume(const Term &term)
Consume a term.
Represents a monomial ideal with int exponents.
void lcm(Word *res, const Word *resEnd, const Word *a, const Word *b)
virtual void beginConsuming()
Tell the consumer to begin consuming an ideal.
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...
A TermGrader assigns a value, the degree, to each monomial.
virtual bool simplify(Slice &slice)
This method calls MsmStrategy::simplify to perform the usual simplification of slice, which then occurs if and only if the usual simplification has been turned on.
Ideal _maxSolutions
Stores the optimal solutions found so far, according to the best value found so far.
OptimizeStrategy(TermGrader &grader, const SplitStrategy *splitStrategy, bool reportAllSolutions, BoundSetting boundSetting)
Construct an OptimizeStrategy.
Term & getMultiply()
Returns for a slice .
mpz_class _simplify_tmpUpperBound
Temporary variable used in simplify.
const TermGrader & _grader
We use _grader to assign values to solutions.
virtual void doneConsuming()
Must be called once after each time beginConsuming has been called.
size_t getGeneratorCount() const
Make no use of the bound.
mpz_class _maxValueToBeat
Is equal to _maxValue minus _reportAllSolutions, except when no solution has been found so far...
static bool divides(const Exponent *a, const Exponent *b, size_t varCount)
Returns whether a divides b.
BoundSetting _boundSetting
Indicates how to use the bound.
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_tmpDominator
Temporary variable used in simplify.
mpz_class _maxValue
The best value of any solution found so far.
const Ideal & getIdeal() const
Returns for a slice .
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.
Eliminate non-improving slices and simplify slices by trying to generate non-improving slices that ar...
mpz_class _tmpC
Temporary variable used in getInnerSimplify and getOuterSimplify.
BoundSetting
The values of BoundSetting indicate how to use the bound.
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...
static void setToIdentity(Exponent *res, size_t varCount)
Set res equal to , i.e. set each entry of res equal to 0.
bool _reportAllSolutions
Indicates whether to compute all optimal solutions, as opposed to computing just one (when there are ...
virtual bool simplify(Slice &slice)
Simplifies slice and returns true if it changed.
size_t getVarCount() const
The number of varibles this object was initialized with.
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.
void insert(const Exponent *term)
virtual void getPivot(Term &pivot, Slice &slice)
Used by pivotSplit to obtain a pivot.
bool getDominator(Slice &slice, Term &dominator)
Sets dominator to be a term dominating every element of the content of slice.
Term _simplify_tmpOldDivisor
Temporary variable used in simplify.
Term represents a product of variables which does not include a coefficient.
const mpz_class & getGrade(size_t var, Exponent exponent) const
virtual void setUseIndependence(bool use)
Independence splits are not supported, so calling this method does nothing.