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

4 files changed, 66 insertions, 67 deletions

diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp
index 5d0e6b828..5795de794 100644
--- 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 8e8ed0d9b..c7398aa3b 100644
--- 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 e61022e99..4c9ec4c0d 100644
--- 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 25abdd108..062a2a59e 100644
--- 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)