Eliminate remaining references to parent TheoryStrings object (#4315)

This PR makes it so that the module dependencies in the theory of strings are acyclic. This is important for further organization towards proofs for strings.

The main change in this PR is to ensure that InferenceManager has a pointer to ExtTheory, which is needed for several of its methods. This required changing several solvers into unique_ptr to properly initialize.

1 files changed, 49 insertions, 104 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 3e490f285..9e14d6a3f 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -73,10 +73,10 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_equalityEngine(d_notify, c, "theory::strings::ee", true),
       d_state(c, d_equalityEngine, d_valuation),
       d_termReg(c, u, d_equalityEngine, out, d_statistics),
-      d_im(*this, c, u, d_state, d_termReg, out, d_statistics),
+      d_im(nullptr),
       d_rewriter(&d_statistics.d_rewrites),
-      d_bsolver(c, u, d_state, d_im),
-      d_csolver(c, u, d_state, d_im, d_termReg, d_bsolver),
+      d_bsolver(nullptr),
+      d_csolver(nullptr),
       d_esolver(nullptr),
       d_rsolver(nullptr),
       d_stringsFmf(c, u, valuation, d_termReg),
@@ -84,18 +84,24 @@ TheoryStrings::TheoryStrings(context::Context* c,
 {
   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(c, u, 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_im,
                                  d_termReg,
                                  d_rewriter,
-                                 d_bsolver,
-                                 d_csolver,
-                                 extt,
+                                 *d_bsolver,
+                                 *d_csolver,
+                                 *extt,
                                  d_statistics));
-  d_rsolver.reset(
-      new RegExpSolver(*this, d_state, d_im, *d_esolver, d_statistics, c, u));
+  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);
@@ -143,11 +149,6 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
   return false;
 }
 
-Node TheoryStrings::getNormalString(Node x, std::vector<Node>& nf_exp)
-{
-  return d_csolver.getNormalString(x, nf_exp);
-}
-
 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
@@ -201,7 +202,7 @@ bool TheoryStrings::propagate(TNode literal) {
 Node 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);
   if( assumptions.empty() ){
     return d_true;
   }else if( assumptions.size()==1 ){
@@ -365,7 +366,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)
         {
           // does it have a code and the length of these equivalence classes are
@@ -499,7 +500,7 @@ bool TheoryStrings::collectModelInfoType(
   //step 4 : assign constants to all other equivalence classes
   for( unsigned i=0; i<nodes.size(); i++ ){
     if( processed.find( nodes[i] )==processed.end() ){
-      NormalForm& nf = d_csolver.getNormalForm(nodes[i]);
+      NormalForm& nf = d_csolver->getNormalForm(nodes[i]);
       if (Trace.isOn("strings-model"))
       {
         Trace("strings-model")
@@ -586,8 +587,6 @@ void TheoryStrings::check(Effort e) {
 
   TimerStat::CodeTimer checkTimer(d_checkTime);
 
-  bool polarity;
-  TNode atom;
   // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
   Trace("strings-check-debug")
       << "Theory of strings, check : " << e << std::endl;
@@ -598,13 +597,9 @@ void TheoryStrings::check(Effort e) {
     TNode fact = assertion.d_assertion;
 
     Trace("strings-assertion") << "get assertion: " << fact << endl;
-    polarity = fact.getKind() != kind::NOT;
-    atom = polarity ? fact : fact[0];
-
-    //assert pending fact
-    assertPendingFact( atom, polarity, fact );
+    d_im->sendAssumption(fact);
   }
-  d_im.doPendingFacts();
+  d_im->doPendingFacts();
 
   Assert(d_strategy_init);
   std::map<Effort, std::pair<unsigned, unsigned> >::iterator itsr =
@@ -661,10 +656,10 @@ void TheoryStrings::check(Effort e) {
       Trace("strings-check") << "  * Run strategy..." << std::endl;
       runStrategy(sbegin, send);
       // 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: ";
@@ -681,8 +676,8 @@ 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() {
@@ -831,68 +826,16 @@ void TheoryStrings::computeCareGraph(){
   }
 }
 
-void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
-  Trace("strings-pending") << "Assert pending fact : " << atom << " " << polarity << " from " << exp << std::endl;
-  Assert(atom.getKind() != kind::OR) << "Infer error: a split.";
-  if( atom.getKind()==kind::EQUAL ){
-    Trace("strings-pending-debug") << "  Register term" << std::endl;
-    for( unsigned j=0; j<2; j++ ) {
-      if (!d_equalityEngine.hasTerm(atom[j])
-          && atom[j].getType().isStringLike())
-      {
-        d_termReg.registerTerm(atom[j], 0);
-      }
-    }
-    Trace("strings-pending-debug") << "  Now assert equality" << std::endl;
-    d_equalityEngine.assertEquality( atom, polarity, exp );
-    Trace("strings-pending-debug") << "  Finished assert equality" << std::endl;
-  } else {
-    d_equalityEngine.assertPredicate( atom, polarity, exp );
-    if (atom.getKind() == STRING_IN_REGEXP)
-    {
-      if (polarity && atom[1].getKind() == REGEXP_CONCAT)
-      {
-        Node eqc = d_equalityEngine.getRepresentative(atom[0]);
-        d_state.addEndpointsToEqcInfo(atom, atom[1], eqc);
-      }
-    }
-  }
-  // process the conflict
-  if (!d_state.isInConflict())
-  {
-    Node pc = d_state.getPendingConflict();
-    if (!pc.isNull())
-    {
-      std::vector<Node> a;
-      a.push_back(pc);
-      Trace("strings-pending")
-          << "Process pending conflict " << pc << std::endl;
-      Node conflictNode = d_im.mkExplain(a);
-      d_state.setConflict();
-      Trace("strings-conflict")
-          << "CONFLICT: Eager prefix : " << conflictNode << std::endl;
-      ++(d_statistics.d_conflictsEagerPrefix);
-      d_out->conflict(conflictNode);
-    }
-  }
-  Trace("strings-pending-debug") << "  Now collect terms" << std::endl;
-  // Collect extended function terms in the atom. Notice that we must register
-  // all extended functions occurring in assertions and shared terms. We
-  // make a similar call to registerTermRec in addSharedTerm.
-  getExtTheory()->registerTermRec( atom );
-  Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
-}
-
 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);
       }
@@ -914,10 +857,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];
@@ -931,7 +874,8 @@ void TheoryStrings::checkCodes()
         Node vc = nm->mkNode(STRING_TO_CODE, cp);
         if (!d_state.areEqual(cc, vc))
         {
-          d_im.sendInference(d_empty_vec, cc.eqNode(vc), Inference::CODE_PROXY);
+          std::vector<Node> emptyVec;
+          d_im->sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY);
         }
         const_codes.push_back(vc);
       }
@@ -945,7 +889,7 @@ void TheoryStrings::checkCodes()
         }
       }
     }
-    if (d_im.hasProcessed())
+    if (d_im->hasProcessed())
     {
       return;
     }
@@ -968,8 +912,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.sendInference(d_empty_vec, inj_lem, Inference::CODE_INJ);
+          d_im->sendPhaseRequirement(deq, false);
+          std::vector<Node> emptyVec;
+          d_im->sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
         }
       }
     }
@@ -978,10 +923,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();
@@ -1039,25 +984,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_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_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_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;
 }
@@ -1165,7 +1110,7 @@ void TheoryStrings::runStrategy(unsigned sbegin, unsigned send)
     InferStep curr = d_infer_steps[i];
     if (curr == BREAK)
     {
-      if (d_im.hasProcessed())
+      if (d_im->hasProcessed())
       {
         break;
       }