Purify applications of exp to transcendental arguments (#2097)

2 files changed, 62 insertions, 43 deletions

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 8380014f3..30debf6d7 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -856,7 +856,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
   Trace("nl-ext-cm-debug") << "  apply pre-substitution..." << std::endl;
   std::vector<Node> pvars;
   std::vector<Node> psubs;
-  for (std::pair<const Node, Node>& tb : d_trig_base)
+  for (std::pair<const Node, Node>& tb : d_tr_base)
   {
     pvars.push_back(tb.first);
     psubs.push_back(tb.second);
@@ -1850,16 +1850,18 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   Trace("nl-ext-mv") << "Extended terms : " << std::endl;
   // register the extended function terms
   std::map< Node, Node > mvarg_to_term;
-  std::vector<Node> trig_no_base;
+  std::vector<Node> tr_no_base;
   bool needPi = false;
-  for( unsigned i=0; i<xts.size(); i++ ){
+  for (unsigned i = 0, xsize = xts.size(); i < xsize; i++)
+  {
     Node a = xts[i];
     computeModelValue(a, 0);
     computeModelValue(a, 1);
     printModelValue("nl-ext-mv", a);
     //Assert(d_mv[1][a].isConst());
     //Assert(d_mv[0][a].isConst());
-    if (a.getKind() == NONLINEAR_MULT)
+    Kind ak = a.getKind();
+    if (ak == NONLINEAR_MULT)
     {
       d_ms.push_back( a );
       
@@ -1892,20 +1894,27 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       }
       */
     }else if( a.getNumChildren()==1 ){
+      if (ak == SINE)
+      {
+        needPi = true;
+      }
       bool consider = true;
-      // get shifted version
-      if (a.getKind() == SINE)
+      // if is an unpurified application of SINE, or it is a transcendental
+      // applied to a trancendental, purify.
+      if (isTranscendentalKind(ak))
       {
-        if( d_trig_is_base.find( a )==d_trig_is_base.end() ){
+        if ((ak == SINE && d_tr_is_base.find(a) == d_tr_is_base.end())
+            || isTranscendentalKind(a[0].getKind()))
+        {
           consider = false;
-          trig_no_base.push_back(a);
-          needPi = true;
+          tr_no_base.push_back(a);
         }
       }
       if( consider ){
         Node r = d_containing.getValuation().getModel()->getRepresentative(a[0]);
-        std::map< Node, Node >::iterator itrm = d_tf_rep_map[a.getKind()].find( r );
-        if( itrm!=d_tf_rep_map[a.getKind()].end() ){
+        std::map<Node, Node>::iterator itrm = d_tf_rep_map[ak].find(r);
+        if (itrm != d_tf_rep_map[ak].end())
+        {
           //verify they have the same model value
           if( d_mv[1][a]!=d_mv[1][itrm->second] ){
             // if not, add congruence lemma
@@ -1915,14 +1924,14 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
             //Assert( false );
           }
         }else{
-          d_tf_rep_map[a.getKind()][r] = a;
+          d_tf_rep_map[ak][r] = a;
         }
       }
     }
-    else if (a.getKind() == PI)
+    else if (ak == PI)
     {
       needPi = true;
-      d_tf_rep_map[a.getKind()][a] = a;
+      d_tf_rep_map[ak][a] = a;
     }
     else
     {
@@ -1943,37 +1952,46 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   }
 
   // process SINE phase shifting
-  for (const Node& a : trig_no_base)
+  for (const Node& a : tr_no_base)
   {
-    if (d_trig_base.find(a) == d_trig_base.end())
+    if (d_tr_base.find(a) == d_tr_base.end())
     {
       Node y =
           nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
       Node new_a = nm->mkNode(a.getKind(), y);
-      d_trig_is_base[new_a] = true;
-      d_trig_base[a] = new_a;
-      Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a
-                         << std::endl;
-      Assert(!d_pi.isNull());
-      Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts");
-      // FIXME : do not introduce shift here, instead needs model-based
-      // refinement for constant shifts (#1284)
-      Node shift_lem = nm->mkNode(
-          AND,
-          mkValidPhase(y, d_pi),
-          nm->mkNode(
-              ITE,
-              mkValidPhase(a[0], d_pi),
-              a[0].eqNode(y),
-              a[0].eqNode(nm->mkNode(
-                  PLUS,
-                  y,
-                  nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi)))),
-          new_a.eqNode(a));
+      d_tr_is_base[new_a] = true;
+      d_tr_base[a] = new_a;
+      Node lem;
+      if (a.getKind() == SINE)
+      {
+        Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a
+                           << std::endl;
+        Assert(!d_pi.isNull());
+        Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts");
+        // FIXME : do not introduce shift here, instead needs model-based
+        // refinement for constant shifts (#1284)
+        lem = nm->mkNode(
+            AND,
+            mkValidPhase(y, d_pi),
+            nm->mkNode(
+                ITE,
+                mkValidPhase(a[0], d_pi),
+                a[0].eqNode(y),
+                a[0].eqNode(nm->mkNode(
+                    PLUS,
+                    y,
+                    nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi)))),
+            new_a.eqNode(a));
+      }
+      else
+      {
+        // do both equalities to ensure that new_a becomes a preregistered term
+        lem = nm->mkNode(AND, a.eqNode(new_a), a[0].eqNode(y));
+      }
       // must do preprocess on this one
       Trace("nl-ext-lemma")
-          << "NonlinearExtension::Lemma : shift : " << shift_lem << std::endl;
-      d_containing.getOutputChannel().lemma(shift_lem, false, true);
+          << "NonlinearExtension::Lemma : purify : " << lem << std::endl;
+      d_containing.getOutputChannel().lemma(lem, false, true);
       lemmas_proc++;
     }
   }
@@ -3764,8 +3782,8 @@ std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() {
               SINE, NodeManager::currentNM()->mkNode(MULT, d_neg_one, t[0]));
           symn = Rewriter::rewrite( symn );
           //can assume its basis since phase is split over 0
-          d_trig_is_base[symn] = true;
-          Assert( d_trig_is_base.find( t ) != d_trig_is_base.end() );
+          d_tr_is_base[symn] = true;
+          Assert(d_tr_is_base.find(t) != d_tr_is_base.end());
           std::vector< Node > children;
 
           lem = NodeManager::currentNM()->mkNode(
@@ -4169,9 +4187,10 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf,
     Node v_pab = r == 0 ? mvb.first : mvb.second;
     if (!v_pab.isNull())
     {
-      Assert(v_pab.isConst());
       Trace("nl-ext-tftp-debug2") << "...model value of " << pab << " is "
                                   << v_pab << std::endl;
+
+      Assert(v_pab.isConst());
       Node comp = nm->mkNode(r == 0 ? LT : GT, v, v_pab);
       Trace("nl-ext-tftp-debug2") << "...compare : " << comp << std::endl;
       Node compr = Rewriter::rewrite(comp);
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index d3698aa94..1e5ca9ad1 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -544,8 +544,8 @@ class NonlinearExtension {
   std::vector<Node> d_order_points;
   
   //transcendental functions
-  std::map<Node, Node> d_trig_base;
-  std::map<Node, bool> d_trig_is_base;
+  std::map<Node, Node> d_tr_base;
+  std::map<Node, bool> d_tr_is_base;
   std::map< Node, bool > d_tf_initial_refine;
   /** the list of lemmas we are waiting to flush until after check model */
   std::vector<Node> d_waiting_lemmas;