{-# LANGUAGE BangPatterns, GeneralizedNewtypeDeriving, CPP #-} module Jukebox.Sat.Easy where import MiniSat hiding (neg) import qualified MiniSat import Jukebox.Form(Signed(..), neg) import qualified Data.Map.Strict as Map import Data.Map(Map) import Control.Monad import Control.Monad.Trans.Class import Control.Monad.IO.Class import Control.Monad.Trans.State.Strict import Control.Monad.Trans.Reader import Data.Maybe #if __GLASGOW_HASKELL__ < 710 import Control.Applicative import Data.Traversable(traverse) #endif newtype Sat1 a b = Sat1 { Sat1 a b -> ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b runSat1_ :: ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b } deriving (a -> Sat1 a b -> Sat1 a a (a -> b) -> Sat1 a a -> Sat1 a b (forall a b. (a -> b) -> Sat1 a a -> Sat1 a b) -> (forall a b. a -> Sat1 a b -> Sat1 a a) -> Functor (Sat1 a) forall a b. a -> Sat1 a b -> Sat1 a a forall a b. (a -> b) -> Sat1 a a -> Sat1 a b forall a a b. a -> Sat1 a b -> Sat1 a a forall a a b. (a -> b) -> Sat1 a a -> Sat1 a b forall (f :: * -> *). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f <$ :: a -> Sat1 a b -> Sat1 a a $c<$ :: forall a a b. a -> Sat1 a b -> Sat1 a a fmap :: (a -> b) -> Sat1 a a -> Sat1 a b $cfmap :: forall a a b. (a -> b) -> Sat1 a a -> Sat1 a b Functor, Functor (Sat1 a) a -> Sat1 a a Functor (Sat1 a) -> (forall a. a -> Sat1 a a) -> (forall a b. Sat1 a (a -> b) -> Sat1 a a -> Sat1 a b) -> (forall a b c. (a -> b -> c) -> Sat1 a a -> Sat1 a b -> Sat1 a c) -> (forall a b. Sat1 a a -> Sat1 a b -> Sat1 a b) -> (forall a b. Sat1 a a -> Sat1 a b -> Sat1 a a) -> Applicative (Sat1 a) Sat1 a a -> Sat1 a b -> Sat1 a b Sat1 a a -> Sat1 a b -> Sat1 a a Sat1 a (a -> b) -> Sat1 a a -> Sat1 a b (a -> b -> c) -> Sat1 a a -> Sat1 a b -> Sat1 a c forall a. Functor (Sat1 a) forall a. a -> Sat1 a a forall a a. a -> Sat1 a a forall a b. Sat1 a a -> Sat1 a b -> Sat1 a a forall a b. Sat1 a a -> Sat1 a b -> Sat1 a b forall a b. Sat1 a (a -> b) -> Sat1 a a -> Sat1 a b forall a a b. Sat1 a a -> Sat1 a b -> Sat1 a a forall a a b. Sat1 a a -> Sat1 a b -> Sat1 a b forall a a b. Sat1 a (a -> b) -> Sat1 a a -> Sat1 a b forall a b c. (a -> b -> c) -> Sat1 a a -> Sat1 a b -> Sat1 a c forall a a b c. (a -> b -> c) -> Sat1 a a -> Sat1 a b -> Sat1 a c forall (f :: * -> *). Functor f -> (forall a. a -> f a) -> (forall a b. f (a -> b) -> f a -> f b) -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c) -> (forall a b. f a -> f b -> f b) -> (forall a b. f a -> f b -> f a) -> Applicative f <* :: Sat1 a a -> Sat1 a b -> Sat1 a a $c<* :: forall a a b. Sat1 a a -> Sat1 a b -> Sat1 a a *> :: Sat1 a a -> Sat1 a b -> Sat1 a b $c*> :: forall a a b. Sat1 a a -> Sat1 a b -> Sat1 a b liftA2 :: (a -> b -> c) -> Sat1 a a -> Sat1 a b -> Sat1 a c $cliftA2 :: forall a a b c. (a -> b -> c) -> Sat1 a a -> Sat1 a b -> Sat1 a c <*> :: Sat1 a (a -> b) -> Sat1 a a -> Sat1 a b $c<*> :: forall a a b. Sat1 a (a -> b) -> Sat1 a a -> Sat1 a b pure :: a -> Sat1 a a $cpure :: forall a a. a -> Sat1 a a $cp1Applicative :: forall a. Functor (Sat1 a) Applicative, Applicative (Sat1 a) a -> Sat1 a a Applicative (Sat1 a) -> (forall a b. Sat1 a a -> (a -> Sat1 a b) -> Sat1 a b) -> (forall a b. Sat1 a a -> Sat1 a b -> Sat1 a b) -> (forall a. a -> Sat1 a a) -> Monad (Sat1 a) Sat1 a a -> (a -> Sat1 a b) -> Sat1 a b Sat1 a a -> Sat1 a b -> Sat1 a b forall a. Applicative (Sat1 a) forall a. a -> Sat1 a a forall a a. a -> Sat1 a a forall a b. Sat1 a a -> Sat1 a b -> Sat1 a b forall a b. Sat1 a a -> (a -> Sat1 a b) -> Sat1 a b forall a a b. Sat1 a a -> Sat1 a b -> Sat1 a b forall a a b. Sat1 a a -> (a -> Sat1 a b) -> Sat1 a b forall (m :: * -> *). Applicative m -> (forall a b. m a -> (a -> m b) -> m b) -> (forall a b. m a -> m b -> m b) -> (forall a. a -> m a) -> Monad m return :: a -> Sat1 a a $creturn :: forall a a. a -> Sat1 a a >> :: Sat1 a a -> Sat1 a b -> Sat1 a b $c>> :: forall a a b. Sat1 a a -> Sat1 a b -> Sat1 a b >>= :: Sat1 a a -> (a -> Sat1 a b) -> Sat1 a b $c>>= :: forall a a b. Sat1 a a -> (a -> Sat1 a b) -> Sat1 a b $cp1Monad :: forall a. Applicative (Sat1 a) Monad, Monad (Sat1 a) Monad (Sat1 a) -> (forall a. IO a -> Sat1 a a) -> MonadIO (Sat1 a) IO a -> Sat1 a a forall a. Monad (Sat1 a) forall a. IO a -> Sat1 a a forall a a. IO a -> Sat1 a a forall (m :: * -> *). Monad m -> (forall a. IO a -> m a) -> MonadIO m liftIO :: IO a -> Sat1 a a $cliftIO :: forall a a. IO a -> Sat1 a a $cp1MonadIO :: forall a. Monad (Sat1 a) MonadIO) newtype Sat a b c = Sat { Sat a b c -> ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c runSat_ :: ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c } deriving (a -> Sat a b b -> Sat a b a (a -> b) -> Sat a b a -> Sat a b b (forall a b. (a -> b) -> Sat a b a -> Sat a b b) -> (forall a b. a -> Sat a b b -> Sat a b a) -> Functor (Sat a b) forall a b. a -> Sat a b b -> Sat a b a forall a b. (a -> b) -> Sat a b a -> Sat a b b forall a b a b. a -> Sat a b b -> Sat a b a forall a b a b. (a -> b) -> Sat a b a -> Sat a b b forall (f :: * -> *). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f <$ :: a -> Sat a b b -> Sat a b a $c<$ :: forall a b a b. a -> Sat a b b -> Sat a b a fmap :: (a -> b) -> Sat a b a -> Sat a b b $cfmap :: forall a b a b. (a -> b) -> Sat a b a -> Sat a b b Functor, Functor (Sat a b) a -> Sat a b a Functor (Sat a b) -> (forall a. a -> Sat a b a) -> (forall a b. Sat a b (a -> b) -> Sat a b a -> Sat a b b) -> (forall a b c. (a -> b -> c) -> Sat a b a -> Sat a b b -> Sat a b c) -> (forall a b. Sat a b a -> Sat a b b -> Sat a b b) -> (forall a b. Sat a b a -> Sat a b b -> Sat a b a) -> Applicative (Sat a b) Sat a b a -> Sat a b b -> Sat a b b Sat a b a -> Sat a b b -> Sat a b a Sat a b (a -> b) -> Sat a b a -> Sat a b b (a -> b -> c) -> Sat a b a -> Sat a b b -> Sat a b c forall a. a -> Sat a b a forall a b. Functor (Sat a b) forall a b. Sat a b a -> Sat a b b -> Sat a b a forall a b. Sat a b a -> Sat a b b -> Sat a b b forall a b. Sat a b (a -> b) -> Sat a b a -> Sat a b b forall a b a. a -> Sat a b a forall a b c. (a -> b -> c) -> Sat a b a -> Sat a b b -> Sat a b c forall a b a b. Sat a b a -> Sat a b b -> Sat a b a forall a b a b. Sat a b a -> Sat a b b -> Sat a b b forall a b a b. Sat a b (a -> b) -> Sat a b a -> Sat a b b forall a b a b c. (a -> b -> c) -> Sat a b a -> Sat a b b -> Sat a b c forall (f :: * -> *). Functor f -> (forall a. a -> f a) -> (forall a b. f (a -> b) -> f a -> f b) -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c) -> (forall a b. f a -> f b -> f b) -> (forall a b. f a -> f b -> f a) -> Applicative f <* :: Sat a b a -> Sat a b b -> Sat a b a $c<* :: forall a b a b. Sat a b a -> Sat a b b -> Sat a b a *> :: Sat a b a -> Sat a b b -> Sat a b b $c*> :: forall a b a b. Sat a b a -> Sat a b b -> Sat a b b liftA2 :: (a -> b -> c) -> Sat a b a -> Sat a b b -> Sat a b c $cliftA2 :: forall a b a b c. (a -> b -> c) -> Sat a b a -> Sat a b b -> Sat a b c <*> :: Sat a b (a -> b) -> Sat a b a -> Sat a b b $c<*> :: forall a b a b. Sat a b (a -> b) -> Sat a b a -> Sat a b b pure :: a -> Sat a b a $cpure :: forall a b a. a -> Sat a b a $cp1Applicative :: forall a b. Functor (Sat a b) Applicative, Applicative (Sat a b) a -> Sat a b a Applicative (Sat a b) -> (forall a b. Sat a b a -> (a -> Sat a b b) -> Sat a b b) -> (forall a b. Sat a b a -> Sat a b b -> Sat a b b) -> (forall a. a -> Sat a b a) -> Monad (Sat a b) Sat a b a -> (a -> Sat a b b) -> Sat a b b Sat a b a -> Sat a b b -> Sat a b b forall a. a -> Sat a b a forall a b. Applicative (Sat a b) forall a b. Sat a b a -> Sat a b b -> Sat a b b forall a b. Sat a b a -> (a -> Sat a b b) -> Sat a b b forall a b a. a -> Sat a b a forall a b a b. Sat a b a -> Sat a b b -> Sat a b b forall a b a b. Sat a b a -> (a -> Sat a b b) -> Sat a b b forall (m :: * -> *). Applicative m -> (forall a b. m a -> (a -> m b) -> m b) -> (forall a b. m a -> m b -> m b) -> (forall a. a -> m a) -> Monad m return :: a -> Sat a b a $creturn :: forall a b a. a -> Sat a b a >> :: Sat a b a -> Sat a b b -> Sat a b b $c>> :: forall a b a b. Sat a b a -> Sat a b b -> Sat a b b >>= :: Sat a b a -> (a -> Sat a b b) -> Sat a b b $c>>= :: forall a b a b. Sat a b a -> (a -> Sat a b b) -> Sat a b b $cp1Monad :: forall a b. Applicative (Sat a b) Monad, Monad (Sat a b) Monad (Sat a b) -> (forall a. IO a -> Sat a b a) -> MonadIO (Sat a b) IO a -> Sat a b a forall a. IO a -> Sat a b a forall a b. Monad (Sat a b) forall a b a. IO a -> Sat a b a forall (m :: * -> *). Monad m -> (forall a. IO a -> m a) -> MonadIO m liftIO :: IO a -> Sat a b a $cliftIO :: forall a b a. IO a -> Sat a b a $cp1MonadIO :: forall a b. Monad (Sat a b) MonadIO) data SatState a = SatState Solver (Map a Lit) type Watch a = a -> Sat1 a () data Form a = Lit (Signed a) | And [Form a] | Or [Form a] nt :: Form a -> Form a nt :: Form a -> Form a nt (Lit Signed a x) = Signed a -> Form a forall a. Signed a -> Form a Lit (Signed a -> Signed a forall a. Signed a -> Signed a neg Signed a x) nt (And [Form a] xs) = [Form a] -> Form a forall a. [Form a] -> Form a Or ((Form a -> Form a) -> [Form a] -> [Form a] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Form a -> Form a forall a. Form a -> Form a nt [Form a] xs) nt (Or [Form a] xs) = [Form a] -> Form a forall a. [Form a] -> Form a And ((Form a -> Form a) -> [Form a] -> [Form a] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Form a -> Form a forall a. Form a -> Form a nt [Form a] xs) true, false :: Form a true :: Form a true = [Form a] -> Form a forall a. [Form a] -> Form a And [] false :: Form a false = [Form a] -> Form a forall a. [Form a] -> Form a Or [] unique :: [Form a] -> Form a unique :: [Form a] -> Form a unique = [Form a] -> Form a forall a. [Form a] -> Form a u where u :: [Form a] -> Form a u [] = Form a forall a. Form a true u [Form a _] = Form a forall a. Form a true u (Form a x:[Form a] xs) = [Form a] -> Form a forall a. [Form a] -> Form a And [[Form a] -> Form a forall a. [Form a] -> Form a Or [Form a -> Form a forall a. Form a -> Form a nt Form a x, [Form a] -> Form a forall a. [Form a] -> Form a And ((Form a -> Form a) -> [Form a] -> [Form a] forall a b. (a -> b) -> [a] -> [b] map Form a -> Form a forall a. Form a -> Form a nt [Form a] xs)], [Form a] -> Form a u [Form a] xs] runSat :: Ord b => Watch a -> [b] -> Sat a b c -> IO c runSat :: Watch a -> [b] -> Sat a b c -> IO c runSat Watch a w [b] idxs Sat a b c x = [b] -> Map b (SatState a) -> IO c go [b] idxs Map b (SatState a) forall k a. Map k a Map.empty where go :: [b] -> Map b (SatState a) -> IO c go [] Map b (SatState a) m = StateT (Map b (SatState a)) IO c -> Map b (SatState a) -> IO c forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a evalStateT (ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c -> Watch a -> StateT (Map b (SatState a)) IO c forall r (m :: * -> *) a. ReaderT r m a -> r -> m a runReaderT (Sat a b c -> ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c forall a b c. Sat a b c -> ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c runSat_ Sat a b c x) Watch a w) Map b (SatState a) m go (b idx:[b] idxs) Map b (SatState a) m = (Solver -> IO c) -> IO c forall a. (Solver -> IO a) -> IO a withNewSolver ((Solver -> IO c) -> IO c) -> (Solver -> IO c) -> IO c forall a b. (a -> b) -> a -> b $ \Solver s -> [b] -> Map b (SatState a) -> IO c go [b] idxs (b -> SatState a -> Map b (SatState a) -> Map b (SatState a) forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert b idx (Solver -> Map a Lit -> SatState a forall a. Solver -> Map a Lit -> SatState a SatState Solver s Map a Lit forall k a. Map k a Map.empty) Map b (SatState a) m) runSat1 :: Ord a => Watch a -> Sat1 a b -> IO b runSat1 :: Watch a -> Sat1 a b -> IO b runSat1 Watch a w Sat1 a b x = Watch a -> [()] -> Sat a () b -> IO b forall b a c. Ord b => Watch a -> [b] -> Sat a b c -> IO c runSat Watch a w [()] (() -> Sat1 a b -> Sat a () b forall a b c. (Ord a, Ord b) => b -> Sat1 a c -> Sat a b c atIndex () Sat1 a b x) atIndex :: (Ord a, Ord b) => b -> Sat1 a c -> Sat a b c atIndex :: b -> Sat1 a c -> Sat a b c atIndex !b idx Sat1 a c m = do Watch a watch <- ReaderT (Watch a) (StateT (Map b (SatState a)) IO) (Watch a) -> Sat a b (Watch a) forall a b c. ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c -> Sat a b c Sat ReaderT (Watch a) (StateT (Map b (SatState a)) IO) (Watch a) forall (m :: * -> *) r. Monad m => ReaderT r m r ask SatState Solver s Map a Lit ls <- ReaderT (Watch a) (StateT (Map b (SatState a)) IO) (SatState a) -> Sat a b (SatState a) forall a b c. ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c -> Sat a b c Sat (StateT (Map b (SatState a)) IO (SatState a) -> ReaderT (Watch a) (StateT (Map b (SatState a)) IO) (SatState a) forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift ((Map b (SatState a) -> SatState a) -> StateT (Map b (SatState a)) IO (SatState a) forall (m :: * -> *) s a. Monad m => (s -> a) -> StateT s m a gets (SatState a -> b -> Map b (SatState a) -> SatState a forall k a. Ord k => a -> k -> Map k a -> a Map.findWithDefault ([Char] -> SatState a forall a. HasCallStack => [Char] -> a error [Char] "withSolver: index not found") b idx))) (c x, Map a Lit ls') <- IO (c, Map a Lit) -> Sat a b (c, Map a Lit) forall (m :: * -> *) a. MonadIO m => IO a -> m a liftIO (StateT (Map a Lit) IO c -> Map a Lit -> IO (c, Map a Lit) forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s) runStateT (ReaderT (Watch a) (StateT (Map a Lit) IO) c -> Watch a -> StateT (Map a Lit) IO c forall r (m :: * -> *) a. ReaderT r m a -> r -> m a runReaderT (ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) c -> Solver -> ReaderT (Watch a) (StateT (Map a Lit) IO) c forall r (m :: * -> *) a. ReaderT r m a -> r -> m a runReaderT (Sat1 a c -> ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) c forall a b. Sat1 a b -> ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b runSat1_ Sat1 a c m) Solver s) Watch a watch) Map a Lit ls) ReaderT (Watch a) (StateT (Map b (SatState a)) IO) () -> Sat a b () forall a b c. ReaderT (Watch a) (StateT (Map b (SatState a)) IO) c -> Sat a b c Sat (StateT (Map b (SatState a)) IO () -> ReaderT (Watch a) (StateT (Map b (SatState a)) IO) () forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift ((Map b (SatState a) -> Map b (SatState a)) -> StateT (Map b (SatState a)) IO () forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m () modify (b -> SatState a -> Map b (SatState a) -> Map b (SatState a) forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert b idx (Solver -> Map a Lit -> SatState a forall a. Solver -> Map a Lit -> SatState a SatState Solver s Map a Lit ls')))) c -> Sat a b c forall (m :: * -> *) a. Monad m => a -> m a return c x solve :: Ord a => [Signed a] -> Sat1 a Bool solve :: [Signed a] -> Sat1 a Bool solve [Signed a] xs = do Solver s <- ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) Solver -> Sat1 a Solver forall a b. ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b -> Sat1 a b Sat1 ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) Solver forall (m :: * -> *) r. Monad m => ReaderT r m r ask [Lit] ls <- (Signed a -> Sat1 a Lit) -> [Signed a] -> Sat1 a [Lit] forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) mapM Signed a -> Sat1 a Lit forall a. Ord a => Signed a -> Sat1 a Lit lit [Signed a] xs IO Bool -> Sat1 a Bool forall (m :: * -> *) a. MonadIO m => IO a -> m a liftIO (Solver -> [Lit] -> IO Bool MiniSat.solve Solver s [Lit] ls) model :: Ord a => Sat1 a (a -> Bool) model :: Sat1 a (a -> Bool) model = do Solver s <- ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) Solver -> Sat1 a Solver forall a b. ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b -> Sat1 a b Sat1 ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) Solver forall (m :: * -> *) r. Monad m => ReaderT r m r ask Map a Lit m <- ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) (Map a Lit) -> Sat1 a (Map a Lit) forall a b. ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b -> Sat1 a b Sat1 (ReaderT (Watch a) (StateT (Map a Lit) IO) (Map a Lit) -> ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) (Map a Lit) forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (StateT (Map a Lit) IO (Map a Lit) -> ReaderT (Watch a) (StateT (Map a Lit) IO) (Map a Lit) forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift StateT (Map a Lit) IO (Map a Lit) forall (m :: * -> *) s. Monad m => StateT s m s get)) Map a (Maybe Bool) vals <- IO (Map a (Maybe Bool)) -> Sat1 a (Map a (Maybe Bool)) forall (m :: * -> *) a. MonadIO m => IO a -> m a liftIO ((Lit -> IO (Maybe Bool)) -> Map a Lit -> IO (Map a (Maybe Bool)) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse (Solver -> Lit -> IO (Maybe Bool) MiniSat.modelValue Solver s) Map a Lit m) (a -> Bool) -> Sat1 a (a -> Bool) forall (m :: * -> *) a. Monad m => a -> m a return (\a v -> Bool -> Maybe Bool -> Bool forall a. a -> Maybe a -> a fromMaybe Bool False (Maybe Bool -> a -> Map a (Maybe Bool) -> Maybe Bool forall k a. Ord k => a -> k -> Map k a -> a Map.findWithDefault Maybe Bool forall a. Maybe a Nothing a v Map a (Maybe Bool) vals)) modelValue :: Ord a => a -> Sat1 a Bool modelValue :: a -> Sat1 a Bool modelValue a x = do Solver s <- ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) Solver -> Sat1 a Solver forall a b. ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b -> Sat1 a b Sat1 ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) Solver forall (m :: * -> *) r. Monad m => ReaderT r m r ask Lit l <- a -> Sat1 a Lit forall a. Ord a => a -> Sat1 a Lit var a x ~(Just Bool b) <- IO (Maybe Bool) -> Sat1 a (Maybe Bool) forall (m :: * -> *) a. MonadIO m => IO a -> m a liftIO (Solver -> Lit -> IO (Maybe Bool) MiniSat.modelValue Solver s Lit l) Bool -> Sat1 a Bool forall (m :: * -> *) a. Monad m => a -> m a return Bool b addForm :: Ord a => Form a -> Sat1 a () addForm :: Form a -> Sat1 a () addForm Form a f = do Solver s <- ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) Solver -> Sat1 a Solver forall a b. ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b -> Sat1 a b Sat1 ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) Solver forall (m :: * -> *) r. Monad m => ReaderT r m r ask [[Lit]] cs <- Form a -> Sat1 a [[Lit]] forall a. Ord a => Form a -> Sat1 a [[Lit]] flatten Form a f IO [Bool] -> Sat1 a [Bool] forall (m :: * -> *) a. MonadIO m => IO a -> m a liftIO (([Lit] -> IO Bool) -> [[Lit]] -> IO [Bool] forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) mapM (Solver -> [Lit] -> IO Bool MiniSat.addClause Solver s) [[Lit]] cs) () -> Sat1 a () forall (m :: * -> *) a. Monad m => a -> m a return () flatten :: Ord a => Form a -> Sat1 a [[Lit]] flatten :: Form a -> Sat1 a [[Lit]] flatten (Lit Signed a l) = (Lit -> [[Lit]]) -> Sat1 a Lit -> Sat1 a [[Lit]] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ([Lit] -> [[Lit]] forall (m :: * -> *) a. Monad m => a -> m a return ([Lit] -> [[Lit]]) -> (Lit -> [Lit]) -> Lit -> [[Lit]] forall b c a. (b -> c) -> (a -> b) -> a -> c . Lit -> [Lit] forall (m :: * -> *) a. Monad m => a -> m a return) (Signed a -> Sat1 a Lit forall a. Ord a => Signed a -> Sat1 a Lit lit Signed a l) flatten (And [Form a] fs) = ([[[Lit]]] -> [[Lit]]) -> Sat1 a [[[Lit]]] -> Sat1 a [[Lit]] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap [[[Lit]]] -> [[Lit]] forall (t :: * -> *) a. Foldable t => t [a] -> [a] concat ((Form a -> Sat1 a [[Lit]]) -> [Form a] -> Sat1 a [[[Lit]]] forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) mapM Form a -> Sat1 a [[Lit]] forall a. Ord a => Form a -> Sat1 a [[Lit]] flatten [Form a] fs) flatten (Or [Form a] fs) = ([[[Lit]]] -> [[Lit]]) -> Sat1 a [[[Lit]]] -> Sat1 a [[Lit]] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (([[Lit]] -> [Lit]) -> [[[Lit]]] -> [[Lit]] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap [[Lit]] -> [Lit] forall (t :: * -> *) a. Foldable t => t [a] -> [a] concat ([[[Lit]]] -> [[Lit]]) -> ([[[Lit]]] -> [[[Lit]]]) -> [[[Lit]]] -> [[Lit]] forall b c a. (b -> c) -> (a -> b) -> a -> c . [[[Lit]]] -> [[[Lit]]] forall (t :: * -> *) (m :: * -> *) a. (Traversable t, Monad m) => t (m a) -> m (t a) sequence) ((Form a -> Sat1 a [[Lit]]) -> [Form a] -> Sat1 a [[[Lit]]] forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) mapM Form a -> Sat1 a [[Lit]] forall a. Ord a => Form a -> Sat1 a [[Lit]] flatten [Form a] fs) lit :: Ord a => Signed a -> Sat1 a Lit lit :: Signed a -> Sat1 a Lit lit (Pos a x) = a -> Sat1 a Lit forall a. Ord a => a -> Sat1 a Lit var a x lit (Neg a x) = (Lit -> Lit) -> Sat1 a Lit -> Sat1 a Lit forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r liftM Lit -> Lit MiniSat.neg (a -> Sat1 a Lit forall a. Ord a => a -> Sat1 a Lit var a x) var :: Ord a => a -> Sat1 a Lit var :: a -> Sat1 a Lit var a x = do Solver s <- ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) Solver -> Sat1 a Solver forall a b. ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b -> Sat1 a b Sat1 ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) Solver forall (m :: * -> *) r. Monad m => ReaderT r m r ask Map a Lit m <- ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) (Map a Lit) -> Sat1 a (Map a Lit) forall a b. ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b -> Sat1 a b Sat1 (ReaderT (Watch a) (StateT (Map a Lit) IO) (Map a Lit) -> ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) (Map a Lit) forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (StateT (Map a Lit) IO (Map a Lit) -> ReaderT (Watch a) (StateT (Map a Lit) IO) (Map a Lit) forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift StateT (Map a Lit) IO (Map a Lit) forall (m :: * -> *) s. Monad m => StateT s m s get)) case a -> Map a Lit -> Maybe Lit forall k a. Ord k => k -> Map k a -> Maybe a Map.lookup a x Map a Lit m of Maybe Lit Nothing -> do Lit l <- IO Lit -> Sat1 a Lit forall (m :: * -> *) a. MonadIO m => IO a -> m a liftIO (Solver -> IO Lit MiniSat.newLit Solver s) ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) () -> Sat1 a () forall a b. ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b -> Sat1 a b Sat1 (ReaderT (Watch a) (StateT (Map a Lit) IO) () -> ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) () forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (StateT (Map a Lit) IO () -> ReaderT (Watch a) (StateT (Map a Lit) IO) () forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (Map a Lit -> StateT (Map a Lit) IO () forall (m :: * -> *) s. Monad m => s -> StateT s m () put (a -> Lit -> Map a Lit -> Map a Lit forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert a x Lit l Map a Lit m)))) Watch a w <- ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) (Watch a) -> Sat1 a (Watch a) forall a b. ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) b -> Sat1 a b Sat1 (ReaderT (Watch a) (StateT (Map a Lit) IO) (Watch a) -> ReaderT Solver (ReaderT (Watch a) (StateT (Map a Lit) IO)) (Watch a) forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift ReaderT (Watch a) (StateT (Map a Lit) IO) (Watch a) forall (m :: * -> *) r. Monad m => ReaderT r m r ask) Watch a w a x Lit -> Sat1 a Lit forall (m :: * -> *) a. Monad m => a -> m a return Lit l Just Lit l -> Lit -> Sat1 a Lit forall (m :: * -> *) a. Monad m => a -> m a return Lit l