(new theory) Update TheoryStrings to new standard (#4963)

This updates theory of strings to the new standard.

This makes strings use the standard template for check and collectModelInfo. It also updates its inference manager to the standard and makes use of assertFactInternal for processing internal facts. This now enables preNotifyFact and notifyFact to be defined in TheoryStrings instead of inside inference manager, which is clearer and eliminates some dependencies within inference manager.

Note that the inference manager of strings for now inherits from TheoryInferenceManager. Further standardization will make it inherit from the new InferenceManagerBuffered class.

This design will be merged into proof-new, which also has significant changes to strings inference manager.

4 files changed, 108 insertions, 190 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index dce038fbf..811c040f3 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -28,19 +28,17 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-InferenceManager::InferenceManager(context::Context* c,
-                                   context::UserContext* u,
+InferenceManager::InferenceManager(Theory& t,
                                    SolverState& s,
                                    TermRegistry& tr,
                                    ExtTheory& e,
-                                   OutputChannel& out,
-                                   SequencesStatistics& statistics)
-    : d_state(s),
+                                   SequencesStatistics& statistics,
+                                   ProofNodeManager* pnm)
+    : TheoryInferenceManager(t, s, pnm),
+      d_state(s),
       d_termReg(tr),
       d_extt(e),
-      d_out(out),
-      d_statistics(statistics),
-      d_keep(c)
+      d_statistics(statistics)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_zero = nm->mkConst(Rational(0));
@@ -49,14 +47,6 @@ InferenceManager::InferenceManager(context::Context* c,
   d_false = nm->mkConst(false);
 }
 
-void InferenceManager::sendAssumption(TNode lit)
-{
-  bool polarity = lit.getKind() != kind::NOT;
-  TNode atom = polarity ? lit : lit[0];
-  // assert pending fact
-  assertPendingFact(atom, polarity, lit);
-}
-
 bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
                                              Node conc,
                                              Inference infer)
@@ -299,7 +289,7 @@ void InferenceManager::doPendingFacts()
         TNode atom = polarity ? fact : fact[0];
         // no double negation or double (conjunctive) conclusions
         Assert(atom.getKind() != NOT && atom.getKind() != AND);
-        assertPendingFact(atom, polarity, exp);
+        assertInternalFact(atom, polarity, exp);
       }
     }
     else
@@ -308,13 +298,8 @@ void InferenceManager::doPendingFacts()
       TNode atom = polarity ? facts : facts[0];
       // no double negation or double (conjunctive) conclusions
       Assert(atom.getKind() != NOT && atom.getKind() != AND);
-      assertPendingFact(atom, polarity, exp);
+      assertInternalFact(atom, polarity, exp);
     }
-    // Must reference count the equality and its explanation, which is not done
-    // by the equality engine. Notice that we do not need to do this for
-    // external assertions, which enter as facts through sendAssumption.
-    d_keep.insert(facts);
-    d_keep.insert(exp);
     i++;
   }
   d_pending.clear();
@@ -392,68 +377,6 @@ void InferenceManager::doPendingLemmas()
   d_pendingReqPhase.clear();
 }
 
