Standardization of Theory (#5181)

This cleans up various interfaces of Theory now that all theories have been updated to the new standard. This includes making check non-virtual, standardizing when trigger terms are added to equality engines, and simplifications for collectModelInfo.

16 files changed, 47 insertions, 131 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 465128b1b..f2db70d90 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -477,10 +477,6 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
   d_ee->assertEquality(eq, true, reason);
 }
 
-void ArithCongruenceManager::addSharedTerm(Node x){
-  d_ee->addTriggerTerm(x, THEORY_ARITH);
-}
-
 bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; }
 
 std::vector<Node> andComponents(TNode an)
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 6115fec8a..44a2b9df6 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -217,9 +217,6 @@ public:
   void equalsConstant(ConstraintCP eq);
   void equalsConstant(ConstraintCP lb, ConstraintCP ub);
 
-
-  void addSharedTerm(Node x);
-
  private:
   class Statistics {
   public:
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 434d2e1c8..bddc8ebcc 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -219,12 +219,9 @@ void TheoryArith::propagate(Effort e) {
   d_internal->propagate(e);
 }
 
-bool TheoryArith::collectModelInfo(TheoryModel* m)
+bool TheoryArith::collectModelInfo(TheoryModel* m,
+                                   const std::set<Node>& termSet)
 {
-  std::set<Node> termSet;
-  // Work out which variables are needed
-  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
-  computeAssertedTerms(termSet, irrKinds);
   // this overrides behavior to not assert equality engine
   return collectModelValues(m, termSet);
 }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 8555156a5..6b279c9ed 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -91,7 +91,7 @@ class TheoryArith : public Theory {
   void propagate(Effort e) override;
   TrustNode explain(TNode n) override;
 
-  bool collectModelInfo(TheoryModel* m) override;
+  bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet) override;
   /**
    * Collect model values in m based on the relevant terms given by termSet.
    */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 557072319..bb6ab0b9c 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1076,7 +1076,6 @@ void TheoryArithPrivate::notifySharedTerm(TNode n)
   if(n.isConst()){
     d_partialModel.invalidateDelta();
   }
-  d_congruenceManager.addSharedTerm(n);
   if(!n.isConst() && !isSetup(n)){
     Polynomial poly = Polynomial::parsePolynomial(n);
     Polynomial::iterator it = poly.begin();
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 5dee75a6c..3270c1c07 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -852,7 +852,6 @@ 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/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 857d4d6fb..79a20c9c9 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -209,11 +209,6 @@ TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
 void TheoryBV::notifySharedTerm(TNode t)
 {
   d_internal->notifySharedTerm(t);
-  // temporary, will be built into Theory::addSharedTerm
-  if (d_equalityEngine != nullptr)
-  {
-    d_equalityEngine->addTriggerTerm(t, THEORY_BV);
-  }
 }
 
 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 863f9a5a6..037b083f4 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -1019,12 +1019,9 @@ Node TheoryFp::getModelValue(TNode var) {
   return d_conv.getValue(d_valuation, var);
 }
 
-bool TheoryFp::collectModelInfo(TheoryModel* m)
+bool TheoryFp::collectModelInfo(TheoryModel* m,
+                                const std::set<Node>& relevantTerms)
 {
-  std::set<Node> relevantTerms;
-  // Work out which variables are needed
-  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
-  computeAssertedTerms(relevantTerms, irrKinds);
   // this override behavior to not assert equality engine
   return collectModelValues(m, relevantTerms);
 }
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 16d984011..42c009893 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -75,7 +75,8 @@ class TheoryFp : public Theory {
   //--------------------------------- end standard check
 
   Node getModelValue(TNode var) override;
-  bool collectModelInfo(TheoryModel* m) override;
+  bool collectModelInfo(TheoryModel* m,
+                        const std::set<Node>& relevantTerms) override;
   /** Collect model values in m based on the relevant terms given by
    * relevantTerms */
   bool collectModelValues(TheoryModel* m,
diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp
index 5ea2799c5..7d121af53 100644
--- a/src/theory/model_manager_distributed.cpp
+++ b/src/theory/model_manager_distributed.cpp
@@ -78,7 +78,12 @@ bool ModelManagerDistributed::prepareModel()
     Theory* t = d_te.theoryOf(theoryId);
     Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId
                            << std::endl;
-    if (!t->collectModelInfo(d_model))
+    // collect the asserted terms
+    std::set<Node> termSet;
+    collectAssertedTerms(theoryId, termSet);
+    // also get relevant terms
+    t->computeRelevantTerms(termSet);
+    if (!t->collectModelInfo(d_model, termSet))
     {
       Trace("model-builder")
           << "ModelManagerDistributed: fail collect model info" << std::endl;
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 1a0b1b1e2..51f49ad1d 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1275,7 +1275,6 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
       d_equalityEngine->addTriggerPredicate(node);
     }
     break;
-    case kind::CARD: d_equalityEngine->addTriggerTerm(node, THEORY_SETS); break;
     default: d_equalityEngine->addTerm(node); break;
   }
 }
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 309b85503..0375fd311 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -163,7 +163,6 @@ 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);
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index cdcec52e3..2a471ec0d 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -273,13 +273,7 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
 
 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);
