diff options
Diffstat (limited to 'test/unit/api/solver_black.h')
-rw-r--r-- | test/unit/api/solver_black.h | 134 |
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"); |