module PureSAT.Clause2 where
import PureSAT.Base
import PureSAT.LitVar
import PureSAT.Prim
data Clause2 = MkClause2 !Bool {-# UNPACK #-} !Lit {-# UNPACK #-} !Lit {-# UNPACK #-} !(PrimArray Lit)
instance Show Clause2 where
showsPrec :: Int -> Clause2 -> ShowS
showsPrec Int
d (MkClause2 Bool
flags Lit
l1 Lit
l2 PrimArray Lit
ls) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"cl " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ShowS
forall a. Show a => a -> ShowS
shows Bool
flags ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Lit] -> ShowS
forall a. Show a => a -> ShowS
shows (Lit
l1 Lit -> [Lit] -> [Lit]
forall a. a -> [a] -> [a]
: Lit
l2 Lit -> [Lit] -> [Lit]
forall a. a -> [a] -> [a]
: PrimArray Lit -> [Lit]
forall a. Prim a => PrimArray a -> [a]
primArrayToList PrimArray Lit
ls)
litInClause :: Lit -> Clause2 -> Bool
litInClause :: Lit -> Clause2 -> Bool
litInClause Lit
l (MkClause2 Bool
_ Lit
l1 Lit
l2 PrimArray Lit
ls) =
Lit
l Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
l1 Bool -> Bool -> Bool
|| Lit
l Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
l2 Bool -> Bool -> Bool
|| (Lit -> Bool -> Bool) -> Bool -> PrimArray Lit -> Bool
forall a b. Prim a => (a -> b -> b) -> b -> PrimArray a -> b
foldrPrimArray (\Lit
l' Bool
next -> Lit
l' Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
l Bool -> Bool -> Bool
|| Bool
next) Bool
False PrimArray Lit
ls
isBinaryClause2 :: Clause2 -> Bool
isBinaryClause2 :: Clause2 -> Bool
isBinaryClause2 (MkClause2 Bool
_ Lit
_ Lit
_ PrimArray Lit
ls) = PrimArray Lit -> Int
forall a. Prim a => PrimArray a -> Int
sizeofPrimArray PrimArray Lit
ls Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
forLitInClause2_ :: Clause2 -> (Lit -> ST s ()) -> ST s ()
forLitInClause2_ :: forall s. Clause2 -> (Lit -> ST s ()) -> ST s ()
forLitInClause2_ (MkClause2 Bool
_ Lit
l1 Lit
l2 PrimArray Lit
ls) Lit -> ST s ()
f = do
Lit -> ST s ()
f Lit
l1
Lit -> ST s ()
f Lit
l2
Int -> ST s ()
forLitInClause2Go Int
0
where
!sz :: Int
sz = PrimArray Lit -> Int
forall a. Prim a => PrimArray a -> Int
sizeofPrimArray PrimArray Lit
ls
forLitInClause2Go :: Int -> ST s ()
forLitInClause2Go !Int
i = Bool -> ST s () -> ST s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
sz) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ Lit -> ST s ()
f (PrimArray Lit -> Int -> Lit
forall a. (HasCallStack, Prim a) => PrimArray a -> Int -> a
indexPrimArray PrimArray Lit
ls Int
i) ST s () -> ST s () -> ST s ()
forall a b. ST s a -> ST s b -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> ST s ()
forLitInClause2Go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
{-# INLINE forLitInClause2_ #-}
nullClause :: Clause2
nullClause :: Clause2
nullClause = Bool -> Lit -> Lit -> PrimArray Lit -> Clause2
MkClause2 Bool
False (Int -> Lit
MkLit Int
1) (Int -> Lit
MkLit Int
1) PrimArray Lit
forall a. PrimArray a
emptyPrimArray
isNullClause :: Clause2 -> Bool
isNullClause :: Clause2 -> Bool
isNullClause (MkClause2 Bool
_ Lit
l1 Lit
l2 PrimArray Lit
_) = Lit
l1 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
l2
sizeofClause2 :: Clause2 -> Int
sizeofClause2 :: Clause2 -> Int
sizeofClause2 (MkClause2 Bool
_ Lit
_ Lit
_ PrimArray Lit
ls) = PrimArray Lit -> Int
forall a. Prim a => PrimArray a -> Int
sizeofPrimArray PrimArray Lit
ls Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2