diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-03 17:55:45 +0100 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-01-03 08:55:45 -0800 |
commit | 99278c017e5b198b416d4a82b0ea63f99d02e739 (patch) | |
tree | b23fe16f9043d4358059bd9a0ff1b86cd92b586d /test/unit/api | |
parent | f179953e2fea6955650ccde8414f2ccd8ee6f63b (diff) |
C++ API: Reintroduce zero-value mkBitVector method (#2770)
PR #2764 removed `Solver::mkBitVector(uint32_t)` (returns a bit-vector
of a given size with value zero), which made the build fail when SymFPU
was enabled because solver_black used it for SymFPU-enabled builds. This
commit simply adds a zero default argument to `mkBitVector(uint32_t,
uint64_t)` to allow users to create zero-valued bit-vectors without
explicitly specifying the value again. Additionally, the commit replaces
the use of the `CVC4_USE_SYMFPU` macro by a call to
`Configuration::isBuiltWithSymFPU()`, making sure that we can catch
compile-time errors regardless of configuration. Finally,
`Solver::mkConst(Kind, uint32_t, uint32_t, Term)` now checks whether
CVC4 has been compiled with SymFPU when creating a `CONST_FLOATINGPOINT`
and throws an exception otherwise (solver_black has been updated
correspondingly).
Diffstat (limited to 'test/unit/api')
-rw-r--r-- | test/unit/api/solver_black.h | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 29e57ef63..d4082163a 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -17,6 +17,7 @@ #include <cxxtest/TestSuite.h> #include "api/cvc4cpp.h" +#include "base/configuration.h" using namespace CVC4::api; @@ -371,11 +372,18 @@ void SolverBlack::testMkConst() TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_BITVECTOR, val2, val2)); // mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const -#ifdef CVC4_USE_SYMFPU Term t1 = d_solver.mkBitVector(8); Term t2 = d_solver.mkBitVector(4); Term t3 = d_solver.mkReal(2); - TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t1)); + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t1)); + } + else + { + TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t1), + CVC4ApiException&); + } TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 0, 5, Term()), CVC4ApiException&); TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 0, 5, t1), @@ -388,7 +396,6 @@ void SolverBlack::testMkConst() CVC4ApiException&); TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, 3, 5, t1), CVC4ApiException&); -#endif } void SolverBlack::testMkEmptySet() |