Add ToJSON instances to converters (WIP)

app/toyconvert.hs

@@ -18,6 +18,7 @@ module Main where
 
 import Control.Applicative
 import Control.Monad
+import qualified Data.Aeson as J
 import qualified Data.ByteString.Builder as ByteStringBuilder
 import Data.Char
 import Data.Default.Class
@@ -259,7 +260,7 @@ supportedFormatsDoc =
 #endif
 
 data Trail sol where
-  Trail :: Transformer a => a -> Trail (Target a)
+  Trail :: (Transformer a, J.ToJSON a) => a -> Trail (Target a)
 
 data Problem
   = ProbOPB PBFile.Formula (Trail SAT.Model)
@@ -390,10 +391,10 @@ writeProblem o problem = do
         , MIP2SMT.optOptimize     = optSMTOptimize o
         }
 
-      writeInfo :: Transformer a => a -> IO ()
+      writeInfo :: (Transformer a, J.ToJSON a) => a -> IO ()
       writeInfo info =
         case optInfoOutput o of
-          Just fname -> writeFile fname (show info)
+          Just fname -> J.encodeFile fname info
           Nothing -> return ()
 
       writeInfo' :: Trail a -> IO ()

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/PB.hs

@@ -1,6 +1,7 @@
 {-# OPTIONS_GHC -Wall #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
 {-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
 -- |
@@ -68,6 +69,9 @@
 import Control.Monad
 import Control.Monad.Primitive
 import Control.Monad.ST
+import qualified Data.Aeson as J
+import qualified Data.Aeson.KeyMap as KeyMap
+import Data.Aeson ((.=))
 import Data.Array.IArray
 import Data.Bits hiding (And (..))
 import Data.Default.Class
@@ -84,6 +88,7 @@
 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 +100,7 @@
 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 +318,12 @@
 instance ObjValueBackwardTransformer PBQuadratizeInfo where
   transformObjValueBackward _ = id
 
+instance J.ToJSON PBQuadratizeInfo where
+  toJSON (PBQuadratizeInfo info) =
+    case J.toJSON info of
+      J.Object obj -> J.Object $ KeyMap.insert "type" (J.String "PBQuadratizeInfo") obj
+      _ -> undefined
+
 -- -----------------------------------------------------------------------------
 
 -- | Convert inequality constraints into equality constraints by introducing surpass variables.
@@ -388,6 +400,22 @@
 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,12 @@
 instance ObjValueBackwardTransformer PBUnconstrainInfo where
   transformObjValueBackward (PBUnconstrainInfo info) = transformObjValueBackward info
 
+instance J.ToJSON PBUnconstrainInfo where
+  toJSON (PBUnconstrainInfo info) =
+    case J.toJSON info of
+      J.Object obj -> J.Object $ KeyMap.insert "type" (J.String "PBUnconstrainInfo") obj
+      _ -> undefined
+
 unconstrainPB' :: PBFile.Formula -> (PBFile.Formula, Integer)
 unconstrainPB' formula =
   ( formula
@@ -506,6 +540,18 @@
 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

src/ToySolver/Converter/QUBO.hs

@@ -1,5 +1,6 @@
 {-# OPTIONS_GHC -Wall #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
@@ -32,6 +33,8 @@ module ToySolver.Converter.QUBO
 
 import Control.Monad
 import Control.Monad.State
+import qualified Data.Aeson as J
+import Data.Aeson ((.=))
 import Data.Array.Unboxed
 import Data.IntMap.Strict (IntMap)
 import qualified Data.IntMap.Strict as IntMap
@@ -92,6 +95,13 @@ instance (Eq a, Show a, Read a, Real a) => ObjValueForwardTransformer (QUBO2PBIn
 instance (Eq a, Show a, Read a, Num a) => ObjValueBackwardTransformer (QUBO2PBInfo a) where
   transformObjValueBackward (QUBO2PBInfo d) obj = fromInteger $ (obj + d - 1) `div` d
 
+instance J.ToJSON (QUBO2PBInfo a) where
+  toJSON (QUBO2PBInfo d) =
+    J.object
+    [ "type" .= J.String "PBAsQUBOInfo"
+    , "objective_function_multiply" .= d
+    ]
+
 -- -----------------------------------------------------------------------------
 
 pbAsQUBO :: forall a. Real a => PBFile.Formula -> Maybe (QUBO.Problem a, PBAsQUBOInfo a)
@@ -144,6 +154,13 @@ instance Num a => ObjValueForwardTransformer (PBAsQUBOInfo a) where
 instance Real a => ObjValueBackwardTransformer (PBAsQUBOInfo a) where
   transformObjValueBackward (PBAsQUBOInfo offset) obj = round (toRational obj) + offset
 
+instance J.ToJSON (PBAsQUBOInfo a) where
+  toJSON (PBAsQUBOInfo offset) =
+    J.object
+    [ "type" .= J.String "PBAsQUBOInfo"
+    , "objective_function_subtract" .= offset
+    ]
+
 -- -----------------------------------------------------------------------------
 
 pb2qubo :: Real a => PBFile.Formula -> ((QUBO.Problem a, a), PB2QUBOInfo a)