diff options
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 21a86c345..ab8884228 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -290,8 +290,8 @@ DeltaRational TheoryArith::computeRowValueUsingAssignment(TNode x){ Row* row = d_tableau.lookup(x); for(Row::iterator i = row->begin(); i != row->end();++i){ - TNode nonbasic = *i; - const Rational& coeff = row->lookup(nonbasic); + TNode nonbasic = i->first; + const Rational& coeff = i->second; const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic); sum = sum + (assignment * coeff); } @@ -307,8 +307,8 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){ Row* row = d_tableau.lookup(x); for(Row::iterator i = row->begin(); i != row->end();++i){ - TNode nonbasic = *i; - const Rational& coeff = row->lookup(nonbasic); + TNode nonbasic = i->first; + const Rational& coeff = i->second; const DeltaRational& assignment = d_partialModel.getSafeAssignment(nonbasic); sum = sum + (assignment * coeff); } @@ -604,8 +604,8 @@ TNode TheoryArith::selectSlack(TNode x_i){ Row* row_i = d_tableau.lookup(x_i); for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){ - TNode nonbasic = *nbi; - const Rational& a_ij = row_i->lookup(nonbasic); + TNode 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 if( cmp < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){ @@ -681,8 +681,8 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){ nb << bound; for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){ - TNode nonbasic = *nbi; - const Rational& a_ij = row_i->lookup(nonbasic); + TNode nonbasic = nbi->first; + const Rational& a_ij = nbi->second; Assert(a_ij != d_constants.d_ZERO); @@ -717,8 +717,8 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){ nb << bound; for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){ - TNode nonbasic = *nbi; - const Rational& a_ij = row_i->lookup(nonbasic); + TNode nonbasic = nbi->first; + const Rational& a_ij = nbi->second; Assert(a_ij != d_constants.d_ZERO); @@ -890,8 +890,8 @@ void TheoryArith::checkTableau(){ for(Row::iterator nonbasicIter = row_k->begin(); nonbasicIter != row_k->end(); ++nonbasicIter){ - TNode nonbasic = *nonbasicIter; - const Rational& coeff = row_k->lookup(nonbasic); + TNode nonbasic = nonbasicIter->first; + const Rational& coeff = nonbasicIter->second; DeltaRational beta = d_partialModel.getAssignment(nonbasic); Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl; sum = sum + (beta*coeff); |