Adding API access methods to get heap/nil expressions when using separation logic (#2194)

2 files changed, 34 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 71256e3d8..a275c7d63 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5251,6 +5251,30 @@ Model* SmtEngine::getModel() {
   return m;
 }
 
+Expr SmtEngine::getHeapExpr() {
+  NodeManagerScope nms(d_nodeManager);
+  Expr heap;
+  Expr nil; // we don't actually use this
+  Model* m = getModel();
+  if (m->getHeapModel( heap, nil ))
+  {
+    return heap;
+  }
+  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 nil;
+  Model* m = getModel();
+  if (m->getHeapModel( heap, nil ))
+  {
+    return nil;
+  }
+  InternalError("SmtEngine::getNilExpr(): failed to obtain nil expression from theory model.");
+}
+
 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 dd1d1b88a..3536c5b1b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -487,6 +487,16 @@ class CVC4_PUBLIC SmtEngine {
   Model* getModel();
 
   /**
+   * When using separation logic, obtain the expression for the heap.
+   */
+  Expr getHeapExpr();
+
+  /**
+   * When using separation logic, obtain the expression for nil.
+   */
+  Expr getNilExpr();
+
+  /**
    * Get an aspect of the current SMT execution environment.
    */
   CVC4::SExpr getOption(const std::string& key) const