Skip to content

Commit 4f56b0b

Browse files
agilotvkuncak
authored andcommitted
Add serialization for fp arithmetic rounding modes
1 parent c888ccf commit 4f56b0b

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -554,6 +554,17 @@ class InoxSerializer(val trees: ast.Trees, serializeProducts: Boolean = false) e
554554
// Floating Point literals are treated specially to avoid having to serialize BitSets
555555
mappingSerializer[FPLiteral](107)(fp => (fp.exponent, fp.significand, fp.value))(p => FPLiteral(p._1, p._2, p._3)),
556556
classSerializer[FPEquals] (108),
557+
classSerializer[FPAdd] (110),
558+
classSerializer[FPSub] (111),
559+
classSerializer[FPMul] (112),
560+
classSerializer[FPDiv] (113),
561+
classSerializer[FPCast] (114),
562+
563+
classSerializer[RoundTowardZero.type] (115),
564+
classSerializer[RoundTowardPositive.type] (116),
565+
classSerializer[RoundTowardNegative.type] (117),
566+
classSerializer[RoundNearestTiesToEven.type] (118),
567+
classSerializer[RoundNearestTiesToAway.type] (119),
557568

558569
// Inox Types
559570
classSerializer[Untyped.type] (75),
@@ -576,6 +587,7 @@ class InoxSerializer(val trees: ast.Trees, serializeProducts: Boolean = false) e
576587
classSerializer[PiType] (101),
577588
classSerializer[SigmaType] (102),
578589
classSerializer[FPType] (106),
590+
classSerializer[RoundingMode.type ] (109),
579591

580592
// Identifier
581593
mappingSerializer[Identifier](90)

0 commit comments

Comments
 (0)