From: Tim King Date: Sat, 5 Mar 2011 23:10:41 +0000 (+0000) Subject: - Adds PermissiveBackArithVarSet. This is very similar to ArithVarSet. The differenc... X-Git-Tag: cvc5-1.0.0~8667 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c01318241e5082478090cba15ff71f82b3f6da6a;p=cvc5.git - Adds PermissiveBackArithVarSet. This is very similar to ArithVarSet. The difference is that set.isMember(x) for an ArithVar x s.t. x > set.allocated() returns false for PermissiveBackArithVarSet and is an assertion failure for ArithVarSet. This cuts down on the memory usage of the ColumnMatrix slightly. --- diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h index 08bc905e0..89b1c9507 100644 --- a/src/theory/arith/arithvar_set.h +++ b/src/theory/arith/arithvar_set.h @@ -32,11 +32,20 @@ namespace arith { * This is an abstraction of a set of ArithVars. * This class is designed to provide constant time insertion, deletion, and element_of * and fast iteration. - * The cost of doing this is that it takes O(M) where M is the total number - * of ArithVars in memory. + * + * ArithVarSets come in 2 varieties ArithVarSet, and PermissiveBackArithVarSet. + * The default ArithVarSet assumes that there is no knowledge assumed about ArithVars + * that are greater than allocated(). Asking isMember() of such an ArithVar + * is an assertion failure. The cost of doing this is that it takes O(M) + * where M is the total number of ArithVars in memory. + * + * PermissiveBackArithVarSet means that all ArithVars are implicitly not in the set, + * and any ArithVar past the end of d_posVector is not in the set. + * A permissiveBack allows for less memory to be consumed on average. + * */ - -class ArithVarSet { +template +class ArithVarSetImpl { public: typedef std::vector VarList; private: @@ -50,7 +59,7 @@ private: public: typedef VarList::const_iterator iterator; - ArithVarSet() : d_list(), d_posVector() {} + ArithVarSetImpl() : d_list(), d_posVector() {} size_t size() const { return d_list.size(); @@ -78,13 +87,17 @@ public: } bool isMember(ArithVar x) const{ - Assert(x < allocated()); - return d_posVector[x] != ARITHVAR_SENTINEL; + if(permissiveBack && x >= allocated()){ + return false; + }else{ + Assert(x < allocated()); + return d_posVector[x] != ARITHVAR_SENTINEL; + } } /** Invalidates iterators */ void init(ArithVar x, bool val) { - Assert(x >= size()); + Assert(x >= allocated()); increaseSize(x); if(val){ add(x); @@ -94,6 +107,9 @@ public: /** Invalidates iterators */ void add(ArithVar x){ Assert(!isMember(x)); + if(permissiveBack && x >= allocated()){ + increaseSize(x); + } d_posVector[x] = size(); d_list.push_back(x); } @@ -139,6 +155,9 @@ public: } }; +typedef ArithVarSetImpl ArithVarSet; +typedef ArithVarSetImpl PermissiveBackArithVarSet; + }; /* namespace arith */ }; /* namespace theory */ }; /* namespace CVC4 */ diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp index 9159d3d6f..8edfb8612 100644 --- a/src/theory/arith/row_vector.cpp +++ b/src/theory/arith/row_vector.cpp @@ -182,7 +182,7 @@ ReducedRowVector::ReducedRowVector(ArithVar basic, const std::vector& variables, const std::vector& coefficients, std::vector& counts, - std::vector& cm): + std::vector& cm): d_basic(basic), d_rowCount(counts), d_columnMatrix(cm) { zip(variables, coefficients, d_entries); diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h index 45412ad3e..5fd471700 100644 --- a/src/theory/arith/row_vector.h +++ b/src/theory/arith/row_vector.h @@ -76,7 +76,7 @@ private: ArithVarContainsSet d_contains; std::vector& d_rowCount; - std::vector& d_columnMatrix; + std::vector& d_columnMatrix; public: @@ -85,7 +85,7 @@ public: const std::vector< ArithVar >& variables, const std::vector< Rational >& coefficients, std::vector& count, - std::vector& columnMatrix); + std::vector< PermissiveBackArithVarSet >& columnMatrix); ~ReducedRowVector(); void enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables, diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 7e83e1b9e..0e2c3797e 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -198,8 +198,8 @@ set tableauAndHasSet(Tableau& tab, ArithVar v){ set columnIteratorSet(Tableau& tab,ArithVar v){ set has; - ArithVarSet::iterator basicIter = tab.beginColumn(v); - ArithVarSet::iterator endIter = tab.endColumn(v); + Column::iterator basicIter = tab.beginColumn(v); + Column::iterator endIter = tab.endColumn(v); for(; basicIter != endIter; ++basicIter){ ArithVar basic = *basicIter; has.insert(basic); @@ -222,8 +222,8 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ DeltaRational diff = v - assignment_x_i; Assert(matchingSets(d_tableau, x_i)); - ArithVarSet::iterator basicIter = d_tableau.beginColumn(x_i); - ArithVarSet::iterator endIter = d_tableau.endColumn(x_i); + Column::iterator basicIter = d_tableau.beginColumn(x_i); + Column::iterator endIter = d_tableau.endColumn(x_i); for(; basicIter != endIter; ++basicIter){ ArithVar x_j = *basicIter; ReducedRowVector& row_j = d_tableau.lookup(x_j); @@ -295,8 +295,8 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR Assert(matchingSets(d_tableau, x_j)); - ArithVarSet::iterator basicIter = d_tableau.beginColumn(x_j); - ArithVarSet::iterator endIter = d_tableau.endColumn(x_j); + Column::iterator basicIter = d_tableau.beginColumn(x_j); + Column::iterator endIter = d_tableau.endColumn(x_j); for(; basicIter != endIter; ++basicIter){ ArithVar x_k = *basicIter; ReducedRowVector& row_k = d_tableau.lookup(x_k); diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 9769c628d..a8bcd28cc 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -36,7 +36,7 @@ void Tableau::internalCopy(const Tableau& tab){ Debug("tableau::copy") << "tableau copy "<< N << endl; if(N > 1){ - d_columnMatrix.insert(d_columnMatrix.end(), N, ArithVarSet()); + d_columnMatrix.insert(d_columnMatrix.end(), N, Column()); d_rowsTable.insert(d_rowsTable.end(), N, NULL); d_basicVariables.increaseSize(N-1); @@ -155,7 +155,7 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ row_s->pivot(x_s); - ArithVarSet::VarList copy(getColumn(x_s).getList()); + Column::VarList copy(getColumn(x_s).getList()); vector::iterator basicIter = copy.begin(), endIter = copy.end(); for(; basicIter != endIter; ++basicIter){ diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 6fe245285..dad4bb2f5 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -37,7 +37,7 @@ namespace CVC4 { namespace theory { namespace arith { -typedef ArithVarSet Column; +typedef PermissiveBackArithVarSet Column; typedef std::vector ColumnMatrix; @@ -79,15 +79,15 @@ public: d_rowsTable.push_back(NULL); d_rowCount.push_back(0); - d_columnMatrix.push_back(ArithVarSet()); + d_columnMatrix.push_back(PermissiveBackArithVarSet()); //TODO replace with version of ArithVarSet that handles misses as non-entries // not as buffer overflows - ColumnMatrix::iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end(); - for(; i != end; ++i){ - Column& col = *i; - col.increaseSize(d_columnMatrix.size()); - } + // ColumnMatrix::iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end(); + // for(; i != end; ++i){ + // Column& col = *i; + // col.increaseSize(d_columnMatrix.size()); + // } } bool isBasic(ArithVar v) const {