{-# 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)
#if !MIN_VERSION_mtl(2,3,0)
import Control.Monad.List (ListT)
#endif
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
(Int -> Header -> ShowS)
-> (Header -> String) -> ([Header] -> ShowS) -> Show Header
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Header -> ShowS
showsPrec :: Int -> Header -> ShowS
$cshow :: Header -> String
show :: Header -> String
$cshowList :: [Header] -> ShowS
showList :: [Header] -> ShowS
Show
#if !MIN_VERSION_mtl(2,3,0)
instance (Monad m, MonadSAT m) => MonadSAT (ListT m) where
fresh = lift fresh
fresh_forall = lift fresh_forall
emit = lift . emit
note = lift . note
#endif
instance (Monad m, MonadSAT m) => MonadSAT (ReaderT r m) where
fresh :: ReaderT r m Literal
fresh = m Literal -> ReaderT r m Literal
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: ReaderT r m Literal
fresh_forall = m Literal -> ReaderT r m Literal
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> ReaderT r m ()
emit = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ())
-> (Clause -> m ()) -> Clause -> ReaderT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> m ()
forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> ReaderT r m ()
note = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ())
-> (String -> m ()) -> String -> ReaderT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m ()
forall (m :: * -> *). MonadSAT m => String -> m ()
note
instance (Monad m, MonadSAT m) => MonadSAT (Lazy.StateT s m) where
fresh :: StateT s m Literal
fresh = m Literal -> StateT s m Literal
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: StateT s m Literal
fresh_forall = m Literal -> StateT s m Literal
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> StateT s m ()
emit = m () -> StateT s m ()
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT s m ())
-> (Clause -> m ()) -> Clause -> StateT s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> m ()
forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> StateT s m ()
note = m () -> StateT s m ()
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT s m ())
-> (String -> m ()) -> String -> StateT s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m ()
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 = m Literal -> RWST r w s m Literal
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: RWST r w s m Literal
fresh_forall = m Literal -> RWST r w s m Literal
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> RWST r w s m ()
emit = m () -> RWST r w s m ()
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> RWST r w s m ())
-> (Clause -> m ()) -> Clause -> RWST r w s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> m ()
forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> RWST r w s m ()
note = m () -> RWST r w s m ()
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> RWST r w s m ())
-> (String -> m ()) -> String -> RWST r w s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m ()
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 = m Literal -> WriterT w m Literal
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: WriterT w m Literal
fresh_forall = m Literal -> WriterT w m Literal
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> WriterT w m ()
emit = m () -> WriterT w m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT w m ())
-> (Clause -> m ()) -> Clause -> WriterT w m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> m ()
forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> WriterT w m ()
note = m () -> WriterT w m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT w m ())
-> (String -> m ()) -> String -> WriterT w m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m ()
forall (m :: * -> *). MonadSAT m => String -> m ()
note
instance (Monad m, MonadSAT m) => MonadSAT (Strict.StateT s m) where
fresh :: StateT s m Literal
fresh = m Literal -> StateT s m Literal
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: StateT s m Literal
fresh_forall = m Literal -> StateT s m Literal
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> StateT s m ()
emit = m () -> StateT s m ()
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT s m ())
-> (Clause -> m ()) -> Clause -> StateT s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> m ()
forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> StateT s m ()
note = m () -> StateT s m ()
forall (m :: * -> *) a. Monad m => m a -> StateT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT s m ())
-> (String -> m ()) -> String -> StateT s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m ()
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 = m Literal -> RWST r w s m Literal
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: RWST r w s m Literal
fresh_forall = m Literal -> RWST r w s m Literal
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> RWST r w s m ()
emit = m () -> RWST r w s m ()
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> RWST r w s m ())
-> (Clause -> m ()) -> Clause -> RWST r w s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> m ()
forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> RWST r w s m ()
note = m () -> RWST r w s m ()
forall (m :: * -> *) a. Monad m => m a -> RWST r w s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> RWST r w s m ())
-> (String -> m ()) -> String -> RWST r w s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m ()
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 = m Literal -> WriterT w m Literal
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: WriterT w m Literal
fresh_forall = m Literal -> WriterT w m Literal
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> WriterT w m ()
emit = m () -> WriterT w m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT w m ())
-> (Clause -> m ()) -> Clause -> WriterT w m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> m ()
forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> WriterT w m ()
note = m () -> WriterT w m ()
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT w m ())
-> (String -> m ()) -> String -> WriterT w m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m ()
forall (m :: * -> *). MonadSAT m => String -> m ()
note
instance (Monad m, MonadSAT m) => MonadSAT (ContT s m) where
fresh :: ContT s m Literal
fresh = m Literal -> ContT s m Literal
forall (m :: * -> *) a. Monad m => m a -> ContT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh
fresh_forall :: ContT s m Literal
fresh_forall = m Literal -> ContT s m Literal
forall (m :: * -> *) a. Monad m => m a -> ContT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m Literal
forall (m :: * -> *). MonadSAT m => m Literal
fresh_forall
emit :: Clause -> ContT s m ()
emit = m () -> ContT s m ()
forall (m :: * -> *) a. Monad m => m a -> ContT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ContT s m ())
-> (Clause -> m ()) -> Clause -> ContT s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> m ()
forall (m :: * -> *). MonadSAT m => Clause -> m ()
emit
note :: String -> ContT s m ()
note = m () -> ContT s m ()
forall (m :: * -> *) a. Monad m => m a -> ContT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ContT s m ())
-> (String -> m ()) -> String -> ContT s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m ()
forall (m :: * -> *). MonadSAT m => String -> m ()
note