module Satchmo.Boolean.Op

( constant
, and, or, xor, xor2, equals2, equals, implies, (||), (&&)
, fun2, fun3
, ifThenElse, ifThenElseM
, assert_fun2, assert_fun3
, monadic
)

where

import Prelude hiding ( and, or, not, (&&), (||) )
import qualified Prelude
import Control.Applicative ((<$>))
import Satchmo.MonadSAT
import Satchmo.Code
import Satchmo.Boolean.Data

-- import Satchmo.SAT ( SAT) -- for specializations

import Control.Monad ( foldM, when )

and :: MonadSAT m => [ Boolean ] -> m Boolean

and :: forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [] = Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
constant Bool
True
and [Boolean
x]= Boolean -> m Boolean
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
x
and [Boolean]
xs = do
    Boolean
y <- m Boolean
forall (m :: * -> *). MonadSAT m => m Boolean
boolean
    [m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([m ()] -> m ()) -> [m ()] -> m ()
forall a b. (a -> b) -> a -> b
$ do
        Boolean
x <- [Boolean]
xs
        m () -> [m ()]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (m () -> [m ()]) -> m () -> [m ()]
forall a b. (a -> b) -> a -> b
$ [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean -> Boolean
not Boolean
y, Boolean
x ]
    [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr ([Boolean] -> m ()) -> [Boolean] -> m ()
forall a b. (a -> b) -> a -> b
$ Boolean
y Boolean -> [Boolean] -> [Boolean]
forall a. a -> [a] -> [a]
: (Boolean -> Boolean) -> [Boolean] -> [Boolean]
forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
not [Boolean]
xs
    Boolean -> m Boolean
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
y

or :: MonadSAT m => [ Boolean ] -> m Boolean
or :: forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [] = Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
constant Bool
False
or [Boolean
x]= Boolean -> m Boolean
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
x
or [Boolean]
xs = do
    Boolean
y <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and ([Boolean] -> m Boolean) -> [Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ (Boolean -> Boolean) -> [Boolean] -> [Boolean]
forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
not [Boolean]
xs
    Boolean -> m Boolean
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Boolean -> m Boolean) -> Boolean -> m Boolean
forall a b. (a -> b) -> a -> b
$ Boolean -> Boolean
not Boolean
y

Boolean
x && :: Boolean -> Boolean -> m Boolean
&& Boolean
y = [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
x,Boolean
y]
Boolean
x || :: Boolean -> Boolean -> m Boolean
|| Boolean
y = [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [Boolean
x,Boolean
y]

xor :: MonadSAT m => [ Boolean ] -> m Boolean
xor :: forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
xor [] = Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
constant Bool
False
xor (Boolean
x:[Boolean]
xs) = (Boolean -> Boolean -> m Boolean)
-> Boolean -> [Boolean] -> m Boolean
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Boolean -> Boolean -> m Boolean
forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
xor2 Boolean
x [Boolean]
xs

equals :: MonadSAT m => [ Boolean ] -> m Boolean
equals :: forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
equals [] = Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
constant Bool
True
equals [Boolean
x] = Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
constant Bool
True
equals (Boolean
x:[Boolean]
xs) = (Boolean -> Boolean -> m Boolean)
-> Boolean -> [Boolean] -> m Boolean
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Boolean -> Boolean -> m Boolean
forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
equals2 Boolean
x [Boolean]
xs

equals2 :: MonadSAT m => Boolean -> Boolean -> m Boolean
equals2 :: forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
equals2 Boolean
a Boolean
b = Boolean -> Boolean
not (Boolean -> Boolean) -> m Boolean -> m Boolean
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Boolean -> Boolean -> m Boolean
forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
xor2 Boolean
a Boolean
b

implies :: MonadSAT m => Boolean -> Boolean -> m Boolean
implies :: forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
implies Boolean
a Boolean
b = [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [Boolean -> Boolean
not Boolean
a, Boolean
b]

ifThenElse :: MonadSAT m => Boolean -> m Boolean -> m Boolean -> m Boolean
ifThenElse :: forall (m :: * -> *).
MonadSAT m =>
Boolean -> m Boolean -> m Boolean -> m Boolean
ifThenElse Boolean
condition m Boolean
ifTrue m Boolean
ifFalse = do
  Boolean
trueBranch <- m Boolean
ifTrue
  Boolean
falseBranch <- m Boolean
ifFalse
  ([Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
condition Boolean -> Boolean -> m Boolean
forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
`implies` Boolean
trueBranch
              , Boolean -> Boolean
not Boolean
condition Boolean -> Boolean -> m Boolean
forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
`implies` Boolean
falseBranch ]

ifThenElseM :: MonadSAT m => m Boolean -> m Boolean -> m Boolean -> m Boolean
ifThenElseM :: forall (m :: * -> *).
MonadSAT m =>
m Boolean -> m Boolean -> m Boolean -> m Boolean
ifThenElseM m Boolean
conditionM m Boolean
ifTrue m Boolean
ifFalse = do
  Boolean
c <- m Boolean
conditionM
  Boolean -> m Boolean -> m Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
Boolean -> m Boolean -> m Boolean -> m Boolean
ifThenElse Boolean
c m Boolean
ifTrue m Boolean
ifFalse

-- | implement the function by giving a full CNF
-- that determines the outcome
fun2 :: MonadSAT m => 
        ( Bool -> Bool -> Bool )
     -> Boolean -> Boolean 
     -> m Boolean
fun2 :: forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 Bool -> Bool -> Bool
f Boolean
x Boolean
y = do
    Boolean
r <- m Boolean
forall (m :: * -> *). MonadSAT m => m Boolean
boolean
    [m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([m ()] -> m ()) -> [m ()] -> m ()
forall a b. (a -> b) -> a -> b
$ do
        Bool
a <- [ Bool
False, Bool
True ]
        Bool
b <- [ Bool
False, Bool
True ]
        let pack :: Bool -> Boolean -> Boolean
pack Bool
flag Boolean
var = if Bool
flag then Boolean -> Boolean
not Boolean
var else Boolean
var
        m () -> [m ()]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (m () -> [m ()]) -> m () -> [m ()]
forall a b. (a -> b) -> a -> b
$ [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr
            [ Bool -> Boolean -> Boolean
pack Bool
a Boolean
x, Bool -> Boolean -> Boolean
pack Bool
b Boolean
y, Bool -> Boolean -> Boolean
pack (Bool -> Bool
Prelude.not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
f Bool
a Bool
b) Boolean
r ]
    Boolean -> m Boolean
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
r

assert_fun2 :: MonadSAT m => 
        ( Bool -> Bool -> Bool )
     -> Boolean -> Boolean 
     -> m ()
assert_fun2 :: forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m ()
assert_fun2 Bool -> Bool -> Bool
f Boolean
x Boolean
y = [m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([m ()] -> m ()) -> [m ()] -> m ()
forall a b. (a -> b) -> a -> b
$ do
        Bool
a <- [ Bool
False, Bool
True ]
        Bool
b <- [ Bool
False, Bool
True ]
        let pack :: Bool -> Boolean -> Boolean
pack Bool
flag Boolean
var = if Bool
flag then Boolean -> Boolean
not Boolean
var else Boolean
var
        m () -> [m ()]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (m () -> [m ()]) -> m () -> [m ()]
forall a b. (a -> b) -> a -> b
$ Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Bool -> Bool
Prelude.not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
f Bool
a Bool
b ) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assert 
            [ Bool -> Boolean -> Boolean
pack Bool
a Boolean
x, Bool -> Boolean -> Boolean
pack Bool
b Boolean
y ]
     

-- | implement the function by giving a full CNF
-- that determines the outcome
fun3 :: MonadSAT m => 
        ( Bool -> Bool -> Bool -> Bool )
     -> Boolean -> Boolean -> Boolean
     -> m Boolean
fun3 :: forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool -> Bool)
-> Boolean -> Boolean -> Boolean -> m Boolean
fun3 Bool -> Bool -> Bool -> Bool
f Boolean
x Boolean
y Boolean
z = do
    Boolean
r <- m Boolean
forall (m :: * -> *). MonadSAT m => m Boolean
boolean
    [m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([m ()] -> m ()) -> [m ()] -> m ()
forall a b. (a -> b) -> a -> b
$ do
        Bool
a <- [ Bool
False, Bool
True ]
        Bool
b <- [ Bool
False, Bool
True ]
        Bool
c <- [ Bool
False, Bool
True ]
        let pack :: Bool -> Boolean -> Boolean
pack Bool
flag Boolean
var = if Bool
flag then Boolean -> Boolean
not Boolean
var else Boolean
var
        m () -> [m ()]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (m () -> [m ()]) -> m () -> [m ()]
forall a b. (a -> b) -> a -> b
$ [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr
            [ Bool -> Boolean -> Boolean
pack Bool
a Boolean
x, Bool -> Boolean -> Boolean
pack Bool
b Boolean
y, Bool -> Boolean -> Boolean
pack Bool
c Boolean
z
            , Bool -> Boolean -> Boolean
pack (Bool -> Bool
Prelude.not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool -> Bool
f Bool
a Bool
b Bool
c) Boolean
r 
            ]
    Boolean -> m Boolean
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
r

assert_fun3 :: MonadSAT m => 
        ( Bool -> Bool -> Bool -> Bool )
     -> Boolean -> Boolean -> Boolean
     -> m ()
assert_fun3 :: forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool -> Bool)
-> Boolean -> Boolean -> Boolean -> m ()
assert_fun3 Bool -> Bool -> Bool -> Bool
f Boolean
x Boolean
y Boolean
z = [m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([m ()] -> m ()) -> [m ()] -> m ()
forall a b. (a -> b) -> a -> b
$ do
        Bool
a <- [ Bool
False, Bool
True ]
        Bool
b <- [ Bool
False, Bool
True ]
        Bool
c <- [ Bool
False, Bool
True ]
        let pack :: Bool -> Boolean -> Boolean
pack Bool
flag Boolean
var = if Bool
flag then Boolean -> Boolean
not Boolean
var else Boolean
var
        m () -> [m ()]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (m () -> [m ()]) -> m () -> [m ()]
forall a b. (a -> b) -> a -> b
$ Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Bool -> Bool
Prelude.not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool -> Bool
f Bool
a Bool
b Bool
c ) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assert 
            [ Bool -> Boolean -> Boolean
pack Bool
a Boolean
x, Bool -> Boolean -> Boolean
pack Bool
b Boolean
y, Bool -> Boolean -> Boolean
pack Bool
c Boolean
z ]
     

xor2 :: MonadSAT m => Boolean -> Boolean -> m Boolean
xor2 :: forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
xor2 = (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
-- xor2 = xor2_orig

-- for historic reasons:
xor2_orig :: MonadSAT m => Boolean -> Boolean -> m Boolean
xor2_orig :: forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
xor2_orig Boolean
x Boolean
y = do
    Boolean
a <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
x, Boolean -> Boolean
not Boolean
y ]
    Boolean
b <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean -> Boolean
not Boolean
x, Boolean
y ]
    [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [ Boolean
a, Boolean
b ]