Split TermRegistry object from TheoryStrings (#4312)

This consolidates functionalities from TheoryStrings and InferenceManager related to registering terms, including sending "preregistration lemmas" for them. The main purpose of this PR is to detangle this module from InferenceManager so that these two modules have exactly one call to OutputChannel::lemma each.

For the purposes of the theory solvers, TermRegistry contains the official SkolemCache of TheoryStrings, and can be seen as subsuming the previous interface for this class.

This PR is needed for further progress on strings proofs, marking as major since this will be a blocker shortly for this project.

A few things were cleaned in this PR. One function changed name InferenceManager::registerTerm --> TermRegistry::getRegisterTermLemma. No major behavior changes.

1 files changed, 5 insertions, 17 deletions

diff --git a/src/theory/strings/strings_fmf.h b/src/theory/strings/strings_fmf.h
index 375a100ff..9dfb1f590 100644
--- a/src/theory/strings/strings_fmf.h
+++ b/src/theory/strings/strings_fmf.h
@@ -22,7 +22,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "theory/decision_strategy.h"
-#include "theory/strings/skolem_cache.h"
+#include "theory/strings/term_registry.h"
 #include "theory/valuation.h"
 
 namespace CVC4 {
@@ -42,15 +42,8 @@ class StringsFmf
   StringsFmf(context::Context* c,
              context::UserContext* u,
              Valuation valuation,
-             SkolemCache& skc);
+             TermRegistry& tr);
   ~StringsFmf();
-  /** preRegister term
-   *
-   * This determines if the term n should be added to d_inputVars, the set
-   * of terms of type string whose length we are minimizing with this decision
-   * strategy.
-   */
-  void preRegisterTerm(TNode n);
   /** presolve
    *
    * This initializes a (new copy) of the decision strategy d_sslds.
@@ -105,15 +98,10 @@ class StringsFmf
   context::Context* d_satContext;
   /** The user level assertion context for the theory of strings. */
   context::UserContext* d_userContext;
-  /** The valuation object */
+  /** The valuation object of theory of strings */
   Valuation d_valuation;
-  /** reference to the skolem cache */
-  SkolemCache& d_skCache;
-  /**
-   * The set of terms of type string whose length we are minimizing
-   * with this decision strategy.
-   */
-  NodeSet d_inputVars;
+  /** The term registry of theory of strings */
+  TermRegistry& d_termReg;
 };
 
 }  // namespace strings