1 files changed, 128 insertions, 14 deletions

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