Further standardization of strings statistics (#6128)

Also eliminates use of raw output channel in strings.

9 files changed, 30 insertions, 70 deletions

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 7eeba8497..e53ba35f8 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -292,6 +292,10 @@ const char* toString(InferenceId i)
     case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS";
     case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION";
     case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT";
+    case InferenceId::STRINGS_REGISTER_TERM_ATOMIC:
+      return "STRINGS_REGISTER_TERM_ATOMIC";
+    case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM";
+    case InferenceId::STRINGS_CMI_SPLIT: return "STRINGS_CMI_SPLIT";
 
     case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE";
     case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index b6d0d3c25..4af7761a0 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -384,7 +384,6 @@ enum class InferenceId
   STRINGS_CARD_SP,
   // The cardinality inference for strings, see Liang et al CAV 2014.
   STRINGS_CARDINALITY,
-  //-------------------- end base solver
   //-------------------- core solver
   // A cycle in the empty string equivalence class, e.g.:
   //   x ++ y = "" => x = ""
@@ -522,14 +521,12 @@ enum class InferenceId
   // is unknown, we apply the inference:
   //   len(s) != len(t) V len(s) = len(t)
   STRINGS_DEQ_LENGTH_SP,
-  //-------------------- end core solver
   //-------------------- codes solver
   // str.to_code( v ) = rewrite( str.to_code(c) )
   // where v is the proxy variable for c.
   STRINGS_CODE_PROXY,
   // str.code(x) = -1 V str.code(x) != str.code(y) V x = y
   STRINGS_CODE_INJ,
-  //-------------------- end codes solver
   //-------------------- regexp solver
   // regular expression normal form conflict
   //   ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false
@@ -565,7 +562,6 @@ enum class InferenceId
   STRINGS_RE_DELTA_CONF,
   // regular expression derive ???
   STRINGS_RE_DERIVE,
-  //-------------------- end regexp solver
   //-------------------- extended function solver
   // Standard extended function inferences from context-dependent rewriting
   // produced by constant substitutions. See Reynolds et al CAV 2017. These are
@@ -611,11 +607,16 @@ enum class InferenceId
   // f(x1, .., xn) and P is the reduction predicate for f
   // (see theory_strings_preprocess).
   STRINGS_REDUCTION,
-  //-------------------- end extended function solver
   //-------------------- prefix conflict
   // prefix conflict (coarse-grained)
   STRINGS_PREFIX_CONFLICT,
-  //-------------------- end prefix conflict
+  //-------------------- other
+  // a lemma added during term registration for an atomic term
+  STRINGS_REGISTER_TERM_ATOMIC,
+  // a lemma added during term registration
+  STRINGS_REGISTER_TERM,
+  // a split during collect model info
+  STRINGS_CMI_SPLIT,
   //-------------------------------------- end strings theory
 
   //-------------------------------------- uf theory
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index b746f2961..3c5bcc98d 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1941,7 +1941,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
     SkolemCache* skc = d_termReg.getSkolemCache();
     Node sk_w = skc->mkSkolem("w_loop");
     Node sk_y = skc->mkSkolem("y_loop");
-    d_termReg.registerTermAtomic(sk_y, LENGTH_GEQ_ONE);
+    iinfo.d_skolems[LENGTH_GEQ_ONE].push_back(sk_y);
     Node sk_z = skc->mkSkolem("z_loop");
     // t1 * ... * tn = y * z
     Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z));
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 0daaac29b..0d4839238 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -372,8 +372,6 @@ TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p)
                           << ii.getId() << std::endl;
   Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by "
                          << ii.getId() << std::endl;
-  ++(d_statistics.d_lemmasInfer);
-
   return tlem;
 }
 
diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp
index ec6b5e89b..c679bc414 100644
--- a/src/theory/strings/sequences_stats.cpp
+++ b/src/theory/strings/sequences_stats.cpp
@@ -31,13 +31,7 @@ SequencesStatistics::SequencesStatistics()
       d_rewrites("theory::strings::rewrites"),
       d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0),
       d_conflictsEager("theory::strings::conflictsEager", 0),
