diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-27 14:47:10 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-27 14:47:10 +0000 |
commit | f813ed144b0945334e03bfd769ea3c2cf8b75843 (patch) | |
tree | e70c9bddf5445aac50b5080c2b1719e6ffb478e0 /src/theory/arith/tableau.cpp | |
parent | 68237f7d39a03905be4cc133a42083fc3342adb4 (diff) |
This merges in the branch cvc4/branches/arithmetic/matrix into trunk.
- Splits the functionality of having a sparse matrix of Ts and a solved matrix of rationals in tableau.
- Splits ArithVarSet into DenseMap and CDDenseSet and simplifies the code.
- No performance loss!
Diffstat (limited to 'src/theory/arith/tableau.cpp')
-rw-r--r-- | src/theory/arith/tableau.cpp | 571 |
1 files changed, 0 insertions, 571 deletions
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp deleted file mode 100644 index 567d8215e..000000000 --- a/src/theory/arith/tableau.cpp +++ /dev/null @@ -1,571 +0,0 @@ -/********************* */ -/*! \file tableau.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - - -#include "theory/arith/tableau.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::arith; - - -/* -void Tableau::addRow(ArithVar basicVar, - const std::vector<Rational>& coeffs, - const std::vector<ArithVar>& variables){ - - Assert(coeffs.size() == variables.size()); - - //The new basic variable cannot already be a basic variable - Assert(!d_basicVariables.isMember(basicVar)); - d_basicVariables.add(basicVar); - ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount, d_columnMatrix); - d_rowsTable[basicVar] = row_current; - - //A variable in the row may have been made non-basic already. - //If this is the case we fake pivoting this variable - vector<ArithVar>::const_iterator varsIter = variables.begin(); - vector<ArithVar>::const_iterator varsEnd = variables.end(); - - for( ; varsIter != varsEnd; ++varsIter){ - ArithVar var = *varsIter; - - if(d_basicVariables.isMember(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(isBasic(basic)); - - ReducedRowVector* row = d_rowsTable[basic]; - - d_basicVariables.remove(basic); - d_rowsTable[basic] = NULL; - - return row; -} -*/ - -void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic){ - Assert(isBasic(oldBasic)); - Assert(!isBasic(newBasic)); - Assert(mergeBufferIsEmpty()); - - Debug("tableau") << "Tableau::pivot(" << oldBasic <<", " << newBasic <<")" << endl; - - rowPivot(oldBasic, newBasic); - loadRowIntoMergeBuffer(newBasic); - - ColIterator colIter = colIterator(newBasic); - while(!colIter.atEnd()){ - EntryID id = colIter.getID(); - TableauEntry& entry = d_entryManager.get(id); - - ++colIter; //needs to be incremented before the variable is removed - if(entry.getRowVar() == newBasic){ continue; } - - ArithVar basicTo = entry.getRowVar(); - Rational coeff = entry.getCoefficient(); - - rowPlusRowTimesConstant(basicTo, coeff, newBasic); - } - emptyRowFromMergeBuffer(newBasic); - - //Clear the column for used for this variable - - Assert(mergeBufferIsEmpty()); - Assert(!isBasic(oldBasic)); - Assert(isBasic(newBasic)); - Assert(getColLength(newBasic) == 1); -} - -Tableau::~Tableau(){} - -void Tableau::setColumnUnused(ArithVar v){ - ColIterator colIter = colIterator(v); - while(!colIter.atEnd()){ - ++colIter; - } -} -void Tableau::printTableau() const { - Debug("tableau") << "Tableau::d_activeRows" << endl; - - ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic(); - for(; basicIter != endIter; ++basicIter){ - ArithVar basic = *basicIter; - printRow(basic); - } -} - -void Tableau::printRow(ArithVar basic) const { - Debug("tableau") << "{" << basic << ":"; - for(RowIterator entryIter = rowIterator(basic); !entryIter.atEnd(); ++entryIter){ - const TableauEntry& entry = *entryIter; - printEntry(entry); - Debug("tableau") << ","; - } - Debug("tableau") << "}" << endl; -} - -void Tableau::printEntry(const TableauEntry& entry) const { - Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient(); -} - -uint32_t Tableau::numNonZeroEntriesByRow() const { - uint32_t rowSum = 0; - ArithVarSet::const_iterator i = d_basicVariables.begin(), end = d_basicVariables.end(); - for(; i != end; ++i){ - ArithVar basic = *i; - 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<Rational>& coefficients, - const std::vector<ArithVar>& variables) -{ - Assert(coefficients.size() == variables.size() ); - Assert(!isBasic(basic)); - - d_basicVariables.add(basic); - - if(Debug.isOn("tableau")){ printTableau(); } - - addEntry(basic, basic, Rational(-1)); - - vector<Rational>::const_iterator coeffIter = coefficients.begin(); - vector<ArithVar>::const_iterator varsIter = variables.begin(); - vector<ArithVar>::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<Node> 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; -} |