diff options
author | Tim King <taking@cs.nyu.edu> | 2010-10-28 21:46:44 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-10-28 21:46:44 +0000 |
commit | 50622574025f55417be020f30a4787714977ddd1 (patch) | |
tree | cd5a5e944216d354a4745e223aed64d3307ffde6 /src/theory/arith/tableau.h | |
parent | d2ff1974a7cd87d841e1bcaeb0d93665f70d9259 (diff) |
The Row implementation has no been replaced by RowVector and ReducedRowVector. A RowVector is an array of ArithVar and Rational pairs. (This replaces a map based implementation in Row.) ReducedRowVector is a RowVector with a notion of having a basic variable. The Tableau is now a collection of ReduceRowVector's. A major difference between ReducedRowVectors and Rows is that the iterator now includes the basic variable and its coefficient (always -1). Before only nonbasic members were accessible by the iterator.
Diffstat (limited to 'src/theory/arith/tableau.h')
-rw-r--r-- | src/theory/arith/tableau.h | 68 |
1 files changed, 10 insertions, 58 deletions
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 588b521b1..758e5d92d 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -25,8 +25,9 @@ #include "theory/arith/arithvar_dense_set.h" #include "theory/arith/normal_form.h" +#include "theory/arith/row_vector.h" + #include <ext/hash_map> -#include <map> #include <set> #ifndef __CVC4__THEORY__ARITH__TABLEAU_H @@ -36,57 +37,6 @@ namespace CVC4 { namespace theory { namespace arith { - -class Row { - ArithVar d_x_i; - - typedef std::map<ArithVar, Rational, std::greater<ArithVar> > CoefficientTable; - - CoefficientTable d_coeffs; - -public: - - typedef CoefficientTable::iterator iterator; - - /** - * Construct a row equal to: - * basic = \sum_{x_i} c_i * x_i - */ - Row(ArithVar basic, - const std::vector< Rational >& coefficients, - const std::vector< ArithVar >& variables); - - - iterator begin(){ - return d_coeffs.begin(); - } - - iterator end(){ - return d_coeffs.end(); - } - - ArithVar basicVar(){ - return d_x_i; - } - - bool has(ArithVar x_j){ - CoefficientTable::iterator x_jPos = d_coeffs.find(x_j); - return x_jPos != d_coeffs.end(); - } - - const Rational& lookup(ArithVar x_j){ - CoefficientTable::iterator x_jPos = d_coeffs.find(x_j); - Assert(x_jPos != d_coeffs.end()); - return (*x_jPos).second; - } - - void pivot(ArithVar x_j); - - void substitute(Row& row_s); - - void printRow(); -}; - class ArithVarSet { private: typedef std::list<ArithVar> VarList; @@ -138,7 +88,7 @@ private: class Tableau { private: - typedef std::vector< Row* > RowsTable; + typedef std::vector< ReducedRowVector* > RowsTable; ArithVarSet d_activeBasicVars; RowsTable d_rowsTable; @@ -171,19 +121,21 @@ public: return d_activeBasicVars.end(); } - Row* lookup(ArithVar var){ + ReducedRowVector* lookup(ArithVar var){ Assert(isActiveBasicVariable(var)); return d_rowsTable[var]; } private: - Row* lookupEjected(ArithVar var){ + ReducedRowVector* lookupEjected(ArithVar var){ Assert(isEjected(var)); return d_rowsTable[var]; } public: - void addRow(ArithVar basicVar, const std::vector<Rational>& coeffs, const std::vector<ArithVar>& variables); + void addRow(ArithVar basicVar, + const std::vector<Rational>& coeffs, + const std::vector<ArithVar>& variables); /** * preconditions: @@ -210,7 +162,7 @@ public: Assert(d_basicManager.isMember(basic)); Assert(isEjected(basic)); - Row* row = lookupEjected(basic); + ReducedRowVector* row = lookupEjected(basic); d_activeBasicVars.insert(basic); updateRow(row); } @@ -219,7 +171,7 @@ private: return d_activeBasicVars.inSet(var); } - void updateRow(Row* row); + void updateRow(ReducedRowVector* row); }; }; /* namespace arith */ |