{-# 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
    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
    setPrimArray levels 0 size zeroLevel

newLevels :: Int -> ST s (Levels s)
newLevels :: forall s. Int -> ST s (Levels s)
newLevels Int
size = do
    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
    setPrimArray levels 0 size zeroLevel
    return (Levels 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
    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 -> Int
nextPowerOf2 (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
oldCapacity Int
newCapacity)
    if capacity <= oldCapacity
    then return levels
    else do
        new <- newPrimArray capacity
        setPrimArray new 0 capacity zeroLevel
        return (Levels new)