SatBinomIdeal.cpp
Go to the documentation of this file.
/* Frobby: Software for monomial ideal computations.
Copyright (C) 2009 Bjarke Hammersholt Roune (www.broune.com)
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see http://www.gnu.org/licenses/.
*/
#include "stdinc.h"
#include "SatBinomIdeal.h"
#include "BigIdeal.h"
#include "Matrix.h"
#include <sstream>
#include <limits>
SatBinomIdeal::SatBinomIdeal() {
}
SatBinomIdeal::SatBinomIdeal(const VarNames& names):
_names(names) {
}
void SatBinomIdeal::insert(const vector<mpz_class>& binom) {
ASSERT(binom.size() == getVarCount());
_gens.push_back(binom);
}
const vector<mpz_class>& SatBinomIdeal::getGenerator(size_t index) const {
ASSERT(index < getGeneratorCount());
return _gens[index];
}
size_t SatBinomIdeal::getGeneratorCount() const {
return _gens.size();
}
void SatBinomIdeal::print(FILE* out) const {
ostringstream tmp;
print(tmp);
fputs(tmp.str().c_str(), out);
}
void SatBinomIdeal::print(ostream& out) const {
out << "/---- SatBinomIdeal of " << _gens.size() << " generators:\n";
for (vector<vector<mpz_class> >::const_iterator it = _gens.begin();
it != _gens.end(); ++it) {
for (vector<mpz_class>::const_iterator entry = it->begin();
entry != it->end(); ++entry)
out << *entry << ' ';
out << '\n';
}
out << "----/ End of list.\n";
}
void SatBinomIdeal::clearAndSetNames(const VarNames& names) {
_gens.clear();
_names = names;
}
size_t SatBinomIdeal::getVarCount() const {
return _names.getVarCount();
}
void SatBinomIdeal::renameVars(const VarNames& names) {
ASSERT(names.getVarCount() == getVarCount());
_names = names;
}
const VarNames& SatBinomIdeal::getNames() const {
return _names;
}
void SatBinomIdeal::clear() {
_gens.clear();
_names.clear();
}
void SatBinomIdeal::reserve(size_t size) {
_gens.reserve(size);
}
void SatBinomIdeal::removeGeneratorsWithLeadingZero() {
size_t gen = 0;
while (gen < getGeneratorCount()) {
if (getGenerator(gen)[0] == 0) {
_gens[gen] = _gens.back();
_gens.pop_back();
} else
++gen;
}
}
void SatBinomIdeal::removeGeneratorsWithoutLeadingZero() {
size_t gen = 0;
while (gen < getGeneratorCount()) {
if (getGenerator(gen)[0] != 0) {
_gens[gen] = _gens.back();
_gens.pop_back();
} else
++gen;
}
}
void SatBinomIdeal::getInitialIdeal(BigIdeal& ideal) const {
ideal.clearAndSetNames(getNames());
ideal.reserve(getGeneratorCount());
for (size_t gen = 0; gen < getGeneratorCount(); ++gen) {
ideal.newLastTerm();
for (size_t var = 0; var < getVarCount(); ++var)
if (getGenerator(gen)[var] > 0)
ideal.getLastTermExponentRef(var) = getGenerator(gen)[var];
}
}
vector<mpz_class>& SatBinomIdeal::getLastBinomRef() {
ASSERT(!_gens.empty());
return _gens.back();
}
void SatBinomIdeal::newLastTerm() {
_gens.resize(_gens.size() + 1);
_gens.back().resize(_names.getVarCount());
}
bool SatBinomIdeal::hasZeroEntry() const {
for (size_t gen = 0; gen < getGeneratorCount(); ++gen)
for (size_t var = 0; var < getVarCount(); ++var)
if (getGenerator(gen)[var] == 0)
return true;
return false;
}
bool SatBinomIdeal::initialIdealIsWeaklyGeneric() const {
vector<mpz_class> v(getVarCount());
for (size_t gen1 = 0; gen1 < getGeneratorCount(); ++gen1) {
for (size_t gen2 = gen1 + 1; gen2 < getGeneratorCount(); ++gen2) {
const vector<mpz_class>& g1 = getGenerator(gen1);
const vector<mpz_class>& g2 = getGenerator(gen2);
// Skip if g1 and g2 are different in each entry.
bool sharesEntry = false;
for (size_t var = 0; var < getVarCount(); ++var) {
if (g1[var] == g2[var] && g1[var] > 0) {
sharesEntry = true;
break;
}
}
if (!sharesEntry)
continue;
if (isPointFreeBody(g1, g2))
return false;
}
}
return true;
}
bool SatBinomIdeal::isPointFreeBody(const vector<mpz_class>& a,
const vector<mpz_class>& b) const {
ASSERT(a.size() == getVarCount());
ASSERT(b.size() == getVarCount());
vector<mpz_class> rhs(getVarCount());
// Set rhs to max(0,g1,g2)-1.
for (size_t var = 0; var < getVarCount(); ++var) {
rhs[var] = a[var] > b[var] ? a[var] : b[var];
if (rhs[var] < 0)
rhs[var] = 0;
rhs[var] -= 1;
}
return !isDominating(rhs);
}
bool SatBinomIdeal::isPointFreeBody(const vector<mpz_class>& a,
const vector<mpz_class>& b,
const vector<mpz_class>& c) const {
ASSERT(a.size() == getVarCount());
ASSERT(b.size() == getVarCount());
vector<mpz_class> rhs(getVarCount());
// Set rhs to max(0,g1,g1+g2)-1.
for (size_t var = 0; var < getVarCount(); ++var) {
rhs[var] = a[var] > b[var] ? a[var] : b[var];
rhs[var] = rhs[var] > c[var] ? rhs[var] : c[var];
if (rhs[var] < 0)
rhs[var] = 0;
rhs[var] -= 1;
}
return !isDominating(rhs);
}
bool SatBinomIdeal::isInterior(const vector<mpz_class>& a,
const vector<mpz_class>& b) const {
ASSERT(a.size() == b.size());
if (!isPointFreeBody(a, b))
return false;
for (size_t var = 1; var < a.size(); ++var)
if (a[var] <= 0 && b[var] <= 0)
return false;
return true;
}
namespace {
bool hasCycle(size_t gen, vector<char>& color, const SatBinomIdeal& ideal) {
// 0 = Not seen before.
// 1 = Exploring now.
// 2 = Already explored. Does not lead to cycle.
if (color[gen] == 1)
return true;
if (color[gen] == 2)
return false;
color[gen] = 1;
for (size_t g = 0; g < ideal.getGeneratorCount(); ++g)
if (ideal.isInteriorEdge(gen, g) &&
!ideal.isTerminatingEdge(gen, g) &&
hasCycle(g, color, ideal))
return true;
color[gen] = 2;
return false;
}
}
bool SatBinomIdeal::validate() const {
// check the graph satisifies what we think it should.
bool generic = !hasZeroEntry();
if (!generic)
return true;
// termination.
vector<char> color(getGeneratorCount());
for (size_t gen = 0; gen < getGeneratorCount(); ++gen)
if (hasCycle(gen, color, *this))
return false;
// out-degree 1 when generic
for (size_t from = 0; from < getGeneratorCount(); ++from) {
const vector<mpz_class>& fromGen = getGenerator(from);
size_t outDegree = 0;
for (size_t to = 0; to < getGeneratorCount(); ++to) {
if (isInteriorEdge(from, to))
++outDegree;
}
if (isInterior(fromGen, fromGen)) {
if (outDegree != 0)
return false;
} else {
if (outDegree != 1)
return false;
}
}
return true;
}
bool SatBinomIdeal::isInteriorEdge(size_t from, size_t to) const {
const vector<mpz_class>& fromGen = getGenerator(from);
const vector<mpz_class>& toGen = getGenerator(to);
if (isInterior(fromGen, fromGen))
return false;
if (isInterior(toGen, toGen))
return false;
vector<mpz_class> sum(fromGen.size());
for (size_t var = 0; var < fromGen.size(); ++var)
sum[var] = fromGen[var] + toGen[var];
return isInterior(toGen, sum);
}
bool SatBinomIdeal::isTerminatingEdge(size_t from, size_t to) const {
if (!isInteriorEdge(from, to))
return false;
const vector<mpz_class> fromGen = getGenerator(from);
const vector<mpz_class> toGen = getGenerator(to);
vector<mpz_class> sum(fromGen.size());
for (size_t var = 0; var < fromGen.size(); ++var)
sum[var] = fromGen[var] + toGen[var];
return isPointFreeBody(fromGen, sum);
}
void SatBinomIdeal::getDoubleTriangleCount(mpz_class& count) const {
vector<mpz_class> sum(getVarCount());
count = 0;
for (size_t gen1 = 0; gen1 < getGeneratorCount(); ++gen1) {
for (size_t gen2 = gen1 + 1; gen2 < getGeneratorCount(); ++gen2) {
const vector<mpz_class>& g1 = getGenerator(gen1);
const vector<mpz_class>& g2 = getGenerator(gen2);
// Set sum = g1 + g2.
for (size_t var = 0; var < getVarCount(); ++var)
sum[var] = g1[var] + g2[var];
if (isPointFreeBody(g1, sum) && isPointFreeBody(g2, sum))
++count;
}
}
}
bool SatBinomIdeal::isGeneric() const {
return !hasZeroEntry() && initialIdealIsWeaklyGeneric();
}
SatBinomIdeal& SatBinomIdeal::operator=(const SatBinomIdeal& ideal) {
_gens = ideal._gens;
_names = ideal._names;
return *this;
}
bool SatBinomIdeal::isDominating(const vector<mpz_class>& v) const {
for (size_t gen = 0; gen < getGeneratorCount(); ++gen) {
bool dom = true;
for (size_t var = 0; var < getVarCount(); ++var) {
if (v[var] < getGenerator(gen)[var]) {
dom = false;
break;
}
}
if (dom)
return true;
}
return false;
}
bool SatBinomIdeal::isGenerator
(const vector<mpz_class>& v) const {
for (size_t gen = 0; gen < getGeneratorCount(); ++gen)
if (getGenerator(gen) == v)
return true;
return false;
}
void SatBinomIdeal::projectVar(size_t var) {
ASSERT(var < getVarCount());
for (size_t gen = 0; gen < getGeneratorCount(); ++gen)
_gens[gen].erase(_gens[gen].begin() + var);
_names.projectVar(var);
}
void SatBinomIdeal::getMatrix(Matrix& matrix) const {
matrix.resize(getGeneratorCount(), getVarCount());
for (size_t gen = 0; gen < getGeneratorCount(); ++gen)
for (size_t var = 0; var < getVarCount(); ++var)
matrix(gen, var) = _gens[gen][var];
}
BigIdeal.h
Matrix.h
SatBinomIdeal.h
BigIdeal
Definition BigIdeal.h:27
BigIdeal::reserve
void reserve(size_t capacity)
Definition BigIdeal.cpp:112
BigIdeal::clearAndSetNames
void clearAndSetNames(const VarNames &names)
Definition BigIdeal.cpp:222
BigIdeal::newLastTerm
void newLastTerm()
Definition BigIdeal.cpp:104
BigIdeal::getLastTermExponentRef
mpz_class & getLastTermExponentRef(size_t var)
Definition BigIdeal.h:126
Matrix
Definition Matrix.h:26
Matrix::resize
void resize(size_t rowCount, size_t colCount)
Set the number of rows and columns.
Definition Matrix.cpp:61
SatBinomIdeal
Represents a saturated binomial ideal.
Definition SatBinomIdeal.h:28
SatBinomIdeal::getDoubleTriangleCount
void getDoubleTriangleCount(mpz_class &count) const
Returns the number of pairs of generators a and b such that {0,a,a+b} and {0,b,a+b}...
Definition SatBinomIdeal.cpp:308
SatBinomIdeal::newLastTerm
void newLastTerm()
Definition SatBinomIdeal.cpp:135
SatBinomIdeal::isGeneric
bool isGeneric() const
Returns true if the generating set is generic, i.e.
Definition SatBinomIdeal.cpp:327
SatBinomIdeal::getLastBinomRef
vector< mpz_class > & getLastBinomRef()
Definition SatBinomIdeal.cpp:129
SatBinomIdeal::validate
bool validate() const
Temporary.
Definition SatBinomIdeal.cpp:246
SatBinomIdeal::isInterior
bool isInterior(const vector< mpz_class > &a, const vector< mpz_class > &b) const
Returns true if max(0,a,b) is strictly positive in every element.
Definition SatBinomIdeal.cpp:213
SatBinomIdeal::isPointFreeBody
bool isPointFreeBody(const vector< mpz_class > &a, const vector< mpz_class > &b) const
Returns true if the smallest body containing zero, a and b has no generator in its interior.
Definition SatBinomIdeal.cpp:175
SatBinomIdeal::isInteriorEdge
bool isInteriorEdge(size_t from, size_t to) const
Returns whether {to,to+from} is an interior edge of Top.
Definition SatBinomIdeal.cpp:280
SatBinomIdeal::print
void print(FILE *file) const
Definition SatBinomIdeal.cpp:49
SatBinomIdeal::renameVars
void renameVars(const VarNames &names)
Requires that names.getVarCount() equals getVarCount().
Definition SatBinomIdeal.cpp:76
SatBinomIdeal::getVarCount
size_t getVarCount() const
Definition SatBinomIdeal.cpp:72
SatBinomIdeal::isTerminatingEdge
bool isTerminatingEdge(size_t from, size_t to) const
Returns wehther {from,to+from} is an interior edge of Top and also {to,to+from} is an edge of Top (no...
Definition SatBinomIdeal.cpp:295
SatBinomIdeal::getGeneratorCount
size_t getGeneratorCount() const
Definition SatBinomIdeal.cpp:45
SatBinomIdeal::operator=
SatBinomIdeal & operator=(const SatBinomIdeal &ideal)
Definition SatBinomIdeal.cpp:331
SatBinomIdeal::insert
void insert(const vector< mpz_class > &binom)
Definition SatBinomIdeal.cpp:33
SatBinomIdeal::getNames
const VarNames & getNames() const
Definition SatBinomIdeal.cpp:82
SatBinomIdeal::getGenerator
const vector< mpz_class > & getGenerator(size_t index) const
Definition SatBinomIdeal.cpp:39
SatBinomIdeal::removeGeneratorsWithoutLeadingZero
void removeGeneratorsWithoutLeadingZero()
Definition SatBinomIdeal.cpp:106
SatBinomIdeal::reserve
void reserve(size_t size)
Definition SatBinomIdeal.cpp:91
SatBinomIdeal::_gens
vector< vector< mpz_class > > _gens
Definition SatBinomIdeal.h:122
SatBinomIdeal::hasZeroEntry
bool hasZeroEntry() const
Returns true if any generator does not involve every variable, i.e.
Definition SatBinomIdeal.cpp:140
SatBinomIdeal::removeGeneratorsWithLeadingZero
void removeGeneratorsWithLeadingZero()
Definition SatBinomIdeal.cpp:95
SatBinomIdeal::clearAndSetNames
void clearAndSetNames(const VarNames &names)
Definition SatBinomIdeal.cpp:67
SatBinomIdeal::isDominating
bool isDominating(const vector< mpz_class > &v) const
Returns true if any generator, considered as an integer vector, is dominated by v.
Definition SatBinomIdeal.cpp:337
SatBinomIdeal::getInitialIdeal
void getInitialIdeal(BigIdeal &ideal) const
Definition SatBinomIdeal.cpp:117
SatBinomIdeal::getMatrix
void getMatrix(Matrix &matrix) const
Definition SatBinomIdeal.cpp:368
SatBinomIdeal::projectVar
void projectVar(size_t var)
Definition SatBinomIdeal.cpp:360
SatBinomIdeal::clear
void clear()
Definition SatBinomIdeal.cpp:86
SatBinomIdeal::SatBinomIdeal
SatBinomIdeal()
Definition SatBinomIdeal.cpp:26
SatBinomIdeal::_names
VarNames _names
Definition SatBinomIdeal.h:123
SatBinomIdeal::initialIdealIsWeaklyGeneric
bool initialIdealIsWeaklyGeneric() const
Returns true if the initial ideal is weakly generic.
Definition SatBinomIdeal.cpp:148
SatBinomIdeal::isGenerator
bool isGenerator(const vector< mpz_class > &v) const
Returns true if v is a generator.
Definition SatBinomIdeal.cpp:353
VarNames
Defines the variables of a polynomial ring and facilities IO involving them.
Definition VarNames.h:40
VarNames::getVarCount
size_t getVarCount() const
Returns the current number of variables.
Definition VarNames.h:113
stdinc.h
This header file includes common definitions and is included as the first line of code in every imple...
ASSERT
#define ASSERT(X)
Definition stdinc.h:86