diff options
Diffstat (limited to 'src/theory/arith/tableau.h')
-rw-r--r-- | src/theory/arith/tableau.h | 85 |
1 files changed, 63 insertions, 22 deletions
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<ArithVar> VarList; + public: - typedef std::set<ArithVar> VarSet; + typedef VarList::const_iterator iterator; private: - typedef __gnu_cxx::hash_map<ArithVar, Row*> 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); |