Make sets and strings solver states inherit from TheoryState (#4918)

This is towards the new standard for theory solvers.

This PR makes the custom states of sets and strings inherit from the standard base class TheoryState. It also makes a minor change to InferenceManager/SolverState to make sets more in line with the plan for a standard base class InferenceManager.

Followup PRs will establish the official TheoryState classes for all other theories (which in most cases will be an instance of the base class).

4 files changed, 10 insertions, 118 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 88cf6d958..a8ebd921a 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -171,7 +171,7 @@ void InferenceManager::sendInference(const InferInfo& ii, bool asLemma)
       // only keep stats if we process it here
       d_statistics.d_inferences << ii.d_id;
       d_out.conflict(conf);
-      d_state.setConflict();
+      d_state.notifyInConflict();
       return;
     }
     Trace("strings-infer-debug") << "...as lemma" << std::endl;
@@ -435,7 +435,7 @@ void InferenceManager::assertPendingFact(Node atom, bool polarity, Node exp)
       Trace("strings-pending")
           << "Process pending conflict " << pc << std::endl;
       Node conflictNode = mkExplain(a);
-      d_state.setConflict();
+      d_state.notifyInConflict();
       Trace("strings-conflict")
           << "CONFLICT: Eager prefix : " << conflictNode << std::endl;
       ++(d_statistics.d_conflictsEagerPrefix);
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 8634478fd..fd0f0174f 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -28,13 +28,7 @@ namespace strings {
 SolverState::SolverState(context::Context* c,
                          context::UserContext* u,
                          Valuation& v)
-    : d_context(c),
-      d_ucontext(u),
-      d_ee(nullptr),
-      d_eeDisequalities(c),
-      d_valuation(v),
-      d_conflict(c, false),
-      d_pendingConflict(c)
+    : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflict(c)
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
 }
@@ -47,59 +41,6 @@ SolverState::~SolverState()
   }
 }
 
-void SolverState::finishInit(eq::EqualityEngine* ee)
-{
-  Assert(ee != nullptr);
-  d_ee = ee;
-}
-
-context::Context* SolverState::getSatContext() const { return d_context; }
-context::UserContext* SolverState::getUserContext() const { return d_ucontext; }
-
-Node SolverState::getRepresentative(Node t) const
-{
-  if (d_ee->hasTerm(t))
-  {
-    return d_ee->getRepresentative(t);
-  }
-  return t;
-}
-
-bool SolverState::hasTerm(Node a) const { return d_ee->hasTerm(a); }
-
-bool SolverState::areEqual(Node a, Node b) const
-{
-  if (a == b)
-  {
-    return true;
-  }
-  else if (hasTerm(a) && hasTerm(b))
-  {
-    return d_ee->areEqual(a, b);
-  }
-  return false;
-}
-
-bool SolverState::areDisequal(Node a, Node b) const
-{
-  if (a == b)
-  {
-    return false;
-  }
-  else if (hasTerm(a) && hasTerm(b))
-  {
-    Node ar = d_ee->getRepresentative(a);
-    Node br = d_ee->getRepresentative(b);
-    return (ar != br && ar.isConst() && br.isConst())
-           || d_ee->areDisequal(ar, br, false);
-  }
-  Node ar = getRepresentative(a);
-  Node br = getRepresentative(b);
-  return ar != br && ar.isConst() && br.isConst();
-}
-
-eq::EqualityEngine* SolverState::getEqualityEngine() const { return d_ee; }
-
 const context::CDList<Node>& SolverState::getDisequalityList() const
 {
   return d_eeDisequalities;
@@ -199,7 +140,7 @@ EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake)
   return nullptr;
 }
 
-TheoryModel* SolverState::getModel() const { return d_valuation.getModel(); }
+TheoryModel* SolverState::getModel() { return d_valuation.getModel(); }
 
 void SolverState::addEndpointsToEqcInfo(Node t, Node concat, Node eqc)
 {
@@ -286,9 +227,6 @@ bool SolverState::isEqualEmptyWord(Node s, Node& emps)
   return false;
 }
 
