diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-09-30 12:07:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-30 17:07:39 +0000 |
commit | 720e3afc907f429cf8105ee49b3628ddaacbf7a3 (patch) | |
tree | 68e8cd29c979cdab7ba92268d7903cb3e7b79779 /src/api/java/cvc5/RoundingMode.java | |
parent | 4e54aa63e13f551e9c647ce59edd958e1d84ddb1 (diff) |
Finish the Java Api (#6396)
This commit finishes the implementation of the Java API.
It also includes all java files in the build along with their unit tests.
Diffstat (limited to 'src/api/java/cvc5/RoundingMode.java')
-rw-r--r-- | src/api/java/cvc5/RoundingMode.java | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/src/api/java/cvc5/RoundingMode.java b/src/api/java/cvc5/RoundingMode.java new file mode 100644 index 000000000..4229bb74a --- /dev/null +++ b/src/api/java/cvc5/RoundingMode.java @@ -0,0 +1,63 @@ +/****************************************************************************** + * 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 cvc5; + +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; + } +} |