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
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)