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.

7 files changed, 273 insertions, 66 deletions

diff --git a/NEWS b/NEWS
index 60ff9dbc8..f5f9bc03a 100644
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,12 @@
 This file contains a summary of important user-visible changes.
 
+Changes since 1.8
+=================
+
+Improvements:
+* New API: Added functions to retrieve the heap/nil term when using separation
+  logic.
+
 Changes since 1.7
 =================
 
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)
 
diff --git a/test/system/sep_log_api.cpp b/test/system/sep_log_api.cpp
index c4244d7cb..9341310a3 100644
--- a/test/system/sep_log_api.cpp
+++ b/test/system/sep_log_api.cpp
@@ -22,10 +22,9 @@
 #include <iostream>
 #include <sstream>
 
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
+#include "api/cvc4cpp.h"
 
-using namespace CVC4;
+using namespace CVC4::api;
 using namespace std;
 
 /**
@@ -34,33 +33,31 @@ using namespace std;
  */
 int validate_exception(void)
 {
-  ExprManager em;
-  Options opts;
-  SmtEngine smt(&em);
+  Solver slv;
 
   /*
    * Setup some options for CVC4 -- we explictly want to use a simplistic
    * theory (e.g., QF_IDL)
    */
-  smt.setLogic("QF_IDL");
-  smt.setOption("produce-models", SExpr("true"));
-  smt.setOption("incremental", SExpr("false"));
+  slv.setLogic("QF_IDL");
+  slv.setOption("produce-models", "true");
+  slv.setOption("incremental", "false");
 
   /* Our integer type */
-  Type integer(em.integerType());
+  Sort integer = slv.getIntegerSort();
 
   /* Our SMT constants */
-  Expr x(em.mkVar("x", integer));
-  Expr y(em.mkVar("y", integer));
+  Term x = slv.mkConst(integer, "x");
+  Term y = slv.mkConst(integer, "y");
 
   /* y > x */
-  Expr y_gt_x(em.mkExpr(kind::GT, y, x));
+  Term y_gt_x(slv.mkTerm(Kind::GT, y, x));
 
   /* assert it */
-  smt.assertFormula(y_gt_x);
+  slv.assertFormula(y_gt_x);
 
   /* check */
-  Result r(smt.checkSat());
+  Result r(slv.checkSat());
 
   /* If this is UNSAT, we have an issue; so bail-out */
   if (!r.isSat())
@@ -83,9 +80,9 @@ int validate_exception(void)
   /* test the heap expression */
   try
   {
-    Expr heap_expr(smt.getSepHeapExpr());
+    Term heap_expr = slv.getSeparationHeap();
   }
-  catch (const CVC4::RecoverableModalException& e)
+  catch (const CVC4ApiException& e)
   {
     caught_on_heap = true;
 
@@ -99,9 +96,9 @@ int validate_exception(void)
   /* test the nil expression */
   try
   {
-    Expr nil_expr(smt.getSepNilExpr());
+    Term nil_expr = slv.getSeparationNilTerm();
   }
-  catch (const CVC4::RecoverableModalException& e)
+  catch (const CVC4ApiException& e)
   {
     caught_on_nil = true;
 
@@ -127,60 +124,56 @@ int validate_exception(void)
  */
 int validate_getters(void)
 {
-  ExprManager em;
-  Options opts;
-  SmtEngine smt(&em);
+  Solver slv;
 
   /* Setup some options for CVC4 */
-  smt.setLogic("QF_ALL_SUPPORTED");
-  smt.setOption("produce-models", SExpr("true"));
-  smt.setOption("incremental", SExpr("false"));
+  slv.setLogic("QF_ALL_SUPPORTED");
+  slv.setOption("produce-models", "true");
+  slv.setOption("incremental", "false");
 
   /* Our integer type */
-  Type integer(em.integerType());
+  Sort integer = slv.getIntegerSort();
 
   /* A "random" constant */
-  Rational val_for_random_constant(Rational(0xDEADBEEF));
-  Expr random_constant(em.mkConst(val_for_random_constant));
+  Term random_constant = slv.mkReal(0xDEADBEEF);
 
   /* Another random constant */
-  Rational val_for_expr_nil_val(Rational(0xFBADBEEF));
-  Expr expr_nil_val(em.mkConst(val_for_expr_nil_val));
+  Term expr_nil_val = slv.mkReal(0xFBADBEEF);
 
   /* Our nil term */
-  Expr nil(em.mkNullaryOperator(integer, kind::SEP_NIL));
+  Term nil = slv.mkSepNil(integer);
 
   /* Our SMT constants */
-  Expr x(em.mkVar("x", integer));
-  Expr y(em.mkVar("y", integer));
-  Expr p1(em.mkVar("p1", integer));
-  Expr p2(em.mkVar("p2", integer));
+  Term x = slv.mkConst(integer, "x");
+  Term y = slv.mkConst(integer, "y");
+  Term p1 = slv.mkConst(integer, "p1");
+  Term p2 = slv.mkConst(integer, "p2");
 
   /* Constraints on x and y */
-  Expr x_equal_const(em.mkExpr(kind::EQUAL, x, random_constant));
-  Expr y_gt_x(em.mkExpr(kind::GT, y, x));
+  Term x_equal_const = slv.mkTerm(Kind::EQUAL, x, random_constant);
+  Term y_gt_x = slv.mkTerm(Kind::GT, y, x);
 
   /* Points-to expressions */
-  Expr p1_to_x(em.mkExpr(kind::SEP_PTO, p1, x));
-  Expr p2_to_y(em.mkExpr(kind::SEP_PTO, p2, y));
+  Term p1_to_x = slv.mkTerm(Kind::SEP_PTO, p1, x);
+  Term p2_to_y = slv.mkTerm(Kind::SEP_PTO, p2, y);
 
   /* Heap -- the points-to have to be "starred"! */
-  Expr heap(em.mkExpr(kind::SEP_STAR, p1_to_x, p2_to_y));
+  Term heap = slv.mkTerm(Kind::SEP_STAR, p1_to_x, p2_to_y);
 
   /* Constain "nil" to be something random */
-  Expr fix_nil(em.mkExpr(kind::EQUAL, nil, expr_nil_val));
+  Term fix_nil = slv.mkTerm(Kind::EQUAL, nil, expr_nil_val);
 
   /* Add it all to the solver! */
-  smt.assertFormula(x_equal_const);
-  smt.assertFormula(y_gt_x);
-  smt.assertFormula(heap);
-  smt.assertFormula(fix_nil);
+  slv.assertFormula(x_equal_const);
+  slv.assertFormula(y_gt_x);
+  slv.assertFormula(heap);
+  slv.assertFormula(fix_nil);
 
   /*
    * Incremental is disabled due to using separation logic, so don't query
    * twice!
    */
-  Result r(smt.checkSat());
+  Result r(slv.checkSat());
 
   /* If this is UNSAT, we have an issue; so bail-out */
   if (!r.isSat())
@@ -189,43 +182,41 @@ int validate_getters(void)
   }
 
   /* Obtain our separation logic terms from the solver */
-  Expr heap_expr(smt.getSepHeapExpr());
-  Expr nil_expr(smt.getSepNilExpr());
+  Term heap_expr = slv.getSeparationHeap();
+  Term nil_expr = slv.getSeparationNilTerm();
 
   /* If the heap is not a separating conjunction, bail-out */
-  if (heap_expr.getKind() != kind::SEP_STAR)
+  if (heap_expr.getKind() != Kind::SEP_STAR)
   {
     return -1;
   }
 
   /* If nil is not a direct equality, bail-out */
-  if (nil_expr.getKind() != kind::EQUAL)
+  if (nil_expr.getKind() != Kind::EQUAL)
   {
     return -1;
   }
 
   /* Obtain the values for our "pointers" */
-  Rational val_for_p1(smt.getValue(p1).getConst<CVC4::Rational>());
-  Rational val_for_p2(smt.getValue(p2).getConst<CVC4::Rational>());
+  Term val_for_p1 = slv.getValue(p1);
+  Term val_for_p2 = slv.getValue(p2);
 
   /* We need to make sure we find both pointers in the heap */
   bool checked_p1(false);
   bool checked_p2(false);
 
   /* Walk all the children */
-  for (Expr child : heap_expr.getChildren())
+  for (const Term& child : heap_expr)
   {
     /* If we don't have a PTO operator, bail-out */
-    if (child.getKind() != kind::SEP_PTO)
+    if (child.getKind() != Kind::SEP_PTO)
     {
       return -1;
     }
 
     /* Find both sides of the PTO operator */
-    Rational addr(
-        smt.getValue(child.getChildren().at(0)).getConst<CVC4::Rational>());
-    Rational value(
-        smt.getValue(child.getChildren().at(1)).getConst<CVC4::Rational>());
+    Term addr = slv.getValue(child[0]);
+    Term value = slv.getValue(child[1]);
 
     /* If the current address is the value for p1 */
     if (addr == val_for_p1)
@@ -233,7 +224,7 @@ int validate_getters(void)
       checked_p1 = true;
 
       /* If it doesn't match the random constant, we have a problem */
-      if (value != val_for_random_constant)
+      if (value != random_constant)
       {
         return -1;
       }
@@ -250,7 +241,8 @@ int validate_getters(void)
        * than the random constant -- if we get a value that is LTE, then
        * something has gone wrong!
        */
-      if (value <= val_for_random_constant)
+      if (std::stoll(value.toString())
+          <= std::stoll(random_constant.toString()))
       {
         return -1;
       }
@@ -274,14 +266,13 @@ int validate_getters(void)
   }
 
   /* We now get our value for what nil is */
-  Rational value_for_nil =
-      smt.getValue(nil_expr.getChildren().at(1)).getConst<CVC4::Rational>();
+  Term value_for_nil = slv.getValue(nil_expr[1]);
 
   /*
    * The value for nil from the solver should be the value we originally tied
    * nil to
    */
-  if (value_for_nil != val_for_expr_nil_val)
+  if (value_for_nil != expr_nil_val)
   {
     return -1;
   }
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 6faab6075..f080f5348 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -106,6 +106,22 @@ class SolverBlack : public CxxTest::TestSuite
   void testGetValue1();
   void testGetValue2();
   void testGetValue3();
+  void testGetSeparationHeapTerm1();
+  void testGetSeparationHeapTerm2();
+  void testGetSeparationHeapTerm3();
+  void testGetSeparationHeapTerm4();
+  void testGetSeparationHeapTerm5();
+  void testGetSeparationNilTerm1();
+  void testGetSeparationNilTerm2();
+  void testGetSeparationNilTerm3();
+  void testGetSeparationNilTerm4();
+  void testGetSeparationNilTerm5();
+
+  /**
+   * When using separation logic, obtain the term for nil.
+   * @return The term for nil
+   */
+  Term getSeparationNilTerm() const;
 
   void testPush1();
   void testPush2();
@@ -1493,6 +1509,124 @@ void SolverBlack::testGetValue3()
   TS_ASSERT_THROWS(slv.getValue(x), CVC4ApiException&);
 }
 
+namespace {
+/**
+ * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks
+ * some simple separation logic constraints.
+ */
+void checkSimpleSeparationConstraints(Solver* solver)
+{
+  Sort integer = solver->getIntegerSort();
+  Term x = solver->mkConst(integer, "x");
+  Term p = solver->mkConst(integer, "p");
+  Term heap = solver->mkTerm(Kind::SEP_PTO, p, x);
+  solver->assertFormula(heap);
+  Term nil = solver->mkSepNil(integer);
+  solver->assertFormula(nil.eqTerm(solver->mkReal(5)));
+  solver->checkSat();
+}
+}  // namespace
+
+void SolverBlack::testGetSeparationHeapTerm1()
+{
+  d_solver->setLogic("QF_BV");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("produce-models", "true");
+  Term t = d_solver->mkTrue();
+  d_solver->assertFormula(t);
+  TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&);
+}
+
+void SolverBlack::testGetSeparationHeapTerm2()
+{
+  d_solver->setLogic("ALL_SUPPORTED");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("produce-models", "false");
+  checkSimpleSeparationConstraints(d_solver.get());
+  TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&);
+}
+
+void SolverBlack::testGetSeparationHeapTerm3()
+{
+  d_solver->setLogic("ALL_SUPPORTED");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("produce-models", "true");
+  Term t = d_solver->mkFalse();
+  d_solver->assertFormula(t);
+  d_solver->checkSat();
+  TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&);
+}
+
+void SolverBlack::testGetSeparationHeapTerm4()
+{
+  d_solver->setLogic("ALL_SUPPORTED");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("produce-models", "true");
+  Term t = d_solver->mkTrue();
+  d_solver->assertFormula(t);
+  d_solver->checkSat();
+  TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&);
+}
+
+void SolverBlack::testGetSeparationHeapTerm5()
+{
+  d_solver->setLogic("ALL_SUPPORTED");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("produce-models", "true");
+  checkSimpleSeparationConstraints(d_solver.get());
+  TS_ASSERT_THROWS_NOTHING(d_solver->getSeparationHeap());
+}
+
+void SolverBlack::testGetSeparationNilTerm1()
+{
+  d_solver->setLogic("QF_BV");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("produce-models", "true");
+  Term t = d_solver->mkTrue();
+  d_solver->assertFormula(t);
+  TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&);
+}
+
+void SolverBlack::testGetSeparationNilTerm2()
+{
+  d_solver->setLogic("ALL_SUPPORTED");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("produce-models", "false");
+  checkSimpleSeparationConstraints(d_solver.get());
+  TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&);
+}
+
+void SolverBlack::testGetSeparationNilTerm3()
+{
+  d_solver->setLogic("ALL_SUPPORTED");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("produce-models", "true");
+  Term t = d_solver->mkFalse();
+  d_solver->assertFormula(t);
+  d_solver->checkSat();
+  TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&);
+}
+
+void SolverBlack::testGetSeparationNilTerm4()
+{
+  d_solver->setLogic("ALL_SUPPORTED");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("produce-models", "true");
+  Term t = d_solver->mkTrue();
+  d_solver->assertFormula(t);
+  d_solver->checkSat();
+  TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&);
+}
+
+void SolverBlack::testGetSeparationNilTerm5()
+{
+  d_solver->setLogic("ALL_SUPPORTED");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("produce-models", "true");
+  checkSimpleSeparationConstraints(d_solver.get());
+  TS_ASSERT_THROWS_NOTHING(d_solver->getSeparationNilTerm());
+}
+
 void SolverBlack::testPush1()
 {
   d_solver->setOption("incremental", "true");