From e58f086195280d6e8239e5244fbac030655e5187 Mon Sep 17 00:00:00 2001 From: Masahiro Sakai Date: Sun, 17 Nov 2024 18:39:21 +0900 Subject: [PATCH 1/4] add ToJSON instances to converters (WIP) --- src/ToySolver/Converter/Base.hs | 23 +++++++++++ src/ToySolver/Converter/Tseitin.hs | 15 +++++++ src/ToySolver/SAT/Formula.hs | 64 ++++++++++++++++++++++++++++++ toysolver.cabal | 1 + 4 files changed, 103 insertions(+) diff --git a/src/ToySolver/Converter/Base.hs b/src/ToySolver/Converter/Base.hs index 55f6166f..ea2450e4 100644 --- a/src/ToySolver/Converter/Base.hs +++ b/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 + ] diff --git a/src/ToySolver/Converter/Tseitin.hs b/src/ToySolver/Converter/Tseitin.hs index d121cb51..29ad2fa6 100644 --- a/src/ToySolver/Converter/Tseitin.hs +++ b/src/ToySolver/Converter/Tseitin.hs @@ -1,6 +1,7 @@ {-# OPTIONS_GHC -Wall #-} {-# OPTIONS_HADDOCK show-extensions #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeFamilies #-} ----------------------------------------------------------------------------- -- | @@ -17,7 +18,10 @@ module ToySolver.Converter.Tseitin ( TseitinInfo (..) ) where +import qualified Data.Aeson as J +import Data.Aeson ((.=)) import Data.Array.IArray +import Data.String import ToySolver.Converter.Base import qualified ToySolver.SAT.Types as SAT import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin @@ -40,4 +44,15 @@ instance ForwardTransformer TseitinInfo where instance BackwardTransformer TseitinInfo where transformBackward (TseitinInfo nv1 _nv2 _defs) = SAT.restrictModel nv1 +instance J.ToJSON TseitinInfo where + toJSON (TseitinInfo nv1 nv2 defs) = + J.object + [ "num_original_variables" .= nv1 + , "num_transformed_variables" .= nv2 + , "definitions" .= J.object + [ fromString ("x" ++ show v) .= J.toJSON formula + | (v, formula) <- defs + ] + ] + -- ----------------------------------------------------------------------------- diff --git a/src/ToySolver/SAT/Formula.hs b/src/ToySolver/SAT/Formula.hs index c47c3423..16916b4d 100644 --- a/src/ToySolver/SAT/Formula.hs +++ b/src/ToySolver/SAT/Formula.hs @@ -3,6 +3,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-} @@ -27,10 +28,14 @@ module ToySolver.SAT.Formula ) where import Control.Monad.ST +import qualified Data.Aeson as J +import Data.Aeson ((.=)) import Data.Hashable import qualified Data.HashTable.Class as H import qualified Data.HashTable.ST.Cuckoo as C import Data.Interned +import Data.String +import qualified Data.Vector as V import GHC.Generics import ToySolver.Data.Boolean import qualified ToySolver.Data.BoolExpr as BoolExpr @@ -224,3 +229,62 @@ isFalse (Or []) = True isFalse _ = False -- ------------------------------------------------------------------------ + +newtype JSON = JSON{ getJSON :: J.Value } + +instance Complement JSON where + notB (JSON x) = JSON $ jNot x + +instance MonotoneBoolean JSON where + andB xs = JSON $ J.object + [ "type" .= J.String "operator" + , "name" .= J.String "and" + , "operands" .= J.Array (V.fromList [x | JSON x <- xs]) + ] + orB xs = JSON $ J.object + [ "type" .= J.String "operator" + , "name" .= J.String "or" + , "operands" .= J.Array (V.fromList [x | JSON x <- xs]) + ] + +instance IfThenElse JSON JSON where + ite (JSON c) (JSON t) (JSON e) = JSON $ J.object + [ "type" .= J.String "operator" + , "name" .= J.String "ite" + , "operands" .= J.Array (V.fromList [c, t, e]) + ] + +instance Boolean JSON where + (.=>.) (JSON p) (JSON q) = JSON $ J.object + [ "type" .= J.String "operator" + , "name" .= J.String "=>" + , "operands" .= J.Array (V.fromList [p, q]) + ] + (.<=>.) (JSON p) (JSON q) = JSON $ J.object + [ "type" .= J.String "operator" + , "name" .= J.String "<=>" + , "operands" .= J.Array (V.fromList [p, q]) + ] + +instance J.ToJSON Formula where + toJSON = getJSON . fold (JSON . jLit) + +jVar :: SAT.Var -> J.Value +jVar v = J.object + [ "type" .= J.String "variable" + , "name" .= (fromString ("x" <> show v) :: J.Value) + ] + +jNot :: J.Value -> J.Value +jNot x = J.object + [ "type" .= J.String "operator" + , "name" .= J.String "not" + , "operands" .= J.Array (V.singleton x) + ] + +jLit :: SAT.Lit -> J.Value +jLit l + | l > 0 = jVar l + | otherwise = jNot $ jVar (- l) + +-- ------------------------------------------------------------------------ diff --git a/toysolver.cabal b/toysolver.cabal index 30e55332..947f611b 100644 --- a/toysolver.cabal +++ b/toysolver.cabal @@ -127,6 +127,7 @@ Library Exposed: True Hs-source-dirs: src Build-Depends: + aeson >=1.4.2.0 && <2.3, array >=0.5, -- GHC >=8.6 && <9.11 base >=4.12 && <4.21, From 5cd8a636b4b633b55c3b6cefe849abf8ea4edb8a Mon Sep 17 00:00:00 2001 From: Masahiro Sakai Date: Tue, 19 Nov 2024 00:18:59 +0900 Subject: [PATCH 2/4] add ToJSON instances to converters (WIP) --- src/ToySolver/Converter/GCNF2MaxSAT.hs | 10 +++++ src/ToySolver/Converter/MIP2PB.hs | 16 ++++++++ src/ToySolver/Converter/PB.hs | 46 +++++++++++++++++++++ src/ToySolver/Converter/PB2IP.hs | 23 +++++++++++ src/ToySolver/Converter/QUBO.hs | 17 ++++++++ src/ToySolver/Converter/Tseitin.hs | 3 +- src/ToySolver/SAT/Formula.hs | 20 +-------- src/ToySolver/SAT/Internal/JSON.hs | 56 ++++++++++++++++++++++++++ toysolver.cabal | 1 + 9 files changed, 172 insertions(+), 20 deletions(-) create mode 100644 src/ToySolver/SAT/Internal/JSON.hs diff --git a/src/ToySolver/Converter/GCNF2MaxSAT.hs b/src/ToySolver/Converter/GCNF2MaxSAT.hs index c2f21bc9..50cf60ac 100644 --- a/src/ToySolver/Converter/GCNF2MaxSAT.hs +++ b/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 diff --git a/src/ToySolver/Converter/MIP2PB.hs b/src/ToySolver/Converter/MIP2PB.hs index 4349c31d..d5bcd5be 100644 --- a/src/ToySolver/Converter/MIP2PB.hs +++ b/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_multiplier" .= d + ] + -- ----------------------------------------------------------------------------- addMIP :: SAT.AddPBNL m enc => enc -> MIP.Problem Rational -> m (Either String (Integer.Expr, MIP2PBInfo)) diff --git a/src/ToySolver/Converter/PB.hs b/src/ToySolver/Converter/PB.hs index 4a8fc1fd..780c2a6b 100644 --- a/src/ToySolver/Converter/PB.hs +++ b/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 @@ module ToySolver.Converter.PB 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 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 +100,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 +318,12 @@ instance ObjValueForwardTransformer PBQuadratizeInfo where 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 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,12 @@ instance ObjValueForwardTransformer PBUnconstrainInfo where 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 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 diff --git a/src/ToySolver/Converter/PB2IP.hs b/src/ToySolver/Converter/PB2IP.hs index 1d8dc4b2..0329715b 100644 --- a/src/ToySolver/Converter/PB2IP.hs +++ b/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 diff --git a/src/ToySolver/Converter/QUBO.hs b/src/ToySolver/Converter/QUBO.hs index 729893d8..d46a5381 100644 --- a/src/ToySolver/Converter/QUBO.hs +++ b/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_multiplier" .= 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" + , "offset" .= offset + ] + -- ----------------------------------------------------------------------------- pb2qubo :: Real a => PBFile.Formula -> ((QUBO.Problem a, a), PB2QUBOInfo a) diff --git a/src/ToySolver/Converter/Tseitin.hs b/src/ToySolver/Converter/Tseitin.hs index 29ad2fa6..f829a984 100644 --- a/src/ToySolver/Converter/Tseitin.hs +++ b/src/ToySolver/Converter/Tseitin.hs @@ -47,7 +47,8 @@ instance BackwardTransformer TseitinInfo where instance J.ToJSON TseitinInfo where toJSON (TseitinInfo nv1 nv2 defs) = J.object - [ "num_original_variables" .= nv1 + [ "type" .= J.String "TseitinInfo" + , "num_original_variables" .= nv1 , "num_transformed_variables" .= nv2 , "definitions" .= J.object [ fromString ("x" ++ show v) .= J.toJSON formula diff --git a/src/ToySolver/SAT/Formula.hs b/src/ToySolver/SAT/Formula.hs index 16916b4d..ac711b47 100644 --- a/src/ToySolver/SAT/Formula.hs +++ b/src/ToySolver/SAT/Formula.hs @@ -34,12 +34,12 @@ import Data.Hashable import qualified Data.HashTable.Class as H import qualified Data.HashTable.ST.Cuckoo as C import Data.Interned -import Data.String import qualified Data.Vector as V import GHC.Generics import ToySolver.Data.Boolean import qualified ToySolver.Data.BoolExpr as BoolExpr import qualified ToySolver.SAT.Types as SAT +import ToySolver.SAT.Internal.JSON -- Should this module be merged into ToySolver.SAT.Types module? @@ -269,22 +269,4 @@ instance Boolean JSON where instance J.ToJSON Formula where toJSON = getJSON . fold (JSON . jLit) -jVar :: SAT.Var -> J.Value -jVar v = J.object - [ "type" .= J.String "variable" - , "name" .= (fromString ("x" <> show v) :: J.Value) - ] - -jNot :: J.Value -> J.Value -jNot x = J.object - [ "type" .= J.String "operator" - , "name" .= J.String "not" - , "operands" .= J.Array (V.singleton x) - ] - -jLit :: SAT.Lit -> J.Value -jLit l - | l > 0 = jVar l - | otherwise = jNot $ jVar (- l) - -- ------------------------------------------------------------------------ diff --git a/src/ToySolver/SAT/Internal/JSON.hs b/src/ToySolver/SAT/Internal/JSON.hs new file mode 100644 index 00000000..b95a173c --- /dev/null +++ b/src/ToySolver/SAT/Internal/JSON.hs @@ -0,0 +1,56 @@ +{-# OPTIONS_GHC -Wall #-} +{-# OPTIONS_HADDOCK show-extensions #-} +{-# LANGUAGE OverloadedStrings #-} +module ToySolver.SAT.Internal.JSON where + +import qualified Data.Aeson as J +import Data.Aeson ((.=)) +import Data.String +import qualified Data.Vector as V + +import qualified Data.PseudoBoolean as PBFile +import qualified ToySolver.SAT.Types as SAT + +jVar :: SAT.Var -> J.Value +jVar v = J.object + [ "type" .= J.String "variable" + , "name" .= (fromString ("x" <> show v) :: J.Value) + ] + +jNot :: J.Value -> J.Value +jNot x = J.object + [ "type" .= J.String "operator" + , "name" .= J.String "not" + , "operands" .= J.Array (V.singleton x) + ] + +jLit :: SAT.Lit -> J.Value +jLit l + | l > 0 = jVar l + | otherwise = jNot $ jVar (- l) + +jConst :: J.ToJSON a => a -> J.Value +jConst x = J.object ["type" .= J.String "constant", "value" .= x] + +jPBSum :: SAT.PBSum -> J.Value +jPBSum s = J.object + [ "type" .= J.String "operator" + , "name" .= J.String "+" + , "operands" .= J.toJSONList + [ J.object + [ "type" .= J.String "operator" + , "name" .= J.String "*" + , "operands" .= + J.toJSONList (jConst c : [jLit lit | lit <- lits]) + ] + | (c, lits) <- s + ] + ] + +jPBConstraint :: PBFile.Constraint -> J.Value +jPBConstraint (lhs, op, rhs) = + J.object + [ "type" .= J.String "operator" + , "name" .= J.String (case op of{ PBFile.Ge -> ">="; PBFile.Eq -> "=" }) + , "operands" .= J.toJSONList [jPBSum lhs, jConst rhs] + ] diff --git a/toysolver.cabal b/toysolver.cabal index 947f611b..311a09a7 100644 --- a/toysolver.cabal +++ b/toysolver.cabal @@ -373,6 +373,7 @@ Library ToySolver.Converter.PB.Internal.Product ToySolver.Data.AlgebraicNumber.Graeffe ToySolver.Data.Polynomial.Base + ToySolver.SAT.Internal.JSON ToySolver.SAT.MUS.Base ToySolver.SAT.MUS.Deletion ToySolver.SAT.MUS.Insertion From 1b6f133b8b8d9be0667a597c2dc3d7e02474c819 Mon Sep 17 00:00:00 2001 From: Masahiro Sakai Date: Tue, 19 Nov 2024 00:32:06 +0900 Subject: [PATCH 3/4] add ToJSON instances to converters (WIP) --- src/ToySolver/Converter/MIP2PB.hs | 2 +- src/ToySolver/Converter/QUBO.hs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ToySolver/Converter/MIP2PB.hs b/src/ToySolver/Converter/MIP2PB.hs index d5bcd5be..7d57924d 100644 --- a/src/ToySolver/Converter/MIP2PB.hs +++ b/src/ToySolver/Converter/MIP2PB.hs @@ -86,7 +86,7 @@ instance J.ToJSON MIP2PBInfo where [ fromString (MIP.fromVar v) .= jPBSum s | (v, Integer.Expr s) <- Map.toList vmap ] - , "objective_function_multiplier" .= d + , "objective_function_multiply" .= d ] -- ----------------------------------------------------------------------------- diff --git a/src/ToySolver/Converter/QUBO.hs b/src/ToySolver/Converter/QUBO.hs index d46a5381..9807736e 100644 --- a/src/ToySolver/Converter/QUBO.hs +++ b/src/ToySolver/Converter/QUBO.hs @@ -99,7 +99,7 @@ instance J.ToJSON (QUBO2PBInfo a) where toJSON (QUBO2PBInfo d) = J.object [ "type" .= J.String "PBAsQUBOInfo" - , "objective_function_multiplier" .= d + , "objective_function_multiply" .= d ] -- ----------------------------------------------------------------------------- @@ -158,7 +158,7 @@ instance J.ToJSON (PBAsQUBOInfo a) where toJSON (PBAsQUBOInfo offset) = J.object [ "type" .= J.String "PBAsQUBOInfo" - , "offset" .= offset + , "objective_function_subtract" .= offset ] -- ----------------------------------------------------------------------------- From 65e3ae494f46fb1ac7c73b5d4715a330bedd418b Mon Sep 17 00:00:00 2001 From: Masahiro Sakai Date: Tue, 19 Nov 2024 00:48:06 +0900 Subject: [PATCH 4/4] change --dump-info to output JSON --- app/toyconvert.hs | 7 ++++--- toysolver.cabal | 1 + 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/app/toyconvert.hs b/app/toyconvert.hs index ded64848..ec6f5ffa 100644 --- a/app/toyconvert.hs +++ b/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 () diff --git a/toysolver.cabal b/toysolver.cabal index 311a09a7..62934769 100644 --- a/toysolver.cabal +++ b/toysolver.cabal @@ -550,6 +550,7 @@ Executable toyconvert Main-is: toyconvert.hs HS-Source-Dirs: app Build-Depends: + aeson, base, bytestring, bytestring-builder,