From 99278c017e5b198b416d4a82b0ea63f99d02e739 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 3 Jan 2019 17:55:45 +0100 Subject: [PATCH] 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). --- src/api/cvc4cpp.cpp | 3 +++ src/api/cvc4cpp.h | 4 ++-- test/unit/api/solver_black.h | 13 ++++++++++--- 3 files changed, 15 insertions(+), 5 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 8a583a671..c0818f54f 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -16,6 +16,7 @@ #include "api/cvc4cpp.h" +#include "base/configuration.h" #include "base/cvc4_assert.h" #include "base/cvc4_check.h" #include "expr/expr.h" @@ -2325,6 +2326,8 @@ Term Solver::mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const { + CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) + << "Expected CVC4 to be compiled with SymFPU support"; CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_FLOATINGPOINT, kind) << "CONST_FLOATINGPOINT"; CVC4_API_ARG_CHECK_EXPECTED(arg1 > 0, arg1) << "a value > 0"; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index e18e3ac6b..1f74a34a9 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1969,7 +1969,7 @@ class CVC4_PUBLIC Solver * @param val the value of the constant * @return the bit-vector constant */ - Term mkBitVector(uint32_t size, uint64_t val) const; + Term mkBitVector(uint32_t size, uint64_t val = 0) const; /** * Create a bit-vector constant from a given string. @@ -2157,7 +2157,7 @@ class CVC4_PUBLIC Solver /** * Create constant of kind: - * - CONST_FLOATINGPOINT + * - CONST_FLOATINGPOINT (requires CVC4 to be compiled with symFPU support) * See enum Kind for a description of the parameters. * @param kind the kind of the constant * @param arg1 the first argument to this kind 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 #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() -- 2.30.2