diff options
| -rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 54 | ||||
| -rw-r--r-- | src/theory/arith/nonlinear_extension.h | 5 |
2 files changed, 6 insertions, 53 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index b43f0d094..e81dcc881 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -1012,7 +1012,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, d_ms.clear(); d_mterms.clear(); d_m_nconst_factor.clear(); - d_tplane_refine_dir.clear(); + d_tplane_refine.clear(); d_ci.clear(); d_ci_exp.clear(); d_ci_max.clear(); @@ -2100,7 +2100,8 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() { for (unsigned k = kstart; k < d_mterms.size(); k++) { Node t = d_mterms[k]; // if this term requires a refinement - if (d_tplane_refine_dir.find(t) != d_tplane_refine_dir.end()) { + if (d_tplane_refine.find(t) != d_tplane_refine.end()) + { Trace("nl-ext-tplanes") << "Look at monomial requiring refinement : " << t << std::endl; // get a decomposition @@ -2284,54 +2285,7 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( // for a possible refinement if (options::nlExtTangentPlanes()) { if (is_false_lit) { - Node rhs_v = computeModelValue(rhs, 0); - Node x_v = computeModelValue(x, 0); - if( rhs_v.isConst() && x_v.isConst() ){ - bool needsRefine = false; - bool refineDir; - if (rhs_v == x_v) { - if (type == GT) - { - needsRefine = true; - refineDir = true; - } - else if (type == LT) - { - needsRefine = true; - refineDir = false; - } - } else if (x_v.getConst<Rational>() > rhs_v.getConst<Rational>()) { - if (type != GT && type != GEQ) - { - needsRefine = true; - refineDir = false; - } - } else { - if (type != LT && type != LEQ) - { - needsRefine = true; - refineDir = true; - } - } - Trace("nl-ext-tplanes-cons-debug") - << "...compute if bound corresponds to a required " - "refinement" - << std::endl; - Trace("nl-ext-tplanes-cons-debug") - << "...M[" << x << "] = " << x_v << ", M[" << rhs - << "] = " << rhs_v << std::endl; - Trace("nl-ext-tplanes-cons-debug") << "...refine = " << needsRefine - << "/" << refineDir << std::endl; - if (needsRefine) { - Trace("nl-ext-tplanes-cons") - << "---> By " << lit << " and since M[" << x << "] = " << x_v - << ", M[" << rhs << "] = " << rhs_v << ", "; - Trace("nl-ext-tplanes-cons") - << "monomial " << x << " should be " - << (refineDir ? "larger" : "smaller") << std::endl; - d_tplane_refine_dir[x][refineDir] = true; - } - } + d_tplane_refine.insert(x); } } } diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 1264a0fb8..c7e6b2b2a 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -487,9 +487,8 @@ private: //list of monomials with factors whose model value is non-constant in model // e.g. y*cos( x ) std::map<Node, bool> d_m_nconst_factor; - // If ( m, p1, true ), then it would help satisfiability if m were ( > - // if p1=true, < if p1=false ) - std::map<Node, std::map<bool, bool> > d_tplane_refine_dir; + /** the set of monomials we should apply tangent planes to */ + std::unordered_set<Node, NodeHashFunction> d_tplane_refine; // term -> coeff -> rhs -> ( status, exp, b ), // where we have that : exp => ( coeff * term <status> rhs ) // b is true if degree( term ) >= degree( rhs ) |