module PureSAT.Stats (
    Stats,
    newStats,
    readStatsConflicts, incrStatsConflicts,
    readStatsRestarts, incrStatsRestarts,
    readStatsLearnt, incrStatsLearnt,
    readStatsClauses, incrStatsClauses,
    readStatsLearntLiterals, incrStatsLearntLiterals,
) where

import PureSAT.Base
import PureSAT.Prim

-------------------------------------------------------------------------------
-- Stats
-------------------------------------------------------------------------------

data Stats s = MkStats (MutablePrimArray s Int)

newStats :: ST s (Stats s)
newStats :: forall s. ST s (Stats s)
newStats = MutablePrimArray s Int -> Stats s
forall s. MutablePrimArray s Int -> Stats s
MkStats (MutablePrimArray s Int -> Stats s)
-> ST s (MutablePrimArray s Int) -> ST s (Stats s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    MutablePrimArray s Int
arr <- Int -> ST s (MutablePrimArray (PrimState (ST s)) Int)
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
Int -> m (MutablePrimArray (PrimState m) a)
newPrimArray Int
size
    MutablePrimArray s Int -> Int -> Int -> Int -> ST s ()
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> Int -> a -> ST s ()
setPrimArray MutablePrimArray s Int
arr Int
0 Int
size Int
0
    MutablePrimArray s Int -> ST s (MutablePrimArray s Int)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return MutablePrimArray s Int
arr
  where
    size :: Int
size = Int
5

readStatsConflicts :: Stats s -> ST s Int
incrStatsConflicts :: Stats s -> ST s ()
(Stats s -> ST s Int
readStatsConflicts, Stats s -> ST s ()
incrStatsConflicts) = Int -> (Stats s -> ST s Int, Stats s -> ST s ())
forall s1 s2. Int -> (Stats s1 -> ST s1 Int, Stats s2 -> ST s2 ())
makeStat Int
0

readStatsRestarts :: Stats s -> ST s Int
incrStatsRestarts :: Stats s -> ST s ()
(Stats s -> ST s Int
readStatsRestarts, Stats s -> ST s ()
incrStatsRestarts) = Int -> (Stats s -> ST s Int, Stats s -> ST s ())
forall s1 s2. Int -> (Stats s1 -> ST s1 Int, Stats s2 -> ST s2 ())
makeStat Int
1

readStatsLearnt :: Stats s -> ST s Int
incrStatsLearnt :: Stats s -> ST s ()
(Stats s -> ST s Int
readStatsLearnt, Stats s -> ST s ()
incrStatsLearnt) = Int -> (Stats s -> ST s Int, Stats s -> ST s ())
forall s1 s2. Int -> (Stats s1 -> ST s1 Int, Stats s2 -> ST s2 ())
makeStat Int
2

readStatsClauses :: Stats s -> ST s Int
incrStatsClauses :: Stats s -> ST s ()
(Stats s -> ST s Int
readStatsClauses, Stats s -> ST s ()
incrStatsClauses) = Int -> (Stats s -> ST s Int, Stats s -> ST s ())
forall s1 s2. Int -> (Stats s1 -> ST s1 Int, Stats s2 -> ST s2 ())
makeStat Int
3

readStatsLearntLiterals :: Stats s -> ST s Int
incrStatsLearntLiterals :: Stats s -> Int -> ST s ()
(Stats s -> ST s Int
readStatsLearntLiterals, Stats s -> Int -> ST s ()
incrStatsLearntLiterals) = Int -> (Stats s -> ST s Int, Stats s -> Int -> ST s ())
forall s1 s2.
Int -> (Stats s1 -> ST s1 Int, Stats s2 -> Int -> ST s2 ())
makeStatBy Int
4

makeStat :: Int -> (Stats s1 -> ST s1 Int, Stats s2 -> ST s2 ())
makeStat :: forall s1 s2. Int -> (Stats s1 -> ST s1 Int, Stats s2 -> ST s2 ())
makeStat Int
i = (Stats s1 -> ST s1 Int
read_, Stats s2 -> ST s2 ()
incr_)
  where
    read_ :: Stats s1 -> ST s1 Int
read_ (MkStats MutablePrimArray s1 Int
arr) = MutablePrimArray s1 Int -> Int -> ST s1 Int
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> ST s a
readPrimArray MutablePrimArray s1 Int
arr Int
i
    incr_ :: Stats s2 -> ST s2 ()
incr_ (MkStats MutablePrimArray s2 Int
arr) = do
        Int
x <- MutablePrimArray s2 Int -> Int -> ST s2 Int
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> ST s a
readPrimArray MutablePrimArray s2 Int
arr Int
i
        MutablePrimArray s2 Int -> Int -> Int -> ST s2 ()
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> a -> ST s ()
writePrimArray MutablePrimArray s2 Int
arr Int
i (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

makeStatBy :: Int -> (Stats s1 -> ST s1 Int, Stats s2 -> Int -> ST s2 ())
makeStatBy :: forall s1 s2.
Int -> (Stats s1 -> ST s1 Int, Stats s2 -> Int -> ST s2 ())
makeStatBy Int
i = (Stats s1 -> ST s1 Int
read_, Stats s2 -> Int -> ST s2 ()
incr_)
  where
    read_ :: Stats s1 -> ST s1 Int
read_ (MkStats MutablePrimArray s1 Int
arr) = MutablePrimArray s1 Int -> Int -> ST s1 Int
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> ST s a
readPrimArray MutablePrimArray s1 Int
arr Int
i
    incr_ :: Stats s2 -> Int -> ST s2 ()
incr_ (MkStats MutablePrimArray s2 Int
arr) !Int
n = do
        Int
x <- MutablePrimArray s2 Int -> Int -> ST s2 Int
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> ST s a
readPrimArray MutablePrimArray s2 Int
arr Int
i
        MutablePrimArray s2 Int -> Int -> Int -> ST s2 ()
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> a -> ST s ()
writePrimArray MutablePrimArray s2 Int
arr Int
i (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)