vec

sat-simple-pure/DPLL.hs

@@ -29,8 +29,8 @@ import Data.Primitive.Types     (Prim)
 import Data.STRef
 import Data.Word                (Word8)
 
-import UnliftedSTRef
 import Lifted
+import UnliftedSTRef
 import Vec
 
 import qualified Data.IntSet as IntSet
@@ -196,11 +196,6 @@ lookupClauseDB :: Lit -> ClauseDB s -> ST s (Vec s Watch)
 lookupClauseDB (MkLit l) (CDB arr) = do
     readArray arr l
 
-clearClauseDB :: Lit -> ClauseDB s -> ST s ()
-clearClauseDB (MkLit l) (CDB arr) = do
-    ws <- readArray arr l
-    clearVec ws
-
 -------------------------------------------------------------------------------
 -- Clause
 -------------------------------------------------------------------------------
@@ -407,39 +402,50 @@ solveLoop !clauseDb !trail !units !pa !vars
 unitPropagate :: forall s. Lit -> ClauseDB s -> Trail -> LitSet -> PartialAssignment s -> VarSet -> ST s Bool
 unitPropagate !l !clauseDb !trail !units !pa !vars = do
     -- traceM $ "unitPropagate " ++ show (l, _sizeClauseDB clauseDb)
-    watches <- lookupClauseDB l clauseDb >>= freezeVec
-    clearClauseDB l clauseDb
-    go units watches 0 (sizeofArray watches)
+    watches <- lookupClauseDB l clauseDb
+    size <- sizeofVec watches
+    go units watches 0 0 size
   where
-    go :: LitSet -> Array Watch -> Int -> Int -> ST s Bool
-    go !us watches i size
+    go :: LitSet -> Vec s Watch -> Int -> Int -> Int -> ST s Bool
+    go !us watches i j size
         | i >= size
-        = solveLoop clauseDb trail us pa vars
+        = do
+            shrinkVec watches j
+            solveLoop clauseDb trail us pa vars
 
         | otherwise
-        , w@(W l' c) <- indexArray watches i
-        = satisfied2_ pa c >>= \case
+        = readVec watches i >>= \ w@(W l' c) -> satisfied2_ pa c >>= \case
             Conflicting_      -> do
-                insertWatch l w clauseDb
-                forM_ [i + 1 .. size - 1] $ \j ->
-                    insertWatch l (indexArray watches j) clauseDb
+                writeVec watches j w
+
+                let copy i' j' =
+                        if i' < size
+                        then do
+                            w' <- readVec watches i'
+                            writeVec watches j' w'
+                            copy (i' + 1) (j' + 1)
+
+                        else shrinkVec watches j'
+
+                copy (i + 1) (j + 1)
+
                 backtrack clauseDb trail pa vars
             Satisfied_        -> do
-                insertWatch l w clauseDb
-                go us watches (i + 1) size
+                writeVec watches j w
+                go us watches (i + 1) (j + 1) size
             Unit_ u           -> do
-                insertWatch l w clauseDb
-                go (insertLitSet u us) watches (i + 1) size
+                writeVec watches j w
+                go (insertLitSet u us) watches (i + 1) (j + 1) size
             Unresolved_ l1 l2
                 | l2 /= l'
                 -> do
                     insertWatch (neg l2) w clauseDb
-                    go us watches (i + 1) size
+                    go us watches (i + 1) j size
 
                 | l1 /= l'
                 -> do
                     insertWatch (neg l1) w clauseDb
-                    go us watches (i + 1) size
+                    go us watches (i + 1) j size
 
                 | otherwise
                 -> error ("watch" ++ show (l1, l2, l'))

sat-simple-pure/Vec.hs

@@ -6,7 +6,7 @@ import Data.STRef
 import Data.Primitive.Array
 import Unsafe.Coerce (unsafeCoerce)
 
-data Vec s a = Vec !(STRef s Int) !(MutableArray s a)
+data Vec s a = Vec {-# UNPACK #-} !(STRef s Int) {-# UNPACK #-} !(MutableArray s a)
 
 newVec
     :: Int             -- ^ capacity
@@ -22,6 +22,11 @@ unused = unsafeCoerce ()
 sizeofVec :: Vec s a -> ST s Int
 sizeofVec (Vec size _) = readSTRef size
 
+-- | Insert at the end: @push_back@
+--
+-- The new vector may be returned.
+-- The vec is done such way, as we use it in mutable context already,
+-- so we don't need an extra STRef.
 insertVec :: Vec s a -> a -> ST s (Vec s a)
 insertVec vec@(Vec sizeRef arr) x = do
     size <- readSTRef sizeRef
@@ -57,9 +62,3 @@ shrinkVec (Vec sizeRef arr) newSize = do
     size <- readSTRef sizeRef
     forM_ [newSize .. size - 1] $ \i -> writeArray arr i unused
     writeSTRef sizeRef newSize
-
--- | TODO: don't use me
-freezeVec :: Vec s a -> ST s (Array a)
-freezeVec (Vec sizeRef arr) = do
-    size <- readSTRef sizeRef
-    freezeArray arr 0 size