Add proper support for the declare-heap command for separation logic (#5405)

This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic.

This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred.

Fixes #5343, fixes #4926.

Work towards CVC4/cvc4-wishues#22.

1 files changed, 36 insertions, 6 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index dc5338199..a5861c6b0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -65,6 +65,7 @@
 #include "theory/logic_info.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
+#include "theory/smt_engine_subsolver.h"
 #include "theory/theory_engine.h"
 #include "util/hash.h"
 #include "util/random.h"
@@ -1448,6 +1449,28 @@ std::vector<Node> SmtEngine::getExpandedAssertions()
   return eassertsProc;
 }
 
+void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
+{
+  if (!d_logic.isTheoryEnabled(THEORY_SEP))
+  {
+    const char* msg =
+        "Cannot declare heap if not using the separation logic theory.";
+    throw RecoverableModalException(msg);
+  }
+  SmtScope smts(this);
+  finishInit();
+  TheoryEngine* te = getTheoryEngine();
+  te->declareSepHeap(locT, dataT);
+}
+
+bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT)
+{
+  SmtScope smts(this);
+  finishInit();
+  TheoryEngine* te = getTheoryEngine();
+  return te->getSepHeapTypes(locT, dataT);
+}
+
 Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
 
 Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
@@ -1483,21 +1506,28 @@ void SmtEngine::checkUnsatCore() {
   Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
   UnsatCore core = getUnsatCore();
 
-  SmtEngine coreChecker(d_exprManager, &d_options);
-  coreChecker.setIsInternalSubsolver();
-  coreChecker.setLogic(getLogicInfo());
-  coreChecker.getOptions().set(options::checkUnsatCores, false);
+  // initialize the core checker
+  std::unique_ptr<SmtEngine> coreChecker;
+  initializeSubsolver(coreChecker);
+  coreChecker->getOptions().set(options::checkUnsatCores, false);
+
+  // set up separation logic heap if necessary
+  TypeNode sepLocType, sepDataType;
+  if (getSepHeapTypes(sepLocType, sepDataType))
+  {
+    coreChecker->declareSepHeap(sepLocType, sepDataType);
+  }
 
   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
     Node assertionAfterExpansion = expandDefinitions(*i);
     Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
              << ", expanded to " << assertionAfterExpansion << "\n";
-    coreChecker.assertFormula(assertionAfterExpansion);
+    coreChecker->assertFormula(assertionAfterExpansion);
   }
   Result r;
   try {
-    r = coreChecker.checkSat();
+    r = coreChecker->checkSat();
   } catch(...) {
     throw;
   }