From a517a9127e0ef70424364d093bb21be64891dd0d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 3 Nov 2021 15:04:34 -0700 Subject: [PATCH] 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 --- src/api/cpp/cvc5.cpp | 7 ++- src/api/cpp/cvc5.h | 6 +-- src/api/java/io/github/cvc5/api/Solver.java | 19 ++++---- src/api/java/jni/solver.cpp | 26 +++++------ src/api/python/cvc5.pxd | 6 +-- src/api/python/cvc5.pxi | 12 ++--- src/smt/command.cpp | 2 +- test/api/sep_log_api.cpp | 10 ++--- test/python/unit/api/test_solver.py | 26 +++++------ test/unit/api/java/SolverTest.java | 48 ++++++++++---------- test/unit/api/solver_black.cpp | 49 ++++++++++----------- 11 files changed, 104 insertions(+), 107 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index d1be25bb4..0450ac06a 100644 --- 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 63dadaef6..f348ae4e5 100644 --- 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 6c1399d9c..0479dce3d 100644 --- 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 2d775c545..cb4d58591 100644 --- 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(pointer); Sort* locSort = reinterpret_cast(locSortPointer); Sort* dataSort = reinterpret_cast(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(pointer); - Term* retPointer = new Term(solver->getSeparationHeap()); + Term* retPointer = new Term(solver->getValueSepHeap()); return reinterpret_cast(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(pointer); - Term* retPointer = new Term(solver->getSeparationNilTerm()); + Term* retPointer = new Term(solver->getValueSepNil()); return reinterpret_cast(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 9504bccae..a2c238985 100644 --- 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 6f50b8401..05138e9bc 100644 --- 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 c2aa1c5f9..1794765b4 100644 --- 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 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) -- 2.30.2