foobar

sat-simple-pure/DPLL.hs

@@ -20,8 +20,8 @@ module DPLL (
 import Control.Monad            (forM_)
 import Control.Monad.ST         (ST)
 import Data.Bits
+import Data.Functor             ((<&>))
 import Data.IntSet              (IntSet)
-import Data.Maybe               (fromMaybe)
 import Data.Primitive.Array
 import Data.Primitive.ByteArray
 import Data.Primitive.PrimArray
@@ -73,6 +73,13 @@ varToLit (MkVar x) = MkLit (var_to_lit x)
 var_to_lit :: Int -> Int
 var_to_lit l = unsafeShiftL l 1
 
+-------------------------------------------------------------------------------
+-- LBool
+-------------------------------------------------------------------------------
+
+data LBool = LFalse | LTrue | LUndef
+  deriving (Eq, Ord, Show)
+
 -------------------------------------------------------------------------------
 -- Partial Assignment
 -------------------------------------------------------------------------------
@@ -99,15 +106,16 @@ extendPartialAssignment (PA ref) = do
     writeByteArray arr' size (0xff :: Word8)
     writeUSTRef ref arr#
 
-lookupPartialAssignment :: Lit -> PartialAssignment s -> ST s (Maybe Bool)
+lookupPartialAssignment :: Lit -> PartialAssignment s -> ST s LBool
 lookupPartialAssignment (MkLit l) (PA ref) = do
     Lift arr <- readUSTRef ref
     readByteArray @Word8 (MutableByteArray arr) (lit_to_var l) >>= \case
-        0x0 -> return (Just (not y))
-        0x1 -> return (Just y)
-        _   -> return Nothing
+        0x0 -> return (if y then LFalse else LTrue)
+        0x1 -> return (if y then LTrue else LFalse)
+        _   -> return LUndef
   where
     y = testBit l 0
+    {-# INLINE y #-}
 
 insertPartialAssignment :: Lit -> PartialAssignment s -> ST s ()
 insertPartialAssignment (MkLit l) (PA ref) = do
@@ -185,7 +193,6 @@ insertClauseDB clause@(MkClause2 l1 l2 _) cdb = do
     insertWatch (neg l1) (W l2 clause) cdb
     insertWatch (neg l2) (W l1 clause) cdb
 
-{-# SCC insertWatch #-}
 insertWatch :: Lit -> Watch -> ClauseDB s -> ST s ()
 insertWatch (MkLit l) !w (CDB cdb) = do
     ws  <- readArray cdb l
@@ -213,21 +220,21 @@ satisfied :: PartialAssignment s -> Clause -> ST s Satisfied
 satisfied pa = go0 where
     go0 []     = return Conflicting
     go0 (l:ls) = lookupPartialAssignment l pa >>= \case
-        Nothing    -> go1 l ls
-        Just True  -> return Satisfied
-        Just False -> go0 ls
+        LUndef -> go1 l ls
+        LTrue  -> return Satisfied
+        LFalse -> go0 ls
 
     go1 l1 []     = return (Unit l1)
     go1 l1 (l:ls) = lookupPartialAssignment l pa >>= \case
-        Nothing    -> go2 l1 l [] ls
-        Just True  -> return Satisfied
-        Just False -> go1 l1 ls
+        LUndef -> go2 l1 l [] ls
+        LTrue  -> return Satisfied
+        LFalse -> go1 l1 ls
 
     go2 l1 l2 acc []     = return (Unresolved (MkClause2 l1 l2 (primArrayFromList acc)))
     go2 l1 l2 acc (l:ls) = lookupPartialAssignment l pa >>= \case
-        Nothing    -> go2 l1 l2 (l : acc) ls
-        Just True  -> return Satisfied
-        Just False -> go2 l1 l2 acc ls
+        LUndef -> go2 l1 l2 (l : acc) ls
+        LTrue  -> return Satisfied
+        LFalse -> go2 l1 l2 acc ls
 
 -------------------------------------------------------------------------------
 -- Clause2
@@ -246,25 +253,25 @@ data Satisfied_
 satisfied2_ :: PartialAssignment s -> Clause2 -> ST s Satisfied_
 satisfied2_ pa (MkClause2 l1 l2 ls) = go0
   where
-    len = sizeofPrimArray ls
+    !len = sizeofPrimArray ls
 
     -- initial state
     go0 = lookupPartialAssignment l1 pa >>= \case
-        Nothing    -> go1
-        Just True  -> return Satisfied_
-        Just False -> go2
+        LUndef -> go1
+        LTrue  -> return Satisfied_
+        LFalse -> go2
 
     -- l1 -> Undef
     go1 = lookupPartialAssignment l2 pa >>= \case
-        Nothing    -> goTwo l1 l2 0
-        Just True  -> return Satisfied_
-        Just False -> goOne l1 0
+        LUndef -> goTwo l1 l2 0
+        LTrue  -> return Satisfied_
+        LFalse -> goOne l1 0
 
     -- l1 -> False
     go2 = lookupPartialAssignment l2 pa >>= \case
-        Nothing -> goOne l2 0
-        Just True -> return Satisfied_
-        Just False -> goNone 0
+        LUndef -> goOne l2 0
+        LTrue  -> return Satisfied_
+        LFalse -> goNone 0
 
     goNone i
         | i >= len
@@ -273,9 +280,9 @@ satisfied2_ pa (MkClause2 l1 l2 ls) = go0
         | otherwise
         , let !l = indexPrimArray ls i
         = lookupPartialAssignment l pa >>= \case
-            Nothing    -> goOne l (i + 1)
-            Just True  -> return Satisfied_
-            Just False -> goNone (i + 1)
+            LUndef -> goOne l (i + 1)
+            LTrue  -> return Satisfied_
+            LFalse -> goNone (i + 1)
 
     goOne k1 i
         | i >= len
@@ -284,9 +291,9 @@ satisfied2_ pa (MkClause2 l1 l2 ls) = go0
         | otherwise
         , let !l = indexPrimArray ls i
         = lookupPartialAssignment l pa >>= \case
-            Nothing    -> goTwo k1 l (i + 1)
-            Just True  -> return Satisfied_
-            Just False -> goOne k1 (i + 1)
+            LUndef -> goTwo k1 l (i + 1)
+            LTrue  -> return Satisfied_
+            LFalse -> goOne k1 (i + 1)
 
     goTwo k1 k2 i
         | i >= len
@@ -295,9 +302,9 @@ satisfied2_ pa (MkClause2 l1 l2 ls) = go0
         | otherwise
         , let !l = indexPrimArray ls i
         = lookupPartialAssignment l pa >>= \case
-            Nothing    -> goTwo k1 k2 (i + 1)
-            Just True  -> return Satisfied_
-            Just False -> goTwo k1 k2 (i + 1)
+            LUndef -> goTwo k1 k2 (i + 1)
+            LTrue  -> return Satisfied_
+            LFalse -> goTwo k1 k2 (i + 1)
 
 -------------------------------------------------------------------------------
 -- Solver
@@ -380,12 +387,12 @@ solveLoop :: ClauseDB s -> Trail -> LitSet -> PartialAssignment s -> VarSet -> S
 solveLoop !clauseDb !trail !units !pa !vars
     | Just (l, units') <- minViewLitSet units
     = lookupPartialAssignment l pa >>= \case
-        Nothing    -> do
+        LUndef -> do
             insertPartialAssignment l pa
             let !vars' = deleteVarSet (litToVar l) vars
             unitPropagate l clauseDb (Deduced l trail) units pa vars'
-        Just True  -> solveLoop clauseDb trail units' pa vars
-        Just False -> backtrack clauseDb trail pa vars
+        LTrue  -> solveLoop clauseDb trail units' pa vars
+        LFalse -> backtrack clauseDb trail pa vars
 
     | Just (v, vars') <- minViewVarSet vars
     = do
@@ -460,6 +467,10 @@ backtrack  clauseDb (Decided l trail) pa vars = do
     insertPartialAssignment (neg l) pa
     unitPropagate (neg l) clauseDb (Deduced (neg l) trail) emptyLitSet pa vars
 
+-------------------------------------------------------------------------------
+-- simplify
+-------------------------------------------------------------------------------
+
 -- | Simplify solver
 simplify :: Solver s -> ST s Bool
 simplify solver@Solver {..} = whenOk ok $ do
@@ -484,10 +495,17 @@ simplifyLoop !acc !pa (c:cs) !vars = satisfied2_ pa c >>= \case
         insertPartialAssignment l pa
         simplifyLoop [] pa (acc ++ cs) (deleteVarSet (litToVar l) vars)
 
+-------------------------------------------------------------------------------
+-- queries
+-------------------------------------------------------------------------------
+
 -- | Lookup model value
 modelValue :: Solver s -> Lit -> ST s Bool
 modelValue Solver {..} l = do
-    fromMaybe False <$> lookupPartialAssignment l solution
+    lookupPartialAssignment l solution <&> \case
+        LUndef -> False
+        LTrue  -> True
+        LFalse -> False
 
 -------------------------------------------------------------------------------
 -- utilities