From: Tim King Date: Thu, 7 Oct 2010 18:47:42 +0000 (+0000) Subject: Small tableau optimization. X-Git-Tag: cvc5-1.0.0~8823 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f7668d89c65b66a8aa5b17a19f56831d48878298;p=cvc5.git Small tableau optimization. --- diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index df80c1118..aaeadb629 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -48,7 +48,6 @@ Row::Row(ArithVar basic, Assert(d_coeffs[var_i] != Rational(0,1)); } } - void Row::subsitute(Row& row_s){ ArithVar x_s = row_s.basicVar(); @@ -115,7 +114,7 @@ void Tableau::addRow(ArithVar basicVar, Assert(!isActiveBasicVariable(basicVar)); d_activeBasicVars.insert(basicVar); Row* row_current = new Row(basicVar,coeffs,variables); - d_activeRows[basicVar] = row_current; + 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 @@ -143,23 +142,22 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ Assert(d_basicManager.isBasic(x_r)); Assert(!d_basicManager.isBasic(x_s)); - RowsTable::iterator ptrRow_r = d_activeRows.find(x_r); - Assert(ptrRow_r != d_activeRows.end()); - - Row* row_s = (*ptrRow_r).second; - + Row* row_s = lookup(x_r); Assert(row_s->has(x_s)); - row_s->pivot(x_s); - d_activeRows.erase(ptrRow_r); + //Swap x_r and x_s in d_activeRows + d_rowsTable[x_s] = row_s; + d_rowsTable[x_r] = NULL; + d_activeBasicVars.erase(x_r); d_basicManager.makeNonbasic(x_r); - d_activeRows.insert(std::make_pair(x_s,row_s)); d_activeBasicVars.insert(x_s); d_basicManager.makeBasic(x_s); - for(VarSet::iterator basicIter = begin(), endIter = end(); + row_s->pivot(x_s); + + for(ArithVarSet::iterator basicIter = begin(), endIter = end(); basicIter != endIter; ++basicIter){ ArithVar basic = *basicIter; Row* row_k = lookup(basic); @@ -169,19 +167,16 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ } } } - void Tableau::printTableau(){ - for(VarSet::iterator basicIter = begin(), endIter = end(); - basicIter != endIter; ++basicIter){ - ArithVar basic = *basicIter; - Row* row_k = lookup(basic); - row_k->printRow(); - } - for(RowsTable::iterator basicIter = d_inactiveRows.begin(), endIter = d_inactiveRows.end(); - basicIter != endIter; ++basicIter){ - ArithVar basic = (*basicIter).first; - Row* row_k = lookupEjected(basic); - row_k->printRow(); + Debug("tableau") << "Tableau::d_activeRows" << endl; + + typedef RowsTable::iterator table_iter; + for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end(); + rowIter != end; ++rowIter){ + Row* row_k = *rowIter; + if(row_k != NULL){ + row_k->printRow(); + } } } diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index ed173a182..a69493ee0 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -88,49 +88,98 @@ public: void printRow(); }; -class Tableau { +class ArithVarSet { +private: + typedef std::list VarList; + public: - typedef std::set VarSet; + typedef VarList::const_iterator iterator; private: - typedef __gnu_cxx::hash_map RowsTable; + VarList d_list; + std::vector< VarList::iterator > d_posVector; + +public: + ArithVarSet() : d_list(), d_posVector() {} + + iterator begin() const{ return d_list.begin(); } + iterator end() const{ return d_list.end(); } + + void insert(ArithVar av){ + Assert(inRange(av) ); + Assert(!inSet(av) ); + + d_posVector[av] = d_list.insert(d_list.end(), av); + } + + void erase(ArithVar var){ + Assert( inRange(var) ); + Assert( inSet(var) ); + + d_list.erase(d_posVector[var]); + d_posVector[var] = d_list.end(); + } - VarSet d_activeBasicVars; - RowsTable d_activeRows, d_inactiveRows; + void increaseSize(){ + d_posVector.push_back(d_list.end()); + } + + bool inSet(ArithVar v) const{ + Assert(inRange(v) ); + + return d_posVector[v] != d_list.end(); + } + +private: + bool inRange(ArithVar v) const{ + return v < d_posVector.size(); + } +}; + +class Tableau { +private: + + typedef std::vector< Row* > RowsTable; + + ArithVarSet d_activeBasicVars; + RowsTable d_rowsTable; ActivityMonitor& d_activityMonitor; IsBasicManager& d_basicManager; - public: /** * Constructs an empty tableau. */ Tableau(ActivityMonitor &am, IsBasicManager& bm) : d_activeBasicVars(), - d_activeRows(), - d_inactiveRows(), + d_rowsTable(), d_activityMonitor(am), d_basicManager(bm) {} - VarSet::iterator begin(){ + void increaseSize(){ + d_activeBasicVars.increaseSize(); + d_rowsTable.push_back(NULL); + } + + ArithVarSet::iterator begin(){ return d_activeBasicVars.begin(); } - VarSet::iterator end(){ + ArithVarSet::iterator end(){ return d_activeBasicVars.end(); } Row* lookup(ArithVar var){ Assert(isActiveBasicVariable(var)); - return d_activeRows[var]; + return d_rowsTable[var]; } private: Row* lookupEjected(ArithVar var){ Assert(isEjected(var)); - return d_inactiveRows[var]; + return d_rowsTable[var]; } public: @@ -147,18 +196,14 @@ public: void printTableau(); bool isEjected(ArithVar var){ - return d_inactiveRows.find(var) != d_inactiveRows.end(); + return d_basicManager.isBasic(var) && !isActiveBasicVariable(var); } void ejectBasic(ArithVar basic){ Assert(d_basicManager.isBasic(basic)); Assert(isActiveBasicVariable(basic)); - Row* row = lookup(basic); - d_activeRows.erase(basic); d_activeBasicVars.erase(basic); - - d_inactiveRows.insert(std::make_pair(basic, row)); } void reinjectBasic(ArithVar basic){ @@ -166,16 +211,12 @@ public: Assert(isEjected(basic)); Row* row = lookupEjected(basic); - - d_inactiveRows.erase(basic); d_activeBasicVars.insert(basic); - d_activeRows.insert(std::make_pair(basic, row)); - updateRow(row); } private: inline bool isActiveBasicVariable(ArithVar var){ - return d_activeBasicVars.find(var) != d_activeBasicVars.end(); + return d_activeBasicVars.inSet(var); } void updateRow(Row* row); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4440a8e15..26bb58e90 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -138,7 +138,7 @@ bool TheoryArith::shouldEject(ArithVar var){ } ArithVar TheoryArith::findBasicRow(ArithVar variable){ - for(Tableau::VarSet::iterator basicIter = d_tableau.begin(); + for(ArithVarSet::iterator basicIter = d_tableau.begin(); basicIter != d_tableau.end(); ++basicIter){ ArithVar x_j = *basicIter; @@ -241,6 +241,7 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ d_activityMonitor.initActivity(varX); d_basicManager.init(varX, basic); + d_tableau.increaseSize(); Debug("arith::arithvar") << x << " |-> " << varX << endl; @@ -501,7 +502,7 @@ void TheoryArith::update(ArithVar x_i, DeltaRational& v){ << assignment_x_i << "|-> " << v << endl; DeltaRational diff = v - assignment_x_i; - for(Tableau::VarSet::iterator basicIter = d_tableau.begin(); + for(ArithVarSet::iterator basicIter = d_tableau.begin(); basicIter != d_tableau.end(); ++basicIter){ ArithVar x_j = *basicIter; @@ -545,7 +546,7 @@ void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta; d_partialModel.setAssignment(x_j, tmp); - for(Tableau::VarSet::iterator basicIter = d_tableau.begin(); + for(ArithVarSet::iterator basicIter = d_tableau.begin(); basicIter != d_tableau.end(); ++basicIter){ ArithVar x_k = *basicIter; @@ -589,7 +590,7 @@ ArithVar TheoryArith::selectSmallestInconsistentVar(){ } if(Debug.isOn("paranoid:variables")){ - for(Tableau::VarSet::iterator basicIter = d_tableau.begin(); + for(ArithVarSet::iterator basicIter = d_tableau.begin(); basicIter != d_tableau.end(); ++basicIter){ @@ -884,7 +885,7 @@ void TheoryArith::check(Effort level){ */ void TheoryArith::checkTableau(){ - for(Tableau::VarSet::iterator basicIter = d_tableau.begin(); + for(ArithVarSet::iterator basicIter = d_tableau.begin(); basicIter != d_tableau.end(); ++basicIter){ ArithVar basic = *basicIter; Row* row_k = d_tableau.lookup(basic);