add test cases for ToJSON/FromJSON instances of converters

test/Test/Converter.hs

@@ -5,6 +5,7 @@
 module Test.Converter (converterTestGroup) where
 
 import Control.Monad
+import qualified Data.Aeson as J
 import Data.Array.IArray
 import qualified Data.Foldable as F
 import Data.Maybe
@@ -47,6 +48,13 @@ prop_sat2naesat_backward = forAll arbitraryCNF $ \cnf ->
         forAllAssignments (fst nae) $ \m ->
           evalCNF (transformBackward info m) cnf === evalNAESAT m nae
 
+prop_sat2naesat_json :: Property
+prop_sat2naesat_json = forAll arbitraryCNF $ \cnf ->
+  let ret@(_,info) = sat2naesat cnf
+      json = J.encode info
+   in counterexample (show ret) $ counterexample (show json) $
+        J.eitherDecode json === Right info
+
 prop_naesat2sat_forward :: Property
 prop_naesat2sat_forward = forAll arbitraryNAESAT $ \nae ->
   let ret@(cnf,info) = naesat2sat nae
@@ -61,6 +69,13 @@ prop_naesat2sat_backward = forAll arbitraryNAESAT $ \nae ->
         forAllAssignments (CNF.cnfNumVars cnf) $ \m ->
           evalNAESAT (transformBackward info m) nae === evalCNF m cnf
 
+prop_naesat2sat_json :: Property
+prop_naesat2sat_json = forAll arbitraryNAESAT $ \nae ->
+  let ret@(_,info) = naesat2sat nae
+      json = J.encode info
+   in counterexample (show ret) $ counterexample (show json) $
+        J.eitherDecode json === Right info
+
 prop_naesat2naeksat_forward :: Property
 prop_naesat2naeksat_forward =
   forAll arbitraryNAESAT $ \nae ->
@@ -81,6 +96,15 @@ prop_naesat2naeksat_backward =
           forAll (arbitraryAssignment (fst nae')) $ \m ->
             evalNAESAT (transformBackward info m) nae || not (evalNAESAT m nae')
 
+prop_naesat2naeksat_json :: Property
+prop_naesat2naeksat_json =
+  forAll arbitraryNAESAT $ \nae ->
+  forAll (choose (3,10)) $ \k ->
+    let ret@(_,info) = naesat2naeksat k nae
+        json = J.encode info
+     in counterexample (show ret) $ counterexample (show json) $
+          J.eitherDecode json === Right info
+
 prop_naesat2maxcut_forward :: Property
 prop_naesat2maxcut_forward =
   forAll arbitraryNAESAT $ \nae ->
@@ -99,6 +123,14 @@ prop_naesat2max2sat_forward =
               Nothing -> property False
               Just v -> evalNAESAT m nae === (v <= threshold)
 
+prop_naesat2max2sat_json :: Property
+prop_naesat2max2sat_json =
+  forAll arbitraryNAESAT $ \nae ->
+    let ret@(_, info) = naesat2max2sat nae
+        json = J.encode info
+     in counterexample (show ret) $ counterexample (show json) $
+          J.eitherDecode json === Right info
+
 ------------------------------------------------------------------------
 
 prop_satToMaxSAT2_forward :: Property
@@ -114,6 +146,14 @@ prop_satToMaxSAT2_forward =
                     Just v -> v <= threshold
        ]
 
+prop_satToMaxSAT2_json :: Property
+prop_satToMaxSAT2_json =
+  forAll arbitraryCNF $ \cnf ->
+    let ret@(_, info) = satToMaxSAT2 cnf
+        json = J.encode info
+     in counterexample (show ret) $ counterexample (show json) $
+          J.eitherDecode json === Right info
+
 prop_simplifyMaxSAT2_forward :: Property
 prop_simplifyMaxSAT2_forward =
   forAll arbitraryMaxSAT2 $ \(wcnf, th1) ->
@@ -128,6 +168,14 @@ prop_simplifyMaxSAT2_forward =
              b2 = o2 <= th2
        ]
 
+prop_simplifyMaxSAT2_json :: Property
+prop_simplifyMaxSAT2_json =
+  forAll arbitraryMaxSAT2 $ \(wcnf, th1) ->
+    let ret@(_, info) = simplifyMaxSAT2 (wcnf, th1)
+        json = J.encode info
+     in counterexample (show ret) $ counterexample (show json) $
+          J.eitherDecode json === Right info
+
 prop_maxSAT2ToSimpleMaxCut_forward :: Property
 prop_maxSAT2ToSimpleMaxCut_forward =
   forAll arbitraryMaxSAT2 $ \(wcnf, th1) ->

toysolver.cabal

@@ -925,6 +925,7 @@ Test-suite TestSuite
     Smtlib.Syntax.Syntax
     Smtlib.Syntax.ShowSL
   Build-depends:
+    aeson,
     array,
     base,
     bytestring,