Add term db mode. Minor changes to quantifiers rewriter: split ITE's where equality resolution is possible on condition, pull nested quantifiers from ITE branches. Minor cleanup.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e589e8f87..136c0409f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -83,6 +83,10 @@ namespace theory {
     class EqualityEngine;
   }/* CVC4::theory::eq namespace */
 
+  namespace quantifiers {
+    class TermDb;
+  }
+
   class EntailmentCheckParameters;
   class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
@@ -101,6 +105,7 @@ class TheoryEngine {
 
   /** Shared terms database can use the internals notify the theories */
   friend class SharedTermsDatabase;
+  friend class theory::quantifiers::TermDb;
 
   /** Associated PropEngine engine */
   prop::PropEngine* d_propEngine;