msakai / toysolver / 513

Committed 24 Nov 2024 08:49AM UTC coverage: 68.675% (-1.0%) from 69.681%

Build # 513

Build Type

push

github

Committed by

web-flow

Commit Message

Merge 496ed4263 into 46e1509c4

Run Details

5 of 121 new or added lines in 7 files covered. (4.13%)

105 existing lines in 14 files now uncovered.

9745 of 14190 relevant lines covered (68.68%)

0.69 hits per line

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

57.02

/src/ToySolver/SAT/Formula.hs

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Formula
-- Copyright   :  (c) Masahiro Sakai 2012-2021
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Formula
  (
  -- * Boolean formula type
    Formula (Atom, And, Or, Not, Equiv, Imply, ITE)
  , fold
  , evalFormula
  , simplify
  ) where

import Control.Monad.ST
import qualified Data.Aeson as J
import Data.Aeson ((.=))
import Data.Hashable
import qualified Data.HashTable.Class as H
import qualified Data.HashTable.ST.Cuckoo as C
import Data.Interned
import qualified Data.Vector as V
import GHC.Generics
import ToySolver.Data.Boolean
import qualified ToySolver.Data.BoolExpr as BoolExpr
import qualified ToySolver.SAT.Types as SAT
import ToySolver.SAT.Internal.JSON

-- Should this module be merged into ToySolver.SAT.Types module?

-- ------------------------------------------------------------------------

