module Jukebox.Sat.ThreeValued where
import Jukebox.Sat
data Lit3 = Lit3{ Lit3 -> Lit
isFalse :: Lit, Lit3 -> Lit
isTrue :: Lit }
false3, true3, bottom3 :: Lit3
false3 :: Lit3
false3 = Lit -> Lit -> Lit3
Lit3 Lit
true Lit
false
true3 :: Lit3
true3 = Lit3 -> Lit3
neg3 Lit3
false3
bottom3 :: Lit3
bottom3 = Lit -> Lit -> Lit3
Lit3 Lit
false Lit
false
neg3 :: Lit3 -> Lit3
neg3 :: Lit3 -> Lit3
neg3 (Lit3 Lit
f Lit
t) = Lit -> Lit -> Lit3
Lit3 Lit
t Lit
f
newLit3 :: SatSolver s => s -> IO Lit3
newLit3 :: s -> IO Lit3
newLit3 s
s =
do Lit
a <- s -> IO Lit
forall s. SatSolver s => s -> IO Lit
newLit s
s
Lit
b <- s -> IO Lit
forall s. SatSolver s => s -> IO Lit
newLit s
s
s -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> IO ()
addClause s
s [Lit -> Lit
neg Lit
a, Lit -> Lit
neg Lit
b]
Lit3 -> IO Lit3
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit -> Lit -> Lit3
Lit3 Lit
a Lit
b)
newLit2 :: SatSolver s => s -> IO Lit3
newLit2 :: s -> IO Lit3
newLit2 s
s =
do Lit
a <- s -> IO Lit
forall s. SatSolver s => s -> IO Lit
newLit s
s
Lit3 -> IO Lit3
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit -> Lit -> Lit3
Lit3 Lit
a (Lit -> Lit
neg Lit
a))
modelValue3 :: SatSolver s => s -> Lit3 -> IO (Maybe Bool)
modelValue3 :: s -> Lit3 -> IO (Maybe Bool)
modelValue3 s
s = (Lit -> IO (Maybe Bool)) -> Lit3 -> IO (Maybe Bool)
val3 (s -> Lit -> IO (Maybe Bool)
forall s. SatSolver s => s -> Lit -> IO (Maybe Bool)
modelValue s
s)
value3 :: SatSolver s => s -> Lit3 -> IO (Maybe Bool)
value3 :: s -> Lit3 -> IO (Maybe Bool)
value3 s
s = (Lit -> IO (Maybe Bool)) -> Lit3 -> IO (Maybe Bool)
val3 (s -> Lit -> IO (Maybe Bool)
forall s. SatSolver s => s -> Lit -> IO (Maybe Bool)
value s
s)
val3 :: (Lit -> IO (Maybe Bool)) -> Lit3 -> IO (Maybe Bool)
val3 :: (Lit -> IO (Maybe Bool)) -> Lit3 -> IO (Maybe Bool)
val3 Lit -> IO (Maybe Bool)
get (Lit3 Lit
f Lit
t) =
do Maybe Bool
mf <- Lit -> IO (Maybe Bool)
get Lit
f
case Maybe Bool
mf of
Just Bool
True -> do Maybe Bool -> IO (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False)
Maybe Bool
_ -> do Maybe Bool
mt <- Lit -> IO (Maybe Bool)
get Lit
t
case Maybe Bool
mt of
Just Bool
True -> Maybe Bool -> IO (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True)
Maybe Bool
_ -> Maybe Bool -> IO (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
forall a. Maybe a
Nothing