From: Tim King Date: Mon, 7 Mar 2011 19:10:16 +0000 (+0000) Subject: Merges branches/arithmetic/tableau-reset into the trunk. The tableau is now heuristi... X-Git-Tag: cvc5-1.0.0~8666 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=423dafb4b4a34d0c99274a7619b062997342179a;p=cvc5.git Merges branches/arithmetic/tableau-reset into the trunk. The tableau is now heuristically reset to its initial state during restarts. --- diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index a8bcd28cc..cb1364488 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -45,11 +45,14 @@ void Tableau::internalCopy(const Tableau& tab){ d_rowCount.insert(d_rowCount.end(), N, 0); } + 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){ + for(; i_colIter != end_colIter; ++i_colIter, ++otherIter){ + Assert(otherIter != tab.d_columnMatrix.end()); Column& col = *i_colIter; - col.increaseSize(d_columnMatrix.size()); + const Column& otherCol = *otherIter; + col.increaseSize(otherCol.allocated()); } ArithVarSet::iterator i_basicIter = tab.d_basicVariables.begin(); @@ -183,3 +186,24 @@ void Tableau::printTableau(){ } } } + +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(); + } + return colSum; +} + +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; +} diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index dad4bb2f5..31f7cfa5a 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -156,7 +156,37 @@ public: ReducedRowVector* removeRow(ArithVar basic); + /** + * Let s = numNonZeroEntries(), n = getNumRows(), and m = d_columnMatrix.size(). + * When n >= 1, + * densityMeasure() := s / (n*m - n**2 + n) + * := s / (n *(m - n + 1)) + * When n = 0, densityMeasure() := 1 + */ + double densityMeasure() const{ + Assert(numNonZeroEntriesByRow() == numNonZeroEntries()); + uint32_t n = getNumRows(); + if(n == 0){ + return 1.0; + }else { + uint32_t s = numNonZeroEntries(); + uint32_t m = d_columnMatrix.size(); + uint32_t divisor = (n *(m - n + 1)); + + Assert(n >= 1); + Assert(m >= n); + Assert(divisor > 0); + Assert(divisor >= s); + + return (double(s)) / divisor; + } + } + private: + + uint32_t numNonZeroEntries() const; + uint32_t numNonZeroEntriesByRow() const; + /** Copies the datastructures in tab to this.*/ void internalCopy(const Tableau& tab); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 60eed27d1..456fdb746 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -60,6 +60,10 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : d_userVariables(), d_diseq(c), d_tableau(), + d_restartsCounter(0), + d_initialDensity(1.0), + d_tableauResetDensity(2.0), + d_tableauResetPeriod(10), d_propagator(c, out), d_simplex(d_constants, d_partialModel, d_out, d_tableau), d_statistics() @@ -74,7 +78,11 @@ TheoryArith::Statistics::Statistics(): d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0), d_staticLearningTimer("theory::arith::staticLearningTimer"), d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0), - d_presolveTime("theory::arith::presolveTime") + d_presolveTime("theory::arith::presolveTime"), + d_initialTableauDensity("theory::arith::initialTableauDensity", 0.0), + d_avgTableauDensityAtRestart("theory::arith::avgTableauDensityAtRestarts"), + d_tableauResets("theory::arith::tableauResets", 0), + d_restartTimer("theory::arith::restartTimer") { StatisticsRegistry::registerStat(&d_statUserVariables); StatisticsRegistry::registerStat(&d_statSlackVariables); @@ -84,6 +92,11 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables); StatisticsRegistry::registerStat(&d_presolveTime); + + StatisticsRegistry::registerStat(&d_initialTableauDensity); + StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart); + StatisticsRegistry::registerStat(&d_tableauResets); + StatisticsRegistry::registerStat(&d_restartTimer); } TheoryArith::Statistics::~Statistics(){ @@ -95,6 +108,11 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables); StatisticsRegistry::unregisterStat(&d_presolveTime); + + StatisticsRegistry::unregisterStat(&d_initialTableauDensity); + StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart); + StatisticsRegistry::unregisterStat(&d_tableauResets); + StatisticsRegistry::unregisterStat(&d_restartTimer); } void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { @@ -658,7 +676,22 @@ void TheoryArith::notifyEq(TNode lhs, TNode rhs) { } void TheoryArith::notifyRestart(){ + TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer); + if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } + + ++d_restartsCounter; + if(d_restartsCounter % d_tableauResetPeriod == 0){ + double currentDensity = d_tableau.densityMeasure(); + d_statistics.d_avgTableauDensityAtRestart.addEntry(currentDensity); + if(currentDensity >= d_tableauResetDensity * d_initialDensity){ + + ++d_statistics.d_tableauResets; + d_tableauResetPeriod += s_TABLEAU_RESET_INCREMENT; + d_tableauResetDensity += .2; + d_tableau = d_initialTableau; + } + } } bool TheoryArith::entireStateIsConsistent(){ @@ -731,7 +764,10 @@ void TheoryArith::presolve(){ } } - //Assert(entireStateIsConsistent()); //Boy is this paranoid + d_initialTableau = d_tableau; + d_initialDensity = d_initialTableau.densityMeasure(); + d_statistics.d_initialTableauDensity.setData(d_initialDensity); + if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } static int callCount = 0; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index fb39eac09..3ff83abdf 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -122,6 +122,27 @@ private: */ Tableau d_tableau; + /** + * A copy of the tableau immediately after removing variables + * without bounds in presolve(). + */ + Tableau d_initialTableau; + + /** Counts the number of notifyRestart() calls to the theory. */ + uint32_t d_restartsCounter; + + /** + * Every number of restarts equal to s_TABLEAU_RESET_PERIOD, + * the density of the tableau, d, is computed. + * If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau + * is set to d_initialTableau. + */ + double d_initialDensity; + double d_tableauResetDensity; + uint32_t d_tableauResetPeriod; + static const uint32_t s_TABLEAU_RESET_INCREMENT = 5; + + ArithUnatePropagator d_propagator; SimplexDecisionProcedure d_simplex; @@ -215,6 +236,12 @@ private: IntStat d_permanentlyRemovedVariables; TimerStat d_presolveTime; + + BackedStat d_initialTableauDensity; + AverageStat d_avgTableauDensityAtRestart; + IntStat d_tableauResets; + TimerStat d_restartTimer; + Statistics(); ~Statistics(); };