diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-07-09 15:47:24 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-07-09 15:47:24 +0000 |
commit | fbcdcf6a0ad9766eb87566c7a9ec5876a65f5585 (patch) | |
tree | 353d29221d74c399046590bc40a32e898c0c59f5 /src/theory/arith/tableau.h | |
parent | ea57b1b4be4cbebccde013b326128a599ae193ee (diff) |
the tableaux optimization
Diffstat (limited to 'src/theory/arith/tableau.h')
-rw-r--r-- | src/theory/arith/tableau.h | 52 |
1 files changed, 19 insertions, 33 deletions
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 7f414db66..12d93d9fe 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -26,6 +26,7 @@ #include <ext/hash_map> +#include <map> #include <set> #ifndef __CVC4__THEORY__ARITH__TABLEAU_H @@ -39,14 +40,13 @@ namespace arith { class Row { TNode d_x_i; - typedef __gnu_cxx::hash_map<TNode, Rational, NodeHashFunction> CoefficientTable; + typedef std::map<TNode, Rational> CoefficientTable; - std::set<TNode> d_nonbasic; CoefficientTable d_coeffs; public: - typedef std::set<TNode>::iterator iterator; + typedef CoefficientTable::iterator iterator; /** * Construct a row equal to: @@ -54,7 +54,6 @@ public: */ Row(TNode basic, TNode sum): d_x_i(basic), - d_nonbasic(), d_coeffs(){ Assert(d_x_i.getMetaKind() == kind::metakind::VARIABLE); @@ -70,7 +69,6 @@ public: Assert(var_i.getKind() == kind::VARIABLE); Assert(!has(var_i)); - d_nonbasic.insert(var_i); d_coeffs[var_i] = coeff.getConst<Rational>(); Assert(coeff.getConst<Rational>() != Rational(0,1)); Assert(d_coeffs[var_i] != Rational(0,1)); @@ -78,11 +76,11 @@ public: } iterator begin(){ - return d_nonbasic.begin(); + return d_coeffs.begin(); } iterator end(){ - return d_nonbasic.end(); + return d_coeffs.end(); } TNode basicVar(){ @@ -105,15 +103,11 @@ public: d_coeffs[d_x_i] = Rational(Integer(-1)); d_coeffs.erase(x_j); - d_nonbasic.erase(x_j); - d_nonbasic.insert(d_x_i); d_x_i = x_j; - for(iterator nonbasicIter = d_nonbasic.begin(); - nonbasicIter != d_nonbasic.end(); - ++nonbasicIter){ - TNode nb = *nonbasicIter; - d_coeffs[nb] *= negInverseA_rs; + for(iterator nonbasicIter = begin(), nonbasicIter_end = end(); + nonbasicIter != nonbasicIter_end; ++nonbasicIter){ + nonbasicIter->second *= negInverseA_rs; } } @@ -122,7 +116,6 @@ public: TNode x_s = row_s.basicVar(); Assert(has(x_s)); - Assert(d_nonbasic.find(x_s) != d_nonbasic.end()); Assert(x_s != d_x_i); Rational zero(0,1); @@ -130,13 +123,11 @@ public: Rational a_rs = lookup(x_s); Assert(a_rs != zero); d_coeffs.erase(x_s); - d_nonbasic.erase(x_s); - for(iterator iter = row_s.d_nonbasic.begin(); - iter != row_s.d_nonbasic.end(); - ++iter){ - TNode x_j = *iter; - Rational a_sj = row_s.lookup(x_j); + for(iterator iter = row_s.begin(), iter_end = row_s.end(); + iter != iter_end; ++iter){ + TNode x_j = iter->first; + Rational a_sj = iter->second; a_sj *= a_rs; CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j); @@ -144,10 +135,8 @@ public: coeff_iter->second += a_sj; if(coeff_iter->second == zero){ d_coeffs.erase(coeff_iter); - d_nonbasic.erase(x_j); } }else{ - d_nonbasic.insert(x_j); d_coeffs.insert(std::make_pair(x_j,a_sj)); } } @@ -155,10 +144,10 @@ public: void printRow(){ Debug("tableau") << d_x_i << " "; - for(iterator nonbasicIter = d_nonbasic.begin(); - nonbasicIter != d_nonbasic.end(); + for(iterator nonbasicIter = d_coeffs.begin(); + nonbasicIter != d_coeffs.end(); ++nonbasicIter){ - TNode nb = *nonbasicIter; + TNode nb = nonbasicIter->first; Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}"; } Debug("tableau") << std::endl; @@ -260,12 +249,9 @@ public: 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); - } + if(row_k->has(x_s)){ + increaseActivity(basic, 30); + row_k->subsitute(*row_s); } } } @@ -310,7 +296,7 @@ private: void updateRow(Row* row){ for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){ - TNode var = *i; + TNode var = i->first; ++i; if(isBasic(var)){ Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); |