{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# 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 Data.Hashable
import qualified Data.HashTable.Class as H
import qualified Data.HashTable.ST.Cuckoo as C
import Data.Interned
import GHC.Generics
import ToySolver.Data.Boolean
import qualified ToySolver.Data.BoolExpr as BoolExpr
import qualified ToySolver.SAT.Types as SAT

-- 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 Id
i UFormula
_ == :: Formula -> Formula -> Bool
== Formula Id
j UFormula
_ = Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
j

instance Show Formula where
  showsPrec :: Id -> Formula -> ShowS
showsPrec Id
d Formula
x = Id -> BoolExpr Id -> ShowS
forall a. Show a => Id -> a -> ShowS
showsPrec Id
d (Formula -> BoolExpr Id
toBoolExpr Formula
x)

instance Read Formula where
  readsPrec :: Id -> ReadS Formula
readsPrec Id
d String
s = [(BoolExpr Id -> Formula
fromBoolExpr BoolExpr Id
b, String
rest) | (BoolExpr Id
b, String
rest) <- Id -> ReadS (BoolExpr Id)
forall a. Read a => Id -> ReadS a
readsPrec Id
d String
s]

instance Hashable Formula where
  hashWithSalt :: Id -> Formula -> Id
hashWithSalt Id
s (Formula Id
i UFormula
_) = Id -> Id -> Id
forall a. Hashable a => Id -> a -> Id
hashWithSalt Id
s Id
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 (Description Formula -> Description Formula -> Bool
(Description Formula -> Description Formula -> Bool)
-> (Description Formula -> Description Formula -> Bool)
-> Eq (Description Formula)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Description Formula -> Description Formula -> Bool
$c/= :: Description Formula -> Description Formula -> Bool
== :: Description Formula -> Description Formula -> Bool
$c== :: Description Formula -> Description Formula -> Bool
Eq, (forall x. Description Formula -> Rep (Description Formula) x)
-> (forall x. Rep (Description Formula) x -> Description Formula)
-> Generic (Description Formula)
forall x. Rep (Description Formula) x -> Description Formula
forall x. Description Formula -> Rep (Description Formula) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep (Description Formula) x -> Description Formula
$cfrom :: forall x. Description Formula -> Rep (Description Formula) x
Generic)
  describe :: Uninterned Formula -> Description Formula
describe (UAtom a) = Id -> Description Formula
DAtom Id
a
  describe (UAnd xs) = [Id] -> Description Formula
DAnd [Id
i | Formula Id
i UFormula
_ <- [Formula]
xs]
  describe (UOr xs) = [Id] -> Description Formula
DOr [Id
i | Formula Id
i UFormula
_ <- [Formula]
xs]
  describe (UNot (Formula i _)) = Id -> Description Formula
DNot Id
i
  describe (UImply (Formula i _) (Formula j _)) = Id -> Id -> Description Formula
DImply Id
i Id
j
  describe (UEquiv (Formula i _) (Formula j _)) = Id -> Id -> Description Formula
DEquiv Id
i Id
j
  describe (UITE (Formula i _) (Formula j _) (Formula k _)) = Id -> Id -> Id -> Description Formula
DITE Id
i Id
j Id
k
  identify :: Id -> Uninterned Formula -> Formula
identify = Id -> Uninterned Formula -> Formula
Id -> UFormula -> Formula
Formula
  cache :: Cache Formula
cache = Cache Formula
formulaCache

instance Hashable (Description Formula)

instance Uninternable Formula where
  unintern :: Formula -> Uninterned Formula
unintern (Formula Id
_ UFormula
uformula) = Uninterned Formula
UFormula
uformula

formulaCache :: Cache Formula
formulaCache :: Cache Formula
formulaCache = Cache Formula
forall t. Interned t => Cache t
mkCache
{-# NOINLINE formulaCache #-}

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

pattern Atom :: SAT.Lit -> Formula
pattern $bAtom :: Id -> Formula
$mAtom :: forall r. Formula -> (Id -> r) -> (Void# -> r) -> r
Atom l <- (unintern -> UAtom l) where
  Atom Id
l = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Id -> UFormula
UAtom Id
l)

pattern Not :: Formula -> Formula
pattern $bNot :: Formula -> Formula
$mNot :: forall r. Formula -> (Formula -> r) -> (Void# -> r) -> r
Not p <- (unintern -> UNot p) where
  Not Formula
p = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> UFormula
UNot Formula
p)

pattern And :: [Formula] -> Formula
pattern $bAnd :: [Formula] -> Formula
$mAnd :: forall r. Formula -> ([Formula] -> r) -> (Void# -> r) -> r
And ps <- (unintern -> UAnd ps) where
  And [Formula]
ps = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern ([Formula] -> UFormula
UAnd [Formula]
ps)

pattern Or :: [Formula] -> Formula
pattern $bOr :: [Formula] -> Formula
$mOr :: forall r. Formula -> ([Formula] -> r) -> (Void# -> r) -> r
Or ps <- (unintern -> UOr ps) where
  Or [Formula]
ps = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern ([Formula] -> UFormula
UOr [Formula]
ps)

pattern Equiv :: Formula -> Formula -> Formula
pattern $bEquiv :: Formula -> Formula -> Formula
$mEquiv :: forall r. Formula -> (Formula -> Formula -> r) -> (Void# -> r) -> r
Equiv p q <- (unintern -> UEquiv p q) where
  Equiv Formula
p Formula
q = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> UFormula
UEquiv Formula
p Formula
q)

pattern Imply :: Formula -> Formula -> Formula
pattern $bImply :: Formula -> Formula -> Formula
$mImply :: forall r. Formula -> (Formula -> Formula -> r) -> (Void# -> r) -> r
Imply p q <- (unintern -> UImply p q) where
  Imply Formula
p Formula
q = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> UFormula
UImply Formula
p Formula
q)

pattern ITE :: Formula -> Formula -> Formula -> Formula
pattern $bITE :: Formula -> Formula -> Formula -> Formula
$mITE :: forall r.
Formula
-> (Formula -> Formula -> Formula -> r) -> (Void# -> r) -> r
ITE p q r <- (unintern -> UITE p q r) where
  ITE Formula
p Formula
q Formula
r = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> Formula -> UFormula
UITE Formula
p Formula
q Formula
r)

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

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

instance Complement Formula where
  notB :: Formula -> Formula
notB = UFormula -> Formula
forall t. Interned t => Uninterned t -> t
intern (UFormula -> Formula)
-> (Formula -> UFormula) -> Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> UFormula
UNot

instance MonotoneBoolean Formula where
  andB :: [Formula] -> Formula
andB = UFormula -> Formula
forall t. Interned t => Uninterned t -> t
intern (UFormula -> Formula)
-> ([Formula] -> UFormula) -> [Formula] -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Formula] -> UFormula
UAnd
  orB :: [Formula] -> Formula
orB  = UFormula -> Formula
forall t. Interned t => Uninterned t -> t
intern (UFormula -> Formula)
-> ([Formula] -> UFormula) -> [Formula] -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Formula] -> UFormula
UOr

instance IfThenElse Formula Formula where
  ite :: Formula -> Formula -> Formula -> Formula
ite Formula
c Formula
t Formula
e = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> Formula -> UFormula
UITE Formula
c Formula
t Formula
e)

instance Boolean Formula where
  .=>. :: Formula -> Formula -> Formula
(.=>.) Formula
p Formula
q = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> UFormula
UImply Formula
p Formula
q)
  .<=>. :: Formula -> Formula -> Formula
