Simplify tangent plane direction (#1824)

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index b43f0d094850d9d31bddaa2089a3091f8935b5d7..e81dcc8811f3de8e0251d2b275df86e30424db95 100644 (file)
--- 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 1264a0fb87a0f751eaa3ecc7192079edb87e2e5f..c7e6b2b2af6147f79a3bb04b5712e6ee64600b46 100644 (file)
--- 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 )