diff options
author | Tim King <taking@cs.nyu.edu> | 2010-11-04 16:26:40 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-11-04 16:26:40 +0000 |
commit | 2e56bd5ca2a19ef37486ec1b7a952e3166abad00 (patch) | |
tree | c55be0d182df37770d63a0fbf85b3a3558f0c5d3 /src | |
parent | eec3e4b96a5ba3a0acfa22d4cd8896d9a5ea66c8 (diff) |
This commit adds the ejected and un-ejected statistics.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/simplex.cpp | 29 | ||||
-rw-r--r-- | src/theory/arith/simplex.h | 1 |
2 files changed, 20 insertions, 10 deletions
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(); }; |