{-# LANGUAGE GeneralizedNewtypeDeriving #-} module PureSAT.Level where import PureSAT.Base import PureSAT.LitVar import PureSAT.Prim import PureSAT.Utils newtype Level = Level Int deriving stock (Level -> Level -> Bool (Level -> Level -> Bool) -> (Level -> Level -> Bool) -> Eq Level forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a $c== :: Level -> Level -> Bool == :: Level -> Level -> Bool $c/= :: Level -> Level -> Bool /= :: Level -> Level -> Bool Eq, Eq Level Eq Level => (Level -> Level -> Ordering) -> (Level -> Level -> Bool) -> (Level -> Level -> Bool) -> (Level -> Level -> Bool) -> (Level -> Level -> Bool) -> (Level -> Level -> Level) -> (Level -> Level -> Level) -> Ord Level Level -> Level -> Bool Level -> Level -> Ordering Level -> Level -> Level forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a $ccompare :: Level -> Level -> Ordering compare :: Level -> Level -> Ordering $c< :: Level -> Level -> Bool < :: Level -> Level -> Bool $c<= :: Level -> Level -> Bool <= :: Level -> Level -> Bool $c> :: Level -> Level -> Bool > :: Level -> Level -> Bool $c>= :: Level -> Level -> Bool >= :: Level -> Level -> Bool $cmax :: Level -> Level -> Level max :: Level -> Level -> Level $cmin :: Level -> Level -> Level min :: Level -> Level -> Level Ord, Int -> Level -> ShowS [Level] -> ShowS Level -> String (Int -> Level -> ShowS) -> (Level -> String) -> ([Level] -> ShowS) -> Show Level forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a $cshowsPrec :: Int -> Level -> ShowS showsPrec :: Int -> Level -> ShowS $cshow :: Level -> String show :: Level -> String $cshowList :: [Level] -> ShowS showList :: [Level] -> ShowS Show) deriving newtype (Addr# -> Int# -> Level ByteArray# -> Int# -> Level Proxy Level -> Int# Level -> Int# (Proxy Level -> Int#) -> (Level -> Int#) -> (Proxy Level -> Int#) -> (Level -> Int#) -> (ByteArray# -> Int# -> Level) -> (forall s. MutableByteArray# s -> Int# -> State# s -> (# State# s, Level #)) -> (forall s. MutableByteArray# s -> Int# -> Level -> State# s -> State# s) -> (forall s. MutableByteArray# s -> Int# -> Int# -> Level -> State# s -> State# s) -> (Addr# -> Int# -> Level) -> (forall s. Addr# -> Int# -> State# s -> (# State# s, Level #)) -> (forall s. Addr# -> Int# -> Level -> State# s -> State# s) -> (forall s. Addr# -> Int# -> Int# -> Level -> State# s -> State# s) -> Prim Level forall s. Addr# -> Int# -> Int# -> Level -> State# s -> State# s forall s. Addr# -> Int# -> State# s -> (# State# s, Level #) forall s. Addr# -> Int# -> Level -> State# s -> State# s forall s. MutableByteArray# s -> Int# -> Int# -> Level -> State# s -> State# s forall s. MutableByteArray# s -> Int# -> State# s -> (# State# s, Level #) forall s. MutableByteArray# s -> Int# -> Level -> State# s -> State# s forall a. (Proxy a -> Int#) -> (a -> Int#) -> (Proxy a -> Int#) -> (a -> Int#) -> (ByteArray# -> Int# -> a) -> (forall s. MutableByteArray# s -> Int# -> State# s -> (# State# s, a #)) -> (forall s. MutableByteArray# s -> Int# -> a -> State# s -> State# s) -> (forall s. MutableByteArray# s -> Int# -> Int# -> a -> State# s -> State# s) -> (Addr# -> Int# -> a) -> (forall s. Addr# -> Int# -> State# s -> (# State# s, a #)) -> (forall s. Addr# -> Int# -> a -> State# s -> State# s) -> (forall s. Addr# -> Int# -> Int# -> a -> State# s -> State# s) -> Prim a $csizeOfType# :: Proxy Level -> Int# sizeOfType# :: Proxy Level -> Int# $csizeOf# :: Level -> Int# sizeOf# :: Level -> Int# $calignmentOfType# :: Proxy Level -> Int# alignmentOfType# :: Proxy Level -> Int# $calignment# :: Level -> Int# alignment# :: Level -> Int# $cindexByteArray# :: ByteArray# -> Int# -> Level indexByteArray# :: ByteArray# -> Int# -> Level $creadByteArray# :: forall s. MutableByteArray# s -> Int# -> State# s -> (# State# s, Level #) readByteArray# :: forall s. MutableByteArray# s -> Int# -> State# s -> (# State# s, Level #) $cwriteByteArray# :: forall s. MutableByteArray# s -> Int# -> Level -> State# s -> State# s writeByteArray# :: forall s. MutableByteArray# s -> Int# -> Level -> State# s -> State# s $csetByteArray# :: forall s. MutableByteArray# s -> Int# -> Int# -> Level -> State# s -> State# s setByteArray# :: forall s. MutableByteArray# s -> Int# -> Int# -> Level -> State# s -> State# s $cindexOffAddr# :: Addr# -> Int# -> Level indexOffAddr# :: Addr# -> Int# -> Level $creadOffAddr# :: forall s. Addr# -> Int# -> State# s -> (# State# s, Level #) readOffAddr# :: forall s. Addr# -> Int# -> State# s -> (# State# s, Level #) $cwriteOffAddr# :: forall s. Addr# -> Int# -> Level -> State# s -> State# s writeOffAddr# :: forall s. Addr# -> Int# -> Level -> State# s -> State# s $csetOffAddr# :: forall s. Addr# -> Int# -> Int# -> Level -> State# s -> State# s setOffAddr# :: forall s. Addr# -> Int# -> Int# -> Level -> State# s -> State# s Prim) instance Enum Level where fromEnum :: Level -> Int fromEnum = Level -> Int forall a b. Coercible a b => a -> b coerce toEnum :: Int -> Level toEnum = Int -> Level forall a b. Coercible a b => a -> b coerce succ :: Level -> Level succ (Level Int l) = Int -> Level Level (Int l Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) pred :: Level -> Level pred (Level Int l) = Int -> Level Level (Int l Int -> Int -> Int forall a. Num a => a -> a -> a - Int 1) zeroLevel :: Level zeroLevel :: Level zeroLevel = Int -> Level Level Int 0 isZeroLevel :: Level -> Bool isZeroLevel :: Level -> Bool isZeroLevel (Level Int n) = Int n Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Int 0 newtype Levels s = Levels (MutablePrimArray s Level) getLevel :: Levels s -> Lit -> ST s Level getLevel :: forall s. Levels s -> Lit -> ST s Level getLevel (Levels MutablePrimArray s Level level) (MkLit Int l) = MutablePrimArray s Level -> Int -> ST s Level forall a s. (HasCallStack, Prim a) => MutablePrimArray s a -> Int -> ST s a readPrimArray MutablePrimArray s Level level (Int -> Int lit_to_var Int l) setLevel :: Levels s -> Lit -> Level -> ST s () setLevel :: forall s. Levels s -> Lit -> Level -> ST s () setLevel (Levels MutablePrimArray s Level levels) (MkLit Int l) Level d = do MutablePrimArray s Level -> Int -> Level -> ST s () forall a s. (HasCallStack, Prim a) => MutablePrimArray s a -> Int -> a -> ST s () writePrimArray MutablePrimArray s Level levels (Int -> Int lit_to_var Int l) Level d clearLevels :: Levels s -> ST s () clearLevels :: forall s. Levels s -> ST s () clearLevels (Levels MutablePrimArray s Level levels) = do Int size <- MutablePrimArray (PrimState (ST s)) Level -> ST s Int forall (m :: * -> *) a. (PrimMonad m, Prim a) => MutablePrimArray (PrimState m) a -> m Int getSizeofMutablePrimArray MutablePrimArray s Level MutablePrimArray (PrimState (ST s)) Level levels MutablePrimArray s Level -> Int -> Int -> Level -> ST s () forall a s. (HasCallStack, Prim a) => MutablePrimArray s a -> Int -> Int -> a -> ST s () setPrimArray MutablePrimArray s Level levels Int 0 Int size Level zeroLevel newLevels :: Int -> ST s (Levels s) newLevels :: forall s. Int -> ST s (Levels s) newLevels Int size = do MutablePrimArray s Level levels <- Int -> ST s (MutablePrimArray (PrimState (ST s)) Level) forall (m :: * -> *) a. (PrimMonad m, Prim a) => Int -> m (MutablePrimArray (PrimState m) a) newPrimArray Int size MutablePrimArray s Level -> Int -> Int -> Level -> ST s () forall a s. (HasCallStack, Prim a) => MutablePrimArray s a -> Int -> Int -> a -> ST s () setPrimArray MutablePrimArray s Level levels Int 0 Int size Level zeroLevel Levels s -> ST s (Levels s) forall a. a -> ST s a forall (m :: * -> *) a. Monad m => a -> m a return (MutablePrimArray s Level -> Levels s forall s. MutablePrimArray s Level -> Levels s Levels MutablePrimArray s Level levels) extendLevels :: Levels s -> Int -> ST s (Levels s) extendLevels :: forall s. Levels s -> Int -> ST s (Levels s) extendLevels levels :: Levels s levels@(Levels MutablePrimArray s Level old) Int newCapacity = do Int oldCapacity <- MutablePrimArray (PrimState (ST s)) Level -> ST s Int forall (m :: * -> *) a. (PrimMonad m, Prim a) => MutablePrimArray (PrimState m) a -> m Int getSizeofMutablePrimArray MutablePrimArray s Level MutablePrimArray (PrimState (ST s)) Level old let capacity :: Int capacity = Int -> Int nextPowerOf2 (Int -> Int -> Int forall a. Ord a => a -> a -> a max Int oldCapacity Int newCapacity) if Int capacity Int -> Int -> Bool forall a. Ord a => a -> a -> Bool <= Int oldCapacity then Levels s -> ST s (Levels s) forall a. a -> ST s a forall (m :: * -> *) a. Monad m => a -> m a return Levels s levels else do MutablePrimArray s Level new <- Int -> ST s (MutablePrimArray (PrimState (ST s)) Level) forall (m :: * -> *) a. (PrimMonad m, Prim a) => Int -> m (MutablePrimArray (PrimState m) a) newPrimArray Int capacity MutablePrimArray s Level -> Int -> Int -> Level -> ST s () forall a s. (HasCallStack, Prim a) => MutablePrimArray s a -> Int -> Int -> a -> ST s () setPrimArray MutablePrimArray s Level new Int 0 Int capacity Level zeroLevel Levels s -> ST s (Levels s) forall a. a -> ST s a forall (m :: * -> *) a. Monad m => a -> m a return (MutablePrimArray s Level -> Levels s forall s. MutablePrimArray s Level -> Levels s Levels MutablePrimArray s Level new)