msakai / toysolver / 520

Committed 25 Nov 2024 04:17PM UTC coverage: 68.129% (-1.6%) from 69.746%

Build # 520

Build Type

push

github

Committed by

web-flow

Commit Message

Merge 1c430fa95 into 38bf6d362

Run Details

0 of 328 new or added lines in 11 files covered. (0.0%)

70 existing lines in 12 files now uncovered.

9812 of 14402 relevant lines covered (68.13%)

0.68 hits per line

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

0.0

/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

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
NEW 34	parseVarNameText name =	×
NEW 35	case T.uncons name of	×
NEW 36	Just ('x', rest) \| (x,[]) : _ <- reads (T.unpack rest) -> pure x	×
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	jConst :: J.ToJSON a => a -> J.Value
NEW 55	jConst x = J.object ["type" .= J.String "constant", "value" .= x]	×
56
57	parseConst :: J.FromJSON a => J.Value -> J.Parser a
NEW 58	parseConst = withTypedObject "constant" $ \obj -> obj .: "value"	×
59
60	jPBSum :: SAT.PBSum -> J.Value
NEW 61	jPBSum s = J.object	×
NEW 62	[ "type" .= J.String "operator"	×
NEW 63	, "name" .= J.String "+"	×
NEW 64	, "operands" .=	×
NEW 65	[ J.object	×
NEW 66	[ "type" .= J.String "operator"	×
NEW 67	, "name" .= J.String "*"	×
NEW 68	, "operands" .= (jConst c : [jLit lit \| lit <- lits])	×
69	]
NEW 70	\| (c, lits) <- s	×
71	]
72	]
73
74	parsePBSum :: J.Value -> J.Parser SAT.PBSum
NEW 75	parsePBSum x = asum	×
NEW 76	[ withOperator "+" (fmap concat . mapM parsePBSum) x	×
NEW 77	, f x >>= \term -> pure [term]	×
78	]
79	where
80	f :: J.Value -> J.Parser (Integer, [SAT.Lit])
NEW 81	f y = asum	×
NEW 82	[ parseConst y >>= \c -> pure (c, [])	×
NEW 83	, parseLit y >>= \lit -> pure (1, [lit])	×
NEW 84	, withOperator "" (fmap ((product ** concat) . unzip) . mapM f) y	×
85	]
86
87	jPBConstraint :: PBFile.Constraint -> J.Value
NEW 88	jPBConstraint (lhs, op, rhs) =	×
NEW 89	J.object	×
NEW 90	[ "type" .= J.String "operator"	×
NEW 91	, "name" .= J.String (case op of{ PBFile.Ge -> ">="; PBFile.Eq -> "=" })	×
NEW 92	, "operands" .= [jPBSum lhs, jConst rhs]	×
93	]
94
95	parsePBConstraint :: J.Value -> J.Parser PBFile.Constraint
NEW 96	parsePBConstraint x = asum	×
NEW 97	[ withOperator ">=" (f PBFile.Ge ">=") x	×
NEW 98	, withOperator "=" (f PBFile.Eq "=") x	×
99	]
100	where
101	f :: PBFile.Op -> String -> [J.Value] -> J.Parser PBFile.Constraint
NEW 102	f op _opStr [lhs, rhs] = do	×
NEW 103	lhs' <- J.parseJSON lhs	×
NEW 104	rhs' <- J.parseJSON rhs	×
NEW 105	pure (lhs', op, rhs')	×
NEW 106	f _ opStr operands = fail ("wrong number of arguments for " ++ show opStr ++ " (given " ++ show (length operands) ++ ", expected 1)")	×
107
108
109	withOperator :: String -> ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
NEW 110	withOperator name k = withTypedObject "operator" $ \obj -> do	×
NEW 111	op <- obj .: "name"	×
NEW 112	unless (name == op) $ fail ("expected operator name " ++ show name ++ ", but found type " ++ show op)	×
NEW 113	operands <- obj .: "operands"	×
NEW 114	k operands	×
115
116	withNot :: (J.Value -> J.Parser a) -> J.Value -> J.Parser a
NEW 117	withNot k = withOperator "not" $ \operands -> do	×
NEW 118	case operands of	×
NEW 119	[x] -> k x	×
NEW 120	_ -> fail ("wrong number of arguments for \"not\" (given " ++ show (length operands) ++ ", expected 1)")	×
121
122	withAnd :: ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
NEW 123	withAnd = withOperator "and"	×
124
125	withOr :: ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
NEW 126	withOr = withOperator "or"	×
127
128	withITE :: (J.Value -> J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
NEW 129	withITE k = withOperator "ite" $ \operands -> do	×
NEW 130	case operands of	×
NEW 131	[c, t, e] -> k c t e	×
NEW 132	_ -> fail ("wrong number of arguments for \"ite\" (given " ++ show (length operands) ++ ", expected 3)")	×
133
134	withImply :: (J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
NEW 135	withImply k = withOperator "=>" $ \operands -> do	×
NEW 136	case operands of	×
NEW 137	[a, b] -> k a b	×
NEW 138	_ -> fail ("wrong number of arguments for \"=>\" (given " ++ show (length operands) ++ ", expected 2)")	×
139
140	withEquiv :: (J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
NEW 141	withEquiv k = withOperator "<=>" $ \operands -> do	×
NEW 142	case operands of	×
NEW 143	[a, b] -> k a b	×
NEW 144	_ -> fail ("wrong number of arguments for \"<=>\" (given " ++ show (length operands) ++ ", expected 2)")	×

msakai / toysolver / 520

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