-  }
+  // do nothing
 }
 
 void Theory::computeCareGraph() {
@@ -357,18 +351,8 @@ std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() cons
   return currentlyShared;
 }
 
-bool Theory::collectModelInfo(TheoryModel* m)
+bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet)
 {
-  // NOTE: the computation of termSet will be moved to model manager
-  // and passed as an argument to collectModelInfo.
-  std::set<Node> termSet;
-  // Compute terms appearing in assertions and shared terms
-  TheoryModel* tm = d_valuation.getModel();
-  Assert(tm != nullptr);
-  const std::set<Kind>& irrKinds = tm->getIrrelevantKinds();
-  computeAssertedTerms(termSet, irrKinds, true);
-  // Compute additional relevant terms (theory-specific)
-  computeRelevantTerms(termSet);
   // if we are using an equality engine, assert it to the model
   if (d_equalityEngine != nullptr)
   {
@@ -381,54 +365,6 @@ bool Theory::collectModelInfo(TheoryModel* m)
   return collectModelValues(m, termSet);
 }
 
-void Theory::collectTerms(TNode n,
-                          const std::set<Kind>& irrKinds,
-                          set<Node>& termSet) const
-{
-  if (termSet.find(n) != termSet.end()) {
-    return;
-  }
-  Kind nk = n.getKind();
-  if (irrKinds.find(nk) == irrKinds.end())
-  {
-    Trace("theory::collectTerms")
-        << "Theory::collectTerms: adding " << n << endl;
-    termSet.insert(n);
-  }
-  if (nk == kind::NOT || nk == kind::EQUAL || !isLeaf(n))
-  {
-    for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
-      collectTerms(*child_it, irrKinds, termSet);
-    }
-  }
-}
-
-void Theory::computeAssertedTerms(std::set<Node>& termSet,
-                                  const std::set<Kind>& irrKinds,
-                                  bool includeShared) const
-{
-  // Collect all terms appearing in assertions
-  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;
-  }
-  // Add terms that are shared terms
-  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);
-  }
-}
-
 void Theory::computeRelevantTerms(std::set<Node>& termSet)
 {
   // by default, there are no additional relevant terms
@@ -532,18 +468,24 @@ void Theory::check(Effort level)
   // standard calls for resource, stats
   d_out->spendResource(ResourceManager::Resource::TheoryCheckStep);
   TimerStat::CodeTimer checkTimer(d_checkTime);
+  Trace("theory-check") << "Theory::preCheck " << level << " " << d_id
+                        << std::endl;
   // pre-check at level
   if (preCheck(level))
   {
     // check aborted for a theory-specific reason
     return;
   }
+  Assert(d_theoryState != nullptr);
+  Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl;
   // 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;
+    Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id
+                          << std::endl;
     bool polarity = fact.getKind() != kind::NOT;
     TNode atom = polarity ? fact : fact[0];
     // call the pre-notify method
@@ -552,6 +494,8 @@ void Theory::check(Effort level)
       // handled in theory-specific way that doesn't involve equality engine
       continue;
     }
+    Trace("theory-check") << "Theory::assert " << fact << " " << d_id
+                          << std::endl;
     // Theories that don't have an equality engine should always return true
     // for preNotifyFact
     Assert(d_equalityEngine != nullptr);