(.<=>.) Formula
p Formula
q = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> UFormula
UEquiv Formula
p Formula
q)

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

fold :: Boolean b => (SAT.Lit -> b) -> Formula -> b
fold :: (Id -> b) -> Formula -> b
fold Id -> b
f Formula
formula = (forall s. ST s b) -> b
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s b) -> b) -> (forall s. ST s b) -> b
forall a b. (a -> b) -> a -> b
$ do
  HashTable s Formula b
h <- Id -> ST s (HashTable s Formula b)
forall s k v. Id -> ST s (HashTable s k v)
C.newSized Id
256
  let g :: Formula -> ST s b
g Formula
x = do
        Maybe b
m <- HashTable s Formula b -> Formula -> ST s (Maybe b)
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s Formula b
h Formula
x
        case Maybe b
m of
          Just b
y -> b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
y
          Maybe b
Nothing -> do
            b
y <-
              case Formula
x of
                Atom Id
lit -> b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> b
f Id
lit)
                And [Formula]
ps -> [b] -> b
forall a. MonotoneBoolean a => [a] -> a
andB ([b] -> b) -> ST s [b] -> ST s b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Formula -> ST s b) -> [Formula] -> ST s [b]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Formula -> ST s b
g [Formula]
ps
                Or [Formula]
ps -> [b] -> b
forall a. MonotoneBoolean a => [a] -> a
orB ([b] -> b) -> ST s [b] -> ST s b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Formula -> ST s b) -> [Formula] -> ST s [b]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Formula -> ST s b
g [Formula]
ps
                Not Formula
p -> b -> b
forall a. Complement a => a -> a
notB (b -> b) -> ST s b -> ST s b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p
                Imply Formula
