Make ExtTheory a utility and not a member of Theory (#4753)

Previously, we assumed that ExtTheory, the module for doing context-dependent simplification, was one-to-one with Theory. This design is not necessary. This makes this class a utility, which can be used as needed. This makes e.g. the initialization of TheoryStrings much easier, since the ExtTheory object can be created first.

4 files changed, 69 insertions, 70 deletions

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 9b1b0e6dd..eff0b3d74 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -74,6 +74,8 @@ ExtfSolver::ExtfSolver(context::Context* c,
 
 ExtfSolver::~ExtfSolver() {}
 
+void ExtfSolver::addSharedTerm(TNode n) { d_extt.registerTermRec(n); }
+
 bool ExtfSolver::doReduction(int effort, Node n)
 {
   Assert(d_extfInfoTmp.find(n) != d_extfInfoTmp.end());
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index d99a881f6..80921550e 100644
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -95,6 +95,11 @@ class ExtfSolver
              SequencesStatistics& statistics);
   ~ExtfSolver();
 
+  /**
+   * Called when a shared term is added to theory of strings, this registers
+   * n with the extended theory utility for context-depdendent simplification.
+   */
+  void addSharedTerm(TNode n);
   /** check extended functions evaluation
    *
    * This applies "context-dependent simplification" for all active extended
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 150ea8977..03f9d8d1c 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -46,35 +46,24 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_equalityEngine(d_notify, c, "theory::strings::ee", true),
       d_state(c, u, d_equalityEngine, d_valuation),
       d_termReg(d_state, d_equalityEngine, out, d_statistics, nullptr),
-      d_im(nullptr),
+      d_extTheory(this),
+      d_im(c, u, d_state, d_termReg, d_extTheory, out, d_statistics),
       d_rewriter(&d_statistics.d_rewrites),
-      d_bsolver(nullptr),
-      d_csolver(nullptr),
-      d_esolver(nullptr),
-      d_rsolver(nullptr),
+      d_bsolver(d_state, d_im),
+      d_csolver(c, u, d_state, d_im, d_termReg, d_bsolver),
+      d_esolver(c,
+                u,
+                d_state,
+                d_im,
+                d_termReg,
+                d_rewriter,
+                d_bsolver,
+                d_csolver,
+                d_extTheory,
+                d_statistics),
+      d_rsolver(d_state, d_im, d_csolver, d_esolver, d_statistics, c, u),
       d_stringsFmf(c, u, valuation, d_termReg)
 {
-  setupExtTheory();
-  ExtTheory* extt = getExtTheory();
-  // initialize the inference manager, which requires the extended theory
-  d_im.reset(
-      new InferenceManager(c, u, d_state, d_termReg, *extt, out, d_statistics));
-  // initialize the solvers
-  d_bsolver.reset(new BaseSolver(d_state, *d_im));
-  d_csolver.reset(new CoreSolver(c, u, d_state, *d_im, d_termReg, *d_bsolver));
-  d_esolver.reset(new ExtfSolver(c,
-                                 u,
-                                 d_state,
-                                 *d_im,
-                                 d_termReg,
-                                 d_rewriter,
-                                 *d_bsolver,
-                                 *d_csolver,
-                                 *extt,
-                                 d_statistics));
-  d_rsolver.reset(new RegExpSolver(
-      d_state, *d_im, *d_csolver, *d_esolver, d_statistics, c, u));
-
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
   d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
@@ -152,7 +141,7 @@ void TheoryStrings::addSharedTerm(TNode t) {
   d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS);
   if (options::stringExp())
   {
-    getExtTheory()->registerTermRec(t);
+    d_esolver.addSharedTerm(t);
   }
   Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl;
 }
@@ -195,7 +184,7 @@ TrustNode TheoryStrings::explain(TNode literal)
 {
   Debug("strings-explain") << "explain called on " << literal << std::endl;
   std::vector< TNode > assumptions;
-  d_im->explain(literal, assumptions);
+  d_im.explain(literal, assumptions);
   Node ret;
   if( assumptions.empty() ){
     ret = d_true;
@@ -213,7 +202,7 @@ bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& var
   for( unsigned i=0; i<vars.size(); i++ ){
     Node n = vars[i];
     Trace("strings-subs") << "  get subs for " << n << "..." << std::endl;
-    Node s = d_esolver->getCurrentSubstitutionFor(effort, n, exp[n]);
+    Node s = d_esolver.getCurrentSubstitutionFor(effort, n, exp[n]);
     subs.push_back(s);
   }
   return true;
@@ -364,7 +353,7 @@ bool TheoryStrings::collectModelInfoType(
       //check if col[i][j] has only variables
       if (!eqc.isConst())
       {
-        NormalForm& nfe = d_csolver->getNormalForm(eqc);
+        NormalForm& nfe = d_csolver.getNormalForm(eqc);
         if (nfe.d_nf.size() == 1)
         {
           // is it an equivalence class with a seq.unit term?
@@ -516,7 +505,7 @@ bool TheoryStrings::collectModelInfoType(
   {
     if (processed.find(rn) == processed.end())
     {
-      NormalForm& nf = d_csolver->getNormalForm(rn);
+      NormalForm& nf = d_csolver.getNormalForm(rn);
       if (Trace.isOn("strings-model"))
       {
         Trace("strings-model")
@@ -625,9 +614,9 @@ void TheoryStrings::check(Effort e) {
     TNode fact = assertion.d_assertion;
 
     Trace("strings-assertion") << "get assertion: " << fact << endl;
-    d_im->sendAssumption(fact);
+    d_im.sendAssumption(fact);
   }
-  d_im->doPendingFacts();
+  d_im.doPendingFacts();
 
   Assert(d_strat.isStrategyInit());
   if (!d_state.isInConflict() && !d_valuation.needCheck()
@@ -680,10 +669,10 @@ void TheoryStrings::check(Effort e) {
       Trace("strings-check") << "  * Run strategy..." << std::endl;
       runStrategy(e);
       // flush the facts
-      addedFact = d_im->hasPendingFact();
-      addedLemma = d_im->hasPendingLemma();
-      d_im->doPendingFacts();
-      d_im->doPendingLemmas();
+      addedFact = d_im.hasPendingFact();
+      addedLemma = d_im.hasPendingLemma();
+      d_im.doPendingFacts();
+      d_im.doPendingLemmas();
       if (Trace.isOn("strings-check"))
       {
         Trace("strings-check") << "  ...finish run strategy: ";
@@ -700,13 +689,13 @@ void TheoryStrings::check(Effort e) {
     } while (!d_state.isInConflict() && !addedLemma && addedFact);
   }
   Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
-  Assert(!d_im->hasPendingFact());
-  Assert(!d_im->hasPendingLemma());
+  Assert(!d_im.hasPendingFact());
+  Assert(!d_im.hasPendingLemma());
 }
 
 bool TheoryStrings::needsCheckLastEffort() {
   if( options::stringGuessModel() ){
-    return d_esolver->hasExtendedFunctions();
+    return d_esolver.hasExtendedFunctions();
   }
   return false;
 }
@@ -853,14 +842,14 @@ void TheoryStrings::computeCareGraph(){
 
 void TheoryStrings::checkRegisterTermsPreNormalForm()
 {
-  const std::vector<Node>& seqc = d_bsolver->getStringEqc();
+  const std::vector<Node>& seqc = d_bsolver.getStringEqc();
   for (const Node& eqc : seqc)
   {
     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
     while (!eqc_i.isFinished())
     {
       Node n = (*eqc_i);
-      if (!d_bsolver->isCongruent(n))
+      if (!d_bsolver.isCongruent(n))
       {
         d_termReg.registerTerm(n, 2);
       }
@@ -882,10 +871,10 @@ void TheoryStrings::checkCodes()
     // str.code applied to the proxy variables for each equivalence classes that
     // are constants of size one
     std::vector<Node> const_codes;
-    const std::vector<Node>& seqc = d_bsolver->getStringEqc();
+    const std::vector<Node>& seqc = d_bsolver.getStringEqc();
     for (const Node& eqc : seqc)
     {
-      NormalForm& nfe = d_csolver->getNormalForm(eqc);
+      NormalForm& nfe = d_csolver.getNormalForm(eqc);
       if (nfe.d_nf.size() == 1 && nfe.d_nf[0].isConst())
       {
         Node c = nfe.d_nf[0];
@@ -900,7 +889,7 @@ void TheoryStrings::checkCodes()
         if (!d_state.areEqual(cc, vc))
         {
           std::vector<Node> emptyVec;
-          d_im->sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY);
+          d_im.sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY);
         }
         const_codes.push_back(vc);
       }
@@ -914,7 +903,7 @@ void TheoryStrings::checkCodes()
         }
       }
     }
-    if (d_im->hasProcessed())
+    if (d_im.hasProcessed())
     {
       return;
     }
@@ -937,9 +926,9 @@ void TheoryStrings::checkCodes()
           Node eqn = c1[0].eqNode(c2[0]);
           // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
           Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn);
-          d_im->sendPhaseRequirement(deq, false);
+          d_im.sendPhaseRequirement(deq, false);
           std::vector<Node> emptyVec;
-          d_im->sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
+          d_im.sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
         }
       }
     }
@@ -948,10 +937,10 @@ void TheoryStrings::checkCodes()
 
 void TheoryStrings::checkRegisterTermsNormalForms()
 {
-  const std::vector<Node>& seqc = d_bsolver->getStringEqc();
+  const std::vector<Node>& seqc = d_bsolver.getStringEqc();
   for (const Node& eqc : seqc)
   {
-    NormalForm& nfi = d_csolver->getNormalForm(eqc);
+    NormalForm& nfi = d_csolver.getNormalForm(eqc);
     // check if there is a length term for this equivalence class
     EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
     Node lt = ei ? ei->d_lengthTerm : Node::null();
@@ -982,7 +971,7 @@ TrustNode TheoryStrings::ppRewrite(TNode atom)
   if( !options::stringLazyPreproc() ){
     //eager preprocess here
     std::vector< Node > new_nodes;
-    StringsPreprocess* p = d_esolver->getPreprocess();
+    StringsPreprocess* p = d_esolver.getPreprocess();
     Node ret = p->processAssertion(atomRet, new_nodes);
     if (ret != atomRet)
     {
@@ -1018,25 +1007,25 @@ void TheoryStrings::runInferStep(InferStep s, int effort)
   Trace("strings-process") << "..." << std::endl;
   switch (s)
   {
-    case CHECK_INIT: d_bsolver->checkInit(); break;
-    case CHECK_CONST_EQC: d_bsolver->checkConstantEquivalenceClasses(); break;
-    case CHECK_EXTF_EVAL: d_esolver->checkExtfEval(effort); break;
-    case CHECK_CYCLES: d_csolver->checkCycles(); break;
-    case CHECK_FLAT_FORMS: d_csolver->checkFlatForms(); break;
+    case CHECK_INIT: d_bsolver.checkInit(); break;
+    case CHECK_CONST_EQC: d_bsolver.checkConstantEquivalenceClasses(); break;
+    case CHECK_EXTF_EVAL: d_esolver.checkExtfEval(effort); break;
+    case CHECK_CYCLES: d_csolver.checkCycles(); break;
+    case CHECK_FLAT_FORMS: d_csolver.checkFlatForms(); break;
     case CHECK_REGISTER_TERMS_PRE_NF: checkRegisterTermsPreNormalForm(); break;
-    case CHECK_NORMAL_FORMS_EQ: d_csolver->checkNormalFormsEq(); break;
-    case CHECK_NORMAL_FORMS_DEQ: d_csolver->checkNormalFormsDeq(); break;
+    case CHECK_NORMAL_FORMS_EQ: d_csolver.checkNormalFormsEq(); break;
+    case CHECK_NORMAL_FORMS_DEQ: d_csolver.checkNormalFormsDeq(); break;
     case CHECK_CODES: checkCodes(); break;
-    case CHECK_LENGTH_EQC: d_csolver->checkLengthsEqc(); break;
+    case CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break;
     case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break;
-    case CHECK_EXTF_REDUCTION: d_esolver->checkExtfReductions(effort); break;
-    case CHECK_MEMBERSHIP: d_rsolver->checkMemberships(); break;
-    case CHECK_CARDINALITY: d_bsolver->checkCardinality(); break;
+    case CHECK_EXTF_REDUCTION: d_esolver.checkExtfReductions(effort); break;
+    case CHECK_MEMBERSHIP: d_rsolver.checkMemberships(); break;
+    case CHECK_CARDINALITY: d_bsolver.checkCardinality(); break;
     default: Unreachable(); break;
   }
   Trace("strings-process") << "Done " << s
-                           << ", addedFact = " << d_im->hasPendingFact()
-                           << ", addedLemma = " << d_im->hasPendingLemma()
+                           << ", addedFact = " << d_im.hasPendingFact()
+                           << ", addedLemma = " << d_im.hasPendingLemma()
                            << ", conflict = " << d_state.isInConflict()
                            << std::endl;
 }
@@ -1053,7 +1042,7 @@ void TheoryStrings::runStrategy(Theory::Effort e)
     InferStep curr = it->first;
     if (curr == BREAK)
     {
-      if (d_im->hasProcessed())
+      if (d_im.hasProcessed())
       {
         break;
       }
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index dfaa99c06..29c3cd64c 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -25,6 +25,7 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "expr/node_trie.h"
+#include "theory/ext_theory.h"
 #include "theory/strings/base_solver.h"
 #include "theory/strings/core_solver.h"
 #include "theory/strings/extf_solver.h"
@@ -275,27 +276,29 @@ class TheoryStrings : public Theory {
   SolverState d_state;
   /** The term registry for this theory */
   TermRegistry d_termReg;
+  /** Extended theory, responsible for context-dependent simplification. */
+  ExtTheory d_extTheory;
   /** The (custom) output channel of the theory of strings */
-  std::unique_ptr<InferenceManager> d_im;
+  InferenceManager d_im;
   /** The theory rewriter for this theory. */
   StringsRewriter d_rewriter;
   /**
    * The base solver, responsible for reasoning about congruent terms and
    * inferring constants for equivalence classes.
    */
-  std::unique_ptr<BaseSolver> d_bsolver;
+  BaseSolver d_bsolver;
   /**
    * The core solver, responsible for reasoning about string concatenation
    * with length constraints.
    */
-  std::unique_ptr<CoreSolver> d_csolver;
+  CoreSolver d_csolver;
   /**
    * Extended function solver, responsible for reductions and simplifications
    * involving extended string functions.
    */
-  std::unique_ptr<ExtfSolver> d_esolver;
+  ExtfSolver d_esolver;
   /** regular expression solver module */
-  std::unique_ptr<RegExpSolver> d_rsolver;
+  RegExpSolver d_rsolver;
   /** regular expression elimination module */
   RegExpElimination d_regexp_elim;
   /** Strings finite model finding decision strategy */