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.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 6f00998d21b71dbae803ed69671f6bef1afc5bed..236137bb2ac7fd0e427a41e7083a22a38881b0cf 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -911,6 +911,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       options::preSkolemQuant.set(true);
     }
+    // must have separation logic
+    logic = logic.getUnlockedCopy();
+    logic.enableTheory(THEORY_SEP);
+    logic.lock();
   }
 
   // now, have determined whether finite model find is on/off

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 59082b55f8e475a1a46333aaac83aa9091d69817..3bfc4ac61a45c19b5e7c16b2788097e83d683cd9 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -498,19 +498,6 @@ void QuantifiersEngine::ppNotifyAssertions(
       quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0);
     }
   }
-  if (d_qepr != NULL)
-  {
-    for (const Node& a : assertions)
-    {
-      d_qepr->registerAssertion(a);
-    }
-    // must handle sources of other new constants e.g. separation logic
-    // FIXME (as part of project 3) : cleanup
-    sep::TheorySep* theory_sep =
-        static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP));
-    theory_sep->initializeBounds();
-    d_qepr->finishInit();
-  }
   if (options::sygus())
   {
     quantifiers::SynthEngine* sye = d_private->d_synth_e.get();

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index dc8ec92036465dd69ed9f67a01dd010f107c1f2c..c9b6a9d892c3e8f8107e01a51b7f223618255a0b 100644 (file)
--- 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