-      d_conflictsInfer("theory::strings::conflictsInfer", 0),
-      d_lemmasEagerPreproc("theory::strings::lemmasEagerPreproc", 0),
-      d_lemmasCmiSplit("theory::strings::lemmasCmiSplit", 0),
-      d_lemmasRegisterTerm("theory::strings::lemmasRegisterTerm", 0),
-      d_lemmasRegisterTermAtomic("theory::strings::lemmasRegisterTermAtomic",
-                                 0),
-      d_lemmasInfer("theory::strings::lemmasInfer", 0)
+      d_conflictsInfer("theory::strings::conflictsInfer", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_checkRuns);
   smtStatisticsRegistry()->registerStat(&d_strategyRuns);
@@ -50,11 +44,6 @@ SequencesStatistics::SequencesStatistics()
   smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine);
   smtStatisticsRegistry()->registerStat(&d_conflictsEager);
   smtStatisticsRegistry()->registerStat(&d_conflictsInfer);
-  smtStatisticsRegistry()->registerStat(&d_lemmasEagerPreproc);
-  smtStatisticsRegistry()->registerStat(&d_lemmasCmiSplit);
-  smtStatisticsRegistry()->registerStat(&d_lemmasRegisterTerm);
-  smtStatisticsRegistry()->registerStat(&d_lemmasRegisterTermAtomic);
-  smtStatisticsRegistry()->registerStat(&d_lemmasInfer);
 }
 
 SequencesStatistics::~SequencesStatistics()
@@ -70,11 +59,6 @@ SequencesStatistics::~SequencesStatistics()
   smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine);
   smtStatisticsRegistry()->unregisterStat(&d_conflictsEager);
   smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer);
-  smtStatisticsRegistry()->unregisterStat(&d_lemmasEagerPreproc);
-  smtStatisticsRegistry()->unregisterStat(&d_lemmasCmiSplit);
-  smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTerm);
-  smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTermAtomic);
-  smtStatisticsRegistry()->unregisterStat(&d_lemmasInfer);
 }
 
 }
diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index 01075eb26..1a0e94cdb 100644
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -47,9 +47,6 @@ namespace strings {
  *
  * "Conflicts" (2) arise from various kinds of reasoning, listed below,
  * where inferences are one of the possible methods for deriving conflicts.
- *
- * "Lemmas" (3) also arise from various kinds of reasoning, listed below,
- * where inferences are one of the possible methods for deriving lemmas.
  */
 class SequencesStatistics
 {
@@ -98,18 +95,6 @@ class SequencesStatistics
   /** Number of inference conflicts */
   IntStat d_conflictsInfer;
   //--------------- end of conflicts
-  //--------------- lemmas, partition of calls to OutputChannel::lemma
-  /** Number of lemmas added due to eager preprocessing */
-  IntStat d_lemmasEagerPreproc;
-  /** Number of collect model info splits */
-  IntStat d_lemmasCmiSplit;
-  /** Number of lemmas added due to registering terms */
-  IntStat d_lemmasRegisterTerm;
-  /** Number of lemmas added due to registering atomic terms */
-  IntStat d_lemmasRegisterTermAtomic;
-  /** Number of lemmas added due to inferences */
-  IntStat d_lemmasInfer;
-  //--------------- end of lemmas
 };
 
 }
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 628b2798d..9497b9661 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -19,6 +19,7 @@
 #include "options/strings_options.h"
 #include "smt/logic_exception.h"
 #include "theory/rewriter.h"
+#include "theory/strings/inference_manager.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
 
@@ -37,11 +38,10 @@ typedef expr::Attribute<StringsProxyVarAttributeId, bool>
     StringsProxyVarAttribute;
 
 TermRegistry::TermRegistry(SolverState& s,
-                           OutputChannel& out,
                            SequencesStatistics& statistics,
                            ProofNodeManager* pnm)
     : d_state(s),
-      d_out(out),
+      d_im(nullptr),
       d_statistics(statistics),
       d_hasStrCode(false),
       d_functionsTerms(s.getSatContext()),