-void InferenceManager::assertPendingFact(Node atom, bool polarity, Node exp)
-{
-  eq::EqualityEngine* ee = d_state.getEqualityEngine();
-  Trace("strings-pending") << "Assert pending fact : " << atom << " "
-                           << polarity << " from " << exp << std::endl;
-  Assert(atom.getKind() != OR) << "Infer error: a split.";
-  if (atom.getKind() == EQUAL)
-  {
-    // we must ensure these terms are registered
-    Trace("strings-pending-debug") << "  Register term" << std::endl;
-    for (const Node& t : atom)
-    {
-      // terms in the equality engine are already registered, hence skip
-      // currently done for only string-like terms, but this could potentially
-      // be avoided.
-      if (!ee->hasTerm(t) && t.getType().isStringLike())
-      {
-        d_termReg.registerTerm(t, 0);
-      }
-    }
-    Trace("strings-pending-debug") << "  Now assert equality" << std::endl;
-    ee->assertEquality(atom, polarity, exp);
-    Trace("strings-pending-debug") << "  Finished assert equality" << std::endl;
-  }
-  else
-  {
-    ee->assertPredicate(atom, polarity, exp);
-    if (atom.getKind() == STRING_IN_REGEXP)
-    {
-      if (polarity && atom[1].getKind() == REGEXP_CONCAT)
-      {
-        Node eqc = ee->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 = mkExplain(a);
-      d_state.notifyInConflict();
-      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 TheoryStrings::addSharedTerm.
-  d_extt.registerTermRec(atom);
-  Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
-}
-
 bool InferenceManager::hasProcessed() const
 {
   return d_state.isInConflict() || !d_pendingLem.empty() || !d_pending.empty();
@@ -475,7 +398,6 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a,
   {
     utils::flattenOp(AND, ac, aconj);
   }
-  eq::EqualityEngine* ee = d_state.getEqualityEngine();
   for (const Node& apc : aconj)
   {
     if (std::find(noExplain.begin(), noExplain.end(), apc) != noExplain.end())
@@ -492,12 +414,12 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a,
     Debug("strings-explain") << "Add to explanation " << apc << std::endl;
     if (apc.getKind() == NOT && apc[0].getKind() == EQUAL)
     {
-      Assert(ee->hasTerm(apc[0][0]));
-      Assert(ee->hasTerm(apc[0][1]));
+      Assert(d_ee->hasTerm(apc[0][0]));
+      Assert(d_ee->hasTerm(apc[0][1]));
       // ensure that we are ready to explain the disequality
-      AlwaysAssert(ee->areDisequal(apc[0][0], apc[0][1], true));
+      AlwaysAssert(d_ee->areDisequal(apc[0][0], apc[0][1], true));
     }
-    Assert(apc.getKind() != EQUAL || ee->areEqual(apc[0], apc[1]));
+    Assert(apc.getKind() != EQUAL || d_ee->areEqual(apc[0], apc[1]));
     // now, explain
     explain(apc, antec_exp);
   }
@@ -522,7 +444,6 @@ void InferenceManager::explain(TNode literal,
 {
   Debug("strings-explain") << "Explain " << literal << " "
                            << d_state.isInConflict() << std::endl;
-  eq::EqualityEngine* ee = d_state.getEqualityEngine();
   bool polarity = literal.getKind() != NOT;
   TNode atom = polarity ? literal : literal[0];
   std::vector<TNode> tassumptions;
@@ -530,14 +451,14 @@ void InferenceManager::explain(TNode literal,
   {
     if (atom[0] != atom[1])
     {
-      Assert(ee->hasTerm(atom[0]));
-      Assert(ee->hasTerm(atom[1]));
-      ee->explainEquality(atom[0], atom[1], polarity, tassumptions);
+      Assert(d_ee->hasTerm(atom[0]));
+      Assert(d_ee->hasTerm(atom[1]));
+      d_ee->explainEquality(atom[0], atom[1], polarity, tassumptions);
     }
   }
   else
   {
-    ee->explainPredicate(atom, polarity, tassumptions);
+    d_ee->explainPredicate(atom, polarity, tassumptions);
   }
   for (const TNode a : tassumptions)
   {
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index 016891737..dc46f1683 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -29,6 +29,7 @@
 #include "theory/strings/sequences_stats.h"
 #include "theory/strings/solver_state.h"
 #include "theory/strings/term_registry.h"
+#include "theory/theory_inference_manager.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
@@ -65,28 +66,20 @@ namespace strings {
  * theory of strings, e.g. sendPhaseRequirement, setIncomplete, and
  * with the extended theory object e.g. markCongruent.
  */
-class InferenceManager
+class InferenceManager : public TheoryInferenceManager
 {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 
  public:
-  InferenceManager(context::Context* c,
-                   context::UserContext* u,
+  InferenceManager(Theory& t,
                    SolverState& s,
                    TermRegistry& tr,
                    ExtTheory& e,
-                   OutputChannel& out,
-                   SequencesStatistics& statistics);
+                   SequencesStatistics& statistics,
+                   ProofNodeManager* pnm);
   ~InferenceManager() {}
 
-  /** send assumption
-   *
-   * This is called when a fact is asserted to TheoryStrings. It adds lit
-   * to the equality engine maintained by this class immediately.
-   */
-  void sendAssumption(TNode lit);
-
   /** send internal inferences
    *
    * This is called when we have inferred exp => conc, where exp is a set
@@ -292,23 +285,12 @@ class InferenceManager
   // ------------------------------------------------- end extended theory
 
  private:
-  /** assert pending fact
-   *
-   * This asserts atom with polarity to the equality engine of this class,
-   * where exp is the explanation of why (~) atom holds.
-   *
-   * This call may trigger further initialization steps involving the terms
-   * of atom, including calls to registerTerm.
-   */
-  void assertPendingFact(Node atom, bool polarity, Node exp);
   /** Reference to the solver state of the theory of strings. */
   SolverState& d_state;
   /** Reference to the term registry of theory of strings */
   TermRegistry& d_termReg;
   /** the extended theory object for the theory of strings */
   ExtTheory& d_extt;
-  /** A reference to the output channel of the theory of strings. */
-  OutputChannel& d_out;
   /** Reference to the statistics for the theory of strings/sequences. */
   SequencesStatistics& d_statistics;
 
@@ -326,13 +308,6 @@ class InferenceManager
   std::map<Node, bool> d_pendingReqPhase;
   /** A list of pending lemmas to be sent on the output channel. */
   std::vector<InferInfo> d_pendingLem;
-  /**
-   * The keep set of this class. This set is maintained to ensure that
-   * facts and their explanations are ref-counted. Since facts and their
-   * explanations are SAT-context-dependent, this set is also
-   * SAT-context-dependent.
-   */
-  NodeSet d_keep;
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 846f9240d..3e60cbc44 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -46,7 +46,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_state(c, u, d_valuation),
       d_termReg(d_state, out, d_statistics, nullptr),
       d_extTheory(this),
-      d_im(c, u, d_state, d_termReg, d_extTheory, out, d_statistics),
+      d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm),
       d_rewriter(&d_statistics.d_rewrites),
       d_bsolver(d_state, d_im),
       d_csolver(d_state, d_im, d_termReg, d_bsolver),
@@ -83,6 +83,8 @@ TheoryStrings::TheoryStrings(context::Context* c,
   }
   // use the state object as the official theory state
   d_theoryState = &d_state;
+  // use the inference manager as the official inference manager
+  d_inferManager = &d_im;
 }
 
 TheoryStrings::~TheoryStrings() {
@@ -165,23 +167,6 @@ void TheoryStrings::notifySharedTerm(TNode t)
   Debug("strings") << "TheoryStrings::notifySharedTerm() finished" << std::endl;
 }
 
-EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
-  if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b))
-  {
-    if (d_equalityEngine->areEqual(a, b))
-    {
-      // The terms are implied to be equal
-      return EQUALITY_TRUE;
-    }
-    if (d_equalityEngine->areDisequal(a, b, false))
-    {
-      // The terms are implied to be dis-equal
-      return EQUALITY_FALSE;
-    }
-  }
-  return EQUALITY_UNKNOWN;
-}
-
 bool TheoryStrings::propagateLit(TNode literal)
 {
   Debug("strings-propagate")
@@ -252,24 +237,10 @@ void TheoryStrings::presolve() {
 // MODEL GENERATION
 /////////////////////////////////////////////////////////////////////////////
 
-bool TheoryStrings::collectModelInfo(TheoryModel* m)
+bool TheoryStrings::collectModelValues(TheoryModel* m,
+                                       const std::set<Node>& termSet)
 {
-  Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl;
-  Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
-
-  std::set<Node> termSet;
-
-  // Compute terms appearing in assertions and shared terms
-  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
-  computeAssertedTerms(termSet, irrKinds);
-  // assert the (relevant) portion of the equality engine to the model
-  if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
-  {
-    Unreachable()
-        << "TheoryStrings::collectModelInfo: failed to assert equality engine"
-        << std::endl;
-    return false;
-  }
+  Trace("strings-model") << "TheoryStrings : Collect model values" << std::endl;
 
   std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > repSet;
   // Generate model
@@ -654,25 +625,68 @@ TrustNode TheoryStrings::expandDefinition(Node node)
   return TrustNode::null();
 }
 
-void TheoryStrings::check(Effort e) {
-  if (done() && e<EFFORT_FULL) {
-    return;
+bool TheoryStrings::preNotifyFact(
+    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+  // this is only required for internal facts, others are already registered
+  if (isInternal && atom.getKind() == EQUAL)
+  {
+    // we must ensure these terms are registered
+    for (const Node& t : atom)
+    {
+      // terms in the equality engine are already registered, hence skip
+      // currently done for only string-like terms, but this could potentially
+      // be avoided.
+      if (!d_equalityEngine->hasTerm(t) && t.getType().isStringLike())
+      {
+        d_termReg.registerTerm(t, 0);
+      }
+    }
   }
+  return false;
+}
 
-  TimerStat::CodeTimer checkTimer(d_checkTime);
-
-  // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
-  Trace("strings-check-debug")
-      << "Theory of strings, check : " << e << std::endl;
-  while (!done() && !d_state.isInConflict())
+void TheoryStrings::notifyFact(TNode atom,
+                               bool polarity,
+                               TNode fact,
+                               bool isInternal)
+{
+  if (atom.getKind() == STRING_IN_REGEXP)
   {
-    // Get all the assertions
-    Assertion assertion = get();
-    TNode fact = assertion.d_assertion;
-
-    Trace("strings-assertion") << "get assertion: " << fact << endl;
-    d_im.sendAssumption(fact);
+    if (polarity && atom[1].getKind() == REGEXP_CONCAT)
+    {
+      Node eqc = d_equalityEngine->getRepresentative(atom[0]);
+      d_state.addEndpointsToEqcInfo(atom, atom[1], eqc);
+    }
   }
+  // process pending conflicts due to reasoning about endpoints
+  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);
+      Trace("strings-conflict")
+          << "CONFLICT: Eager prefix : " << conflictNode << std::endl;
+      ++(d_statistics.d_conflictsEagerPrefix);
+      d_im.conflict(conflictNode);
+      return;
+    }
+  }
+  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 TheoryStrings::addSharedTerm.
+  d_extTheory.registerTermRec(atom);
+  Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
+}
+
+void TheoryStrings::postCheck(Effort e)
+{
   d_im.doPendingFacts();
 
   Assert(d_strat.isStrategyInit());
@@ -681,8 +695,10 @@ void TheoryStrings::check(Effort e) {
   {
     Trace("strings-check-debug")
         << "Theory of strings " << e << " effort check " << std::endl;
-    if(Trace.isOn("strings-eqc")) {
-      for( unsigned t=0; t<2; t++ ) {
+    if (Trace.isOn("strings-eqc"))
+    {
+      for (unsigned t = 0; t < 2; t++)
+      {
         eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine);
         Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
         while( !eqcs2_i.isFinished() ){
@@ -726,7 +742,9 @@ void TheoryStrings::check(Effort e) {
       ++(d_statistics.d_strategyRuns);
       Trace("strings-check") << "  * Run strategy..." << std::endl;
       runStrategy(e);
-      // flush the facts
+      // Send the facts *and* the lemmas. We send lemmas regardless of whether
+      // we send facts since some lemmas cannot be dropped. Other lemmas are
+      // otherwise avoided by aborting the strategy when a fact is ready.
       addedFact = d_im.hasPendingFact();
       addedLemma = d_im.hasPendingLemma();
       d_im.doPendingFacts();
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index f4aa0675c..0f59e73dc 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -97,27 +97,33 @@ class TheoryStrings : public Theory {
   void shutdown() override {}
   /** add shared term */
   void notifySharedTerm(TNode n) override;
-  /** get equality status */
-  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   /** preregister term */
   void preRegisterTerm(TNode n) override;
   /** Expand definition */
   TrustNode expandDefinition(Node n) override;
-  /** Check at effort e */
-  void check(Effort e) override;
-  /** needs check last effort */
+  //--------------------------------- standard check
+  /** Do we need a check call at last call effort? */
   bool needsCheckLastEffort() override;
+  bool preNotifyFact(TNode atom,
+                     bool pol,
+                     TNode fact,
+                     bool isPrereg,
+                     bool isInternal) override;
+  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+  /** Post-check, called after the fact queue of the theory is processed. */
+  void postCheck(Effort level) override;
+  //--------------------------------- end standard check
+  /** propagate method */
+  bool propagateLit(TNode literal);
   /** Conflict when merging two constants */
   void conflict(TNode a, TNode b);
   /** called when a new equivalence class is created */
   void eqNotifyNewClass(TNode t);
   /** preprocess rewrite */
   TrustNode ppRewrite(TNode atom) override;
-  /**
-   * Get all relevant information in this theory regarding the current
-   * model. Return false if a contradiction is discovered.
-   */
-  bool collectModelInfo(TheoryModel* m) override;
+  /** Collect model values in m based on the relevant terms given by termSet */
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
 
  private:
   /** NotifyClass for equality engine */
@@ -171,8 +177,6 @@ class TheoryStrings : public Theory {
     /** The solver state of the theory of strings */
     SolverState& d_state;
   };/* class TheoryStrings::NotifyClass */
-  /** propagate method */
-  bool propagateLit(TNode literal);
   /** compute care graph */
   void computeCareGraph() override;
   /**