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).

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 8a583a6717933e63a6dc56093de9e957ee002b7c..c0818f54f60ee52ccc125c34f398366bb17330bc 100644 (file)
--- 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 e18e3ac6b2581d0ccb730e01393dd233590c1eb9..1f74a34a9e21c79478574a8f9b62f14820f65bf5 100644 (file)
--- 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 29e57ef63f40bfe69b3e43aeb1478c06fe30814c..d4082163adff3d81203b68a630752f97a0b268c3 100644 (file)
--- 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()