From: Tim King Date: Thu, 28 Oct 2010 21:46:44 +0000 (+0000) Subject: The Row implementation has no been replaced by RowVector and ReducedRowVector. A... X-Git-Tag: cvc5-1.0.0~8763 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=50622574025f55417be020f30a4787714977ddd1;p=cvc5.git 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. --- diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 21ec99390..907c8820f 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -21,6 +21,8 @@ libarith_la_SOURCES = \ arithvar_dense_set.h \ tableau.h \ tableau.cpp \ + row_vector.h \ + row_vector.cpp \ arith_propagator.h \ arith_propagator.cpp \ theory_arith.h \ diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 0a962283c..1c9b2685d 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -740,6 +740,11 @@ public: static Comparison parseNormalForm(TNode n); + inline static bool isNormalAtom(TNode n){ + Comparison parse = Comparison::parseNormalForm(n); + return parse.isNormalForm(); + } + };/* class Comparison */ }/* CVC4::theory::arith namespace */ diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp new file mode 100644 index 000000000..6835fc435 --- /dev/null +++ b/src/theory/arith/row_vector.cpp @@ -0,0 +1,131 @@ + +#include "theory/arith/row_vector.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::arith ; + +void RowVector::zip(const vector< ArithVar >& variables, + const vector< Rational >& coefficients, + VarCoeffArray& output){ + + Assert(coefficients.size() == variables.size() ); + + vector::const_iterator coeffIter = coefficients.begin(); + vector::const_iterator coeffEnd = coefficients.end(); + vector::const_iterator varIter = variables.begin(); + + for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){ + const Rational& coeff = *coeffIter; + ArithVar var_i = *varIter; + + output.push_back(make_pair(var_i, coeff)); + } +} + +RowVector::RowVector(const vector< ArithVar >& variables, + const vector< Rational >& coefficients){ + zip(variables, coefficients, d_entries); + + std::sort(d_entries.begin(), d_entries.end(), cmp); + + Assert(isSorted(d_entries, true)); + Assert(noZeroCoefficients(d_entries)); +} + +void RowVector::merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c){ + VarCoeffArray copy = arr; + arr.clear(); + + iterator curr1 = copy.begin(); + iterator end1 = copy.end(); + + NonZeroIterator curr2 = other.begin(); + NonZeroIterator end2 = other.end(); + + while(curr1 != end1 && curr2 != end2){ + if(getArithVar(*curr1) < getArithVar(*curr2)){ + arr.push_back(*curr1); + ++curr1; + }else if(getArithVar(*curr1) > getArithVar(*curr2)){ + arr.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2))); + ++curr2; + }else{ + Rational res = getCoefficient(*curr1) + c * getCoefficient(*curr2); + if(res != 0){ + arr.push_back(make_pair(getArithVar(*curr1), res)); + } + ++curr1; + ++curr2; + } + } + while(curr1 != end1){ + arr.push_back(*curr1); + ++curr1; + } + while(curr2 != end2){ + arr.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2))); + ++curr2; + } +} + +void RowVector::multiply(const Rational& c){ + Assert(c != 0); + + for(iterator i = d_entries.begin(), end = d_entries.end(); i != end; ++i){ + getCoefficient(*i) *= c; + } +} + +void RowVector::addRowTimesConstant(const Rational& c, const RowVector& other){ + Assert(c != 0); + + merge(d_entries, other.d_entries, c); +} + +void RowVector::printRow(){ + for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){ + ArithVar nb = getArithVar(*i); + Debug("tableau") << "{" << nb << "," << getCoefficient(*i) << "}"; + } + Debug("tableau") << std::endl; +} + +ReducedRowVector::ReducedRowVector(ArithVar basic, + const vector& variables, + const vector& coefficients): + RowVector(variables, coefficients), d_basic(basic){ + + + VarCoeffArray justBasic; + justBasic.push_back(make_pair(basic, Rational(-1))); + + merge(d_entries,justBasic, Rational(1)); + + Assert(wellFormed()); +} + +void ReducedRowVector::substitute(const ReducedRowVector& row_s){ + ArithVar x_s = row_s.basic(); + + Assert(has(x_s)); + Assert(x_s != basic()); + + Rational a_rs = lookup(x_s); + Assert(a_rs != 0); + + addRowTimesConstant(a_rs, row_s); + + Assert(!has(x_s)); + Assert(wellFormed()); +} + +void ReducedRowVector::pivot(ArithVar x_j){ + Assert(has(x_j)); + Assert(basic() != x_j); + Rational negInverseA_rs = -(lookup(x_j).inverse()); + multiply(negInverseA_rs); + d_basic = x_j; + + Assert(wellFormed()); +} diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h new file mode 100644 index 000000000..2c88721ea --- /dev/null +++ b/src/theory/arith/row_vector.h @@ -0,0 +1,176 @@ + + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__ROW_VECTOR_H +#define __CVC4__THEORY__ARITH__ROW_VECTOR_H + +#include "theory/arith/arith_utilities.h" +#include "util/rational.h" +#include + +namespace CVC4 { +namespace theory { +namespace arith { + +typedef std::pair VarCoeffPair; +inline ArithVar getArithVar(const VarCoeffPair& v) { return v.first; } +inline Rational& getCoefficient(VarCoeffPair& v) { return v.second; } +inline const Rational& getCoefficient(const VarCoeffPair& v) { return v.second; } + +inline bool cmp(const VarCoeffPair& a, const VarCoeffPair& b){ + return CVC4::theory::arith::getArithVar(a) < CVC4::theory::arith::getArithVar(b); +} + +/** + * RowVector is a sparse vector representation that represents the + * row as a strictly sorted array of "VarCoeffPair"s. + */ +class RowVector { +public: + typedef std::vector VarCoeffArray; + typedef VarCoeffArray::const_iterator NonZeroIterator; + + /** + * Let c be -1 if strictlySorted is true and c be 0 otherwise. + * isSorted(arr, strictlySorted) is then equivalent to + * If i= 2){ + NonZeroIterator curr = arr.begin(); + NonZeroIterator end = arr.end(); + ArithVar prev = getArithVar(*curr); + ++curr; + for(;curr != end; ++curr){ + ArithVar v = getArithVar(*curr); + if(strictlySorted && prev > v) return false; + if(!strictlySorted && prev >= v) return false; + prev = v; + } + } + return true; + } + + /** + * noZeroCoefficients(arr) is equivalent to + * 0 != getCoefficient(arr[i]) for all i. + */ + static bool noZeroCoefficients(const VarCoeffArray& arr){ + for(NonZeroIterator curr = arr.begin(), end = arr.end(); + curr != end; ++curr){ + const Rational& coeff = getCoefficient(*curr); + if(coeff == 0) return false; + } + return true; + } + + /** + * Zips together an array of variables and coefficients and appends + * it to the end of an output vector. + */ + static void zip(const std::vector< ArithVar >& variables, + const std::vector< Rational >& coefficients, + VarCoeffArray& output); + + static void merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c); + + +protected: + /** + * Invariants: + * - isSorted(d_entries, true) + * - noZeroCoefficients(d_entries) + */ + VarCoeffArray d_entries; + + NonZeroIterator lower_bound(ArithVar x_j) const{ + return std::lower_bound(d_entries.begin(), d_entries.end(), make_pair(x_j,0), cmp); + } + + typedef VarCoeffArray::iterator iterator; + +public: + + RowVector() : d_entries() {} + + RowVector(const std::vector< ArithVar >& variables, + const std::vector< Rational >& coefficients); + + + //Iterates over the nonzero entries in the Vector + NonZeroIterator beginNonZero() const { return d_entries.begin(); } + NonZeroIterator endNonZero() const { return d_entries.end(); } + + /** Returns true if the variable is in the row. */ + bool has(ArithVar x_j) const{ + NonZeroIterator lb = lower_bound(x_j); + return getArithVar(*lb) == x_j; + } + + /** + * Returns the coefficient of a variable in the row. + */ + const Rational& lookup(ArithVar x_j) const{ + Assert(has(x_j)); + NonZeroIterator lb = lower_bound(x_j); + return getCoefficient(*lb); + } + + /** Multiplies the coefficients of the RowVector by c (where c != 0). */ + void multiply(const Rational& c); + + /** + * \sum(this->entries) += c * (\sum(other.d_entries) ) + * + * Updates the current row to be the sum of itself and + * another vector times c (c != 0). + */ + void addRowTimesConstant(const Rational& c, const RowVector& other); + + void printRow(); +}; /* class RowVector */ + +/** + * A reduced row is similar to a normal row except + * that it also has a notion of a basic variable. + * This variable that must have a coefficient of -1 in the array. + */ +class ReducedRowVector : public RowVector{ +private: + ArithVar d_basic; + + bool wellFormed() const{ + return + isSorted(d_entries, true) && + noZeroCoefficients(d_entries) && + basicIsSet() && + has(basic()) && + lookup(basic()) == Rational(-1); + } + +public: + + bool basicIsSet() const { return d_basic != ARITHVAR_SENTINEL; } + + ReducedRowVector(ArithVar basic, + const std::vector< ArithVar >& variables, + const std::vector< Rational >& coefficients); + + + ArithVar basic() const{ + Assert(basicIsSet()); + return d_basic; + } + + void pivot(ArithVar x_j); + + void substitute(const ReducedRowVector& other); +}; /* class ReducedRowVector */ + + +}/* namespace CVC4::theory::arith */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ + +#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */ diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 2490ed51b..c22c21a46 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -24,85 +24,6 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; -Row::Row(ArithVar basic, - const std::vector< Rational >& coefficients, - const std::vector< ArithVar >& variables): - d_x_i(basic), - d_coeffs(){ - - Assert(coefficients.size() == variables.size() ); - - std::vector::const_iterator coeffIter = coefficients.begin(); - std::vector::const_iterator coeffEnd = coefficients.end(); - std::vector::const_iterator varIter = variables.begin(); - - for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){ - const Rational& coeff = *coeffIter; - ArithVar var_i = *varIter; - - Assert(var_i != d_x_i); - Assert(!has(var_i)); - Assert(coeff != Rational(0,1)); - - d_coeffs[var_i] = coeff; - Assert(d_coeffs[var_i] != Rational(0,1)); - } -} -void Row::substitute(Row& row_s){ - ArithVar x_s = row_s.basicVar(); - - Assert(has(x_s)); - Assert(x_s != d_x_i); - - Rational zero(0,1); - - Rational a_rs = lookup(x_s); - Assert(a_rs != zero); - d_coeffs.erase(x_s); - - for(iterator iter = row_s.begin(), iter_end = row_s.end(); - iter != iter_end; ++iter){ - ArithVar x_j = iter->first; - Rational a_sj = iter->second; - a_sj *= a_rs; - CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j); - - if(coeff_iter != d_coeffs.end()){ - coeff_iter->second += a_sj; - if(coeff_iter->second == zero){ - d_coeffs.erase(coeff_iter); - } - }else{ - d_coeffs.insert(std::make_pair(x_j,a_sj)); - } - } -} - -void Row::pivot(ArithVar x_j){ - Rational negInverseA_rs = -(lookup(x_j).inverse()); - d_coeffs[d_x_i] = Rational(Integer(-1)); - d_coeffs.erase(x_j); - - d_x_i = x_j; - - for(iterator nonbasicIter = begin(), nonbasicIter_end = end(); - nonbasicIter != nonbasicIter_end; ++nonbasicIter){ - nonbasicIter->second *= negInverseA_rs; - } - -} - -void Row::printRow(){ - Debug("tableau") << d_x_i << " "; - for(iterator nonbasicIter = d_coeffs.begin(); - nonbasicIter != d_coeffs.end(); - ++nonbasicIter){ - ArithVar nb = nonbasicIter->first; - Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}"; - } - Debug("tableau") << std::endl; -} - void Tableau::addRow(ArithVar basicVar, const std::vector& coeffs, const std::vector& variables){ @@ -113,15 +34,15 @@ void Tableau::addRow(ArithVar basicVar, //The new basic variable cannot already be a basic variable Assert(!isActiveBasicVariable(basicVar)); d_activeBasicVars.insert(basicVar); - Row* row_current = new Row(basicVar,coeffs,variables); + ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs); d_rowsTable[basicVar] = row_current; //A variable in the row may have been made non-basic already. //If this is the case we fake pivoting this variable - std::vector::const_iterator coeffsIter = coeffs.begin(); - std::vector::const_iterator coeffsEnd = coeffs.end(); + vector::const_iterator coeffsIter = coeffs.begin(); + vector::const_iterator coeffsEnd = coeffs.end(); - std::vector::const_iterator varsIter = variables.begin(); + vector::const_iterator varsIter = variables.begin(); for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){ ArithVar var = *varsIter; @@ -132,7 +53,7 @@ void Tableau::addRow(ArithVar basicVar, } Assert(isActiveBasicVariable(var)); - Row* row_var = lookup(var); + ReducedRowVector* row_var = lookup(var); row_current->substitute(*row_var); } } @@ -142,7 +63,7 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ Assert(d_basicManager.isMember(x_r)); Assert(!d_basicManager.isMember(x_s)); - Row* row_s = lookup(x_r); + ReducedRowVector* row_s = lookup(x_r); Assert(row_s->has(x_s)); //Swap x_r and x_s in d_activeRows @@ -160,7 +81,9 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ for(ArithVarSet::iterator basicIter = begin(), endIter = end(); basicIter != endIter; ++basicIter){ ArithVar basic = *basicIter; - Row* row_k = lookup(basic); + if(basic == x_s) continue; + + ReducedRowVector* row_k = lookup(basic); if(row_k->has(x_s)){ d_activityMonitor[basic] += 30; row_k->substitute(*row_s); @@ -173,7 +96,7 @@ void Tableau::printTableau(){ typedef RowsTable::iterator table_iter; for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end(); rowIter != end; ++rowIter){ - Row* row_k = *rowIter; + ReducedRowVector* row_k = *rowIter; if(row_k != NULL){ row_k->printRow(); } @@ -181,18 +104,19 @@ void Tableau::printTableau(){ } -void Tableau::updateRow(Row* row){ - for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){ +void Tableau::updateRow(ReducedRowVector* row){ + ArithVar basic = row->basic(); + for(ReducedRowVector::NonZeroIterator i=row->beginNonZero(), endIter = row->endNonZero(); i != endIter; ){ ArithVar var = i->first; ++i; - if(d_basicManager.isMember(var)){ - Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); + if(var != basic && d_basicManager.isMember(var)){ + ReducedRowVector* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); Assert(row_var != row); row->substitute(*row_var); - i = row->begin(); - endIter = row->end(); + i = row->beginNonZero(); + endIter = row->endNonZero(); } } } 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 -#include #include #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 > 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 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& coeffs, const std::vector& variables); + void addRow(ArithVar basicVar, + const std::vector& coeffs, + const std::vector& 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 */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index bd686737a..6efffa21c 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -104,28 +104,6 @@ TheoryArith::Statistics::~Statistics(){ } -bool isBasicSum(TNode n){ - if(n.getKind() != kind::PLUS) return false; - - for(TNode::const_iterator i=n.begin(); i!=n.end(); ++i){ - TNode child = *i; - if(child.getKind() != MULT) return false; - if(child[0].getKind() != CONST_RATIONAL) return false; - for(unsigned j=1; jhas(variable)){ return x_j; @@ -208,7 +186,7 @@ void TheoryArith::preRegisterTerm(TNode n) { //TODO is an atom if(isRelationOperator(k)){ - Assert(isNormalAtom(n)); + Assert(Comparison::isNormalAtom(n)); d_propagator.addAtom(n); @@ -331,10 +309,12 @@ DeltaRational TheoryArith::computeRowValue(ArithVar x, bool useSafe){ Assert(d_basicManager.isMember(x)); DeltaRational sum = d_constants.d_ZERO_DELTA; - Row* row = d_tableau.lookup(x); - for(Row::iterator i = row->begin(); i != row->end();++i){ - ArithVar nonbasic = i->first; - const Rational& coeff = i->second; + ReducedRowVector* row = d_tableau.lookup(x); + for(ReducedRowVector::NonZeroIterator i = row->beginNonZero(), end = row->endNonZero(); + i != end;++i){ + ArithVar nonbasic = getArithVar(*i); + if(nonbasic == row->basic()) continue; + const Rational& coeff = getCoefficient(*i); const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe); sum = sum + (assignment * coeff); @@ -484,7 +464,7 @@ void TheoryArith::update(ArithVar x_i, const DeltaRational& v){ basicIter != d_tableau.end(); ++basicIter){ ArithVar x_j = *basicIter; - Row* row_j = d_tableau.lookup(x_j); + ReducedRowVector* row_j = d_tableau.lookup(x_j); if(row_j->has(x_i)){ const Rational& a_ji = row_j->lookup(x_i); @@ -509,7 +489,7 @@ void TheoryArith::update(ArithVar x_i, const DeltaRational& v){ void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ Assert(x_i != x_j); - Row* row_i = d_tableau.lookup(x_i); + ReducedRowVector* row_i = d_tableau.lookup(x_i); const Rational& a_ij = row_i->lookup(x_j); @@ -528,7 +508,7 @@ void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ basicIter != d_tableau.end(); ++basicIter){ ArithVar x_k = *basicIter; - Row* row_k = d_tableau.lookup(x_k); + ReducedRowVector* row_k = d_tableau.lookup(x_k); if(x_k != x_i && row_k->has(x_j)){ const Rational& a_kj = row_k->lookup(x_j); @@ -585,10 +565,13 @@ ArithVar TheoryArith::selectSmallestInconsistentVar(){ template ArithVar TheoryArith::selectSlack(ArithVar x_i){ - Row* row_i = d_tableau.lookup(x_i); + ReducedRowVector* row_i = d_tableau.lookup(x_i); + + for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); + nbi != end; ++nbi){ + ArithVar nonbasic = getArithVar(*nbi); + if(nonbasic == x_i) continue; - for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){ - ArithVar nonbasic = nbi->first; const Rational& a_ij = nbi->second; int cmp = a_ij.cmp(d_constants.d_ZERO); if(above){ // beta(x_i) > u_i @@ -653,7 +636,7 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 Node TheoryArith::generateConflictAbove(ArithVar conflictVar){ - Row* row_i = d_tableau.lookup(conflictVar); + ReducedRowVector* row_i = d_tableau.lookup(conflictVar); NodeBuilder<> nb(kind::AND); TNode bound = d_partialModel.getUpperConstraint(conflictVar); @@ -665,8 +648,11 @@ Node TheoryArith::generateConflictAbove(ArithVar conflictVar){ nb << bound; - for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){ - ArithVar nonbasic = nbi->first; + for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); + nbi != end; ++nbi){ + ArithVar nonbasic = getArithVar(*nbi); + if(nonbasic == conflictVar) continue; + const Rational& a_ij = nbi->second; Assert(a_ij != d_constants.d_ZERO); @@ -690,7 +676,7 @@ Node TheoryArith::generateConflictAbove(ArithVar conflictVar){ } Node TheoryArith::generateConflictBelow(ArithVar conflictVar){ - Row* row_i = d_tableau.lookup(conflictVar); + ReducedRowVector* row_i = d_tableau.lookup(conflictVar); NodeBuilder<> nb(kind::AND); TNode bound = d_partialModel.getLowerConstraint(conflictVar); @@ -701,8 +687,10 @@ Node TheoryArith::generateConflictBelow(ArithVar conflictVar){ << " " << bound << endl; nb << bound; - for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){ - ArithVar nonbasic = nbi->first; + for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); nbi != end; ++nbi){ + ArithVar nonbasic = getArithVar(*nbi); + if(nonbasic != conflictVar) continue; + const Rational& a_ij = nbi->second; Assert(a_ij != d_constants.d_ZERO); @@ -867,13 +855,15 @@ void TheoryArith::checkTableau(){ for(ArithVarSet::iterator basicIter = d_tableau.begin(); basicIter != d_tableau.end(); ++basicIter){ ArithVar basic = *basicIter; - Row* row_k = d_tableau.lookup(basic); + ReducedRowVector* row_k = d_tableau.lookup(basic); DeltaRational sum; Debug("paranoid:check_tableau") << "starting row" << basic << endl; - for(Row::iterator nonbasicIter = row_k->begin(); - nonbasicIter != row_k->end(); + for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k->beginNonZero(); + nonbasicIter != row_k->endNonZero(); ++nonbasicIter){ ArithVar nonbasic = nonbasicIter->first; + if(basic == nonbasic) continue; + const Rational& coeff = nonbasicIter->second; DeltaRational beta = d_partialModel.getAssignment(nonbasic); Debug("paranoid:check_tableau") << nonbasic << beta << coeff<