From: Tim King Date: Mon, 21 Feb 2011 00:22:18 +0000 (+0000) Subject: - Adds the statistic d_avgNumRowsNotContainingOnPivot. X-Git-Tag: cvc5-1.0.0~8698 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=71b73af2ff69f41d71b892d6fc920a7b38fe736a;p=cvc5.git - Adds the statistic d_avgNumRowsNotContainingOnPivot. - Removed a bug in row counting in row counting. --- diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp index 07fc0186d..2af03bf08 100644 --- a/src/theory/arith/row_vector.cpp +++ b/src/theory/arith/row_vector.cpp @@ -117,7 +117,8 @@ void RowVector::merge(VarCoeffArray& arr, }else{ Rational res = getCoefficient(*curr1) + c * getCoefficient(*curr2); if(res != 0){ - ++counts[getArithVar(*curr2)]; + //The variable is not new so the count stays the same + //bug: ++counts[getArithVar(*curr2)]; arr.push_back(make_pair(getArithVar(*curr1), res)); }else{ @@ -177,6 +178,7 @@ ReducedRowVector::ReducedRowVector(ArithVar basic, merge(d_entries, d_contains, justBasic, Rational(1), d_rowCount); Assert(wellFormed()); + Assert(d_rowCount[d_basic] == 1); } void ReducedRowVector::substitute(const ReducedRowVector& row_s){ @@ -192,6 +194,7 @@ void ReducedRowVector::substitute(const ReducedRowVector& row_s){ Assert(!has(x_s)); Assert(wellFormed()); + Assert(d_rowCount[basic()] == 1); } void ReducedRowVector::pivot(ArithVar x_j){ @@ -202,6 +205,9 @@ void ReducedRowVector::pivot(ArithVar x_j){ d_basic = x_j; 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. } @@ -237,3 +243,10 @@ Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{ Node basicVar = (map.find(basic()))->second; return NodeBuilder<2>(EQUAL) << basicVar << sum; } + + +ReducedRowVector::~ReducedRowVector(){ + //This executes before the super classes destructor RowVector, + // which will set this to 0. + Assert(d_rowCount[basic()] == 1); +} diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h index 2b48564a4..85a188063 100644 --- a/src/theory/arith/row_vector.h +++ b/src/theory/arith/row_vector.h @@ -178,6 +178,7 @@ public: const std::vector< Rational >& coefficients, std::vector& count); + ~ReducedRowVector(); ArithVar basic() const{ Assert(basicIsSet()); diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 0f4f27a76..d8d39c24f 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -22,7 +22,9 @@ SimplexDecisionProcedure::Statistics::Statistics(): d_selectInitialConflictTime("theory::arith::selectInitialConflictTime"), d_pivotsAfterConflict("theory::arith::pivotsAfterConflict", 0), d_checksWithWastefulPivots("theory::arith::checksWithWastefulPivots", 0), - d_pivotTime("theory::arith::pivotTime") + d_pivotTime("theory::arith::pivotTime"), + d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"), + d_avgNumRowsNotContainingOnPivot("theory::arith::avgNumRowsNotContainingOnPivot") { StatisticsRegistry::registerStat(&d_statPivots); StatisticsRegistry::registerStat(&d_statUpdates); @@ -36,6 +38,9 @@ SimplexDecisionProcedure::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_pivotsAfterConflict); StatisticsRegistry::registerStat(&d_checksWithWastefulPivots); StatisticsRegistry::registerStat(&d_pivotTime); + + StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnUpdate); + StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnPivot); } SimplexDecisionProcedure::Statistics::~Statistics(){ @@ -51,6 +56,9 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_pivotsAfterConflict); StatisticsRegistry::unregisterStat(&d_checksWithWastefulPivots); StatisticsRegistry::unregisterStat(&d_pivotTime); + + StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnUpdate); + StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnPivot); } /* procedure AssertLower( x_i >= c_i ) */ @@ -188,6 +196,10 @@ 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)); + + (d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference); if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } @@ -261,8 +273,12 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR ++(d_statistics.d_pivotsAfterConflict); } + Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_j)); + double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_j)); + (d_statistics.d_avgNumRowsNotContainingOnPivot).addEntry(difference); d_tableau.pivot(x_i, x_j); + checkBasicVariable(x_j); // Debug found conflict diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 84d7cdcbb..c5c4da661 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -208,6 +208,10 @@ private: IntStat d_pivotsAfterConflict, d_checksWithWastefulPivots; TimerStat d_pivotTime; + + AverageStat d_avgNumRowsNotContainingOnUpdate; + AverageStat d_avgNumRowsNotContainingOnPivot; + Statistics(); ~Statistics(); }; diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 32c2986e3..36d61ba25 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -59,6 +59,10 @@ public: {} ~Tableau(); + size_t getNumRows() const { + return d_basicVariables.size(); + } + void increaseSize(){ d_basicVariables.increaseSize(); d_rowsTable.push_back(NULL); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4e84c85db..6084e3463 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -694,9 +694,11 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ Node eq = row->asEquality(d_arithVarToNodeMap); 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_removedRows.find(v) == d_removedRows.end()); d_removedRows[v] = eq; }