diff options
Diffstat (limited to 'test/unit/api/solver_black.h')
-rw-r--r-- | test/unit/api/solver_black.h | 65 |
1 files changed, 54 insertions, 11 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 9837d6b00..11dbbb7ae 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -27,12 +27,14 @@ class SolverBlack : public CxxTest::TestSuite void setUp() override; void tearDown() override; + void testSupportsFloatingPoint(); + void testGetBooleanSort(); void testGetIntegerSort(); void testGetNullSort(); void testGetRealSort(); void testGetRegExpSort(); - void testGetRoundingmodeSort(); + void testGetRoundingModeSort(); void testGetStringSort(); void testMkArraySort(); @@ -169,6 +171,20 @@ void SolverBlack::setUp() { d_solver.reset(new Solver()); } void SolverBlack::tearDown() { d_solver.reset(nullptr); } +void SolverBlack::testSupportsFloatingPoint() +{ + if (d_solver->supportsFloatingPoint()) + { + TS_ASSERT_THROWS_NOTHING( + d_solver->mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN)); + } + else + { + TS_ASSERT_THROWS(d_solver->mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN), + CVC4ApiException&); + } +} + void SolverBlack::testGetBooleanSort() { TS_ASSERT_THROWS_NOTHING(d_solver->getBooleanSort()); @@ -199,9 +215,16 @@ void SolverBlack::testGetStringSort() TS_ASSERT_THROWS_NOTHING(d_solver->getStringSort()); } -void SolverBlack::testGetRoundingmodeSort() +void SolverBlack::testGetRoundingModeSort() { - TS_ASSERT_THROWS_NOTHING(d_solver->getRoundingmodeSort()); + if (d_solver->supportsFloatingPoint()) + { + TS_ASSERT_THROWS_NOTHING(d_solver->getRoundingModeSort()); + } + else + { + TS_ASSERT_THROWS(d_solver->getRoundingModeSort(), CVC4ApiException&); + } } void SolverBlack::testMkArraySort() @@ -210,15 +233,20 @@ void SolverBlack::testMkArraySort() Sort intSort = d_solver->getIntegerSort(); Sort realSort = d_solver->getRealSort(); Sort bvSort = d_solver->mkBitVectorSort(32); - Sort fpSort = d_solver->mkFloatingPointSort(3, 5); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, boolSort)); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(intSort, intSort)); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, realSort)); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, bvSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(fpSort, fpSort)); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, intSort)); TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, bvSort)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort)); + + if (d_solver->supportsFloatingPoint()) + { + Sort fpSort = d_solver->mkFloatingPointSort(3, 5); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(fpSort, fpSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort)); + } + Solver slv; TS_ASSERT_THROWS(slv.mkArraySort(boolSort, boolSort), CVC4ApiException&); } @@ -231,9 +259,16 @@ void SolverBlack::testMkBitVectorSort() void SolverBlack::testMkFloatingPointSort() { - TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPointSort(4, 8)); - TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(0, 8), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 0), CVC4ApiException&); + if (d_solver->supportsFloatingPoint()) + { + TS_ASSERT_THROWS_NOTHING(d_solver->mkFloatingPointSort(4, 8)); + TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(0, 8), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 0), CVC4ApiException&); + } + else + { + TS_ASSERT_THROWS(d_solver->mkFloatingPointSort(4, 8), CVC4ApiException&); + } } void SolverBlack::testMkDatatypeSort() @@ -480,8 +515,16 @@ void SolverBlack::testMkBoolean() void SolverBlack::testMkRoundingMode() { - TS_ASSERT_THROWS_NOTHING( - d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + TS_ASSERT_THROWS_NOTHING( + d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); + } + else + { + TS_ASSERT_THROWS(d_solver->mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO), + CVC4ApiException&); + } } void SolverBlack::testMkUninterpretedConst() |