{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
#if (__GLASGOW_HASKELL__ >= 708)
{-# LANGUAGE AllowAmbiguousTypes #-}
#endif
module Satchmo.MonadSAT
( MonadSAT(..), Weight
, Header (..)
)
where
import Satchmo.Data
import Satchmo.Code
import Control.Applicative
import Control.Monad.Trans (lift)
import Control.Monad.Cont (ContT)
import Control.Monad.List (ListT)
import Control.Monad.Reader (ReaderT)
import Control.Monad.Fix ( MonadFix )
import qualified Control.Monad.State as Lazy (StateT)
import qualified Control.Monad.Writer as Lazy (WriterT)
import qualified Control.Monad.RWS as Lazy (RWST)
import qualified Control.Monad.State.Strict as Strict (StateT)
import qualified Control.Monad.Writer.Strict as Strict (WriterT)
import qualified Control.Monad.RWS.Strict as Strict (RWST)
import Data.Monoid
type Weight = Int
class (
Applicative m, Monad m) => MonadSAT m where
fresh, fresh_forall :: m Literal
emit :: Clause -> m ()
note :: String -> m ()
type Decoder m :: * -> *
decode_variable :: Variable -> Decoder m Bool
type NumClauses = Integer
type NumVars = Integer
data =
{ Header -> Int
numClauses, Header -> Int
numVars :: !Int
, Header -> [Int]
universals :: ![Int]
}
deriving Int -> Header -> ShowS
[Header] -> ShowS
Header -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Header] -> ShowS
$cshowList :: [Header] -> ShowS
show :: Header -> String
$cshow :: Header -> String
showsPrec :: Int -> Header -> ShowS
$cshowsPrec :: Int -> Header -> ShowS
Show
instance (Monad m, MonadSAT m) => MonadSAT (ListT m) where
fresh :: ListT m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: ListT m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> ListT m ()
emit = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> ListT m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note
instance (Monad m, MonadSAT m) => MonadSAT (ReaderT r m) where
fresh :: ReaderT r m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: ReaderT r m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> ReaderT r m ()
emit = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> ReaderT r m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note
instance (Monad m, MonadSAT m) => MonadSAT (Lazy.StateT s m) where
fresh :: StateT s m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: StateT s m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> StateT s m ()
emit = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> StateT s m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note
instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.RWST r w s m) where
fresh :: RWST r w s m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: RWST r w s m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> RWST r w s m ()
emit = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> RWST r w s m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note
instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.WriterT w m) where
fresh :: WriterT w m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: WriterT w m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> WriterT w m ()
emit = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> WriterT w m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note
instance (Monad m, MonadSAT m) => MonadSAT (Strict.StateT s m) where
fresh :: StateT s m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: StateT s m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> StateT s m ()
emit = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> StateT s m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note
instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.RWST r w s m) where
fresh :: RWST r w s m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: RWST r w s m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> RWST r w s m ()
emit = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> RWST r w s m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note
instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.WriterT w m) where
fresh :: WriterT w m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: WriterT w m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> WriterT w m ()
emit = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> WriterT w m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note
instance (Monad m, MonadSAT m) => MonadSAT (ContT s m) where
fresh :: ContT s m Literal
fresh = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: ContT s m Literal
fresh_forall = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> ContT s m ()
emit = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> ContT s m ()
note = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadSAT m => String -> m ()
note