@@ -564,11 +508,15 @@ void Theory::check(Effort level)
     {
       d_equalityEngine->assertPredicate(atom, polarity, fact);
     }
+    Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id
+                          << std::endl;
     // notify the theory of the new fact, which is not internal
     notifyFact(atom, polarity, fact, false);
   }
+  Trace("theory-check") << "Theory::postCheck " << d_id << std::endl;
   // post-check at level
   postCheck(level);
+  Trace("theory-check") << "Theory::finish check " << d_id << std::endl;
 }
 
 bool Theory::preCheck(Effort level) { return false; }
@@ -596,6 +544,11 @@ void Theory::addSharedTerm(TNode n)
   d_sharedTerms.push_back(n);
   // now call theory-specific method notifySharedTerm
   notifySharedTerm(n);
+  // if we have an equality engine, add the trigger term
+  if (d_equalityEngine != nullptr)
+  {
+    d_equalityEngine->addTriggerTerm(n, d_id);
+  }
 }
 
 eq::EqualityEngine* Theory::getEqualityEngine()
diff --git a/src/theory/theory.h b/src/theory/theory.h
index bc6c995a7..6f6c863df 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -179,15 +179,6 @@ class Theory {
    */
   context::CDList<TNode> d_sharedTerms;
 
-  //---------------------------------- private collect model info
-  /**
-   * Helper function for computeRelevantTerms
-   */
-  void collectTerms(TNode n,
-                    const std::set<Kind>& irrKinds,
-                    std::set<Node>& termSet) const;
-  //---------------------------------- end private collect model info
-
   /**
    * Construct a Theory.
    *
@@ -492,6 +483,16 @@ class Theory {
   DecisionManager* getDecisionManager() { return d_decManager; }
 
   /**
+   * @return The theory state associated with this theory.
+   */
+  TheoryState* getTheoryState() { return d_theoryState; }
+
+  /**
+   * @return The theory inference manager associated with this theory.
+   */
+  TheoryInferenceManager* getInferenceManager() { return d_inferManager; }
+
+  /**
    * Expand definitions in the term node. This returns a term that is
    * equivalent to node. It wraps this term in a TrustNode of kind
    * TrustNodeKind::REWRITE. If node is unchanged by this method, the
@@ -600,11 +601,8 @@ class Theory {
    *
    * 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);
+  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
@@ -662,28 +660,9 @@ class Theory {
    * 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);
-  /**
-   * Scans the current set of assertions and shared terms top-down
-   * until a theory-leaf is reached, and adds all terms found to
-   * termSet.  This is used by collectModelInfo to delimit the set of
-   * terms that should be used when constructing a model.
-   *
-   * @param irrKinds The kinds of terms that appear in assertions that should *not*
-   * be included in termSet. Note that the kinds EQUAL and NOT are always
-   * treated as irrelevant kinds.
-   *
-   * @param includeShared Whether to include shared terms in termSet. Notice that
-   * shared terms are not influenced by irrKinds.
-   *
-   * TODO (project #39): this method will be deleted. The version in
-   * model manager will be used.
+   * conform to the new standard, delete, move to model manager distributed.
    */
-  void computeAssertedTerms(std::set<Node>& termSet,
-                            const std::set<Kind>& irrKinds,
-                            bool includeShared = true) const;
+  virtual bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet);
   /**
    * Compute terms that are not necessarily part of the assertions or
    * shared terms that should be considered relevant, add them to termSet.
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 94477d1e8..2d0a80599 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -444,7 +444,7 @@ bool TheoryModel::assertPredicate(TNode a, bool polarity)
 
 /** assert equality engine */
 bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee,
-                                       set<Node>* termSet)
+                                       const std::set<Node>* termSet)
 {
   Assert(d_equalityEngine->consistent());
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 00b2107bd..b1401c074 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -110,7 +110,7 @@ public:
    * is consistent after asserting the equality engine to this model.
    */
   bool assertEqualityEngine(const eq::EqualityEngine* ee,
-                            std::set<Node>* termSet = NULL);
+                            const std::set<Node>* termSet = NULL);
   /** assert skeleton
    *
    * This method gives a "skeleton" for the model value of the equivalence