{-# 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