api: Rename some separation logic functions for consistency. (#7564)

This renames Solver::getSeparationHeap to Solver::getValueSepHeap,
Solver::getSeparationNilTerm to Solver::getSepNil and
Solver::declareSeparationHeap to Solver::declareSepHeap.

@mudathirmahgoub @alex-ozdemir @yoni206

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d1be25bb47f543bdae86fb5ab46fdd90bf570434..0450ac06a7a236ed1024b52f594bd381f952d0b3 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7345,8 +7345,7 @@ Term Solver::getQuantifierEliminationDisjunct(const Term& q) const
   CVC5_API_TRY_CATCH_END;
 }
 
-void Solver::declareSeparationHeap(const Sort& locSort,
-                                   const Sort& dataSort) const
+void Solver::declareSepHeap(const Sort& locSort, const Sort& dataSort) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(locSort);
@@ -7360,7 +7359,7 @@ void Solver::declareSeparationHeap(const Sort& locSort,
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::getSeparationHeap() const
+Term Solver::getValueSepHeap() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(d_slv->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
@@ -7377,7 +7376,7 @@ Term Solver::getSeparationHeap() const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::getSeparationNilTerm() const
+Term Solver::getValueSepNil() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(d_slv->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 63dadaef630b86e0214993972bea60ba15185549..f348ae4e5e1d694c2d8103030adc1c67ac797934 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4090,19 +4090,19 @@ class CVC5_EXPORT Solver
    * @param locSort The location sort of the heap
    * @param dataSort The data sort of the heap
    */
-  void declareSeparationHeap(const Sort& locSort, const Sort& dataSort) const;
+  void declareSepHeap(const Sort& locSort, const Sort& dataSort) const;
 
   /**
    * When using separation logic, obtain the term for the heap.
    * @return The term for the heap
    */
-  Term getSeparationHeap() const;
+  Term getValueSepHeap() const;
 
   /**
    * When using separation logic, obtain the term for nil.
    * @return The term for nil
    */
-  Term getSeparationNilTerm() const;
+  Term getValueSepNil() const;
 
   /**
    * Declare a symbolic pool of terms with the given initial value.

diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 6c1399d9cfd49b3311a120e08e9a9d9fd734e103..0479dce3df29f571e076edacee81b542b0f70b32 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -2052,37 +2052,36 @@ public class Solver implements IPointer, AutoCloseable
    * @param locSort The location sort of the heap
    * @param dataSort The data sort of the heap
    */
-  public void declareSeparationHeap(Sort locSort, Sort dataSort)
+  public void declareSepHeap(Sort locSort, Sort dataSort)
   {
-    declareSeparationHeap(pointer, locSort.getPointer(), dataSort.getPointer());
+    declareSepHeap(pointer, locSort.getPointer(), dataSort.getPointer());
   }
 
-  private native void declareSeparationHeap(
-      long pointer, long locSortPointer, long dataSortPointer);
+  private native void declareSepHeap(long pointer, long locSortPointer, long dataSortPointer);
 
   /**
    * When using separation logic, obtain the term for the heap.
    * @return The term for the heap
    */
-  public Term getSeparationHeap()
+  public Term getValueSepHeap()
   {
-    long termPointer = getSeparationHeap(pointer);
+    long termPointer = getValueSepHeap(pointer);
     return new Term(this, termPointer);
   }
 
-  private native long getSeparationHeap(long pointer);
+  private native long getValueSepHeap(long pointer);
 
   /**
    * When using separation logic, obtain the term for nil.
    * @return The term for nil
    */
-  public Term getSeparationNilTerm()
+  public Term getValueSepNil()
   {
-    long termPointer = getSeparationNilTerm(pointer);
+    long termPointer = getValueSepNil(pointer);
     return new Term(this, termPointer);
   }
 
-  private native long getSeparationNilTerm(long pointer);
+  private native long getValueSepNil(long pointer);
 
   /**
    * Declare a symbolic pool of terms with the given initial value.

diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index 2d775c5451b3b1fda1bd8c757142b8303f4a556f..cb4d58591b296bca9ed8ec7137e1927f82ca7978 100644 (file)
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -2106,50 +2106,50 @@ Java_io_github_cvc5_api_Solver_getQuantifierEliminationDisjunct(JNIEnv* env,
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    declareSeparationHeap
+ * Method:    declareSepHeap
  * Signature: (JJJ)V
  */
 JNIEXPORT void JNICALL
-Java_io_github_cvc5_api_Solver_declareSeparationHeap(JNIEnv* env,
-                                                     jobject,
-                                                     jlong pointer,
-                                                     jlong locSortPointer,
-                                                     jlong dataSortPointer)
+Java_io_github_cvc5_api_Solver_declareSepHeap(JNIEnv* env,
+                                              jobject,
+                                              jlong pointer,
+                                              jlong locSortPointer,
+                                              jlong dataSortPointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
   Sort* locSort = reinterpret_cast<Sort*>(locSortPointer);
   Sort* dataSort = reinterpret_cast<Sort*>(dataSortPointer);
-  solver->declareSeparationHeap(*locSort, *dataSort);
+  solver->declareSepHeap(*locSort, *dataSort);
   CVC5_JAVA_API_TRY_CATCH_END(env);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    getSeparationHeap
+ * Method:    getValueSepHeap
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getSeparationHeap(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getValueSepHeap(
     JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* retPointer = new Term(solver->getSeparationHeap());
+  Term* retPointer = new Term(solver->getValueSepHeap());
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    getSeparationNilTerm
+ * Method:    getValueSepNil
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getSeparationNilTerm(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_getValueSepNil(
     JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* retPointer = new Term(solver->getSeparationNilTerm());
+  Term* retPointer = new Term(solver->getValueSepNil());
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 9504bccae0778ff47db93127f47566e47801e012..a2c2389859c536c8950ef3ab7c99280964cfe800 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -281,9 +281,9 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         vector[Term] getValue(const vector[Term]& terms) except +
         vector[Term] getModelDomainElements(Sort sort) except +
         bint isModelCoreSymbol(Term v) except +
-        void declareSeparationHeap(Sort locSort, Sort dataSort) except +
-        Term getSeparationHeap() except +
-        Term getSeparationNilTerm() except +
+        void declareSepHeap(Sort locSort, Sort dataSort) except +
+        Term getValueSepHeap() except +
+        Term getValueSepNil() except +
         Term declarePool(const string& name, Sort sort, vector[Term]& initValue) except +
         void pop(uint32_t nscopes) except +
         void push(uint32_t nscopes) except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 6f50b840182b0905f646ec59472a6a4311e30867..05138e9bc2de307f944a5550f769fecefc470377 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2047,25 +2047,25 @@ cdef class Solver:
         """
         return self.csolver.isModelCoreSymbol(v.cterm)
 
-    def getSeparationHeap(self):
+    def getValueSepHeap(self):
         """When using separation logic, obtain the term for the heap.
 
         :return: The term for the heap
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.getSeparationHeap()
+        term.cterm = self.csolver.getValueSepHeap()
         return term
 
-    def getSeparationNilTerm(self):
+    def getValueSepNil(self):
         """When using separation logic, obtain the term for nil.
 
         :return: The term for nil
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.getSeparationNilTerm()
+        term.cterm = self.csolver.getValueSepNil()
         return term
 
-    def declareSeparationHeap(self, Sort locType, Sort dataType):
+    def declareSepHeap(self, Sort locType, Sort dataType):
         """
         When using separation logic, this sets the location sort and the
         datatype sort to the given ones. This method should be invoked exactly
@@ -2074,7 +2074,7 @@ cdef class Solver:
         :param locSort: The location sort of the heap
         :param dataSort: The data sort of the heap
         """
-        self.csolver.declareSeparationHeap(locType.csort, dataType.csort)
+        self.csolver.declareSepHeap(locType.csort, dataType.csort)
 
     def declarePool(self, str symbol, Sort sort, initValue):
         """Declare a symbolic pool of terms with the given initial value.

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index c2aa1c5f9d1f3dee981cbc9b8fbce8481ca60ea1..1794765b42e6a1515e1dd1d6249ff2681351e23e 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1470,7 +1470,7 @@ api::Sort DeclareHeapCommand::getDataSort() const { return d_dataSort; }
 
 void DeclareHeapCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
-  solver->declareSeparationHeap(d_locSort, d_dataSort);
+  solver->declareSepHeap(d_locSort, d_dataSort);
 }
 
 Command* DeclareHeapCommand::clone() const

diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp
index 5d0e6b8285a1f1370b4e7e019e5e0b1b781072cf..5795de794e3f5fe95d1396e7a9d446c9387e2fdb 100644 (file)
--- a/test/api/sep_log_api.cpp
+++ b/test/api/sep_log_api.cpp
@@ -83,7 +83,7 @@ int validate_exception(void)
   /* test the heap expression */
   try
   {
-    Term heap_expr = slv.getSeparationHeap();
+    Term heap_expr = slv.getValueSepHeap();
   }
   catch (const CVC5ApiException& e)
   {
@@ -99,7 +99,7 @@ int validate_exception(void)
   /* test the nil expression */
   try
   {
-    Term nil_expr = slv.getSeparationNilTerm();
+    Term nil_expr = slv.getValueSepNil();
   }
   catch (const CVC5ApiException& e)
   {
@@ -138,7 +138,7 @@ int validate_getters(void)
   Sort integer = slv.getIntegerSort();
 
   /** Declare the separation logic heap types */
-  slv.declareSeparationHeap(integer, integer);
+  slv.declareSepHeap(integer, integer);
 
   /* A "random" constant */
   Term random_constant = slv.mkInteger(0xDEADBEEF);
@@ -188,8 +188,8 @@ int validate_getters(void)
   }
 
   /* Obtain our separation logic terms from the solver */
-  Term heap_expr = slv.getSeparationHeap();
-  Term nil_expr = slv.getSeparationNilTerm();
+  Term heap_expr = slv.getValueSepHeap();
+  Term nil_expr = slv.getValueSepNil();
 
   /* If the heap is not a separating conjunction, bail-out */
   if (heap_expr.getKind() != Kind::SEP_STAR)

diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 8e8ed0d9b286cfb6d272a8dbe7ea0666ce25f107..c7398aa3b05d95561e2b43e3135aa8cc9188d1d7 100644 (file)
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -1262,10 +1262,10 @@ def test_get_value3(solver):
 def test_declare_separation_heap(solver):
     solver.setLogic("ALL")
     integer = solver.getIntegerSort()
-    solver.declareSeparationHeap(integer, integer)
+    solver.declareSepHeap(integer, integer)
     # cannot declare separation logic heap more than once
     with pytest.raises(RuntimeError):
-        solver.declareSeparationHeap(integer, integer)
+        solver.declareSepHeap(integer, integer)
 
 
 # Helper function for test_get_separation_{heap,nil}_termX. Asserts and checks
@@ -1273,7 +1273,7 @@ def test_declare_separation_heap(solver):
 def checkSimpleSeparationConstraints(slv):
     integer = slv.getIntegerSort()
     # declare the separation heap
-    slv.declareSeparationHeap(integer, integer)
+    slv.declareSepHeap(integer, integer)
     x = slv.mkConst(integer, "x")
     p = slv.mkConst(integer, "p")
     heap = slv.mkTerm(kinds.SepPto, p, x)
@@ -1290,7 +1290,7 @@ def test_get_separation_heap_term1(solver):
     t = solver.mkTrue()
     solver.assertFormula(t)
     with pytest.raises(RuntimeError):
-        solver.getSeparationHeap()
+        solver.getValueSepHeap()
 
 
 def test_get_separation_heap_term2(solver):
@@ -1299,7 +1299,7 @@ def test_get_separation_heap_term2(solver):
     solver.setOption("produce-models", "false")
     checkSimpleSeparationConstraints(solver)
     with pytest.raises(RuntimeError):
-        solver.getSeparationHeap()
+        solver.getValueSepHeap()
 
 
 def test_get_separation_heap_term3(solver):
@@ -1310,7 +1310,7 @@ def test_get_separation_heap_term3(solver):
     solver.assertFormula(t)
     solver.checkSat()
     with pytest.raises(RuntimeError):
-        solver.getSeparationHeap()
+        solver.getValueSepHeap()
 
 
 def test_get_separation_heap_term4(solver):
@@ -1321,7 +1321,7 @@ def test_get_separation_heap_term4(solver):
     solver.assertFormula(t)
     solver.checkSat()
     with pytest.raises(RuntimeError):
-        solver.getSeparationHeap()
+        solver.getValueSepHeap()
 
 
 def test_get_separation_heap_term5(solver):
@@ -1329,7 +1329,7 @@ def test_get_separation_heap_term5(solver):
     solver.setOption("incremental", "false")
     solver.setOption("produce-models", "true")
     checkSimpleSeparationConstraints(solver)
-    solver.getSeparationHeap()
+    solver.getValueSepHeap()
 
 
 def test_get_separation_nil_term1(solver):
@@ -1339,7 +1339,7 @@ def test_get_separation_nil_term1(solver):
     t = solver.mkTrue()
     solver.assertFormula(t)
     with pytest.raises(RuntimeError):
-        solver.getSeparationNilTerm()
+        solver.getValueSepNil()
 
 
 def test_get_separation_nil_term2(solver):
@@ -1348,7 +1348,7 @@ def test_get_separation_nil_term2(solver):
     solver.setOption("produce-models", "false")
     checkSimpleSeparationConstraints(solver)
     with pytest.raises(RuntimeError):
-        solver.getSeparationNilTerm()
+        solver.getValueSepNil()
 
 
 def test_get_separation_nil_term3(solver):
@@ -1359,7 +1359,7 @@ def test_get_separation_nil_term3(solver):
     solver.assertFormula(t)
     solver.checkSat()
     with pytest.raises(RuntimeError):
-        solver.getSeparationNilTerm()
+        solver.getValueSepNil()
 
 
 def test_get_separation_nil_term4(solver):
@@ -1370,7 +1370,7 @@ def test_get_separation_nil_term4(solver):
     solver.assertFormula(t)
     solver.checkSat()
     with pytest.raises(RuntimeError):
-        solver.getSeparationNilTerm()
+        solver.getValueSepNil()
 
 
 def test_get_separation_nil_term5(solver):
@@ -1378,7 +1378,7 @@ def test_get_separation_nil_term5(solver):
     solver.setOption("incremental", "false")
     solver.setOption("produce-models", "true")
     checkSimpleSeparationConstraints(solver)
-    solver.getSeparationNilTerm()
+    solver.getValueSepNil()
 
 
 def test_push1(solver):

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index e61022e99f46656b1ef989435ef85cfd799edb44..4c9ec4c0d83e287fe8a42364a97614d24d1095d2 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1736,13 +1736,13 @@ class SolverTest
     slv.close();
   }
 
-  @Test void declareSeparationHeap() throws CVC5ApiException
+  @Test void declareSepHeap() throws CVC5ApiException
   {
     d_solver.setLogic("ALL");
     Sort integer = d_solver.getIntegerSort();
-    assertDoesNotThrow(() -> d_solver.declareSeparationHeap(integer, integer));
+    assertDoesNotThrow(() -> d_solver.declareSepHeap(integer, integer));
     // cannot declare separation logic heap more than once
-    assertThrows(CVC5ApiException.class, () -> d_solver.declareSeparationHeap(integer, integer));
+    assertThrows(CVC5ApiException.class, () -> d_solver.declareSepHeap(integer, integer));
   }
 
   /**
@@ -1754,7 +1754,7 @@ class SolverTest
   {
     Sort integer = solver.getIntegerSort();
     // declare the separation heap
-    solver.declareSeparationHeap(integer, integer);
+    solver.declareSepHeap(integer, integer);
     Term x = solver.mkConst(integer, "x");
     Term p = solver.mkConst(integer, "p");
     Term heap = solver.mkTerm(SEP_PTO, p, x);
@@ -1764,26 +1764,26 @@ class SolverTest
     solver.checkSat();
   }
 
-  @Test void getSeparationHeapTerm1() throws CVC5ApiException
+  @Test void getValueSepHeap1() throws CVC5ApiException
   {
     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);
-    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap());
   }
 
-  @Test void getSeparationHeapTerm2() throws CVC5ApiException
+  @Test void getValueSepHeap2() throws CVC5ApiException
   {
     d_solver.setLogic("ALL");
     d_solver.setOption("incremental", "false");
     d_solver.setOption("produce-models", "false");
     checkSimpleSeparationConstraints(d_solver);
-    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap());
   }
 
-  @Test void getSeparationHeapTerm3() throws CVC5ApiException
+  @Test void getValueSepHeap3() throws CVC5ApiException
   {
     d_solver.setLogic("ALL");
     d_solver.setOption("incremental", "false");
@@ -1791,10 +1791,10 @@ class SolverTest
     Term t = d_solver.mkFalse();
     d_solver.assertFormula(t);
     d_solver.checkSat();
-    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap());
   }
 
-  @Test void getSeparationHeapTerm4() throws CVC5ApiException
+  @Test void getValueSepHeap4() throws CVC5ApiException
   {
     d_solver.setLogic("ALL");
     d_solver.setOption("incremental", "false");
@@ -1802,38 +1802,38 @@ class SolverTest
     Term t = d_solver.mkTrue();
     d_solver.assertFormula(t);
     d_solver.checkSat();
-    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap());
   }
 
-  @Test void getSeparationHeapTerm5() throws CVC5ApiException
+  @Test void getValueSepHeap5() throws CVC5ApiException
   {
     d_solver.setLogic("ALL");
     d_solver.setOption("incremental", "false");
     d_solver.setOption("produce-models", "true");
     checkSimpleSeparationConstraints(d_solver);
-    assertDoesNotThrow(() -> d_solver.getSeparationHeap());
+    assertDoesNotThrow(() -> d_solver.getValueSepHeap());
   }
 
-  @Test void getSeparationNilTerm1() throws CVC5ApiException
+  @Test void getValueSepNil1() throws CVC5ApiException
   {
     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);
-    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil());
   }
 
-  @Test void getSeparationNilTerm2() throws CVC5ApiException
+  @Test void getValueSepNil2() throws CVC5ApiException
   {
     d_solver.setLogic("ALL");
     d_solver.setOption("incremental", "false");
     d_solver.setOption("produce-models", "false");
     checkSimpleSeparationConstraints(d_solver);
-    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil());
   }
 
-  @Test void getSeparationNilTerm3() throws CVC5ApiException
+  @Test void getValueSepNil3() throws CVC5ApiException
   {
     d_solver.setLogic("ALL");
     d_solver.setOption("incremental", "false");
@@ -1841,10 +1841,10 @@ class SolverTest
     Term t = d_solver.mkFalse();
     d_solver.assertFormula(t);
     d_solver.checkSat();
-    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil());
   }
 
-  @Test void getSeparationNilTerm4() throws CVC5ApiException
+  @Test void getValueSepNil4() throws CVC5ApiException
   {
     d_solver.setLogic("ALL");
     d_solver.setOption("incremental", "false");
@@ -1852,16 +1852,16 @@ class SolverTest
     Term t = d_solver.mkTrue();
     d_solver.assertFormula(t);
     d_solver.checkSat();
-    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil());
   }
 
-  @Test void getSeparationNilTerm5() throws CVC5ApiException
+  @Test void getValueSepNil5() throws CVC5ApiException
   {
     d_solver.setLogic("ALL");
     d_solver.setOption("incremental", "false");
     d_solver.setOption("produce-models", "true");
     checkSimpleSeparationConstraints(d_solver);
-    assertDoesNotThrow(() -> d_solver.getSeparationNilTerm());
+    assertDoesNotThrow(() -> d_solver.getValueSepNil());
   }
 
   @Test void push1()

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 25abdd108844ef914866999596924b750bec67db..062a2a59e1a7c12c28ccb68fb1949af5b88a4295 100644 (file)
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1685,14 +1685,13 @@ TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct)
   ASSERT_NO_THROW(d_solver.getQuantifierEliminationDisjunct(forall));
 }
 
-TEST_F(TestApiBlackSolver, declareSeparationHeap)
+TEST_F(TestApiBlackSolver, declareSepHeap)
 {
   d_solver.setLogic("ALL");
   Sort integer = d_solver.getIntegerSort();
-  ASSERT_NO_THROW(d_solver.declareSeparationHeap(integer, integer));
+  ASSERT_NO_THROW(d_solver.declareSepHeap(integer, integer));
   // cannot declare separation logic heap more than once
-  ASSERT_THROW(d_solver.declareSeparationHeap(integer, integer),
-               CVC5ApiException);
+  ASSERT_THROW(d_solver.declareSepHeap(integer, integer), CVC5ApiException);
 }
 
 namespace {
@@ -1704,7 +1703,7 @@ void checkSimpleSeparationConstraints(Solver* solver)
 {
   Sort integer = solver->getIntegerSort();
   // declare the separation heap
-  solver->declareSeparationHeap(integer, integer);
+  solver->declareSepHeap(integer, integer);
   Term x = solver->mkConst(integer, "x");
   Term p = solver->mkConst(integer, "p");
   Term heap = solver->mkTerm(cvc5::api::Kind::SEP_PTO, p, x);
@@ -1715,26 +1714,26 @@ void checkSimpleSeparationConstraints(Solver* solver)
 }
 }  // namespace
 
-TEST_F(TestApiBlackSolver, getSeparationHeapTerm1)
+TEST_F(TestApiBlackSolver, getValueSepHeap1)
 {
   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);
-  ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException);
+  ASSERT_THROW(d_solver.getValueSepHeap(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSolver, getSeparationHeapTerm2)
+TEST_F(TestApiBlackSolver, getValueSepHeap2)
 {
   d_solver.setLogic("ALL");
   d_solver.setOption("incremental", "false");
   d_solver.setOption("produce-models", "false");
   checkSimpleSeparationConstraints(&d_solver);
-  ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException);
+  ASSERT_THROW(d_solver.getValueSepHeap(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSolver, getSeparationHeapTerm3)
+TEST_F(TestApiBlackSolver, getValueSepHeap3)
 {
   d_solver.setLogic("ALL");
   d_solver.setOption("incremental", "false");
@@ -1742,10 +1741,10 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm3)
   Term t = d_solver.mkFalse();
   d_solver.assertFormula(t);
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException);
+  ASSERT_THROW(d_solver.getValueSepHeap(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSolver, getSeparationHeapTerm4)
+TEST_F(TestApiBlackSolver, getValueSepHeap4)
 {
   d_solver.setLogic("ALL");
   d_solver.setOption("incremental", "false");
@@ -1753,38 +1752,38 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm4)
   Term t = d_solver.mkTrue();
   d_solver.assertFormula(t);
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException);
+  ASSERT_THROW(d_solver.getValueSepHeap(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSolver, getSeparationHeapTerm5)
+TEST_F(TestApiBlackSolver, getValueSepHeap5)
 {
   d_solver.setLogic("ALL");
   d_solver.setOption("incremental", "false");
   d_solver.setOption("produce-models", "true");
   checkSimpleSeparationConstraints(&d_solver);
-  ASSERT_NO_THROW(d_solver.getSeparationHeap());
+  ASSERT_NO_THROW(d_solver.getValueSepHeap());
 }
 
-TEST_F(TestApiBlackSolver, getSeparationNilTerm1)
+TEST_F(TestApiBlackSolver, getValueSepNil1)
 {
   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);
-  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException);
+  ASSERT_THROW(d_solver.getValueSepNil(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSolver, getSeparationNilTerm2)
+TEST_F(TestApiBlackSolver, getValueSepNil2)
 {
   d_solver.setLogic("ALL");
   d_solver.setOption("incremental", "false");
   d_solver.setOption("produce-models", "false");
   checkSimpleSeparationConstraints(&d_solver);
-  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException);
+  ASSERT_THROW(d_solver.getValueSepNil(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSolver, getSeparationNilTerm3)
+TEST_F(TestApiBlackSolver, getValueSepNil3)
 {
   d_solver.setLogic("ALL");
   d_solver.setOption("incremental", "false");
@@ -1792,10 +1791,10 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm3)
   Term t = d_solver.mkFalse();
   d_solver.assertFormula(t);
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException);
+  ASSERT_THROW(d_solver.getValueSepNil(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSolver, getSeparationNilTerm4)
+TEST_F(TestApiBlackSolver, getValueSepNil4)
 {
   d_solver.setLogic("ALL");
   d_solver.setOption("incremental", "false");
@@ -1803,16 +1802,16 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm4)
   Term t = d_solver.mkTrue();
   d_solver.assertFormula(t);
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException);
+  ASSERT_THROW(d_solver.getValueSepNil(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSolver, getSeparationNilTerm5)
+TEST_F(TestApiBlackSolver, getValueSepNil5)
 {
   d_solver.setLogic("ALL");
   d_solver.setOption("incremental", "false");
   d_solver.setOption("produce-models", "true");
   checkSimpleSeparationConstraints(&d_solver);
-  ASSERT_NO_THROW(d_solver.getSeparationNilTerm());
+  ASSERT_NO_THROW(d_solver.getValueSepNil());
 }
 
 TEST_F(TestApiBlackSolver, push1)