-- | Arbitrary formula not restricted to CNF
data Formula = Formula {-# UNPACK #-} !Id UFormula

instance Eq Formula where
  Formula i _ == Formula j _ = i == j

instance Show Formula where
  showsPrec d x = showsPrec d (toBoolExpr x)

instance Read Formula where
  readsPrec d s = [(fromBoolExpr b, rest) | (b, rest) <- readsPrec d s]

instance Hashable Formula where
  hashWithSalt s (Formula i _) = hashWithSalt s i

data UFormula
  = UAtom SAT.Lit
  | UAnd [Formula]
  | UOr [Formula]
  | UNot Formula
  | UImply Formula Formula
  | UEquiv Formula Formula
  | UITE Formula Formula Formula

instance Interned Formula where
  type Uninterned Formula = UFormula
  data Description Formula
    = DAtom SAT.Lit
    | DAnd [Id]
    | DOr [Id]
    | DNot Id
    | DImply Id Id
    | DEquiv Id Id
    | DITE Id Id Id
    deriving (Eq, Generic)
  describe (UAtom a) = DAtom a
  describe (UAnd xs) = DAnd [i | Formula i _ <- xs]
  describe (UOr xs) = DOr [i | Formula i _ <- xs]
  describe (UNot (Formula i _)) = DNot i
  describe (UImply (Formula i _) (Formula j _)) = DImply i j
  describe (UEquiv (Formula i _) (Formula j _)) = DEquiv i j
  describe (UITE (Formula i _) (Formula j _) (Formula k _)) = DITE i j k
  identify = Formula
  cache = formulaCache

instance Hashable (Description Formula)

instance Uninternable Formula where
  unintern (Formula _ uformula) = uformula

formulaCache :: Cache Formula
formulaCache = mkCache
{-# NOINLINE formulaCache #-}

-- ------------------------------------------------------------------------

pattern Atom :: SAT.Lit -> Formula
pattern Atom l <- (unintern -> UAtom l) where
  Atom l = intern (UAtom l)

pattern Not :: Formula -> Formula
pattern Not p <- (unintern -> UNot p) where
  Not p = intern (UNot p)

pattern And :: [Formula] -> Formula
pattern And ps <- (unintern -> UAnd ps) where
  And ps = intern (UAnd ps)

pattern Or :: [Formula] -> Formula
pattern Or ps <- (unintern -> UOr ps) where
  Or ps = intern (UOr ps)

pattern Equiv :: Formula -> Formula -> Formula
pattern Equiv p q <- (unintern -> UEquiv p q) where
  Equiv p q = intern (UEquiv p q)

pattern Imply :: Formula -> Formula -> Formula
pattern Imply p q <- (unintern -> UImply p q) where
  Imply p q = intern (UImply p q)

pattern ITE :: Formula -> Formula -> Formula -> Formula
pattern ITE p q r <- (unintern -> UITE p q r) where
  ITE p q r = intern (UITE p q r)

{-# COMPLETE Atom, Not, And, Or, Equiv, Imply, ITE #-}

-- ------------------------------------------------------------------------

instance Complement Formula where
  notB = intern . UNot

instance MonotoneBoolean Formula where
  andB = intern . UAnd
  orB  = intern . UOr

instance IfThenElse Formula Formula where
  ite c t e = intern (UITE c t e)

instance Boolean Formula where
  (.=>.) p q = intern (UImply p q)
  (.<=>.) p q = intern (UEquiv p q)

-- ------------------------------------------------------------------------

fold :: Boolean b => (SAT.Lit -> b) -> Formula -> b
fold f formula = runST $ do
  h <- C.newSized 256
  let g x = do
        m <- H.lookup h x
        case m of
          Just y -> return y
          Nothing -> do
            y <-
              case x of
                Atom lit -> return (f lit)
                And ps -> andB <$> mapM g ps
                Or ps -> orB <$> mapM g ps
                Not p -> notB <$> g p
                Imply p q -> (.=>.) <$> g p <*> g q
                Equiv p q -> (.<=>.) <$> g p <*> g q
                ITE p q r -> ite <$> g p <*> g q <*> g r
            H.insert h x y
            return y
  g formula

evalFormula :: SAT.IModel m => m -> Formula -> Bool
evalFormula m = fold (SAT.evalLit m)

toBoolExpr :: Formula -> BoolExpr.BoolExpr SAT.Lit
toBoolExpr = fold BoolExpr.Atom

fromBoolExpr :: BoolExpr.BoolExpr SAT.Lit -> Formula
fromBoolExpr = BoolExpr.fold Atom

-- ------------------------------------------------------------------------

simplify :: Formula -> Formula
simplify = runSimplify . fold (Simplify . Atom)

newtype Simplify = Simplify{ runSimplify :: Formula }

instance Complement Simplify where
  notB (Simplify (Not x)) = Simplify x
  notB (Simplify x) = Simplify (Not x)

instance MonotoneBoolean (Simplify) where
  orB xs
    | any isTrue ys = Simplify true
    | otherwise = Simplify $ Or ys
    where
      ys = concat [f x | Simplify x <- xs]
      f (Or zs) = zs
      f z = [z]
  andB xs
    | any isFalse ys = Simplify false
    | otherwise = Simplify $ And ys
    where
      ys = concat [f x | Simplify x <- xs]
      f (And zs) = zs
      f z = [z]

instance IfThenElse Simplify Simplify where
  ite (Simplify c) (Simplify t) (Simplify e)
    | isTrue c  = Simplify t
    | isFalse c = Simplify e
    | otherwise = Simplify (ITE c t e)

instance Boolean Simplify where
  Simplify x .=>. Simplify y
    | isFalse x = true
    | isTrue y  = true
    | isTrue x  = Simplify y
    | isFalse y = notB (Simplify x)
    | otherwise = Simplify (x .=>. y)

isTrue :: Formula -> Bool
isTrue (And []) = True
isTrue _ = False

isFalse :: Formula -> Bool
isFalse (Or []) = True
isFalse _ = False

-- ------------------------------------------------------------------------

newtype JSON = JSON{ getJSON :: J.Value }

instance Complement JSON where
  notB (JSON x) = JSON $ jNot x

instance MonotoneBoolean JSON where
  andB xs = JSON $ J.object
    [ "type" .= J.String "operator"
    , "name" .= J.String "and"
    , "operands" .= J.Array (V.fromList [x | JSON x <- xs])
    ]
  orB xs = JSON $ J.object
    [ "type" .= J.String "operator"
    , "name" .= J.String "or"
    , "operands" .= J.Array (V.fromList [x | JSON x <- xs])
    ]

instance IfThenElse JSON JSON where
  ite (JSON c) (JSON t) (JSON e) = JSON $ J.object
    [ "type" .= J.String "operator"
    , "name" .= J.String "ite"
    , "operands" .= J.Array (V.fromList [c, t, e])
    ]

instance Boolean JSON where
  (.=>.) (JSON p) (JSON q) = JSON $ J.object
    [ "type" .= J.String "operator"
    , "name" .= J.String "=>"
    , "operands" .= J.Array (V.fromList [p, q])
    ]
  (.<=>.) (JSON p) (JSON q) = JSON $ J.object
    [ "type" .= J.String "operator"
    , "name" .= J.String "<=>"
    , "operands" .= J.Array (V.fromList [p, q])
    ]

instance J.ToJSON Formula where
  toJSON = getJSON . fold (JSON . jLit)

-- ------------------------------------------------------------------------

1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE DeriveGeneric #-}
4	{-# LANGUAGE FlexibleInstances #-}
5	{-# LANGUAGE MultiParamTypeClasses #-}
6	{-# LANGUAGE OverloadedStrings #-}
7	{-# LANGUAGE PatternSynonyms #-}
8	{-# LANGUAGE TypeFamilies #-}
9	{-# LANGUAGE ViewPatterns #-}
10	-----------------------------------------------------------------------------
11	-- \|
12	-- Module : ToySolver.SAT.Formula
13	-- Copyright : (c) Masahiro Sakai 2012-2021
14	-- License : BSD-style
15	--
16	-- Maintainer : masahiro.sakai@gmail.com
17	-- Stability : provisional
18	-- Portability : non-portable
19	--
20	-----------------------------------------------------------------------------
21	module ToySolver.SAT.Formula
22	(
23	-- * Boolean formula type
24	Formula (Atom, And, Or, Not, Equiv, Imply, ITE)
25	, fold
26	, evalFormula
27	, simplify
28	) where
29
30	import Control.Monad.ST
31	import qualified Data.Aeson as J
32	import Data.Aeson ((.=))
33	import Data.Hashable
34	import qualified Data.HashTable.Class as H
35	import qualified Data.HashTable.ST.Cuckoo as C
36	import Data.Interned
37	import qualified Data.Vector as V
38	import GHC.Generics
39	import ToySolver.Data.Boolean
40	import qualified ToySolver.Data.BoolExpr as BoolExpr
41	import qualified ToySolver.SAT.Types as SAT
42	import ToySolver.SAT.Internal.JSON
43
44	-- Should this module be merged into ToySolver.SAT.Types module?
45
46	-- ------------------------------------------------------------------------
47
48	-- \| Arbitrary formula not restricted to CNF
49	data Formula = Formula {-# UNPACK #-} !Id UFormula
50
51	instance Eq Formula where	×
52	Formula i _ == Formula j _ = i == j	1✔
53
54	instance Show Formula where	×
55	showsPrec d x = showsPrec d (toBoolExpr x)	×
56
57	instance Read Formula where	×
58	readsPrec d s = [(fromBoolExpr b, rest) \| (b, rest) <- readsPrec d s]	×
59
60	instance Hashable Formula where	1✔
61	hashWithSalt s (Formula i _) = hashWithSalt s i	1✔
62
63	data UFormula
64	= UAtom SAT.Lit
65	\| UAnd [Formula]
66	\| UOr [Formula]
67	\| UNot Formula
68	\| UImply Formula Formula
69	\| UEquiv Formula Formula
70	\| UITE Formula Formula Formula
71
72	instance Interned Formula where	1✔
73	type Uninterned Formula = UFormula
74	data Description Formula
75	= DAtom SAT.Lit
76	\| DAnd [Id]
77	\| DOr [Id]
78	\| DNot Id
79	\| DImply Id Id
80	\| DEquiv Id Id
81	\| DITE Id Id Id
82	deriving (Eq, Generic)	×
83	describe (UAtom a) = DAtom a	1✔
84	describe (UAnd xs) = DAnd [i \| Formula i _ <- xs]	1✔
85	describe (UOr xs) = DOr [i \| Formula i _ <- xs]	1✔
86	describe (UNot (Formula i _)) = DNot i	1✔
87	describe (UImply (Formula i _) (Formula j _)) = DImply i j	1✔
88	describe (UEquiv (Formula i _) (Formula j _)) = DEquiv i j	1✔
89	describe (UITE (Formula i _) (Formula j _) (Formula k _)) = DITE i j k	1✔
90	identify = Formula	1✔
91	cache = formulaCache	1✔
92
93	instance Hashable (Description Formula)	1✔
94
95	instance Uninternable Formula where
96	unintern (Formula _ uformula) = uformula	1✔
97
98	formulaCache :: Cache Formula
99	formulaCache = mkCache	1✔
100	{-# NOINLINE formulaCache #-}
101
102	-- ------------------------------------------------------------------------
103
104	pattern Atom :: SAT.Lit -> Formula
105	pattern Atom l <- (unintern -> UAtom l) where	1✔
106	Atom l = intern (UAtom l)	1✔
107
108	pattern Not :: Formula -> Formula
109	pattern Not p <- (unintern -> UNot p) where	1✔
110	Not p = intern (UNot p)	1✔
111
112	pattern And :: [Formula] -> Formula
113	pattern And ps <- (unintern -> UAnd ps) where	1✔
114	And ps = intern (UAnd ps)	1✔
115
116	pattern Or :: [Formula] -> Formula
117	pattern Or ps <- (unintern -> UOr ps) where	1✔
118	Or ps = intern (UOr ps)	1✔
119
120	pattern Equiv :: Formula -> Formula -> Formula
121	pattern Equiv p q <- (unintern -> UEquiv p q) where	1✔
122	Equiv p q = intern (UEquiv p q)	1✔
123
124	pattern Imply :: Formula -> Formula -> Formula
125	pattern Imply p q <- (unintern -> UImply p q) where	1✔
126	Imply p q = intern (UImply p q)	×
127
128	pattern ITE :: Formula -> Formula -> Formula -> Formula
129	pattern ITE p q r <- (unintern -> UITE p q r) where	1✔
130	ITE p q r = intern (UITE p q r)	×
131
132	{-# COMPLETE Atom, Not, And, Or, Equiv, Imply, ITE #-}
133
134	-- ------------------------------------------------------------------------
135
136	instance Complement Formula where
137	notB = intern . UNot	1✔
138
139	instance MonotoneBoolean Formula where	1✔
140	andB = intern . UAnd	1✔
141	orB = intern . UOr	1✔
142
143	instance IfThenElse Formula Formula where
144	ite c t e = intern (UITE c t e)	1✔
145
146	instance Boolean Formula where
147	(.=>.) p q = intern (UImply p q)	1✔
148	(.<=>.) p q = intern (UEquiv p q)	1✔
149
150	-- ------------------------------------------------------------------------
151
152	fold :: Boolean b => (SAT.Lit -> b) -> Formula -> b
153	fold f formula = runST $ do	1✔
154	h <- C.newSized 256	1✔
155	let g x = do	1✔
156	m <- H.lookup h x	1✔
157	case m of	1✔
158	Just y -> return y	1✔
159	Nothing -> do	1✔
160	y <-
161	case x of	1✔
162	Atom lit -> return (f lit)	1✔
163	And ps -> andB <$> mapM g ps	1✔
164	Or ps -> orB <$> mapM g ps	1✔
165	Not p -> notB <$> g p	1✔
166	Imply p q -> (.=>.) <$> g p <*> g q	1✔
167	Equiv p q -> (.<=>.) <$> g p <*> g q	×
168	ITE p q r -> ite <$> g p <> g q <> g r	×
169	H.insert h x y	1✔
170	return y	1✔
171	g formula	1✔
172
173	evalFormula :: SAT.IModel m => m -> Formula -> Bool
174	evalFormula m = fold (SAT.evalLit m)	1✔
175
176	toBoolExpr :: Formula -> BoolExpr.BoolExpr SAT.Lit
177	toBoolExpr = fold BoolExpr.Atom	×
178
179	fromBoolExpr :: BoolExpr.BoolExpr SAT.Lit -> Formula
180	fromBoolExpr = BoolExpr.fold Atom	×
181
182	-- ------------------------------------------------------------------------
183
184	simplify :: Formula -> Formula
185	simplify = runSimplify . fold (Simplify . Atom)	1✔
186
187	newtype Simplify = Simplify{ runSimplify :: Formula }	1✔
188
189	instance Complement Simplify where
190	notB (Simplify (Not x)) = Simplify x	×
191	notB (Simplify x) = Simplify (Not x)	1✔
192
193	instance MonotoneBoolean (Simplify) where	×
194	orB xs	1✔
195	\| any isTrue ys = Simplify true	1✔
196	\| otherwise = Simplify $ Or ys	×
197	where
198	ys = concat [f x \| Simplify x <- xs]	1✔
199	f (Or zs) = zs	1✔
200	f z = [z]	1✔
201	andB xs	1✔
202	\| any isFalse ys = Simplify false	1✔
203	\| otherwise = Simplify $ And ys	×
204	where
205	ys = concat [f x \| Simplify x <- xs]	1✔
206	f (And zs) = zs	1✔
207	f z = [z]	1✔
208
209	instance IfThenElse Simplify Simplify where
210	ite (Simplify c) (Simplify t) (Simplify e)	×
211	\| isTrue c = Simplify t	×
212	\| isFalse c = Simplify e	×
213	\| otherwise = Simplify (ITE c t e)	×
214
215	instance Boolean Simplify where	×
216	Simplify x .=>. Simplify y	×
217	\| isFalse x = true	×
218	\| isTrue y = true	×
219	\| isTrue x = Simplify y	×
220	\| isFalse y = notB (Simplify x)	×
221	\| otherwise = Simplify (x .=>. y)	×
222
223	isTrue :: Formula -> Bool
224	isTrue (And []) = True	1✔
225	isTrue _ = False	1✔
226
227	isFalse :: Formula -> Bool
228	isFalse (Or []) = True	1✔
229	isFalse _ = False	1✔
230
231	-- ------------------------------------------------------------------------
232
NEW 233	newtype JSON = JSON{ getJSON :: J.Value }	×
234
235	instance Complement JSON where
NEW 236	notB (JSON x) = JSON $ jNot x	×
237
NEW 238	instance MonotoneBoolean JSON where	×
NEW 239	andB xs = JSON $ J.object	×
NEW 240	[ "type" .= J.String "operator"	×
NEW 241	, "name" .= J.String "and"	×
NEW 242	, "operands" .= J.Array (V.fromList [x \| JSON x <- xs])	×
243	]
NEW 244	orB xs = JSON $ J.object	×
NEW 245	[ "type" .= J.String "operator"	×
NEW 246	, "name" .= J.String "or"	×
NEW 247	, "operands" .= J.Array (V.fromList [x \| JSON x <- xs])	×
248	]
249
250	instance IfThenElse JSON JSON where
NEW 251	ite (JSON c) (JSON t) (JSON e) = JSON $ J.object	×
NEW 252	[ "type" .= J.String "operator"	×
NEW 253	, "name" .= J.String "ite"	×
NEW 254	, "operands" .= J.Array (V.fromList [c, t, e])	×
255	]
256
257	instance Boolean JSON where
NEW 258	(.=>.) (JSON p) (JSON q) = JSON $ J.object	×
NEW 259	[ "type" .= J.String "operator"	×
NEW 260	, "name" .= J.String "=>"	×
NEW 261	, "operands" .= J.Array (V.fromList [p, q])	×
262	]
NEW 263	(.<=>.) (JSON p) (JSON q) = JSON $ J.object	×
NEW 264	[ "type" .= J.String "operator"	×
NEW 265	, "name" .= J.String "<=>"	×
NEW 266	, "operands" .= J.Array (V.fromList [p, q])	×
267	]
268
NEW 269	instance J.ToJSON Formula where	×
NEW 270	toJSON = getJSON . fold (JSON . jLit)	×
271
272	-- ------------------------------------------------------------------------

msakai / toysolver / 513

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