From e2f6a008feb304fd4e6497bfc41a4a32740e2adf Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 10 Nov 2019 21:13:06 +0000
Subject: Add counter example parsing

---
 src/Verismith.hs | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

(limited to 'src/Verismith.hs')

diff --git a/src/Verismith.hs b/src/Verismith.hs
index 19237ae..48f851e 100644
--- a/src/Verismith.hs
+++ b/src/Verismith.hs
@@ -72,6 +72,19 @@ import           Verismith.Tool.Internal
 import           Verismith.Verilog
 import           Verismith.Verilog.Parser (parseSourceInfoFile)
 
+-- | Generate a specific number of random bytestrings of size 256.
+randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString]
+randomByteString gen n bytes
+    | n == 0    = ranBytes : bytes
+    | otherwise = randomByteString newGen (n - 1) $ ranBytes : bytes
+    where Right (ranBytes, newGen) = C.genBytes 32 gen
+
+-- | generates the specific number of bytestring with a random seed.
+generateByteString :: Int -> IO [ByteString]
+generateByteString n = do
+    gen <- C.newGenIO :: IO C.CtrDRBG
+    return $ randomByteString gen n []
+
 toFP :: String -> FilePath
 toFP = fromText . T.pack
 
@@ -196,10 +209,10 @@ handleOpts (Reduce f t _ ls' True) = do
                     runSynth b src
                     runEquiv (toFP datadir) a b src
             case res of
-                Pass _            -> putStrLn "Equivalence check passed"
-                Fail EquivFail    -> putStrLn "Equivalence check failed"
-                Fail TimeoutError -> putStrLn "Equivalence check timed out"
-                Fail _            -> putStrLn "Equivalence check error"
+                Pass _             -> putStrLn "Equivalence check passed"
+                Fail (EquivFail _) -> putStrLn "Equivalence check failed"
+                Fail TimeoutError  -> putStrLn "Equivalence check timed out"
+                Fail _             -> putStrLn "Equivalence check error"
             return ()
         as -> do
             putStrLn "Synthesis check"
@@ -218,19 +231,6 @@ defaultMain = do
     optsparsed <- execParser opts
     handleOpts optsparsed
 
--- | Generate a specific number of random bytestrings of size 256.
-randomByteString :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString]
-randomByteString gen n bytes
-    | n == 0    = ranBytes : bytes
-    | otherwise = randomByteString newGen (n - 1) $ ranBytes : bytes
-    where Right (ranBytes, newGen) = C.genBytes 32 gen
-
--- | generates the specific number of bytestring with a random seed.
-generateByteString :: Int -> IO [ByteString]
-generateByteString n = do
-    gen <- C.newGenIO :: IO C.CtrDRBG
-    return $ randomByteString gen n []
-
 makeSrcInfo :: ModDecl -> SourceInfo
 makeSrcInfo m = SourceInfo (getIdentifier $ m ^. modId) (Verilog [m])
 
-- 
cgit