diff options
Diffstat (limited to 'src/theory/arith/tableau.cpp')
-rw-r--r-- | src/theory/arith/tableau.cpp | 179 |
1 files changed, 179 insertions, 0 deletions
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp new file mode 100644 index 000000000..c54b0857a --- /dev/null +++ b/src/theory/arith/tableau.cpp @@ -0,0 +1,179 @@ +#include "theory/arith/tableau.h" + +using namespace std; +namespace CVC4 { +namespace theory { +namespace arith { + + +void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic, CoefficientChangeCallback& cb){ + Assert(isBasic(oldBasic)); + Assert(!isBasic(newBasic)); + Assert(d_mergeBuffer.empty()); + + Debug("tableau") << "Tableau::pivot(" << oldBasic <<", " << newBasic <<")" << endl; + + 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(); + Entry& entry = d_entries.get(id); + + ++colIter; //needs to be incremented before the variable is removed + if(entry.getRowIndex() == ridx){ continue; } + + RowIndex to = entry.getRowIndex(); + Rational coeff = entry.getCoefficient(); + if(cb.canUseRow(to)){ + rowPlusBufferTimesConstant(to, coeff, cb); + }else{ + rowPlusBufferTimesConstant(to, coeff); + } + } + clearBuffer(); + + //Clear the column for used for this variable + + Assert(d_mergeBuffer.empty()); + Assert(!isBasic(oldBasic)); + Assert(isBasic(newBasic)); + Assert(getColLength(newBasic) == 1); +} + +/** + * Changes basic to newbasic (a variable on the row). + */ +void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCallback& cb){ + Assert(isBasic(basicOld)); + Assert(!isBasic(basicNew)); + + RowIndex rid = basicToRowIndex(basicOld); + + EntryID newBasicID = findOnRow(rid, basicNew); + + Assert(newBasicID != ENTRYID_SENTINEL); + + 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 = basicRowIterator(basicOld); !i.atEnd(); ++i){ + EntryID id = i.getID(); + Tableau::Entry& entry = d_entries.get(id); + + entry.getCoefficient() *= negInverseA_rs; + } + + d_basic2RowIndex.remove(basicOld); + d_basic2RowIndex.set(basicNew, rid); + d_rowIndex2basic.set(rid, basicNew); + + cb.swap(basicOld, basicNew, a_rs_sgn); +} + + + +void Tableau::addRow(ArithVar basic, + const std::vector<Rational>& coefficients, + const std::vector<ArithVar>& variables) +{ + Assert(basic < getNumColumns()); + + Assert(coefficients.size() == variables.size() ); + Assert(!isBasic(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("matrix")){ printMatrix(); } + + 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){ + ArithVar var = *varsIter; + + if(isBasic(var)){ + Rational coeff = *coeffIter; + + RowIndex ri = basicToRowIndex(var); + + loadRowIntoBuffer(ri); + rowPlusBufferTimesConstant(newRow, coeff, *cccb); + clearBuffer(); + } + } + + if(Debug.isOn("matrix")) { printMatrix(); } + + Assert(debugNoZeroCoefficients(newRow)); + Assert(debugMatchingCountsForRow(newRow)); + Assert(getColLength(basic) == 1); +} + +void Tableau::removeBasicRow(ArithVar basic){ + RowIndex rid = basicToRowIndex(basic); + + removeRow(rid); + d_basic2RowIndex.remove(basic); + d_rowIndex2basic.remove(rid); +} + +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); + + cb.update(to_idx, from, 0, mult.sgn()); + + loadRowIntoBuffer(from_idx); + rowPlusBufferTimesConstant(to_idx, mult, cb); + clearBuffer(); + } +} + +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; +} + +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 Tableau::printBasicRow(ArithVar basic, std::ostream& out){ + printRow(basicToRowIndex(basic), out); +} + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ |