From b831d23137a97a481c6d74ad9259df2bdcf4243e Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Fri, 31 Jan 2025 19:32:48 +0100 Subject: [PATCH] renaming of tracing --- src/theory/quantifiers/mbqi_fast_sygus.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/theory/quantifiers/mbqi_fast_sygus.cpp b/src/theory/quantifiers/mbqi_fast_sygus.cpp index c39805a8d58..c7a7af7418d 100644 --- a/src/theory/quantifiers/mbqi_fast_sygus.cpp +++ b/src/theory/quantifiers/mbqi_fast_sygus.cpp @@ -67,20 +67,20 @@ void MVarInfo::initialize(Env& env, trules.push_back(symbol); } } - Trace("mbqi-fast-enum") << "Symbols: " << trules << std::endl; + Trace("mbqi-enum") << "Symbols: " << trules << std::endl; SygusGrammarCons sgc; Node bvl; TypeNode tng = sgc.mkDefaultSygusType(env, retType, bvl, trules); - if (TraceIsOn("mbqi-fast-enum")) + if (TraceIsOn("mbqi-enum")) { - Trace("mbqi-fast-enum") << "Enumerate terms for " << retType; + Trace("mbqi-enum") << "Enumerate terms for " << retType; if (!d_lamVars.isNull()) { - Trace("mbqi-fast-enum") << ", variable list " << d_lamVars; + Trace("mbqi-enum") << ", variable list " << d_lamVars; } - Trace("mbqi-fast-enum") << std::endl; - Trace("mbqi-fast-enum") << "Based on grammar:" << std::endl; - Trace("mbqi-fast-enum") + Trace("mbqi-enum") << std::endl; + Trace("mbqi-enum") << "Based on grammar:" << std::endl; + Trace("mbqi-enum") << printer::smt2::Smt2Printer::sygusGrammarString(tng) << std::endl; } d_senum.reset(new SygusTermEnumerator(env, tng));