Skip to content

Commit

Permalink
renaming of tracing
Browse files Browse the repository at this point in the history
  • Loading branch information
kondylidou committed Jan 31, 2025
1 parent eb595d1 commit b831d23
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions src/theory/quantifiers/mbqi_fast_sygus.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down

0 comments on commit b831d23

Please sign in to comment.