From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 10 Aug 2017 11:08:46 +0000 (-0500)
Subject: Maintain frontier for tangent planes.
X-Git-Tag: cvc5-1.0.0~5683
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4b5460a79838e93f8d417462c930806a77c09d31;p=cvc5.git

Maintain frontier for tangent planes.
---

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 42f9636dc..3c3301db1 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -2034,28 +2034,60 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() {
               dproc[a][b] = true;
               Trace("nl-ext-tplanes")
                   << "  decomposable into : " << a << " * " << b << std::endl;
-              Node a_v = computeModelValue(a, 1);
-              Node b_v = computeModelValue(b, 1);
-              // tangent plane
-              Node tplane = NodeManager::currentNM()->mkNode(
-                  kind::MINUS,
-                  NodeManager::currentNM()->mkNode(
-                      kind::PLUS,
-                      NodeManager::currentNM()->mkNode(kind::MULT, b_v, a),
-                      NodeManager::currentNM()->mkNode(kind::MULT, a_v, b)),
-                  NodeManager::currentNM()->mkNode(kind::MULT, a_v, b_v));
-              for (unsigned d = 0; d < 4; d++) {
-                Node aa = NodeManager::currentNM()->mkNode(
-                    d == 0 || d == 3 ? kind::GEQ : kind::LEQ, a, a_v);
-                Node ab = NodeManager::currentNM()->mkNode(
-                    d == 1 || d == 3 ? kind::GEQ : kind::LEQ, b, b_v);
-                Node conc = NodeManager::currentNM()->mkNode(
-                    d <= 1 ? kind::LEQ : kind::GEQ, t, tplane);
-                Node tlem = NodeManager::currentNM()->mkNode(
-                    kind::OR, aa.negate(), ab.negate(), conc);
-                Trace("nl-ext-tplanes")
-                    << "Tangent plane lemma : " << tlem << std::endl;
-                lemmas.push_back(tlem);
+              Node a_v_c = computeModelValue(a, 1);
+              Node b_v_c = computeModelValue(b, 1);
+              // points we will add tangent planes for
+              std::vector< Node > pts[2];
+              pts[0].push_back( a_v_c );
+              pts[1].push_back( b_v_c );
+              // if previously refined
+              bool prevRefine = d_tangent_val_bound[0][a].find( b )!=d_tangent_val_bound[0][a].end();
+              // a_min, a_max, b_min, b_max
+              for( unsigned p=0; p<4; p++ ){
+                Node curr_v = p<=1 ? a_v_c : b_v_c;
+                if( prevRefine ){
+                  Node pt_v = d_tangent_val_bound[p][a][b];
+                  Assert( !pt_v.isNull() );
+                  if( curr_v!=pt_v ){
+                    Node do_extend = NodeManager::currentNM()->mkNode( ( p==1 || p==3 ) ? GT : LT, curr_v, pt_v );
+                    do_extend = Rewriter::rewrite( do_extend );
+                    if( do_extend==d_true ){
+                      for( unsigned q=0; q<2; q++ ){
+                        pts[ p<=1 ? 0 : 1 ].push_back( curr_v );
+                        pts[ p<=1 ? 1 : 0 ].push_back( d_tangent_val_bound[ p<=1 ? 2+q : q ][a][b] );
+                      }
+                    }
+                  }
+                }else{
+                  d_tangent_val_bound[p][a][b] = curr_v;
+                }
+              }
+              
+              for( unsigned p=0; p<pts[0].size(); p++ ){
+                Node a_v = pts[0][p];
+                Node b_v = pts[1][p];
+              
+                // tangent plane
+                Node tplane = NodeManager::currentNM()->mkNode(
+                    kind::MINUS,
+                    NodeManager::currentNM()->mkNode(
+                        kind::PLUS,
+                        NodeManager::currentNM()->mkNode(kind::MULT, b_v, a),
+                        NodeManager::currentNM()->mkNode(kind::MULT, a_v, b)),
+                    NodeManager::currentNM()->mkNode(kind::MULT, a_v, b_v));
+                for (unsigned d = 0; d < 4; d++) {
+                  Node aa = NodeManager::currentNM()->mkNode(
+                      d == 0 || d == 3 ? kind::GEQ : kind::LEQ, a, a_v);
+                  Node ab = NodeManager::currentNM()->mkNode(
+                      d == 1 || d == 3 ? kind::GEQ : kind::LEQ, b, b_v);
+                  Node conc = NodeManager::currentNM()->mkNode(
+                      d <= 1 ? kind::LEQ : kind::GEQ, t, tplane);
+                  Node tlem = NodeManager::currentNM()->mkNode(
+                      kind::OR, aa.negate(), ab.negate(), conc);
+                  Trace("nl-ext-tplanes")
+                      << "Tangent plane lemma : " << tlem << std::endl;
+                  lemmas.push_back(tlem);
+                }
               }
             }
           }
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 1a19eb67a..e8cfae1d7 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -243,6 +243,9 @@ private:
   std::map< Node, Node > d_factor_skolem;
   Node getFactorSkolem( Node n, std::vector< Node >& lemmas );
   
+  // tangent plane bounds
+  std::map< Node, std::map< Node, Node > > d_tangent_val_bound[4];
+  
   Node getTaylor( Node tf, Node x, unsigned n, std::vector< Node >& lemmas );
 private:
   // Returns a vector containing a split on whether each term is 0 or not for