-/********************* */
-/*! \file tableau.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 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;
+namespace cvc5 {
+namespace theory {
+namespace arith {
-Tableau::Tableau(const Tableau& tab){
- internalCopy(tab);
-}
+void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic, CoefficientChangeCallback& cb){
+ Assert(isBasic(oldBasic));
+ Assert(!isBasic(newBasic));
+ Assert(d_mergeBuffer.empty());
-void Tableau::internalCopy(const Tableau& tab){
- uint32_t N = tab.d_rowsTable.size();
+ Debug("tableau") << "Tableau::pivot(" << oldBasic <<", " << newBasic <<")" << endl;
- Debug("tableau::copy") << "tableau copy "<< N << endl;
+ RowIndex ridx = basicToRowIndex(oldBasic);
- if(N > 1){
- d_columnMatrix.insert(d_columnMatrix.end(), N, Column());
- d_rowsTable.insert(d_rowsTable.end(), N, NULL);
- d_basicVariables.increaseSize(N-1);
+ rowPivot(oldBasic, newBasic, cb);
+ Assert(ridx == basicToRowIndex(newBasic));
- Assert(d_basicVariables.allocated() == tab.d_basicVariables.allocated());
+ loadRowIntoBuffer(ridx);
- d_rowCount.insert(d_rowCount.end(), N, 0);
- }
+ ColIterator colIter = colIterator(newBasic);
+ while(!colIter.atEnd()){
+ EntryID id = colIter.getID();
+ Entry& entry = d_entries.get(id);
+
+ ++colIter; //needs to be incremented before the variable is removed
+ if(entry.getRowIndex() == ridx){ continue; }
- 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());
+ RowIndex to = entry.getRowIndex();
+ Rational coeff = entry.getCoefficient();
+ if(cb.canUseRow(to)){
+ rowPlusBufferTimesConstant(to, coeff, cb);
+ }else{
+ rowPlusBufferTimesConstant(to, coeff);
+ }
}
+ clearBuffer();
- 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];
+ //Clear the column for used for this variable
- Assert(otherRow != NULL);
+ Assert(d_mergeBuffer.empty());
+ Assert(!isBasic(oldBasic));
+ Assert(isBasic(newBasic));
+ Assert(getColLength(newBasic) == 1);
+}
- std::vector< ArithVar > variables;
- std::vector< Rational > coefficients;
- otherRow->enqueueNonBasicVariablesAndCoefficients(variables, coefficients);
+/**
+ * Changes basic to newbasic (a variable on the row).
+ */
+void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb){
+ Assert(isBasic(basicOld));
+ Assert(!isBasic(basicNew));
- ReducedRowVector* copy = new ReducedRowVector(basicVar, variables, coefficients, d_rowCount, d_columnMatrix);
+ RowIndex rid = basicToRowIndex(basicOld);
- Debug("tableau::copy") << "copying " << basicVar << endl;
- copy->printRow();
+ EntryID newBasicID = findOnRow(rid, basicNew);
- d_basicVariables.add(basicVar);
- d_rowsTable[basicVar] = copy;
- }
-}
+ Assert(newBasicID != ENTRYID_SENTINEL);
-Tableau& Tableau::operator=(const Tableau& other){
- clear();
- internalCopy(other);
- return (*this);
-}
+ 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());
-Tableau::~Tableau(){
- clear();
-}
+ for(RowIterator i = basicRowIterator(basicOld); !i.atEnd(); ++i){
+ EntryID id = i.getID();
+ Tableau::Entry& entry = d_entries.get(id);
-void Tableau::clear(){
- while(!d_basicVariables.empty()){
- ArithVar curr = *(d_basicVariables.begin());
- ReducedRowVector* vec = removeRow(curr);
- delete vec;
+ entry.getCoefficient() *= negInverseA_rs;
}
- d_rowsTable.clear();
- d_basicVariables.clear();
- d_rowCount.clear();
- d_columnMatrix.clear();
+ d_basic2RowIndex.remove(basicOld);
+ d_basic2RowIndex.set(basicNew, rid);
+ d_rowIndex2basic.set(rid, basicNew);
+
+ cb.multiplyRow(rid, -a_rs_sgn);
}
-void Tableau::addRow(ArithVar basicVar,
- const std::vector<Rational>& coeffs,
- const std::vector<ArithVar>& variables){
+void Tableau::addRow(ArithVar basic,
+ const std::vector<Rational>& coefficients,
+ const std::vector<ArithVar>& variables)
+{
+ Assert(basic < getNumColumns());
+ Assert(debugIsASet(variables));
+ Assert(coefficients.size() == variables.size());
+ Assert(!isBasic(basic));
- Assert(coeffs.size() == variables.size());
+ RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
+ addEntry(newRow, basic, Rational(-1));
- //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;
+ Assert(!d_basic2RowIndex.isKey(basic));
+ Assert(!d_rowIndex2basic.isKey(newRow));
- //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();
+ d_basic2RowIndex.set(basic, newRow);
+ d_rowIndex2basic.set(newRow, basic);
- for( ; varsIter != varsEnd; ++varsIter){
- ArithVar var = *varsIter;
- if(d_basicVariables.isMember(var)){
- ReducedRowVector& row_var = lookup(var);
- row_current->substitute(row_var);
- }
- }
-}
-
-ReducedRowVector* Tableau::removeRow(ArithVar basic){
- Assert(d_basicVariables.isMember(basic));
-
- ReducedRowVector* row = d_rowsTable[basic];
-
- d_basicVariables.remove(basic);
- d_rowsTable[basic] = NULL;
+ if(Debug.isOn("matrix")){ printMatrix(); }
- return row;
-}
+ NoEffectCCCB noeffect;
+ NoEffectCCCB* nep = &noeffect;
+ CoefficientChangeCallback* cccb = static_cast<CoefficientChangeCallback*>(nep);
-void Tableau::pivot(ArithVar x_r, ArithVar x_s){
- Assert(d_basicVariables.isMember(x_r));
- Assert(!d_basicVariables.isMember(x_s));
+ 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){
+ ArithVar var = *varsIter;
- Debug("tableau") << "Tableau::pivot(" << x_r <<", " <<x_s <<")" << endl;
+ if(isBasic(var)){
+ Rational coeff = *coeffIter;
- ReducedRowVector* row_s = d_rowsTable[x_r];
- Assert(row_s != NULL);
- Assert(row_s->has(x_s));
+ RowIndex ri = basicToRowIndex(var);
- //Swap x_r and x_s in d_activeRows
- d_rowsTable[x_s] = row_s;
- d_rowsTable[x_r] = NULL;
+ loadRowIntoBuffer(ri);
+ rowPlusBufferTimesConstant(newRow, coeff, *cccb);
+ clearBuffer();
+ }
+ }
- d_basicVariables.remove(x_r);
+ if(Debug.isOn("matrix")) { printMatrix(); }
- d_basicVariables.add(x_s);
+ Assert(debugNoZeroCoefficients(newRow));
+ Assert(debugMatchingCountsForRow(newRow));
+ Assert(getColLength(basic) == 1);
+}
- row_s->pivot(x_s);
+void Tableau::removeBasicRow(ArithVar basic){
+ RowIndex rid = basicToRowIndex(basic);
- Column::VarList copy(getColumn(x_s).getList());
- vector<ArithVar>::iterator basicIter = copy.begin(), endIter = copy.end();
+ removeRow(rid);
+ d_basic2RowIndex.remove(basic);
+ d_rowIndex2basic.remove(rid);
+}
- for(; basicIter != endIter; ++basicIter){
- ArithVar basic = *basicIter;
- if(basic == x_s) continue;
+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);
- ReducedRowVector& row_k = lookup(basic);
- Assert(row_k.has(x_s));
+ cb.update(to_idx, from, 0, mult.sgn());
- row_k.substitute(*row_s);
+ loadRowIntoBuffer(from_idx);
+ rowPlusBufferTimesConstant(to_idx, mult, cb);
+ clearBuffer();
}
- 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();
- }
+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();
}
+ return complexity;
}
-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();
+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 colSum;
+ return (rows == 0) ? 0 : (sum/rows);
}
-uint32_t Tableau::numNonZeroEntriesByRow() const {
- uint32_t rowSum = 0;
- ArithVarSet::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();
- }
- return rowSum;
+void Tableau::printBasicRow(ArithVar basic, std::ostream& out){
+ printRow(basicToRowIndex(basic), out);
}
+
+} // namespace arith
+} // namespace theory
+} // namespace cvc5
projects / cvc5.git / blobdiff