From 595024febc8dc014518db8e74a489d3c6d169493 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 17 Feb 2011 18:22:16 +0000 Subject: [PATCH] This commit is the promised clean up after removing row ejection. --- src/theory/arith/simplex.cpp | 74 ------------------------------- src/theory/arith/simplex.h | 23 ++++------ src/theory/arith/tableau.cpp | 26 ----------- src/theory/arith/tableau.h | 57 +++++------------------- src/theory/arith/theory_arith.cpp | 10 ----- 5 files changed, 20 insertions(+), 170 deletions(-) diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 6e7685570..4d417659e 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -17,8 +17,6 @@ SimplexDecisionProcedure::Statistics::Statistics(): d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0), d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0), d_statUpdateConflicts("theory::arith::UpdateConflicts", 0), - d_statEjections("theory::arith::Ejections", 0), - d_statUnEjections("theory::arith::UnEjections", 0), d_statEarlyConflicts("theory::arith::EarlyConflicts", 0), d_statEarlyConflictImprovements("theory::arith::EarlyConflictImprovements", 0), d_selectInitialConflictTime("theory::arith::selectInitialConflictTime"), @@ -31,8 +29,6 @@ SimplexDecisionProcedure::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); StatisticsRegistry::registerStat(&d_statUpdateConflicts); - StatisticsRegistry::registerStat(&d_statEjections); - StatisticsRegistry::registerStat(&d_statUnEjections); StatisticsRegistry::registerStat(&d_statEarlyConflicts); StatisticsRegistry::registerStat(&d_statEarlyConflictImprovements); StatisticsRegistry::registerStat(&d_selectInitialConflictTime); @@ -48,8 +44,6 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts); StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts); StatisticsRegistry::unregisterStat(&d_statUpdateConflicts); - StatisticsRegistry::unregisterStat(&d_statEjections); - StatisticsRegistry::unregisterStat(&d_statUnEjections); StatisticsRegistry::unregisterStat(&d_statEarlyConflicts); StatisticsRegistry::unregisterStat(&d_statEarlyConflictImprovements); StatisticsRegistry::unregisterStat(&d_selectInitialConflictTime); @@ -59,62 +53,10 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_pivotTime); } - -/* -void SimplexDecisionProcedure::ejectInactiveVariables(){ - return; //die die die - - 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_statistics.d_statUnEjections); - - d_tableau.reinjectBasic(x); - - DeltaRational safeAssignment = computeRowValue(x, true); - DeltaRational assignment = computeRowValue(x, false); - d_partialModel.setAssignment(x,safeAssignment,assignment); -} -*/ - -/* -bool SimplexDecisionProcedure::shouldEject(ArithVar var){ - if(d_partialModel.hasEitherBound(var)){ - return false; - }else if(d_tableau.isEjected(var)) { - return false; - }else if(!d_partialModel.hasEverHadABound(var)){ - return true; - }else if(d_activityMonitor[var] >= ACTIVITY_THRESHOLD){ - return false; - } - return false; -} -*/ - /* procedure AssertLower( x_i >= c_i ) */ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; - /* - if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ - reinjectVariable(x_i); - } - */ - if(d_partialModel.belowLowerBound(x_i, c_i, false)){ return false; //sat } @@ -145,11 +87,6 @@ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_ bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; - /* - if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ - reinjectVariable(x_i); - } - */ if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i return false; //sat @@ -183,12 +120,6 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl; - /* - if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ - reinjectVariable(x_i); - } - */ - // u_i <= c_i <= l_i // This can happen if both c_i <= x_i and x_i <= c_i are in the system. if(d_partialModel.belowLowerBound(x_i, c_i, false) && @@ -544,7 +475,6 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ Debug("arith") << "updateInconsistentVars" << endl; uint32_t iteratationNum = 0; - //static const int EJECT_FREQUENCY = 10; while(!d_pivotStage || iteratationNum <= d_numVariables){ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } @@ -557,10 +487,6 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ } ++iteratationNum; - /* - if(iteratationNum % EJECT_FREQUENCY == 0) - ejectInactiveVariables(); - */ DeltaRational beta_i = d_partialModel.getAssignment(x_i); ArithVar x_j = ARITHVAR_SENTINEL; diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index e02e001e3..abd5cb5e6 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -170,16 +170,12 @@ private: Node generateConflictBelow(ArithVar conflictVar); public: - /** Checks to make sure the assignment is consistent with the tableau. */ + /** + * Checks to make sure the assignment is consistent with the tableau. + * This code is for debugging. + */ void checkTableau(); -private: - //bool shouldEject(ArithVar var); - //void ejectInactiveVariables(); - -public: - //void reinjectVariable(ArithVar x); - /** * Computes the value of a basic variable using the assignments * of the values of the variables in the basic variable's row tableau. @@ -200,17 +196,16 @@ private: */ Node checkBasicForConflict(ArithVar b); - bool d_foundAConflict; - unsigned d_pivotsSinceConflict; + bool d_foundAConflict; // This field is used for statistics keeping ONLY! + unsigned d_pivotsSinceConflict; // This field is used for statistics keeping ONLY! /** These fields are designed to be accessable to TheoryArith methods. */ class Statistics { public: - IntStat d_statPivots, d_statUpdates, d_statAssertUpperConflicts; - IntStat d_statAssertLowerConflicts, d_statUpdateConflicts; - - IntStat d_statEjections, d_statUnEjections; + IntStat d_statPivots, d_statUpdates; + IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts; + IntStat d_statUpdateConflicts; IntStat d_statEarlyConflicts, d_statEarlyConflictImprovements; TimerStat d_selectInitialConflictTime; diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 75363af7f..5f142fe8a 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -46,12 +46,6 @@ void Tableau::addRow(ArithVar basicVar, ArithVar var = *varsIter; if(d_basicManager.isMember(var)){ - /* - if(!isActiveBasicVariable(var)){ - reinjectBasic(var); - } - Assert(isActiveBasicVariable(var)); - */ Assert(d_activeBasicVars.isMember(var)); ReducedRowVector& row_var = lookup(var); @@ -117,23 +111,3 @@ void Tableau::printTableau(){ } } } - - -/* -void Tableau::updateRow(ReducedRowVector* row){ - ArithVar basic = row->basic(); - for(ReducedRowVector::NonZeroIterator i=row->beginNonZero(), endIter = row->endNonZero(); i != endIter; ){ - ArithVar var = i->first; - ++i; - if(var != basic && d_basicManager.isMember(var)){ - ReducedRowVector* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); - - Assert(row_var != row); - row->substitute(*row_var); - - i = row->beginNonZero(); - endIter = row->endNonZero(); - } - } -} -*/ diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index f74e662cf..bd30dc13e 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -79,22 +79,23 @@ public: return *(d_rowsTable[var]); } - /* -private: - ReducedRowVector* lookupEjected(ArithVar var){ - Assert(isEjected(var)); - return d_rowsTable[var]; - } - */ public: - - uint32_t getRowCount(ArithVar x){ Assert(x < d_rowCount.size()); return d_rowCount[x]; } - + /** + * Adds a row to the tableau. + * The new row is equivalent to: + * basicVar = \sum_i coeffs[i] * variables[i] + * preconditions: + * basicVar is already declared to be basic + * basicVar does not have a row associated with it in the tableau. + * + * Note: each variables[i] does not have to be non-basic. + * Pivoting will be mimicked if it is basic. + */ void addRow(ArithVar basicVar, const std::vector& coeffs, const std::vector& variables); @@ -109,43 +110,7 @@ public: void printTableau(); - /* - bool isEjected(ArithVar var){ - return d_basicManager.isMember(var) && !isActiveBasicVariable(var); - } - */ - ReducedRowVector* removeRow(ArithVar basic); - - /* - void ejectBasic(ArithVar basic){ - Assert(d_basicManager.isMember(basic)); - Assert(isActiveBasicVariable(basic)); - - d_activeBasicVars.remove(basic); - } - */ - - /* - void reinjectBasic(ArithVar basic){ - AlwaysAssert(false); - - Assert(d_basicManager.isMember(basic)); - Assert(isEjected(basic)); - - ReducedRowVector* row = lookupEjected(basic); - d_activeBasicVars.add(basic); - updateRow(row); - } - */ -private: - /* - inline bool isActiveBasicVariable(ArithVar var){ - return d_activeBasicVars.isMember(var); - } - */ - - void updateRow(ReducedRowVector* row); }; }; /* namespace arith */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index ca3b76410..dbfa86a98 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -507,11 +507,6 @@ void TheoryArith::check(Effort effortLevel){ TNode rhs = eq[1]; Assert(rhs.getKind() == CONST_RATIONAL); ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL); - /* - if(d_tableau.isEjected(lhsVar)){ - d_simplex.reinjectVariable(lhsVar); - } - */ DeltaRational lhsValue = d_partialModel.getAssignment(lhsVar); DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL); if (lhsValue == rhsValue) { @@ -579,11 +574,6 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { switch(n.getKind()) { case kind::VARIABLE: { ArithVar var = asArithVar(n); - /* - if(d_tableau.isEjected(var)){ - d_simplex.reinjectVariable(var); - } - */ DeltaRational drat = d_partialModel.getAssignment(var); const Rational& delta = d_partialModel.getDelta(); -- 2.30.2