Improvements for NL traces (#5846)

This makes it so that -t nl-ext is a concise summary of what the nl-ext solver is doing, which I use frequently for debugging.

This is a temporary solution, we should consider a deeper refactoring of traces throughout NL at some point.

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index c6787140da925dde8db2242f98713511d8487e54..49385294c4df2d4e125c59d21229e2ab0abd8679 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -176,7 +176,7 @@ unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas,
 
 void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
 {
-  Trace("nl-ext") << "Getting assertions..." << std::endl;
+  Trace("nl-ext-assert-debug") << "Getting assertions..." << std::endl;
   bool useRelevance = false;
   if (options::nlRlvMode() == options::NlRlvMode::INTERLEAVE)
   {
@@ -197,8 +197,8 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
        ++it)
   {
     const Assertion& assertion = *it;
-    Trace("nl-ext") << "Loaded " << assertion.d_assertion << " from theory"
-                    << std::endl;
+    Trace("nl-ext-assert-debug")
+        << "Loaded " << assertion.d_assertion << " from theory" << std::endl;
     Node lit = assertion.d_assertion;
     if (useRelevance && !v.isRelevant(lit))
     {
@@ -234,7 +234,7 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
     auto iait = init_assertions.find(lit);
     if (iait != init_assertions.end())
     {
-      Trace("nl-ext") << "Adding " << lit << std::endl;
+      Trace("nl-ext-assert-debug") << "Adding " << lit << std::endl;
       assertions.push_back(lit);
       init_assertions.erase(iait);
     }
@@ -243,7 +243,7 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
   // function by the code above.
   for (const Node& a : init_assertions)
   {
-    Trace("nl-ext") << "Adding " << a << std::endl;
+    Trace("nl-ext-assert-debug") << "Adding " << a << std::endl;
     assertions.push_back(a);
   }
   Trace("nl-ext") << "...keep " << assertions.size() << " / "
@@ -599,11 +599,11 @@ void NonlinearExtension::runStrategy(Theory::Effort effort,
 {
   ++(d_stats.d_checkRuns);
 
-  if (Trace.isOn("nl-ext"))
+  if (Trace.isOn("nl-strategy"))
   {
     for (const auto& a : assertions)
     {
-      Trace("nl-ext") << "Input assertion: " << a << std::endl;
+      Trace("nl-strategy") << "Input assertion: " << a << std::endl;
     }
   }
   if (!d_strategy.isStrategyInit())
@@ -616,7 +616,7 @@ void NonlinearExtension::runStrategy(Theory::Effort effort,
   while (!stop && steps.hasNext())
   {
     InferStep step = steps.next();
-    Trace("nl-ext") << "Step " << step << std::endl;
+    Trace("nl-strategy") << "Step " << step << std::endl;
     switch (step)
     {
       case InferStep::BREAK: stop = d_im.hasPendingLemma(); break;
@@ -676,6 +676,7 @@ void NonlinearExtension::runStrategy(Theory::Effort effort,
     }
   }
 
+  Trace("nl-ext") << "finished strategy" << std::endl;
   Trace("nl-ext") << "  ...finished with " << d_im.numWaitingLemmas()
                   << " waiting lemmas." << std::endl;
   Trace("nl-ext") << "  ...finished with " << d_im.numPendingLemmas()

diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index b0254d2c5de9c80d1e9177c25ff672450c55a449..2ad7d39a252280d29fc4231d2a4245b376f3a5ee 100644 (file)
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -52,15 +52,15 @@ void ExponentialSolver::doPurification(TNode a, TNode new_a, TNode y)
 void ExponentialSolver::checkInitialRefine()
 {
   NodeManager* nm = NodeManager::currentNM();
-  Trace("nl-ext")
-      << "Get initial refinement lemmas for transcendental functions..."
-      << std::endl;
   for (std::pair<const Kind, std::vector<Node> >& tfl : d_data->d_funcMap)
   {
     if (tfl.first != Kind::EXPONENTIAL)
     {
       continue;
     }
+    Trace("nl-ext")
+        << "Get initial (exp) refinement lemmas for transcendental functions..."
+        << std::endl;
     Assert(tfl.first == Kind::EXPONENTIAL);
     for (const Node& t : tfl.second)
     {
@@ -107,9 +107,6 @@ void ExponentialSolver::checkInitialRefine()
 
 void ExponentialSolver::checkMonotonic()
 {
-  Trace("nl-ext") << "Get monotonicity lemmas for transcendental functions..."
-                  << std::endl;
-
   auto it = d_data->d_funcMap.find(Kind::EXPONENTIAL);
   if (it == d_data->d_funcMap.end())
   {
@@ -117,6 +114,9 @@ void ExponentialSolver::checkMonotonic()
     return;
   }
 
+  Trace("nl-ext")
+      << "Get monotonicity lemmas for (exp) transcendental functions..."
+      << std::endl;
   // sort arguments of all transcendentals
   std::vector<Node> tf_args;
   std::map<Node, Node> tf_arg_to_term;

diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index a88dd7faf808acef67e4f866f4f41a449c0ca943..1e3e1753dbd9a4ca5f46ebbc894fc5be519edc75 100644 (file)
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -86,15 +86,15 @@ void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y)
 void SineSolver::checkInitialRefine()
 {
   NodeManager* nm = NodeManager::currentNM();
-  Trace("nl-ext")
-      << "Get initial refinement lemmas for transcendental functions..."
-      << std::endl;
   for (std::pair<const Kind, std::vector<Node> >& tfl : d_data->d_funcMap)
   {
     if (tfl.first != Kind::SINE)
     {
       continue;
     }
+    Trace("nl-ext") << "Get initial (sine) refinement lemmas for "
+                       "transcendental functions..."
+                    << std::endl;
     for (const Node& t : tfl.second)
     {
       // initial refinements
@@ -181,8 +181,6 @@ void SineSolver::checkInitialRefine()
 
 void SineSolver::checkMonotonic()
 {
-  Trace("nl-ext") << "Get monotonicity lemmas for transcendental functions..."
-                  << std::endl;
 
   auto it = d_data->d_funcMap.find(Kind::SINE);
   if (it == d_data->d_funcMap.end())
@@ -190,6 +188,9 @@ void SineSolver::checkMonotonic()
     Trace("nl-ext-exp") << "No sine terms" << std::endl;
     return;
   }
+  Trace("nl-ext")
+      << "Get monotonicity lemmas for (sine) transcendental functions..."
+      << std::endl;
 
   // sort arguments of all transcendentals
   std::vector<Node> tf_args;

diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 233667e5be7dd2953dd1b9c624208f2b2c906d04..54f4303721a6ddddaa6340e4e9822310a140bf45 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -195,8 +195,15 @@ void TranscendentalSolver::checkTranscendentalMonotonic()
 
 void TranscendentalSolver::checkTranscendentalTangentPlanes()
 {
-  Trace("nl-ext") << "Get tangent plane lemmas for transcendental functions..."
-                  << std::endl;
+  if (Trace.isOn("nl-ext"))
+  {
+    if (!d_tstate.d_funcMap.empty())
+    {
+      Trace("nl-ext")
+          << "Get tangent plane lemmas for transcendental functions..."
+          << std::endl;
+    }
+  }
   // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions
   // via Incremental Linearization" by Cimatti et al
   for (const std::pair<const Kind, std::vector<Node> >& tfs :