Serialization for fp arithmetic

Author: agilot

src/main/scala/inox/utils/Serialization.scala

@@ -476,7 +476,7 @@ class InoxSerializer(val trees: ast.Trees, serializeProducts: Boolean = false) e
     * The `Serializer[_]` identifiers in this mapping range from 10 to 105
     * (ignoring special identifiers that are smaller than 10).
     *
-    * NEXT ID: 106
+    * NEXT ID: 109
     */
   protected def classSerializers: Map[Class[?], Serializer[?]] = Map(
     // Inox Expressions
@@ -550,6 +550,10 @@ class InoxSerializer(val trees: ast.Trees, serializeProducts: Boolean = false) e
     classSerializer[MapUpdated]        (74),
     classSerializer[BVUnsignedToSigned](104),
     classSerializer[BVSignedToUnsigned](105),
+    // FPLiteral id=107
+    // Floating Point literals are treated specially to avoid having to serialize BitSets
+    mappingSerializer[FPLiteral](107)(fp => (fp.exponent, fp.significand, fp.value))(p => FPLiteral(p._1, p._2, p._3)),
+    classSerializer[FPEquals]          (108),
 
     // Inox Types
     classSerializer[Untyped.type] (75),
@@ -571,6 +575,7 @@ class InoxSerializer(val trees: ast.Trees, serializeProducts: Boolean = false) e
     classSerializer[RefinementType](100),
     classSerializer[PiType]        (101),
     classSerializer[SigmaType]     (102),
+    classSerializer[FPType]        (106),
 
     // Identifier
     mappingSerializer[Identifier](90)

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

@@ -406,15 +406,11 @@ class SemanticsSuite extends AnyFunSuite {
       check(s, Float32Literal(i), Float32Literal(i))
     }
 
-    check(s, Float32Literal(0), Float32Literal(0))
-    check(s, Float32Literal(-0), Float32Literal(-0))
 
     for (i <- doubleValues) {
       check(s, Float64Literal(i), Float64Literal(i))
     }
 
-    check(s, Float64Literal(0), Float64Literal(0))
-    check(s, Float64Literal(-0), Float64Literal(-0))
   }
 
   test("Floating Point Arithmetic", filterSolvers(_, princess = true)) { ctx =>