Use standard equality engine information in quantifiers state (#5824)

This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.

This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.

1 files changed, 9 insertions, 1 deletions

diff --git a/src/theory/ee_setup_info.h b/src/theory/ee_setup_info.h
index 78f2f211e..7770cfc49 100644
--- a/src/theory/ee_setup_info.h
+++ b/src/theory/ee_setup_info.h
@@ -37,13 +37,21 @@ class EqualityEngineNotify;
  */
 struct EeSetupInfo
 {
-  EeSetupInfo() : d_notify(nullptr), d_constantsAreTriggers(true) {}
+  EeSetupInfo()
+      : d_notify(nullptr), d_constantsAreTriggers(true), d_useMaster(false)
+  {
+  }
   /** The notification class of the theory */
   eq::EqualityEngineNotify* d_notify;
   /** The name of the equality engine */
   std::string d_name;
   /** Constants are triggers */
   bool d_constantsAreTriggers;
+  /**
+   * Whether we want our state to use the master equality engine. This should
+   * be true exclusively for the theory of quantifiers.
+   */
+  bool d_useMaster;
 };
 
 }  // namespace theory