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.

1 files changed, 134 insertions, 0 deletions

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");