From: Andres Noetzli Date: Tue, 29 Mar 2022 01:13:46 +0000 (-0700) Subject: Move `RoundingMode` to `cvc5_types.h` (#8427) X-Git-Tag: cvc5-1.0.0~146 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bf2d64336c2d3cda4db39b6b528c2a3fc7e0f792;p=cvc5.git Move `RoundingMode` to `cvc5_types.h` (#8427) This moves RoundingMode to cvc5_types.h and switches to using the auto-generated enum bindings. It also fixes the Java-bindings generator for enums (certain parts were previously hardcoded for Kind) and extends the unit tests for Solver::mkRoundingMode() to actually check the value being created. --- diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index 493561a68..768c88ba3 100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -17,7 +17,7 @@ ## import cvc5 -from cvc5 import Kind +from cvc5 import Kind, RoundingMode if __name__ == "__main__": slv = cvc5.Solver() @@ -29,7 +29,7 @@ if __name__ == "__main__": fp32 = slv.mkFloatingPointSort(8, 24) # the standard rounding mode - rm = slv.mkRoundingMode(cvc5.RoundNearestTiesToEven) + rm = slv.mkRoundingMode(RoundingMode.RoundNearestTiesToEven) # create a few single-precision variables x = slv.mkConst(fp32, 'x') diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index c84bd15d0..5c92c9d3a 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7668,12 +7668,6 @@ size_t hash::operator()(const cvc5::api::Op& t) const } } -size_t std::hash::operator()( - cvc5::api::RoundingMode rm) const -{ - return static_cast(rm); -} - size_t std::hash::operator()(const cvc5::api::Sort& s) const { return std::hash()(*s.d_type); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 4e9db9364..c3e5b93ea 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2716,75 +2716,6 @@ class CVC5_EXPORT Grammar */ std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC5_EXPORT; -/* -------------------------------------------------------------------------- */ -/* Rounding Mode for Floating-Points */ -/* -------------------------------------------------------------------------- */ - -/** - * Rounding modes for floating-point numbers. - * - * For many floating-point operations, infinitely precise results may not be - * representable with the number of available bits. Thus, the results are - * rounded in a certain way to one of the representable floating-point numbers. - * - * \verbatim embed:rst:leading-asterisk - * These rounding modes directly follow the SMT-LIB theory for floating-point - * arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`. - * The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE - * Standard 754. - * \endverbatim - */ -enum RoundingMode -{ - /** - * Round to the nearest even number. - * If the two nearest floating-point numbers bracketing an unrepresentable - * infinitely precise result are equally near, the one with an even least - * significant digit will be delivered. - */ - ROUND_NEAREST_TIES_TO_EVEN, - /** - * Round towards positive infinity (+oo). - * The result shall be the format's floating-point number (possibly +oo) - * closest to and no less than the infinitely precise result. - */ - ROUND_TOWARD_POSITIVE, - /** - * Round towards negative infinity (-oo). - * The result shall be the format's floating-point number (possibly -oo) - * closest to and no less than the infinitely precise result. - */ - ROUND_TOWARD_NEGATIVE, - /** - * Round towards zero. - * The result shall be the format's floating-point number closest to and no - * greater in magnitude than the infinitely precise result. - */ - ROUND_TOWARD_ZERO, - /** - * Round to the nearest number away from zero. - * If the two nearest floating-point numbers bracketing an unrepresentable - * infinitely precise result are equally near, the one with larger magnitude - * will be selected. - */ - ROUND_NEAREST_TIES_TO_AWAY, -}; - -} // namespace cvc5::api - -namespace std { - -/** - * Hash function for RoundingModes. - */ -template <> -struct CVC5_EXPORT hash -{ - size_t operator()(cvc5::api::RoundingMode rm) const; -}; -} // namespace std -namespace cvc5::api { - /* -------------------------------------------------------------------------- */ /* Options */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/cpp/cvc5_types.h b/src/api/cpp/cvc5_types.h index 3ce20688b..a5cda3d6b 100644 --- a/src/api/cpp/cvc5_types.h +++ b/src/api/cpp/cvc5_types.h @@ -18,6 +18,60 @@ #ifndef CVC5__API__CVC5_TYPES_H #define CVC5__API__CVC5_TYPES_H +namespace cvc5::api { + +/** + * Rounding modes for floating-point numbers. + * + * For many floating-point operations, infinitely precise results may not be + * representable with the number of available bits. Thus, the results are + * rounded in a certain way to one of the representable floating-point numbers. + * + * \verbatim embed:rst:leading-asterisk + * These rounding modes directly follow the SMT-LIB theory for floating-point + * arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`. + * The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE + * Standard 754. + * \endverbatim + */ +enum RoundingMode +{ + /** + * Round to the nearest even number. + * If the two nearest floating-point numbers bracketing an unrepresentable + * infinitely precise result are equally near, the one with an even least + * significant digit will be delivered. + */ + ROUND_NEAREST_TIES_TO_EVEN, + /** + * Round towards positive infinity (+oo). + * The result shall be the format's floating-point number (possibly +oo) + * closest to and no less than the infinitely precise result. + */ + ROUND_TOWARD_POSITIVE, + /** + * Round towards negative infinity (-oo). + * The result shall be the format's floating-point number (possibly -oo) + * closest to and no less than the infinitely precise result. + */ + ROUND_TOWARD_NEGATIVE, + /** + * Round towards zero. + * The result shall be the format's floating-point number closest to and no + * greater in magnitude than the infinitely precise result. + */ + ROUND_TOWARD_ZERO, + /** + * Round to the nearest number away from zero. + * If the two nearest floating-point numbers bracketing an unrepresentable + * infinitely precise result are equally near, the one with larger magnitude + * will be selected. + */ + ROUND_NEAREST_TIES_TO_AWAY, +}; + +} // namespace cvc5::api + namespace cvc5::modes { enum BlockModelsMode diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index da4fa60c4..bafda8323 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -41,6 +41,7 @@ add_custom_target(generate-java-kinds DEPENDS ${JAVA_KIND_FILE}) set(JAVA_TYPES_FILES "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/BlockModelsMode.java" + "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/RoundingMode.java" ) add_custom_command( OUTPUT @@ -78,7 +79,6 @@ set(JAVA_FILES ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/OptionInfo.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Pair.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Result.java - ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/RoundingMode.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Solver.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Sort.java ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Stat.java diff --git a/src/api/java/genenums.py.in b/src/api/java/genenums.py.in index 5ecd5bd40..3b7260f4d 100644 --- a/src/api/java/genenums.py.in +++ b/src/api/java/genenums.py.in @@ -46,37 +46,50 @@ public enum {name} ENUM_JAVA_BOTTOM = \ r"""; - /* the int value of the kind */ + /* the int value of the {name} */ private int value; - private static Map kindMap = new HashMap<>(); - private Kind(int value) - { + private static int minValue = 0; + private static int maxValue = 0; + private static Map enumMap = new HashMap<>(); + + private {name}(int value) + {{ this.value = value; - } + }} static - { - for (Kind kind : Kind.values()) - { - kindMap.put(kind.getValue(), kind); - } - } - - public static Kind fromInt(int value) throws CVC5ApiException - { - if (value < INTERNAL_KIND.value || value > LAST_KIND.value) - { - throw new CVC5ApiException("Kind value " + value + " is outside the valid range [" - + INTERNAL_KIND.value + "," + LAST_KIND.value + "]"); - } - return kindMap.get(value); - } + {{ + boolean firstValue = true; + for ({name} enumerator : {name}.values()) + {{ + int value = enumerator.getValue(); + if (firstValue) + {{ + minValue = value; + maxValue = value; + firstValue = false; + }} + minValue = Math.min(minValue, value); + maxValue = Math.max(maxValue, value); + enumMap.put(value, enumerator); + }} + }} + + public static {name} fromInt(int value) throws CVC5ApiException + {{ + if (value < minValue || value > maxValue) + {{ + throw new CVC5ApiException("{name} value " + value + " is outside the valid range [" + + minValue + "," + maxValue + "]"); + }} + return enumMap.get(value); + }} public int getValue() - { + {{ return value; - } -} + }} +}} """ # mapping from c++ patterns to java @@ -129,7 +142,7 @@ def gen_java(parser: EnumParser, path): comment = format_comment(comment) code += "{comment}\n {name}({enum_value}),\n".format( comment=comment, name=name, enum_value=value) - code += ENUM_JAVA_BOTTOM + code += ENUM_JAVA_BOTTOM.format(name=enum.name) f.write(code) diff --git a/src/api/java/io/github/cvc5/api/RoundingMode.java b/src/api/java/io/github/cvc5/api/RoundingMode.java deleted file mode 100644 index 6a3c274a1..000000000 --- a/src/api/java/io/github/cvc5/api/RoundingMode.java +++ /dev/null @@ -1,63 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package io.github.cvc5.api; - -public enum RoundingMode { - /** - * Round to the nearest even number. - * If the two nearest floating-point numbers bracketing an unrepresentable - * infinitely precise result are equally near, the one with an even least - * significant digit will be delivered. - */ - ROUND_NEAREST_TIES_TO_EVEN(0), - /** - * Round towards positive infinity (+oo). - * The result shall be the format's floating-point number (possibly +oo) - * closest to and no less than the infinitely precise result. - */ - ROUND_TOWARD_POSITIVE(1), - /** - * Round towards negative infinity (-oo). - * The result shall be the format's floating-point number (possibly -oo) - * closest to and no less than the infinitely precise result. - */ - ROUND_TOWARD_NEGATIVE(2), - /** - * Round towards zero. - * The result shall be the format's floating-point number closest to and no - * greater in magnitude than the infinitely precise result. - */ - ROUND_TOWARD_ZERO(3), - /** - * Round to the nearest number away from zero. - * If the two nearest floating-point numbers bracketing an unrepresentable - * infinitely precise result are equally near, the one with larger magnitude - * will be selected. - */ - ROUND_NEAREST_TIES_TO_AWAY(4); - - private int value; - - private RoundingMode(int value) - { - this.value = value; - } - - public int getValue() - { - return value; - } -} diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index b5cbdf7cc..15fd5f3e9 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -8,6 +8,7 @@ from libcpp.string cimport string from libcpp.vector cimport vector from libcpp.pair cimport pair from cvc5kinds cimport Kind +from cvc5types cimport RoundingMode cdef extern from "" namespace "std": @@ -201,9 +202,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isUnknown() except + string toString() except + - cdef cppclass RoundingMode: - pass - cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::Result": cdef cppclass UnknownExplanation: pass @@ -528,14 +526,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": size_t operator()(const Term & t) except + -cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::RoundingMode": - cdef RoundingMode ROUND_NEAREST_TIES_TO_EVEN, - cdef RoundingMode ROUND_TOWARD_POSITIVE, - cdef RoundingMode ROUND_TOWARD_NEGATIVE, - cdef RoundingMode ROUND_TOWARD_ZERO, - cdef RoundingMode ROUND_NEAREST_TIES_TO_AWAY - - cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::Result::UnknownExplanation": cdef UnknownExplanation REQUIRES_FULL_CHECK cdef UnknownExplanation INCOMPLETE diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index fc24f32a2..b9734761e 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -22,7 +22,6 @@ from cvc5 cimport DatatypeDecl as c_DatatypeDecl from cvc5 cimport DatatypeSelector as c_DatatypeSelector from cvc5 cimport Result as c_Result from cvc5 cimport SynthResult as c_SynthResult -from cvc5 cimport RoundingMode as c_RoundingMode from cvc5 cimport UnknownExplanation as c_UnknownExplanation from cvc5 cimport Op as c_Op from cvc5 cimport OptionInfo as c_OptionInfo @@ -33,9 +32,6 @@ from cvc5 cimport Statistics as c_Statistics from cvc5 cimport Stat as c_Stat from cvc5 cimport Grammar as c_Grammar from cvc5 cimport Sort as c_Sort -from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE -from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO -from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON @@ -46,6 +42,7 @@ from cvc5 cimport wstring as c_wstring from cvc5 cimport tuple as c_tuple from cvc5 cimport get0, get1, get2 from cvc5kinds cimport Kind as c_Kind +from cvc5types cimport RoundingMode as c_RoundingMode cdef extern from "Python.h": wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *) @@ -672,44 +669,6 @@ cdef class SynthResult: def __repr__(self): return self.cr.toString().decode() -cdef class RoundingMode: - """ - Rounding modes for floating-point numbers. - - For many floating-point operations, infinitely precise results may not be - representable with the number of available bits. Thus, the results are - rounded in a certain way to one of the representable floating-point numbers. - - These rounding modes directly follow the SMT-LIB theory for floating-point - arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`. - The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE - Standard 754. - - Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`. - """ - cdef c_RoundingMode crm - cdef str name - def __cinit__(self, int rm): - # crm always assigned externally - self.crm = rm - self.name = __rounding_modes[rm] - - def __eq__(self, RoundingMode other): - return ( self.crm) == ( other.crm) - - def __ne__(self, RoundingMode other): - return not self.__eq__(other) - - def __hash__(self): - return hash(( self.crm, self.name)) - - def __str__(self): - return self.name - - def __repr__(self): - return self.name - - cdef class UnknownExplanation: """ Wrapper class for :cpp:enum:`cvc5::api::Result::UnknownExplanation`. @@ -1415,13 +1374,13 @@ cdef class Solver: term.cterm = self.csolver.mkFloatingPointNegZero(exp, sig) return term - def mkRoundingMode(self, RoundingMode rm): + def mkRoundingMode(self, rm): """Create a roundingmode constant. :param rm: the floating point rounding mode this constant represents """ cdef Term term = Term(self) - term.cterm = self.csolver.mkRoundingMode( rm.crm) + term.cterm = self.csolver.mkRoundingMode( rm.value) return term def mkFloatingPoint(self, int exp, int sig, Term val): @@ -3663,29 +3622,6 @@ cdef class Term: return res -# Generate rounding modes -cdef __rounding_modes = { - ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven", - ROUND_TOWARD_POSITIVE: "RoundTowardPositive", - ROUND_TOWARD_NEGATIVE: "RoundTowardNegative", - ROUND_TOWARD_ZERO: "RoundTowardZero", - ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway" -} - -mod_ref = sys.modules[__name__] -for rm_int, name in __rounding_modes.items(): - r = RoundingMode(rm_int) - - if name in dir(mod_ref): - raise RuntimeError("Redefinition of Python RoundingMode %s."%name) - - setattr(mod_ref, name, r) - -del r -del rm_int -del name - - # Generate unknown explanations cdef __unknown_explanations = { REQUIRES_FULL_CHECK: "RequiresFullCheck", @@ -3700,6 +3636,7 @@ cdef __unknown_explanations = { UNKNOWN_REASON: "UnknownReason" } +mod_ref = sys.modules[__name__] for ue_int, name in __unknown_explanations.items(): u = UnknownExplanation(ue_int) diff --git a/src/api/python/cvc5_python_base.pyx b/src/api/python/cvc5_python_base.pyx index f09300265..a70433140 100644 --- a/src/api/python/cvc5_python_base.pyx +++ b/src/api/python/cvc5_python_base.pyx @@ -1,2 +1,3 @@ include "cvc5kinds.pxi" +include "cvc5types.pxi" include "cvc5.pxi" diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index edb9c291a..d9a38ec08 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -452,7 +452,20 @@ TEST_F(TestApiBlackSolver, mkBoolean) TEST_F(TestApiBlackSolver, mkRoundingMode) { - ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); + ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN) + .toString(), + "roundNearestTiesToEven"); + ASSERT_EQ( + d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_POSITIVE).toString(), + "roundTowardPositive"); + ASSERT_EQ( + d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_NEGATIVE).toString(), + "roundTowardNegative"); + ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO).toString(), + "roundTowardZero"); + ASSERT_EQ(d_solver.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY) + .toString(), + "roundNearestTiesToAway"); } TEST_F(TestApiBlackSolver, mkFloatingPoint) diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index c0e4d9d46..eebc335d9 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -430,7 +430,16 @@ class SolverTest @Test void mkRoundingMode() throws CVC5ApiException { - assertDoesNotThrow(() -> d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO)); + assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).toString(), + "roundNearestTiesToEven"); + assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE).toString(), + "roundTowardPositive"); + assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE).toString(), + "roundTowardNegative"); + assertEquals( + d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO).toString(), "roundTowardZero"); + assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY).toString(), + "roundNearestTiesToAway"); } @Test void mkFloatingPoint() throws CVC5ApiException diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index f1c69e8cd..fdb71ed44 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -15,7 +15,7 @@ import pytest import cvc5 import sys -from cvc5 import Kind +from cvc5 import Kind, RoundingMode @pytest.fixture @@ -32,7 +32,7 @@ def test_recoverable_exception(solver): def test_supports_floating_point(solver): - solver.mkRoundingMode(cvc5.RoundNearestTiesToEven) + solver.mkRoundingMode(RoundingMode.RoundNearestTiesToEven) def test_get_boolean_sort(solver): @@ -407,7 +407,16 @@ def test_mk_boolean(solver): def test_mk_rounding_mode(solver): - solver.mkRoundingMode(cvc5.RoundTowardZero) + assert str(solver.mkRoundingMode( + RoundingMode.RoundNearestTiesToEven)) == "roundNearestTiesToEven" + assert str(solver.mkRoundingMode( + RoundingMode.RoundTowardPositive)) == "roundTowardPositive" + assert str(solver.mkRoundingMode( + RoundingMode.RoundTowardNegative)) == "roundTowardNegative" + assert str(solver.mkRoundingMode( + RoundingMode.RoundTowardZero)) == "roundTowardZero" + assert str(solver.mkRoundingMode( + RoundingMode.RoundNearestTiesToAway)) == "roundNearestTiesToAway" def test_mk_floating_point(solver):