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

Boolean
x && :: Boolean -> Boolean -> m Boolean
&& Boolean
y = forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
x,Boolean
y]
Boolean
x || :: Boolean -> Boolean -> m Boolean
|| Boolean
y = 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 [] = forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
constant Bool
False
xor (Boolean
x:[Boolean]
xs) = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM 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 [] = forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
constant Bool
True
equals [Boolean
x] = forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
constant Bool
True
equals (Boolean
x:[Boolean]
xs) = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = 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
  forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
condition forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
`implies` Boolean
trueBranch
              , Boolean -> Boolean
not Boolean
condition 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
  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 <- forall (m :: * -> *). MonadSAT m => m Boolean
boolean
    forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ 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
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
f Bool
a Bool
b) Boolean
r ]
    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 = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ 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
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Bool -> Bool
Prelude.not forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
f Bool
a Bool
b ) forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *). MonadSAT m => m Boolean
boolean
    forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ 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
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool -> Bool
f Bool
a Bool
b Bool
c) Boolean
r 
            ]
    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 = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ 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
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Bool -> Bool
Prelude.not forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool -> Bool
f Bool
a Bool
b Bool
c ) forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 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 <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
x, Boolean -> Boolean
not Boolean
y ]
    Boolean
b <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean -> Boolean
not Boolean
x, Boolean
y ]
    forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [ Boolean
a, Boolean
b ]