-void SolverState::setConflict() { d_conflict = true; }
-bool SolverState::isInConflict() const { return d_conflict; }
-
 void SolverState::setPendingConflictWhen(Node conf)
 {
   if (!conf.isNull() && d_pendingConflict.get().isNull())
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index 0322abdb7..fc27b847b 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -39,7 +39,7 @@ namespace strings {
  * (2) Whether the set of assertions is in conflict.
  * (3) Equivalence class information as in the class above.
  */
-class SolverState
+class SolverState : public TheoryState
 {
   typedef context::CDList<Node> NodeList;
 
@@ -48,36 +48,8 @@ class SolverState
               context::UserContext* u,
               Valuation& v);
   ~SolverState();
-  /**
-   * Finish initialize, ee is a pointer to the official equality engine
-   * of theory of strings.
-   */
-  void finishInit(eq::EqualityEngine* ee);
-  /** Get the SAT context */
-  context::Context* getSatContext() const;
-  /** Get the user context */
-  context::UserContext* getUserContext() const;
   //-------------------------------------- equality information
   /**
-   * Get the representative of t in the equality engine of this class, or t
-   * itself if it is not registered as a term.
-   */
-  Node getRepresentative(Node t) const;
-  /** Is t registered as a term in the equality engine of this class? */
-  bool hasTerm(Node a) const;
-  /**
-   * Are a and b equal according to the equality engine of this class? Also
-   * returns true if a and b are identical.
-   */
-  bool areEqual(Node a, Node b) const;
-  /**
-   * Are a and b disequal according to the equality engine of this class? Also
-   * returns true if the representative of a and b are distinct constants.
-   */
-  bool areDisequal(Node a, Node b) const;
-  /** get equality engine */
-  eq::EqualityEngine* getEqualityEngine() const;
-  /**
    * Get the list of disequalities that are currently asserted to the equality
    * engine.
    */
@@ -92,14 +64,6 @@ class SolverState
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
   //-------------------------------------- end notifications for equalities
   //------------------------------------------ conflicts
-  /**
-   * Set that the current state of the solver is in conflict. This should be
-   * called immediately after a call to conflict(...) on the output channel of
-   * the theory of strings.
-   */
-  void setConflict();
-  /** Are we currently in conflict? */
-  bool isInConflict() const;
   /** set pending conflict
    *
    * If conf is non-null, this is called when conf is a conjunction of literals
@@ -153,7 +117,7 @@ class SolverState
    */
   EqcInfo* getOrMakeEqcInfo(Node eqc, bool doMake = true);
   /** Get pointer to the model object of the Valuation object */
-  TheoryModel* getModel() const;
+  TheoryModel* getModel();
 
   /** add endpoints to eqc info
    *
@@ -186,21 +150,11 @@ class SolverState
  private:
   /** Common constants */
   Node d_zero;
-  /** Pointer to the SAT context object used by the theory of strings. */
-  context::Context* d_context;
-  /** Pointer to the user context object used by the theory of strings. */
-  context::UserContext* d_ucontext;
-  /** Pointer to equality engine of the theory of strings. */
-  eq::EqualityEngine* d_ee;
   /**
    * The (SAT-context-dependent) list of disequalities that have been asserted
    * to the equality engine above.
    */
   NodeList d_eeDisequalities;
-  /** Reference to the valuation of the theory of strings */
-  Valuation& d_valuation;
-  /** Are we in conflict? */
-  context::CDO<bool> d_conflict;
   /** The pending conflict if one exists */
   context::CDO<Node> d_pendingConflict;
   /** Map from representatives to their equivalence class information */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index c78e8dc2a..6d81c742a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -81,6 +81,8 @@ TheoryStrings::TheoryStrings(context::Context* c,
     // add checkers
     d_sProofChecker.registerTo(pc);
   }
+  // use the state object as the official theory state
+  d_theoryState = &d_state;
 }
 
 TheoryStrings::~TheoryStrings() {
@@ -126,8 +128,6 @@ void TheoryStrings::finishInit()
   d_equalityEngine->addFunctionKind(kind::STRING_TOLOWER, eagerEval);
   d_equalityEngine->addFunctionKind(kind::STRING_TOUPPER, eagerEval);
   d_equalityEngine->addFunctionKind(kind::STRING_REV, eagerEval);
-
-  d_state.finishInit(d_equalityEngine);
 }
 
 std::string TheoryStrings::identify() const
@@ -196,7 +196,7 @@ bool TheoryStrings::propagate(TNode literal) {
   // Propagate out
   bool ok = d_out->propagate(literal);
   if (!ok) {
-    d_state.setConflict();
+    d_state.notifyInConflict();
   }
   return ok;
 }
@@ -762,7 +762,7 @@ void TheoryStrings::conflict(TNode a, TNode b){
   if (!d_state.isInConflict())
   {
     Debug("strings-conflict") << "Making conflict..." << std::endl;
-    d_state.setConflict();
+    d_state.notifyInConflict();
     TrustNode conflictNode = explain(a.eqNode(b));
     Trace("strings-conflict")
         << "CONFLICT: Eq engine conflict : " << conflictNode.getNode()