-/********************* */
-/*! \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
- **/
-
+/******************************************************************************
+ * Top contributors (to current version):
+ * Tim King
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
+#include "base/output.h"
#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];
+namespace cvc5 {
+namespace theory {
+namespace arith {
- d_basicVariables.remove(basic);
- d_rowsTable[basic] = NULL;
-
- return row;
-}
-*/
-void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic){
+void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic, CoefficientChangeCallback& cb){
Assert(isBasic(oldBasic));
Assert(!isBasic(newBasic));
- Assert(mergeBufferIsEmpty());
+ Assert(d_mergeBuffer.empty());
Debug("tableau") << "Tableau::pivot(" << oldBasic <<", " << newBasic <<")" << endl;
- rowPivot(oldBasic, newBasic);
- loadRowIntoMergeBuffer(newBasic);
+ RowIndex ridx = basicToRowIndex(oldBasic);
+
+ rowPivot(oldBasic, newBasic, cb);
+ Assert(ridx == basicToRowIndex(newBasic));
+
+ loadRowIntoBuffer(ridx);
ColIterator colIter = colIterator(newBasic);
while(!colIter.atEnd()){
EntryID id = colIter.getID();
- TableauEntry& entry = d_entryManager.get(id);
+ Entry& entry = d_entries.get(id);
++colIter; //needs to be incremented before the variable is removed
- if(entry.getRowVar() == newBasic){ continue; }
+ if(entry.getRowIndex() == ridx){ continue; }
- ArithVar basicTo = entry.getRowVar();
+ RowIndex to = entry.getRowIndex();
Rational coeff = entry.getCoefficient();
-
- rowPlusRowTimesConstant(basicTo, coeff, newBasic);
+ if(cb.canUseRow(to)){
+ rowPlusBufferTimesConstant(to, coeff, cb);
+ }else{
+ rowPlusBufferTimesConstant(to, coeff);
+ }
}
- emptyRowFromMergeBuffer(newBasic);
+ clearBuffer();
//Clear the column for used for this variable
- Assert(mergeBufferIsEmpty());
+ Assert(d_mergeBuffer.empty());
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());
+void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb){
Assert(isBasic(basicOld));
Assert(!isBasic(basicNew));
- EntryID newBasicID = findOnRow(basicOld, basicNew);
+ RowIndex rid = basicToRowIndex(basicOld);
+
+ EntryID newBasicID = findOnRow(rid, basicNew);
Assert(newBasicID != ENTRYID_SENTINEL);
- TableauEntry& newBasicEntry = d_entryManager.get(newBasicID);
- Rational negInverseA_rs = -(newBasicEntry.getCoefficient().inverse());
+ Tableau::Entry& newBasicEntry = d_entries.get(newBasicID);
+ const Rational& a_rs = newBasicEntry.getCoefficient();
+ int a_rs_sgn = a_rs.sgn();
+ Rational negInverseA_rs = -(a_rs.inverse());
- for(RowIterator i = rowIterator(basicOld); !i.atEnd(); ++i){
+ for(RowIterator i = basicRowIterator(basicOld); !i.atEnd(); ++i){
EntryID id = i.getID();
- TableauEntry& entry = d_entryManager.get(id);
+ Tableau::Entry& entry = d_entries.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_basic2RowIndex.remove(basicOld);
+ d_basic2RowIndex.set(basicNew, rid);
+ d_rowIndex2basic.set(rid, basicNew);
- 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();
+ cb.multiplyRow(rid, -a_rs_sgn);
}
void Tableau::addRow(ArithVar basic,
const std::vector<Rational>& coefficients,
const std::vector<ArithVar>& variables)
{
- Assert(coefficients.size() == variables.size() );
+ Assert(basic < getNumColumns());
+ Assert(debugIsASet(variables));
+ Assert(coefficients.size() == variables.size());
Assert(!isBasic(basic));
- d_basicVariables.add(basic);
+ RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
+ addEntry(newRow, basic, Rational(-1));
+
+ Assert(!d_basic2RowIndex.isKey(basic));
+ Assert(!d_rowIndex2basic.isKey(newRow));
+
+ d_basic2RowIndex.set(basic, newRow);
+ d_rowIndex2basic.set(newRow, basic);
+
- if(Debug.isOn("tableau")){ printTableau(); }
+ if(Debug.isOn("matrix")){ printMatrix(); }
- addEntry(basic, basic, Rational(-1));
+ NoEffectCCCB noeffect;
+ NoEffectCCCB* nep = &noeffect;
+ CoefficientChangeCallback* cccb = static_cast<CoefficientChangeCallback*>(nep);
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);
+ RowIndex ri = basicToRowIndex(var);
+
+ loadRowIntoBuffer(ri);
+ rowPlusBufferTimesConstant(newRow, coeff, *cccb);
+ clearBuffer();
}
}
- if(Debug.isOn("tableau")) { printTableau(); }
+ if(Debug.isOn("matrix")) { printMatrix(); }
- Assert(debugNoZeroCoefficients(basic));
-
- Assert(debugMatchingCountsForRow(basic));
+ Assert(debugNoZeroCoefficients(newRow));
+ Assert(debugMatchingCountsForRow(newRow));
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;
-}
+void Tableau::removeBasicRow(ArithVar basic){
+ RowIndex rid = basicToRowIndex(basic);
-uint32_t Tableau::debugCountRowLength(ArithVar var){
- uint32_t count = 0;
- for(RowIterator i=rowIterator(var); !i.atEnd(); ++i){
- ++count;
- }
- return count;
+ removeRow(rid);
+ d_basic2RowIndex.remove(basic);
+ d_rowIndex2basic.remove(rid);
}
-/*
-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);
- }
- }
- }*/
+void Tableau::substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult, CoefficientChangeCallback& cb){
+ if(!mult.isZero()){
+ RowIndex to_idx = basicToRowIndex(to);
+ addEntry(to_idx, from, mult); // Add an entry to be cancelled out
+ RowIndex from_idx = basicToRowIndex(from);
-Node Tableau::rowAsEquality(ArithVar basic, const ArithVarToNodeMap& map){
- using namespace CVC4::kind;
+ cb.update(to_idx, from, 0, mult.sgn());
- 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);
+ loadRowIntoBuffer(from_idx);
+ rowPlusBufferTimesConstant(to_idx, mult, cb);
+ clearBuffer();
}
+}
- Node sum = Node::null();
- if(nonBasicPairs.size() == 1 ){
- sum = nonBasicPairs.front();
- }else{
- Assert(nonBasicPairs.size() >= 2);
- NodeBuilder<> sumBuilder(PLUS);
- sumBuilder.append(nonBasicPairs);
- sum = sumBuilder;
+uint32_t Tableau::rowComplexity(ArithVar basic) const{
+ uint32_t complexity = 0;
+ for(RowIterator i = basicRowIterator(basic); !i.atEnd(); ++i){
+ const Entry& e = *i;
+ complexity += e.getCoefficient().complexity();
}
- Node basicVar = (map.find(basic))->second;
- return NodeBuilder<2>(EQUAL) << basicVar << sum;
+ return complexity;
}
-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;
+double Tableau::avgRowComplexity() const{
+ double sum = 0;
+ uint32_t rows = 0;
+ for(BasicIterator i = beginBasic(), i_end = endBasic(); i != i_end; ++i){
+ sum += rowComplexity(*i);
+ rows++;
}
+ return (rows == 0) ? 0 : (sum/rows);
}
-void TableauEntryManager::freeEntry(EntryID id){
- Assert(get(id).blank());
- Assert(d_size > 0);
-
- d_freedEntries.push(id);
- --d_size;
+void Tableau::printBasicRow(ArithVar basic, std::ostream& out){
+ printRow(basicToRowIndex(basic), out);
}
-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;
-}
+} // namespace arith
+} // namespace theory
+} // namespace cvc5
projects / cvc5.git / blobdiff