File tree 1 file changed +3
-19
lines changed
src/org/sosy_lab/java_smt/solvers/bitwuzla
1 file changed +3
-19
lines changed Original file line number Diff line number Diff line change @@ -97,26 +97,10 @@ private Sort mkFpaSort(FloatingPointType pType) {
97
97
@ Override
98
98
protected Term makeNumberAndRound (
99
99
String pN , FloatingPointType pType , Term pFloatingPointRoundingMode ) {
100
- // Convert input string to "canonical" format, that is without trailing zeroes, but at least
101
- // one digit after the dot
102
- String canonical = pN .replaceAll ("(\\ .[0-9]+?)0*$" , "$1" );
103
- if (!canonical .contains ("." )) {
104
- canonical = canonical + ".0" ;
100
+ if (isNegativeZero (Double .valueOf (pN ))) {
101
+ return termManager .mk_fp_neg_zero (mkFpaSort (pType ));
105
102
}
106
-
107
- // Handle special cases
108
- switch (canonical ) {
109
- case "-inf" :
110
- return termManager .mk_fp_neg_inf (mkFpaSort (pType ));
111
- case "-0.0" :
112
- return termManager .mk_fp_neg_zero (mkFpaSort (pType ));
113
- case "nan" :
114
- return termManager .mk_fp_nan (mkFpaSort (pType ));
115
- case "inf" :
116
- return termManager .mk_fp_pos_inf (mkFpaSort (pType ));
117
- }
118
-
119
- String decimalString = new BigDecimal (canonical ).toPlainString ();
103
+ String decimalString = new BigDecimal (pN ).toPlainString ();
120
104
return termManager .mk_fp_value (mkFpaSort (pType ), pFloatingPointRoundingMode , decimalString );
121
105
}
122
106
You can’t perform that action at this time.
0 commit comments