From: Tim King Date: Thu, 4 Nov 2010 16:26:40 +0000 (+0000) Subject: This commit adds the ejected and un-ejected statistics. X-Git-Tag: cvc5-1.0.0~8749 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2e56bd5ca2a19ef37486ec1b7a952e3166abad00;p=cvc5.git This commit adds the ejected and un-ejected statistics. --- diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index e30d935f3..153ccad98 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -16,13 +16,17 @@ SimplexDecisionProcedure::Statistics::Statistics(): d_statUpdates("theory::arith::updates",0), d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0), d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0), - d_statUpdateConflicts("theory::arith::UpdateConflicts", 0) + d_statUpdateConflicts("theory::arith::UpdateConflicts", 0), + d_statEjections("theory::arith::Ejections", 0), + d_statUnEjections("theory::arith::UnEjections", 0) { StatisticsRegistry::registerStat(&d_statPivots); StatisticsRegistry::registerStat(&d_statUpdates); StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); StatisticsRegistry::registerStat(&d_statUpdateConflicts); + StatisticsRegistry::registerStat(&d_statEjections); + StatisticsRegistry::registerStat(&d_statUnEjections); } SimplexDecisionProcedure::Statistics::~Statistics(){ @@ -31,25 +35,30 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts); StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts); StatisticsRegistry::unregisterStat(&d_statUpdateConflicts); + StatisticsRegistry::unregisterStat(&d_statEjections); + StatisticsRegistry::unregisterStat(&d_statUnEjections); } void SimplexDecisionProcedure::ejectInactiveVariables(){ - Debug("decay") << "begin ejectInactiveVariables()" << endl; - for(ArithVar variable = 0, end = d_numVariables; variable != end; ++variable){ - if(shouldEject(variable)){ - if(d_basicManager.isMember(variable)){ - Debug("decay") << "ejecting basic " << variable << endl;; - d_tableau.ejectBasic(variable); - } + for(ArithVarSet::iterator i = d_tableau.begin(), end = d_tableau.end(); i != end;){ + ArithVar variable = *i; + ++i; + Assert(d_basicManager.isMember(variable)); + + if(d_basicManager.isMember(variable) && shouldEject(variable)){ + Debug("decay") << "ejecting basic " << variable << endl; + ++(d_statistics.d_statEjections); + d_tableau.ejectBasic(variable); } } } void SimplexDecisionProcedure::reinjectVariable(ArithVar x){ - d_tableau.reinjectBasic(x); + ++(d_statistics.d_statUnEjections); + d_tableau.reinjectBasic(x); DeltaRational safeAssignment = computeRowValue(x, true); DeltaRational assignment = computeRowValue(x, false); @@ -64,7 +73,7 @@ bool SimplexDecisionProcedure::shouldEject(ArithVar var){ }else if(!d_partialModel.hasEverHadABound(var)){ return true; }else if(d_activityMonitor[var] >= ACTIVITY_THRESHOLD){ - return true; + return false; } return false; } diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index e753ebc28..7514b6284 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -196,6 +196,7 @@ private: IntStat d_statPivots, d_statUpdates, d_statAssertUpperConflicts; IntStat d_statAssertLowerConflicts, d_statUpdateConflicts; + IntStat d_statEjections, d_statUnEjections; Statistics(); ~Statistics(); };