Add API for retrieving separation heap/nil term (#4663)

This commit extends the API to support the retrieval of heap/nil term
when separation logic is used and changes the corresponding system test
accordingly. This commit is in preparation of making the constructor of
`ExprManager` private.

4 files changed, 78 insertions, 3 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index cebba9b5e..0c8de5291 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -33,6 +33,9 @@
 
 #include "api/cvc4cpp.h"
 
+#include <cstring>
+#include <sstream>
+
 #include "base/check.h"
 #include "base/configuration.h"
 #include "expr/expr.h"
@@ -49,13 +52,11 @@
 #include "smt/model.h"
 #include "smt/smt_engine.h"
 #include "theory/logic_info.h"
+#include "theory/theory_model.h"
 #include "util/random.h"
 #include "util/result.h"
 #include "util/utility.h"
 
-#include <cstring>
-#include <sstream>
-
 namespace CVC4 {
 namespace api {
 
@@ -4673,6 +4674,56 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::getSeparationHeap() const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(
+      d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
+      << "Cannot obtain separation logic expressions if not using the "
+         "separation logic theory.";
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::produceModels())
+      << "Cannot get separation heap term unless model generation is enabled "
+         "(try --produce-models)";
+  CVC4_API_CHECK(d_smtEngine->getSmtMode()
+                 != SmtEngine::SmtMode::SMT_MODE_UNSAT)
+      << "Cannot get separtion heap term when in unsat mode.";
+
+  theory::TheoryModel* m =
+      d_smtEngine->getAvailableModel("get separation logic heap and nil");
+  Expr heap, nil;
+  bool hasHeapModel = m->getHeapModel(heap, nil);
+  CVC4_API_CHECK(hasHeapModel)
+      << "Failed to obtain heap term from theory model.";
+  return Term(this, d_smtEngine->getSepHeapExpr());
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+Term Solver::getSeparationNilTerm() const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(
+      d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
+      << "Cannot obtain separation logic expressions if not using the "
+         "separation logic theory.";
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::produceModels())
+      << "Cannot get separation nil term unless model generation is enabled "
+         "(try --produce-models)";
+  CVC4_API_CHECK(d_smtEngine->getSmtMode()
+                 != SmtEngine::SmtMode::SMT_MODE_UNSAT)
+      << "Cannot get separtion nil term when in unsat mode.";
+
+  theory::TheoryModel* m =
+      d_smtEngine->getAvailableModel("get separation logic heap and nil");
+  Expr heap, nil;
+  bool hasHeapModel = m->getHeapModel(heap, nil);
+  CVC4_API_CHECK(hasHeapModel)
+      << "Failed to obtain nil term from theory model.";
+  return Term(this, nil);
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 /**
  *  ( pop <numeral> )
  */
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 049cf6709..828dc6f65 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -3004,6 +3004,18 @@ class CVC4_PUBLIC Solver
   std::vector<Term> getValue(const std::vector<Term>& terms) const;
 
   /**
+   * When using separation logic, obtain the term for the heap.
+   * @return The term for the heap
+   */
+  Term getSeparationHeap() const;
+
+  /**
+   * When using separation logic, obtain the term for nil.
+   * @return The term for nil
+   */
+  Term getSeparationNilTerm() const;
+
+  /**
    * Pop (a) level(s) from the assertion stack.
    * SMT-LIB: ( pop <numeral> )
    * @param nscopes the number of levels to pop
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index eb4254560..ee05709b7 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -197,6 +197,8 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         vector[Term] getUnsatCore() except +
         Term getValue(Term term) except +
         vector[Term] getValue(const vector[Term]& terms) except +
+        Term getSeparationHeap() except +
+        Term getSeparationNilTerm() except +
         void pop(uint32_t nscopes) except +
         void printModel(ostream& out)
         void push(uint32_t nscopes) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 5abbfb113..ab174ef0d 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -917,6 +917,16 @@ cdef class Solver:
         term.cterm = self.csolver.getValue(t.cterm)
         return term
 
+    def getSeparationHeap(self):
+        cdef Term term = Term()
+        term.cterm = self.csolver.getSeparationHeap()
+        return term
+
+    def getSeparationNilTerm(self):
+        cdef Term term = Term()
+        term.cterm = self.csolver.getSeparationNilTerm()
+        return term
+
     def pop(self, nscopes=1):
         self.csolver.pop(nscopes)