Eliminate a custom use of TheorySep in quantifiers engine for EPR (#5039)

This moves the initialization of the connection between separation logic and EPR to the separation logic theory, which is a more logical place for this. This eliminates a backwards reference to theory engine from quantifiers engine.

1 files changed, 16 insertions, 0 deletions

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index dc8ec9203..c9b6a9d89 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1001,6 +1001,22 @@ void TheorySep::ppNotifyAssertions(const std::vector<Node>& assertions) {
       d_loc_to_data_type[d_type_ref] = d_type_data;
     }
   }
+  // initialize the EPR utility
+  QuantifiersEngine* qe = getQuantifiersEngine();
+  if (qe != nullptr)
+  {
+    quantifiers::QuantEPR* qepr = qe->getQuantEPR();
+    if (qepr != nullptr)
+    {
+      for (const Node& a : assertions)
+      {
+        qepr->registerAssertion(a);
+      }
+      // must handle sources of other new constants e.g. separation logic
+      initializeBounds();
+      qepr->finishInit();
+    }
+  }
 }
 
 //return cardinality