From 907850f58916c4a6890156a08301a68b5be43fcb Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 17 Feb 2011 17:46:31 +0000 Subject: [PATCH] Row ejection is now completely disabled. Another commit cleaning this one up will follow shortly. --- src/theory/arith/simplex.cpp | 73 +++++++++++++++++++------------ src/theory/arith/simplex.h | 6 +-- src/theory/arith/tableau.cpp | 41 +++++++++++------ src/theory/arith/tableau.h | 21 +++++++-- src/theory/arith/theory_arith.cpp | 20 +++++---- 5 files changed, 106 insertions(+), 55 deletions(-) diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index f7e3c112c..9e3ba726a 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -60,6 +60,7 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ } +/* void SimplexDecisionProcedure::ejectInactiveVariables(){ return; //die die die @@ -75,7 +76,9 @@ void SimplexDecisionProcedure::ejectInactiveVariables(){ } } } +*/ +/* void SimplexDecisionProcedure::reinjectVariable(ArithVar x){ ++(d_statistics.d_statUnEjections); @@ -85,7 +88,9 @@ void SimplexDecisionProcedure::reinjectVariable(ArithVar x){ DeltaRational assignment = computeRowValue(x, false); d_partialModel.setAssignment(x,safeAssignment,assignment); } +*/ +/* bool SimplexDecisionProcedure::shouldEject(ArithVar var){ if(d_partialModel.hasEitherBound(var)){ return false; @@ -98,14 +103,17 @@ bool SimplexDecisionProcedure::shouldEject(ArithVar var){ } 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 @@ -138,9 +146,11 @@ 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 @@ -176,9 +186,11 @@ 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. @@ -234,10 +246,10 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ basicIter != d_tableau.end(); ++basicIter){ ArithVar x_j = *basicIter; - ReducedRowVector* row_j = d_tableau.lookup(x_j); + ReducedRowVector& row_j = d_tableau.lookup(x_j); - if(row_j->has(x_i)){ - const Rational& a_ji = row_j->lookup(x_i); + if(row_j.has(x_i)){ + const Rational& a_ji = row_j.lookup(x_i); const DeltaRational& assignment = d_partialModel.getAssignment(x_j); DeltaRational nAssignment = assignment+(diff * a_ji); @@ -263,9 +275,9 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR if(Debug.isOn("arith::pivotAndUpdate")){ Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl; - ReducedRowVector* row_k = d_tableau.lookup(x_i); - for(ReducedRowVector::NonZeroIterator varIter = row_k->beginNonZero(); - varIter != row_k->endNonZero(); + ReducedRowVector& row_k = d_tableau.lookup(x_i); + for(ReducedRowVector::NonZeroIterator varIter = row_k.beginNonZero(); + varIter != row_k.endNonZero(); ++varIter){ ArithVar var = varIter->first; @@ -285,8 +297,8 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR } - ReducedRowVector* row_i = d_tableau.lookup(x_i); - const Rational& a_ij = row_i->lookup(x_j); + ReducedRowVector& row_i = d_tableau.lookup(x_i); + const Rational& a_ij = row_i.lookup(x_j); const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i); @@ -300,14 +312,13 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta; d_partialModel.setAssignment(x_j, tmp); - for(ArithVarSet::iterator basicIter = d_tableau.begin(); - basicIter != d_tableau.end(); - ++basicIter){ + ArithVarSet::iterator basicIter = d_tableau.begin(), end = d_tableau.end(); + for(; basicIter != end; ++basicIter){ ArithVar x_k = *basicIter; - ReducedRowVector* row_k = d_tableau.lookup(x_k); + ReducedRowVector& row_k = d_tableau.lookup(x_k); - if(x_k != x_i && row_k->has(x_j)){ - const Rational& a_kj = row_k->lookup(x_j); + if(x_k != x_i && row_k.has(x_j)){ + const Rational& a_kj = row_k.lookup(x_j); DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj); d_partialModel.setAssignment(x_k, nextAssignment); @@ -384,12 +395,12 @@ ArithVar SimplexDecisionProcedure::selectSmallestInconsistentVar(){ template ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ - ReducedRowVector* row_i = d_tableau.lookup(x_i); + ReducedRowVector& row_i = d_tableau.lookup(x_i); ArithVar slack = ARITHVAR_SENTINEL; uint32_t numRows = std::numeric_limits::max(); - for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); + for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); nbi != end; ++nbi){ ArithVar nonbasic = getArithVar(*nbi); if(nonbasic == x_i) continue; @@ -541,7 +552,7 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ Debug("arith") << "updateInconsistentVars" << endl; uint32_t iteratationNum = 0; - static const int EJECT_FREQUENCY = 10; + //static const int EJECT_FREQUENCY = 10; while(!d_pivotStage || iteratationNum <= d_numVariables){ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } @@ -554,8 +565,10 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ } ++iteratationNum; + /* if(iteratationNum % EJECT_FREQUENCY == 0) ejectInactiveVariables(); + */ DeltaRational beta_i = d_partialModel.getAssignment(x_i); ArithVar x_j = ARITHVAR_SENTINEL; @@ -605,7 +618,7 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ - ReducedRowVector* row_i = d_tableau.lookup(conflictVar); + ReducedRowVector& row_i = d_tableau.lookup(conflictVar); NodeBuilder<> nb(kind::AND); TNode bound = d_partialModel.getUpperConstraint(conflictVar); @@ -617,8 +630,10 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ nb << bound; - for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); - nbi != end; ++nbi){ + typedef ReducedRowVector::NonZeroIterator RowIterator; + RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); + + for(; nbi != end; ++nbi){ ArithVar nonbasic = getArithVar(*nbi); if(nonbasic == conflictVar) continue; @@ -645,7 +660,7 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ } Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ - ReducedRowVector* row_i = d_tableau.lookup(conflictVar); + ReducedRowVector& row_i = d_tableau.lookup(conflictVar); NodeBuilder<> nb(kind::AND); TNode bound = d_partialModel.getLowerConstraint(conflictVar); @@ -656,7 +671,9 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ << " " << bound << endl; nb << bound; - for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); nbi != end; ++nbi){ + typedef ReducedRowVector::NonZeroIterator RowIterator; + RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); + for(; nbi != end; ++nbi){ ArithVar nonbasic = getArithVar(*nbi); if(nonbasic == conflictVar) continue; @@ -691,11 +708,11 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe Assert(d_basicManager.isMember(x)); DeltaRational sum = d_constants.d_ZERO_DELTA; - ReducedRowVector* row = d_tableau.lookup(x); - for(ReducedRowVector::NonZeroIterator i = row->beginNonZero(), end = row->endNonZero(); + ReducedRowVector& row = d_tableau.lookup(x); + for(ReducedRowVector::NonZeroIterator i = row.beginNonZero(), end = row.endNonZero(); i != end;++i){ ArithVar nonbasic = getArithVar(*i); - if(nonbasic == row->basic()) continue; + if(nonbasic == row.basic()) continue; const Rational& coeff = getCoefficient(*i); const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe); @@ -732,11 +749,11 @@ void SimplexDecisionProcedure::checkTableau(){ for(ArithVarSet::iterator basicIter = d_tableau.begin(); basicIter != d_tableau.end(); ++basicIter){ ArithVar basic = *basicIter; - ReducedRowVector* row_k = d_tableau.lookup(basic); + ReducedRowVector& row_k = d_tableau.lookup(basic); DeltaRational sum; Debug("paranoid:check_tableau") << "starting row" << basic << endl; - for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k->beginNonZero(); - nonbasicIter != row_k->endNonZero(); + for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k.beginNonZero(); + nonbasicIter != row_k.endNonZero(); ++nonbasicIter){ ArithVar nonbasic = nonbasicIter->first; if(basic == nonbasic) continue; diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 587f468e0..7589e7936 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -178,11 +178,11 @@ public: void checkTableau(); private: - bool shouldEject(ArithVar var); - void ejectInactiveVariables(); + //bool shouldEject(ArithVar var); + //void ejectInactiveVariables(); public: - void reinjectVariable(ArithVar x); + //void reinjectVariable(ArithVar x); /** * Computes the value of a basic variable using the assignments diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 1cf6d07cd..95ea166af 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -32,41 +32,54 @@ void Tableau::addRow(ArithVar basicVar, Assert(d_basicManager.isMember(basicVar)); //The new basic variable cannot already be a basic variable - Assert(!isActiveBasicVariable(basicVar)); + Assert(!d_activeBasicVars.isMember(basicVar)); d_activeBasicVars.add(basicVar); ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount); d_rowsTable[basicVar] = row_current; //A variable in the row may have been made non-basic already. //If this is the case we fake pivoting this variable - vector::const_iterator coeffsIter = coeffs.begin(); - vector::const_iterator coeffsEnd = coeffs.end(); - vector::const_iterator varsIter = variables.begin(); + vector::const_iterator varsEnd = variables.end(); - for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){ + for( ; varsIter != varsEnd; ++varsIter){ 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); - row_current->substitute(*row_var); + ReducedRowVector& row_var = lookup(var); + row_current->substitute(row_var); } } } +ReducedRowVector* Tableau::removeRow(ArithVar basic){ + Assert(d_basicManager.isMember(basic)); + Assert(d_activeBasicVars.isMember(basic)); + + ReducedRowVector* row = d_rowsTable[basic]; + + d_activeBasicVars.remove(basic); + d_rowsTable[basic] = NULL; + + return row; +} + void Tableau::pivot(ArithVar x_r, ArithVar x_s){ Assert(d_basicManager.isMember(x_r)); Assert(!d_basicManager.isMember(x_s)); - Debug("tableau") << "Tableau::pivot(" - << x_r <<", " <has(x_s)); //Swap x_r and x_s in d_activeRows @@ -86,10 +99,10 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ ArithVar basic = *basicIter; if(basic == x_s) continue; - ReducedRowVector* row_k = lookup(basic); - if(row_k->has(x_s)){ + ReducedRowVector& row_k = lookup(basic); + if(row_k.has(x_s)){ d_activityMonitor[basic] += 30; - row_k->substitute(*row_s); + row_k.substitute(*row_s); } } } @@ -107,6 +120,7 @@ void Tableau::printTableau(){ } +/* void Tableau::updateRow(ReducedRowVector* row){ ArithVar basic = row->basic(); for(ReducedRowVector::NonZeroIterator i=row->beginNonZero(), endIter = row->endNonZero(); i != endIter; ){ @@ -123,3 +137,4 @@ void Tableau::updateRow(ReducedRowVector* row){ } } } +*/ diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 05fcf6cf8..5f2a36505 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -76,23 +76,28 @@ public: return d_activeBasicVars.end(); } - ReducedRowVector* lookup(ArithVar var){ - Assert(isActiveBasicVariable(var)); - return d_rowsTable[var]; + ReducedRowVector& lookup(ArithVar var){ + Assert(d_activeBasicVars.isMember(var)); + Assert(d_rowsTable[var] != NULL); + 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]; } + void addRow(ArithVar basicVar, const std::vector& coeffs, const std::vector& variables); @@ -107,17 +112,24 @@ 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); @@ -128,10 +140,13 @@ public: d_activeBasicVars.add(basic); updateRow(row); } + */ private: + /* inline bool isActiveBasicVariable(ArithVar var){ return d_activeBasicVars.isMember(var); } + */ void updateRow(ReducedRowVector* row); }; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1e1ac03ba..ecc740655 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -199,13 +199,13 @@ ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){ basicIter != d_tableau.end(); ++basicIter){ ArithVar x_j = *basicIter; - ReducedRowVector* row_j = d_tableau.lookup(x_j); + ReducedRowVector& row_j = d_tableau.lookup(x_j); - if(row_j->has(variable)){ + if(row_j.has(variable)){ if((bestBasic == ARITHVAR_SENTINEL) || - (bestBasic != ARITHVAR_SENTINEL && row_j->size() < rowLength)){ + (bestBasic != ARITHVAR_SENTINEL && row_j.size() < rowLength)){ bestBasic = x_j; - rowLength = row_j->size(); + rowLength = row_j.size(); } } } @@ -511,9 +511,11 @@ 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) { @@ -581,9 +583,11 @@ 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(); @@ -683,6 +687,8 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ if(basic == ARITHVAR_SENTINEL){ //Case 3) do nothing else. //TODO think hard about if this is okay... + //Probably wrecks havoc with model generation + //*feh* DO IT ANYWAYS! return; } @@ -692,11 +698,9 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ Assert(d_basicManager.isMember(v)); - d_tableau.ejectBasic(v); //remove the row from the tableau - //TODO: It would be better to remove the row from the tableau - //and store this row in another data structure - + ReducedRowVector* row = d_tableau.removeRow(v); + d_removedRows[v] = row; Debug("arith::permanentlyRemoveVariable") << v << " died an ignoble death."<< endl; ++(d_statistics.d_permanentlyRemovedVariables); -- 2.30.2