Set up fine grained equality notifications (#6734)

This adds fields to equality engine setup information which will be used to hook up theories to the central equality engine.

This PR does not impact any behavior.

This is in preparation for the central equality engine.

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index ea18b31806b27d904a4bb70c4eae2a066347080a..be8e1a08e76af8312df000cd8b84bf21c6529126 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -151,6 +151,8 @@ bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
   esi.d_name = d_instanceName + "ee";
+  esi.d_notifyNewClass = true;
+  esi.d_notifyMerge = true;
   return true;
 }
 

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index dc57e4165875882b8ee9c807af7c2e5e173fc4cd..53f1282862a22827f19d65884ee4254d33618268 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -94,6 +94,9 @@ bool TheoryDatatypes::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
   esi.d_name = "theory::datatypes::ee";
+  // need notifications on new constructors, merging datatype eqcs
+  esi.d_notifyNewClass = true;
+  esi.d_notifyMerge = true;
   return true;
 }
 

diff --git a/src/theory/ee_setup_info.h b/src/theory/ee_setup_info.h
index f6139d1090af6ecf4bc4847cb0b6d4181033beb3..130241c4a9ab0903bf4221616da24fcfec80fb63 100644 (file)
--- a/src/theory/ee_setup_info.h
+++ b/src/theory/ee_setup_info.h
@@ -39,7 +39,12 @@ class EqualityEngineNotify;
 struct EeSetupInfo
 {
   EeSetupInfo()
-      : d_notify(nullptr), d_constantsAreTriggers(true), d_useMaster(false)
+      : d_notify(nullptr),
+        d_constantsAreTriggers(true),
+        d_notifyNewClass(false),
+        d_notifyMerge(false),
+        d_notifyDisequal(false),
+        d_useMaster(false)
   {
   }
   /** The notification class of the theory */
@@ -48,11 +53,25 @@ struct EeSetupInfo
   std::string d_name;
   /** Constants are triggers */
   bool d_constantsAreTriggers;
+  //-------------------------- fine grained notifications
+  /** Whether we need to be notified of new equivalence classes */
+  bool d_notifyNewClass;
+  /** Whether we need to be notified of merged equivalence classes */
+  bool d_notifyMerge;
+  /** Whether we need to be notified of disequal equivalence classes */
+  bool d_notifyDisequal;
+  //-------------------------- end fine grained notifications
   /**
    * Whether we want our state to use the master equality engine. This should
    * be true exclusively for the theory of quantifiers.
    */
   bool d_useMaster;
+  /** Does it need notifications when equivalence classes are created? */
+  bool needsNotifyNewClass() const { return d_notifyNewClass; }
+  /** Does it need notifications when equivalence classes are merged? */
+  bool needsNotifyMerge() const { return d_notifyMerge; }
+  /** Does it need notifications when disequalities are generated? */
+  bool needsNotifyDisequal() const { return d_notifyDisequal; }
 };
 
 }  // namespace theory

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 6d1b9955afcc20d043ef0855941e85f531407985..efede77ba54cc6d3fad7739b751f7dd0a338da8d 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -95,6 +95,7 @@ bool TheorySep::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
   esi.d_name = "theory::sep::ee";
+  esi.d_notifyMerge = true;
   return true;
 }
 

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 4cca76057a21574bb4dc9c3ecbd7ba2a2818eaa0..439e9443d4e2c5650a99a427bb2e55a3791151a7 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -60,6 +60,9 @@ bool TheorySets::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
   esi.d_name = "theory::sets::ee";
+  esi.d_notifyNewClass = true;
+  esi.d_notifyMerge = true;
+  esi.d_notifyDisequal = true;
   return true;
 }
 

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index aac9e93136293c6a0093f63050a3f0c42415beee..8c5805b37be86f9d8a08a0b03a7814702d02ad94 100644 (file)
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -249,7 +249,8 @@ void TermRegistry::preRegisterTerm(TNode n)
   // Concatenation terms do not need to be considered here because
   // their arguments have string type and do not introduce any shared
   // terms.
-  if (n.hasOperator() && ee->isFunctionKind(k) && k != STRING_CONCAT)
+  if (n.hasOperator() && ee->isFunctionKind(k)
+      && kindToTheoryId(k) == THEORY_STRINGS && k != STRING_CONCAT)
   {
     d_functionsTerms.push_back(n);
   }

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f4daed85d030c24b225a38abc1e5fcef3a8b7454..f0763e153d5b09e4ef7ce24fd995ee2b9a852942 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -103,6 +103,9 @@ bool TheoryStrings::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
   esi.d_name = "theory::strings::ee";
+  esi.d_notifyNewClass = true;
+  esi.d_notifyMerge = true;
+  esi.d_notifyDisequal = true;
   return true;
 }
 

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 36b05b1450ac953f65f3e0670569a22edec04ef0..f1adde143ae743ef78306e1f54d4b90a91398d71 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -73,6 +73,14 @@ bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi)
 {
   esi.d_notify = &d_notify;
   esi.d_name = d_instanceName + "theory::uf::ee";
+  if (options::finiteModelFind()
+      && options::ufssMode() != options::UfssMode::NONE)
+  {
+    // need notifications about sorts
+    esi.d_notifyNewClass = true;
+    esi.d_notifyMerge = true;
+    esi.d_notifyDisequal = true;
+  }
   return true;
 }