Extend the standard Theory template based on equality engine (#4929)

Apart from { quantifiers, bool, builtin }, each Theory now has an official equality engine. This PR elaborates on the standard recommended template that Theory should follow, which applies to all theories, regardless of whether they have an equality engine.

This includes:

A standard check method. The Theory is now expected to implement 4 callbacks (preCheck, postCheck, preNotifyFact, notifyFact).
A standard collectModelInfo method. The Theory is now expected to implement 2 callbacks (computeRelevantTerms, collectModelValues).
Additionally, 2 more methods have an obvious default:
(1) getEqualityStatus, which returns information based on an equality engine if it exists,
(2) addSharedTerm, which adds the term as a trigger term to the equality engine of the theory if it exists. Notice that for the sake of more consistent naming, theories now implement notifySharedTerm (previously TheoryEngine called theory-independent addSharedTermInternal which called addSharedTerm, this is updated now to addSharedTerm/notifySharedTerm).

Other methods will not be standardized yet e.g. preRegisterTerm, since they vary per theory.

FYI @barrettcw

Each theory on the branch https://github.com/ajreynol/CVC4/tree/centralEe conforms to this template (e.g. they do not override check or collectModelInfo). The next step will be to pull the new implementation of each Theory from that branch.

21 files changed, 290 insertions, 118 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 4e0582f50..ea751ca74 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -87,9 +87,7 @@ TrustNode TheoryArith::expandDefinition(Node node)
   return d_internal->expandDefinition(node);
 }
 
