msakai / toysolver / 524

Committed 27 Nov 2024 03:47PM UTC coverage: 69.32% (-0.7%) from 70.001%

Build # 524

Build Type

push

github

Committed by

web-flow

Commit Message

Merge 7b4eae581 into 79456f7ed

Run Details

48 of 336 new or added lines in 11 files covered. (14.29%)

68 existing lines in 10 files now uncovered.

9989 of 14410 relevant lines covered (69.32%)

0.69 hits per line

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

9.21

/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 <|> parseLit 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 = asum
  [ withOperator "+" (fmap concat . mapM parsePBSum) x
  , f x >>= \term -> pure [term]
  ]
  where
    f :: J.Value -> J.Parser (Integer, [SAT.Lit])
    f y = asum
      [ 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 = asum
  [ 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' <- J.parseJSON lhs
      rhs' <- J.parseJSON 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
NEW 22	jVar v = J.object	×
NEW 23	[ "type" .= J.String "variable"	×
NEW 24	, "name" .= (fromString ("x" <> show v) :: J.Value)	×
25	]
26
27	parseVar :: J.Value -> J.Parser SAT.Var
NEW 28	parseVar = withTypedObject "variable" $ \obj -> parseVarName =<< obj .: "name"	×
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
NEW 40	jNot x = J.object	×
NEW 41	[ "type" .= J.String "operator"	×
NEW 42	, "name" .= J.String "not"	×
NEW 43	, "operands" .= J.Array (V.singleton x)	×
44	]
45
46	jLit :: SAT.Lit -> J.Value
NEW 47	jLit l	×
NEW 48	\| l > 0 = jVar l	×
NEW 49	\| otherwise = jNot $ jVar (- l)	×
50
51	parseLit :: J.Value -> J.Parser SAT.Lit
NEW 52	parseLit x = parseVar x <\|> parseLit x	×
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
NEW 64	jConst x = J.object ["type" .= J.String "constant", "value" .= x]	×
65
66	parseConst :: J.FromJSON a => J.Value -> J.Parser a
NEW 67	parseConst = withTypedObject "constant" $ \obj -> obj .: "value"	×
68
69	jPBSum :: SAT.PBSum -> J.Value
NEW 70	jPBSum s = J.object	×
NEW 71	[ "type" .= J.String "operator"	×
NEW 72	, "name" .= J.String "+"	×
NEW 73	, "operands" .=	×
NEW 74	[ J.object	×
NEW 75	[ "type" .= J.String "operator"	×
NEW 76	, "name" .= J.String "*"	×
NEW 77	, "operands" .= (jConst c : [jLit lit \| lit <- lits])	×
78	]
NEW 79	\| (c, lits) <- s	×
80	]
81	]
82
83	parsePBSum :: J.Value -> J.Parser SAT.PBSum
NEW 84	parsePBSum x = asum	×
NEW 85	[ withOperator "+" (fmap concat . mapM parsePBSum) x	×
NEW 86	, f x >>= \term -> pure [term]	×
87	]
88	where
89	f :: J.Value -> J.Parser (Integer, [SAT.Lit])
NEW 90	f y = asum	×
NEW 91	[ parseConst y >>= \c -> pure (c, [])	×
NEW 92	, parseLit y >>= \lit -> pure (1, [lit])	×
NEW 93	, withOperator "" (fmap ((product ** concat) . unzip) . mapM f) y	×
94	]
95
96	jPBConstraint :: PBFile.Constraint -> J.Value
NEW 97	jPBConstraint (lhs, op, rhs) =	×
NEW 98	J.object	×
NEW 99	[ "type" .= J.String "operator"	×
NEW 100	, "name" .= J.String (case op of{ PBFile.Ge -> ">="; PBFile.Eq -> "=" })	×
NEW 101	, "operands" .= [jPBSum lhs, jConst rhs]	×
102	]
103
104	parsePBConstraint :: J.Value -> J.Parser PBFile.Constraint
NEW 105	parsePBConstraint x = asum	×
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
NEW 111	f op _opStr [lhs, rhs] = do	×
NEW 112	lhs' <- J.parseJSON lhs	×
NEW 113	rhs' <- J.parseJSON rhs	×
NEW 114	pure (lhs', op, rhs')	×
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
NEW 119	withOperator name k = withTypedObject "operator" $ \obj -> do	×
NEW 120	op <- obj .: "name"	×
NEW 121	unless (name == op) $ fail ("expected operator name " ++ show name ++ ", but found type " ++ show op)	×
NEW 122	operands <- obj .: "operands"	×
NEW 123	k operands	×
124
125	withNot :: (J.Value -> J.Parser a) -> J.Value -> J.Parser a
NEW 126	withNot k = withOperator "not" $ \operands -> do	×
NEW 127	case operands of	×
NEW 128	[x] -> k x	×
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
NEW 132	withAnd = withOperator "and"	×
133
134	withOr :: ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
NEW 135	withOr = withOperator "or"	×
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 / 524

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