Move master equality engine notification to own file (#6877)

Preparation for central equality engine.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 95b6f401e607b94171247fcaa1106db3d8399417..8053ba25e86dc17f86c0248ef7a78b15e289d979 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -797,6 +797,8 @@ libcvc5_add_sources(
   theory/quantifiers/instantiation_list.h
   theory/quantifiers/lazy_trie.cpp
   theory/quantifiers/lazy_trie.h
+  theory/quantifiers/master_eq_notify.cpp
+  theory/quantifiers/master_eq_notify.h
   theory/quantifiers/proof_checker.cpp
   theory/quantifiers/proof_checker.h
   theory/quantifiers/quant_bound_inference.cpp

diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp
index 384bace159223f963daa338d6f7a0b61deaf8317..7e4932767e13d2d346fc4f9cafa9db2026405f73 100644 (file)
--- a/src/theory/ee_manager_distributed.cpp
+++ b/src/theory/ee_manager_distributed.cpp
@@ -56,7 +56,7 @@ void EqEngineManagerDistributed::initializeTheories()
     Assert(d_masterEqualityEngine == nullptr);
     QuantifiersEngine* qe = d_te.getQuantifiersEngine();
     Assert(qe != nullptr);
-    d_masterEENotify.reset(new MasterNotifyClass(qe));
+    d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe));
     d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
                                                         d_te.getSatContext(),
                                                         "theory::master",
@@ -109,11 +109,5 @@ void EqEngineManagerDistributed::notifyModel(bool incomplete)
   }
 }
 
-void EqEngineManagerDistributed::MasterNotifyClass::eqNotifyNewClass(TNode t)
-{
-  // adds t to the quantifiers term database
-  d_quantEngine->eqNotifyNewClass(t);
-}
-
 }  // namespace theory
 }  // namespace cvc5

diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h
index 0bf184a579846afcaaa9e26e42e3494791b65c7e..8c7bb261802f7b71830270d680c91355f1839ab2 100644 (file)
--- a/src/theory/ee_manager_distributed.h
+++ b/src/theory/ee_manager_distributed.h
@@ -22,6 +22,7 @@
 #include <memory>
 
 #include "theory/ee_manager.h"
+#include "theory/quantifiers/master_eq_notify.h"
 
 namespace cvc5 {
 namespace theory {
@@ -59,38 +60,8 @@ class EqEngineManagerDistributed : public EqEngineManager
   void notifyModel(bool incomplete) override;
 
  private:
-  /** notify class for master equality engine */
-  class MasterNotifyClass : public theory::eq::EqualityEngineNotify
-  {
-   public:
-    MasterNotifyClass(QuantifiersEngine* qe) : d_quantEngine(qe) {}
-    /**
-     * Called when a new equivalence class is created in the master equality
-     * engine.
-     */
-    void eqNotifyNewClass(TNode t) override;
-
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
-    {
-      return true;
-    }
-    bool eqNotifyTriggerTermEquality(TheoryId tag,
-                                     TNode t1,
-                                     TNode t2,
-                                     bool value) override
-    {
-      return true;
-    }
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
-    void eqNotifyMerge(TNode t1, TNode t2) override {}
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
-
-   private:
-    /** Pointer to quantifiers engine */
-    QuantifiersEngine* d_quantEngine;
-  };
   /** The master equality engine notify class */
-  std::unique_ptr<MasterNotifyClass> d_masterEENotify;
+  std::unique_ptr<quantifiers::MasterNotifyClass> d_masterEENotify;
   /** The master equality engine. */
   std::unique_ptr<eq::EqualityEngine> d_masterEqualityEngine;
   /** The equality engine of the shared solver / shared terms database. */

diff --git a/src/theory/quantifiers/master_eq_notify.cpp b/src/theory/quantifiers/master_eq_notify.cpp
new file mode 100644 (file)
index 0000000..7aaec56
--- /dev/null
+++ b/src/theory/quantifiers/master_eq_notify.cpp
@@ -0,0 +1,34 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Notification class for the master equality engine
+ */
+
+#include "theory/quantifiers/master_eq_notify.h"
+
+#include "theory/quantifiers_engine.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+MasterNotifyClass::MasterNotifyClass(QuantifiersEngine* qe) : d_quantEngine(qe) {}
+
+void MasterNotifyClass::eqNotifyNewClass(TNode t)
+{
+  d_quantEngine->eqNotifyNewClass(t);
+}
+
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5

diff --git a/src/theory/quantifiers/master_eq_notify.h b/src/theory/quantifiers/master_eq_notify.h
new file mode 100644 (file)
index 0000000..262ec48
--- /dev/null
+++ b/src/theory/quantifiers/master_eq_notify.h
@@ -0,0 +1,68 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Notification class for the master equality engine
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__MASTER_EQ_NOTIFY__H
+#define CVC5__THEORY__QUANTIFIERS__MASTER_EQ_NOTIFY__H
+
+#include <memory>
+
+#include "theory/uf/equality_engine_notify.h"
+
+namespace cvc5 {
+namespace theory {
+  
+class QuantifiersEngine;
+
+namespace quantifiers {
+
+/** notify class for master equality engine */
+class MasterNotifyClass : public theory::eq::EqualityEngineNotify
+{
+ public:
+  MasterNotifyClass(QuantifiersEngine* qe);
+  /**
+    * Called when a new equivalence class is created in the master equality
+    * engine.
+    */
+  void eqNotifyNewClass(TNode t) override;
+
+  bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+  {
+    return true;
+  }
+  bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                    TNode t1,
+                                    TNode t2,
+                                    bool value) override
+  {
+    return true;
+  }
+  void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
+  void eqNotifyMerge(TNode t1, TNode t2) override {}
+  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
+
+  private:
+  /** Pointer to quantifiers engine */
+  QuantifiersEngine* d_quantEngine;
+};
+
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /* CVC5__THEORY__QUANTIFIERS__MASTER_EQ_NOTIFY__H */