From c7116b06892b5ff21fb04a3996880bfe48e44053 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 Jun 2021 21:24:40 -0500 Subject: [PATCH] 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. --- src/theory/arrays/theory_arrays.cpp | 2 ++ src/theory/datatypes/theory_datatypes.cpp | 3 +++ src/theory/ee_setup_info.h | 21 ++++++++++++++++++++- src/theory/sep/theory_sep.cpp | 1 + src/theory/sets/theory_sets.cpp | 3 +++ src/theory/strings/term_registry.cpp | 3 ++- src/theory/strings/theory_strings.cpp | 3 +++ src/theory/uf/theory_uf.cpp | 8 ++++++++ 8 files changed, 42 insertions(+), 2 deletions(-) diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index ea18b3180..be8e1a08e 100644 --- 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 dc57e4165..53f128286 100644 --- 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 f6139d109..130241c4a 100644 --- 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 6d1b9955a..efede77ba 100644 --- 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 4cca76057..439e9443d 100644 --- 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 aac9e9313..8c5805b37 100644 --- 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 f4daed85d..f0763e153 100644 --- 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 36b05b145..f1adde143 100644 --- 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; } -- 2.30.2