From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 8 Sep 2020 16:45:38 +0000 (-0500)
Subject: Eliminate a custom use of TheorySep in quantifiers engine for EPR (#5039)
X-Git-Tag: cvc5-1.0.0~2889
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=be3543ef7e01eb32aab3161fa2778953fabc988d;p=cvc5.git

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 6f00998d2..236137bb2 100644
--- 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 59082b55f..3bfc4ac61 100644
--- 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 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