Start refactoring of `-o` and `-v` (#7449)

This PR does the first step in consolidating our various output mechanisms. The goal is to have only three major ways to output information:
- verbose(level) prints log-like information to the user via stderr, -v and -q increase and decrease the verbosity, respectively.
- output(tag) prints structured information (as s-expressions) to the user via stdout, -o enables individual tags.
- Trace(tag) prints log-like information to the developer via stdout, -t enables individual tags.
While Debug and Trace (and eventually Dump) will be combined within Trace, all of Warning, Message, Notice and Chat will be combined into verbose.

9 files changed, 25 insertions, 32 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index fe48aa59d..1c6e3f0cb 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -382,9 +382,7 @@ void TheoryDatatypes::postCheck(Effort level)
   }
 
   Trace("datatypes-check") << "Finished check effort " << level << std::endl;
-  if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
-    Notice() << "TheoryDatatypes::check(): done" << endl;
-  }
+  Debug("datatypes") << "TheoryDatatypes::check(): done" << std::endl;
 }
 
 bool TheoryDatatypes::needsCheckLastEffort() {
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index f4370c017..0c9a5ba46 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -172,9 +172,9 @@ TrustNode AlphaEquivalence::reduceQuantifier(Node q)
   lem = ret.eqNode(q);
   if (q.getNumChildren() == 3)
   {
-    Notice() << "Ignoring annotated quantified formula based on alpha "
-                "equivalence: "
-             << q << std::endl;
+    verbose(1) << "Ignoring annotated quantified formula based on alpha "
+                  "equivalence: "
+               << q << std::endl;
   }
   // if successfully computed the substitution above
   if (isProofEnabled() && !vars.empty())
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index fdb0d0db3..f1d80032b 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -153,10 +153,9 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
         && d_auto_gen_trigger[1][f].empty() && !QuantAttributes::hasPattern(f))
     {
       Trace("trigger-warn") << "Could not find trigger for " << f << std::endl;
-      if (d_env.isOutputOn(options::OutputTag::TRIGGER))
+      if (isOutputOn(OutputTag::TRIGGER))
       {
-        d_env.getOutput(options::OutputTag::TRIGGER)
-            << "(no-trigger " << f << ")" << std::endl;
+        output(OutputTag::TRIGGER) << "(no-trigger " << f << ")" << std::endl;
       }
     }
   }
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index ff02e5f3e..e267b470d 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -78,12 +78,11 @@ Trigger::Trigger(Env& env,
     extNodes.push_back(ns);
   }
   d_trNode = NodeManager::currentNM()->mkNode(SEXPR, extNodes);
-  if (d_env.isOutputOn(options::OutputTag::TRIGGER))
+  if (isOutputOn(OutputTag::TRIGGER))
   {
     QuantAttributes& qa = d_qreg.getQuantAttributes();
-    d_env.getOutput(options::OutputTag::TRIGGER)
-        << "(trigger " << qa.quantToString(q) << " " << d_trNode << ")"
-        << std::endl;
+    output(OutputTag::TRIGGER) << "(trigger " << qa.quantToString(q) << " "
+                               << d_trNode << ")" << std::endl;
   }
   QuantifiersStatistics& stats = qs.getStats();
   if( d_nodes.size()==1 ){
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 23f789f4e..1af2b3f75 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -706,7 +706,7 @@ void Instantiate::notifyEndRound()
           << " * " << i.second << " for " << i.first << std::endl;
     }
   }
-  if (d_env.isOutputOn(options::OutputTag::INST))
+  if (isOutputOn(OutputTag::INST))
   {
     bool req = !options().printer.printInstFull;
     for (std::pair<const Node, uint32_t>& i : d_instDebugTemp)
@@ -716,9 +716,8 @@ void Instantiate::notifyEndRound()
       {
         continue;
       }
-      d_env.getOutput(options::OutputTag::INST)
-          << "(num-instantiations " << name << " " << i.second << ")"
-          << std::endl;
+      output(OutputTag::INST) << "(num-instantiations " << name << " "
+                              << i.second << ")" << std::endl;
     }
   }
 }
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 6c3f5e70b..1fde43913 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -372,7 +372,7 @@ bool SynthConjecture::doCheck()
     }
   }
 
-  bool printDebug = d_env.isOutputOn(options::OutputTag::SYGUS);
+  bool printDebug = isOutputOn(OutputTag::SYGUS);
   if (!constructed_cand)
   {
     // get the model value of the relevant terms from the master module
@@ -437,9 +437,9 @@ bool SynthConjecture::doCheck()
           }
         }
         Trace("sygus-engine") << std::endl;
-        if (d_env.isOutputOn(options::OutputTag::SYGUS))
+        if (d_env.isOutputOn(OutputTag::SYGUS))
         {
-          d_env.getOutput(options::OutputTag::SYGUS)
+          d_env.output(OutputTag::SYGUS)
               << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
         }
       }
@@ -518,16 +518,15 @@ bool SynthConjecture::doCheck()
   // print the candidate solution for debugging
   if (constructed_cand && printDebug)
   {
-    const Options& sopts = options();
-    std::ostream& out = *sopts.base.out;
+    std::ostream& out = output(OutputTag::SYGUS);
     out << "(sygus-candidate ";
     Assert(d_quant[0].getNumChildren() == candidate_values.size());
     for (size_t i = 0, ncands = candidate_values.size(); i < ncands; i++)
     {
       Node v = candidate_values[i];
-      std::stringstream ss;
-      TermDbSygus::toStreamSygus(ss, v);
-      out << "(" << d_quant[0][i] << " " << ss.str() << ")";
+      out << "(" << d_quant[0][i] << " ";
+      TermDbSygus::toStreamSygus(out, v);
+      out << ")";
     }
     out << ")" << std::endl;
   }
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 08fab59eb..2fc7f0c29 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -815,10 +815,11 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr, std::ostream& out)
     }
     if (!ptDisequalConst)
     {
-      Notice() << "Warning: " << bv << " and " << bvr
-               << " evaluate to different (non-constant) values on point:"
-               << std::endl;
-      Notice() << ptOut.str();
+      d_env.verbose(1)
+          << "Warning: " << bv << " and " << bvr
+          << " evaluate to different (non-constant) values on point:"
+          << std::endl;
+      d_env.verbose(1) << ptOut.str();
       return;
     }
     // we have detected unsoundness in the rewriter
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 03880bfbb..5aafae367 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1892,7 +1892,7 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
               // assertions with unevaluable operators, e.g. transcendental
               // functions. It also may happen for separation logic, where
               // check-model support is limited.
-              Warning() << ss.str();
+              warning() << ss.str();
             }
           }
         }
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 650ef1d70..83862e8bb 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -828,7 +828,6 @@ void SortModel::getDisequalitiesToRegions(int ri,
       for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
         if( (*it2).second ){
           Assert(isValid(d_regions_map[(*it2).first]));
-          //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
           regions_diseq[ d_regions_map[ (*it2).first ] ]++;
         }
       }
@@ -1046,7 +1045,6 @@ int SortModel::addSplit(Region* r)
     //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
     //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
     //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
-    //Notice() << "*** Split on " << s << std::endl;
     //split on the equality s
     Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
     // send lemma, with caching