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

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

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

instance Hashable Formula where
  hashWithSalt :: Lit -> Formula -> Lit
hashWithSalt Lit
s (Formula Lit
i UFormula
_) = forall a. Hashable a => Lit -> a -> Lit
hashWithSalt Lit
s Lit
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
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. 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 Lit
a) = Lit -> Description Formula
DAtom Lit
a
  describe (UAnd [Formula]
xs) = [Lit] -> Description Formula
DAnd [Lit
i | Formula Lit
i UFormula
_ <- [Formula]
xs]
  describe (UOr [Formula]
xs) = [Lit] -> Description Formula
DOr [Lit
i | Formula Lit
i UFormula
_ <- [Formula]
xs]
  describe (UNot (Formula Lit
i UFormula
_)) = Lit -> Description Formula
DNot Lit
i
  describe (UImply (Formula Lit
i UFormula
_) (Formula Lit
j UFormula
_)) = Lit -> Lit -> Description Formula
DImply Lit
i Lit
j
  describe (UEquiv (Formula Lit
i UFormula
_) (Formula Lit
j UFormula
_)) = Lit -> Lit -> Description Formula
DEquiv Lit
i Lit
j
  describe (UITE (Formula Lit
i UFormula
_) (Formula Lit
j UFormula
_) (Formula Lit
k UFormula
_)) = Lit -> Lit -> Lit -> Description Formula
DITE Lit
i Lit
j Lit
k
  identify :: Lit -> Uninterned Formula -> Formula
identify = Lit -> UFormula -> Formula
Formula
  cache :: Cache Formula
cache = Cache Formula
formulaCache

instance Hashable (Description Formula)

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

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

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

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

pattern Not :: Formula -> Formula
pattern $bNot :: Formula -> Formula
$mNot :: forall {r}. Formula -> (Formula -> r) -> ((# #) -> r) -> r
Not p <- (unintern -> UNot p) where
  Not Formula
p = 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) -> ((# #) -> r) -> r
And ps <- (unintern -> UAnd ps) where
  And [Formula]
ps = 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) -> ((# #) -> r) -> r
Or ps <- (unintern -> UOr ps) where
  Or [Formula]
ps = 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) -> ((# #) -> r) -> r
Equiv p q <- (unintern -> UEquiv p q) where
  Equiv Formula
p Formula
q = 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) -> ((# #) -> r) -> r
Imply p q <- (unintern -> UImply p q) where
  Imply Formula
p Formula
q = 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) -> ((# #) -> r) -> r
ITE p q r <- (unintern -> UITE p q r) where
  ITE Formula
p Formula
q Formula
r = 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 = forall t. Interned t => Uninterned t -> t
intern forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> UFormula
UNot

instance MonotoneBoolean Formula where
  andB :: [Formula] -> Formula
andB = forall t. Interned t => Uninterned t -> t
intern forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Formula] -> UFormula
UAnd
  orB :: [Formula] -> Formula
orB  = forall t. Interned t => Uninterned t -> t
intern 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 = 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 = forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> UFormula
UImply Formula
p Formula
q)
  .<=>. :: Formula -> Formula -> Formula
(.<=>.) Formula
p Formula
q = 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 :: forall b. Boolean b => (Lit -> b) -> Formula -> b
fold Lit -> b
f Formula
formula = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
  HashTable s Formula b
h <- forall s k v. Lit -> ST s (HashTable s k v)
C.newSized Lit
256
  let g :: Formula -> ST s b
g Formula
x = do
        Maybe b
m <- 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return b
y
          Maybe b
Nothing -> do
            b
y <-
              case Formula
x of
                Atom Lit
lit -> forall (m :: * -> *) a. Monad m => a -> m a
return (Lit -> b
f Lit
lit)
                And [Formula]
ps -> forall a. MonotoneBoolean a => [a] -> a
andB forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 -> forall a. MonotoneBoolean a => [a] -> a
orB forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 -> forall a. Complement a => a -> a
notB forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p
                Imply Formula
p Formula
q -> forall a. Boolean a => a -> a -> a
(.=>.) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p 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 -> forall a. Boolean a => a -> a -> a
(.<=>.) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p 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 -> forall b a. IfThenElse b a => b -> a -> a -> a
ite forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> ST s b
g Formula
q forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> ST s b
g Formula
r
            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
            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 :: forall m. IModel m => m -> Formula -> Bool
evalFormula m
m = forall b. Boolean b => (Lit -> b) -> Formula -> b
fold (forall m. IModel m => m -> Lit -> Bool
SAT.evalLit m
m)

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

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

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

simplify :: Formula -> Formula
simplify :: Formula -> Formula
simplify = Simplify -> Formula
runSimplify forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. Boolean b => (Lit -> b) -> Formula -> b
fold (Formula -> Simplify
Simplify forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lit -> 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
    | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Formula -> Bool
isTrue [Formula]
ys = Formula -> Simplify
Simplify forall a. MonotoneBoolean a => a
true
    | Bool
otherwise = Formula -> Simplify
Simplify forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Or [Formula]
ys
    where
      ys :: [Formula]
ys = 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
    | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Formula -> Bool
isFalse [Formula]
ys = Formula -> Simplify
Simplify forall a. MonotoneBoolean a => a
false
    | Bool
otherwise = Formula -> Simplify
Simplify forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
And [Formula]
ys
    where
      ys :: [Formula]
ys = 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 = forall a. MonotoneBoolean a => a
true
    | Formula -> Bool
isTrue Formula
y  = forall a. MonotoneBoolean a => a
true
    | Formula -> Bool
isTrue Formula
x  = Formula -> Simplify
Simplify Formula
y
    | Formula -> Bool
isFalse Formula
y = forall a. Complement a => a -> a
notB (Formula -> Simplify
Simplify Formula
x)
    | Bool
otherwise = Formula -> Simplify
Simplify (Formula
x 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

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