From d35d086268fa2a3d9b3c387157e4c54f1b967e0e Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 30 Mar 2011 01:06:37 +0000 Subject: Merged the branch sparse-tableau into trunk. --- src/theory/arith/Makefile.am | 2 - src/theory/arith/arithvar_set.h | 6 +- src/theory/arith/row_vector.cpp | 316 -------------------- src/theory/arith/row_vector.h | 233 --------------- src/theory/arith/simplex.cpp | 235 ++++++++------- src/theory/arith/simplex.h | 15 +- src/theory/arith/tableau.cpp | 599 ++++++++++++++++++++++++++++++-------- src/theory/arith/tableau.h | 367 ++++++++++++++++++----- src/theory/arith/theory_arith.cpp | 102 ++++--- src/theory/arith/theory_arith.h | 19 +- src/util/stats.h | 44 +++ 11 files changed, 1019 insertions(+), 919 deletions(-) delete mode 100644 src/theory/arith/row_vector.cpp delete mode 100644 src/theory/arith/row_vector.h diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 2c00f5d4d..12088b493 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -26,8 +26,6 @@ libarith_la_SOURCES = \ arith_priority_queue.cpp \ simplex.h \ simplex.cpp \ - row_vector.h \ - row_vector.cpp \ unate_propagator.h \ unate_propagator.cpp \ theory_arith.h \ diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h index 89b1c9507..0d59e3aea 100644 --- a/src/theory/arith/arithvar_set.h +++ b/src/theory/arith/arithvar_set.h @@ -57,7 +57,7 @@ private: std::vector d_posVector; public: - typedef VarList::const_iterator iterator; + typedef VarList::const_iterator const_iterator; ArithVarSetImpl() : d_list(), d_posVector() {} @@ -114,8 +114,8 @@ public: d_list.push_back(x); } - iterator begin() const{ return d_list.begin(); } - iterator end() const{ return d_list.end(); } + const_iterator begin() const{ return d_list.begin(); } + const_iterator end() const{ return d_list.end(); } const VarList& getList() const{ return d_list; diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp deleted file mode 100644 index 8edfb8612..000000000 --- a/src/theory/arith/row_vector.cpp +++ /dev/null @@ -1,316 +0,0 @@ - -#include "theory/arith/row_vector.h" - -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::arith; - -using namespace std; - -bool ReducedRowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) { - if(arr.size() >= 2){ - const_iterator curr = arr.begin(); - const_iterator end = arr.end(); - ArithVar prev = (*curr).getArithVar(); - ++curr; - for(;curr != end; ++curr){ - ArithVar v = (*curr).getArithVar(); - if(strictlySorted && prev > v) return false; - if(!strictlySorted && prev >= v) return false; - prev = v; - } - } - return true; -} - -ReducedRowVector::~ReducedRowVector(){ - //This executes before the super classes destructor RowVector, - // which will set this to 0. - Assert(d_rowCount[basic()] == 1); - - const_iterator curr = begin(); - const_iterator endEntries = end(); - for(;curr != endEntries; ++curr){ - ArithVar v = (*curr).getArithVar(); - Assert(d_rowCount[v] >= 1); - d_columnMatrix[v].remove(basic()); - --(d_rowCount[v]); - } - - Assert(matchingCounts()); -} - - -bool ReducedRowVector::matchingCounts() const{ - for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ - ArithVar v = (*i).getArithVar(); - if(d_columnMatrix[v].size() != d_rowCount[v]){ - return false; - } - } - return true; -} - -bool ReducedRowVector::noZeroCoefficients(const VarCoeffArray& arr){ - for(const_iterator curr = arr.begin(), endEntries = arr.end(); - curr != endEntries; ++curr){ - const Rational& coeff = (*curr).getCoefficient(); - if(coeff == 0) return false; - } - return true; -} - -void ReducedRowVector::zip(const std::vector< ArithVar >& variables, - const std::vector< Rational >& coefficients, - VarCoeffArray& output){ - - Assert(coefficients.size() == variables.size() ); - - vector::const_iterator coeffIter = coefficients.begin(); - vector::const_iterator coeffEnd = coefficients.end(); - vector::const_iterator varIter = variables.begin(); - - for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){ - const Rational& coeff = *coeffIter; - ArithVar var_i = *varIter; - - output.push_back(VarCoeffPair(var_i, coeff)); - } -} - -void ReducedRowVector::addArithVar(ArithVarContainsSet& contains, ArithVar v){ - if(v >= contains.size()){ - contains.resize(v+1, false); - } - contains[v] = true; -} - -void ReducedRowVector::removeArithVar(ArithVarContainsSet& contains, ArithVar v){ - Assert(v < contains.size()); - Assert(contains[v]); - contains[v] = false; -} - -void ReducedRowVector::multiply(const Rational& c){ - Assert(c != 0); - - for(iterator i = d_entries.begin(), end = d_entries.end(); i != end; ++i){ - (*i).getCoefficient() *= c; - } -} - -void ReducedRowVector::addRowTimesConstant(const Rational& c, const ReducedRowVector& other){ - Assert(c != 0); - Assert(d_buffer.empty()); - Assert(wellFormed()); - - d_buffer.reserve(other.d_entries.size()); - - iterator curr1 = d_entries.begin(); - iterator end1 = d_entries.end(); - - const_iterator curr2 = other.d_entries.begin(); - const_iterator end2 = other.d_entries.end(); - - while(curr1 != end1 && curr2 != end2){ - ArithVar var1 = (*curr1).getArithVar(); - ArithVar var2 = (*curr2).getArithVar(); - - if(var1 < var2){ - d_buffer.push_back(*curr1); - ++curr1; - }else if(var1 > var2){ - - ++d_rowCount[var2]; - d_columnMatrix[var2].add(d_basic); - - addArithVar(d_contains, var2); - const Rational& coeff2 = (*curr2).getCoefficient(); - d_buffer.push_back( VarCoeffPair(var2, c * coeff2)); - ++curr2; - }else{ - Assert(var1 == var2); - const Rational& coeff1 = (*curr1).getCoefficient(); - const Rational& coeff2 = (*curr2).getCoefficient(); - Rational res = coeff1 + (c * coeff2); - if(res != 0){ - //The variable is not new so the count stays the same - d_buffer.push_back(VarCoeffPair(var1, res)); - }else{ - removeArithVar(d_contains, var1); - - --d_rowCount[var1]; - d_columnMatrix[var1].remove(d_basic); - } - ++curr1; - ++curr2; - } - } - while(curr1 != end1){ - d_buffer.push_back(*curr1); - ++curr1; - } - while(curr2 != end2){ - ArithVar var2 = (*curr2).getArithVar(); - const Rational& coeff2 = (*curr2).getCoefficient(); - ++d_rowCount[var2]; - d_columnMatrix[var2].add(d_basic); - - addArithVar(d_contains, var2); - - d_buffer.push_back(VarCoeffPair(var2, c * coeff2)); - ++curr2; - } - - d_buffer.swap(d_entries); - d_buffer.clear(); - - Assert(d_buffer.empty()); -} - -void ReducedRowVector::printRow(){ - for(const_iterator i = begin(); i != end(); ++i){ - ArithVar nb = (*i).getArithVar(); - const Rational& coeff = (*i).getCoefficient(); - Debug("row::print") << "{" << nb << "," << coeff << "}"; - } - Debug("row::print") << std::endl; -} - - -ReducedRowVector::ReducedRowVector(ArithVar basic, - const std::vector& variables, - const std::vector& coefficients, - std::vector& counts, - std::vector& cm): - d_basic(basic), d_rowCount(counts), d_columnMatrix(cm) -{ - zip(variables, coefficients, d_entries); - d_entries.push_back(VarCoeffPair(basic, Rational(-1))); - - std::sort(d_entries.begin(), d_entries.end()); - - for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ - ArithVar var = (*i).getArithVar(); - ++d_rowCount[var]; - addArithVar(d_contains, var); - d_columnMatrix[var].add(d_basic); - } - - Assert(isSorted(d_entries, true)); - Assert(noZeroCoefficients(d_entries)); - - Assert(matchingCounts()); - Assert(wellFormed()); - Assert(d_rowCount[d_basic] == 1); -} - -void ReducedRowVector::substitute(const ReducedRowVector& row_s){ - ArithVar x_s = row_s.basic(); - - Assert(has(x_s)); - Assert(x_s != basic()); - - Rational a_rs = lookup(x_s); - Assert(a_rs != 0); - - addRowTimesConstant(a_rs, row_s); - - - Assert(!has(x_s)); - Assert(wellFormed()); - Assert(matchingCounts()); - Assert(d_rowCount[basic()] == 1); -} - -void ReducedRowVector::pivot(ArithVar x_j){ - Assert(has(x_j)); - Assert(basic() != x_j); - Rational negInverseA_rs = -(lookup(x_j).inverse()); - multiply(negInverseA_rs); - - for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ - ArithVar var = (*i).getArithVar(); - d_columnMatrix[var].remove(d_basic); - d_columnMatrix[var].add(x_j); - } - - d_basic = x_j; - - Assert(matchingCounts()); - Assert(wellFormed()); - //The invariant Assert(d_rowCount[basic()] == 1); does not hold. - //This is because the pivot is within the row first then - //is moved through the propagated through the rest of the tableau. -} - - -Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{ - using namespace CVC4::kind; - - Assert(size() >= 2); - - vector nonBasicPairs; - for(const_iterator i = begin(); i != end(); ++i){ - ArithVar nb = (*i).getArithVar(); - if(nb == basic()) continue; - Node var = (map.find(nb))->second; - Node coeff = mkRationalNode((*i).getCoefficient()); - - Node mult = NodeBuilder<2>(MULT) << coeff << var; - nonBasicPairs.push_back(mult); - } - - Node sum = Node::null(); - if(nonBasicPairs.size() == 1 ){ - sum = nonBasicPairs.front(); - }else{ - Assert(nonBasicPairs.size() >= 2); - NodeBuilder<> sumBuilder(PLUS); - sumBuilder.append(nonBasicPairs); - sum = sumBuilder; - } - Node basicVar = (map.find(basic()))->second; - return NodeBuilder<2>(EQUAL) << basicVar << sum; - - /* - Node sum = Node::null(); - if(size() > 2){ - NodeBuilder<> sumBuilder(PLUS); - - for(const_iterator i = begin(); i != end(); ++i){ - ArithVar nb = (*i).getArithVar(); - if(nb == basic()) continue; - Node var = (map.find(nb))->second; - Node coeff = mkRationalNode((*i).getCoefficient()); - - Node mult = NodeBuilder<2>(MULT) << coeff << var; - sumBuilder << mult; - } - sum = sumBuilder; - }else{ - Assert(size() == 2); - const_iterator i = begin(); - if((*i).getArithVar() == basic()){ - ++i; - } - Assert((*i).getArithVar() != basic()); - Node var = (map.find((*i).getArithVar()))->second; - Node coeff = mkRationalNode((*i).getCoefficient()); - sum = NodeBuilder<2>(MULT) << coeff << var; - } - Node basicVar = (map.find(basic()))->second; - return NodeBuilder<2>(EQUAL) << basicVar << sum; -*/ -} - -void ReducedRowVector::enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,std::vector< Rational >& coefficients) const{ - for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ - ArithVar var = (*i).getArithVar(); - const Rational& q = (*i).getCoefficient(); - if(var != basic()){ - variables.push_back(var); - coefficients.push_back(q); - } - } -} diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h deleted file mode 100644 index 5fd471700..000000000 --- a/src/theory/arith/row_vector.h +++ /dev/null @@ -1,233 +0,0 @@ - - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__ARITH__ROW_VECTOR_H -#define __CVC4__THEORY__ARITH__ROW_VECTOR_H - -#include "theory/arith/arith_utilities.h" -#include "theory/arith/arithvar_set.h" -#include "util/rational.h" -#include - -namespace CVC4 { -namespace theory { -namespace arith { - -class VarCoeffPair { -private: - ArithVar d_variable; - Rational d_coeff; - -public: - VarCoeffPair(ArithVar v, const Rational& q): d_variable(v), d_coeff(q) {} - - ArithVar getArithVar() const { return d_variable; } - Rational& getCoefficient() { return d_coeff; } - const Rational& getCoefficient() const { return d_coeff; } - - bool operator<(const VarCoeffPair& other) const{ - return getArithVar() < other.getArithVar(); - } - - static bool variableLess(const VarCoeffPair& a, const VarCoeffPair& b){ - return a < b; - } -}; - -/** - * ReducedRowVector is a sparse vector representation that represents the - * row as a strictly sorted array of "VarCoeffPair"s. - * The row has a notion of a basic variable. - * This is a variable that must have a coefficient of -1 in the array. - */ -class ReducedRowVector { -public: - typedef std::vector VarCoeffArray; - typedef VarCoeffArray::const_iterator const_iterator; - -private: - typedef std::vector ArithVarContainsSet; - typedef VarCoeffArray::iterator iterator; - - /** - * Invariants: - * - isSorted(d_entries, true) - * - noZeroCoefficients(d_entries) - */ - VarCoeffArray d_entries; - - /** - * Buffer for d_entries to reduce allocations by addRowTimesConstant. - */ - VarCoeffArray d_buffer; - - /** - * The basic variable associated with the row. - * Must have a coefficient of -1. - */ - ArithVar d_basic; - - - /** - * Invariants: - * - This set is the same as the set maintained in d_entries. - */ - ArithVarContainsSet d_contains; - - std::vector& d_rowCount; - std::vector& d_columnMatrix; - - -public: - - ReducedRowVector(ArithVar basic, - const std::vector< ArithVar >& variables, - const std::vector< Rational >& coefficients, - std::vector& count, - std::vector< PermissiveBackArithVarSet >& columnMatrix); - ~ReducedRowVector(); - - void enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables, - std::vector< Rational >& coefficients) const; - - /** Returns the basic variable.*/ - ArithVar basic() const{ - Assert(basicIsSet()); - return d_basic; - } - - /** Returns the number of nonzero variables in the vector. */ - uint32_t size() const { - return d_entries.size(); - } - - /** Iterates over the nonzero entries in the vector. */ - const_iterator begin() const { return d_entries.begin(); } - const_iterator end() const { return d_entries.end(); } - - /** Returns true if the variable is in the row. */ - bool has(ArithVar x_j) const{ - if(x_j >= d_contains.size()){ - return false; - }else{ - return d_contains[x_j]; - } - } - - /** - * Returns the coefficient of a variable in the row. - */ - const Rational& lookup(ArithVar x_j) const{ - Assert(has(x_j)); - Assert(hasInEntries(x_j)); - const_iterator lb = lower_bound(x_j); - return (*lb).getCoefficient(); - } - - - /** Prints the row to the buffer Debug("row::print"). */ - void printRow(); - - /** - * Changes the basic variable to x_j. - * Precondition: has(x_j) - */ - void pivot(ArithVar x_j); - - /** - * Replaces other.basic() in the current row using the other row. - * This assumes the other row represents an equality equal to zero. - * - * \sum(this->entries) -= this->lookup(other.basic()) * (\sum(other.d_entries)) - * Precondition: - * has(other.basic()) - * basic != other.basic() - */ - void substitute(const ReducedRowVector& other); - - /** - * Returns the reduced row as an equality with - * the basic variable on the lhs equal to the sum of the non-basics variables. - * The mapped from ArithVars to Nodes is specificied by map. - */ - Node asEquality(const ArithVarToNodeMap& map) const; - -private: - - /** - * \sum(this->entries) += c * (\sum(other.d_entries) ) - * - * Updates the current row to be the sum of itself and - * another vector times c (c != 0). - */ - void addRowTimesConstant(const Rational& c, const ReducedRowVector& other); - - - /** Multiplies the coefficients of the RowVector by c (where c != 0). */ - void multiply(const Rational& c); - - /** - * Adds v to d_contains. - * This may resize d_contains. - */ - static void addArithVar(ArithVarContainsSet& contains, ArithVar v); - - /** Removes v from d_contains. */ - static void removeArithVar(ArithVarContainsSet& contains, ArithVar v); - - - /** - * Let c be -1 if strictlySorted is true and c be 0 otherwise. - * isSorted(arr, strictlySorted) is then equivalent to - * If i& variables, - const std::vector< Rational >& coefficients, - VarCoeffArray& output); - - /** - * Debugging code. - * noZeroCoefficients(arr) is equivalent to - * 0 != getCoefficient(arr[i]) for all i. - */ - static bool noZeroCoefficients(const VarCoeffArray& arr); - - /** Debugging code.*/ - bool matchingCounts() const; - - const_iterator lower_bound(ArithVar x_j) const{ - return std::lower_bound(d_entries.begin(), d_entries.end(), VarCoeffPair(x_j, 0)); - } - - /** Debugging code */ - bool wellFormed() const{ - return - isSorted(d_entries, true) && - noZeroCoefficients(d_entries) && - basicIsSet() && - has(basic()) && - lookup(basic()) == Rational(-1); - } - - bool basicIsSet() const { return d_basic != ARITHVAR_SENTINEL; } - - /** Debugging code. */ - bool hasInEntries(ArithVar x_j) const { - return std::binary_search(d_entries.begin(), d_entries.end(), VarCoeffPair(x_j,0)); - } - -}; /* class ReducedRowVector */ - - -}/* namespace CVC4::theory::arith */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ - -#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */ diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 6e73ca999..1a9c39984 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -209,36 +209,38 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& return Node::null(); } -set tableauAndHasSet(Tableau& tab, ArithVar v){ - set has; - for(ArithVarSet::iterator basicIter = tab.begin(); - basicIter != tab.end(); - ++basicIter){ - ArithVar basic = *basicIter; - ReducedRowVector& row = tab.lookup(basic); - - if(row.has(v)){ - has.insert(basic); - } - } - return has; -} - -set columnIteratorSet(Tableau& tab,ArithVar v){ - set has; - Column::iterator basicIter = tab.beginColumn(v); - Column::iterator endIter = tab.endColumn(v); - for(; basicIter != endIter; ++basicIter){ - ArithVar basic = *basicIter; - has.insert(basic); - } - return has; -} - - +// set tableauAndHasSet(Tableau& tab, ArithVar v){ +// set has; +// for(ArithVarSet::const_iterator basicIter = tab.beginBasic(); +// basicIter != tab.endBasic(); +// ++basicIter){ +// ArithVar basic = *basicIter; +// ReducedRowVector& row = tab.lookup(basic); + +// if(row.has(v)){ +// has.insert(basic); +// } +// } +// return has; +// } + +// set columnIteratorSet(Tableau& tab,ArithVar v){ +// set has; +// Column::iterator basicIter = tab.beginColumn(v); +// Column::iterator endIter = tab.endColumn(v); +// for(; basicIter != endIter; ++basicIter){ +// ArithVar basic = *basicIter; +// has.insert(basic); +// } +// return has; +// } + + +/* bool matchingSets(Tableau& tab, ArithVar v){ return tableauAndHasSet(tab, v) == columnIteratorSet(tab, v); } +*/ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ Assert(!d_tableau.isBasic(x_i)); @@ -249,15 +251,17 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ << assignment_x_i << "|-> " << v << endl; DeltaRational diff = v - assignment_x_i; - Assert(matchingSets(d_tableau, x_i)); - Column::iterator basicIter = d_tableau.beginColumn(x_i); - Column::iterator endIter = d_tableau.endColumn(x_i); - for(; basicIter != endIter; ++basicIter){ - ArithVar x_j = *basicIter; - ReducedRowVector& row_j = d_tableau.lookup(x_j); + //Assert(matchingSets(d_tableau, x_i)); + Tableau::ColIterator basicIter = d_tableau.colIterator(x_i); + for(; !basicIter.atEnd(); ++basicIter){ + const TableauEntry& entry = *basicIter; + Assert(entry.getColVar() == x_i); + + ArithVar x_j = entry.getRowVar(); + //ReducedRowVector& row_j = d_tableau.lookup(x_j); - Assert(row_j.has(x_i)); - const Rational& a_ji = row_j.lookup(x_i); + //const Rational& a_ji = row_j.lookup(x_i); + const Rational& a_ji = entry.getCoefficient(); const DeltaRational& assignment = d_partialModel.getAssignment(x_j); DeltaRational nAssignment = assignment+(diff * a_ji); @@ -268,13 +272,34 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ d_partialModel.setAssignment(x_i, v); - Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_i)); - double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_i)); + Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_i)); + double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_i)); (d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference); - if(Debug.isOn("paranoid:check_tableau")){ - checkTableau(); + if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } +} + +void SimplexDecisionProcedure::debugPivotSimplex(ArithVar x_i, ArithVar x_j){ + Debug("arith::simplex:row") << "debugRowSimplex(" + << x_i << "|->" << x_j + << ")" << endl; + + for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + + ArithVar var = entry.getColVar(); + const Rational& coeff = entry.getCoefficient(); + DeltaRational beta = d_partialModel.getAssignment(var); + Debug("arith::simplex:row") << var << beta << coeff; + if(d_partialModel.hasLowerBound(var)){ + Debug("arith::simplex:row") << "(lb " << d_partialModel.getLowerBound(var) << ")"; + } + if(d_partialModel.hasUpperBound(var)){ + Debug("arith::simplex:row") << "(up " << d_partialModel.getUpperBound(var) << ")"; + } + Debug("arith::simplex:row") << endl; } + Debug("arith::simplex:row") << "end row"<< endl; } void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ @@ -282,32 +307,13 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime); - if(Debug.isOn("arith::pivotAndUpdate")){ - Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl; - ReducedRowVector& row_k = d_tableau.lookup(x_i); - for(ReducedRowVector::const_iterator varIter = row_k.begin(); - varIter != row_k.end(); - ++varIter){ - - ArithVar var = (*varIter).getArithVar(); - const Rational& coeff = (*varIter).getCoefficient(); - DeltaRational beta = d_partialModel.getAssignment(var); - Debug("arith::pivotAndUpdate") << var << beta << coeff; - if(d_partialModel.hasLowerBound(var)){ - Debug("arith::pivotAndUpdate") << "(lb " << d_partialModel.getLowerBound(var) << ")"; - } - if(d_partialModel.hasUpperBound(var)){ - Debug("arith::pivotAndUpdate") << "(up " << d_partialModel.getUpperBound(var) - << ")"; - } - Debug("arith::pivotAndUpdate") << endl; - } - Debug("arith::pivotAndUpdate") << "end row"<< endl; - } + if(Debug.isOn("arith::simplex:row")){ debugPivotSimplex(x_i, x_j); } + + const TableauEntry& entry_ij = d_tableau.findEntry(x_i, x_j); + Assert(!entry_ij.blank()); - ReducedRowVector& row_i = d_tableau.lookup(x_i); - const Rational& a_ij = row_i.lookup(x_j); + const Rational& a_ij = entry_ij.getCoefficient(); const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i); @@ -322,16 +328,13 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR d_partialModel.setAssignment(x_j, tmp); - Assert(matchingSets(d_tableau, x_j)); - Column::iterator basicIter = d_tableau.beginColumn(x_j); - Column::iterator endIter = d_tableau.endColumn(x_j); - for(; basicIter != endIter; ++basicIter){ - ArithVar x_k = *basicIter; - ReducedRowVector& row_k = d_tableau.lookup(x_k); - - Assert(row_k.has(x_j)); + //Assert(matchingSets(d_tableau, x_j)); + for(Tableau::ColIterator iter = d_tableau.colIterator(x_j); !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + Assert(entry.getColVar() == x_j); + ArithVar x_k = entry.getRowVar(); if(x_k != x_i ){ - const Rational& a_kj = row_k.lookup(x_j); + const Rational& a_kj = entry.getCoefficient(); DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj); d_partialModel.setAssignment(x_k, nextAssignment); @@ -342,8 +345,8 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR // Pivots ++(d_statistics.d_statPivots); - Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_j)); - double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_j)); + Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_j)); + double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_j)); (d_statistics.d_avgNumRowsNotContainingOnPivot).addEntry(difference); d_tableau.pivot(x_i, x_j); @@ -367,14 +370,18 @@ ArithVar SimplexDecisionProcedure::minVarOrder(const SimplexDecisionProcedure& s } } -ArithVar SimplexDecisionProcedure::minRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){ +ArithVar SimplexDecisionProcedure::minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){ Assert(x != ARITHVAR_SENTINEL); Assert(y != ARITHVAR_SENTINEL); Assert(!simp.d_tableau.isBasic(x)); Assert(!simp.d_tableau.isBasic(y)); - if(simp.d_tableau.getRowCount(x) > simp.d_tableau.getRowCount(y)){ - return y; - } else { + uint32_t xLen = simp.d_tableau.getColLength(x); + uint32_t yLen = simp.d_tableau.getColLength(y); + if( xLen > yLen){ + return y; + } else if( xLen== yLen ){ + return minVarOrder(simp,x,y); + }else{ return x; } } @@ -389,27 +396,22 @@ ArithVar SimplexDecisionProcedure::minBoundAndRowCount(const SimplexDecisionProc }else if(!simp.d_partialModel.hasEitherBound(x) && simp.d_partialModel.hasEitherBound(y)){ return x; }else { - return minRowCount(simp, x, y); + return minColLength(simp, x, y); } } template ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ - ReducedRowVector& row_i = d_tableau.lookup(x_i); - ArithVar slack = ARITHVAR_SENTINEL; - for(ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end(); - nbi != end; ++nbi){ - ArithVar nonbasic = (*nbi).getArithVar(); + for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); if(nonbasic == x_i) continue; - const Rational& a_ij = (*nbi).getCoefficient(); + const Rational& a_ij = entry.getCoefficient(); int sgn = a_ij.sgn(); - if(( above && sgn < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) || - ( above && sgn > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)) || - (!above && sgn > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) || - (!above && sgn < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic))) { + if(isAcceptableSlack(sgn, nonbasic)){ //If one of the above conditions is met, we have found an acceptable //nonbasic variable to pivot x_i with. We can now choose which one we //prefer the most. @@ -563,7 +565,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera Assert(remainingIterations > 0); while(remainingIterations > 0){ - if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } ArithVar x_i = d_queue.dequeueInconsistentBasicVariable(); Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl; @@ -612,8 +614,6 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ - ReducedRowVector& row_i = d_tableau.lookup(conflictVar); - NodeBuilder<> nb(kind::AND); TNode bound = d_partialModel.getUpperConstraint(conflictVar); @@ -624,13 +624,13 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ nb << bound; - ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end(); - - for(; nbi != end; ++nbi){ - ArithVar nonbasic = (*nbi).getArithVar(); + Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar); + for(; !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); if(nonbasic == conflictVar) continue; - const Rational& a_ij = (*nbi).getCoefficient(); + const Rational& a_ij = entry.getCoefficient(); Assert(a_ij != d_ZERO); int sgn = a_ij.sgn(); @@ -655,8 +655,6 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ } Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ - ReducedRowVector& row_i = d_tableau.lookup(conflictVar); - NodeBuilder<> nb(kind::AND); TNode bound = d_partialModel.getLowerConstraint(conflictVar); @@ -667,12 +665,13 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ nb << bound; - ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end(); - for(; nbi != end; ++nbi){ - ArithVar nonbasic = (*nbi).getArithVar(); + Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar); + for(; !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); if(nonbasic == conflictVar) continue; - const Rational& a_ij = (*nbi).getCoefficient(); + const Rational& a_ij = entry.getCoefficient(); int sgn = a_ij.sgn(); Assert(a_ij != d_ZERO); @@ -706,12 +705,11 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe Assert(d_tableau.isBasic(x)); DeltaRational sum(0); - ReducedRowVector& row = d_tableau.lookup(x); - for(ReducedRowVector::const_iterator i = row.begin(), end = row.end(); - i != end;++i){ - ArithVar nonbasic = (*i).getArithVar(); - if(nonbasic == row.basic()) continue; - const Rational& coeff = (*i).getCoefficient(); + for(Tableau::RowIterator i = d_tableau.rowIterator(x); !i.atEnd(); ++i){ + const TableauEntry& entry = (*i); + ArithVar nonbasic = entry.getColVar(); + if(nonbasic == x) continue; + const Rational& coeff = entry.getCoefficient(); const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe); sum = sum + (assignment * coeff); @@ -726,21 +724,20 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe * checkTableau(); * } */ -void SimplexDecisionProcedure::checkTableau(){ - - for(ArithVarSet::iterator basicIter = d_tableau.begin(); - basicIter != d_tableau.end(); ++basicIter){ +void SimplexDecisionProcedure::debugCheckTableau(){ + ArithVarSet::const_iterator basicIter = d_tableau.beginBasic(); + ArithVarSet::const_iterator endIter = d_tableau.endBasic(); + for(; basicIter != endIter; ++basicIter){ ArithVar basic = *basicIter; - ReducedRowVector& row_k = d_tableau.lookup(basic); DeltaRational sum; Debug("paranoid:check_tableau") << "starting row" << basic << endl; - for(ReducedRowVector::const_iterator nonbasicIter = row_k.begin(); - nonbasicIter != row_k.end(); - ++nonbasicIter){ - ArithVar nonbasic = (*nonbasicIter).getArithVar(); + Tableau::RowIterator nonbasicIter = d_tableau.rowIterator(basic); + for(; !nonbasicIter.atEnd(); ++nonbasicIter){ + const TableauEntry& entry = *nonbasicIter; + ArithVar nonbasic = entry.getColVar(); if(basic == nonbasic) continue; - const Rational& coeff = (*nonbasicIter).getCoefficient(); + const Rational& coeff = entry.getCoefficient(); DeltaRational beta = d_partialModel.getAssignment(nonbasic); Debug("paranoid:check_tableau") << nonbasic << beta << coeff< + inline bool isAcceptableSlack(int sgn, ArithVar nonbasic){ + return + ( above && sgn < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) || + ( above && sgn > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)) || + (!above && sgn > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) || + (!above && sgn < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)); + } + /** * Checks a basic variable, b, to see if it is in conflict. * If a conflict is discovered a node summarizing the conflict is returned. diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index cb1364488..367e90301 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -26,80 +26,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::arith; -Tableau::Tableau(const Tableau& tab){ - internalCopy(tab); -} - -void Tableau::internalCopy(const Tableau& tab){ - uint32_t N = tab.d_rowsTable.size(); - - Debug("tableau::copy") << "tableau copy "<< N << endl; - - if(N > 1){ - d_columnMatrix.insert(d_columnMatrix.end(), N, Column()); - d_rowsTable.insert(d_rowsTable.end(), N, NULL); - d_basicVariables.increaseSize(N-1); - - Assert(d_basicVariables.allocated() == tab.d_basicVariables.allocated()); - - d_rowCount.insert(d_rowCount.end(), N, 0); - } - - ColumnMatrix::const_iterator otherIter = tab.d_columnMatrix.begin(); - ColumnMatrix::iterator i_colIter = d_columnMatrix.begin(); - ColumnMatrix::iterator end_colIter = d_columnMatrix.end(); - for(; i_colIter != end_colIter; ++i_colIter, ++otherIter){ - Assert(otherIter != tab.d_columnMatrix.end()); - Column& col = *i_colIter; - const Column& otherCol = *otherIter; - col.increaseSize(otherCol.allocated()); - } - - ArithVarSet::iterator i_basicIter = tab.d_basicVariables.begin(); - ArithVarSet::iterator i_basicEnd = tab.d_basicVariables.end(); - for(; i_basicIter != i_basicEnd; ++i_basicIter){ - ArithVar basicVar = *i_basicIter; - const ReducedRowVector* otherRow = tab.d_rowsTable[basicVar]; - - Assert(otherRow != NULL); - - std::vector< ArithVar > variables; - std::vector< Rational > coefficients; - otherRow->enqueueNonBasicVariablesAndCoefficients(variables, coefficients); - - ReducedRowVector* copy = new ReducedRowVector(basicVar, variables, coefficients, d_rowCount, d_columnMatrix); - - Debug("tableau::copy") << "copying " << basicVar << endl; - copy->printRow(); - - d_basicVariables.add(basicVar); - d_rowsTable[basicVar] = copy; - } -} - -Tableau& Tableau::operator=(const Tableau& other){ - clear(); - internalCopy(other); - return (*this); -} - -Tableau::~Tableau(){ - clear(); -} - -void Tableau::clear(){ - while(!d_basicVariables.empty()){ - ArithVar curr = *(d_basicVariables.begin()); - ReducedRowVector* vec = removeRow(curr); - delete vec; - } - - d_rowsTable.clear(); - d_basicVariables.clear(); - d_rowCount.clear(); - d_columnMatrix.clear(); -} - +/* void Tableau::addRow(ArithVar basicVar, const std::vector& coeffs, const std::vector& variables){ @@ -121,14 +48,21 @@ void Tableau::addRow(ArithVar basicVar, ArithVar var = *varsIter; if(d_basicVariables.isMember(var)){ - ReducedRowVector& row_var = lookup(var); - row_current->substitute(row_var); + EntryID varID = find(basicVar, var); + TableauEntry& entry = d_entryManager.get(varID); + const Rational& coeff = entry.getCoefficient(); + + loadRowIntoMergeBuffer(var); + rowPlusRowTimesConstant(coeff, basicVar, var); + emptyRowFromMergeBuffer(var); } } } +*/ +/* ReducedRowVector* Tableau::removeRow(ArithVar basic){ - Assert(d_basicVariables.isMember(basic)); + Assert(isBasic(basic)); ReducedRowVector* row = d_rowsTable[basic]; @@ -137,73 +71,502 @@ ReducedRowVector* Tableau::removeRow(ArithVar basic){ return row; } +*/ -void Tableau::pivot(ArithVar x_r, ArithVar x_s){ - Assert(d_basicVariables.isMember(x_r)); - Assert(!d_basicVariables.isMember(x_s)); +void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic){ + Assert(isBasic(oldBasic)); + Assert(!isBasic(newBasic)); + Assert(mergeBufferIsEmpty()); - Debug("tableau") << "Tableau::pivot(" << x_r <<", " <has(x_s)); + rowPivot(oldBasic, newBasic); + loadRowIntoMergeBuffer(newBasic); - //Swap x_r and x_s in d_activeRows - d_rowsTable[x_s] = row_s; - d_rowsTable[x_r] = NULL; + ColIterator colIter = colIterator(newBasic); + while(!colIter.atEnd()){ + EntryID id = colIter.getID(); + TableauEntry& entry = d_entryManager.get(id); - d_basicVariables.remove(x_r); + ++colIter; //needs to be incremented before the variable is removed + if(entry.getRowVar() == newBasic){ continue; } - d_basicVariables.add(x_s); + ArithVar basicTo = entry.getRowVar(); + Rational coeff = entry.getCoefficient(); - row_s->pivot(x_s); + rowPlusRowTimesConstant(basicTo, coeff, newBasic); + } + emptyRowFromMergeBuffer(newBasic); - Column::VarList copy(getColumn(x_s).getList()); - vector::iterator basicIter = copy.begin(), endIter = copy.end(); + //Clear the column for used for this variable - for(; basicIter != endIter; ++basicIter){ - ArithVar basic = *basicIter; - if(basic == x_s) continue; + Assert(mergeBufferIsEmpty()); + Assert(!isBasic(oldBasic)); + Assert(isBasic(newBasic)); + Assert(getColLength(newBasic) == 1); +} - ReducedRowVector& row_k = lookup(basic); - Assert(row_k.has(x_s)); +Tableau::~Tableau(){} - row_k.substitute(*row_s); +void Tableau::setColumnUnused(ArithVar v){ + ColIterator colIter = colIterator(v); + while(!colIter.atEnd()){ + ++colIter; } - Assert(getColumn(x_s).size() == 1); - Assert(getRowCount(x_s) == 1); } - void Tableau::printTableau(){ Debug("tableau") << "Tableau::d_activeRows" << endl; - typedef RowsTable::iterator table_iter; - for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end(); - rowIter != end; ++rowIter){ - ReducedRowVector* row_k = *rowIter; - if(row_k != NULL){ - row_k->printRow(); - } + ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic(); + for(; basicIter != endIter; ++basicIter){ + ArithVar basic = *basicIter; + printRow(basic); } } -uint32_t Tableau::numNonZeroEntries() const { - uint32_t colSum = 0; - ColumnMatrix::const_iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end(); - for(; i != end; ++i){ - const Column& col = *i; - colSum += col.size(); +void Tableau::printRow(ArithVar basic){ + Debug("tableau") << "{" << basic << ":"; + for(RowIterator entryIter = rowIterator(basic); !entryIter.atEnd(); ++entryIter){ + const TableauEntry& entry = *entryIter; + printEntry(entry); + Debug("tableau") << ","; } - return colSum; + Debug("tableau") << "}" << endl; +} + +void Tableau::printEntry(const TableauEntry& entry){ + Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient(); } uint32_t Tableau::numNonZeroEntriesByRow() const { uint32_t rowSum = 0; - ArithVarSet::iterator i = d_basicVariables.begin(), end = d_basicVariables.end(); + ArithVarSet::const_iterator i = d_basicVariables.begin(), end = d_basicVariables.end(); for(; i != end; ++i){ ArithVar basic = *i; - const ReducedRowVector& row = *(d_rowsTable[basic]); - rowSum += row.size(); + rowSum += getRowLength(basic); } return rowSum; } + +uint32_t Tableau::numNonZeroEntriesByCol() const { + uint32_t colSum = 0; + VectorSizeTable::const_iterator i = d_colLengths.begin(); + VectorSizeTable::const_iterator end = d_colLengths.end(); + for(; i != end; ++i){ + colSum += *i; + } + return colSum; +} + + +EntryID Tableau::findOnRow(ArithVar row, ArithVar col){ + for(RowIterator i = rowIterator(row); !i.atEnd(); ++i){ + EntryID id = i.getID(); + const TableauEntry& entry = *i; + ArithVar colVar = entry.getColVar(); + + if(colVar == col){ + return id; + } + } + return ENTRYID_SENTINEL; +} + +EntryID Tableau::findOnCol(ArithVar row, ArithVar col){ + for(ColIterator i = colIterator(col); !i.atEnd(); ++i){ + EntryID id = i.getID(); + const TableauEntry& entry = *i; + ArithVar rowVar = entry.getRowVar(); + + if(rowVar == row){ + return id; + } + } + return ENTRYID_SENTINEL; +} + +const TableauEntry& Tableau::findEntry(ArithVar row, ArithVar col){ + bool colIsShorter = getColLength(col) < getRowLength(row); + EntryID id = colIsShorter ? findOnCol(row,col) : findOnRow(row,col); + if(id == ENTRYID_SENTINEL){ + return d_failedFind; + }else{ + return d_entryManager.get(id); + } +} + +void Tableau::removeRow(ArithVar basic){ + RowIterator i = rowIterator(basic); + while(!i.atEnd()){ + EntryID id = i.getID(); + ++i; + removeEntry(id); + } + d_basicVariables.remove(basic); +} + +void Tableau::loadRowIntoMergeBuffer(ArithVar basic){ + Assert(mergeBufferIsEmpty()); + for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){ + EntryID id = i.getID(); + const TableauEntry& entry = *i; + ArithVar colVar = entry.getColVar(); + d_mergeBuffer[colVar] = make_pair(id, false); + } +} + +void Tableau::emptyRowFromMergeBuffer(ArithVar basic){ + Assert(isBasic(basic)); + for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){ + const TableauEntry& entry = *i; + ArithVar colVar = entry.getColVar(); + Assert(d_mergeBuffer[colVar].first == i.getID()); + d_mergeBuffer[colVar] = make_pair(ENTRYID_SENTINEL, false); + } + + Assert(mergeBufferIsEmpty()); +} + + +/** + * Changes basic to newbasic (a variable on the row). + */ +void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew){ + Assert(mergeBufferIsEmpty()); + Assert(isBasic(basicOld)); + Assert(!isBasic(basicNew)); + + EntryID newBasicID = findOnRow(basicOld, basicNew); + + Assert(newBasicID != ENTRYID_SENTINEL); + + TableauEntry& newBasicEntry = d_entryManager.get(newBasicID); + Rational negInverseA_rs = -(newBasicEntry.getCoefficient().inverse()); + + for(RowIterator i = rowIterator(basicOld); !i.atEnd(); ++i){ + EntryID id = i.getID(); + TableauEntry& entry = d_entryManager.get(id); + + entry.getCoefficient() *= negInverseA_rs; + entry.setRowVar(basicNew); + } + + d_rowHeads[basicNew] = d_rowHeads[basicOld]; + d_rowHeads[basicOld] = ENTRYID_SENTINEL; + + d_rowLengths[basicNew] = d_rowLengths[basicOld]; + d_rowLengths[basicOld] = 0; + + d_basicVariables.remove(basicOld); + d_basicVariables.add(basicNew); +} + +void Tableau::addEntry(ArithVar row, ArithVar col, const Rational& coeff){ + Assert(coeff != 0); + + EntryID newId = d_entryManager.newEntry(); + TableauEntry& newEntry = d_entryManager.get(newId); + newEntry = TableauEntry( row, col, + d_rowHeads[row], d_colHeads[col], + ENTRYID_SENTINEL, ENTRYID_SENTINEL, + coeff); + Assert(newEntry.getCoefficient() != 0); + + Debug("tableau") << "addEntry(" << row << "," << col <<"," << coeff << ")" << endl; + + ++d_entriesInUse; + + if(d_rowHeads[row] != ENTRYID_SENTINEL) + d_entryManager.get(d_rowHeads[row]).setPrevRowID(newId); + + if(d_colHeads[col] != ENTRYID_SENTINEL) + d_entryManager.get(d_colHeads[col]).setPrevColID(newId); + + d_rowHeads[row] = newId; + d_colHeads[col] = newId; + ++d_rowLengths[row]; + ++d_colLengths[col]; +} + +void Tableau::removeEntry(EntryID id){ + Assert(d_entriesInUse > 0); + --d_entriesInUse; + + TableauEntry& entry = d_entryManager.get(id); + + ArithVar row = entry.getRowVar(); + ArithVar col = entry.getColVar(); + + Assert(d_rowLengths[row] > 0); + Assert(d_colLengths[col] > 0); + + + --d_rowLengths[row]; + --d_colLengths[col]; + + EntryID prevRow = entry.getPrevRowID(); + EntryID prevCol = entry.getPrevColID(); + + EntryID nextRow = entry.getNextRowID(); + EntryID nextCol = entry.getNextColID(); + + if(d_rowHeads[row] == id){ + d_rowHeads[row] = nextRow; + } + if(d_colHeads[col] == id){ + d_colHeads[col] = nextCol; + } + + entry.markBlank(); + + if(prevRow != ENTRYID_SENTINEL){ + d_entryManager.get(prevRow).setNextRowID(nextRow); + } + if(nextRow != ENTRYID_SENTINEL){ + d_entryManager.get(nextRow).setPrevRowID(prevRow); + } + + if(prevCol != ENTRYID_SENTINEL){ + d_entryManager.get(prevCol).setNextColID(nextCol); + } + if(nextCol != ENTRYID_SENTINEL){ + d_entryManager.get(nextCol).setPrevColID(prevCol); + } + + d_entryManager.freeEntry(id); +} + +void Tableau::rowPlusRowTimesConstant(ArithVar basicTo, const Rational& c, ArithVar basicFrom){ + + Debug("tableau") << "rowPlusRowTimesConstant(" + << basicTo << "," << c << "," << basicFrom << ")" + << endl; + + Assert(debugNoZeroCoefficients(basicTo)); + Assert(debugNoZeroCoefficients(basicFrom)); + + Assert(c != 0); + Assert(isBasic(basicTo)); + Assert(isBasic(basicFrom)); + Assert( d_usedList.empty() ); + + + RowIterator i = rowIterator(basicTo); + while(!i.atEnd()){ + EntryID id = i.getID(); + TableauEntry& entry = d_entryManager.get(id); + ArithVar colVar = entry.getColVar(); + + ++i; + if(bufferPairIsNotEmpty(d_mergeBuffer[colVar])){ + d_mergeBuffer[colVar].second = true; + d_usedList.push_back(colVar); + + EntryID inOtherRow = d_mergeBuffer[colVar].first; + const TableauEntry& other = d_entryManager.get(inOtherRow); + entry.getCoefficient() += c * other.getCoefficient(); + + if(entry.getCoefficient().sgn() == 0){ + removeEntry(id); + } + } + } + + for(RowIterator i = rowIterator(basicFrom); !i.atEnd(); ++i){ + const TableauEntry& entry = *i; + ArithVar colVar = entry.getColVar(); + + if(!(d_mergeBuffer[colVar]).second){ + Rational newCoeff = c * entry.getCoefficient(); + addEntry(basicTo, colVar, newCoeff); + } + } + + clearUsedList(); + + if(Debug.isOn("tableau")) { printTableau(); } +} + +void Tableau::clearUsedList(){ + ArithVarArray::iterator i, end; + for(i = d_usedList.begin(), end = d_usedList.end(); i != end; ++i){ + ArithVar pos = *i; + d_mergeBuffer[pos].second = false; + } + d_usedList.clear(); +} + +void Tableau::addRow(ArithVar basic, + const std::vector& coefficients, + const std::vector& variables) +{ + Assert(coefficients.size() == variables.size() ); + Assert(!isBasic(basic)); + + d_basicVariables.add(basic); + + if(Debug.isOn("tableau")){ printTableau(); } + + addEntry(basic, basic, Rational(-1)); + + vector::const_iterator coeffIter = coefficients.begin(); + vector::const_iterator varsIter = variables.begin(); + vector::const_iterator varsEnd = variables.end(); + + for(; varsIter != varsEnd; ++coeffIter, ++varsIter){ + const Rational& coeff = *coeffIter; + ArithVar var_i = *varsIter; + addEntry(basic, var_i, coeff); + } + + varsIter = variables.begin(); + coeffIter = coefficients.begin(); + for(; varsIter != varsEnd; ++coeffIter, ++varsIter){ + ArithVar var = *varsIter; + + if(isBasic(var)){ + Rational coeff = *coeffIter; + + loadRowIntoMergeBuffer(var); + rowPlusRowTimesConstant(basic, coeff, var); + emptyRowFromMergeBuffer(var); + } + } + + if(Debug.isOn("tableau")) { printTableau(); } + + Assert(debugNoZeroCoefficients(basic)); + + Assert(debugMatchingCountsForRow(basic)); + Assert(getColLength(basic) == 1); +} + +bool Tableau::debugNoZeroCoefficients(ArithVar basic){ + for(RowIterator i=rowIterator(basic); !i.atEnd(); ++i){ + const TableauEntry& entry = *i; + if(entry.getCoefficient() == 0){ + return false; + } + } + return true; +} +bool Tableau::debugMatchingCountsForRow(ArithVar basic){ + for(RowIterator i=rowIterator(basic); !i.atEnd(); ++i){ + const TableauEntry& entry = *i; + ArithVar colVar = entry.getColVar(); + uint32_t count = debugCountColLength(colVar); + Debug("tableau") << "debugMatchingCountsForRow " + << basic << ":" << colVar << " " << count + <<" "<< d_colLengths[colVar] << endl; + if( count != d_colLengths[colVar] ){ + return false; + } + } + return true; +} + + +uint32_t Tableau::debugCountColLength(ArithVar var){ + Debug("tableau") << var << " "; + uint32_t count = 0; + for(ColIterator i=colIterator(var); !i.atEnd(); ++i){ + const TableauEntry& entry = *i; + Debug("tableau") << "(" << entry.getRowVar() << ", " << i.getID() << ") "; + ++count; + } + Debug("tableau") << endl; + return count; +} + +uint32_t Tableau::debugCountRowLength(ArithVar var){ + uint32_t count = 0; + for(RowIterator i=rowIterator(var); !i.atEnd(); ++i){ + ++count; + } + return count; +} + +/* +void ReducedRowVector::enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,std::vector< Rational >& coefficients) const{ + for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ + ArithVar var = (*i).getArithVar(); + const Rational& q = (*i).getCoefficient(); + if(var != basic()){ + variables.push_back(var); + coefficients.push_back(q); + } + } + }*/ + +Node Tableau::rowAsEquality(ArithVar basic, const ArithVarToNodeMap& map){ + using namespace CVC4::kind; + + Assert(getRowLength(basic) >= 2); + + vector nonBasicPairs; + for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){ + const TableauEntry& entry = *i; + ArithVar colVar = entry.getColVar(); + if(colVar == basic) continue; + Node var = (map.find(colVar))->second; + Node coeff = mkRationalNode(entry.getCoefficient()); + + Node mult = NodeBuilder<2>(MULT) << coeff << var; + nonBasicPairs.push_back(mult); + } + + Node sum = Node::null(); + if(nonBasicPairs.size() == 1 ){ + sum = nonBasicPairs.front(); + }else{ + Assert(nonBasicPairs.size() >= 2); + NodeBuilder<> sumBuilder(PLUS); + sumBuilder.append(nonBasicPairs); + sum = sumBuilder; + } + Node basicVar = (map.find(basic))->second; + return NodeBuilder<2>(EQUAL) << basicVar << sum; +} + +double Tableau::densityMeasure() const{ + Assert(numNonZeroEntriesByRow() == numNonZeroEntries()); + Assert(numNonZeroEntriesByCol() == numNonZeroEntries()); + + uint32_t n = getNumRows(); + if(n == 0){ + return 1.0; + }else { + uint32_t s = numNonZeroEntries(); + uint32_t m = d_colHeads.size(); + uint32_t divisor = (n *(m - n + 1)); + + Assert(n >= 1); + Assert(m >= n); + Assert(divisor > 0); + Assert(divisor >= s); + + return (double(s)) / divisor; + } +} + +void TableauEntryManager::freeEntry(EntryID id){ + Assert(get(id).blank()); + Assert(d_size > 0); + + d_freedEntries.push(id); + --d_size; +} + +EntryID TableauEntryManager::newEntry(){ + EntryID newId; + if(d_freedEntries.empty()){ + newId = d_entries.size(); + d_entries.push_back(TableauEntry()); + }else{ + newId = d_freedEntries.front(); + d_freedEntries.pop(); + } + ++d_size; + return newId; +} diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 31f7cfa5a..fa227757a 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -25,10 +25,9 @@ #include "theory/arith/arithvar_set.h" #include "theory/arith/normal_form.h" -#include "theory/arith/row_vector.h" - -#include -#include +#include +#include +#include #ifndef __CVC4__THEORY__ARITH__TABLEAU_H #define __CVC4__THEORY__ARITH__TABLEAU_H @@ -37,38 +36,229 @@ namespace CVC4 { namespace theory { namespace arith { -typedef PermissiveBackArithVarSet Column; +typedef uint32_t EntryID; +#define ENTRYID_SENTINEL std::numeric_limits::max() + +class TableauEntry { +private: + ArithVar d_rowVar; + ArithVar d_colVar; + + EntryID d_nextRow; + EntryID d_nextCol; + + EntryID d_prevRow; + EntryID d_prevCol; + + Rational d_coefficient; + +public: + TableauEntry(): + d_rowVar(ARITHVAR_SENTINEL), + d_colVar(ARITHVAR_SENTINEL), + d_nextRow(ENTRYID_SENTINEL), + d_nextCol(ENTRYID_SENTINEL), + d_prevRow(ENTRYID_SENTINEL), + d_prevCol(ENTRYID_SENTINEL), + d_coefficient(0) + {} + + TableauEntry(ArithVar row, ArithVar col, + EntryID nextRowEntry, EntryID nextColEntry, + EntryID prevRowEntry, EntryID prevColEntry, + const Rational& coeff): + d_rowVar(row), + d_colVar(col), + d_nextRow(nextRowEntry), + d_nextCol(nextColEntry), + d_prevRow(prevRowEntry), + d_prevCol(prevColEntry), + d_coefficient(coeff) + {} + +private: + bool unusedConsistent() const { + return + (d_rowVar == ARITHVAR_SENTINEL && d_colVar == ARITHVAR_SENTINEL) || + (d_rowVar != ARITHVAR_SENTINEL && d_colVar != ARITHVAR_SENTINEL); + } + +public: + + EntryID getNextRowID() const { + return d_nextRow; + } + + EntryID getNextColID() const { + return d_nextCol; + } + EntryID getPrevRowID() const { + return d_prevRow; + } + + EntryID getPrevColID() const { + return d_prevCol; + } + + void setNextRowID(EntryID id) { + d_nextRow = id; + } + void setNextColID(EntryID id) { + d_nextCol = id; + } + void setPrevRowID(EntryID id) { + d_prevRow = id; + } + void setPrevColID(EntryID id) { + d_prevCol = id; + } + + void setRowVar(ArithVar newRowVar){ + d_rowVar = newRowVar; + } + + ArithVar getRowVar() const{ + return d_rowVar; + } + ArithVar getColVar() const{ + return d_colVar; + } + + const Rational& getCoefficient() const { + return d_coefficient; + } + + Rational& getCoefficient(){ + return d_coefficient; + } + + void markBlank() { + d_rowVar = ARITHVAR_SENTINEL; + d_colVar = ARITHVAR_SENTINEL; + } + + bool blank() const{ + Assert(unusedConsistent()); + + return d_rowVar == ARITHVAR_SENTINEL; + } +}; + +class TableauEntryManager { +private: + typedef std::vector EntryArray; + + EntryArray d_entries; + std::queue d_freedEntries; + + uint32_t d_size; + +public: + TableauEntryManager(): + d_entries(), d_freedEntries(), d_size(0) + {} + + const TableauEntry& get(EntryID id) const{ + Assert(inBounds(id)); + return d_entries[id]; + } + + TableauEntry& get(EntryID id){ + Assert(inBounds(id)); + return d_entries[id]; + } + + void freeEntry(EntryID id); + + EntryID newEntry(); -typedef std::vector ColumnMatrix; + uint32_t size() const{ return d_size; } + uint32_t capacity() const{ return d_entries.capacity(); } + + +private: + bool inBounds(EntryID id) const{ + return id < d_entries.size(); + } +}; class Tableau { private: - typedef std::vector< ReducedRowVector* > RowsTable; + // VectorHeadTable : ArithVar |-> EntryID of the head of the vector + typedef std::vector VectorHeadTable; + VectorHeadTable d_rowHeads; + VectorHeadTable d_colHeads; - RowsTable d_rowsTable; + // VectorSizeTable : ArithVar |-> length of the vector + typedef std::vector VectorSizeTable; + VectorSizeTable d_colLengths; + VectorSizeTable d_rowLengths; + // Set of all of the basic variables in the tableau. ArithVarSet d_basicVariables; - std::vector d_rowCount; - ColumnMatrix d_columnMatrix; + typedef std::pair PosUsedPair; + typedef std::vector PosUsedPairArray; + PosUsedPairArray d_mergeBuffer; + + typedef std::vector ArithVarArray; + ArithVarArray d_usedList; + + + uint32_t d_entriesInUse; + TableauEntryManager d_entryManager; public: /** * Constructs an empty tableau. */ - Tableau() : - d_rowsTable(), - d_basicVariables(), - d_rowCount(), - d_columnMatrix() - {} - - /** Copy constructor. */ - Tableau(const Tableau& tab); + Tableau() : d_entriesInUse(0) {} ~Tableau(); - Tableau& operator=(const Tableau& tab); +private: + void addEntry(ArithVar row, ArithVar col, const Rational& coeff); + void removeEntry(EntryID id); + + template + class Iterator { + private: + EntryID d_curr; + TableauEntryManager& d_entryManager; + + public: + Iterator(EntryID start, TableauEntryManager& manager) : + d_curr(start), d_entryManager(manager) + {} + + public: + + EntryID getID() const { + return d_curr; + } + + const TableauEntry& operator*() const{ + Assert(!atEnd()); + return d_entryManager.get(d_curr); + } + + Iterator& operator++(){ + Assert(!atEnd()); + TableauEntry& entry = d_entryManager.get(d_curr); + d_curr = isRowIterator ? entry.getNextRowID() : entry.getNextColID(); + return *this; + } + + bool atEnd() const { + return d_curr == ENTRYID_SENTINEL; + } + }; + +public: + typedef Iterator RowIterator; + typedef Iterator ColIterator; + + double densityMeasure() const; size_t getNumRows() const { return d_basicVariables.size(); @@ -76,56 +266,49 @@ public: void increaseSize(){ d_basicVariables.increaseSize(); - d_rowsTable.push_back(NULL); - d_rowCount.push_back(0); - d_columnMatrix.push_back(PermissiveBackArithVarSet()); + d_rowHeads.push_back(ENTRYID_SENTINEL); + d_colHeads.push_back(ENTRYID_SENTINEL); + + d_colLengths.push_back(0); + d_rowLengths.push_back(0); - //TODO replace with version of ArithVarSet that handles misses as non-entries - // not as buffer overflows - // ColumnMatrix::iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end(); - // for(; i != end; ++i){ - // Column& col = *i; - // col.increaseSize(d_columnMatrix.size()); - // } + d_mergeBuffer.push_back(std::make_pair(ENTRYID_SENTINEL, false)); } bool isBasic(ArithVar v) const { return d_basicVariables.isMember(v); } - ArithVarSet::iterator begin(){ + ArithVarSet::const_iterator beginBasic() const{ return d_basicVariables.begin(); } - ArithVarSet::iterator end(){ + ArithVarSet::const_iterator endBasic() const{ return d_basicVariables.end(); } - const Column& getColumn(ArithVar v){ - Assert(v < d_columnMatrix.size()); - return d_columnMatrix[v]; + RowIterator rowIterator(ArithVar v){ + Assert(v < d_rowHeads.size()); + EntryID head = d_rowHeads[v]; + return RowIterator(head, d_entryManager); } - Column::iterator beginColumn(ArithVar v){ - return getColumn(v).begin(); - } - Column::iterator endColumn(ArithVar v){ - return getColumn(v).end(); + ColIterator colIterator(ArithVar v){ + Assert(v < d_colHeads.size()); + EntryID head = d_colHeads[v]; + return ColIterator(head, d_entryManager); } - ReducedRowVector& lookup(ArithVar var){ - Assert(d_basicVariables.isMember(var)); - Assert(d_rowsTable[var] != NULL); - return *(d_rowsTable[var]); + uint32_t getRowLength(ArithVar x) const{ + Assert(x < d_rowLengths.size()); + return d_rowLengths[x]; } - uint32_t getRowCount(ArithVar x){ - Assert(x < d_rowCount.size()); - AlwaysAssert(d_rowCount[x] == getColumn(x).size()); - - return d_rowCount[x]; + uint32_t getColLength(ArithVar x) const{ + Assert(x < d_colLengths.size()); + return d_colLengths[x]; } /** @@ -149,49 +332,73 @@ public: * x_s is non-basic, and * a_rs != 0. */ - void pivot(ArithVar x_r, ArithVar x_s); + void pivot(ArithVar basicOld, ArithVar basicNew); +private: + void rowPivot(ArithVar basicOld, ArithVar basicNew); + /** Requires merge buffer to be loaded with basicFrom and used to be empty. */ + void rowPlusRowTimesConstant(ArithVar basicTo, const Rational& coeff, ArithVar basicFrom); - void printTableau(); + EntryID findOnRow(ArithVar basic, ArithVar find); + EntryID findOnCol(ArithVar basic, ArithVar find); - ReducedRowVector* removeRow(ArithVar basic); + TableauEntry d_failedFind; +public: + /** If the find fails, isUnused is true on the entry. */ + const TableauEntry& findEntry(ArithVar row, ArithVar col); /** - * Let s = numNonZeroEntries(), n = getNumRows(), and m = d_columnMatrix.size(). - * When n >= 1, - * densityMeasure() := s / (n*m - n**2 + n) - * := s / (n *(m - n + 1)) - * When n = 0, densityMeasure() := 1 + * Prints the contents of the Tableau to Debug("tableau::print") */ - double densityMeasure() const{ - Assert(numNonZeroEntriesByRow() == numNonZeroEntries()); - uint32_t n = getNumRows(); - if(n == 0){ - return 1.0; - }else { - uint32_t s = numNonZeroEntries(); - uint32_t m = d_columnMatrix.size(); - uint32_t divisor = (n *(m - n + 1)); - - Assert(n >= 1); - Assert(m >= n); - Assert(divisor > 0); - Assert(divisor >= s); - - return (double(s)) / divisor; - } - } + void printTableau(); + void printRow(ArithVar basic); + void printEntry(const TableauEntry& entry); + private: + void loadRowIntoMergeBuffer(ArithVar basic); + void emptyRowFromMergeBuffer(ArithVar basic); + void clearUsedList(); - uint32_t numNonZeroEntries() const; + static bool bufferPairIsNotEmpty(const PosUsedPair& p){ + return !(p.first == ENTRYID_SENTINEL && p.second == false); + } + + static bool bufferPairIsEmpty(const PosUsedPair& p){ + return (p.first == ENTRYID_SENTINEL && p.second == false); + } + bool mergeBufferIsEmpty() const { + return d_mergeBuffer.end() == std::find_if(d_mergeBuffer.begin(), + d_mergeBuffer.end(), + bufferPairIsNotEmpty); + } + + void setColumnUnused(ArithVar v); + +public: + uint32_t size() const { + return d_entriesInUse; + } + uint32_t getNumEntriesInTableau() const { + return d_entryManager.size(); + } + uint32_t getEntryCapacity() const { + return d_entryManager.capacity(); + } + + void removeRow(ArithVar basic); + Node rowAsEquality(ArithVar basic, const ArithVarToNodeMap& map); +private: + uint32_t numNonZeroEntries() const { return size(); } uint32_t numNonZeroEntriesByRow() const; + uint32_t numNonZeroEntriesByCol() const; + - /** Copies the datastructures in tab to this.*/ - void internalCopy(const Tableau& tab); + bool debugNoZeroCoefficients(ArithVar basic); + bool debugMatchingCountsForRow(ArithVar basic); + uint32_t debugCountColLength(ArithVar var); + uint32_t debugCountRowLength(ArithVar var); - /** Clears the structures in the tableau. */ - void clear(); }; }; /* namespace arith */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4b40e582c..c22b0019d 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -41,7 +41,6 @@ #include "theory/arith/theory_arith.h" #include "theory/arith/normal_form.h" -#include #include using namespace std; @@ -52,6 +51,8 @@ using namespace CVC4::kind; using namespace CVC4::theory; using namespace CVC4::theory::arith; +static const uint32_t RESET_START = 2; + struct SlackAttrID; typedef expr::Attribute Slack; @@ -62,8 +63,8 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valu d_diseq(c), d_tableau(), d_restartsCounter(0), - d_initialDensity(1.0), - d_tableauResetDensity(2.0), + d_presolveHasBeenCalled(false), + d_tableauResetDensity(1.6), d_tableauResetPeriod(10), d_propagator(c, out), d_simplex(d_partialModel, d_tableau), @@ -81,9 +82,10 @@ TheoryArith::Statistics::Statistics(): d_staticLearningTimer("theory::arith::staticLearningTimer"), d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0), d_presolveTime("theory::arith::presolveTime"), - d_initialTableauDensity("theory::arith::initialTableauDensity", 0.0), - d_avgTableauDensityAtRestart("theory::arith::avgTableauDensityAtRestarts"), - d_tableauResets("theory::arith::tableauResets", 0), + d_initialTableauSize("theory::arith::initialTableauSize", 0), + //d_tableauSizeHistory("theory::arith::tableauSizeHistory"), + d_currSetToSmaller("theory::arith::currSetToSmaller", 0), + d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0), d_restartTimer("theory::arith::restartTimer") { StatisticsRegistry::registerStat(&d_statUserVariables); @@ -96,9 +98,10 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_presolveTime); - StatisticsRegistry::registerStat(&d_initialTableauDensity); - StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart); - StatisticsRegistry::registerStat(&d_tableauResets); + StatisticsRegistry::registerStat(&d_initialTableauSize); + //StatisticsRegistry::registerStat(&d_tableauSizeHistory); + StatisticsRegistry::registerStat(&d_currSetToSmaller); + StatisticsRegistry::registerStat(&d_smallerSetToCurr); StatisticsRegistry::registerStat(&d_restartTimer); } @@ -113,9 +116,10 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_presolveTime); - StatisticsRegistry::unregisterStat(&d_initialTableauDensity); - StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart); - StatisticsRegistry::unregisterStat(&d_tableauResets); + StatisticsRegistry::unregisterStat(&d_initialTableauSize); + //StatisticsRegistry::unregisterStat(&d_tableauSizeHistory); + StatisticsRegistry::unregisterStat(&d_currSetToSmaller); + StatisticsRegistry::unregisterStat(&d_smallerSetToCurr); StatisticsRegistry::unregisterStat(&d_restartTimer); } @@ -129,21 +133,21 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){ ArithVar bestBasic = ARITHVAR_SENTINEL; - uint64_t rowLength = std::numeric_limits::max(); - - Column::iterator basicIter = d_tableau.beginColumn(variable); - Column::iterator end = d_tableau.endColumn(variable); - for(; basicIter != end; ++basicIter){ - ArithVar x_j = *basicIter; - ReducedRowVector& row_j = d_tableau.lookup(x_j); - - Assert(row_j.has(variable)); - if((row_j.size() < rowLength) || - (row_j.size() == rowLength && x_j < bestBasic)){ - bestBasic = x_j; - rowLength = row_j.size(); + uint64_t bestRowLength = std::numeric_limits::max(); + + Tableau::ColIterator basicIter = d_tableau.colIterator(variable); + for(; !basicIter.atEnd(); ++basicIter){ + const TableauEntry& entry = *basicIter; + Assert(entry.getColVar() == variable); + ArithVar basic = entry.getRowVar(); + uint32_t rowLength = d_tableau.getRowLength(basic); + if((rowLength < bestRowLength) || + (rowLength == bestRowLength && basic < bestBasic)){ + bestBasic = basic; + bestRowLength = rowLength; } } + Assert(bestBasic == ARITHVAR_SENTINEL || bestRowLength < std::numeric_limits::max()); return bestBasic; } @@ -409,7 +413,7 @@ void TheoryArith::check(Effort effortLevel){ } } - if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } if(Debug.isOn("arith::print_model")) { debugPrintModel(); } Debug("arith") << "TheoryArith::check end" << std::endl; } @@ -579,15 +583,15 @@ Node TheoryArith::getValue(TNode n) { } void TheoryArith::notifyEq(TNode lhs, TNode rhs) { - } void TheoryArith::notifyRestart(){ TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer); - if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } ++d_restartsCounter; + /* if(d_restartsCounter % d_tableauResetPeriod == 0){ double currentDensity = d_tableau.densityMeasure(); d_statistics.d_avgTableauDensityAtRestart.addEntry(currentDensity); @@ -599,6 +603,32 @@ void TheoryArith::notifyRestart(){ d_tableau = d_initialTableau; } } + */ + static const bool debugResetPolicy = false; + + uint32_t currSize = d_tableau.size(); + uint32_t copySize = d_smallTableauCopy.size(); + + //d_statistics.d_tableauSizeHistory << currSize; + if(debugResetPolicy){ + cout << "curr " << currSize << " copy " << copySize << endl; + } + if(d_presolveHasBeenCalled && copySize == 0 && currSize > 0){ + if(debugResetPolicy){ + cout << "initial copy " << d_restartsCounter << endl; + } + d_smallTableauCopy = d_tableau; // The initial copy + } + + if(d_presolveHasBeenCalled && d_restartsCounter >= RESET_START){ + if(copySize >= currSize * 1.1 ){ + ++d_statistics.d_smallerSetToCurr; + d_smallTableauCopy = d_tableau; + }else if(d_tableauResetDensity * copySize <= currSize){ + ++d_statistics.d_currSetToSmaller; + d_tableau = d_smallTableauCopy; + } + } } bool TheoryArith::entireStateIsConsistent(){ @@ -639,15 +669,14 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ Assert(!noRow); //remove the row from the tableau - ReducedRowVector* row = d_tableau.removeRow(v); - Node eq = row->asEquality(d_arithVarToNodeMap); + Node eq = d_tableau.rowAsEquality(v, d_arithVarToNodeMap); + d_tableau.removeRow(v); - if(Debug.isOn("row::print")) row->printRow(); if(Debug.isOn("tableau")) d_tableau.printTableau(); Debug("arith::permanentlyRemoveVariable") << eq << endl; - delete row; - Assert(d_tableau.getRowCount(v) == 0); + Assert(d_tableau.getRowLength(v) == 0); + Assert(d_tableau.getColLength(v) == 0); Assert(d_removedRows.find(v) == d_removedRows.end()); d_removedRows[v] = eq; } @@ -671,16 +700,15 @@ void TheoryArith::presolve(){ } } - d_initialTableau = d_tableau; - d_initialDensity = d_initialTableau.densityMeasure(); - d_statistics.d_initialTableauDensity.setData(d_initialDensity); + d_statistics.d_initialTableauSize.setData(d_tableau.size()); - if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } static int callCount = 0; Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl; learner.clear(); + d_presolveHasBeenCalled = true; check(FULL_EFFORT); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 11cbfb425..a90e37bdc 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -119,11 +119,6 @@ private: */ Tableau d_tableau; - /** - * A copy of the tableau immediately after removing variables - * without bounds in presolve(). - */ - Tableau d_initialTableau; /** Counts the number of notifyRestart() calls to the theory. */ uint32_t d_restartsCounter; @@ -134,11 +129,16 @@ private: * If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau * is set to d_initialTableau. */ - double d_initialDensity; + bool d_presolveHasBeenCalled; double d_tableauResetDensity; uint32_t d_tableauResetPeriod; static const uint32_t s_TABLEAU_RESET_INCREMENT = 5; + /** + * A copy of the tableau immediately after removing variables + * without bounds in presolve(). + */ + Tableau d_smallTableauCopy; ArithUnatePropagator d_propagator; SimplexDecisionProcedure d_simplex; @@ -252,9 +252,10 @@ private: IntStat d_permanentlyRemovedVariables; TimerStat d_presolveTime; - BackedStat d_initialTableauDensity; - AverageStat d_avgTableauDensityAtRestart; - IntStat d_tableauResets; + IntStat d_initialTableauSize; + //ListStat d_tableauSizeHistory; + IntStat d_currSetToSmaller; + IntStat d_smallerSetToCurr; TimerStat d_restartTimer; Statistics(); diff --git a/src/util/stats.h b/src/util/stats.h index a78070de4..bf962d02b 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -29,6 +29,7 @@ #include #include #include +#include #include "util/Assert.h" #include "lib/clock_gettime.h" @@ -502,6 +503,49 @@ public: };/* class AverageStat */ +template +class ListStat : public Stat{ +private: + typedef std::vector List; + List d_list; +public: + + /** + * Construct an integer-valued statistic with the given name and + * initial value. + */ + ListStat(const std::string& name) : Stat(name) {} + ~ListStat() {} + + void flushInformation(std::ostream& out) const{ + if(__CVC4_USE_STATISTICS) { + typename List::const_iterator i = d_list.begin(), end = d_list.end(); + out << "["; + if(i != end){ + out << *i; + ++i; + for(; i != end; ++i){ + out << ", " << *i; + } + } + out << "]"; + } + } + + ListStat& operator<<(const T& val){ + if(__CVC4_USE_STATISTICS) { + d_list.push_back(val); + } + return (*this); + } + + std::string getValue() const { + std::stringstream ss; + flushInformation(ss); + return ss.str(); + } + +};/* class ListStat */ /****************************************************************************/ /* Some utility functions for ::timespec */ -- cgit v1.2.3