{-# language MultiParamTypeClasses #-}
{-# language TypeSynonymInstances #-}
{-# language FlexibleInstances #-}
{-# language NoMonomorphismRestriction #-}
{-# language TemplateHaskell #-}
{-# language DeriveGeneric #-}

module Satchmo.Boolean.Data

( Boolean(..), Booleans, encode
, boolean, exists, forall_
, constant
, not, monadic
, assertOr -- , assertOrW
, assertAnd -- , assertAndW
, assert -- for legacy code
)

where

import Prelude hiding ( not )
import qualified Prelude

import qualified Satchmo.Code as C

import Satchmo.Data
import Satchmo.MonadSAT

-- import Data.Function.Memoize
import Data.Array
import Data.Maybe ( fromJust )
import Data.List ( partition )

import Control.Monad
import Control.Monad.Reader

import GHC.Generics (Generic)
import Data.Hashable

data Boolean = Boolean { Boolean -> Literal
encode :: !Literal }
     | Constant { Boolean -> Bool
value :: !Bool }
  deriving (Boolean -> Boolean -> Bool
(Boolean -> Boolean -> Bool)
-> (Boolean -> Boolean -> Bool) -> Eq Boolean
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Boolean -> Boolean -> Bool
== :: Boolean -> Boolean -> Bool
$c/= :: Boolean -> Boolean -> Bool
/= :: Boolean -> Boolean -> Bool
Eq, Eq Boolean
Eq Boolean =>
(Boolean -> Boolean -> Ordering)
-> (Boolean -> Boolean -> Bool)
-> (Boolean -> Boolean -> Bool)
-> (Boolean -> Boolean -> Bool)
-> (Boolean -> Boolean -> Bool)
-> (Boolean -> Boolean -> Boolean)
-> (Boolean -> Boolean -> Boolean)
-> Ord Boolean
Boolean -> Boolean -> Bool
Boolean -> Boolean -> Ordering
Boolean -> Boolean -> Boolean
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Boolean -> Boolean -> Ordering
compare :: Boolean -> Boolean -> Ordering
$c< :: Boolean -> Boolean -> Bool
< :: Boolean -> Boolean -> Bool
$c<= :: Boolean -> Boolean -> Bool
<= :: Boolean -> Boolean -> Bool
$c> :: Boolean -> Boolean -> Bool
> :: Boolean -> Boolean -> Bool
$c>= :: Boolean -> Boolean -> Bool
>= :: Boolean -> Boolean -> Bool
$cmax :: Boolean -> Boolean -> Boolean
max :: Boolean -> Boolean -> Boolean
$cmin :: Boolean -> Boolean -> Boolean
min :: Boolean -> Boolean -> Boolean
Ord, Int -> Boolean -> ShowS
[Boolean] -> ShowS
Boolean -> String
(Int -> Boolean -> ShowS)
-> (Boolean -> String) -> ([Boolean] -> ShowS) -> Show Boolean
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Boolean -> ShowS
showsPrec :: Int -> Boolean -> ShowS
$cshow :: Boolean -> String
show :: Boolean -> String
$cshowList :: [Boolean] -> ShowS
showList :: [Boolean] -> ShowS
Show, (forall x. Boolean -> Rep Boolean x)
-> (forall x. Rep Boolean x -> Boolean) -> Generic Boolean
forall x. Rep Boolean x -> Boolean
forall x. Boolean -> Rep Boolean x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Boolean -> Rep Boolean x
from :: forall x. Boolean -> Rep Boolean x
$cto :: forall x. Rep Boolean x -> Boolean
to :: forall x. Rep Boolean x -> Boolean
Generic)

instance Hashable Boolean

--  $(deriveMemoizable ''Boolean)

{-

-- FIXME: @Pepe: what is the reason for these instances?

instance Eq Boolean where
  b1@Boolean{}  == b2@Boolean{}  = encode b1 == encode b2
  b1@Constant{} == b2@Constant{} = value  b1 == value  b2
  _ == _ = False

instance Ord Boolean where
  b1@Boolean{}  `compare` b2@Boolean{}  = encode b1 `compare` encode b2
  b1@Constant{} `compare` b2@Constant{} = value  b1 `compare` value  b2
  Boolean{} `compare` Constant{} = GT
  Constant{} `compare` Boolean{} = LT

instance Enum Boolean where
  fromEnum (Constant True)  = -1
  fromEnum (Constant False) = 0
  fromEnum (Boolean (Literal lit) dec) = lit

  toEnum 0    = Constant False
  toEnum (-1) = Constant True
  toEnum l    = let x = literal l in Boolean x (asks $ \fm -> fromJust (M.lookup x fm))

-}

type Booleans = [ Boolean ]

isConstant :: Boolean -> Bool
isConstant :: Boolean -> Bool
isConstant ( Constant {} ) = Bool
True
isConstant Boolean
_ = Bool
False


boolean :: MonadSAT m => m ( Boolean )
boolean :: forall (m :: * -> *). MonadSAT m => m Boolean
boolean = m Boolean
forall (m :: * -> *). MonadSAT m => m Boolean
exists

exists :: MonadSAT m => m ( Boolean )
exists :: forall (m :: * -> *). MonadSAT m => m Boolean
exists = do
    Literal
x <- m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh
    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 
           { encode :: Literal
encode = Literal
x
{-                      
           , decode = asks $ \ fm -> 
                      ( positive x == )
                    $ fromJust
                    $ M.lookup ( variable x ) fm
-}
           }

forall_ :: MonadSAT m => m ( Boolean )
forall_ :: forall (m :: * -> *). MonadSAT m => m Boolean
forall_ = do
    Literal
x <- m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
    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 
           { encode :: Literal
encode = Literal
x
--           , decode = error "Boolean.forall_ cannot be decoded"
           }

constant :: MonadSAT m => Bool -> m (Boolean)
constant :: forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
constant Bool
v = do
    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
$ Constant { value :: Bool
value = Bool
v } 
{-# INLINABLE constant #-}

-- not :: Boolean -> Boolean
not :: Boolean -> Boolean
not Boolean
b = case Boolean
b of
    Boolean {} -> Boolean 
      { encode :: Literal
encode = Literal -> Literal
nicht (Literal -> Literal) -> Literal -> Literal
forall a b. (a -> b) -> a -> b
$ Boolean -> Literal
encode Boolean
b
      -- , decode = do x <- decode b ; return $ Prelude.not x
      }
    Constant {} -> Constant { value :: Bool
value = Bool -> Bool
Prelude.not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Boolean -> Bool
value Boolean
b }
{-# INLINABLE not #-}

-- assertOr, assertAnd :: MonadSAT m => [ Boolean (Literal m ) ] -> m ()
assertOr :: [Boolean] -> m ()
assertOr = [Boolean] -> m ()
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert

assert :: MonadSAT m => [ Boolean ] -> m ()
assert :: forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean]
bs = do
    let ( [Boolean]
con, [Boolean]
uncon ) = (Boolean -> Bool) -> [Boolean] -> ([Boolean], [Boolean])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Boolean -> Bool
isConstant [Boolean]
bs
    let cval :: Bool
cval = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Boolean -> Bool) -> [Boolean] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Bool
value [Boolean]
con
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Bool -> Bool
Prelude.not Bool
cval ) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Clause -> m ()
forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit (Clause -> m ()) -> Clause -> m ()
forall a b. (a -> b) -> a -> b
$ [Literal] -> Clause
clause ([Literal] -> Clause) -> [Literal] -> Clause
forall a b. (a -> b) -> a -> b
$ (Boolean -> Literal) -> [Boolean] -> [Literal]
forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Literal
encode [Boolean]
uncon
{-# INLINABLE assert #-}

-- assertAnd :: MonadSAT m => [ Boolean ] -> m ()
assertAnd :: t Boolean -> m ()
assertAnd t Boolean
bs = t Boolean -> (Boolean -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ t Boolean
bs ((Boolean -> m ()) -> m ()) -> (Boolean -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ [Boolean] -> m ()
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr ([Boolean] -> m ()) -> (Boolean -> [Boolean]) -> Boolean -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Boolean -> [Boolean]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return

{-

assertOrW, assertAndW :: MonadSAT m => Weight -> [ Boolean ] -> m ()
assertOrW w bs = do
    let ( con, uncon ) = partition isConstant bs
    let cval = Prelude.or $ map value con
    when ( Prelude.not cval ) $ emitW w $ clause $ map encode uncon

assertAndW w bs = forM_ bs $ assertOrW w . return

-}

monadic :: Monad m
        => ( [ a ] -> m b )
        -> ( [ m a ] -> m b )
monadic :: forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic [a] -> m b
f [m a]
ms = do
    [a]
xs <- [m a] -> m [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [m a]
ms
    [a] -> m b
f [a]
xs