diff options
61 files changed, 86 insertions, 658 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index b555c7bdc..b29585f3b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -128,7 +128,6 @@ cvc5_option(USE_EDITLINE "Use Editline for better interactive support") # > for options where we don't need to detect if set by user (default: OFF) option(USE_POLY "Use LibPoly for polynomial arithmetic") option(USE_COCOA "Use CoCoALib for further polynomial operations") -option(USE_SYMFPU "Use SymFPU for floating point support") option(USE_PYTHON2 "Force Python 2 (deprecated)") # Custom install directories for dependencies @@ -476,13 +475,7 @@ if(USE_EDITLINE) endif() endif() -if(USE_SYMFPU) - find_package(SymFPU REQUIRED) - add_definitions(-DCVC5_USE_SYMFPU) - set(CVC5_USE_SYMFPU 1) -else() - set(CVC5_USE_SYMFPU 0) -endif() +find_package(SymFPU REQUIRED) if(GPL_LIBS) if(NOT ENABLE_GPL) @@ -673,7 +666,6 @@ else() print_config("MP library " "gmp") endif() print_config("Editline " ${USE_EDITLINE}) -print_config("SymFPU " ${USE_SYMFPU}) message("") print_config("Api docs " ${BUILD_DOCS}) message("") diff --git a/INSTALL.md b/INSTALL.md index 41f770288..1a9c03476 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -57,6 +57,7 @@ minimum versions; more recent versions should be compatible. - [GMP v6.1 (GNU Multi-Precision arithmetic library)](https://gmplib.org) - [ANTLR 3.4](http://www.antlr3.org/) - [Java >= 1.6](https://www.java.com) +- [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4) ### ANTLR 3.4 parser generator @@ -74,8 +75,6 @@ cross-compile, or you want to build cvc5 statically but the distribution does not ship static libraries, cvc5 builds GMP automatically when `--auto-download` is given. -## Optional Dependencies - ### SymFPU (Support for the Theory of Floating Point Numbers) [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4) @@ -83,7 +82,8 @@ is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms of bit-vector operations. It is required for supporting the theory of floating-point numbers and can be downloaded and built automatically. -Configure cvc5 with `configure.sh --symfpu` to build with this dependency. + +## Optional Dependencies ### CaDiCaL (Optional SAT solver) @@ -4,6 +4,7 @@ Changes since CVC4 1.8 ====================== New Features: +* SymFPU is now a required dependency. * New unsat-core production modes based on the new proof infrastructure (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature of Minisat (`--unsat-cores-mode=assumptions`). The mode based on SAT diff --git a/configure.sh b/configure.sh index 487bbcb5a..25203f8a6 100755 --- a/configure.sh +++ b/configure.sh @@ -64,7 +64,6 @@ The following flags enable optional packages (disable with --no-<option name>). --kissat use the Kissat SAT solver --poly use the LibPoly library [default=yes] --cocoa use the CoCoA library - --symfpu use SymFPU for floating point solver [default=yes] --editline support the editline library Optional Path to Optional Packages: @@ -133,7 +132,6 @@ editline=default shared=default static_binary=default statistics=default -symfpu=ON tracing=default tsan=default ubsan=default @@ -260,9 +258,6 @@ do --statistics) statistics=ON;; --no-statistics) statistics=OFF;; - --symfpu) symfpu=ON;; - --no-symfpu) symfpu=OFF;; - --tracing) tracing=ON;; --no-tracing) tracing=OFF;; @@ -398,8 +393,6 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_POLY=$poly" [ $cocoa != default ] \ && cmake_opts="$cmake_opts -DUSE_COCOA=$cocoa" -[ $symfpu != default ] \ - && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu" [ "$abc_dir" != default ] \ && cmake_opts="$cmake_opts -DABC_DIR=$abc_dir" [ "$glpk_dir" != default ] \ diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java index 61ab18148..46f8b8330 100644 --- a/examples/api/java/FloatingPointArith.java +++ b/examples/api/java/FloatingPointArith.java @@ -27,13 +27,6 @@ public class FloatingPointArith { System.loadLibrary("cvc4jni"); // Test whether CVC4 was built with floating-point support - if (!Configuration.isBuiltWithSymFPU()) { - System.out.println("CVC4 was built without floating-point support."); - System.out.println("Configure with --symfpu and rebuild CVC4 to run"); - System.out.println("this example."); - System.exit(77); - } - ExprManager em = new ExprManager(); SmtEngine smt = new SmtEngine(em); diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index 66b18642d..0001f726b 100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -22,12 +22,6 @@ from pycvc5 import kinds if __name__ == "__main__": slv = pycvc5.Solver() - if not slv.supportsFloatingPoint(): - # cvc5 must be built with SymFPU to support the theory of - # floating-point numbers - print("cvc5 was not built with floating-point support.") - exit() - slv.setOption("produce-models", "true") slv.setLogic("QF_FP") diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2419e1e41..d7da67cbe 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1204,9 +1204,8 @@ endif() if(USE_POLY) target_link_libraries(cvc5 PRIVATE Polyxx) endif() -if(USE_SYMFPU) - target_link_libraries(cvc5 PRIVATE SymFPU) -endif() + +target_link_libraries(cvc5 PRIVATE SymFPU) # Note: When linked statically GMP needs to be linked after CLN since CLN # depends on GMP. diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 307222988..43bb3d2dc 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5197,18 +5197,6 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const << " children (the one under construction has " << nchildren << ")"; } -/* Solver Configuration */ -/* -------------------------------------------------------------------------- */ - -bool Solver::supportsFloatingPoint() const -{ - CVC5_API_TRY_CATCH_BEGIN; - //////// all checks before this line - return Configuration::isBuiltWithSymFPU(); - //////// - CVC5_API_TRY_CATCH_END; -} - /* Sorts Handling */ /* -------------------------------------------------------------------------- */ @@ -5276,8 +5264,6 @@ Sort Solver::getRoundingModeSort(void) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return Sort(this, getNodeManager()->roundingModeType()); //////// @@ -5314,8 +5300,6 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0"; CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0"; //////// all checks before this line @@ -5794,8 +5778,6 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( FloatingPoint::makeInf(FloatingPointSize(exp, sig), false)); @@ -5807,8 +5789,6 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( FloatingPoint::makeInf(FloatingPointSize(exp, sig), true)); @@ -5820,8 +5800,6 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( FloatingPoint::makeNaN(FloatingPointSize(exp, sig))); @@ -5833,8 +5811,6 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( FloatingPoint::makeZero(FloatingPointSize(exp, sig), false)); @@ -5846,8 +5822,6 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( FloatingPoint::makeZero(FloatingPointSize(exp, sig), true)); @@ -5859,8 +5833,6 @@ Term Solver::mkRoundingMode(RoundingMode rm) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; //////// all checks before this line return mkValHelper<cvc5::RoundingMode>(s_rmodes.at(rm)); //////// @@ -5914,8 +5886,6 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(Configuration::isBuiltWithSymFPU()) - << "Expected cvc5 to be compiled with SymFPU support"; CVC5_API_SOLVER_CHECK_TERM(val); CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0"; CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0"; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index a1421cf12..161522654 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2752,12 +2752,6 @@ class CVC5_EXPORT Solver Solver& operator=(const Solver&) = delete; /* .................................................................... */ - /* Solver Configuration */ - /* .................................................................... */ - - bool supportsFloatingPoint() const; - - /* .................................................................... */ /* Sorts Handling */ /* .................................................................... */ diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index fdc1872e7..9d980267d 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -151,7 +151,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": cdef cppclass Solver: Solver(Options*) except + - bint supportsFloatingPoint() except + Sort getBooleanSort() except + Sort getIntegerSort() except + Sort getRealSort() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 258005207..874c63c3d 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -460,9 +460,6 @@ cdef class Solver: def __dealloc__(self): del self.csolver - def supportsFloatingPoint(self): - return self.csolver.supportsFloatingPoint() - def getBooleanSort(self): cdef Sort sort = Sort(self) sort.csort = self.csolver.getBooleanSort() diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 61951841b..1befb34ea 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -123,7 +123,6 @@ std::string Configuration::copyright() { if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical() || Configuration::isBuiltWithCryptominisat() || Configuration::isBuiltWithKissat() - || Configuration::isBuiltWithSymFPU() || Configuration::isBuiltWithEditline()) { ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n" @@ -151,12 +150,6 @@ std::string Configuration::copyright() { << " See https://fmv.jku.at/kissat for copyright " << "information.\n\n"; } - if (Configuration::isBuiltWithSymFPU()) - { - ss << " SymFPU - The Symbolic Floating Point Unit\n" - << " See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright " - << "information.\n\n"; - } if (Configuration::isBuiltWithEditline()) { ss << " Editline Library\n" @@ -165,6 +158,10 @@ std::string Configuration::copyright() { } } + ss << " SymFPU - The Symbolic Floating Point Unit\n" + << " See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright " + << "information.\n\n"; + if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly()) { ss << "This version of cvc5 is linked against the following third party\n" @@ -259,8 +256,6 @@ bool Configuration::isBuiltWithPoly() return IS_POLY_BUILD; } -bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; } - unsigned Configuration::getNumDebugTags() { #if defined(CVC5_DEBUG) && defined(CVC5_TRACING) /* -1 because a NULL pointer is inserted as the last value */ diff --git a/src/base/configuration.h b/src/base/configuration.h index 78e86f920..2a7df1b4a 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -113,8 +113,6 @@ public: static bool isBuiltWithPoly(); - static bool isBuiltWithSymFPU(); - /* Return the number of debug tags */ static unsigned getNumDebugTags(); /* Return a sorted array of the debug tags name */ diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 3027b23bc..39c5e89e9 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -126,12 +126,6 @@ namespace cvc5 { #define IS_EDITLINE_BUILD false #endif /* HAVE_LIBEDITLINE */ -#ifdef CVC5_USE_SYMFPU -#define IS_SYMFPU_BUILD true -#else /* HAVE_SYMFPU_HEADERS */ -#define IS_SYMFPU_BUILD false -#endif /* HAVE_SYMFPU_HEADERS */ - #if CVC5_GPL_DEPS # define IS_GPL_BUILD true #else /* CVC5_GPL_DEPS */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index e109ab44c..d31d2e58f 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -403,7 +403,6 @@ void OptionsHandler::showConfiguration(const std::string& option, print_config_cond("kissat", Configuration::isBuiltWithKissat()); print_config_cond("poly", Configuration::isBuiltWithPoly()); print_config_cond("editline", Configuration::isBuiltWithEditline()); - print_config_cond("symfpu", Configuration::isBuiltWithSymFPU()); exit(0); } diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 0d1b25549..0e196c0e0 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -23,7 +23,6 @@ #include "util/floatingpoint.h" #include "util/floatingpoint_literal_symfpu.h" -#ifdef CVC5_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" #include "symfpu/core/compare.h" @@ -38,9 +37,7 @@ #include "symfpu/core/sqrt.h" #include "symfpu/utils/numberOfRoundingModes.h" #include "symfpu/utils/properties.h" -#endif -#ifdef CVC5_USE_SYMFPU namespace symfpu { using namespace ::cvc5::theory::fp::symfpuSymbolic; @@ -143,11 +140,6 @@ void probabilityAnnotation<traits, traits::prop>(const traits::prop &p, return; } }; -#endif - -#ifndef CVC5_USE_SYMFPU -#define SYMFPU_NUMBER_OF_ROUNDING_MODES 5 -#endif namespace cvc5 { namespace theory { @@ -242,11 +234,7 @@ symbolicProposition symbolicProposition::operator^( bool symbolicRoundingMode::checkNodeType(const TNode n) { -#ifdef CVC5_USE_SYMFPU return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES); -#else - return false; -#endif } symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n) @@ -254,7 +242,6 @@ symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n) Assert(checkNodeType(*this)); } -#ifdef CVC5_USE_SYMFPU symbolicRoundingMode::symbolicRoundingMode(const unsigned v) : nodeWrapper(NodeManager::currentNM()->mkConst( BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v))) @@ -262,14 +249,6 @@ symbolicRoundingMode::symbolicRoundingMode(const unsigned v) Assert((v & (v - 1)) == 0 && v != 0); // Exactly one bit set Assert(checkNodeType(*this)); } -#else -symbolicRoundingMode::symbolicRoundingMode(const unsigned v) - : nodeWrapper(NodeManager::currentNM()->mkConst( - BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v))) -{ - Unreachable(); -} -#endif symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old) : nodeWrapper(old) @@ -755,20 +734,17 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const FpConverter::FpConverter(context::UserContext* user) : d_additionalAssertions(user) -#ifdef CVC5_USE_SYMFPU , d_fpMap(user), d_rmMap(user), d_boolMap(user), d_ubvMap(user), d_sbvMap(user) -#endif { } FpConverter::~FpConverter() {} -#ifdef CVC5_USE_SYMFPU Node FpConverter::ufToNode(const fpt &format, const uf &u) const { NodeManager *nm = NodeManager::currentNM(); @@ -843,7 +819,6 @@ FpConverter::uf FpConverter::buildComponents(TNode current) return tmp; } -#endif // Non-convertible things should only be added to the stack at the very start, // thus... @@ -851,7 +826,6 @@ FpConverter::uf FpConverter::buildComponents(TNode current) Node FpConverter::convert(TNode node) { -#ifdef CVC5_USE_SYMFPU std::vector<TNode> workStack; TNode result = node; @@ -1704,9 +1678,6 @@ Node FpConverter::convert(TNode node) } return result; -#else - Unimplemented() << "Conversion is dependent on SymFPU"; -#endif } #undef CVC5_FPCONV_PASSTHROUGH @@ -1715,7 +1686,6 @@ Node FpConverter::getValue(Valuation &val, TNode var) { Assert(Theory::isLeafOf(var, THEORY_FP)); -#ifdef CVC5_USE_SYMFPU TypeNode t(var.getType()); Assert(t.isRoundingMode() || t.isFloatingPoint()) @@ -1735,9 +1705,6 @@ Node FpConverter::getValue(Valuation &val, TNode var) Assert(i != d_fpMap.end()) << "Asking for the value of an unregistered expression"; return ufToNode(fpt(t), (*i).second); -#else - Unimplemented() << "Conversion is dependent on SymFPU"; -#endif } } // namespace fp diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index f1b7c8a83..9900c2987 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -33,9 +33,7 @@ #include "util/floatingpoint_size.h" #include "util/hash.h" -#ifdef CVC5_USE_SYMFPU #include "symfpu/core/unpackedFloat.h" -#endif #ifdef CVC5_SYM_SYMBOLIC_EVAL // This allows debugging of the cvc5 symbolic back-end. @@ -120,9 +118,7 @@ class symbolicProposition : public nodeWrapper protected: bool checkNodeType(const TNode node); -#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicProposition>; // For ITE -#endif public: symbolicProposition(const Node n); @@ -141,9 +137,7 @@ class symbolicRoundingMode : public nodeWrapper protected: bool checkNodeType(const TNode n); -#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>; // For ITE -#endif public: symbolicRoundingMode(const Node n); @@ -183,10 +177,8 @@ class symbolicBitVector : public nodeWrapper bool checkNodeType(const TNode n); friend symbolicBitVector<!isSigned>; // To allow conversion between the types -#ifdef CVC5_USE_SYMFPU friend ::symfpu::ite<symbolicProposition, symbolicBitVector<isSigned> >; // For ITE -#endif public: symbolicBitVector(const Node n); @@ -314,7 +306,6 @@ class FpConverter context::CDList<Node> d_additionalAssertions; protected: -#ifdef CVC5_USE_SYMFPU typedef symfpuSymbolic::traits traits; typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf; typedef symfpuSymbolic::traits::rm rm; @@ -348,7 +339,6 @@ class FpConverter /* Creates the relevant components for a variable */ uf buildComponents(TNode current); -#endif }; } // namespace fp diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 3d81a2995..77dba0724 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -661,7 +661,7 @@ bool TheoryFp::isRegistered(TNode node) { void TheoryFp::preRegisterTerm(TNode node) { - if (Configuration::isBuiltWithSymFPU() && !options::fpExp()) + if (!options::fpExp()) { TypeNode tn = node.getType(); if (tn.isFloatingPoint()) diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 76f7d55cf..8bc7900de 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -1026,12 +1026,10 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) bool result; switch (k) { -#ifdef CVC5_USE_SYMFPU case kind::FLOATINGPOINT_COMPONENT_NAN: result = arg0.isNaN(); break; case kind::FLOATINGPOINT_COMPONENT_INF: result = arg0.isInfinite(); break; case kind::FLOATINGPOINT_COMPONENT_ZERO: result = arg0.isZero(); break; case kind::FLOATINGPOINT_COMPONENT_SIGN: result = arg0.getSign(); break; -#endif default: Unreachable() << "Unknown kind used in componentFlag"; break; } @@ -1050,11 +1048,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) // \todo Add a proper interface for this sort of thing to FloatingPoint #1915 return RewriteResponse( REWRITE_DONE, -#ifdef CVC5_USE_SYMFPU NodeManager::currentNM()->mkConst((BitVector)arg0.getExponent()) -#else - node -#endif ); } @@ -1066,11 +1060,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) return RewriteResponse( REWRITE_DONE, -#ifdef CVC5_USE_SYMFPU NodeManager::currentNM()->mkConst((BitVector)arg0.getSignificand()) -#else - node -#endif ); } @@ -1080,7 +1070,6 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) BitVector value; -#ifdef CVC5_USE_SYMFPU /* \todo fix the numbering of rounding modes so this doesn't need * to call symfpu at all and remove the dependency on fp_converter.h #1915 */ RoundingMode arg0(node[0].getConst<RoundingMode>()); @@ -1110,9 +1099,6 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) Unreachable() << "Unknown rounding mode in roundingModeBitBlast"; break; } -#else - value = BitVector(5U, 0U); -#endif return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(value)); } diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp index b78ef24c7..77c1ef8f0 100644 --- a/src/theory/fp/theory_fp_type_rules.cpp +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -727,7 +727,6 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager, } } -#ifdef CVC5_USE_SYMFPU /* Need to create some symfpu objects as the size of bit-vector * that is needed for this component is dependent on the encoding * used (i.e. whether subnormals are forcibly normalised or not). @@ -735,9 +734,6 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager, * back-end but it should't make a difference. */ FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); uint32_t bw = FloatingPoint::getUnpackedExponentWidth(fps); -#else - uint32_t bw = 2; -#endif return nodeManager->mkBitVectorType(bw); } @@ -767,13 +763,9 @@ TypeNode FloatingPointComponentSignificand::computeType( } } -#ifdef CVC5_USE_SYMFPU /* As before we need to use some of sympfu. */ FloatingPointSize fps = operandType.getConst<FloatingPointSize>(); uint32_t bw = FloatingPoint::getUnpackedSignificandWidth(fps); -#else - uint32_t bw = 1; -#endif return nodeManager->mkBitVectorType(bw); } diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 8ba43aa1a..d53b06151 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -44,10 +44,6 @@ LogicInfo::LogicInfo() { for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { - if (id == THEORY_FP && !Configuration::isBuiltWithSymFPU()) - { - continue; - } enableTheory(id); } } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 2938ddcca..71742dfce 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -13,9 +13,6 @@ # The build system configuration. ## -configure_file(floatingpoint_literal_symfpu.h.in floatingpoint_literal_symfpu.h) -configure_file(floatingpoint_literal_symfpu_traits.h.in - floatingpoint_literal_symfpu_traits.h) configure_file(rational.h.in rational.h) configure_file(integer.h.in integer.h) configure_file(real_algebraic_number.h.in real_algebraic_number.h) diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp index c2c3fe77b..dc3dce6b9 100644 --- a/src/util/floatingpoint_literal_symfpu.cpp +++ b/src/util/floatingpoint_literal_symfpu.cpp @@ -16,7 +16,6 @@ #include "base/check.h" -#ifdef CVC5_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" #include "symfpu/core/compare.h" @@ -31,11 +30,9 @@ #include "symfpu/core/sqrt.h" #include "symfpu/utils/numberOfRoundingModes.h" #include "symfpu/utils/properties.h" -#endif /* -------------------------------------------------------------------------- */ -#ifdef CVC5_USE_SYMFPU namespace symfpu { #define CVC5_LIT_ITE_DFN(T) \ @@ -57,7 +54,6 @@ CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::ubv); #undef CVC5_LIT_ITE_DFN } // namespace symfpu -#endif /* -------------------------------------------------------------------------- */ @@ -65,44 +61,30 @@ namespace cvc5 { uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size) { -#ifdef CVC5_USE_SYMFPU return SymFPUUnpackedFloatLiteral::exponentWidth(size); -#else - unimplemented(); - return 2; -#endif } uint32_t FloatingPointLiteral::getUnpackedSignificandWidth( FloatingPointSize& size) { -#ifdef CVC5_USE_SYMFPU return SymFPUUnpackedFloatLiteral::significandWidth(size); -#else - unimplemented(); - return 2; -#endif } FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size, uint32_t sig_size, const BitVector& bv) : d_fp_size(exp_size, sig_size) -#ifdef CVC5_USE_SYMFPU , d_symuf(symfpu::unpack<symfpuLiteral::traits>( symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv)) -#endif { } FloatingPointLiteral::FloatingPointLiteral( const FloatingPointSize& size, FloatingPointLiteral::SpecialConstKind kind) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(SymFPUUnpackedFloatLiteral::makeNaN(size)) -#endif { Assert(kind == FloatingPointLiteral::SpecialConstKind::FPNAN); } @@ -112,12 +94,10 @@ FloatingPointLiteral::FloatingPointLiteral( FloatingPointLiteral::SpecialConstKind kind, bool sign) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(kind == FloatingPointLiteral::SpecialConstKind::FPINF ? SymFPUUnpackedFloatLiteral::makeInf(size, sign) : SymFPUUnpackedFloatLiteral::makeZero(size, sign)) -#endif { Assert(kind == FloatingPointLiteral::SpecialConstKind::FPINF || kind == FloatingPointLiteral::SpecialConstKind::FPZERO); @@ -126,10 +106,8 @@ FloatingPointLiteral::FloatingPointLiteral( FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv)) -#endif { } @@ -138,7 +116,6 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv, bool signedBV) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>( symfpuLiteral::Cvc5FPSize(size), @@ -148,97 +125,61 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, symfpuLiteral::Cvc5FPSize(size), symfpuLiteral::Cvc5RM(rm), symfpuLiteral::Cvc5UnsignedBitVector(bv))) -#endif { } BitVector FloatingPointLiteral::pack(void) const { -#ifdef CVC5_USE_SYMFPU BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf)); -#else - unimplemented(); - BitVector bv(4u, 0u); -#endif return bv; } FloatingPointLiteral FloatingPointLiteral::absolute(void) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::negate(void) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::add( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::add<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf, true)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::sub( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::add<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf, false)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::mult( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::multiply<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::div( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::divide<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::fma( @@ -246,276 +187,150 @@ FloatingPointLiteral FloatingPointLiteral::fma( const FloatingPointLiteral& arg1, const FloatingPointLiteral& arg2) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg1.d_fp_size); Assert(d_fp_size == arg2.d_fp_size); return FloatingPointLiteral( d_fp_size, symfpu::fma<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg1.d_symuf, arg2.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::rem( const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::remainder<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::maxTotal( const FloatingPointLiteral& arg, bool zeroCaseLeft) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral( d_fp_size, symfpu::max<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::minTotal( const FloatingPointLiteral& arg, bool zeroCaseLeft) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral( d_fp_size, symfpu::min<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft)); -#else - unimplemented(); - return *this; -#endif } bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const { -#ifdef CVC5_USE_SYMFPU return ((d_fp_size == fp.d_fp_size) && symfpu::smtlibEqual<symfpuLiteral::traits>( d_fp_size, d_symuf, fp.d_symuf)); -#else - unimplemented(); - return ((d_fp_size == fp.d_fp_size)); -#endif } bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return symfpu::lessThanOrEqual<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return symfpu::lessThan<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf); -#else - unimplemented(); - return false; -#endif } BitVector FloatingPointLiteral::getExponent() const { -#ifdef CVC5_USE_SYMFPU return d_symuf.exponent; -#else - unimplemented(); - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return BitVector(); -#endif } BitVector FloatingPointLiteral::getSignificand() const { -#ifdef CVC5_USE_SYMFPU return d_symuf.significand; -#else - unimplemented(); - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return BitVector(); -#endif } bool FloatingPointLiteral::getSign() const { -#ifdef CVC5_USE_SYMFPU return d_symuf.sign; -#else - unimplemented(); - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return false; -#endif } bool FloatingPointLiteral::isNormal(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isSubnormal(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isZero(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isInfinite(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isNaN(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isNegative(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isPositive(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } FloatingPointLiteral FloatingPointLiteral::convert( const FloatingPointSize& target, const RoundingMode& rm) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( target, symfpu::convertFloatToFloat<symfpuLiteral::traits>( d_fp_size, target, rm, d_symuf)); -#else - unimplemented(); - return *this; -#endif } BitVector FloatingPointLiteral::convertToSBVTotal(BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const { -#ifdef CVC5_USE_SYMFPU return symfpu::convertFloatToSBV<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, width, undefinedCase); -#else - unimplemented(); - return undefinedCase; -#endif } BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const { -#ifdef CVC5_USE_SYMFPU return symfpu::convertFloatToUBV<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, width, undefinedCase); -#else - unimplemented(); - return undefinedCase; -#endif } -#ifndef CVC5_USE_SYMFPU -void FloatingPointLiteral::unimplemented(void) -{ - Unimplemented() << "no concrete implementation of FloatingPointLiteral"; -} - -size_t FloatingPointLiteral::hash(void) const -{ - unimplemented(); - return 23; -} -#endif - } // namespace cvc5 diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h index 54827a308..5b2b0f7c8 100644 --- a/src/util/floatingpoint_literal_symfpu.h.in +++ b/src/util/floatingpoint_literal_symfpu.h @@ -20,20 +20,16 @@ #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H #include "util/bitvector.h" -#include "util/floatingpoint_size.h" #include "util/floatingpoint_literal_symfpu_traits.h" +#include "util/floatingpoint_size.h" #include "util/roundingmode.h" /* -------------------------------------------------------------------------- */ namespace cvc5 { -// clang-format off -#if @CVC5_USE_SYMFPU@ -// clang-format on using SymFPUUnpackedFloatLiteral = ::symfpu::unpackedFloat<symfpuLiteral::traits>; -#endif class FloatingPointLiteral { @@ -65,13 +61,6 @@ class FloatingPointLiteral */ static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size); -// clang-format off -#if !@CVC5_USE_SYMFPU@ - // clang-format on - /** Catch-all for unimplemented functions. */ - static void unimplemented(void); -#endif - /** Constructors. */ /** Create a FP literal from its IEEE bit-vector representation. */ @@ -197,18 +186,10 @@ class FloatingPointLiteral BitVector convertToUBVTotal(BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const; -// clang-format off -#if @CVC5_USE_SYMFPU@ - // clang-format on /** Return wrapped floating-point literal. */ const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; } -#else - /** Dummy hash function. */ - size_t hash(void) const; -#endif private: - /** * Create a FP literal from unpacked representation. * @@ -223,34 +204,19 @@ class FloatingPointLiteral const bool sign, const BitVector& exp, const BitVector& sig) - : d_fp_size(size) -// clang-format off -#if @CVC5_USE_SYMFPU@ - // clang-format on - , - d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig)) -#endif + : d_fp_size(size), d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig)) { } -// clang-format off -#if @CVC5_USE_SYMFPU@ - // clang-format on - /** Create a FP literal from a symFPU unpacked float. */ FloatingPointLiteral(const FloatingPointSize& size, SymFPUUnpackedFloatLiteral symuf) : d_fp_size(size), d_symuf(symuf){}; -#endif /** The floating-point size of this floating-point literal. */ FloatingPointSize d_fp_size; -// clang-format off -#if @CVC5_USE_SYMFPU@ - // clang-format on /** The actual floating-point value, a SymFPU unpackedFloat. */ SymFPUUnpackedFloatLiteral d_symuf; -#endif }; /* -------------------------------------------------------------------------- */ diff --git a/src/util/floatingpoint_literal_symfpu_traits.cpp b/src/util/floatingpoint_literal_symfpu_traits.cpp index 071b69912..0f46708b0 100644 --- a/src/util/floatingpoint_literal_symfpu_traits.cpp +++ b/src/util/floatingpoint_literal_symfpu_traits.cpp @@ -13,8 +13,6 @@ * SymFPU glue code for floating-point values. */ -#if CVC5_USE_SYMFPU - #include "util/floatingpoint_literal_symfpu_traits.h" #include "base/check.h" @@ -413,4 +411,3 @@ void traits::invariant(const traits::prop& p) } } // namespace symfpuLiteral } // namespace cvc5 -#endif diff --git a/src/util/floatingpoint_literal_symfpu_traits.h.in b/src/util/floatingpoint_literal_symfpu_traits.h index 76d2f47e2..bc5caaf88 100644 --- a/src/util/floatingpoint_literal_symfpu_traits.h.in +++ b/src/util/floatingpoint_literal_symfpu_traits.h @@ -25,16 +25,12 @@ #ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H -// clang-format off -#if @CVC5_USE_SYMFPU@ -// clang-format on +#include <symfpu/core/unpackedFloat.h> #include "util/bitvector.h" #include "util/floatingpoint_size.h" #include "util/roundingmode.h" -#include <symfpu/core/unpackedFloat.h> - /* -------------------------------------------------------------------------- */ namespace cvc5 { @@ -258,7 +254,6 @@ class wrappedBitVector : public BitVector Cvc5BitWidth lower) const; }; } // namespace symfpuLiteral -} +} // namespace cvc5 #endif -#endif diff --git a/test/api/issue4889.cpp b/test/api/issue4889.cpp index f84d99f42..8e0853682 100644 --- a/test/api/issue4889.cpp +++ b/test/api/issue4889.cpp @@ -19,7 +19,6 @@ using namespace cvc5::api; int main() { -#ifdef CVC5_USE_SYMFPU Solver slv; Sort sort_int = slv.getIntegerSort(); Sort sort_array = slv.mkArraySort(sort_int, sort_int); @@ -33,6 +32,5 @@ int main() Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1); Term isnan = slv.mkTerm(FLOATINGPOINT_ISNAN, rem); slv.checkSatAssuming(isnan); -#endif return 0; } diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index 44ce684dd..1255bf270 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -32,11 +32,7 @@ def test_recoverable_exception(solver): def test_supports_floating_point(solver): - if solver.supportsFloatingPoint(): - solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) - else: - with pytest.raises(RuntimeError): - solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) + solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) def test_get_boolean_sort(solver): @@ -60,11 +56,7 @@ def test_get_string_sort(solver): def test_get_rounding_mode_sort(solver): - if solver.supportsFloatingPoint(): - solver.getRoundingModeSort() - else: - with pytest.raises(RuntimeError): - solver.getRoundingModeSort() + solver.getRoundingModeSort() def test_mk_array_sort(solver): @@ -79,10 +71,9 @@ def test_mk_array_sort(solver): solver.mkArraySort(boolSort, intSort) solver.mkArraySort(realSort, bvSort) - if (solver.supportsFloatingPoint()): - fpSort = solver.mkFloatingPointSort(3, 5) - solver.mkArraySort(fpSort, fpSort) - solver.mkArraySort(bvSort, fpSort) + fpSort = solver.mkFloatingPointSort(3, 5) + solver.mkArraySort(fpSort, fpSort) + solver.mkArraySort(bvSort, fpSort) slv = pycvc5.Solver() with pytest.raises(RuntimeError): @@ -96,15 +87,11 @@ def test_mk_bit_vector_sort(solver): def test_mk_floating_point_sort(solver): - if solver.supportsFloatingPoint(): - solver.mkFloatingPointSort(4, 8) - with pytest.raises(RuntimeError): - solver.mkFloatingPointSort(0, 8) - with pytest.raises(RuntimeError): - solver.mkFloatingPointSort(4, 0) - else: - with pytest.raises(RuntimeError): - solver.mkFloatingPointSort(4, 8) + solver.mkFloatingPointSort(4, 8) + with pytest.raises(RuntimeError): + solver.mkFloatingPointSort(0, 8) + with pytest.raises(RuntimeError): + solver.mkFloatingPointSort(4, 0) def test_mk_datatype_sort(solver): @@ -313,11 +300,7 @@ def test_mk_boolean(solver): def test_mk_rounding_mode(solver): - if solver.supportsFloatingPoint(): - solver.mkRoundingMode(pycvc5.RoundTowardZero) - else: - with pytest.raises(RuntimeError): - solver.mkRoundingMode(pycvc5.RoundTowardZero) + solver.mkRoundingMode(pycvc5.RoundTowardZero) def test_mk_uninterpreted_const(solver): @@ -333,11 +316,7 @@ def test_mk_floating_point(solver): t1 = solver.mkBitVector(8) t2 = solver.mkBitVector(4) t3 = solver.mkInteger(2) - if (solver.supportsFloatingPoint()): - solver.mkFloatingPoint(3, 5, t1) - else: - with pytest.raises(RuntimeError): - solver.mkFloatingPoint(3, 5, t1) + solver.mkFloatingPoint(3, 5, t1) with pytest.raises(RuntimeError): solver.mkFloatingPoint(0, 5, pycvc5.Term(solver)) @@ -350,10 +329,9 @@ def test_mk_floating_point(solver): with pytest.raises(RuntimeError): solver.mkFloatingPoint(3, 5, t2) - if (solver.supportsFloatingPoint()): - slv = pycvc5.Solver() - with pytest.raises(RuntimeError): - slv.mkFloatingPoint(3, 5, t1) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkFloatingPoint(3, 5, t1) def test_mk_empty_set(solver): @@ -382,43 +360,23 @@ def test_mk_false(solver): def test_mk_nan(solver): - if (solver.supportsFloatingPoint()): - solver.mkNaN(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkNaN(3, 5) + solver.mkNaN(3, 5) def test_mk_neg_zero(solver): - if (solver.supportsFloatingPoint()): - solver.mkNegZero(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkNegZero(3, 5) + solver.mkNegZero(3, 5) def test_mk_neg_inf(solver): - if (solver.supportsFloatingPoint()): - solver.mkNegInf(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkNegInf(3, 5) + solver.mkNegInf(3, 5) def test_mk_pos_inf(solver): - if (solver.supportsFloatingPoint()): - solver.mkPosInf(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkPosInf(3, 5) + solver.mkPosInf(3, 5) def test_mk_pos_zero(solver): - if (solver.supportsFloatingPoint()): - solver.mkPosZero(3, 5) - else: - with pytest.raises(RuntimeError): - solver.mkPosZero(3, 5) + solver.mkPosZero(3, 5) def test_mk_pi(solver): diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py index 5e86382ee..def539cf4 100644 --- a/test/python/unit/api/test_sort.py +++ b/test/python/unit/api/test_sort.py @@ -89,9 +89,8 @@ def test_is_reg_exp(solver): def test_is_rounding_mode(solver): - if solver.supportsFloatingPoint(): - assert solver.getRoundingModeSort().isRoundingMode() - Sort(solver).isRoundingMode() + assert solver.getRoundingModeSort().isRoundingMode() + Sort(solver).isRoundingMode() def test_is_bit_vector(solver): @@ -100,9 +99,8 @@ def test_is_bit_vector(solver): def test_is_floating_point(solver): - if solver.supportsFloatingPoint(): - assert solver.mkFloatingPointSort(8, 24).isFloatingPoint() - Sort(solver).isFloatingPoint() + assert solver.mkFloatingPointSort(8, 24).isFloatingPoint() + Sort(solver).isFloatingPoint() def test_is_datatype(solver): @@ -447,21 +445,19 @@ def test_get_bv_size(solver): def test_get_fp_exponent_size(solver): - if solver.supportsFloatingPoint(): - fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPExponentSize() - setSort = solver.mkSetSort(solver.getIntegerSort()) - with pytest.raises(RuntimeError): - setSort.getFPExponentSize() + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPExponentSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getFPExponentSize() def test_get_fp_significand_size(solver): - if solver.supportsFloatingPoint(): - fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPSignificandSize() - setSort = solver.mkSetSort(solver.getIntegerSort()) - with pytest.raises(RuntimeError): - setSort.getFPSignificandSize() + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFPSignificandSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getFPSignificandSize() def test_get_datatype_paramsorts(solver): diff --git a/test/regress/README.md b/test/regress/README.md index efd79472b..ca6fc30ab 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -115,11 +115,11 @@ configurations. The `REQUIRES` directive can be used to only run a given benchmark when a feature is supported. For example: ``` -; REQUIRES: symfpu +; REQUIRES: cryptominisat ``` -This benchmark is only run when symfpu has been configured. Multiple +This benchmark is only run when CryptoMiniSat has been configured. Multiple `REQUIRES` directives are supported. For a list of features that can be listed as a requirement, refer to cvc5's `--show-config` output. Features can also be -excluded by adding the `no-` prefix, e.g. `no-symfpu` means that the test is -not valid for builds that include symfpu support. +excluded by adding the `no-` prefix, e.g. `no-cryptominisat` means that the +test is not valid for builds that include CryptoMiniSat support. diff --git a/test/regress/regress0/fp/abs-unsound.smt2 b/test/regress/regress0/fp/abs-unsound.smt2 index b5aa0452e..ae7117047 100644 --- a/test/regress/regress0/fp/abs-unsound.smt2 +++ b/test/regress/regress0/fp/abs-unsound.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: sat (set-logic QF_FP) diff --git a/test/regress/regress0/fp/abs-unsound2.smt2 b/test/regress/regress0/fp/abs-unsound2.smt2 index ad603f8c9..3040f9ba9 100644 --- a/test/regress/regress0/fp/abs-unsound2.smt2 +++ b/test/regress/regress0/fp/abs-unsound2.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: unsat (set-logic QF_FP) diff --git a/test/regress/regress0/fp/down-cast-RNA.smt2 b/test/regress/regress0/fp/down-cast-RNA.smt2 index dc99ff144..62314f284 100644 --- a/test/regress/regress0/fp/down-cast-RNA.smt2 +++ b/test/regress/regress0/fp/down-cast-RNA.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: unsat diff --git a/test/regress/regress0/fp/ext-rew-test.smt2 b/test/regress/regress0/fp/ext-rew-test.smt2 index 726487e18..3fb3a9e53 100644 --- a/test/regress/regress0/fp/ext-rew-test.smt2 +++ b/test/regress/regress0/fp/ext-rew-test.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg ; EXPECT: unsat (set-info :smt-lib-version 2.6) diff --git a/test/regress/regress0/fp/from_sbv.smt2 b/test/regress/regress0/fp/from_sbv.smt2 index 3211339d6..226d6589c 100644 --- a/test/regress/regress0/fp/from_sbv.smt2 +++ b/test/regress/regress0/fp/from_sbv.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: unsat (set-logic QF_BVFP) diff --git a/test/regress/regress0/fp/from_ubv.smt2 b/test/regress/regress0/fp/from_ubv.smt2 index c02f8d304..6939e478a 100644 --- a/test/regress/regress0/fp/from_ubv.smt2 +++ b/test/regress/regress0/fp/from_ubv.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat (set-logic QF_FP) (declare-const r RoundingMode) diff --git a/test/regress/regress0/fp/issue-5524.smt2 b/test/regress/regress0/fp/issue-5524.smt2 index 8c361163c..741d77a19 100644 --- a/test/regress/regress0/fp/issue-5524.smt2 +++ b/test/regress/regress0/fp/issue-5524.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat (set-logic QF_FP) (declare-fun fpv5 () Float32) diff --git a/test/regress/regress0/fp/issue3536.smt2 b/test/regress/regress0/fp/issue3536.smt2 index 68a17347e..6a58b371f 100644 --- a/test/regress/regress0/fp/issue3536.smt2 +++ b/test/regress/regress0/fp/issue3536.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_FP) diff --git a/test/regress/regress0/fp/issue3582.smt2 b/test/regress/regress0/fp/issue3582.smt2 index 2de76b680..c06cdb110 100644 --- a/test/regress/regress0/fp/issue3582.smt2 +++ b/test/regress/regress0/fp/issue3582.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat (set-logic QF_FP) (declare-fun bv () (_ BitVec 1)) diff --git a/test/regress/regress0/fp/issue3619.smt2 b/test/regress/regress0/fp/issue3619.smt2 index 3e0858035..ab3c781bb 100644 --- a/test/regress/regress0/fp/issue3619.smt2 +++ b/test/regress/regress0/fp/issue3619.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_FPLRA) diff --git a/test/regress/regress0/fp/issue4277-assign-func.smt2 b/test/regress/regress0/fp/issue4277-assign-func.smt2 index c42bad235..d1fbc73d2 100644 --- a/test/regress/regress0/fp/issue4277-assign-func.smt2 +++ b/test/regress/regress0/fp/issue4277-assign-func.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: -q ; EXPECT: sat -; REQUIRES: symfpu (set-logic HO_ALL) (set-option :assign-function-values false) (set-info :status sat) diff --git a/test/regress/regress0/fp/issue5511.smt2 b/test/regress/regress0/fp/issue5511.smt2 index d4393486c..911db54ee 100644 --- a/test/regress/regress0/fp/issue5511.smt2 +++ b/test/regress/regress0/fp/issue5511.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: sat (set-logic QF_FP) (declare-fun a () (_ FloatingPoint 53 11)) diff --git a/test/regress/regress0/fp/issue5734.smt2 b/test/regress/regress0/fp/issue5734.smt2 index 2ad9ac921..d66e6aec7 100644 --- a/test/regress/regress0/fp/issue5734.smt2 +++ b/test/regress/regress0/fp/issue5734.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: sat (set-logic QF_FP) (declare-fun a () RoundingMode) diff --git a/test/regress/regress0/fp/issue6164.smt2 b/test/regress/regress0/fp/issue6164.smt2 index 056a98afc..3ec9f1594 100644 --- a/test/regress/regress0/fp/issue6164.smt2 +++ b/test/regress/regress0/fp/issue6164.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: sat ; EXPECT: ((((_ to_fp 5 11) roundNearestTiesToAway (/ 1 10)) (fp #b0 #b01011 #b1001100110))) (set-logic ALL) diff --git a/test/regress/regress0/fp/rti_3_5_bug.smt2 b/test/regress/regress0/fp/rti_3_5_bug.smt2 index 2c837b415..724e08b8c 100644 --- a/test/regress/regress0/fp/rti_3_5_bug.smt2 +++ b/test/regress/regress0/fp/rti_3_5_bug.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu
; COMMAND-LINE: --fp-exp
; EXPECT: unsat
diff --git a/test/regress/regress0/fp/simple.smt2 b/test/regress/regress0/fp/simple.smt2 index 0b4a11f08..754186943 100644 --- a/test/regress/regress0/fp/simple.smt2 +++ b/test/regress/regress0/fp/simple.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat (set-logic QF_FP) (declare-const x Float32) diff --git a/test/regress/regress0/fp/wrong-model.smt2 b/test/regress/regress0/fp/wrong-model.smt2 index 7694d8a35..298c21b18 100644 --- a/test/regress/regress0/fp/wrong-model.smt2 +++ b/test/regress/regress0/fp/wrong-model.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: sat diff --git a/test/regress/regress0/issue5370.smt2 b/test/regress/regress0/issue5370.smt2 index 848567e2c..971602e14 100644 --- a/test/regress/regress0/issue5370.smt2 +++ b/test/regress/regress0/issue5370.smt2 @@ -1,5 +1,4 @@ ; COMMAND-LINE: --bv-to-bool -; REQUIRES: symfpu (set-logic ALL) (set-info :status sat) (declare-fun c () (Array (_ BitVec 2) (_ BitVec 1))) diff --git a/test/regress/regress0/parser/to_fp.smt2 b/test/regress/regress0/parser/to_fp.smt2 index 277209ff8..1cd83816a 100644 --- a/test/regress/regress0/parser/to_fp.smt2 +++ b/test/regress/regress0/parser/to_fp.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --strict-parsing -q ; EXPECT: sat (set-logic QF_FP) diff --git a/test/regress/regress1/fp/rti_3_5_bug_report.smt2 b/test/regress/regress1/fp/rti_3_5_bug_report.smt2 index 3e94e6e05..6c0b68c95 100644 --- a/test/regress/regress1/fp/rti_3_5_bug_report.smt2 +++ b/test/regress/regress1/fp/rti_3_5_bug_report.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --fp-exp ; EXPECT: unsat diff --git a/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 index 1ee8e6c11..3ab7495ea 100644 --- a/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 +++ b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu (set-info :smt-lib-version 2.6) (set-logic FP) (set-info :status unsat) diff --git a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 index 796d7e753..d30bd563d 100644 --- a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 +++ b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 @@ -1,5 +1,4 @@ ; COMMAND-LINE: --no-jh-rlv-order -; REQUIRES: symfpu ; EXPECT: unsat (set-logic AUFBVFPDTNIRA) (set-info :status unsat) diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy index 30828ca76..2970fd0de 100644 --- a/test/regress/regress1/rr-verify/fp-arith.sy +++ b/test/regress/regress1/rr-verify/fp-arith.sy @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy index 6704198c3..e4b3a0fac 100644 --- a/test/regress/regress1/rr-verify/fp-bool.sy +++ b/test/regress/regress1/rr-verify/fp-bool.sy @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' diff --git a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy index fa8bdc2d7..385ade07f 100644 --- a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy +++ b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL) diff --git a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 index c674c4039..4648c327a 100644 --- a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 +++ b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; COMMAND-LINE: --decision=internal -q ; COMMAND-LINE: --decision=justification -q ; EXPECT: sat diff --git a/test/regress/regress2/sygus/min_IC_1.sy b/test/regress/regress2/sygus/min_IC_1.sy index c0cae0025..8c0e2d82b 100644 --- a/test/regress/regress2/sygus/min_IC_1.sy +++ b/test/regress/regress2/sygus/min_IC_1.sy @@ -1,4 +1,3 @@ -; REQUIRES: symfpu ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --fp-exp (set-logic ALL) diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 018207293..20e0977f8 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -35,15 +35,7 @@ TEST_F(TestApiBlackSolver, recoverableException) TEST_F(TestApiBlackSolver, supportsFloatingPoint) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN)); - } - else - { - ASSERT_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN), - CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN)); } TEST_F(TestApiBlackSolver, getBooleanSort) @@ -78,14 +70,7 @@ TEST_F(TestApiBlackSolver, getStringSort) TEST_F(TestApiBlackSolver, getRoundingModeSort) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.getRoundingModeSort()); - } - else - { - ASSERT_THROW(d_solver.getRoundingModeSort(), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.getRoundingModeSort()); } TEST_F(TestApiBlackSolver, mkArraySort) @@ -101,12 +86,9 @@ TEST_F(TestApiBlackSolver, mkArraySort) ASSERT_NO_THROW(d_solver.mkArraySort(boolSort, intSort)); ASSERT_NO_THROW(d_solver.mkArraySort(realSort, bvSort)); - if (d_solver.supportsFloatingPoint()) - { - Sort fpSort = d_solver.mkFloatingPointSort(3, 5); - ASSERT_NO_THROW(d_solver.mkArraySort(fpSort, fpSort)); - ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, fpSort)); - } + Sort fpSort = d_solver.mkFloatingPointSort(3, 5); + ASSERT_NO_THROW(d_solver.mkArraySort(fpSort, fpSort)); + ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, fpSort)); Solver slv; ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC5ApiException); @@ -120,16 +102,9 @@ TEST_F(TestApiBlackSolver, mkBitVectorSort) TEST_F(TestApiBlackSolver, mkFloatingPointSort) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8)); - ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC5ApiException); - ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC5ApiException); - } - else - { - ASSERT_THROW(d_solver.mkFloatingPointSort(4, 8), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8)); + ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC5ApiException); + ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkDatatypeSort) @@ -377,15 +352,7 @@ TEST_F(TestApiBlackSolver, mkBoolean) TEST_F(TestApiBlackSolver, mkRoundingMode) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); - } - else - { - ASSERT_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO), - CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); } TEST_F(TestApiBlackSolver, mkUninterpretedConst) @@ -420,25 +387,15 @@ TEST_F(TestApiBlackSolver, mkFloatingPoint) Term t1 = d_solver.mkBitVector(8); Term t2 = d_solver.mkBitVector(4); Term t3 = d_solver.mkInteger(2); - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1)); - } - else - { - ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t1), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1)); ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, Term()), CVC5ApiException); ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, t1), CVC5ApiException); ASSERT_THROW(d_solver.mkFloatingPoint(3, 0, t1), CVC5ApiException); ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException); ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException); - if (d_solver.supportsFloatingPoint()) - { - Solver slv; - ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException); - } + Solver slv; + ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkEmptySet) @@ -478,64 +435,26 @@ TEST_F(TestApiBlackSolver, mkFalse) ASSERT_NO_THROW(d_solver.mkFalse()); } -TEST_F(TestApiBlackSolver, mkNaN) -{ - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkNaN(3, 5)); - } - else - { - ASSERT_THROW(d_solver.mkNaN(3, 5), CVC5ApiException); - } -} +TEST_F(TestApiBlackSolver, mkNaN) { ASSERT_NO_THROW(d_solver.mkNaN(3, 5)); } TEST_F(TestApiBlackSolver, mkNegZero) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkNegZero(3, 5)); - } - else - { - ASSERT_THROW(d_solver.mkNegZero(3, 5), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkNegZero(3, 5)); } TEST_F(TestApiBlackSolver, mkNegInf) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkNegInf(3, 5)); - } - else - { - ASSERT_THROW(d_solver.mkNegInf(3, 5), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkNegInf(3, 5)); } TEST_F(TestApiBlackSolver, mkPosInf) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkPosInf(3, 5)); - } - else - { - ASSERT_THROW(d_solver.mkPosInf(3, 5), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkPosInf(3, 5)); } TEST_F(TestApiBlackSolver, mkPosZero) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_NO_THROW(d_solver.mkPosZero(3, 5)); - } - else - { - ASSERT_THROW(d_solver.mkPosZero(3, 5), CVC5ApiException); - } + ASSERT_NO_THROW(d_solver.mkPosZero(3, 5)); } TEST_F(TestApiBlackSolver, mkOp) diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index d1b096bda..757bacad6 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -95,11 +95,8 @@ TEST_F(TestApiBlackSort, isRegExp) TEST_F(TestApiBlackSort, isRoundingMode) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_TRUE(d_solver.getRoundingModeSort().isRoundingMode()); - ASSERT_NO_THROW(Sort().isRoundingMode()); - } + ASSERT_TRUE(d_solver.getRoundingModeSort().isRoundingMode()); + ASSERT_NO_THROW(Sort().isRoundingMode()); } TEST_F(TestApiBlackSort, isBitVector) @@ -110,11 +107,8 @@ TEST_F(TestApiBlackSort, isBitVector) TEST_F(TestApiBlackSort, isFloatingPoint) { - if (d_solver.supportsFloatingPoint()) - { - ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint()); - ASSERT_NO_THROW(Sort().isFloatingPoint()); - } + ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint()); + ASSERT_NO_THROW(Sort().isFloatingPoint()); } TEST_F(TestApiBlackSort, isDatatype) @@ -486,24 +480,18 @@ TEST_F(TestApiBlackSort, getBVSize) TEST_F(TestApiBlackSort, getFPExponentSize) { - if (d_solver.supportsFloatingPoint()) - { - Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPExponentSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException); - } + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + ASSERT_NO_THROW(fpSort.getFPExponentSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException); } TEST_F(TestApiBlackSort, getFPSignificandSize) { - if (d_solver.supportsFloatingPoint()) - { - Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPSignificandSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException); - } + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + ASSERT_NO_THROW(fpSort.getFPSignificandSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException); } TEST_F(TestApiBlackSort, getDatatypeParamSorts) diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp index 7a6e34abb..e999297fd 100644 --- a/test/unit/theory/logic_info_white.cpp +++ b/test/unit/theory/logic_info_white.cpp @@ -616,28 +616,14 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) info.arithOnlyLinear(); info.disableIntegers(); info.lock(); - if (cvc5::Configuration::isBuiltWithSymFPU()) - { - ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA"); - } - else - { - ASSERT_EQ(info.getLogicString(), "SEP_AUFBVDTLRA"); - } + ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA"); info = info.getUnlockedCopy(); ASSERT_FALSE(info.isLocked()); info.disableQuantifiers(); info.disableTheory(THEORY_BAGS); info.lock(); - if (cvc5::Configuration::isBuiltWithSymFPU()) - { - ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA"); - } - else - { - ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVDTLRA"); - } + ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA"); info = info.getUnlockedCopy(); ASSERT_FALSE(info.isLocked()); @@ -647,14 +633,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) info.enableIntegers(); info.disableReals(); info.lock(); - if (cvc5::Configuration::isBuiltWithSymFPU()) - { - ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA"); - } - else - { - ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFLIA"); - } + ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA"); info = info.getUnlockedCopy(); ASSERT_FALSE(info.isLocked()); diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 26ab40614..c1630a203 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -24,9 +24,7 @@ cvc5_add_unit_test_white(check_white util) cvc5_add_unit_test_black(configuration_black util) cvc5_add_unit_test_black(datatype_black util) cvc5_add_unit_test_black(exception_black util) -if(CVC5_USE_SYMFPU) cvc5_add_unit_test_black(floatingpoint_black util) -endif() cvc5_add_unit_test_black(integer_black util) cvc5_add_unit_test_white(integer_white util) cvc5_add_unit_test_black(output_black util) |