arithvar_dense_set.h \
tableau.h \
tableau.cpp \
+ row_vector.h \
+ row_vector.cpp \
arith_propagator.h \
arith_propagator.cpp \
theory_arith.h \
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 */
--- /dev/null
+
+#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<Rational>::const_iterator coeffIter = coefficients.begin();
+ vector<Rational>::const_iterator coeffEnd = coefficients.end();
+ vector<ArithVar>::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<ArithVar>& variables,
+ const vector<Rational>& 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());
+}
--- /dev/null
+
+
+#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 <vector>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+typedef std::pair<ArithVar, Rational> 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<VarCoeffPair> 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<j, cmp(getArithVar(d_entries[i]), getArithVar(d_entries[j])) <= c.
+ */
+ static bool isSorted(const VarCoeffArray& arr, bool strictlySorted) {
+ if(arr.size() >= 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 */
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<Rational>::const_iterator coeffIter = coefficients.begin();
- std::vector<Rational>::const_iterator coeffEnd = coefficients.end();
- std::vector<ArithVar>::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<Rational>& coeffs,
const std::vector<ArithVar>& variables){
//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<Rational>::const_iterator coeffsIter = coeffs.begin();
- std::vector<Rational>::const_iterator coeffsEnd = coeffs.end();
+ vector<Rational>::const_iterator coeffsIter = coeffs.begin();
+ vector<Rational>::const_iterator coeffsEnd = coeffs.end();
-
std::vector<ArithVar>::const_iterator varsIter = variables.begin();
+ vector<ArithVar>::const_iterator varsIter = variables.begin();
for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){
ArithVar var = *varsIter;
}
Assert(isActiveBasicVariable(var));
- Row* row_var = lookup(var);
+ ReducedRowVector* row_var = lookup(var);
row_current->substitute(*row_var);
}
}
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
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);
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();
}
}
-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();
}
}
}
#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
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;
class Tableau {
private:
- typedef std::vector< Row* > RowsTable;
+ typedef std::vector< ReducedRowVector* > RowsTable;
ArithVarSet d_activeBasicVars;
RowsTable d_rowsTable;
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:
Assert(d_basicManager.isMember(basic));
Assert(isEjected(basic));
- Row* row = lookupEjected(basic);
+ ReducedRowVector* row = lookupEjected(basic);
d_activeBasicVars.insert(basic);
updateRow(row);
}
return d_activeBasicVars.inSet(var);
}
- void updateRow(Row* row);
+ void updateRow(ReducedRowVector* row);
};
}; /* namespace arith */
}
-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; j<child.getNumChildren(); ++j){
- TNode var = child[j];
- if(var.getMetaKind() != metakind::VARIABLE) return false;
- }
- }
- return true;
-}
-
-bool isNormalAtom(TNode n){
-
- Comparison parse = Comparison::parseNormalForm(n);
-
- return parse.isNormalForm();
-}
-
bool TheoryArith::shouldEject(ArithVar var){
if(d_partialModel.hasEitherBound(var)){
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(variable)){
return x_j;
//TODO is an atom
if(isRelationOperator(k)){
- Assert(isNormalAtom(n));
+ Assert(Comparison::isNormalAtom(n));
d_propagator.addAtom(n);
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);
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);
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);
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);
template <bool above>
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
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);
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);
}
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);
<< " " << 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);
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<<endl;
projects / cvc5.git / commitdiff