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

    -- initial state
    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

    -- l1 -> Undef
    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

    -- l1 -> False
    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)