E4M3: Add support for encoding infinities

Golds/encodeE4M3_+inf.gold

@@ -0,0 +1,14 @@
+Arguments: -fe4m3    inf
+Exit code: ExitSuccess
+Satisfiable. Model:
+  ENCODED = NaN :: E4M3
+                  7 6543 210
+                  S -E4- S3-
+   Binary layout: 0 1111 111
+      Hex layout: 7F
+       Precision: 4 exponent bits, 3 significand bits
+            Sign: Positive
+        Exponent: 8 (Stored: 15, Bias: 7)
+  Classification: FP_NAN (Quiet)
+           Value: NaN
+            Note: The input value was infinite, which is not representable in E4M3.

Golds/encodeE4M3_-inf.gold

@@ -0,0 +1,14 @@
+Arguments: -fe4m3 -- -inf
+Exit code: ExitSuccess
+Satisfiable. Model:
+  ENCODED = NaN :: E4M3
+                  7 6543 210
+                  S -E4- S3-
+   Binary layout: 0 1111 111
+      Hex layout: 7F
+       Precision: 4 exponent bits, 3 significand bits
+            Sign: Positive
+        Exponent: 8 (Stored: 15, Bias: 7)
+  Classification: FP_NAN (Quiet)
+           Value: NaN
+            Note: The input value was infinite, which is not representable in E4M3.

src/CrackNum/Main.hs

@@ -20,7 +20,7 @@ module Main(main) where
 
 import Control.Monad         (when)
 import Data.Char             (isDigit, isSpace, toLower)
-import Data.List             (isPrefixOf, isSuffixOf, unfoldr, isInfixOf)
+import Data.List             (isPrefixOf, isSuffixOf, unfoldr, isInfixOf, intercalate)
 import Data.Maybe            (fromMaybe)
 
 import Text.Read             (readMaybe)
@@ -597,8 +597,9 @@ encodeE4M3 debug inp = case reads (fixup True inp) of
                   , verbose  = debug
                   }
 
-       fixEncoded res@(SatResult (Satisfiable{})) = mapM_ putStrLn (concatMap fixNaN (map fixType (lines (show res))))
-       fixEncoded res                             = print res
+       fixEncoded :: SatResult -> String
+       fixEncoded res@(SatResult (Satisfiable{})) = intercalate "\n" $ map fixType (lines (show res))
+       fixEncoded res                             = show res
 
        fixType :: String -> String
        fixType s
@@ -607,6 +608,8 @@ encodeE4M3 debug inp = case reads (fixup True inp) of
          | True
          = s
 
+       onEach f = intercalate "\n" . concatMap f . lines
+
        -- nan representation is unique for E4M3
        fixNaN :: String -> [String]
        fixNaN s | "Representation for NaN's is not unique" `isInfixOf` s = []
@@ -616,8 +619,15 @@ encodeE4M3 debug inp = case reads (fixup True inp) of
        analyze v
          -- NaN has two representations, with surface value S.1111.111; we use 0x7F for simplicity
          | isNaN v
-         = fixEncoded =<< satWith config{crackNumSurfaceVals = [("ENCODED", 0x7F)]}
-                                  (do x :: SFloatingPoint 4 4 <- sFloatingPoint "ENCODED"
-                                      constrain $ fpIsNaN x)
+         = do res <- satWith config{crackNumSurfaceVals = [("ENCODED", 0x7F)]}
+                             (do x :: SFloatingPoint 4 4 <- sFloatingPoint "ENCODED"
+                                 constrain $ fpIsNaN x)
+              putStrLn $ onEach fixNaN $ fixEncoded res
+         | isInfinite v
+         = do res <- satWith config{crackNumSurfaceVals = [("ENCODED", 0x7F)]}
+                             (do x :: SFloatingPoint 4 4 <- sFloatingPoint "ENCODED"
+                                 constrain $ fpIsNaN x)
+              putStrLn $ onEach fixNaN $ fixEncoded res
+              putStrLn "            Note: The input value was infinite, which is not representable in E4M3."
          | True
          = error "not supported yet"

src/CrackNum/TestSuite.hs

@@ -70,7 +70,9 @@ tests = testGroup "CrackNum" [
              , gold "encode16" "-fe5m2 2.5"
             ]
           , testGroup "EncodeE4M3" [
-               gold "encodeE4M3_nan" "-fe4m3 nan"
+               gold "encodeE4M3_nan"  "-fe4m3    nan"
+            ,  gold "encodeE4M3_+inf" "-fe4m3    inf"
+            ,  gold "encodeE4M3_-inf" "-fe4m3 -- -inf"
             ]
           , testGroup "Decode" [
                gold "decode0" "-i4       0b0110"