Remove spurious map (#2750)

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 0b378875c2838293939769e8a6e21fd6f1a1bc7d..c9db6273584176ac4c9f740a7c6bde818e76daf0 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -1323,7 +1323,6 @@ Node SygusUnifIo::constructSol(
       Trace("sygus-sui-dt")
           << "...try STRATEGY " << strat << "..." << std::endl;
 
-      std::map<unsigned, Node> look_ahead_solved_children;
       std::vector<Node> dt_children_cons;
       bool success = true;
 
@@ -1338,108 +1337,95 @@ Node SygusUnifIo::constructSol(
         Trace("sygus-sui-dt")
             << "construct PBE child #" << sc << "..." << std::endl;
         Node rec_c;
-        std::map<unsigned, Node>::iterator itla =
-            look_ahead_solved_children.find(sc);
-        if (itla != look_ahead_solved_children.end())
+
+        std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc];
+
+        // update the context
+        std::vector<Node> prev;
+        if (strat == strat_ITE && sc > 0)
         {
-          rec_c = itla->second;
-          indent("sygus-sui-dt-debug", ind + 1);
-          Trace("sygus-sui-dt-debug")
-              << "ConstructPBE: look ahead solved : "
-              << d_tds->sygusToBuiltin(rec_c) << std::endl;
+          EnumCache& ecache_cond = d_ecache[split_cond_enum];
+          Assert(set_split_cond_res_index);
+          Assert(split_cond_res_index < ecache_cond.d_enum_vals_res.size());
+          prev = x.d_vals;
+          x.updateContext(this,
+                          ecache_cond.d_enum_vals_res[split_cond_res_index],
+                          sc == 1);
+          // return value of above call may be false in corner cases where we
+          // must choose a non-separating condition to traverse to another
+          // strategy node
         }
-        else
-        {
-          std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc];
 
-          // update the context
-          std::vector<Node> prev;
-          if (strat == strat_ITE && sc > 0)
-          {
-            EnumCache& ecache_cond = d_ecache[split_cond_enum];
-            Assert(set_split_cond_res_index);
-            Assert(split_cond_res_index < ecache_cond.d_enum_vals_res.size());
-            prev = x.d_vals;
-            x.updateContext(this,
-                            ecache_cond.d_enum_vals_res[split_cond_res_index],
-                            sc == 1);
-            // return value of above call may be false in corner cases where we
-            // must choose a non-separating condition to traverse to another
-            // strategy node
-          }
-
-          // recurse
-          if (strat == strat_ITE && sc == 0)
-          {
-            Node ce = cenum.first;
+        // recurse
+        if (strat == strat_ITE && sc == 0)
+        {
+          Node ce = cenum.first;
 
-            EnumCache& ecache_child = d_ecache[ce];
+          EnumCache& ecache_child = d_ecache[ce];
 
-            // get the conditionals in the current context : they must be
-            // distinguishable
-            std::map<int, std::vector<Node> > possible_cond;
-            std::map<Node, int> solved_cond;  // stores branch
-            ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
+          // get the conditionals in the current context : they must be
+          // distinguishable
+          std::map<int, std::vector<Node> > possible_cond;
+          std::map<Node, int> solved_cond;  // stores branch
+          ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
 
-            std::map<int, std::vector<Node>>::iterator itpc =
-                possible_cond.find(0);
-            if (itpc != possible_cond.end())
+          std::map<int, std::vector<Node>>::iterator itpc =
+              possible_cond.find(0);
+          if (itpc != possible_cond.end())
+          {
+            if (Trace.isOn("sygus-sui-dt-debug"))
             {
-              if (Trace.isOn("sygus-sui-dt-debug"))
+              indent("sygus-sui-dt-debug", ind + 1);
+              Trace("sygus-sui-dt-debug")
+                  << "PBE : We have " << itpc->second.size()
+                  << " distinguishable conditionals:" << std::endl;
+              for (Node& cond : itpc->second)
               {
-                indent("sygus-sui-dt-debug", ind + 1);
+                indent("sygus-sui-dt-debug", ind + 2);
                 Trace("sygus-sui-dt-debug")
-                    << "PBE : We have " << itpc->second.size()
-                    << " distinguishable conditionals:" << std::endl;
-                for (Node& cond : itpc->second)
-                {
-                  indent("sygus-sui-dt-debug", ind + 2);
-                  Trace("sygus-sui-dt-debug")
-                      << d_tds->sygusToBuiltin(cond) << std::endl;
-                }
-              }
-              if (rec_c.isNull())
-              {
-                rec_c = constructBestConditional(ce, itpc->second);
-                Assert(!rec_c.isNull());
-                indent("sygus-sui-dt", ind);
-                Trace("sygus-sui-dt")
-                    << "PBE: ITE strategy : choose best conditional "
-                    << d_tds->sygusToBuiltin(rec_c) << std::endl;
+                    << d_tds->sygusToBuiltin(cond) << std::endl;
               }
             }
-            else
+            if (rec_c.isNull())
             {
-              // TODO (#1250) : degenerate case where children have different
-              // types?
+              rec_c = constructBestConditional(ce, itpc->second);
+              Assert(!rec_c.isNull());
               indent("sygus-sui-dt", ind);
-              Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, "
-                                       "cannot find a distinguishable condition"
-                                    << std::endl;
-            }
-            if (!rec_c.isNull())
-            {
-              Assert(ecache_child.d_enum_val_to_index.find(rec_c)
-                     != ecache_child.d_enum_val_to_index.end());
-              split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
-              set_split_cond_res_index = true;
-              split_cond_enum = ce;
-              Assert(split_cond_res_index
-                     < ecache_child.d_enum_vals_res.size());
+              Trace("sygus-sui-dt")
+                  << "PBE: ITE strategy : choose best conditional "
+                  << d_tds->sygusToBuiltin(rec_c) << std::endl;
             }
           }
           else
           {
-            did_recurse = true;
-            rec_c = constructSol(f, cenum.first, cenum.second, ind + 2, lemmas);
+            // TODO (#1250) : degenerate case where children have different
+            // types?
+            indent("sygus-sui-dt", ind);
+            Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, "
+                                      "cannot find a distinguishable condition"
+                                  << std::endl;
           }
-
-          // undo update the context
-          if (strat == strat_ITE && sc > 0)
+          if (!rec_c.isNull())
           {
-            x.d_vals = prev;
+            Assert(ecache_child.d_enum_val_to_index.find(rec_c)
+                    != ecache_child.d_enum_val_to_index.end());
+            split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
+            set_split_cond_res_index = true;
+            split_cond_enum = ce;
+            Assert(split_cond_res_index
+                    < ecache_child.d_enum_vals_res.size());
           }
         }
+        else
+        {
+          did_recurse = true;
+          rec_c = constructSol(f, cenum.first, cenum.second, ind + 2, lemmas);
+        }
+        // undo update the context
+        if (strat == strat_ITE && sc > 0)
+        {
+          x.d_vals = prev;
+        }
         if (!rec_c.isNull())
         {
           dt_children_cons.push_back(rec_c);