From 25d3eea9614a0882a5c18c455e5a14d118a78dce Mon Sep 17 00:00:00 2001
From: ayveejay <41393247+ayveejay@users.noreply.github.com>
Date: Tue, 24 Jul 2018 22:16:16 +0100
Subject: [PATCH] Adding API access methods to get heap/nil expressions when
 using separation logic (#2194)

---
 src/smt/smt_engine.cpp | 24 ++++++++++++++++++++++++
 src/smt/smt_engine.h   | 10 ++++++++++
 2 files changed, 34 insertions(+)

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
@@ -486,6 +486,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.
    */
-- 
2.30.2