module Satchmo.Boolean.Data
( Boolean(Constant), Booleans, encode
, boolean, exists, forall
, constant
, not, assert, assertW, monadic
)
where
import Prelude hiding ( not )
import qualified Prelude
import qualified Satchmo.Code as C
import Satchmo.Data
import Satchmo.MonadSAT
import Satchmo.SAT (SAT)
import Data.Array
import Data.Maybe ( fromJust )
import Data.List ( partition )
import Control.Monad.Reader
data Boolean = Boolean
{ encode :: ! Literal
}
| Constant { value :: ! Bool }
type Booleans = [ Boolean ]
isConstant :: Boolean -> Bool
isConstant ( Constant {} ) = True
isConstant _ = False
instance C.Decode Boolean Bool where
decode b = case b of
Boolean {} -> asks $ \ arr ->
let x = encode b
in positive x == arr ! ( variable x )
Constant {} -> return $ value b
boolean :: MonadSAT m => m Boolean
boolean = exists
exists :: MonadSAT m => m Boolean
exists = do
x <- fresh
return $ Boolean
{ encode = x
}
forall :: MonadSAT m => m Boolean
forall = do
x <- fresh_forall
return $ Boolean
{ encode = x
}
constant :: MonadSAT m => Bool -> m Boolean
constant v = do
return $ Constant { value = v }
not :: Boolean -> Boolean
not b = case b of
Boolean {} -> Boolean
{ encode = nicht $ encode b
}
Constant {} -> Constant { value = Prelude.not $ value b }
assert :: MonadSAT m => [ Boolean ] -> m ()
assert bs = do
let ( con, uncon ) = partition isConstant bs
let cval = Prelude.or $ map value con
when ( Prelude.not cval ) $ emit $ clause $ map encode uncon
assertW :: MonadSAT m => Weight -> [ Boolean ] -> m ()
assertW 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
monadic :: Monad m
=> ( [ a ] -> m b )
-> ( [ m a ] -> m b )
monadic f ms = do
xs <- sequence ms
f xs