Use text (instead of integer) to represent special variable in SAT2NAESATInfo's JSON encoding

src/ToySolver/Converter/NAESAT.hs

@@ -100,12 +100,13 @@ instance J.ToJSON SAT2NAESATInfo where
   toJSON (SAT2NAESATInfo z) =
     J.object
     [ "type" .= ("SAT2NAESATInfo" :: J.Value)
-    , "special_variable" .= z
+    , "special_variable" .= (jVarName z :: J.Value)
     ]
 
 instance J.FromJSON SAT2NAESATInfo where
-  parseJSON = withTypedObject "SAT2NAESATInfo" $ \obj ->
-    SAT2NAESATInfo <$> obj .: "special_variable" -- TODO: use Text instead of Int
+  parseJSON = withTypedObject "SAT2NAESATInfo" $ \obj -> do
+    z <- parseVarName =<< (obj .: "special_variable")
+    pure $ SAT2NAESATInfo z
 
 -- | Information of 'naesat2sat' conversion
 type NAESAT2SATInfo = IdentityTransformer SAT.Model
@@ -177,14 +178,13 @@ instance J.ToJSON NAESAT2NAEKSATInfo where
     , "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))
+        [ ( jVarName v :: J.Value
+          , map (jLitName . SAT.unpackLit) (VG.toList cs1) :: [J.Value]
+          , map (jLitName . SAT.unpackLit) (VG.toList cs2) :: [J.Value]
+          )
         | (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

src/ToySolver/Converter/PB.hs

@@ -87,7 +87,6 @@ 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
@@ -420,7 +419,7 @@ instance J.ToJSON PBInequalitiesToEqualitiesInfo where
         [ J.object
           [ "lhs" .= jPBSum lhs
           , "rhs" .= rhs
-          , "slack" .= [fromString ("x" ++ show v) :: J.Value | v <- vs]
+          , "slack" .= [jVarName v :: J.Value | v <- vs]
           ]
         | (lhs, rhs, vs) <- defs
         ]
@@ -577,7 +576,7 @@ instance J.ToJSON WBO2PBInfo where
     , "num_original_variables" .= nv1
     , "num_transformed_variables" .= nv2
     , "definitions" .= J.object
-        [ fromString ("x" ++ show v) .= jPBConstraint constr
+        [ jVarName v .= jPBConstraint constr
         | (v, constr) <- IntMap.toList defs
         ]
     ]

src/ToySolver/Converter/Tseitin.hs

@@ -23,7 +23,6 @@ import Data.Aeson ((.=), (.:))
 import Data.Array.IArray
 import qualified Data.IntMap.Strict as IntMap
 import qualified Data.Map.Lazy as Map
-import Data.String
 import qualified Data.Text as T
 import ToySolver.Converter.Base
 import ToySolver.Internal.JSON
@@ -57,7 +56,7 @@ instance J.ToJSON TseitinInfo where
     , "num_original_variables" .= nv1
     , "num_transformed_variables" .= nv2
     , "definitions" .= J.object
-        [ fromString ("x" ++ show v) .= formula
+        [ jVarName v .= formula
         | (v, formula) <- IntMap.toList defs
         ]
     ]

src/ToySolver/SAT/Internal/JSON.hs

@@ -10,6 +10,7 @@ import Control.Monad
 import qualified Data.Aeson as J
 import qualified Data.Aeson.Types as J
 import Data.Aeson ((.=), (.:))
+import Data.String
 import qualified Data.Text as T
 
 import qualified Data.PseudoBoolean as PBFile
@@ -19,9 +20,17 @@ import qualified ToySolver.SAT.Types as SAT
 jVar :: SAT.Var -> J.Value
 jVar v = J.object
   [ "type" .= ("variable" :: J.Value)
-  , "name" .= ("x" ++ show v)
+  , "name" .= (jVarName v :: J.Value)
   ]
 
+jVarName :: IsString a => SAT.Var -> a
+jVarName v = fromString ("x" ++ show v)
+
+jLitName :: IsString a => SAT.Var -> a
+jLitName v
+  | v >= 0 = jVarName v
+  | otherwise = fromString ("~x" ++ show (- v))
+
 parseVar :: J.Value -> J.Parser SAT.Var
 parseVar = withTypedObject "variable" $ \obj -> parseVarName =<< obj .: "name"