Fix unif trace (#2550)

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 9706e3732bf75540f43c73c8652e93c21eb0cf39..ad45fb9b770f313939be1acb2729b6537b2487b7 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -215,21 +215,9 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
     Trace("cegis") << "  Enumerators :\n";
     for (unsigned i = 0, size = enums.size(); i < size; ++i)
     {
-      bool isUnit = false;
-      for (const Node& hd_unit : d_rl_eval_hds)
-      {
-        if (enums[i] == hd_unit[0])
-        {
-          isUnit = true;
-          break;
-        }
-      }
-      Trace("cegis") << "    " << enums[i]
-                     << (options::sygusUnif() && isUnit ? "*" : "") << " -> ";
-      std::stringstream ss;
-      Printer::getPrinter(options::outputLanguage())
-          ->toStreamSygus(ss, enum_values[i]);
-      Trace("cegis") << ss.str() << std::endl;
+      Trace("cegis") << "    " << enums[i] << " -> ";
+      TermDbSygus::toStreamSygus("cegis", enum_values[i]);
+      Trace("cegis") << "\n";
     }
   }
   // if we are using grammar-based repair

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index fc26d72f64988d29d45b790e6e9af39f028fa39d..9367444ac15f384e793a14cc4c2ab83c5158350b 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -150,8 +150,9 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
       for (unsigned index = 0; index < 2; index++)
       {
         std::vector<Node> es, vs;
-        Trace("cegis") << "  " << (index == 0 ? "Return values" : "Conditions")
-                       << " for " << e << ":\n";
+        Trace("cegis-unif")
+            << "  " << (index == 0 ? "Return values" : "Conditions") << " for "
+            << e << ":\n";
         // get the current unification enumerators
         d_u_enum_manager.getEnumeratorsForStrategyPt(e, es, index);
         // set enums for condition enumerators
@@ -163,7 +164,7 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
             // whether valueus exhausted
             if (mvMap.find(es[0]) == mvMap.end())
             {
-              Trace("cegis") << "    " << es[0] << " -> N/A\n";
+              Trace("cegis-unif") << "    " << es[0] << " -> N/A\n";
               es.clear();
             }
           }
@@ -174,13 +175,11 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
         {
           Assert(mvMap.find(eu) != mvMap.end());
           Node m_eu = mvMap[eu];
-          if (Trace.isOn("cegis"))
+          if (Trace.isOn("cegis-unif"))
           {
-            Trace("cegis") << "    " << eu << " -> ";
-            std::stringstream ss;
-            Printer::getPrinter(options::outputLanguage())
-                ->toStreamSygus(ss, m_eu);
-            Trace("cegis") << ss.str() << std::endl;
+            Trace("cegis-unif") << "    " << eu << " -> ";
+            TermDbSygus::toStreamSygus("cegis-unif", m_eu);
+            Trace("cegis-unif") << "\n";
           }
           vs.push_back(m_eu);
         }
@@ -289,6 +288,34 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
     return Cegis::processConstructCandidates(
         enums, enum_values, candidates, candidate_values, satisfiedRl, lems);
   }
+  if (Trace.isOn("cegis-unif"))
+  {
+    for (const Node& c : d_unif_candidates)
+    {
+      // Collect heads of candidates
+      Trace("cegis-unif") << "  Evaluation heads for " << c << " :\n";
+      for (const Node& hd : d_sygus_unif.getEvalPointHeads(c))
+      {
+        bool isUnit = false;
+        // d_rl_eval_hds accumulates eval apps, so need to look at operators
+        for (const Node& hd_unit : d_rl_eval_hds)
+        {
+          if (hd == hd_unit[0])
+          {
+            isUnit = true;
+            break;
+          }
+        }
+        Trace("cegis-unif") << "    " << hd << (isUnit ? "*" : "") << " -> ";
+        Assert(std::find(enums.begin(), enums.end(), hd) != enums.end());
+        unsigned i = std::distance(enums.begin(),
+                                   std::find(enums.begin(), enums.end(), hd));
+        Assert(i >= 0 && i < enum_values.size());
+        TermDbSygus::toStreamSygus("cegis-unif", enum_values[i]);
+        Trace("cegis-unif") << "\n";
+      }
+    }
+  }
   // the unification enumerators for conditions and their model values
   std::map<Node, std::vector<Node>> unif_cenums;
   std::map<Node, std::vector<Node>> unif_cvalues;