msakai / toysolver / 527

Committed 30 Nov 2024 02:35PM UTC coverage: 69.316% (-0.7%) from 70.001%

Build # 527

Build Type

push

github

Committed by

web-flow

Commit Message

Merge f09df53e8 into 79456f7ed

Run Details

221 of 368 new or added lines in 13 files covered. (60.05%)

136 existing lines in 16 files now uncovered.

10003 of 14431 relevant lines covered (69.32%)

0.69 hits per line

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

72.37

/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.Vector as V

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" .= J.String "variable"
  , "name" .= (fromString ("x" <> show v) :: J.Value)
  ]

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" .= 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)

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" .= J.String "constant", "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" .= J.String "operator"
  , "name" .= J.String "+"
  , "operands" .=
      [ J.object
          [ "type" .= J.String "operator"
          , "name" .= J.String "*"
          , "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
      ]

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

msakai / toysolver / 527

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