From 4c1f67446ad59f1c5efe7230b96b0d3ccac0e692 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 2 Feb 2021 09:49:25 -0600 Subject: [PATCH] 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. --- src/theory/arith/nl/nonlinear_extension.cpp | 17 +++++++++-------- .../nl/transcendental/exponential_solver.cpp | 12 ++++++------ .../arith/nl/transcendental/sine_solver.cpp | 11 ++++++----- .../nl/transcendental/transcendental_solver.cpp | 11 +++++++++-- 4 files changed, 30 insertions(+), 21 deletions(-) diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index c6787140d..49385294c 100644 --- 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& lemmas, void NonlinearExtension::getAssertions(std::vector& 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& 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& 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& 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 b0254d2c5..2ad7d39a2 100644 --- 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 >& 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 tf_args; std::map 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 a88dd7faf..1e3e1753d 100644 --- 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 >& 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 tf_args; diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 233667e5b..54f430372 100644 --- 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 >& tfs : -- 2.30.2