{-# LANGUAGE LambdaCase #-}
module PureSAT.Satisfied where
import PureSAT.Base
import PureSAT.LitVar
import PureSAT.Clause2
import PureSAT.LBool
import PureSAT.PartialAssignment
import PureSAT.Prim
data Satisfied_
= Satisfied_
| Conflicting_
| Unit_ !Lit
| Unresolved_ !Lit !Lit
deriving Int -> Satisfied_ -> ShowS
[Satisfied_] -> ShowS
Satisfied_ -> String
(Int -> Satisfied_ -> ShowS)
-> (Satisfied_ -> String)
-> ([Satisfied_] -> ShowS)
-> Show Satisfied_
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Satisfied_ -> ShowS
showsPrec :: Int -> Satisfied_ -> ShowS
$cshow :: Satisfied_ -> String
show :: Satisfied_ -> String
$cshowList :: [Satisfied_] -> ShowS
showList :: [Satisfied_] -> ShowS
Show
{-# INLINE satisfied2_ #-}
satisfied2_ :: PartialAssignment s -> Clause2 -> (Satisfied_ -> ST s r) -> ST s r
satisfied2_ :: forall s r.
PartialAssignment s -> Clause2 -> (Satisfied_ -> ST s r) -> ST s r
satisfied2_ !PartialAssignment s
pa !(MkClause2 Bool
_ Lit
l1 Lit
l2 PrimArray Lit
ls) Satisfied_ -> ST s r
kont = ST s r
go0
where
!len :: Int
len = PrimArray Lit -> Int
forall a. Prim a => PrimArray a -> Int
sizeofPrimArray PrimArray Lit
ls
go0 :: ST s r
go0 = Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l1 PartialAssignment s
pa ST s LBool -> (LBool -> ST s r) -> ST s r
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
LBool
LUndef -> ST s r
go1
LBool
LTrue -> Satisfied_ -> ST s r
kont Satisfied_
Satisfied_
LBool
LFalse -> ST s r
go2
go1 :: ST s r
go1 = Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l2 PartialAssignment s
pa ST s LBool -> (LBool -> ST s r) -> ST s r
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
LBool
LUndef -> Lit -> Lit -> Int -> ST s r
goTwo Lit
l1 Lit
l2 Int
0
LBool
LTrue -> Satisfied_ -> ST s r
kont Satisfied_
Satisfied_
LBool
LFalse -> Lit -> Int -> ST s r
goOne Lit
l1 Int
0
go2 :: ST s r
go2 = Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l2 PartialAssignment s
pa ST s LBool -> (LBool -> ST s r) -> ST s r
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
LBool
LUndef -> Lit -> Int -> ST s r
goOne Lit
l2 Int
0
LBool
LTrue -> Satisfied_ -> ST s r
kont Satisfied_
Satisfied_
LBool
LFalse -> Int -> ST s r
goNone Int
0
goNone :: Int -> ST s r
goNone !Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
len
= Satisfied_ -> ST s r
kont Satisfied_
Conflicting_
| Bool
otherwise
, let !l :: Lit
l = PrimArray Lit -> Int -> Lit
forall a. (HasCallStack, Prim a) => PrimArray a -> Int -> a
indexPrimArray PrimArray Lit
ls Int
i
= Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l PartialAssignment s
pa ST s LBool -> (LBool -> ST s r) -> ST s r
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
LBool
LUndef -> Lit -> Int -> ST s r
goOne Lit
l (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
LBool
LTrue -> Satisfied_ -> ST s r
kont Satisfied_
Satisfied_
LBool
LFalse -> Int -> ST s r
goNone (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
goOne :: Lit -> Int -> ST s r
goOne !Lit
k1 !Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
len
= Satisfied_ -> ST s r
kont (Satisfied_ -> ST s r) -> Satisfied_ -> ST s r
forall a b. (a -> b) -> a -> b
$! Lit -> Satisfied_
Unit_ Lit
k1
| Bool
otherwise
, let !l :: Lit
l = PrimArray Lit -> Int -> Lit
forall a. (HasCallStack, Prim a) => PrimArray a -> Int -> a
indexPrimArray PrimArray Lit
ls Int
i
= Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l PartialAssignment s
pa ST s LBool -> (LBool -> ST s r) -> ST s r
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
LBool
LUndef -> Lit -> Lit -> Int -> ST s r
goTwo Lit
k1 Lit
l (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
LBool
LTrue -> Satisfied_ -> ST s r
kont Satisfied_
Satisfied_
LBool
LFalse -> Lit -> Int -> ST s r
goOne Lit
k1 (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
goTwo :: Lit -> Lit -> Int -> ST s r
goTwo !Lit
k1 !Lit
k2 !Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
len
= Satisfied_ -> ST s r
kont (Satisfied_ -> ST s r) -> Satisfied_ -> ST s r
forall a b. (a -> b) -> a -> b
$! Lit -> Lit -> Satisfied_
Unresolved_ Lit
k1 Lit
k2
| Bool
otherwise
, let !l :: Lit
l = PrimArray Lit -> Int -> Lit
forall a. (HasCallStack, Prim a) => PrimArray a -> Int -> a
indexPrimArray PrimArray Lit
ls Int
i
= Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l PartialAssignment s
pa ST s LBool -> (LBool -> ST s r) -> ST s r
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
LBool
LUndef -> Lit -> Lit -> Int -> ST s r
goTwo Lit
k1 Lit
k2 (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
LBool
LTrue -> Satisfied_ -> ST s r
kont Satisfied_
Satisfied_
LBool
LFalse -> Lit -> Lit -> Int -> ST s r
goTwo Lit
k1 Lit
k2 (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)