cherry picking #1 from WIP-1.6.1

src/SAT/Mios.hs

@@ -52,7 +52,7 @@ import SAT.Mios.Validator
 
 -- | version name
 versionId :: String
-versionId = "mios-81 -- https://github.com/shnarazk/mios"
+versionId = "#81 -- https://github.com/shnarazk/mios"
 
 reportElapsedTime :: Bool -> String -> Integer -> IO Integer
 reportElapsedTime False _ 0 = return 0
@@ -73,11 +73,15 @@ executeSolverOn path = executeSolver (miosDefaultOption { _targetFile = Just pat
 -- This is another entry point for standalone programs.
 executeSolver :: MiosProgramOption -> IO ()
 executeSolver opts@(_targetFile -> (Just cnfFile)) = do
-  t0 <- reportElapsedTime False "" $ if _confVerbose opts || 0 <= _confBenchmark opts then -1 else 0
+  solverId <- myThreadId
   (desc, cls) <- parseCNF (_targetFile opts)
   -- when (_numberOfVariables desc == 0) $ error $ "couldn't load " ++ show cnfFile
+  when (_confMaxClauses opts < _numberOfClauses desc) $
+    if -1 == _confBenchmark opts
+      then errorWithoutStackTrace $ "ABORT: too many clauses to solve, " ++ show desc
+      else reportResult opts 0 (Left OutOfMemory) >> killThread solverId
   token <- newEmptyMVar --  :: IO (MVar (Maybe Solver))
-  solverId <- myThreadId
+  t0 <- reportElapsedTime False "" $ if _confVerbose opts || 0 <= _confBenchmark opts then -1 else 0
   handle (\case
              UserInterrupt -> putStrLn "User interrupt recieved."
              ThreadKilled  -> reportResult opts t0 =<< readMVar token
@@ -87,14 +91,14 @@ executeSolver opts@(_targetFile -> (Just cnfFile)) = do
                          threadDelay $ fromMicro * fromIntegral (_confBenchmark opts)
                          putMVar token (Left TimeOut)
                          killThread solverId
-    when (_confMaxSize opts < _numberOfVariables desc) $
-      if -1 == _confBenchmark opts
-        then errorWithoutStackTrace $ "ABORT: too many variables to solve, " ++ show desc
-        else putMVar token (Left OutOfMemory) >> killThread solverId
     s <- newSolver (toMiosConf opts) desc
+    -- ct <- reportElapsedTime True "- making a new solver: " t0
     injectClausesFromCNF s desc cls
     void $ reportElapsedTime (_confVerbose opts) ("## [" ++ showPath cnfFile ++ "] Parse: ") t0
-    when (0 < _confDumpStat opts) $ dumpSolver DumpCSVHeader s
+    -- putMVar token (Left TimeOut)
+    -- killThread solverId
+    -- ct <- reportElapsedTime True "injecting w/ ByteString: " ct
+    when (0 < _confDumpStat opts) $ dumpStats DumpCSVHeader s
     result <- solve s []
     putMVar token result
     killThread solverId
@@ -125,7 +129,7 @@ reportResult opts@(_targetFile -> Just cnfFile) t0 (Right result) = do
     UNSAT t -> do when (_confVerbose opts) $ hPutStrLn stderr "UNSAT" -- contradiction
                   print t
   dumpAssigmentAsCNF (_outputFile opts) result
-  valid <- if _confCheckAnswer opts || 0 <= _confBenchmark opts
+  valid <- if _confCheckAnswer opts -- || 0 <= _confBenchmark opts
            then case result of
                   SAT asg -> do (desc, cls) <- parseCNF (_targetFile opts)
                                 s' <- newSolver (toMiosConf opts) desc
@@ -241,6 +245,13 @@ dumpAssigmentAsCNF (Just fname) (UNSAT _) =
 dumpAssigmentAsCNF (Just fname) (SAT l) =
   withFile fname WriteMode $ \h -> do hPutStrLn h "s SAT"; hPutStrLn h . (++ " 0") . unwords $ map show l
 
+showPath :: FilePath -> String
+showPath str = replicate (len - length basename) ' ' ++ if elem '/' str then basename else basename'
+  where
+    len = 50
+    basename = reverse . takeWhile (/= '/') . reverse $ str
+    basename' = take len str
+
 --------------------------------------------------------------------------------
 -- DIMACS CNF Reader
 --------------------------------------------------------------------------------
@@ -253,37 +264,30 @@ parseCNF target@(Just cnfFile) = do
                       (x, second) -> case B.readInt (skipWhitespace second) of
                                        Just (y, _) -> CNFDescription x y target
       seek :: B.ByteString -> IO (CNFDescription, B.ByteString)
-      seek bs
+      seek !bs
         | B.head bs == 'p' = return (parseP l, B.tail bs')
         | otherwise = seek (B.tail bs')
         where (l, bs') = B.span ('\n' /=) bs
   seek =<< B.readFile cnfFile
 
 -- | parses ByteString then injects the clauses in it into a solver
+{-# INLINABLE injectClausesFromCNF #-}
 injectClausesFromCNF :: Solver -> CNFDescription -> B.ByteString -> IO ()
 injectClausesFromCNF s (CNFDescription nv nc _) bs = do
   let maxLit = int2lit $ negate nv
-  buffer <- newVec (maxLit + 1) 0
-  polvec <- newVec (maxLit + 1) 0
+  buffer <- newVec (maxLit + 1) 0 :: IO (Vec Int)
   let loop :: Int -> B.ByteString -> IO ()
       loop ((< nc) -> False) _ = return ()
-      loop !i !b = loop (i + 1) =<< readClause s buffer polvec b
+      loop !i !b = loop (i + 1) =<< readClause s buffer b
   loop 0 bs
-  -- static polarity
-  let checkPolarity :: Int -> IO ()
-      checkPolarity ((< nv) -> False) = return ()
-      checkPolarity v = do
-        p <- getNth polvec $ var2lit v True
-        if p == LiftedF
-          then setAssign s v p
-          else do n <- getNth polvec $ var2lit v False
-                  when (n == LiftedF) $ setAssign s v p
-        checkPolarity $ v + 1
-  checkPolarity 1
 
 {-# INLINE skipWhitespace #-}
 skipWhitespace :: B.ByteString -> B.ByteString
-skipWhitespace !s = B.dropWhile (`elem` " \t\n") s
+skipWhitespace !s = B.dropWhile (== ' ') {- (`elem` " \t") -} s
+
+{-# INLINE skipWhitespace' #-}
+skipWhitespace' :: B.ByteString -> B.ByteString
+skipWhitespace' !s = B.dropWhile (`elem` " \t\n") s
 
 -- | skip comment lines
 -- __Pre-condition:__ we are on the benngining of a line
@@ -295,41 +299,27 @@ skipComments !s
   where
     c = B.head s
 
-{-# INLINABLE parseInt #-}
+{-# INLINE parseInt #-}
 parseInt :: B.ByteString -> (Int, B.ByteString)
 parseInt !st = do
   let !zero = ord '0'
       loop :: B.ByteString -> Int -> (Int, B.ByteString)
-      loop !s !val = case B.head s of
-        c | '0' <= c && c <= '9'  -> loop (B.tail s) (val * 10 + ord c - zero)
-        _ -> (val, B.tail s)
-  case B.head st of
-    '-' -> let (k, x) = loop (B.tail st) 0 in (negate k, x)
-    '0' -> (0, B.tail st)
---    '+' -> loop st (0 :: Int)
-    _   -> loop st 0
---    c | '0' <= c && c <= '9'  -> loop st 0
---    _ -> error "PARSE ERROR! Unexpected char"
+      loop !s !val = case B.uncons s of
+        Just (c, s') -> if '0' <= c && c <= '9' then loop s' (val * 10 + ord c - zero) else (val, s')
+  case B.uncons st of
+    Just ('-', st') -> let (k, x) = loop st' 0 in (negate k, x)
+    Just ('0', st') -> (0, st')
+    _ -> loop st 0
 
-{-# INLINABLE readClause #-}
-readClause :: Solver -> Stack -> Vec Int -> B.ByteString -> IO B.ByteString
-readClause s buffer bvec stream = do
-  let
-    loop :: Int -> B.ByteString -> IO B.ByteString
-    loop !i !b = case parseInt $ skipWhitespace b of
-                   (0, b') -> do setNth buffer 0 $ i - 1
-                                 sortStack buffer
-                                 void $ addClause s buffer
-                                 return b'
-                   (k, b') -> case int2lit k of
-                                l -> do setNth buffer i l
-                                        setNth bvec l LiftedT
+{-# INLINE readClause #-}
+readClause :: Solver -> Stack {- -> Vec Int -} -> B.ByteString -> IO B.ByteString
+readClause s buffer {- bvec -} stream = do
+  let loop :: Int -> B.ByteString -> IO B.ByteString
+      loop !i !b = case parseInt $ skipWhitespace b of
+                     (k, b') -> if k == 0
+                                then do setNth buffer 0 $ i - 1
+                                        void $ addClause s buffer
+                                        return b'
+                                else do setNth buffer i (int2lit k)
                                         loop (i + 1) b'
-  loop 1 . skipComments . skipWhitespace $ stream
-
-showPath :: FilePath -> String
-showPath str = replicate (len - length basename) ' ' ++ if elem '/' str then basename else basename'
-  where
-    len = 50
-    basename = reverse . takeWhile (/= '/') . reverse $ str
-    basename' = take len str
+  loop 1 . skipComments . skipWhitespace' $ stream

src/SAT/Mios/Criteria.hs

@@ -20,10 +20,14 @@ module SAT.Mios.Criteria
        , lbdOf
          -- * Restart
        , checkRestartCondition
+         -- * Reporting
+       , dumpStats
        )
         where
 
 import Control.Monad (when)
+import Data.List (intercalate)
+import Numeric (showFFloat)
 import SAT.Mios.Types
 import SAT.Mios.Clause
 import SAT.Mios.ClauseManager
@@ -41,7 +45,7 @@ varBumpActivity s@Solver{..} x = do
   a <- (+) <$> getNth activities x <*> get' varInc
   setNth activities x a
   when (varActivityThreshold < a) $ varRescaleActivity s
-  update s x                    -- update the position in heap
+  updateVO s x                    -- update the position in heap
 
 -- | __Fig. 14 (p.19)__
 {-# INLINABLE varDecayActivity #-}
@@ -297,17 +301,17 @@ checkRestartCondition s@Solver{..} (fromIntegral -> lbd) = do
          incrementStat s NumOfGeometricRestart 1
          k' <- getStat s NumOfGeometricRestart
          set' nextRestart (count + floor (fromIntegral step * gef ** fromIntegral k'))
-         when (3 == dumpStat config) $ dumpSolver DumpCSV s
+         when (3 == dumpSolverStatMode config) $ dumpStats DumpCSV s
          return True
      | 1.25 * as < af -> do
          incrementStat s NumOfBlockRestart 1
          set' nextRestart (count + floor (fromIntegral step + gef ** fromIntegral k))
-         when (3 == dumpStat config) $ dumpSolver DumpCSV s
+         when (3 == dumpSolverStatMode config) $ dumpStats DumpCSV s
          return False
      | 1.25 * ds < df -> do
          incrementStat s NumOfRestart 1
          set' nextRestart (count + step)
-         when (3 == dumpStat config) $ dumpSolver DumpCSV s
+         when (3 == dumpSolverStatMode config) $ dumpStats DumpCSV s
          return True
      | otherwise      -> return False
 
@@ -325,3 +329,41 @@ luby y x_ = loop 1 0
       | sz - 1 == x = y ** fromIntegral sq
       | otherwise   = let s = div (sz - 1) 2 in loop2 (mod x s) s (sq - 1)
 -}
+
+-------------------------------------------------------------------------------- dump
+
+emaLabels :: [(String, Solver -> Double')]
+emaLabels = [ ("emaAFast", emaAFast)
+            , ("emaASlow", emaASlow)
+--            , ("emaBDLvl", emaBDLvl)
+--            , ("emaCDLvl", emaCDLvl)
+            , ("emaDFast", emaDFast)
+            , ("emaDSlow", emaDSlow)
+            ]
+
+{-# INLINABLE dumpStats #-}
+-- | print statatistic data to stdio. This should be called after each restart.
+dumpStats :: DumpMode -> Solver -> IO ()
+
+dumpStats NoDump _ = return ()
+
+dumpStats DumpCSVHeader s@Solver{..} = do
+  sts <- init <$> getStats s
+  putStrLn . intercalate "," $ map (show . fst) sts ++ map fst emaLabels
+
+dumpStats DumpCSV s@Solver{..} = do
+  -- update the stat data before dump
+  va <- get' trailLim
+  setStat s NumOfVariable . (nVars -) =<< if va == 0 then get' trail else getNth trailLim 1
+  setStat s NumOfAssigned =<< nAssigns s
+  setStat s NumOfClause =<< get' clauses
+  setStat s NumOfLearnt =<< get' learnts
+  sts <- init <$> getStats s
+  let fs :: (Solver -> Double') -> IO String
+      fs e = do x <- get' (e s)
+                return $ showFFloat (Just 3) x ""
+  vals <- mapM (fs . snd) emaLabels
+  putStrLn . intercalate "," $ map (show . snd) sts ++ vals
+
+-- | FIXME: use Util/Stat
+dumpStats DumpJSON _ = return ()                -- mode 2: JSON

src/SAT/Mios/Main.hs

@@ -16,7 +16,7 @@ module SAT.Mios.Main
        , newSolver
        , setAssign
        , addClause
-       , dumpSolver
+       , dumpStats
          -- * Main function
        , simplifyDB
        , solve
@@ -671,7 +671,7 @@ search s@Solver{..} = do
                   nl <- floor <$> get' maxLearnts
                   when (nl < k1 - k2) $ do
                     reduceDB s    -- Reduce the set of learnt clauses.
-                    when (2 == dumpStat config) $ dumpSolver DumpCSV s
+                    when (2 == dumpSolverStatMode config) $ dumpStats DumpCSV s
                   if | k2 == nVars -> return True     -- Model found
                      | restart -> do                  -- Reached bound on number of conflicts
                          (s `cancelUntil`) =<< get' rootLevel -- force a restart
@@ -690,7 +690,7 @@ search s@Solver{..} = do
 -}
                          loop False
                      | otherwise -> do                -- New variable decision
-                         v <- select s
+                         v <- selectVO s
                          -- #phasesaving <<<<  many have heuristic for polarity here
                          oldVal <- getNth phases v
                          unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@
@@ -733,7 +733,7 @@ solve s@Solver{..} assumps = do
                 toInt v = (\p -> if LiftedT == p then v else negate v) <$> valueVar s v
             asg1 <- mapM toInt [1 .. nVars]
             asg2 <- map lit2int <$> asList conflicts
-            when (0 < dumpStat config) $ dumpSolver DumpCSV s
+            when (0 < dumpSolverStatMode config) $ dumpStats DumpCSV s
             cancelUntil s 0     -- reset solver
             flag <- get' ok
             if | status && flag == LiftedT     -> return $ Right (SAT asg1)