add ToJSON 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,8 @@ module ToySolver.Converter.Base
   , ReversedTransformer (..)
   ) where
 
+import qualified Data.Aeson as J
+import Data.Aeson ((.=))
 
 class (Eq a, Show a) => Transformer a where
   type Source a
@@ -78,6 +81,13 @@ 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" .= J.toJSON a
+    , "second" .= J.toJSON b
+    ]
 
 
 data IdentityTransformer a = IdentityTransformer
@@ -93,6 +103,12 @@ 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"
+    ]
+
 
 data ReversedTransformer t = ReversedTransformer t
   deriving (Eq, Show, Read)
@@ -116,3 +132,10 @@ 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"
+    , "original" .= J.toJSON t
+    ]

src/ToySolver/Converter/GCNF2MaxSAT.hs

@@ -1,5 +1,6 @@
 {-# OPTIONS_GHC -Wall #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
 -- |
@@ -17,6 +18,8 @@ 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
@@ -32,6 +35,13 @@ 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
+    ]
+
 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,12 +24,15 @@ 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
@@ -38,6 +42,7 @@ import ToySolver.Converter.Base
 import ToySolver.Data.OrdRel
 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 +78,17 @@ 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_multiply" .= 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,15 @@ 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 qualified ToySolver.FileFormat.CNF as CNF
+import ToySolver.SAT.Internal.JSON
 import qualified ToySolver.SAT.Types as SAT
 
 type NAESAT = (Int, [NAEClause])
@@ -91,6 +95,13 @@ 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 "NAESAT2SATInfo"
+    , "special_variable" .= z
+    ]
+
 -- | Information of 'naesat2sat' conversion
 type NAESAT2SATInfo = IdentityTransformer SAT.Model
 
@@ -154,6 +165,18 @@ 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 "NAESAT2SATInfo"
+    , "num_original_variables" .= nv1
+    , "num_transformed_variables" .= nv2
+    , "table" .=
+        [ (v, map (jLit . SAT.unpackLit) (VG.toList cs1), map (jLit . SAT.unpackLit) (VG.toList cs2))
+        | (v, cs1, cs2) <- table
+        ]
+    ]
+
 -- ------------------------------------------------------------------------
 
 type NAESAT2Max2SATInfo = ComposedTransformer NAESAT2NAEKSATInfo NAE3SAT2Max2SATInfo

src/ToySolver/Converter/PB.hs

