##
import cvc5
-from cvc5 import Kind
+from cvc5 import Kind, RoundingMode
if __name__ == "__main__":
slv = cvc5.Solver()
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')
}
}
-size_t std::hash<cvc5::api::RoundingMode>::operator()(
- cvc5::api::RoundingMode rm) const
-{
- return static_cast<size_t>(rm);
-}
-
size_t std::hash<cvc5::api::Sort>::operator()(const cvc5::api::Sort& s) const
{
return std::hash<cvc5::TypeNode>()(*s.d_type);
*/
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<cvc5::api::RoundingMode>
-{
- size_t operator()(cvc5::api::RoundingMode rm) const;
-};
-} // namespace std
-namespace cvc5::api {
-
/* -------------------------------------------------------------------------- */
/* Options */
/* -------------------------------------------------------------------------- */
#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
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
${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
ENUM_JAVA_BOTTOM = \
r""";
- /* the int value of the kind */
+ /* the int value of the {name} */
private int value;
- private static Map<Integer, Kind> kindMap = new HashMap<>();
- private Kind(int value)
- {
+ private static int minValue = 0;
+ private static int maxValue = 0;
+ private static Map<Integer, {name}> 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
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)
+++ /dev/null
-/******************************************************************************
- * 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;
- }
-}
from libcpp.vector cimport vector
from libcpp.pair cimport pair
from cvc5kinds cimport Kind
+from cvc5types cimport RoundingMode
cdef extern from "<iostream>" namespace "std":
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
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
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
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
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 *)
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 = <c_RoundingMode> rm
- self.name = __rounding_modes[rm]
-
- def __eq__(self, RoundingMode other):
- return (<int> self.crm) == (<int> other.crm)
-
- def __ne__(self, RoundingMode other):
- return not self.__eq__(other)
-
- def __hash__(self):
- return hash((<int> 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`.
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(<c_RoundingMode> rm.crm)
+ term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.value)
return term
def mkFloatingPoint(self, int exp, int sig, Term val):
return res
-# Generate rounding modes
-cdef __rounding_modes = {
- <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven",
- <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive",
- <int> ROUND_TOWARD_NEGATIVE: "RoundTowardNegative",
- <int> ROUND_TOWARD_ZERO: "RoundTowardZero",
- <int> 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 = {
<int> REQUIRES_FULL_CHECK: "RequiresFullCheck",
<int> UNKNOWN_REASON: "UnknownReason"
}
+mod_ref = sys.modules[__name__]
for ue_int, name in __unknown_explanations.items():
u = UnknownExplanation(ue_int)
include "cvc5kinds.pxi"
+include "cvc5types.pxi"
include "cvc5.pxi"
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)
@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
import cvc5
import sys
-from cvc5 import Kind
+from cvc5 import Kind, RoundingMode
@pytest.fixture
def test_supports_floating_point(solver):
- solver.mkRoundingMode(cvc5.RoundNearestTiesToEven)
+ solver.mkRoundingMode(RoundingMode.RoundNearestTiesToEven)
def test_get_boolean_sort(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):
projects / cvc5.git / commitdiff