Add ToJSON/FromJSON instances to converters

src/ToySolver/Converter/Base.hs

@@ -1,6 +1,7 @@
 {-# OPTIONS_GHC -Wall #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 -----------------------------------------------------------------------------
@@ -26,6 +27,9 @@ module ToySolver.Converter.Base
   , ReversedTransformer (..)
   ) where
 
+import qualified Data.Aeson as J
+import Data.Aeson ((.=), (.:))
+import ToySolver.Internal.JSON (withTypedObject)
 
 class (Eq a, Show a) => Transformer a where
   type Source a
@@ -78,6 +82,19 @@ instance (ObjValueBackwardTransformer a, ObjValueBackwardTransformer b, TargetOb
   => ObjValueBackwardTransformer (ComposedTransformer a b) where
   transformObjValueBackward (ComposedTransformer a b) = transformObjValueBackward a . transformObjValueBackward b
 
+instance (J.ToJSON a, J.ToJSON b) => J.ToJSON (ComposedTransformer a b) where
+  toJSON (ComposedTransformer a b) =
+    J.object
+    [ "type" .= J.String "ComposedTransformer"
+    , "first" .= a
+    , "second" .= b
+    ]
+
+instance (J.FromJSON a, J.FromJSON b) => J.FromJSON (ComposedTransformer a b) where
+  parseJSON = withTypedObject "ComposedTransformer" $ \obj -> do
+    ComposedTransformer
+      <$> obj .: "first"
+      <*> obj .: "second"
 
 
 data IdentityTransformer a = IdentityTransformer
@@ -93,6 +110,15 @@ instance ForwardTransformer (IdentityTransformer a) where
 instance BackwardTransformer (IdentityTransformer a) where
   transformBackward IdentityTransformer = id
 
+instance J.ToJSON (IdentityTransformer a) where
+  toJSON IdentityTransformer =
+    J.object
+    [ "type" .= J.String "IdentityTransformer"
+    ]
+
+instance J.FromJSON (IdentityTransformer a) where
+  parseJSON = withTypedObject "IdentityTransformer" $ \_ -> pure IdentityTransformer
+
 
 data ReversedTransformer t = ReversedTransformer t
   deriving (Eq, Show, Read)
@@ -116,3 +142,14 @@ instance ObjValueBackwardTransformer t => ObjValueForwardTransformer (ReversedTr
 
 instance ObjValueForwardTransformer t => ObjValueBackwardTransformer (ReversedTransformer t) where
   transformObjValueBackward (ReversedTransformer t) = transformObjValueForward t
+
+instance J.ToJSON t => J.ToJSON (ReversedTransformer t) where
+  toJSON (ReversedTransformer t) =
+    J.object
+    [ "type" .= J.String "ReversedTransformer"
+    , "base" .= t
+    ]
+
+instance J.FromJSON t => J.FromJSON (ReversedTransformer t) where
+  parseJSON = withTypedObject "ReversedTransformer" $ \v ->
+    ReversedTransformer <$> v .: "base"

src/ToySolver/Converter/GCNF2MaxSAT.hs

@@ -1,5 +1,6 @@
 {-# OPTIONS_GHC -Wall #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
 -- |
@@ -17,9 +18,12 @@ module ToySolver.Converter.GCNF2MaxSAT
   , GCNF2MaxSATInfo (..)
   ) where
 
+import qualified Data.Aeson as J
+import Data.Aeson ((.=), (.:))
 import qualified Data.Vector.Generic as VG
 import ToySolver.Converter.Base
 import qualified ToySolver.FileFormat.CNF as CNF
+import ToySolver.Internal.JSON
 import qualified ToySolver.SAT.Types as SAT
 
 data GCNF2MaxSATInfo = GCNF2MaxSATInfo !Int
@@ -32,6 +36,17 @@ instance Transformer GCNF2MaxSATInfo where
 instance BackwardTransformer GCNF2MaxSATInfo where
   transformBackward (GCNF2MaxSATInfo nv1) = SAT.restrictModel nv1
 
+instance J.ToJSON GCNF2MaxSATInfo where
+  toJSON (GCNF2MaxSATInfo nv) =
+    J.object
+    [ "type" .= J.String "GCNF2MaxSATInfo"
+    , "num_original_variables" .= nv
+    ]
+
+instance J.FromJSON GCNF2MaxSATInfo where
+  parseJSON = withTypedObject "GCNF2MaxSATInfo" $ \obj ->
+    GCNF2MaxSATInfo <$> obj .: "num_original_variables"
+
 gcnf2maxsat :: CNF.GCNF -> (CNF.WCNF, GCNF2MaxSATInfo)
 gcnf2maxsat
   CNF.GCNF

src/ToySolver/Converter/MIP2PB.hs

@@ -1,6 +1,7 @@
 {-# OPTIONS_GHC -Wall #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
 -- |
@@ -23,21 +24,26 @@ import Control.Monad
 import Control.Monad.ST
 import Control.Monad.Trans
 import Control.Monad.Trans.Except
+import qualified Data.Aeson as J
+import Data.Aeson ((.=), (.:))
 import Data.List (intercalate, foldl', sortBy)
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Ord
 import Data.Ratio
 import qualified Data.Set as Set
+import Data.String
 import Data.VectorSpace
 
 import qualified Data.PseudoBoolean as PBFile
 import qualified Numeric.Optimization.MIP as MIP
 
 import ToySolver.Converter.Base
 import ToySolver.Data.OrdRel
+import ToySolver.Internal.JSON
 import qualified ToySolver.SAT.Types as SAT
 import qualified ToySolver.SAT.Encoder.Integer as Integer
+import ToySolver.SAT.Internal.JSON
 import ToySolver.SAT.Store.PB
 import ToySolver.Internal.Util (revForM)
 
@@ -73,6 +79,25 @@ instance ObjValueForwardTransformer MIP2PBInfo where
 instance ObjValueBackwardTransformer MIP2PBInfo where
   transformObjValueBackward (MIP2PBInfo _vmap d) val = fromIntegral val / fromIntegral d
 
+instance J.ToJSON MIP2PBInfo where
+  toJSON (MIP2PBInfo vmap d) =
+    J.object
+    [ "type" .= J.String "MIP2PBInfo"
+    , "substitutions" .= J.object
+        [ fromString (MIP.fromVar v) .= jPBSum s
+        | (v, Integer.Expr s) <- Map.toList vmap
+        ]
+    , "objective_function_scale_factor" .= d
+    ]
+
+instance J.FromJSON MIP2PBInfo where
+  parseJSON = withTypedObject "MIP2PBInfo" $ \obj -> do
+    subst <- obj .: "substitutions"
+    d <- obj .: "objective_function_scale_factor"
+    pure $ MIP2PBInfo
+      (Map.fromList [(MIP.toVar name, Integer.Expr expr) | (name, expr) <- Map.toList subst])
+      d
+
 -- -----------------------------------------------------------------------------
 
 addMIP :: SAT.AddPBNL m enc => enc -> MIP.Problem Rational -> m (Either String (Integer.Expr, MIP2PBInfo))

src/ToySolver/Converter/NAESAT.hs

@@ -2,6 +2,7 @@
 {-# OPTIONS_HADDOCK show-extensions #-}
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
 -- |
@@ -43,12 +44,16 @@ module ToySolver.Converter.NAESAT
 
 import Control.Monad
 import Control.Monad.State.Strict
+import qualified Data.Aeson as J
+import Data.Aeson ((.=), (.:))
 import Data.Array.Unboxed
 import qualified Data.IntMap as IntMap
 import qualified Data.Vector.Generic as VG
 import qualified Data.Vector.Unboxed as VU
 import ToySolver.Converter.Base
+import ToySolver.Internal.JSON
 import qualified ToySolver.FileFormat.CNF as CNF
+import ToySolver.SAT.Internal.JSON
 import qualified ToySolver.SAT.Types as SAT
 
 type NAESAT = (Int, [NAEClause])
@@ -91,6 +96,17 @@ instance BackwardTransformer SAT2NAESATInfo where
     SAT.restrictModel (z - 1) $
       if SAT.evalVar m z then amap not m else m
 
+instance J.ToJSON SAT2NAESATInfo where
+  toJSON (SAT2NAESATInfo z) =
+    J.object
+    [ "type" .= J.String "SAT2NAESATInfo"
+    , "special_variable" .= z
+    ]
+
+instance J.FromJSON SAT2NAESATInfo where
+  parseJSON = withTypedObject "SAT2NAESATInfo" $ \obj ->
+    SAT2NAESATInfo <$> obj .: "special_variable" -- TODO: use Text instead of Int
+
 -- | Information of 'naesat2sat' conversion
 type NAESAT2SATInfo = IdentityTransformer SAT.Model
 
@@ -154,6 +170,35 @@ instance ForwardTransformer NAESAT2NAEKSATInfo where
 instance BackwardTransformer NAESAT2NAEKSATInfo where
   transformBackward (NAESAT2NAEKSATInfo n1 _n2 _table) = SAT.restrictModel n1
 
+instance J.ToJSON NAESAT2NAEKSATInfo where
+  toJSON (NAESAT2NAEKSATInfo nv1 nv2 table) =
+    J.object
+    [ "type" .= J.String "NAESAT2NAEKSATInfo"
+    , "num_original_variables" .= nv1
+    , "num_transformed_variables" .= nv2
+    , "table" .=
+        [ (f v, map (f . SAT.unpackLit) (VG.toList cs1), map (f . SAT.unpackLit) (VG.toList cs2))
+        | (v, cs1, cs2) <- table
+        ]
+    ]
+    where
+      f lit
+        | lit < 0   = "~x" ++ show (- lit)
+        | otherwise = "x" ++ show lit
+
+instance J.FromJSON NAESAT2NAEKSATInfo where
+  parseJSON = withTypedObject "NAESAT2NAEKSATInfo" $ \obj -> do
+    NAESAT2NAEKSATInfo
+      <$> obj .: "num_original_variables"
+      <*> obj .: "num_transformed_variables"
+      <*> (mapM f =<< obj .: "table")
+    where
+      f (v, cs1, cs2) = do
+        v' <- parseVarNameText v
+        cs1' <- mapM parseLitNameText cs1
+        cs2' <- mapM parseLitNameText cs2
+        return (v', VG.fromList (map SAT.packLit cs1'), VG.fromList (map SAT.packLit cs2'))
+
 -- ------------------------------------------------------------------------
 
 type NAESAT2Max2SATInfo = ComposedTransformer NAESAT2NAEKSATInfo NAE3SAT2Max2SATInfo