{-# 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
, assertAnd
, assert
)
where
import Prelude hiding ( not )
import qualified Prelude
import qualified Satchmo.Code as C
import Satchmo.Data
import Satchmo.MonadSAT
import Data.Array
import Data.Maybe ( fromJust )
import Data.List ( partition )
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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Boolean -> Boolean -> Bool
$c/= :: Boolean -> Boolean -> Bool
== :: Boolean -> Boolean -> Bool
$c== :: Boolean -> Boolean -> Bool
Eq, Eq 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
min :: Boolean -> Boolean -> Boolean
$cmin :: Boolean -> Boolean -> Boolean
max :: Boolean -> Boolean -> Boolean
$cmax :: Boolean -> Boolean -> Boolean
>= :: Boolean -> Boolean -> Bool
$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
compare :: Boolean -> Boolean -> Ordering
$ccompare :: Boolean -> Boolean -> Ordering
Ord, Int -> Boolean -> ShowS
[Boolean] -> ShowS
Boolean -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Boolean] -> ShowS
$cshowList :: [Boolean] -> ShowS
show :: Boolean -> String
$cshow :: Boolean -> String
showsPrec :: Int -> Boolean -> ShowS
$cshowsPrec :: Int -> Boolean -> ShowS
Show, 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
$cto :: forall x. Rep Boolean x -> Boolean
$cfrom :: forall x. Boolean -> Rep Boolean x
Generic)
instance Hashable Boolean
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 = forall (m :: * -> *). MonadSAT m => m Boolean
exists
exists :: MonadSAT m => m ( Boolean )
exists :: forall (m :: * -> *). MonadSAT m => m Boolean
exists = do
Literal
x <- forall (m :: * -> *). MonadSAT m => m Literal
fresh
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Boolean
{ encode :: Literal
encode = Literal
x
}
forall :: MonadSAT m => m ( Boolean )
forall :: forall (m :: * -> *). MonadSAT m => m Boolean
forall = do
Literal
x <- forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Boolean
{ encode :: Literal
encode = Literal
x
}
constant :: MonadSAT m => Bool -> m (Boolean)
constant :: forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
constant Bool
v = do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Constant { value :: Bool
value = Bool
v }
{-# INLINABLE constant #-}
not :: Boolean -> Boolean
not Boolean
b = case Boolean
b of
Boolean {} -> Boolean
{ encode :: Literal
encode = Literal -> Literal
nicht forall a b. (a -> b) -> a -> b
$ Boolean -> Literal
encode Boolean
b
}
Constant {} -> Constant { value :: Bool
value = Bool -> Bool
Prelude.not forall a b. (a -> b) -> a -> b
$ Boolean -> Bool
value Boolean
b }
{-# INLINABLE not #-}
assertOr :: [Boolean] -> m ()
assertOr = 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 ) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Boolean -> Bool
isConstant [Boolean]
bs
let cval :: Bool
cval = forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.or forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Bool
value [Boolean]
con
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Bool -> Bool
Prelude.not Bool
cval ) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit forall a b. (a -> b) -> a -> b
$ [Literal] -> Clause
clause forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Literal
encode [Boolean]
uncon
{-# INLINABLE assert #-}
assertAnd :: t Boolean -> m ()
assertAnd t Boolean
bs = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ t Boolean
bs forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
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 <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [m a]
ms
[a] -> m b
f [a]
xs