Improve cegqi engine trace. (#2714)

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e1cbed0446e7511c5834685c86d7933bcf8ea5d0..3f0ac70f5171cef19a94dba852dac58a054550bc 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -354,7 +354,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     if (!d_master->allowPartialModel() && !fullModel)
     {
       // we retain the values in d_ev_active_gen_waiting
-      Trace("cegqi-engine") << "...partial model, fail." << std::endl;
+      Trace("cegqi-engine-debug") << "...partial model, fail." << std::endl;
       // if we are partial due to an active enumerator, we may still succeed
       // on the next call
       return !activeIncomplete;
@@ -362,19 +362,27 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     // the waiting values are passed to the module below, clear
     d_ev_active_gen_waiting.clear();
 
-    // debug print
     Assert(terms.size() == enum_values.size());
     bool emptyModel = true;
-    Trace("cegqi-engine") << "  * Value is : ";
     for (unsigned i = 0, size = terms.size(); i < size; i++)
     {
-      Node nv = enum_values[i];
-      if (!nv.isNull())
+      if (!enum_values[i].isNull())
       {
         emptyModel = false;
       }
-      if (Trace.isOn("cegqi-engine"))
+    }
+    if (emptyModel)
+    {
+      Trace("cegqi-engine-debug") << "...empty model, fail." << std::endl;
+      return !activeIncomplete;
+    }
+    // debug print
+    if (Trace.isOn("cegqi-engine"))
+    {
+      Trace("cegqi-engine") << "  * Value is : ";
+      for (unsigned i = 0, size = terms.size(); i < size; i++)
       {
+        Node nv = enum_values[i];
         Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv;
         TypeNode tn = onv.getType();
         std::stringstream ss;
@@ -395,12 +403,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
           }
         }
       }
-    }
-    Trace("cegqi-engine") << std::endl;
-    if (emptyModel)
-    {
-      Trace("cegqi-engine") << "...empty model, fail." << std::endl;
-      return !activeIncomplete;
+      Trace("cegqi-engine") << std::endl;
     }
     Assert(candidate_values.empty());
     constructed_cand = d_master->constructCandidates(

diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 479cfa53513fa1418b39dbdd1839a45443ff6af9..d3eff1750fd3c76fdcb9ad12e43f36254e8de47d 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -321,7 +321,8 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
       return true;
     }
 
-    Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
+    Trace("cegqi-engine-debug")
+        << "  *** Check candidate phase..." << std::endl;
     std::vector<Node> cclems;
     bool ret = conj->doCheck(cclems);
     bool addedLemma = false;
@@ -343,7 +344,8 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
     }
     if (addedLemma)
     {
-      Trace("cegqi-engine") << "  ...check for counterexample." << std::endl;
+      Trace("cegqi-engine-debug")
+          << "  ...check for counterexample." << std::endl;
       return true;
     }
     else
@@ -358,7 +360,8 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
   }
   else
   {
-    Trace("cegqi-engine") << "  *** Refine candidate phase..." << std::endl;
+    Trace("cegqi-engine-debug")
+        << "  *** Refine candidate phase..." << std::endl;
     std::vector<Node> rlems;
     conj->doRefine(rlems);
     bool addedLemma = false;
@@ -381,7 +384,7 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
     }
     if (addedLemma)
     {
-      Trace("cegqi-engine") << "  ...refine candidate." << std::endl;
+      Trace("cegqi-engine-debug") << "  ...refine candidate." << std::endl;
     }
   }
   return true;