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

--------------------------------------------------------------------------------