p Formula
q -> b -> b -> b
forall a. Boolean a => a -> a -> a
(.=>.) (b -> b -> b) -> ST s b -> ST s (b -> b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p ST s (b -> b) -> ST s b -> ST s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> ST s b
g Formula
q
                Equiv Formula
p Formula
q -> b -> b -> b
forall a. Boolean a => a -> a -> a
(.<=>.) (b -> b -> b) -> ST s b -> ST s (b -> b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p ST s (b -> b) -> ST s b -> ST s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> ST s b
g Formula
q
                ITE Formula
p Formula
q Formula
r -> b -> b -> b -> b
forall b a. IfThenElse b a => b -> a -> a -> a
ite (b -> b -> b -> b) -> ST s b -> ST s (b -> b -> b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p ST s (b -> b -> b) -> ST s b -> ST s (b -> b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> ST s b
g Formula
q ST s (b -> b) -> ST s b -> ST s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> ST s b
g Formula
r
            HashTable s Formula b -> Formula -> b -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s Formula b
h Formula
x b
y
            b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
y
  Formula -> ST s b
g Formula
formula

evalFormula :: SAT.IModel m => m -> Formula -> Bool
evalFormula :: m -> Formula -> Bool
evalFormula m
m = (Id -> Bool) -> Formula -> Bool
forall b. Boolean b => (Id -> b) -> Formula -> b
fold (m -> Id -> Bool
forall m. IModel m => m -> Id -> Bool
SAT.evalLit m
m)

toBoolExpr :: Formula -> BoolExpr.BoolExpr SAT.Lit
toBoolExpr :: Formula -> BoolExpr Id
toBoolExpr = (Id -> BoolExpr Id) -> Formula -> BoolExpr Id
forall b. Boolean b => (Id -> b) -> Formula -> b
fold Id -> BoolExpr Id
forall a. a -> BoolExpr a
BoolExpr.Atom

fromBoolExpr :: BoolExpr.BoolExpr SAT.Lit -> Formula
fromBoolExpr :: BoolExpr Id -> Formula
fromBoolExpr = (Id -> Formula) -> BoolExpr Id -> Formula
forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
BoolExpr.fold Id -> Formula
Atom

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

simplify :: Formula -> Formula
simplify :: Formula -> Formula
simplify = Simplify -> Formula
runSimplify (Simplify -> Formula)
-> (Formula -> Simplify) -> Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id -> Simplify) -> Formula -> Simplify
forall b. Boolean b => (Id -> b) -> Formula -> b
fold (Formula -> Simplify
Simplify (Formula -> Simplify) -> (Id -> Formula) -> Id -> Simplify
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Formula
Atom)

newtype Simplify = Simplify{ Simplify -> Formula
runSimplify :: Formula }

instance Complement Simplify where
  notB :: Simplify -> Simplify
notB (Simplify (Not Formula
x)) = Formula -> Simplify
Simplify Formula
x
  notB (Simplify Formula
x) = Formula -> Simplify
Simplify (Formula -> Formula
Not Formula
x)

instance MonotoneBoolean (Simplify) where
  orB :: [Simplify] -> Simplify
orB [Simplify]
xs
    | (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Formula -> Bool
isTrue [Formula]
ys = Formula -> Simplify
Simplify Formula
forall a. MonotoneBoolean a => a
true
    | Bool
otherwise = Formula -> Simplify
Simplify (Formula -> Simplify) -> Formula -> Simplify
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Or [Formula]
ys
    where
      ys :: [Formula]
ys = [[Formula]] -> [Formula]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Formula -> [Formula]
f Formula
x | Simplify Formula
x <- [Simplify]
xs]
      f :: Formula -> [Formula]
f (Or [Formula]
zs) = [Formula]
zs
      f Formula
z = [Formula
z]
  andB :: [Simplify] -> Simplify
andB [Simplify]
xs
    | (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Formula -> Bool
isFalse [Formula]
ys = Formula -> Simplify
Simplify Formula
forall a. MonotoneBoolean a => a
false
    | Bool
otherwise = Formula -> Simplify
Simplify (Formula -> Simplify) -> Formula -> Simplify
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
And [Formula]
ys
    where
      ys :: [Formula]
ys = [[Formula]] -> [Formula]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Formula -> [Formula]
f Formula
x | Simplify Formula
x <- [Simplify]
xs]
      f :: Formula -> [Formula]
f (And [Formula]
zs) = [Formula]
zs
      f Formula
z = [Formula
z]

instance IfThenElse Simplify Simplify where
  ite :: Simplify -> Simplify -> Simplify -> Simplify
ite (Simplify Formula
c) (Simplify Formula
t) (Simplify Formula
e)
    | Formula -> Bool
isTrue Formula
c  = Formula -> Simplify
Simplify Formula
t
    | Formula -> Bool
isFalse Formula
c = Formula -> Simplify
Simplify Formula
e
    | Bool
otherwise = Formula -> Simplify
Simplify (Formula -> Formula -> Formula -> Formula
ITE Formula
c Formula
t Formula
e)

instance Boolean Simplify where
  Simplify Formula
x .=>. :: Simplify -> Simplify -> Simplify
.=>. Simplify Formula
y
    | Formula -> Bool
isFalse Formula
x = Simplify
forall a. MonotoneBoolean a => a
true
    | Formula -> Bool
isTrue Formula
y  = Simplify
forall a. MonotoneBoolean a => a
true
    | Formula -> Bool
isTrue Formula
x  = Formula -> Simplify
Simplify Formula
y
    | Formula -> Bool
isFalse Formula
y = Simplify -> Simplify
forall a. Complement a => a -> a
notB (Formula -> Simplify
Simplify Formula
x)
    | Bool
otherwise = Formula -> Simplify
Simplify (Formula
x Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. Formula
y)

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

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

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