Skip to content

Commit facf943

Browse files
agilotvkuncak
authored andcommitted
Small refactoring
1 parent e48ccf7 commit facf943

File tree

3 files changed

+0
-295
lines changed

3 files changed

+0
-295
lines changed

src/main/scala/inox/ast/Expressions.scala

Lines changed: 0 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33
package inox
44
package ast
55

6-
import scala.collection.immutable
76
import scala.collection.immutable.BitSet
87

98
/** Expression definitions for Pure Scala.
@@ -233,26 +232,7 @@ trait Expressions { self: Trees =>
233232
/** $encodingof a floating point literal */
234233
sealed case class FPLiteral(exponent: Int, significand: Int, value: BitSet) extends Literal[BitSet] {
235234
override def getType(using Symbols) = FPType(exponent, significand)
236-
def isNegative: Boolean = !isNaN && value(exponent + significand)
237-
def isPositive: Boolean = !isNaN && !isNegative
238-
def isZero: Boolean = !Range(1, significand + exponent).exists(value)
239-
def isNumber: Boolean = !Range(significand, significand + exponent).forall(value)
240-
def isNaN: Boolean = !isNumber && Range(1, significand).exists(value)
241-
def isInfinite: Boolean = !isNumber && !isNaN
242235
def toBV: BVLiteral = BVLiteral(true, value, exponent + significand)
243-
244-
def strictEquals(obj: Any): Boolean = obj match {
245-
case lit @ FPLiteral(e2, s2, v2) => exponent == e2 && significand == s2 && value == v2
246-
case _ => false
247-
}
248-
249-
/** Semantic equality for FP */
250-
def semEquals(obj: Any): Boolean = obj match
251-
case lit @ FPLiteral(e2, s2, v2) =>
252-
!isNaN && !lit.isNaN && ((isZero && lit.isZero) || strictEquals(obj))
253-
case _ => strictEquals(obj)
254-
255-
override def equals(obj: Any): Boolean = strictEquals(obj)
256236
}
257237

258238
object FPLiteral {

src/test/scala/inox/ast/FloatingPointSuite.scala

Lines changed: 0 additions & 273 deletions
This file was deleted.

src/test/scala/inox/solvers/SemanticsSuite.scala

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -449,7 +449,6 @@ class SemanticsSuite extends AnyFunSuite {
449449

450450

451451
for (i <- floatValues; j <- floatValues) {
452-
check(s, FPEquals(Float32Literal(i), Float32Literal(j)), BooleanLiteral(Float32Literal(i).semEquals(Float32Literal(j))))
453452
check(s, FPEquals(Float32Literal(i), Float32Literal(j)), BooleanLiteral(i == j))
454453
check(s, GreaterEquals(Float32Literal(i), Float32Literal(j)), BooleanLiteral(i >= j))
455454
check(s, GreaterThan(Float32Literal(i), Float32Literal(j)), BooleanLiteral(i > j))
@@ -480,7 +479,6 @@ class SemanticsSuite extends AnyFunSuite {
480479
check(s, FPIsNaN(Float32Literal(Float.NaN)), BooleanLiteral(true))
481480

482481
for (i <- doubleValues; j <- doubleValues) {
483-
check(s, FPEquals(Float64Literal(i), Float64Literal(j)), BooleanLiteral(Float64Literal(i).semEquals(Float64Literal(j))))
484482
check(s, FPEquals(Float64Literal(i), Float64Literal(j)), BooleanLiteral(i == j))
485483
check(s, GreaterEquals(Float64Literal(i), Float64Literal(j)), BooleanLiteral(i >= j))
486484
check(s, GreaterThan(Float64Literal(i), Float64Literal(j)), BooleanLiteral(i > j))

0 commit comments

Comments
 (0)