msakai / toysolver / 544

Committed 05 Dec 2024 11:36AM UTC coverage: 69.382% (-0.4%) from 69.767%

Build # 544

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #129 from msakai/feature/naesat-json-special-var

Use text (instead of integer) to represent special variable in SAT2NAESATInfo's JSON encoding

Run Details

14 of 15 new or added lines in 4 files covered. (93.33%)

79 existing lines in 12 files now uncovered.

10066 of 14508 relevant lines covered (69.38%)

0.69 hits per line

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

72.5

/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
      ]

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✔
NEW 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	jPBConstraint :: PBFile.Constraint -> J.Value
104	jPBConstraint (lhs, op, rhs) =	1✔
105	J.object	1✔
106	[ "type" .= ("operator" :: J.Value)	1✔
107	, "name" .= (case op of{ PBFile.Ge -> ">="; PBFile.Eq -> "=" } :: J.Value)	1✔
108	, "operands" .= [jPBSum lhs, jConst rhs]	1✔
109	]
110
111	parsePBConstraint :: J.Value -> J.Parser PBFile.Constraint
112	parsePBConstraint x = msum	1✔
113	[ withOperator ">=" (f PBFile.Ge ">=") x	×
114	, withOperator "=" (f PBFile.Eq "=") x	×
115	]
116	where
117	f :: PBFile.Op -> String -> [J.Value] -> J.Parser PBFile.Constraint
118	f op _opStr [lhs, rhs] = do	1✔
119	lhs' <- parsePBSum lhs	1✔
120	rhs' <- parseConst rhs	1✔
121	pure (lhs', op, rhs')	1✔
122	f _ opStr operands = fail ("wrong number of arguments for " ++ show opStr ++ " (given " ++ show (length operands) ++ ", expected 1)")	×
123
124
125	withOperator :: String -> ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
126	withOperator name k = withTypedObject "operator" $ \obj -> do	1✔
127	op <- obj .: "name"	1✔
128	unless (name == op) $ fail ("expected operator name " ++ show name ++ ", but found type " ++ show op)	×
129	operands <- obj .: "operands"	1✔
130	k operands	1✔
131
132	withNot :: (J.Value -> J.Parser a) -> J.Value -> J.Parser a
133	withNot k = withOperator "not" $ \operands -> do	1✔
134	case operands of	1✔
135	[x] -> k x	1✔
136	_ -> fail ("wrong number of arguments for \"not\" (given " ++ show (length operands) ++ ", expected 1)")	×
137
138	withAnd :: ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
139	withAnd = withOperator "and"	1✔
140
141	withOr :: ([J.Value] -> J.Parser a) -> J.Value -> J.Parser a
142	withOr = withOperator "or"	1✔
143
144	withITE :: (J.Value -> J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
145	withITE k = withOperator "ite" $ \operands -> do	×
146	case operands of	×
147	[c, t, e] -> k c t e	×
148	_ -> fail ("wrong number of arguments for \"ite\" (given " ++ show (length operands) ++ ", expected 3)")	×
149
150	withImply :: (J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
151	withImply k = withOperator "=>" $ \operands -> do	×
152	case operands of	×
153	[a, b] -> k a b	×
154	_ -> fail ("wrong number of arguments for \"=>\" (given " ++ show (length operands) ++ ", expected 2)")	×
155
156	withEquiv :: (J.Value -> J.Value -> J.Parser a) -> J.Value -> J.Parser a
157	withEquiv k = withOperator "<=>" $ \operands -> do	×
158	case operands of	×
159	[a, b] -> k a b	×
160	_ -> fail ("wrong number of arguments for \"<=>\" (given " ++ show (length operands) ++ ", expected 2)")	×

msakai / toysolver / 544

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