Simplify storing of transcendental function applications that occur in assertions (#2458)

1 files changed, 107 insertions, 53 deletions

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index f4e9f9d6b..9f6608dc5 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -883,13 +883,12 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
   // get model bounds for all transcendental functions
   Trace("nl-ext-cm-debug") << "  get bounds for transcendental functions..."
                            << std::endl;
-  for (std::pair<const Kind, std::map<Node, Node> >& tfs : d_tf_rep_map)
+  for (std::pair<const Kind, std::vector<Node> >& tfs : d_f_map)
   {
     Kind k = tfs.first;
-    for (std::pair<const Node, Node>& tfr : tfs.second)
+    for (const Node& tf : tfs.second)
     {
-      // Figure 3 : tf( x )
-      Node tf = tfr.second;
+      // tf is Figure 3 : tf( x )
       Node atf = computeModelValue(tf, 0);
       if (k == PI)
       {
@@ -1827,6 +1826,33 @@ std::vector<Node> NonlinearExtension::checkSplitZero() {
   return lemmas;
 }
 
+/** An argument trie, for computing congruent terms */
+class ArgTrie
+{
+ public:
+  /** children of this node */
+  std::map<Node, ArgTrie> d_children;
+  /** the data of this node */
+  Node d_data;
+  /**
+   * Set d as the data on the node whose path is [args], return either d if
+   * that node has no data, or the data that already occurs there.
+   */
+  Node add(Node d, const std::vector<Node>& args)
+  {
+    ArgTrie* at = this;
+    for (const Node& a : args)
+    {
+      at = &(at->d_children[a]);
+    }
+    if (at->d_data.isNull())
+    {
+      at->d_data = d;
+    }
+    return at->d_data;
+  }
+};
+
 int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
                                       const std::vector<Node>& false_asserts,
                                       const std::vector<Node>& xts)
@@ -1840,7 +1866,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   d_ci.clear();
   d_ci_exp.clear();
   d_ci_max.clear();
-  d_tf_rep_map.clear();
+  d_f_map.clear();
   d_tf_region.clear();
   d_waiting_lemmas.clear();
 
@@ -1853,6 +1879,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   std::map< Node, Node > mvarg_to_term;
   std::vector<Node> tr_no_base;
   bool needPi = false;
+  // for computing congruence
+  std::map<Kind, ArgTrie> argTrie;
   for (unsigned i = 0, xsize = xts.size(); i < xsize; i++)
   {
     Node a = xts[i];
@@ -1894,7 +1922,9 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
         }
       }
       */
-    }else if( a.getNumChildren()==1 ){
+    }
+    else if (a.getNumChildren() > 0)
+    {
       if (ak == SINE)
       {
         needPi = true;
@@ -1904,35 +1934,61 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       // applied to a trancendental, purify.
       if (isTranscendentalKind(ak))
       {
-        if ((ak == SINE && d_tr_is_base.find(a) == d_tr_is_base.end())
-            || isTranscendentalKind(a[0].getKind()))
+        if (ak == SINE && d_tr_is_base.find(a) == d_tr_is_base.end())
         {
           consider = false;
+        }
+        else
+        {
+          for (const Node& ac : a)
+          {
+            if (isTranscendentalKind(ac.getKind()))
+            {
+              consider = false;
+              break;
+            }
+          }
+        }
+        if (!consider)
+        {
           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[ak].find(r);
-        if (itrm != d_tf_rep_map[ak].end())
+        std::vector<Node> repList;
+        for (const Node& ac : a)
+        {
+          Node r =
+              d_containing.getValuation().getModel()->getRepresentative(a[0]);
+          repList.push_back(r);
+        }
+        Node aa = argTrie[ak].add(a, repList);
+        if (aa != a)
         {
-          //verify they have the same model value
-          if( d_mv[1][a]!=d_mv[1][itrm->second] ){
-            // if not, add congruence lemma
-            Node cong_lemma = nm->mkNode(
-                IMPLIES, a[0].eqNode(itrm->second[0]), a.eqNode(itrm->second));
+          // apply congruence to pairs of terms that are disequal and congruent
+          Assert(aa.getNumChildren() == a.getNumChildren());
+          if (d_mv[1][a] != d_mv[1][aa])
+          {
+            std::vector<Node> exp;
+            for (unsigned j = 0, size = a.getNumChildren(); j < size; j++)
+            {
+              exp.push_back(a[j].eqNode(aa[j]));
+            }
+            Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
+            Node cong_lemma = nm->mkNode(OR, expn.negate(), a.eqNode(aa));
             lemmas.push_back( cong_lemma );
-            //Assert( false );
           }
-        }else{
-          d_tf_rep_map[ak][r] = a;
+        }
+        else
+        {
+          d_f_map[ak].push_back(a);
         }
       }
     }
     else if (ak == PI)
     {
       needPi = true;
-      d_tf_rep_map[ak][a] = a;
+      d_f_map[ak].push_back(a);
     }
     else
     {
@@ -2025,19 +2081,14 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   {
     Trace("nl-ext-mv") << "Arguments of trancendental functions : "
                        << std::endl;
-    for (std::map<Kind, std::map<Node, Node> >::iterator it =
-             d_tf_rep_map.begin();
-         it != d_tf_rep_map.end();
-         ++it)
+    for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
     {
-      Kind k = it->first;
+      Kind k = tfl.first;
       if (k == SINE || k == EXPONENTIAL)
       {
-        for (std::map<Node, Node>::iterator itt = it->second.begin();
-             itt != it->second.end();
-             ++itt)
+        for (const Node& tf : tfl.second)
         {
-          Node v = itt->second[0];
+          Node v = tf[0];
           computeModelValue(v, 0);
           computeModelValue(v, 1);
           printModelValue("nl-ext-mv", v);
@@ -3769,15 +3820,17 @@ std::vector<Node> NonlinearExtension::checkMonomialInferResBounds() {
 std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() {
   std::vector< Node > lemmas;
   Trace("nl-ext") << "Get initial refinement lemmas for transcendental functions..." << std::endl;
-  for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){
-    for( std::map< Node, Node >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
-      Node t = itt->second;
+  for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+  {
+    Kind k = tfl.first;
+    for (const Node& t : tfl.second)
+    {
       Assert( d_mv[1].find( t )!=d_mv[1].end() );
       //initial refinements
       if( d_tf_initial_refine.find( t )==d_tf_initial_refine.end() ){
         d_tf_initial_refine[t] = true;
         Node lem;
-        if (it->first == SINE)
+        if (k == SINE)
         {
           Node symn = NodeManager::currentNM()->mkNode(
               SINE, NodeManager::currentNM()->mkNode(MULT, d_neg_one, t[0]));
@@ -3839,7 +3892,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() {
                           NodeManager::currentNM()->mkNode(
                               MINUS, d_pi_neg, t[0])))));
         }
-        else if (it->first == EXPONENTIAL)
+        else if (k == EXPONENTIAL)
         {
           // ( exp(x) > 0 ) ^ ( x=0 <=> exp( x ) = 1 ) ^ ( x < 0 <=> exp( x ) <
           // 1 ) ^ ( x <= 0 V exp( x ) > x + 1 )
@@ -3877,23 +3930,22 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
   //sort arguments of all transcendentals
   std::map< Kind, std::vector< Node > > sorted_tf_args;
   std::map< Kind, std::map< Node, Node > > tf_arg_to_term;
-  
-  for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){
-    Kind k = it->first;
+
+  for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+  {
+    Kind k = tfl.first;
     if (k == EXPONENTIAL || k == SINE)
     {
-      for (std::map<Node, Node>::iterator itt = it->second.begin();
-           itt != it->second.end();
-           ++itt)
+      for (const Node& tf : tfl.second)
       {
-        Node a = itt->second[0];
+        Node a = tf[0];
         computeModelValue(a, 1);
         Assert(d_mv[1].find(a) != d_mv[1].end());
         if (d_mv[1][a].isConst())
         {
           Trace("nl-ext-tf-mono-debug") << "...tf term : " << a << std::endl;
           sorted_tf_args[k].push_back(a);
-          tf_arg_to_term[k][a] = itt->second;
+          tf_arg_to_term[k][a] = tf;
         }
       }
     }
@@ -3904,12 +3956,14 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
   //sort by concrete values
   smv.d_order_type = 0;
   smv.d_reverse_order = true;
-  for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){
-    Kind k = it->first;
+  for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+  {
+    Kind k = tfl.first;
     if( !sorted_tf_args[k].empty() ){
       std::sort( sorted_tf_args[k].begin(), sorted_tf_args[k].end(), smv );
       Trace("nl-ext-tf-mono") << "Sorted transcendental function list for " << k << " : " << std::endl;
-      for( unsigned i=0; i<sorted_tf_args[it->first].size(); i++ ){
+      for (unsigned i = 0; i < sorted_tf_args[k].size(); i++)
+      {
         Node targ = sorted_tf_args[k][i];
         Assert( d_mv[1].find( targ )!=d_mv[1].end() );
         Trace("nl-ext-tf-mono") << "  " << targ << " -> " << d_mv[1][targ] << std::endl;
@@ -3919,7 +3973,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
       }
       std::vector< Node > mpoints;
       std::vector< Node > mpoints_vals;
-      if (it->first == SINE)
+      if (k == SINE)
       {
         mpoints.push_back( d_pi );
         mpoints.push_back( d_pi_2 );
@@ -3927,7 +3981,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
         mpoints.push_back( d_pi_neg_2 );
         mpoints.push_back( d_pi_neg );
       }
-      else if (it->first == EXPONENTIAL)
+      else if (k == EXPONENTIAL)
       {
         mpoints.push_back( Node::null() );
       }
@@ -3946,7 +4000,8 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
         int monotonic_dir = -1;
         Node mono_bounds[2];
         Node targ, targval, t, tval;
-        for( unsigned i=0; i<sorted_tf_args[it->first].size(); i++ ){
+        for (unsigned i = 0, size = sorted_tf_args[k].size(); i < size; i++)
+        {
           Node sarg = sorted_tf_args[k][i];
           Assert( d_mv[1].find( sarg )!=d_mv[1].end() );
           Node sargval = d_mv[1][sarg];
@@ -3975,7 +4030,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
               tval = Node::null();
               mono_bounds[1] = mpoints[mdir_index];
               mdir_index++;
-              monotonic_dir = regionToMonotonicityDir(it->first, mdir_index);
+              monotonic_dir = regionToMonotonicityDir(k, mdir_index);
               if (mdir_index < mpoints.size())
               {
                 mono_bounds[0] = mpoints[mdir_index];
@@ -4038,7 +4093,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes()
                   << std::endl;
   // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions
   // via Incremental Linearization" by Cimatti et al
-  for (std::pair<const Kind, std::map<Node, Node> >& tfs : d_tf_rep_map)
+  for (std::pair<const Kind, std::vector<Node> >& tfs : d_f_map)
   {
     Kind k = tfs.first;
     if (k == PI)
@@ -4060,10 +4115,9 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes()
 
     // we substitute into the Taylor sum P_{n,f(0)}( x )
 
-    for (std::pair<const Node, Node>& tfr : tfs.second)
+    for (const Node& tf : tfs.second)
     {
-      // Figure 3 : tf( x )
-      Node tf = tfr.second;
+      // tf is Figure 3 : tf( x )
       if (isRefineableTfFun(tf))
       {
         Trace("nl-ext-tftp") << "Compute tangent planes " << tf << std::endl;