From c7116b06892b5ff21fb04a3996880bfe48e44053 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 Jun 2021 21:24:40 -0500 Subject: 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/uf/theory_uf.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/theory/uf') 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; } -- cgit v1.2.3