-void TheoryArith::addSharedTerm(TNode n){
-  d_internal->addSharedTerm(n);
-}
+void TheoryArith::notifySharedTerm(TNode n) { d_internal->addSharedTerm(n); }
 
 TrustNode TheoryArith::ppRewrite(TNode atom)
 {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index d0147fe9f..bfe30db61 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -104,7 +104,7 @@ class TheoryArith : public Theory {
 
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
-  void addSharedTerm(TNode n) override;
+  void notifySharedTerm(TNode n) override;
 
   Node getModelValue(TNode var) override;
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 34c4fd156..b4a234748 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -883,9 +883,11 @@ Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
 // SHARING
 /////////////////////////////////////////////////////////////////////////////
 
-
-void TheoryArrays::addSharedTerm(TNode t) {
-  Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
+void TheoryArrays::notifySharedTerm(TNode t)
+{
+  Debug("arrays::sharing") << spaces(getSatContext()->getLevel())
+                           << "TheoryArrays::notifySharedTerm(" << t << ")"
+                           << std::endl;
   d_equalityEngine->addTriggerTerm(t, THEORY_ARRAYS);
   if (t.getType().isArray()) {
     d_sharedArrays.insert(t);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index a1fa19631..8cbf826c1 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -251,7 +251,7 @@ class TheoryArrays : public Theory {
   void checkPair(TNode r1, TNode r2);
 
  public:
-  void addSharedTerm(TNode t) override;
+  void notifySharedTerm(TNode t) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   void computeCareGraph() override;
   bool isShared(TNode t)
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d03d81a3d..1696d6185 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -880,9 +880,10 @@ TrustNode TheoryBV::explain(TNode node)
   return TrustNode::mkTrustPropExp(node, explanation, nullptr);
 }
 
-
-void TheoryBV::addSharedTerm(TNode t) {
-  Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
+void TheoryBV::notifySharedTerm(TNode t)
+{
+  Debug("bitvector::sharing")
+      << indent() << "TheoryBV::notifySharedTerm(" << t << ")" << std::endl;
   d_sharedTermsSet.insert(t);
   if (options::bitvectorEqualitySolver()) {
     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 65100f98f..c6e9282f4 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -244,7 +244,7 @@ class TheoryBV : public Theory {
    */
   void explain(TNode literal, std::vector<TNode>& assumptions);
 
-  void addSharedTerm(TNode t) override;
+  void notifySharedTerm(TNode t) override;
 
   bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 65264bb3f..f85b79c53 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -727,11 +727,13 @@ TrustNode TheoryDatatypes::ppRewrite(TNode in)
   return TrustNode::null();
 }
 
-void TheoryDatatypes::addSharedTerm(TNode t) {
-  Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
-                     << t << " " << t.getType().isBoolean() << endl;
+void TheoryDatatypes::notifySharedTerm(TNode t)
+{
+  Debug("datatypes") << "TheoryDatatypes::notifySharedTerm(): " << t << " "
+                     << t.getType().isBoolean() << endl;
   d_equalityEngine->addTriggerTerm(t, THEORY_DATATYPES);
-  Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
+  Debug("datatypes") << "TheoryDatatypes::notifySharedTerm() finished"
+                     << std::endl;
 }
 
 bool TheoryDatatypes::propagateLit(TNode literal)
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 137aae469..6dd990b30 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -290,7 +290,7 @@ private:
   void preRegisterTerm(TNode n) override;
   TrustNode expandDefinition(Node n) override;
   TrustNode ppRewrite(TNode n) override;
-  void addSharedTerm(TNode t) override;
+  void notifySharedTerm(TNode t) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   bool collectModelInfo(TheoryModel* m) override;
   void shutdown() override {}
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 82086aafe..0c5a92572 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -908,9 +908,10 @@ void TheoryFp::preRegisterTerm(TNode node)
   return;
 }
 
-void TheoryFp::addSharedTerm(TNode node) {
+void TheoryFp::notifySharedTerm(TNode node)
+{
   Trace("fp-addSharedTerm")
-      << "TheoryFp::addSharedTerm(): " << node << std::endl;
+      << "TheoryFp::notifySharedTerm(): " << node << std::endl;
   // A system-wide invariant; terms must be registered before they are shared
   Assert(isRegistered(node));
   return;
@@ -998,7 +999,6 @@ void TheoryFp::check(Effort level) {
   }
 
   // Resolve the abstractions for the conversion lemmas
-  //  if (level == EFFORT_COMBINATION) {
   if (level == EFFORT_LAST_CALL)
   {
     Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl;
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index ad052f92a..79ece7bce 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -58,7 +58,7 @@ class TheoryFp : public Theory {
   TrustNode expandDefinition(Node node) override;
 
   void preRegisterTerm(TNode node) override;
-  void addSharedTerm(TNode node) override;
+  void notifySharedTerm(TNode node) override;
 
   TrustNode ppRewrite(TNode node) override;
 
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index cf3cf2f9a..0059d9f3a 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -160,9 +160,9 @@ TrustNode TheorySep::explain(TNode literal)
 // SHARING
 /////////////////////////////////////////////////////////////////////////////
 
-
-void TheorySep::addSharedTerm(TNode t) {
-  Debug("sep") << "TheorySep::addSharedTerm(" << t << ")" << std::endl;
+void TheorySep::notifySharedTerm(TNode t)
+{
+  Debug("sep") << "TheorySep::notifySharedTerm(" << t << ")" << std::endl;
   d_equalityEngine->addTriggerTerm(t, THEORY_SEP);
 }
 
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index bbb37a3a2..af411c64a 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -114,7 +114,7 @@ class TheorySep : public Theory {
   TrustNode explain(TNode n) override;
 
  public:
-  void addSharedTerm(TNode t) override;
+  void notifySharedTerm(TNode t) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   void computeCareGraph() override;
 
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 647a7bb47..63ebacc23 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -88,9 +88,7 @@ void TheorySets::finishInit()
   d_internal->finishInit();
 }
 
-void TheorySets::addSharedTerm(TNode n) {
-  d_internal->addSharedTerm(n);
-}
+void TheorySets::notifySharedTerm(TNode n) { d_internal->addSharedTerm(n); }
 
 void TheorySets::check(Effort e) {
   if (done() && e < Theory::EFFORT_FULL) {
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 9e04b89a7..a7fb31dab 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -58,7 +58,7 @@ class TheorySets : public Theory
   void finishInit() override;
   //--------------------------------- end initialization
 
-  void addSharedTerm(TNode) override;
+  void notifySharedTerm(TNode) override;
   void check(Effort) override;
   bool collectModelInfo(TheoryModel* m) override;
   void computeCareGraph() override;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index e42796354..0de0cc33c 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -153,15 +153,16 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
   return false;
 }
 
-void TheoryStrings::addSharedTerm(TNode t) {
-  Debug("strings") << "TheoryStrings::addSharedTerm(): "
-                     << t << " " << t.getType().isBoolean() << endl;
+void TheoryStrings::notifySharedTerm(TNode t)
+{
+  Debug("strings") << "TheoryStrings::notifySharedTerm(): " << t << " "
+                   << t.getType().isBoolean() << endl;
   d_equalityEngine->addTriggerTerm(t, THEORY_STRINGS);
   if (options::stringExp())
   {
     d_esolver.addSharedTerm(t);
   }
-  Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl;
+  Debug("strings") << "TheoryStrings::notifySharedTerm() finished" << std::endl;
 }
 
 EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 8a1afe6b3..f4aa0675c 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -96,7 +96,7 @@ class TheoryStrings : public Theory {
   /** shutdown */
   void shutdown() override {}
   /** add shared term */
-  void addSharedTerm(TNode n) override;
+  void notifySharedTerm(TNode n) override;
   /** get equality status */
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   /** preregister term */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 7220e2e1c..f65a7c45c 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -44,8 +44,6 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){
     os << "EFFORT_STANDARD"; break;
   case Theory::EFFORT_FULL:
     os << "EFFORT_FULL"; break;
-  case Theory::EFFORT_COMBINATION:
-    os << "EFFORT_COMBINATION"; break;
   case Theory::EFFORT_LAST_CALL:
     os << "EFFORT_LAST_CALL"; break;
   default:
@@ -109,9 +107,11 @@ void Theory::setEqualityEngine(eq::EqualityEngine* ee)
     d_theoryState->setEqualityEngine(ee);
   }
 }
+
 void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
 {
   Assert(d_quantEngine == nullptr);
+  // quantifiers engine may be null if not in quantified logic
   d_quantEngine = qe;
 }
 
@@ -266,11 +266,15 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
   return tid;
 }
 
-void Theory::addSharedTermInternal(TNode n) {
-  Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
-  Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
-  d_sharedTerms.push_back(n);
-  addSharedTerm(n);
+void Theory::notifySharedTerm(TNode n)
+{
+  // TODO (project #39): this will move to addSharedTerm, as every theory with
+  // an equality does this in their notifySharedTerm method.
+  // if we have an equality engine, add the trigger term
+  if (d_equalityEngine != nullptr)
+  {
+    d_equalityEngine->addTriggerTerm(n, d_id);
+  }
 }
 
 void Theory::computeCareGraph() {
@@ -394,17 +398,23 @@ void Theory::computeRelevantTermsInternal(std::set<Node>& termSet,
   // Collect all terms appearing in assertions
   irrKinds.insert(kind::EQUAL);
   irrKinds.insert(kind::NOT);
-  context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
-  for (; assert_it != assert_it_end; ++assert_it) {
+  context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
+                                             assert_it_end = facts_end();
+  for (; assert_it != assert_it_end; ++assert_it)
+  {
     collectTerms(*assert_it, irrKinds, termSet);
   }
 
-  if (!includeShared) return;
-
+  if (!includeShared)
+  {
+    return;
+  }
   // Add terms that are shared terms
-  set<Kind> kempty;
-  context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
-  for (; shared_it != shared_it_end; ++shared_it) {
+  std::set<Kind> kempty;
+  context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(),
+                                         shared_it_end = shared_terms_end();
+  for (; shared_it != shared_it_end; ++shared_it)
+  {
     collectTerms(*shared_it, kempty, termSet);
   }
 }
@@ -474,6 +484,110 @@ void Theory::getCareGraph(CareGraph* careGraph) {
   d_careGraph = NULL;
 }
 
+EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
+{
+  // if not using an equality engine, then by default we don't know the status
+  if (d_equalityEngine == nullptr)
+  {
+    return EQUALITY_UNKNOWN;
+  }
+  Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
+
+  // Check for equality (simplest)
+  if (d_equalityEngine->areEqual(a, b))
+  {
+    // The terms are implied to be equal
+    return EQUALITY_TRUE;
+  }
+
+  // Check for disequality
+  if (d_equalityEngine->areDisequal(a, b, false))
+  {
+    // The terms are implied to be dis-equal
+    return EQUALITY_FALSE;
+  }
+
+  // All other terms are unknown, which is conservative. A theory may override
+  // this method if it knows more information.
+  return EQUALITY_UNKNOWN;
+}
+
+void Theory::check(Effort level)
+{
+  // see if we are already done (as an optimization)
+  if (done() && level < EFFORT_FULL)
+  {
+    return;
+  }
+  Assert(d_theoryState!=nullptr);
+  // standard calls for resource, stats
+  d_out->spendResource(ResourceManager::Resource::TheoryCheckStep);
+  TimerStat::CodeTimer checkTimer(d_checkTime);
+  // pre-check at level
+  if (preCheck(level))
+  {
+    // check aborted for a theory-specific reason
+    return;
+  }
+  // process the pending fact queue
+  while (!done() && !d_theoryState->isInConflict())
+  {
+    // Get the next assertion from the fact queue
+    Assertion assertion = get();
+    TNode fact = assertion.d_assertion;
+    bool polarity = fact.getKind() != kind::NOT;
+    TNode atom = polarity ? fact : fact[0];
+    // call the pre-notify method
+    if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered))
+    {
+      // handled in theory-specific way that doesn't involve equality engine
+      continue;
+    }
+    // Theories that don't have an equality engine should always return true
+    // for preNotifyFact
+    Assert(d_equalityEngine != nullptr);
+    // assert to the equality engine
+    if (atom.getKind() == kind::EQUAL)
+    {
+      d_equalityEngine->assertEquality(atom, polarity, fact);
+    }
+    else
+    {
+      d_equalityEngine->assertPredicate(atom, polarity, fact);
+    }
+    // notify the theory of the new fact, which is not internal
+    notifyFact(atom, polarity, fact, false);
+  }
+  // post-check at level
+  postCheck(level);
+}
+
+bool Theory::preCheck(Effort level) { return false; }
+
+void Theory::postCheck(Effort level) {}
+
+bool Theory::preNotifyFact(TNode atom, bool polarity, TNode fact, bool isPrereg)
+{
+  return false;
+}
+
+void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal)
+{
+}
+
+void Theory::preRegisterTerm(TNode node) {}
+
+void Theory::addSharedTerm(TNode n)
+{
+  Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")"
+                   << std::endl;
+  Debug("theory::assertions")
+      << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
+  d_sharedTerms.push_back(n);
+  // now call theory-specific method notifySharedTerm
+  notifySharedTerm(n);
+}
+
 eq::EqualityEngine* Theory::getEqualityEngine()
 {
   // get the assigned equality engine, which is a pointer stored in this class
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 349f36a57..8ea64e724 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -138,9 +138,6 @@ class Theory {
   /** Index into the head of the facts list */
   context::CDO<unsigned> d_factsHead;
 
-  /** Add shared term to the theory. */
-  void addSharedTermInternal(TNode node);
-
   /** Indices for splitting on the shared terms. */
   context::CDO<unsigned> d_sharedTermsIndex;
 
@@ -184,7 +181,7 @@ class Theory {
    */
   context::CDList<TNode> d_sharedTerms;
 
-  //---------------------------------- collect model info
+  //---------------------------------- private collect model info
   /**
    * Scans the current set of assertions and shared terms top-down
    * until a theory-leaf is reached, and adds all terms found to
@@ -207,21 +204,7 @@ class Theory {
   void collectTerms(TNode n,
                     std::set<Kind>& irrKinds,
                     std::set<Node>& termSet) const;
-  /**
-   * Same as above, but with empty irrKinds. This version can be overridden
-   * by the theory, e.g. by restricting or extending the set of terms returned
-   * by computeRelevantTermsInternal, which is called by default with no
-   * irrKinds.
-   */
-  virtual void computeRelevantTerms(std::set<Node>& termSet,
-                                    bool includeShared = true);
-  /**
-   * Collect model values, after equality information is added to the model.
-   * The argument termSet is the set of relevant terms returned by
-   * computeRelevantTerms.
-   */
-  virtual bool collectModelValues(TheoryModel* m, std::set<Node>& termSet);
-  //---------------------------------- end collect model info
+  //---------------------------------- end private collect model info
 
   /**
    * Construct a Theory.
@@ -334,6 +317,16 @@ class Theory {
   virtual void finishInit() {}
   //--------------------------------- end private initialization
 
+  /**
+   * This method is called to notify a theory that the node n should
+   * be considered a "shared term" by this theory. This does anything
+   * theory-specific concerning the fact that n is now marked as a shared
+   * term, which is done in addition to explicitly storing n as a shared
+   * term and adding it as a trigger term in the equality engine of this
+   * class (see addSharedTerm).
+   */
+  virtual void notifySharedTerm(TNode n);
+
  public:
   //--------------------------------- initialization
   /**
@@ -435,25 +428,23 @@ class Theory {
    * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
    * with FULL_EFFORT.
    */
-  enum Effort {
+  enum Effort
+  {
     /**
      * Standard effort where theory need not do anything
      */
     EFFORT_STANDARD = 50,
     /**
-     * Full effort requires the theory make sure its assertions are satisfiable or not
+     * Full effort requires the theory make sure its assertions are satisfiable
+     * or not
      */
     EFFORT_FULL = 100,
     /**
-     * Combination effort means that the individual theories are already satisfied, and
-     * it is time to put some effort into propagation of shared term equalities
-     */
-    EFFORT_COMBINATION = 150,
-    /**
-     * Last call effort, reserved for quantifiers.
+     * Last call effort, called after theory combination has completed with
+     * no lemmas and a model is available.
      */
     EFFORT_LAST_CALL = 200
-  };/* enum Effort */
+  }; /* enum Effort */
 
   static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION
     { return e >= EFFORT_STANDARD; }
@@ -461,8 +452,6 @@ class Theory {
     { return e >= EFFORT_STANDARD && e <  EFFORT_FULL; }
   static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION
     { return e == EFFORT_FULL; }
-  static inline bool combination(Effort e) CVC4_CONST_FUNCTION
-    { return e == EFFORT_COMBINATION; }
 
   /**
    * Get the id for this Theory.
@@ -506,6 +495,9 @@ class Theory {
     return d_valuation;
   }
 
+  /** Get the equality engine being used by this theory. */
+  eq::EqualityEngine* getEqualityEngine();
+
   /**
    * Get the quantifiers engine associated to this theory.
    */
@@ -513,13 +505,6 @@ class Theory {
     return d_quantEngine;
   }
 
-  /**
-   * Get the quantifiers engine associated to this theory (const version).
-   */
-  const QuantifiersEngine* getQuantifiersEngine() const {
-    return d_quantEngine;
-  }
-
   /** Get the decision manager associated to this theory. */
   DecisionManager* getDecisionManager() { return d_decManager; }
 
@@ -559,7 +544,7 @@ class Theory {
   /**
    * Pre-register a term.  Done one time for a Node per SAT context level.
    */
-  virtual void preRegisterTerm(TNode) { }
+  virtual void preRegisterTerm(TNode);
 
   /**
    * Assert a fact in the current context.
@@ -571,16 +556,8 @@ class Theory {
     d_facts.push_back(Assertion(assertion, isPreregistered));
   }
 
-  /**
-   * This method is called to notify a theory that the node n should
-   * be considered a "shared term" by this theory
-   */
-  virtual void addSharedTerm(TNode n) { }
-
-  /**
-   * Get the official equality engine of this theory.
-   */
-  eq::EqualityEngine* getEqualityEngine();
+  /** Add shared term to the theory. */
+  void addSharedTerm(TNode node);
 
   /**
    * Return the current theory care graph. Theories should overload
@@ -593,31 +570,17 @@ class Theory {
    * Return the status of two terms in the current context. Should be
    * implemented in sub-theories to enable more efficient theory-combination.
    */
-  virtual EqualityStatus getEqualityStatus(TNode a, TNode b) {
-    return EQUALITY_UNKNOWN;
-  }
+  virtual EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   /**
    * Return the model value of the give shared term (or null if not available).
-   */
-  virtual Node getModelValue(TNode var) { return Node::null(); }
-
-  /**
-   * Check the current assignment's consistency.
    *
-   * An implementation of check() is required to either:
-   * - return a conflict on the output channel,
-   * - be interrupted,
-   * - throw an exception
-   * - or call get() until done() is true.
+   * TODO (project #39): this method is likely to become deprecated.
    */
-  virtual void check(Effort level = EFFORT_FULL) { }
-
-  /** Needs last effort check? */
-  virtual bool needsCheckLastEffort() { return false; }
+  virtual Node getModelValue(TNode var) { return Node::null(); }
 
   /** T-propagate new literal assignments in the current context. */
-  virtual void propagate(Effort level = EFFORT_FULL) { }
+  virtual void propagate(Effort level = EFFORT_FULL) {}
 
   /**
    * Return an explanation for the literal represented by parameter n
@@ -630,6 +593,74 @@ class Theory {
                        "Theory::explain() interface!";
   }
 
+  //--------------------------------- check
+  /**
+   * Does this theory wish to be called to check at last call effort? This is
+   * the case for any theory that wishes to run when a model is available.
+   */
+  virtual bool needsCheckLastEffort() { return false; }
+  /**
+   * Check the current assignment's consistency.
+   *
+   * An implementation of check() is required to either:
+   * - return a conflict on the output channel,
+   * - be interrupted,
+   * - throw an exception
+   * - or call get() until done() is true.
+   *
+   * The standard method for check consists of a loop that processes the entire
+   * fact queue when preCheck returns false. It makes four theory-specific
+   * callbacks, (preCheck, postCheck, preNotifyFact, notifyFact) as described
+   * below. It asserts each fact to the official equality engine when
+   * preNotifyFact returns false.
+   *
+   * Theories that use this check method must use an official theory
+   * state object (d_theoryState).
+   *
+   * TODO (project #39): this method should be non-virtual, once all theories
+   * conform to the new standard
+   */
+  virtual void check(Effort level = EFFORT_FULL);
+  /**
+   * Pre-check, called before the fact queue of the theory is processed.
+   * If this method returns false, then the theory will process its fact
+   * queue. If this method returns true, then the theory has indicated
+   * its check method should finish immediately.
+   */
+  virtual bool preCheck(Effort level = EFFORT_FULL);
+  /**
+   * Post-check, called after the fact queue of the theory is processed.
+   */
+  virtual void postCheck(Effort level = EFFORT_FULL);
+  /**
+   * Pre-notify fact, return true if the theory processed it. If this
+   * method returns false, then the atom will be added to the equality engine
+   * of the theory and notifyFact will be called with isInternal=false.
+   *
+   * Theories that implement check but do not use official equality
+   * engines should always return true for this method.
+   *
+   * @param atom The atom
+   * @param polarity Its polarity
+   * @param fact The original literal that was asserted
+   * @param isPrereg Whether the assertion is preregistered
+   * @return true if the theory completely processed this fact, i.e. it does
+   * not need to assert the fact to its equality engine.
+   */
+  virtual bool preNotifyFact(TNode atom, bool pol, TNode fact, bool isPrereg);
+  /**
+   * Notify fact, called immediately after the fact was pushed into the
+   * equality engine.
+   *
+   * @param atom The atom
+   * @param polarity Its polarity
+   * @param fact The original literal that was asserted
+   * @param isInternal Whether the origin of the fact was internal
+   */
+  virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal);
+  //--------------------------------- end check
+
+  //--------------------------------- collect model info
   /**
    * Get all relevant information in this theory regarding the current
    * model.  This should be called after a call to check( FULL_EFFORT )
@@ -637,10 +668,34 @@ class Theory {
    *
    * This method returns true if and only if the equality engine of m is
    * consistent as a result of this call.
+   *
+   * The standard method for collectModelInfo computes the relevant terms,
+   * asserts the theory's equality engine to the model (if necessary) and
+   * then calls computeModelValues.
+   *
+   * TODO (project #39): this method should be non-virtual, once all theories
+   * conform to the new standard
    */
   virtual bool collectModelInfo(TheoryModel* m);
+  /**
+   * Same as above, but with empty irrKinds. This version can be overridden
+   * by the theory, e.g. by restricting or extending the set of terms returned
+   * by computeRelevantTermsInternal, which is called by default with no
+   * irrKinds.
+   */
+  virtual void computeRelevantTerms(std::set<Node>& termSet,
+                                    bool includeShared = true);
+  /**
+   * Collect model values, after equality information is added to the model.
+   * The argument termSet is the set of relevant terms returned by
+   * computeRelevantTerms.
+   */
+  virtual bool collectModelValues(TheoryModel* m, std::set<Node>& termSet);
   /** if theories want to do something with model after building, do it here */
   virtual void postProcessModel( TheoryModel* m ){ }
+  //--------------------------------- end collect model info
+
+  //--------------------------------- preprocessing
   /**
    * Statically learn from assertion "in," which has been asserted
    * true at the top level.  The theory should only add (via
@@ -681,6 +736,7 @@ class Theory {
    * preprocessing before they are asserted to theory engine.
    */
   virtual void ppNotifyAssertions(const std::vector<Node>& assertions) {}
+  //--------------------------------- end preprocessing
 
   /**
    * A Theory is called with presolve exactly one time per user
@@ -941,7 +997,6 @@ class Theory {
 
   /** Turn on proof-production mode. */
   void produceProofs() { d_proofsEnabled = true; }
-
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b88b6158e..cf29039ff 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1219,7 +1219,7 @@ void TheoryEngine::assertFact(TNode literal)
         Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term);
         for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) {
           if (Theory::setContains(id, theories)) {
-            theoryOf(id)->addSharedTermInternal(term);
+            theoryOf(id)->addSharedTerm(term);
           }
         }
         d_sharedTerms.markNotified(term, theories);
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 29014d33f..7d554c613 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -503,7 +503,8 @@ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
   return EQUALITY_FALSE_IN_MODEL;
 }
 
-void TheoryUF::addSharedTerm(TNode t) {
+void TheoryUF::notifySharedTerm(TNode t)
+{
   Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
   d_equalityEngine->addTriggerTerm(t, THEORY_UF);
 }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 8efaf79e3..916c6ef6b 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -184,7 +184,7 @@ private:
   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
   void presolve() override;
 
-  void addSharedTerm(TNode n) override;
+  void notifySharedTerm(TNode n) override;
   void computeCareGraph() override;
 
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;