diff options
Diffstat (limited to 'src/theory/arith/nl_model.cpp')
| -rw-r--r-- | src/theory/arith/nl_model.cpp | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index 3c1d5f1e9..d09a138fe 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -45,9 +45,9 @@ void NlModel::reset(TheoryModel* m, std::map<Node, Node>& arithModel) d_arithVal.clear(); // process arithModel std::map<Node, Node>::iterator it; - for (const std::pair<const Node, Node>& m : arithModel) + for (const std::pair<const Node, Node>& m2 : arithModel) { - d_arithVal[m.first] = m.second; + d_arithVal[m2.first] = m2.second; } } @@ -700,14 +700,14 @@ bool NlModel::solveEqualitySimple(Node eq, Assert(m_var.isConst()); for (unsigned r = 0; r < 2; r++) { - for (unsigned b = 0; b < 2; b++) + for (unsigned b2 = 0; b2 < 2; b2++) { - Node val = b == 0 ? l : u; + Node val = b2 == 0 ? l : u; // (-b +- approx_sqrt( b^2 - 4ac ))/2a Node approx = nm->mkNode( MULT, coeffa, nm->mkNode(r == 0 ? MINUS : PLUS, negb, val)); approx = Rewriter::rewrite(approx); - bounds[r][b] = approx; + bounds[r][b2] = approx; Assert(approx.isConst()); } if (bounds[r][0].getConst<Rational>() > bounds[r][1].getConst<Rational>()) @@ -776,13 +776,13 @@ bool NlModel::simpleCheckModelLit(Node lit) // x = a is ( x >= a ^ x <= a ) for (unsigned i = 0; i < 2; i++) { - Node lit = nm->mkNode(GEQ, atom[i], atom[1 - i]); + Node lit2 = nm->mkNode(GEQ, atom[i], atom[1 - i]); if (!pol) { - lit = lit.negate(); + lit2 = lit2.negate(); } - lit = Rewriter::rewrite(lit); - bool success = simpleCheckModelLit(lit); + lit2 = Rewriter::rewrite(lit2); + bool success = simpleCheckModelLit(lit2); if (success != pol) { // false != true -> one conjunct of equality is false, we fail @@ -1167,7 +1167,7 @@ bool NlModel::simpleCheckModelMsum(const std::map<Node, Node>& msum, bool pol) } // must over/under approximate based on vc_set_lower, computed above Node vb = vc_set_lower ? l : u; - for (unsigned i = 0; i < vcfact; i++) + for (unsigned i2 = 0; i2 < vcfact; i2++) { vbs.push_back(vb); } @@ -1317,7 +1317,7 @@ void NlModel::getModelValueRepair( Node v = cb.first; if (l != u) { - Node pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); + pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); Trace("nl-model") << v << " approximated as " << pred << std::endl; Node witness; if (options::modelWitnessChoice()) |