module PureSAT.Stats (
Stats,
newStats,
readStatsConflicts, incrStatsConflicts,
readStatsRestarts, incrStatsRestarts,
readStatsLearnt, incrStatsLearnt,
readStatsClauses, incrStatsClauses,
readStatsLearntLiterals, incrStatsLearntLiterals,
) where
import PureSAT.Base
import PureSAT.Prim
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
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
setPrimArray arr 0 size 0
return 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
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
writePrimArray arr i (x + 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
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
writePrimArray arr i (x + n)