@@ -65,6 +65,8 @@ TermRegistry::TermRegistry(SolverState& s,
 
 TermRegistry::~TermRegistry() {}
 
+void TermRegistry::finishInit(InferenceManager* im) { d_im = im; }
+
 Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
 {
   NodeManager* nm = NodeManager::currentNM();
@@ -162,7 +164,7 @@ void TermRegistry::preRegisterTerm(TNode n)
   }
   else if (k == STRING_IN_REGEXP)
   {
-    d_out.requirePhase(n, true);
+    d_im->requirePhase(n, true);
     ee->addTriggerPredicate(n);
     ee->addTerm(n[0]);
     ee->addTerm(n[1]);
@@ -302,8 +304,7 @@ void TermRegistry::registerTerm(Node n, int effort)
                            << std::endl;
     Trace("strings-assert")
         << "(assert " << regTermLem.getNode() << ")" << std::endl;
-    ++(d_statistics.d_lemmasRegisterTerm);
-    d_out.trustedLemma(regTermLem);
+    d_im->trustedLemma(regTermLem, InferenceId::STRINGS_REGISTER_TERM);
   }
 }
 
@@ -416,12 +417,11 @@ void TermRegistry::registerTermAtomic(Node n, LengthStatus s)
                            << std::endl;
     Trace("strings-assert")
         << "(assert " << lenLem.getNode() << ")" << std::endl;
-    ++(d_statistics.d_lemmasRegisterTermAtomic);
-    d_out.trustedLemma(lenLem);
+    d_im->trustedLemma(lenLem, InferenceId::STRINGS_REGISTER_TERM_ATOMIC);
   }
   for (const std::pair<const Node, bool>& rp : reqPhase)
   {
-    d_out.requirePhase(rp.first, rp.second);
+    d_im->requirePhase(rp.first, rp.second);
   }
 }
 
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index 261ba277c..a3d1d1e0e 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -32,6 +32,7 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
+class InferenceManager;
 /**
  * This class manages all the (pre)registration tasks for terms. These tasks
  * include:
@@ -50,10 +51,11 @@ class TermRegistry
 
  public:
   TermRegistry(SolverState& s,
-               OutputChannel& out,
                SequencesStatistics& statistics,
                ProofNodeManager* pnm);
   ~TermRegistry();
+  /** Finish initialize, which sets the inference manager */
+  void finishInit(InferenceManager* im);
   /** The eager reduce routine
    *
    * Constructs a lemma for t that is incomplete, but communicates pertinent
@@ -205,8 +207,8 @@ class TermRegistry
   uint32_t d_cardSize;
   /** Reference to the solver state of the theory of strings. */
   SolverState& d_state;
-  /** Reference to the output channel of the theory of strings. */
-  OutputChannel& d_out;
+  /** Pointer to the inference manager of the theory of strings. */
+  InferenceManager* d_im;
   /** Reference to the statistics for the theory of strings/sequences. */
   SequencesStatistics& d_statistics;
   /** have we asserted any str.code terms? */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index fbede89f0..2a5d043f5 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -47,7 +47,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_statistics(),
       d_state(c, u, d_valuation),
       d_eagerSolver(d_state),
-      d_termReg(d_state, out, d_statistics, pnm),
+      d_termReg(d_state, d_statistics, pnm),
       d_extTheoryCb(),
       d_extTheory(d_extTheoryCb, c, u, out),
       d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm),
@@ -71,6 +71,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_regexp_elim(options::regExpElimAgg(), pnm, u),
       d_stringsFmf(c, u, valuation, d_termReg)
 {
+  d_termReg.finishInit(&d_im);
 
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -167,21 +168,7 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
 
 bool TheoryStrings::propagateLit(TNode literal)
 {
-  Debug("strings-propagate")
-      << "TheoryStrings::propagateLit(" << literal << ")" << std::endl;
-  // If already in conflict, no more propagation
-  if (d_state.isInConflict())
-  {
-    Debug("strings-propagate") << "TheoryStrings::propagateLit(" << literal
-                               << "): already in conflict" << std::endl;
-    return false;
-  }
-  // Propagate out
-  bool ok = d_out->propagate(literal);
-  if (!ok) {
-    d_state.notifyInConflict();
-  }
-  return ok;
+  return d_im.propagateLit(literal);
 }
 
 TrustNode TheoryStrings::explain(TNode literal)
@@ -455,8 +442,7 @@ bool TheoryStrings::collectModelInfoType(
               for (const Node& sl : len_splits)
               {
                 Node spl = nm->mkNode(OR, sl, sl.negate());
-                ++(d_statistics.d_lemmasCmiSplit);
-                d_out->lemma(spl);
+                d_im.lemma(spl, InferenceId::STRINGS_CMI_SPLIT);
                 Trace("strings-lemma")
                     << "Strings::CollectModelInfoSplit: " << spl << std::endl;
               }