@@ -1,6 +1,7 @@
 {-# OPTIONS_GHC -Wall #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
 {-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
 -- |
@@ -68,6 +69,8 @@ module ToySolver.Converter.PB
 import Control.Monad
 import Control.Monad.Primitive
 import Control.Monad.ST
+import qualified Data.Aeson as J
+import Data.Aeson ((.=))
 import Data.Array.IArray
 import Data.Bits hiding (And (..))
 import Data.Default.Class
@@ -84,6 +87,7 @@ import Data.Primitive.MutVar
 import qualified Data.Sequence as Seq
 import Data.Set (Set)
 import qualified Data.Set as Set
+import Data.String
 import qualified Data.PseudoBoolean as PBFile
 
 import ToySolver.Converter.Base
@@ -95,6 +99,7 @@ import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
 import ToySolver.SAT.Encoder.Tseitin (Formula (..))
 import qualified ToySolver.SAT.Encoder.PB as PB
 import qualified ToySolver.SAT.Encoder.PBNLC as PBNLC
+import ToySolver.SAT.Internal.JSON
 import ToySolver.SAT.Store.CNF
 import ToySolver.SAT.Store.PB
 
@@ -312,6 +317,13 @@ instance ObjValueForwardTransformer PBQuadratizeInfo where
 instance ObjValueBackwardTransformer PBQuadratizeInfo where
   transformObjValueBackward _ = id
 
+instance J.ToJSON PBQuadratizeInfo where
+  toJSON (PBQuadratizeInfo info) =
+    J.object
+    [ "type" .= J.String "PBQuadratizeInfo"
+    , "base" .= info
+    ]
+
 -- -----------------------------------------------------------------------------
 
 -- | Convert inequality constraints into equality constraints by introducing surpass variables.
@@ -388,6 +400,22 @@ instance ObjValueForwardTransformer PBInequalitiesToEqualitiesInfo where
 instance ObjValueBackwardTransformer PBInequalitiesToEqualitiesInfo where
   transformObjValueBackward _ = id
 
+instance J.ToJSON PBInequalitiesToEqualitiesInfo where
+  toJSON (PBInequalitiesToEqualitiesInfo nv1 nv2 defs) =
+    J.object
+    [ "type" .= J.String "PBInequalitiesToEqualitiesInfo"
+    , "num_original_variables" .= nv1
+    , "num_transformed_variables" .= nv2
+    , "slack" .= J.toJSONList
+        [ J.object
+          [ "lhs" .= jPBSum lhs
+          , "rhs" .= rhs
+          , "slack" .= J.toJSONList [fromString ("x" ++ show v) :: J.Value | v <- vs]
+          ]
+        | (lhs, rhs, vs) <- defs
+        ]
+    ]
+
 -- -----------------------------------------------------------------------------
 
 unconstrainPB :: PBFile.Formula -> ((PBFile.Formula, Integer), PBUnconstrainInfo)
@@ -422,6 +450,13 @@ instance ObjValueForwardTransformer PBUnconstrainInfo where
 instance ObjValueBackwardTransformer PBUnconstrainInfo where
   transformObjValueBackward (PBUnconstrainInfo info) = transformObjValueBackward info
 
+instance J.ToJSON PBUnconstrainInfo where
+  toJSON (PBUnconstrainInfo info) =
+    J.object
+    [ "type" .= J.String "PBUnconstrainInfo"
+    , "base" .= info
+    ]
+
 unconstrainPB' :: PBFile.Formula -> (PBFile.Formula, Integer)
 unconstrainPB' formula =
   ( formula
@@ -506,6 +541,18 @@ instance ForwardTransformer WBO2PBInfo where
 instance BackwardTransformer WBO2PBInfo where
   transformBackward (WBO2PBInfo nv1 _nv2 _defs) = SAT.restrictModel nv1
 
+instance J.ToJSON WBO2PBInfo where
+  toJSON (WBO2PBInfo nv1 nv2 defs) =
+    J.object
+    [ "type" .= J.String "WBO2PBInfo"
+    , "num_original_variables" .= nv1
+    , "num_transformed_variables" .= nv2
+    , "definitions" .= J.object
+        [ fromString ("x" ++ show v) .= jPBConstraint constr
+        | (v, constr) <- defs
+        ]
+    ]
+
 addWBO :: (PrimMonad m, SAT.AddPBNL m enc) => enc -> PBFile.SoftFormula -> m (SAT.PBSum, [(SAT.Var, PBFile.Constraint)])
 addWBO db wbo = do
   SAT.newVars_ db $ PBFile.wboNumVars wbo

src/ToySolver/Converter/PB2IP.hs

@@ -1,5 +1,6 @@
 {-# OPTIONS_GHC -Wall #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
 -- |
@@ -24,11 +25,14 @@ module ToySolver.Converter.PB2IP
   , MaxSAT2IPInfo
   ) where
 
+import qualified Data.Aeson as J
+import Data.Aeson ((.=))
 import Data.Array.IArray
 import Data.Default.Class
 import Data.Maybe
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.String
 
 import qualified Data.PseudoBoolean as PBFile
 import qualified Numeric.Optimization.MIP as MIP
@@ -37,6 +41,7 @@ import Numeric.Optimization.MIP ((.==.), (.<=.), (.>=.))
 import ToySolver.Converter.Base
 import ToySolver.Converter.PB
 import qualified ToySolver.FileFormat.CNF as CNF
+import ToySolver.SAT.Internal.JSON
 import qualified ToySolver.SAT.Types as SAT
 
 -- -----------------------------------------------------------------------------
@@ -55,6 +60,13 @@ instance ForwardTransformer PB2IPInfo where
 instance BackwardTransformer PB2IPInfo where
   transformBackward (PB2IPInfo nv) = mtrans nv
 
+instance J.ToJSON PB2IPInfo where
+  toJSON (PB2IPInfo nv) =
+    J.object
+    [ "type" .= J.String "PB2IPInfo"
+    , "num_original_variables" .= nv
+    ]
+
 pb2ip :: PBFile.Formula -> (MIP.Problem Integer, PB2IPInfo)
 pb2ip formula = (mip, PB2IPInfo (PBFile.pbNumVars formula))
   where
@@ -110,6 +122,17 @@ instance ForwardTransformer WBO2IPInfo where
 instance BackwardTransformer WBO2IPInfo where
   transformBackward (WBO2IPInfo nv _relaxVariables) = mtrans nv
 
+instance J.ToJSON WBO2IPInfo where
+  toJSON (WBO2IPInfo nv defs) =
+    J.object
+    [ "type" .= J.String "WBO2IPInfo"
+    , "num_original_variables" .= nv
+    , "definitions" .= J.object
+        [ fromString ("x" ++ show v) .= jPBConstraint constr
+        | (v, (Just _, constr)) <- defs
+        ]
+    ]
+
 wbo2ip :: Bool -> PBFile.SoftFormula -> (MIP.Problem Integer, WBO2IPInfo)
 wbo2ip useIndicator formula = (mip, WBO2IPInfo (PBFile.wboNumVars formula) relaxVariables)
   where