msakai / toysolver / 660

Committed 13 Apr 2025 03:23PM UTC coverage: 71.204% (+0.2%) from 70.98%

Build # 660

Build Type

push

github

Committed by

msakai

Commit Message

minor: use MIP.varName instead of deprecated MIP.fromVar

Run Details

10707 of 15037 relevant lines covered (71.2%)

0.71 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

73.56

/src/ToySolver/SAT/Internal/JSON.hs

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
module ToySolver.SAT.Internal.JSON where

import Control.Applicative
import Control.Arrow ((***))
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
import ToySolver.Internal.JSON
import qualified ToySolver.SAT.Types as SAT

jVar :: SAT.Var -> J.Value
jVar v = J.object
  [ "type" .= ("variable" :: J.Value)
  , "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"

parseVarName :: J.Value -> J.Parser SAT.Var
parseVarName = J.withText "variable name" parseVarNameText

parseVarNameText :: T.Text -> J.Parser SAT.Var
parseVarNameText name =
  case T.uncons name of
    Just ('x', rest) | (x,[]) : _ <- reads (T.unpack rest) -> pure x
    _ -> fail ("failed to parse variable name: " ++ show name)

jNot :: J.Value -> J.Value
jNot x = J.object
  [ "type" .= ("operator" :: J.Value)
  , "name" .= ("not" :: J.Value)
  , "operands" .= [x]
  ]

jLit :: SAT.Lit -> J.Value
jLit l
  | l > 0 = jVar l
  | otherwise = jNot $ jVar (- l)

parseLit :: J.Value -> J.Parser SAT.Lit
parseLit x = parseVar x <|> withNot (fmap negate . parseVar) x

parseLitName :: J.Value -> J.Parser SAT.Lit
parseLitName = J.withText "literal" parseLitNameText

parseLitNameText :: T.Text -> J.Parser SAT.Lit
parseLitNameText name =
  case T.uncons name of
    Just ('~', rest) -> negate <$> parseVarNameText rest
    _ -> parseVarNameText name

jConst :: J.ToJSON a => a -> J.Value
jConst x = J.object ["type" .= ("constant" :: J.Value), "value" .= x]

parseConst :: J.FromJSON a => J.Value -> J.Parser a
parseConst = withTypedObject "constant" $ \obj -> obj .: "value"

jPBSum :: SAT.PBSum -> J.Value
jPBSum s = J.object
  [ "type" .= ("operator" :: J.Value)
  , "name" .= ("+" :: J.Value)
  , "operands" .=
      [ J.object
          [ "type" .= ("operator" :: J.Value)
          , "name" .= ("*" :: J.Value)
          , "operands" .= (jConst c : [jLit lit | lit <- lits])
          ]
      | (c, lits) <- s
      ]
  ]

parsePBSum :: J.Value -> J.Parser SAT.PBSum
parsePBSum x = msum
  [ withOperator "+" (fmap concat . mapM parsePBSum) x
  , f x >>= \term -> pure [term]
  ]
  where
    f :: J.Value -> J.Parser (Integer, [SAT.Lit])
    f y = msum
      [ parseConst y >>= \c -> pure (c, [])
      , parseLit y >>= \lit -> pure (1, [lit])
      , withOperator "*" (fmap ((product *** concat) . unzip) . mapM f) y
      ]

jPBLinSum :: SAT.PBLinSum -> J.Value
jPBLinSum s = jPBSum [(c, [l]) | (c,l) <- s]

parsePBLinSum :: J.Value -> J.Parser SAT.PBLinSum
parsePBLinSum x = do
  s <- parsePBSum x
  forM s $ \(c, ls) ->
    case ls of
      [l] -> pure (c, l)
      _ -> fail "non-linear expression (linear expression expected)"

jPBConstraint :: PBFile.Constraint -> J.Value
jPBConstraint (lhs, op, rhs) =
  J.object
  [ "type" .= ("operator" :: J.Value)
  , "name" .= (case op of{ PBFile.Ge -> ">="; PBFile.Eq -> "=" } :: J.Value)
  , "operands" .= [jPBSum lhs, jConst rhs]
  ]

parsePBConstraint :: J.Value -> J.Parser PBFile.Constraint
parsePBConstraint x = msum
  [ withOperator ">=" (f PBFile.Ge ">=") x
  , withOperator "=" (f PBFile.Eq "=") x
  ]
  where
    f :: PBFile.Op -> String -> [J.Value] -> J.Parser PBFile.Constraint
    f op _opStr [lhs, rhs] = do
      lhs' <- parsePBSum lhs
      rhs' <- parseConst rhs
      pure (lhs', op, rhs')
    f _ opStr operands = fail ("wrong number of arguments for " ++ show opStr ++ " (given " ++ show (length operands) ++ ", expected 1)")


withOperator :: String -> ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
withOperator name k = withTypedObject "operator" $ \obj -> do
  op <- obj .: "name"
  unless (name == op) $ fail ("expected operator name " ++ show name ++ ", but found type " ++ show op)
  operands <- obj .: "operands"
  k operands

withNot :: (J.Value -> J.Parser a) -> J.Value -> J.Parser a
withNot k = withOperator "not" $ \operands -> do
  case operands of
    [x] -> k x
    _ -> fail ("wrong number of arguments for \"not\" (given " ++ show (length operands) ++ ", expected 1)")

withAnd :: ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
withAnd = withOperator "and"

withOr :: ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
withOr = withOperator "or"

withITE :: (J.Value -> J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
withITE k = withOperator "ite" $ \operands -> do
  case operands of
    [c, t, e] -> k c t e
    _ -> fail ("wrong number of arguments for \"ite\" (given " ++ show (length operands) ++ ", expected 3)")

withImply :: (J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
withImply k = withOperator "=>" $ \operands -> do
  case operands of
    [a, b] -> k a b
    _ -> fail ("wrong number of arguments for \"=>\" (given " ++ show (length operands) ++ ", expected 2)")

withEquiv :: (J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
withEquiv k = withOperator "<=>" $ \operands -> do
  case operands of
    [a, b] -> k a b
    _ -> fail ("wrong number of arguments for \"<=>\" (given " ++ show (length operands) ++ ", expected 2)")

1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE OverloadedStrings #-}
4	{-# LANGUAGE ScopedTypeVariables #-}
5	module ToySolver.SAT.Internal.JSON where
6
7	import Control.Applicative
8	import Control.Arrow ((***))
9	import Control.Monad
10	import qualified Data.Aeson as J
11	import qualified Data.Aeson.Types as J
12	import Data.Aeson ((.=), (.:))
13	import Data.String
14	import qualified Data.Text as T
15
16	import qualified Data.PseudoBoolean as PBFile
17	import ToySolver.Internal.JSON
18	import qualified ToySolver.SAT.Types as SAT
19
20	jVar :: SAT.Var -> J.Value
21	jVar v = J.object	1✔
22	[ "type" .= ("variable" :: J.Value)	1✔
23	, "name" .= (jVarName v :: J.Value)	1✔
24	]
25
26	jVarName :: IsString a => SAT.Var -> a
27	jVarName v = fromString ("x" ++ show v)	1✔
28
29	jLitName :: IsString a => SAT.Var -> a
30	jLitName v	1✔
31	\| v >= 0 = jVarName v	1✔
32	\| otherwise = fromString ("~x" ++ show (- v))	×
33
34	parseVar :: J.Value -> J.Parser SAT.Var
35	parseVar = withTypedObject "variable" $ \obj -> parseVarName =<< obj .: "name"	1✔
36
37	parseVarName :: J.Value -> J.Parser SAT.Var
38	parseVarName = J.withText "variable name" parseVarNameText	×
39
40	parseVarNameText :: T.Text -> J.Parser SAT.Var
41	parseVarNameText name =	1✔
42	case T.uncons name of	1✔
43	Just ('x', rest) \| (x,[]) : _ <- reads (T.unpack rest) -> pure x	1✔
44	_ -> fail ("failed to parse variable name: " ++ show name)	×
45
46	jNot :: J.Value -> J.Value
47	jNot x = J.object	1✔
48	[ "type" .= ("operator" :: J.Value)	1✔
49	, "name" .= ("not" :: J.Value)	1✔
50	, "operands" .= [x]	1✔
51	]
52
53	jLit :: SAT.Lit -> J.Value
54	jLit l	1✔
55	\| l > 0 = jVar l	1✔
56	\| otherwise = jNot $ jVar (- l)	×
57
58	parseLit :: J.Value -> J.Parser SAT.Lit
59	parseLit x = parseVar x <\|> withNot (fmap negate . parseVar) x	1✔
60
61	parseLitName :: J.Value -> J.Parser SAT.Lit
62	parseLitName = J.withText "literal" parseLitNameText	×
63
64	parseLitNameText :: T.Text -> J.Parser SAT.Lit
65	parseLitNameText name =	1✔
66	case T.uncons name of	1✔
67	Just ('~', rest) -> negate <$> parseVarNameText rest	1✔
68	_ -> parseVarNameText name	1✔
69
70	jConst :: J.ToJSON a => a -> J.Value
71	jConst x = J.object ["type" .= ("constant" :: J.Value), "value" .= x]	1✔
72
73	parseConst :: J.FromJSON a => J.Value -> J.Parser a
74	parseConst = withTypedObject "constant" $ \obj -> obj .: "value"	1✔
75
76	jPBSum :: SAT.PBSum -> J.Value
77	jPBSum s = J.object	1✔
78	[ "type" .= ("operator" :: J.Value)	1✔
79	, "name" .= ("+" :: J.Value)	1✔
80	, "operands" .=	1✔
81	[ J.object	1✔
82	[ "type" .= ("operator" :: J.Value)	1✔
83	, "name" .= ("*" :: J.Value)	1✔
84	, "operands" .= (jConst c : [jLit lit \| lit <- lits])	1✔
85	]
86	\| (c, lits) <- s	1✔
87	]
88	]
89
90	parsePBSum :: J.Value -> J.Parser SAT.PBSum
91	parsePBSum x = msum	1✔
92	[ withOperator "+" (fmap concat . mapM parsePBSum) x	1✔
93	, f x >>= \term -> pure [term]	1✔
94	]
95	where
96	f :: J.Value -> J.Parser (Integer, [SAT.Lit])
97	f y = msum	1✔
98	[ parseConst y >>= \c -> pure (c, [])	1✔
99	, parseLit y >>= \lit -> pure (1, [lit])	1✔
100	, withOperator "" (fmap ((product ** concat) . unzip) . mapM f) y	1✔
101	]
102
103	jPBLinSum :: SAT.PBLinSum -> J.Value
104	jPBLinSum s = jPBSum [(c, [l]) \| (c,l) <- s]	1✔
105
106	parsePBLinSum :: J.Value -> J.Parser SAT.PBLinSum
107	parsePBLinSum x = do	1✔
108	s <- parsePBSum x	1✔
109	forM s $ \(c, ls) ->	1✔
110	case ls of	1✔
111	[l] -> pure (c, l)	1✔
112	_ -> fail "non-linear expression (linear expression expected)"	×
113
114	jPBConstraint :: PBFile.Constraint -> J.Value
115	jPBConstraint (lhs, op, rhs) =	1✔
116	J.object	1✔
117	[ "type" .= ("operator" :: J.Value)	1✔
118	, "name" .= (case op of{ PBFile.Ge -> ">="; PBFile.Eq -> "=" } :: J.Value)	1✔
119	, "operands" .= [jPBSum lhs, jConst rhs]	1✔
120	]
121
122	parsePBConstraint :: J.Value -> J.Parser PBFile.Constraint
123	parsePBConstraint x = msum	1✔
124	[ withOperator ">=" (f PBFile.Ge ">=") x	×
125	, withOperator "=" (f PBFile.Eq "=") x	×
126	]
127	where
128	f :: PBFile.Op -> String -> [J.Value] -> J.Parser PBFile.Constraint
129	f op _opStr [lhs, rhs] = do	1✔
130	lhs' <- parsePBSum lhs	1✔
131	rhs' <- parseConst rhs	1✔
132	pure (lhs', op, rhs')	1✔
133	f _ opStr operands = fail ("wrong number of arguments for " ++ show opStr ++ " (given " ++ show (length operands) ++ ", expected 1)")	×
134
135
136	withOperator :: String -> ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
137	withOperator name k = withTypedObject "operator" $ \obj -> do	1✔
138	op <- obj .: "name"	1✔
139	unless (name == op) $ fail ("expected operator name " ++ show name ++ ", but found type " ++ show op)	×
140	operands <- obj .: "operands"	1✔
141	k operands	1✔
142
143	withNot :: (J.Value -> J.Parser a) -> J.Value -> J.Parser a
144	withNot k = withOperator "not" $ \operands -> do	1✔
145	case operands of	1✔
146	[x] -> k x	1✔
147	_ -> fail ("wrong number of arguments for \"not\" (given " ++ show (length operands) ++ ", expected 1)")	×
148
149	withAnd :: ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
150	withAnd = withOperator "and"	1✔
151
152	withOr :: ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
153	withOr = withOperator "or"	1✔
154
155	withITE :: (J.Value -> J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
156	withITE k = withOperator "ite" $ \operands -> do	×
157	case operands of	×
158	[c, t, e] -> k c t e	×
159	_ -> fail ("wrong number of arguments for \"ite\" (given " ++ show (length operands) ++ ", expected 3)")	×
160
161	withImply :: (J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
162	withImply k = withOperator "=>" $ \operands -> do	×
163	case operands of	×
164	[a, b] -> k a b	×
165	_ -> fail ("wrong number of arguments for \"=>\" (given " ++ show (length operands) ++ ", expected 2)")	×
166
167	withEquiv :: (J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
168	withEquiv k = withOperator "<=>" $ \operands -> do	×
169	case operands of	×
170	[a, b] -> k a b	×
171	_ -> fail ("wrong number of arguments for \"<=>\" (given " ++ show (length operands) ++ ", expected 2)")	×

msakai / toysolver / 660

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous