Improvements and tests for the API around separation logic (#2229)

- Introduces a system that validating that, when not using THEORY_SEP, that it is not possible to
  obtain the separation logic heap/nil (validate_exception())
- Introduces a system test demonstrating how to use the separation logic theory, and then how
  to use the "getters" to obtain and interrogate the heap/nil expressions (validate_getters())
- Refactors the original getters to avoid duplicate code
- Add a check as part of the getters to ensure that THEORY_SEP is in use

2 files changed, 23 insertions, 20 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 801711a13..cfafd63c4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5258,36 +5258,32 @@ Model* SmtEngine::getModel() {
   return m;
 }
 
-Expr SmtEngine::getHeapExpr()
+std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void)
 {
-  NodeManagerScope nms(d_nodeManager);
-  Expr heap;
-  Expr nil;  // we don't actually use this
-  Model* m = getModel();
-  if (m->getHeapModel(heap, nil))
+  if (!d_logic.isTheoryEnabled(THEORY_SEP))
   {
-    return heap;
+    const char* msg =
+        "Cannot obtain separation logic expressions if not using the "
+        "separation logic theory.";
+    throw RecoverableModalException(msg);
   }
-  InternalError(
-      "SmtEngine::getHeapExpr(): failed to obtain heap expression from theory "
-      "model.");
-}
-
-Expr SmtEngine::getNilExpr()
-{
   NodeManagerScope nms(d_nodeManager);
-  Expr heap;  // we don't actually use this
+  Expr heap;
   Expr nil;
   Model* m = getModel();
   if (m->getHeapModel(heap, nil))
   {
-    return nil;
+    return std::make_pair(heap, nil);
   }
   InternalError(
-      "SmtEngine::getNilExpr(): failed to obtain nil expression from theory "
-      "model.");
+      "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
+      "expressions from theory model.");
 }
 
+Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
+
+Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
+
 void SmtEngine::checkUnsatCore() {
   Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3536c5b1b..e4bd7d77d 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -429,6 +429,13 @@ class CVC4_PUBLIC SmtEngine {
                               const std::vector<Expr>& formals,
                               Expr func);
 
+  /**
+   * Helper method to obtain both the heap and nil from the solver. Returns a
+   * std::pair where the first element is the heap expression and the second
+   * element is the nil expression.
+   */
+  std::pair<Expr, Expr> getSepHeapAndNilExpr();
+
  public:
 
   /**
@@ -489,12 +496,12 @@ class CVC4_PUBLIC SmtEngine {
   /**
    * When using separation logic, obtain the expression for the heap.
    */
-  Expr getHeapExpr();
+  Expr getSepHeapExpr();
 
   /**
    * When using separation logic, obtain the expression for nil.
    */
-  Expr getNilExpr();
+  Expr getSepNilExpr();
 
   /**
    * Get an aspect of the current SMT execution environment.