diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-29 22:01:30 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-29 22:01:30 +0000 |
commit | b1200db566d19132a3f0861eeef35f3c0aaa0a08 (patch) | |
tree | 9d7855232f833230ca5d92cb8948e5b894dff197 /src/theory/arith/tableau.h | |
parent | 200a0b748085004595a948fdea7c73a5ab45bdcf (diff) |
This commit merges the decaying-rows branch into the main trunk.
Diffstat (limited to 'src/theory/arith/tableau.h')
-rw-r--r-- | src/theory/arith/tableau.h | 97 |
1 files changed, 76 insertions, 21 deletions
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 0cadc8d10..4e4088bb0 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -22,6 +22,8 @@ #include "expr/attribute.h" #include "theory/arith/basic.h" +#include "theory/arith/arith_activity.h" + #include <ext/hash_map> #include <set> @@ -170,28 +172,35 @@ public: private: typedef __gnu_cxx::hash_map<TNode, Row*, NodeHashFunction> RowsTable; - VarSet d_basicVars; - RowsTable d_rows; + VarSet d_activeBasicVars; + RowsTable d_activeRows, d_inactiveRows; public: /** * Constructs an empty tableau. */ - Tableau() : d_basicVars(), d_rows() {} + Tableau() : d_activeBasicVars(), d_activeRows(), d_inactiveRows() {} VarSet::iterator begin(){ - return d_basicVars.begin(); + return d_activeBasicVars.begin(); } VarSet::iterator end(){ - return d_basicVars.end(); + return d_activeBasicVars.end(); } Row* lookup(TNode var){ - Assert(contains(var)); - return d_rows[var]; + Assert(isActiveBasicVariable(var)); + return d_activeRows[var]; + } + +private: + Row* lookupEjected(TNode var){ + Assert(isEjected(var)); + return d_inactiveRows[var]; } +public: void addRow(TNode eq){ Assert(eq.getKind() == kind::EQUAL); @@ -203,10 +212,10 @@ public: Assert(var.getAttribute(IsBasic())); //The new basic variable cannot already be a basic variable - Assert(d_basicVars.find(var) == d_basicVars.end()); - d_basicVars.insert(var); + Assert(!isActiveBasicVariable(var)); + d_activeBasicVars.insert(var); Row* row_var = new Row(var,sum); - d_rows[var] = row_var; + d_activeRows[var] = row_var; //A variable in the row may have been made non-basic already. //If this is the case we fake pivoting this variable @@ -217,7 +226,7 @@ public: Assert(child[0].getKind() == kind::CONST_RATIONAL); TNode c = child[1]; Assert(var.getMetaKind() == kind::metakind::VARIABLE); - if(contains(c)){ + if(isActiveBasicVariable(c)){ Row* row_c = lookup(c); row_var->subsitute(*row_c); } @@ -231,42 +240,88 @@ public: * a_rs != 0. */ void pivot(TNode x_r, TNode x_s){ - RowsTable::iterator ptrRow_r = d_rows.find(x_r); - Assert(ptrRow_r != d_rows.end()); + RowsTable::iterator ptrRow_r = d_activeRows.find(x_r); + Assert(ptrRow_r != d_activeRows.end()); Row* row_s = (*ptrRow_r).second; Assert(row_s->has(x_s)); row_s->pivot(x_s); - d_rows.erase(ptrRow_r); - d_basicVars.erase(x_r); + d_activeRows.erase(ptrRow_r); + d_activeBasicVars.erase(x_r); makeNonbasic(x_r); - d_rows.insert(std::make_pair(x_s,row_s)); - d_basicVars.insert(x_s); + d_activeRows.insert(std::make_pair(x_s,row_s)); + d_activeBasicVars.insert(x_s); makeBasic(x_s); - for(VarSet::iterator basicIter = begin(); basicIter != end(); ++basicIter){ + for(VarSet::iterator basicIter = begin(), endIter = end(); + basicIter != endIter; ++basicIter){ TNode basic = *basicIter; Row* row_k = lookup(basic); if(row_k->basicVar() != x_s){ if(row_k->has(x_s)){ + increaseActivity(basic, 30); + row_k->subsitute(*row_s); } } } } void printTableau(){ - for(VarSet::iterator basicIter = begin(); basicIter != end(); ++basicIter){ + for(VarSet::iterator basicIter = begin(), endIter = end(); + basicIter != endIter; ++basicIter){ TNode basic = *basicIter; Row* row_k = lookup(basic); row_k->printRow(); } } + + bool isEjected(TNode var){ + return d_inactiveRows.find(var) != d_inactiveRows.end(); + } + + void ejectBasic(TNode basic){ + Assert(isActiveBasicVariable(basic)); + + Row* row = lookup(basic); + d_activeRows.erase(basic); + d_activeBasicVars.erase(basic); + + d_inactiveRows.insert(make_pair(basic, row)); + } + + void reinjectBasic(TNode basic){ + Assert(isEjected(basic)); + + Row* row = lookupEjected(basic); + + d_inactiveRows.erase(basic); + d_activeBasicVars.insert(basic); + d_activeRows.insert(make_pair(basic, row)); + + updateRow(row); + } private: - inline bool contains(TNode var){ - return d_basicVars.find(var) != d_basicVars.end(); + inline bool isActiveBasicVariable(TNode var){ + return d_activeBasicVars.find(var) != d_activeBasicVars.end(); + } + + void updateRow(Row* row){ + for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){ + TNode var = *i; + ++i; + if(isBasic(var)){ + Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); + + Assert(row_var != row); + row->subsitute(*row_var); + + i = row->begin(); + endIter = row->end(); + } + } } }; |