Minor cleanup of quantifiers engine (#4994)

Eventually, QuanitifersEngine should not depend on TheoryEngine. This is a first step in this direction. It eliminates some uses of TheoryEngine and eliminates a unnecessary friend relationship between quantifiers::TermDb and TheoryEngine. Further refactoring will be done in future PRs.

1 files changed, 19 insertions, 9 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 6e5dca4ef..bac67c7b6 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1091,15 +1091,25 @@ bool TermDb::reset( Theory::Effort effort ){
       }
       ++eqcs_i;
     }
-    for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
-      Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId];
-      if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) {
-        context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
-        for (unsigned i = 0; it != it_end; ++ it, ++i) {
-          if ((*it).d_assertion.getKind() != INST_CLOSURE)
-          {
-            setHasTerm((*it).d_assertion);
-          }
+    TheoryEngine* te = d_quantEngine->getTheoryEngine();
+    const LogicInfo& logicInfo = te->getLogicInfo();
+    for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
+    {
+      if (!logicInfo.isTheoryEnabled(theoryId))
+      {
+        continue;
+      }
+      Theory* theory = te->theoryOf(theoryId);
+      Assert(theory != nullptr);
+      for (context::CDList<Assertion>::const_iterator
+               it = theory->facts_begin(),
+               it_end = theory->facts_end();
+           it != it_end;
+           ++it)
+      {
+        if ((*it).d_assertion.getKind() != INST_CLOSURE)
+        {
+          setHasTerm((*it).d_assertion);
         }
       }
     }