mios 1.4.0 → 1.5.4

raw patch · 39 files changed

+4423/−3424 lines, 39 filesdep +miosdep +primitivedep ~basedep ~vectornew-component:exe:cnf-statnew-component:exe:mc-averagecsvnew-component:exe:mc-dump2csvnew-component:exe:mc-numbersnew-component:exe:mc-pickupnew-component:exe:mc-stat2csvnew-component:exe:mc-summarynew-component:exe:mios-1.5.4new-component:exe:mios-mcPVP ok

version bump matches the API change (PVP)

Dependencies added: mios, primitive

Dependency ranges changed: base, vector

API changes (from Hackage documentation)

Files

• MultiConflict/utils/averagecsv.hs +13/−0
• MultiConflict/utils/dump2csv.hs +10/−0
• MultiConflict/utils/numbers.hs +119/−0
• MultiConflict/utils/pickup.hs +123/−0
• MultiConflict/utils/stat2csv.hs +10/−0
• MultiConflict/utils/summary.hs +104/−0
• SAT/Mios.hs +0/−293
• SAT/Mios/Clause.hs +0/−145
• SAT/Mios/ClauseManager.hs +0/−234
• SAT/Mios/Main.hs +0/−817
• SAT/Mios/OptionParser.hs +0/−132
• SAT/Mios/Solver.hs +0/−633
• SAT/Mios/Types.hs +0/−257
• SAT/Mios/Util/BoolExp.hs +0/−244
• SAT/Mios/Util/DIMACS.hs +0/−31
• SAT/Mios/Util/DIMACS/MinisatReader.hs +0/−73
• SAT/Mios/Util/DIMACS/Reader.hs +0/−130
• SAT/Mios/Util/DIMACS/Writer.hs +0/−58
• SAT/Mios/Validator.hs +0/−47
• SAT/Mios/Vec.hs +0/−276
• app/mios.hs +12/−8
• mios.cabal +138/−46
• src/SAT/Mios.hs +335/−0
• src/SAT/Mios/Clause.hs +129/−0
• src/SAT/Mios/ClauseManager.hs +293/−0
• src/SAT/Mios/ClausePool.hs +75/−0
• src/SAT/Mios/Criteria.hs +327/−0
• src/SAT/Mios/Main.hs +759/−0
• src/SAT/Mios/OptionParser.hs +145/−0
• src/SAT/Mios/Solver.hs +454/−0
• src/SAT/Mios/Types.hs +337/−0
• src/SAT/Mios/Util/BoolExp.hs +249/−0
• src/SAT/Mios/Util/DIMACS.hs +31/−0
• src/SAT/Mios/Util/DIMACS/MinisatReader.hs +77/−0
• src/SAT/Mios/Util/DIMACS/Reader.hs +143/−0
• src/SAT/Mios/Util/DIMACS/Writer.hs +58/−0
• src/SAT/Mios/Validator.hs +69/−0
• src/SAT/Mios/Vec.hs +359/−0
• utils/cnf-stat.hs +54/−0

@@ -0,0 +1,13 @@+-- | Usage:+-- > mios-averagecsv < a.csv > ave.csv+module Main where++import Data.List (sort)+import SAT.Mios.Util.Stat++main :: IO ()+main = do+  putStrLn $ fst (header :: (String, MergedDump))+  d <- parseBy [(fst (header :: (String, MiosDump)), fromCSV)] <$> getContents+  mapM_ (putStrLn . toCSV) . sort =<< merge d+

@@ -0,0 +1,10 @@+-- | Usage:+-- > mios --dump ... | mios-dump2csv > a.csv+module Main where++import SAT.Mios.Util.Stat++main :: IO ()+main = do+  putStrLn $ fst (header :: (String, MiosDump))+  mapM_ (putStrLn . toCSV) =<< parseBy [("", fromDump)] <$> getContents

@@ -0,0 +1,119 @@+-- | Usage:+-- > mios-summary < average.csv > summary.tbl (for org-mode or github-flavored markdown)+{-# LANGUAGE ViewPatterns #-}+module Main where++import Data.List (intercalate, lookup, minimumBy, nub)+import Data.Maybe (fromMaybe)+import Data.Ord (comparing)+import Numeric (showFFloat)+import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo)+import System.Environment (getArgs)+import SAT.Mios.Types+import SAT.Mios.Util.Stat++data Opt = Opt+  {+    threshold :: Double+  , p1 :: (Double, Double)+  , p2 :: (Double, Double)+  , p3 :: (Int, Int)+  , p4 :: (Int, Int)+  , message :: String+  , help :: Bool+  }++optDefault :: Opt+optDefault = Opt 0 (0, 10) (0, 10) (0, 10) (0, 10) "#-*-mode:org-*-" False++options ::[OptDescr (Opt -> Opt)]+options =+  [+    Option ['t'] ["threshold"]+    (ReqArg (\v c -> c { threshold = read v }) "0.0") "threshold for p1"+  , Option [] ["UF250"]+    (NoArg (\c -> c { threshold = 12109075.01 })) "threshold for UF250; 12109075.01 (7.083)"+  , Option [] ["38bits"]+    (NoArg (\c -> c { threshold = 191761341.00 })) "threshold for 38bits; 191761341.00 (8.283)"+  , Option [] ["44bits"]+    (NoArg (\c -> c { threshold = 5204447789.00 })) "threshold for 44bits; 5204447789.00 (9.716)"+  , Option ['1'] ["p1"]+    (ReqArg (\v c -> c { p1 = read v }) "\"(0,10)\"") "range of p1"+  , Option ['2'] ["p2"]+    (ReqArg (\v c -> c { p2 = read v }) "\"(0,10)\"") "range of p2"+  , Option ['3'] ["p3"]+    (ReqArg (\v c -> c { p3 = read v }) "\"(0,10)\"") "range of p3"+  , Option ['4'] ["p4"]+    (ReqArg (\v c -> c { p4 = read v }) "\"(0,10)\"") "range of p4"+  , Option ['m'] ["message"]+    (ReqArg (\v c -> c { message = undecodeNewline v }) "\"\"") "extra message embeded into output"+  , Option ['h'] ["help"]+    (NoArg (\c -> c { help = True })) "display help message"+  ]++parseOptions :: String -> [String] -> IO Opt+parseOptions mes argv =+    case getOpt Permute options argv of+      (o,  [], []) -> return $ foldl (flip id) optDefault o+      (o,   _, []) -> return $ foldl (flip id) optDefault o+      (_,   _, err) -> ioError (userError (concat err ++ usageInfo mes options))++-- | builds "MiosProgramOption" from a String+parseOptionsFromArgs :: String -> IO Opt+parseOptionsFromArgs mes = parseOptions mes =<< getArgs++undecodeNewline :: String -> String+undecodeNewline [] = []+undecodeNewline [a] = [a]+undecodeNewline ('\\' : 'n' : x) = '\n' : undecodeNewline x+undecodeNewline (a : x) = a : undecodeNewline x++showf :: Double -> String+showf x = showFFloat (Just 2) x ""++main :: IO ()+main = do+  opts <- parseOptionsFromArgs "gp-summary"+  if help opts+    then putStrLn $ usageInfo "" options+    else do putStrLn $ message opts+            putStrLn ""+            putStrLn "| p1   | good | bad |"+            putStrLn "| ---- | ---- | --- |"+            result <- pickup opts . parseBy [(fst (header :: (String, MergedDump)), fromMergedCSV)] <$> getContents+            mapM_ (putStrLn . toString) result+            let ngs = sum $ map (fst . snd) result+                nbs = sum $ map (snd . snd) result+            putStrLn $ intercalate "," [showf (fromIntegral ngs / fromIntegral (ngs + nbs)), show (ngs + nbs) ++ "/" ++ show (ngs, nbs)]++toString :: (Double, (Int, Int))  -> String+toString (p1, (ng, nb)) = "| " ++ intercalate " | " [showf p1, show ng, show nb] ++ " |"++pickup :: Opt -> [MergedDump] -> [(Double, (Int, Int))]+pickup opts l = filter notEmpty $ map gather keys+  where+    notEmpty (_, (0, 0)) = False+    notEmpty _ = True+    thr = threshold opts+    keys = nub $ map (gpParameter1 .  snd. _mergedConf) l+    gather :: Double -> (Double, (Int, Int))+    gather key = (key, (ng, length targets - ng))+      where+        targets' :: [MergedDump]+        targets' = filter ((key ==) . gpParameter1 .  snd. _mergedConf) l+        inBand :: MergedDump -> Bool+        inBand (_mergedConf -> snd -> conf) = c1 && c2 && c3 && c4+          where+            c1 = inPair (p1 opts) (gpParameter1 conf)+            c2 = inPair (p2 opts) (gpParameter2 conf)+            c3 = inPair (p3 opts) (extraParameter3 conf)+            c4 = inPair (p4 opts) (extraParameter4 conf)+            inPair :: (Num a, Ord a) => (a, a) -> a -> Bool+            inPair (b, t) x = b <= x && x <= t+        targets = filter inBand targets'+        ng = length $ filter (< thr) (map value targets)+    value :: MergedDump -> Double+    value m = case lookup PropagationS . (\(MiosStats s) -> s) . _mergedStat $ m of+      Just (Right v) -> fromIntegral v+      Just (Left v)  -> v+      Nothing        -> 10000000

@@ -0,0 +1,123 @@+-- | Usage:+-- > mios-summary < average.csv > summary.tbl (for org-mode or github-flavored markdown)+module Main where++import Data.List (intercalate, lookup, maximumBy, minimumBy, nub)+import Data.Maybe (fromMaybe)+import Data.Ord (comparing)+import Numeric (showFFloat)+import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo)+import System.Environment (getArgs)+import SAT.Mios.Types+import SAT.Mios.Util.Stat++data Opt = Opt+  {+    message :: String+  , useLog :: Bool+  , help :: Bool+  }++optDefault :: Opt+optDefault = Opt "#-*-mode:org-*-" False False++options ::[OptDescr (Opt -> Opt)]+options =+  [+    Option ['m'] ["message"]+    (ReqArg (\v c -> c { message = undecodeNewline v }) "\"string\"") "extra message embeded into output"+  , Option ['l'] ["useLog"]+    (NoArg (\c -> c { useLog = True })) "use Logarithmic value for propagation"+  , Option ['h'] ["help"]+    (NoArg (\c -> c { help = True })) "display help message"+  ]++parseOptions :: String -> [String] -> IO Opt+parseOptions mes argv =+    case getOpt Permute options argv of+      (o,  [], []) -> return $ foldl (flip id) optDefault o+      (o,   _, []) -> return $ foldl (flip id) optDefault o+      (_,   _, err) -> ioError (userError (concat err ++ usageInfo mes options))++-- | builds "MiosProgramOption" from a String+parseOptionsFromArgs :: String -> IO Opt+parseOptionsFromArgs mes = parseOptions mes =<< getArgs++undecodeNewline :: String -> String+undecodeNewline [] = []+undecodeNewline [a] = [a]+undecodeNewline ('\\' : 'n' : x) = '\n' : undecodeNewline x+undecodeNewline (a : x) = a : undecodeNewline x++showf :: Double -> String+showf x = showFFloat (Just 2) x ""++showi :: Int -> String+showi x+  | 3 <= length s = s+  | otherwise = reverse . take 3 . (++ "   ") . reverse $ s+  where s = show x++showl :: Either Double Int -> String+showl (Left x) = showf x+showl (Right x) = showf (fromIntegral x)++main :: IO ()+main = do+  opts <- parseOptionsFromArgs "gp-summary"+  if help opts+    then putStrLn $ usageInfo "" options+    else do let parsers = [ (fst (header :: (String, MiosDump)), toMerge <$> fromCSV)+                          , (fst (header :: (String, MergedDump)), fromMergedCSV)]+            putStrLn $ message opts+            putStrLn ""+            if useLog opts+              then do putStrLn "|   n |   p1 |   p2 |  p3 |  p4 | log(P) | conflict |   learnt | backjump | re-st | rate |  extra | pr/bj |"+                      putStrLn "| --- | ---- | ---- | --- | --- | ------ | -------- | -------- | -------- | ----- | ---- |  ----- | ----- |"+              else do putStrLn "|   n |   p1 |   p2 |  p3 |  p4 | propagation | conflict |   learnt | backjump | re-st | rate |  extra | pr/bj |"+                      putStrLn "| --- | ---- | ---- | --- | --- | ----------- | -------- | -------- | -------- | ----- | ---- |  ----- | ----- |"+            d <- parseBy parsers <$> getContents+            mapM_ (putStrLn . toSummary (useLog opts)) $ pickup True d+            putStrLn ""+            mapM_ (putStrLn . toSummary (useLog opts)) $ pickup False d+            putStrLn ""++toSummary :: Bool -> MergedDump -> String+toSummary uLog (MergedDump (_, MiosConfiguration _ _ p1 p2 p3 p4) n (MiosStats l) _) =+  "| " ++ intercalate " | " [show n, m', s', showf pr] ++ " |"+  where+    m' = intercalate " | " [showf p1, showf p2, showi p3, showi p4]+    s' = intercalate " | " $ map (showl . snd) (convert uLog l) -- (tail . init $ l)+    convert :: Bool -> [DumpedValue] -> [DumpedValue]+    convert uL ks+      | uL = logOf PropagationS : map valOf [ConflictS .. ExtraS]+      | otherwise = map valOf [PropagationS .. ExtraS]+      where+        logOf :: DumpTag -> DumpedValue+        logOf key = (key, Left $ logBase 10 (val key))+        valOf key = (key, Left $ val key)+        val :: DumpTag -> Double+        val key+          | Just (Left x) <- lookup key ks = x+          | Just (Right x) <- lookup key ks = fromIntegral x+          | otherwise = 0+    pr = fromMaybe 0 $ div' <$> lookup PropagationS l <*> lookup BackjumpS l+    div' :: Either Double Int -> Either Double Int -> Double+    div' (Right a) (Right b) = fromIntegral a / fromIntegral b+    div' (Right a) (Left b)  = fromIntegral a / b+    div' (Left a) (Right b)  = a / fromIntegral b+    div' (Left a) (Left b)   = a / b++pickup :: Bool -> [MergedDump] -> [MergedDump]+pickup good l = map selectData keys+  where+    keys = nub $ map (gpParameter1 .  snd. _mergedConf) l+    selectData :: Double -> MergedDump+    selectData key+      | good      = minimumBy (comparing value) $ filter ((key ==) . gpParameter1 .  snd. _mergedConf) l+      | otherwise = maximumBy (comparing value) $ filter ((key ==) . gpParameter1 .  snd. _mergedConf) l+    value :: MergedDump -> Double+    value m = case lookup PropagationS . (\(MiosStats s) -> s) . _mergedStat $ m of+      Just (Right v) -> fromIntegral v+      Just (Left v)  -> v+      Nothing        -> 10000000

@@ -0,0 +1,10 @@+-- | Usage:+-- > mios --stat -X ... | mios-stat2csv > a.csv+module Main where++import SAT.Mios.Util.Stat++main :: IO ()+main = do+  putStrLn $ fst (header :: (String, MiosDump))+  mapM_ (putStrLn . toCSV) =<< parseBy [("", fromStat)] <$> getContents

@@ -0,0 +1,104 @@+-- | Usage:+-- > mios-summary < average.csv > summary.tbl (for org-mode or github-flavored markdown)+module Main where++import Data.List (intercalate, lookup)+import Data.Maybe (fromMaybe)+import Numeric (showFFloat)+import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo)+import System.Environment (getArgs)+import SAT.Mios.Types+import SAT.Mios.Util.Stat++data Opt = Opt+  {+    message :: String+  , useLog :: Bool+  , help :: Bool+  }++optDefault :: Opt+optDefault = Opt "#-*-mode:org-*-" False False++options ::[OptDescr (Opt -> Opt)]+options =+  [+    Option ['m'] ["message"]+    (ReqArg (\v c -> c { message = undecodeNewline v }) "\"string\"") "extra message embeded into output"+  , Option ['l'] ["useLog"]+    (NoArg (\c -> c { useLog = True })) "use Logarithmic value for propagation"+  , Option ['h'] ["help"]+    (NoArg (\c -> c { help = True })) "display help message"+  ]++parseOptions :: String -> [String] -> IO Opt+parseOptions mes argv =+    case getOpt Permute options argv of+      (o,  [], []) -> return $ foldl (flip id) optDefault o+      (o,   _, []) -> return $ foldl (flip id) optDefault o+      (_,   _, err) -> ioError (userError (concat err ++ usageInfo mes options))++-- | builds "MiosProgramOption" from a String+parseOptionsFromArgs :: String -> IO Opt+parseOptionsFromArgs mes = parseOptions mes =<< getArgs++undecodeNewline :: String -> String+undecodeNewline [] = []+undecodeNewline [a] = [a]+undecodeNewline ('\\' : 'n' : x) = '\n' : undecodeNewline x+undecodeNewline (a : x) = a : undecodeNewline x++showf :: Double -> String+showf x = showFFloat (Just 2) x ""++showi :: Int -> String+showi x+  | 3 <= length s = s+  | otherwise = reverse . take 3 . (++ "   ") . reverse $ s+  where s = show x++showl :: Either Double Int -> String+showl (Left x) = showf x+showl (Right x) = showf (fromIntegral x)++main :: IO ()+main = do+  opts <- parseOptionsFromArgs "gp-summary"+  if help opts+    then putStrLn $ usageInfo "" options+    else do let parsers = [ (fst (header :: (String, MiosDump)), toMerge <$> fromCSV)+                          , (fst (header :: (String, MergedDump)), fromMergedCSV)]+            putStrLn $ message opts+            putStrLn ""+            if useLog opts+              then do putStrLn "|   n |   p1 |   p2 |  p3 |  p4 | log(P) | conflict |   learnt | backjump | re-st | rate | extra | pr/bj |"+                      putStrLn "| --- | ---- | ---- | --- | --- | ------ | -------- | -------- | -------- | ----- | ---- | ----- | ----- |"+              else do putStrLn "|   n |   p1 |   p2 |  p3 |  p4 | propagation | conflict |   learnt | backjump | re-st | rate | extra | pr/bj |"+                      putStrLn "| --- | ---- | ---- | --- | --- | ----------- | -------- | -------- | -------- | ----- | ---- | ----- | ----- |"+            mapM_ (putStrLn . toSummary (useLog opts)) . parseBy parsers =<< getContents++toSummary :: Bool -> MergedDump -> String+toSummary uLog (MergedDump (_, MiosConfiguration _ _ p1 p2 p3 p4) n (MiosStats l) _) =+  "| " ++ intercalate " | " [show n, m', s', showf pr] ++ " |"+  where+    m' = intercalate " | " [showf p1, showf p2, showi p3, showi p4]+    s' = intercalate " | " $ map (showl . snd) (convert uLog l) -- (tail . init $ l)+    convert :: Bool -> [DumpedValue] -> [DumpedValue]+    convert uL ks+      | uL = logOf PropagationS : map valOf [ConflictS .. ExtraS]+      | otherwise = map valOf [PropagationS .. ExtraS]+      where+        logOf :: DumpTag -> DumpedValue+        logOf key = (key, Left $ logBase 10 (val key))+        valOf key = (key, Left $ val key)+        val :: DumpTag -> Double+        val key+          | Just (Left x) <- lookup key ks = x+          | Just (Right x) <- lookup key ks = fromIntegral x+          | otherwise = 0+    pr = fromMaybe 0 $ div' <$> lookup PropagationS l <*> lookup BackjumpS l+    div' :: Either Double Int -> Either Double Int -> Double+    div' (Right a) (Right b) = fromIntegral a / fromIntegral b+    div' (Right a) (Left b)  = fromIntegral a / b+    div' (Left a) (Right b)  = a / fromIntegral b+    div' (Left a) (Left b)   = a / b

@@ -1,293 +0,0 @@-{-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE Safe #-}---- | Minisat-based Implementation and Optimization Study on SAT solver-module SAT.Mios-       (-         -- * Interface to the core of solver-         versionId-       , CNFDescription (..)-       , module SAT.Mios.OptionParser-       , runSolver-       , solveSAT-       , solveSATWithConfiguration-       , solve-       , getModel-         -- * Assignment Validator-       , validateAssignment-       , validate-         -- * For standalone programs-       , executeSolverOn-       , executeSolver-       , executeValidatorOn-       , executeValidator-         -- * File IO-       , dumpAssigmentAsCNF-       )-       where--import Control.Monad ((<=<), unless, void, when)-import Data.Char-import qualified Data.ByteString.Char8 as B-import Data.List-import Numeric (showFFloat)-import System.CPUTime-import System.Exit-import System.IO--import SAT.Mios.Types-import SAT.Mios.Solver-import SAT.Mios.Main-import SAT.Mios.OptionParser-import SAT.Mios.Validator---- | version name-versionId :: String-versionId = "mios 1.4.0 -- https://github.com/shnarazk/mios"--reportElapsedTime :: Bool -> String -> Integer -> IO Integer-reportElapsedTime False _ _ = return 0-reportElapsedTime _ _ 0 = getCPUTime-reportElapsedTime _ mes t = do-  now <- getCPUTime-  let toSecond = 1000000000000 :: Double-  hPutStr stderr mes-  hPutStrLn stderr $ showFFloat (Just 3) ((fromIntegral (now - t)) / toSecond) " sec"-  return now---- | executes a solver on the given CNF file.--- This is the simplest entry to standalone programs; not for Haskell programs.-executeSolverOn :: FilePath -> IO ()-executeSolverOn path = executeSolver (miosDefaultOption { _targetFile = Just path })---- | executes a solver on the given 'arg :: MiosConfiguration'.--- This is another entry point for standalone programs.-executeSolver :: MiosProgramOption -> IO ()-executeSolver opts@(_targetFile -> target@(Just cnfFile)) = do-  t0 <- reportElapsedTime (_confTimeProbe opts) "" 0-  (desc, cls) <- parseHeader target <$> B.readFile cnfFile-  when (_numberOfVariables desc == 0) $ error $ "couldn't load " ++ show cnfFile-  s <- newSolver (toMiosConf opts) desc-  parseClauses s desc cls-  t1 <- reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Parse: ") t0-  when (_confVerbose opts) $ do-    nc <- nClauses s-    hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (nVars s, _numberOfVariables desc) ++ " #c = " ++ show (nc, _numberOfClauses desc)-  res <- simplifyDB s-  -- when (_confVerbose opts) $ hPutStrLn stderr $ "`simplifyDB`: " ++ show res-  result <- if res then solve s [] else return False-  case result of-    True  | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "SATISFIABLE"-    False | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "UNSATISFIABLE"-    True  -> print =<< getModel s-    False -> do          -- contradiction-      -- FIXMEin future-      when (_confVerbose opts) $ hPutStrLn stderr "UNSAT"-      -- print =<< map lit2int <$> asList (conflict s)-      putStrLn "[]"-  case _outputFile opts of-    Just fname -> dumpAssigmentAsCNF fname result =<< getModel s-    Nothing -> return ()-  t2 <- reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Solve: ") t1-  when (result && _confCheckAnswer opts) $ do-    asg <- getModel s-    s' <- newSolver (toMiosConf opts) desc-    parseClauses s' desc cls-    good <- validate s' asg-    if _confVerbose opts-      then hPutStrLn stderr $ if good then "A vaild answer" else "Internal error: mios returns a wrong answer"-      else unless good $ hPutStrLn stderr "Internal error: mios returns a wrong answer"-    void $ reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Validate: ") t2-  void $ reportElapsedTime (_confTimeProbe opts) ("## [" ++ showPath cnfFile ++ "] Total: ") t0-  when (_confStatProbe opts) $ do-    hPutStr stderr $ "## [" ++ showPath cnfFile ++ "] "-    hPutStrLn stderr . intercalate ", " . map (\(k, v) -> show k ++ ": " ++ show v) =<< getStats s--executeSolver _ = return ()---- | new top-level interface that returns:------ * conflicting literal set :: Left [Int]--- * satisfiable assignment :: Right [Int]----runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int])-runSolver m d c = do-  s <- newSolver m d-  mapM_ ((s `addClause`) <=< (newStackFromList . map int2lit)) c-  noConf <- simplifyDB s-  if noConf-    then do-        x <- solve s []-        if x-            then Right <$> getModel s-            else Left .  map lit2int <$> asList (conflicts s)-    else return $ Left []---- | The easiest interface for Haskell programs.--- This returns the result @::[[Int]]@ for a given @(CNFDescription, [[Int]])@.--- The first argument @target@ can be build by @Just target <- cnfFromFile targetfile@.--- The second part of the first argument is a list of vector, which 0th element is the number of its real elements.-solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int]-solveSAT = solveSATWithConfiguration defaultConfiguration---- | solves the problem (2rd arg) under the configuration (1st arg).--- and returns an assignment as list of literals :: Int.-solveSATWithConfiguration :: Traversable m => MiosConfiguration -> CNFDescription -> m [Int] -> IO [Int]-solveSATWithConfiguration conf desc cls = do-  s <- newSolver conf desc-  -- mapM_ (const (newVar s)) [0 .. _numberOfVariables desc - 1]-  mapM_ ((s `addClause`) <=< (newStackFromList . map int2lit)) cls-  noConf <- simplifyDB s-  if noConf-    then do-        result <- solve s []-        if result-            then getModel s-            else return []-    else return []---- | validates a given assignment from STDIN for the CNF file (2nd arg).--- this is the entry point for standalone programs.-executeValidatorOn :: FilePath -> IO ()-executeValidatorOn path = executeValidator (miosDefaultOption { _targetFile = Just path })---- | validates a given assignment for the problem (2nd arg).--- This is another entry point for standalone programs; see app/mios.hs.-executeValidator :: MiosProgramOption -> IO ()-executeValidator opts@(_targetFile -> target@(Just cnfFile)) = do-  (desc, cls) <- parseHeader target <$> B.readFile cnfFile-  when (_numberOfVariables desc == 0) . error $ "couldn't load " ++ show cnfFile-  s <- newSolver (toMiosConf opts) desc-  parseClauses s desc cls-  when (_confVerbose opts) $-    hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (_numberOfVariables desc) ++ " #c = " ++ show (_numberOfClauses desc)-  when (_confVerbose opts) $ do-    nc <- nClauses s-    nl <- nLearnts s-    hPutStrLn stderr $ "(nv, nc, nl) = " ++ show (nVars s, nc, nl)-  asg <- read <$> getContents-  unless (_confNoAnswer opts) $ print asg-  result <- s `validate` (asg :: [Int])-  if result-    then putStrLn ("It's a valid assignment for " ++ cnfFile ++ ".") >> exitSuccess-    else putStrLn ("It's an invalid assignment for " ++ cnfFile ++ ".") >> exitFailure--executeValidator _  = return ()---- | returns True if a given assignment (2nd arg) satisfies the problem (1st arg).--- if you want to check the @answer@ which a @slover@ returned, run @solver `validate` answer@,--- where 'validate' @ :: Traversable t => Solver -> t Lit -> IO Bool@.-validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool-validateAssignment desc cls asg = do-  s <- newSolver defaultConfiguration desc-  mapM_ ((s `addClause`) <=< (newStackFromList . map int2lit)) cls-  s `validate` asg---- | dumps an assigment to file.--- 2nd arg is------ * @True@ if the assigment is satisfiable assigment------ * @False@ if not------ >>> do y <- solve s ... ; dumpAssigmentAsCNF "result.cnf" y <$> model s----dumpAssigmentAsCNF :: FilePath -> Bool -> [Int] -> IO ()-dumpAssigmentAsCNF fname False _ = do-  withFile fname WriteMode $ \h -> hPutStrLn h "UNSAT"--dumpAssigmentAsCNF fname True l = do-  withFile fname WriteMode $ \h -> do hPutStrLn h "SAT"; hPutStrLn h . unwords $ map show l------------------------------------------------------------------------------------- DIMACS CNF Reader-----------------------------------------------------------------------------------parseHeader :: Maybe FilePath -> B.ByteString -> (CNFDescription, B.ByteString)-parseHeader target bs = if B.head bs == 'p' then (parseP l, B.tail bs') else parseHeader target (B.tail bs')-  where-    (l, bs') = B.span ('\n' /=) bs-    -- format: p cnf n m, length "p cnf" == 5-    parseP line = case B.readInt $ B.dropWhile (`elem` " \t") (B.drop 5 line) of-      Just (x, second) -> case B.readInt (B.dropWhile (`elem` " \t") second) of-        Just (y, _) -> CNFDescription x y target-        _ -> CNFDescription 0 0 target-      _ -> CNFDescription 0 0 target--parseClauses :: Solver -> CNFDescription -> B.ByteString -> IO ()-parseClauses s (CNFDescription nv nc _) bs = do-  let maxLit = int2lit $ negate nv-  buffer <- newVec (maxLit + 1) 0-  polvec <- newVec (maxLit + 1) 0-  let-    loop :: Int -> B.ByteString -> IO ()-    loop ((< nc) -> False) _ = return ()-    loop i b = loop (i + 1) =<< readClause s buffer polvec b-  loop 0 bs-  -- static polarity-  let-    asg = assigns s-    checkPolarity :: Int -> IO ()-    checkPolarity ((< nv) -> False) = return ()-    checkPolarity v = do-      p <- getNth polvec $ var2lit v True-      n <- getNth polvec $ var2lit v False-      when (p == lFalse || n == lFalse) $ setNth asg v p-      checkPolarity $ v + 1-  checkPolarity 1--skipWhitespace :: B.ByteString -> B.ByteString-skipWhitespace s-  | elem c " \t\n" = skipWhitespace $ B.tail s-  | otherwise = s-    where-      c = B.head s---- | skip comment lines--- __Pre-condition:__ we are on the benngining of a line-skipComments :: B.ByteString -> B.ByteString-skipComments s-  | c == 'c' = skipComments . B.tail . B.dropWhile (/= '\n') $ s-  | otherwise = s-  where-    c = B.head s--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)-    '+' -> loop st (0 :: Int)-    c | '0' <= c && c <= '9'  -> loop st 0-    _ -> error "PARSE ERROR! Unexpected char"--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 = do-      let (k, b') = parseInt $ skipWhitespace b-      if k == 0-        then do-            -- putStrLn . ("clause: " ++) . show . map lit2int =<< asList stack-            setNth buffer 0 $ i - 1-            void $ addClause s buffer-            return b'-        else do-            let l = int2lit k-            setNth buffer i l-            setNth bvec l lTrue-            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

@@ -1,145 +0,0 @@-{-# LANGUAGE-    BangPatterns-  , FlexibleInstances-  , MagicHash-  , MultiParamTypeClasses-  , RecordWildCards-  , ViewPatterns-  #-}-{-# LANGUAGE Trustworthy #-}---- | Clause, supporting pointer-based equality-module SAT.Mios.Clause-       (-         Clause (..)---       , isLit---       , getLit-       , newClauseFromStack-         -- * Vector of Clause-       , ClauseVector-       , newClauseVector-       )-       where--import GHC.Prim (tagToEnum#, reallyUnsafePtrEquality#)-import qualified Data.Vector as V-import qualified Data.Vector.Mutable as MV--- import Data.List (intercalate)-import SAT.Mios.Types---- | __Fig. 7.(p.11)__--- normal, null (and binary) clause.--- This matches both of @Clause@ and @GClause@ in MiniSat.-data Clause = Clause-              {-                learnt     :: !Bool     -- ^ whether this is a learnt clause---              , rank     :: !Int'     -- ^ goodness like LBD; computed in 'Ranking'-              , activity   :: !Double'  -- ^ activity of this clause-              , protected  :: !Bool'    -- ^ protected from reduce-              , lits       :: !Stack    -- ^ which this clause consists of-              }-  | NullClause                              -- as null pointer---  | BinaryClause Lit                        -- binary clause consists of only a propagating literal---- | The equality on 'Clause' is defined with 'reallyUnsafePtrEquality'.-instance Eq Clause where-  {-# SPECIALIZE INLINE (==) :: Clause -> Clause -> Bool #-}-  (==) x y = x `seq` y `seq` tagToEnum# (reallyUnsafePtrEquality# x y)--instance Show Clause where-  show NullClause = "NullClause"-  show _ = "a clause"---- | 'Clause' is a 'VecFamily' of 'Lit'.-instance VecFamily Clause Lit where-  {-# SPECIALIZE INLINE getNth :: Clause -> Int -> IO Int #-}-  getNth Clause{..} n = error "no getNth for Clause"-  {-# SPECIALIZE INLINE setNth :: Clause -> Int -> Int -> IO () #-}-  setNth Clause{..} n x = error "no setNth for Clause"-  -- | returns a vector of literals in it.-  {-# SPECIALIZE INLINE asUVector :: Clause -> UVector Int #-}-  asUVector = asUVector . lits-  asList NullClause = return []-  asList Clause{..} = take <$> get' lits <*> asList lits-  -- dump mes NullClause = return $ mes ++ "Null"-  -- dump mes Clause{..} = return $ mes ++ "a clause"-{--  dump mes Clause{..} = do-    a <- show <$> get' activity-    n <- get' lits-    l <- asList lits-    return $ mes ++ "C" ++ show n ++ "{" ++ intercalate "," [show learnt, a, show (map lit2int l)] ++ "}"--}---- | 'Clause' is a 'SingleStorage' on the number of literals in it.-instance SingleStorage Clause Int where-  -- | returns the number of literals in a clause, even if the given clause is a binary clause-  {-# SPECIALIZE INLINE get' :: Clause -> IO Int #-}-  get' = get' . lits-  -- getSize (BinaryClause _) = return 1-  -- | sets the number of literals in a clause, even if the given clause is a binary clause-  {-# SPECIALIZE INLINE set' :: Clause -> Int -> IO () #-}-  set' c n = set' (lits c) n-  -- getSize (BinaryClause _) = return 1---- | 'Clause' is a 'Stackfamily'on literals since literals in it will be discared if satisifed at level = 0.-instance StackFamily Clause Lit where-  -- | drop the last /N/ literals in a 'Clause' to eliminate unsatisfied literals-  {-# SPECIALIZE INLINE shrinkBy :: Clause -> Int -> IO () #-}-  shrinkBy c n = modifyNth (lits c) (subtract n) 0---- returns True if it is a 'BinaryClause'.--- FIXME: this might be discarded in minisat 2.2--- isLit :: Clause -> Bool--- isLit (BinaryClause _) = True--- isLit _ = False---- returns the literal in a BinaryClause.--- FIXME: this might be discarded in minisat 2.2--- getLit :: Clause -> Lit--- getLit (BinaryClause x) = x---- coverts a binary clause to normal clause in order to reuse map-on-literals-in-a-clause codes.--- liftToClause :: Clause -> Clause--- liftToClause (BinaryClause _) = error "So far I use generic function approach instead of lifting"---- | copies /vec/ and return a new 'Clause'.--- Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically.-{-# INLINABLE newClauseFromStack #-}-newClauseFromStack :: Bool -> Stack -> IO Clause-newClauseFromStack l vec = do-  n <- get' vec-  v <- newStack n-  let-    loop ((<= n) -> False) = return ()-    loop i = (setNth v i =<< getNth vec i) >> loop (i + 1)-  loop 0-  Clause l <$> {- new' 0 <*> -} new' 0.0 <*> new' False <*> return v---------------------------------------------------------------------------------- Clause Vector---- | Mutable 'Clause' Vector-type ClauseVector = MV.IOVector Clause---- | 'ClauseVector' is a vector of 'Clause'.-instance VecFamily ClauseVector Clause where-  {-# SPECIALIZE INLINE getNth :: ClauseVector -> Int -> IO Clause #-}-  getNth = MV.unsafeRead-  {-# SPECIALIZE INLINE setNth :: ClauseVector -> Int -> Clause -> IO () #-}-  setNth = MV.unsafeWrite-  {-# SPECIALIZE INLINE swapBetween :: ClauseVector -> Int -> Int -> IO () #-}-  swapBetween = MV.unsafeSwap-  asList cv = V.toList <$> V.freeze cv-{--  dump mes cv = do-    l <- asList cv-    sts <- mapM (dump ",") (l :: [Clause])-    return $ mes ++ tail (concat sts)--}---- | returns a new 'ClauseVector'.-newClauseVector  :: Int -> IO ClauseVector-newClauseVector n = do-  v <- MV.new (max 4 n)-  MV.set v NullClause-  return v

@@ -1,234 +0,0 @@-{-# LANGUAGE-    BangPatterns-  , FlexibleInstances-  , MultiParamTypeClasses-  , RecordWildCards-  , ViewPatterns-  #-}-{-# LANGUAGE Trustworthy #-}---- | A shrinkable vector of 'C.Clause'-module SAT.Mios.ClauseManager-       (-         -- * higher level interface for ClauseVector-         ClauseManager (..)-         -- * Manager with an extra Int (used as sort key or blocking literal)-       , ClauseExtManager-       , pushClauseWithKey-       , getKeyVector-       , markClause---       , purifyManager-         -- * WatcherList-       , WatcherList-       , newWatcherList-       , getNthWatcher-       )-       where--import Control.Monad (unless, when)-import qualified Data.IORef as IORef-import qualified Data.Vector as V-import qualified Data.Vector.Mutable as MV-import SAT.Mios.Types-import qualified SAT.Mios.Clause as C---- | Resizable vector of 'C.Clause'.-class ClauseManager a where-  newManager      :: Int -> IO a-  getClauseVector :: a -> IO C.ClauseVector---  removeClause    :: a -> C.Clause -> IO ()---  removeNthClause :: a -> Int -> IO ()-------------------------------------------------------------------------------------- | Clause + Blocking Literal-data ClauseExtManager = ClauseExtManager-  {-    _nActives     :: !Int'                         -- number of active clause-  , _purged       :: !Bool'                        -- whether it needs gc-  , _clauseVector :: IORef.IORef C.ClauseVector    -- clause list-  , _keyVector    :: IORef.IORef (UVector Int)     -- Int list-  }---- | 'ClauseExtManager' is a 'SingleStorage` on the numeber of clauses in it.-instance SingleStorage ClauseExtManager Int where-  {-# SPECIALIZE INLINE get' :: ClauseExtManager -> IO Int #-}-  get' m = get' (_nActives m)-  {-# SPECIALIZE INLINE set' :: ClauseExtManager -> Int -> IO () #-}-  set' m = set' (_nActives m)---- | 'ClauseExtManager' is a 'StackFamily` on clauses.-instance StackFamily ClauseExtManager C.Clause where-  {-# SPECIALIZE INLINE shrinkBy :: ClauseExtManager -> Int -> IO () #-}-  shrinkBy m k = modify' (_nActives m) (subtract k)-  pushTo ClauseExtManager{..} c = do-    -- checkConsistency m c-    !n <- get' _nActives-    !v <- IORef.readIORef _clauseVector-    !b <- IORef.readIORef _keyVector-    if MV.length v - 1 <= n-      then do-          let len = max 8 $ MV.length v-          v' <- MV.unsafeGrow v len-          b' <- growBy b len-          MV.unsafeWrite v' n c-          setNth b' n 0-          IORef.writeIORef _clauseVector v'-          IORef.writeIORef _keyVector b'-      else MV.unsafeWrite v n c >> setNth b n 0-    modify' _nActives (1 +)---- | 'ClauseExtManager' is a 'ClauseManager'-instance ClauseManager ClauseExtManager where-  -- | returns a new instance.-  {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-}-  newManager initialSize = do-    i <- new' 0-    v <- C.newClauseVector initialSize-    b <- newVec (MV.length v) 0-    ClauseExtManager i <$> new' False <*> IORef.newIORef v <*> IORef.newIORef b-  -- | returns the internal 'C.ClauseVector'.-  {-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-}-  getClauseVector !m = IORef.readIORef (_clauseVector m)-{--  -- | O(1) insertion function-  pushClause !ClauseExtManager{..} !c = do-    -- checkConsistency m c-    !n <- get' _nActives-    !v <- IORef.readIORef _clauseVector-    !b <- IORef.readIORef _keyVector-    if MV.length v - 1 <= n-      then do-          let len = max 8 $ MV.length v-          v' <- MV.unsafeGrow v len-          b' <- growBy b len-          MV.unsafeWrite v' n c-          setNth b' n 0-          IORef.writeIORef _clauseVector v'-          IORef.writeIORef _keyVector b'-      else MV.unsafeWrite v n c >> setNth b n 0-    modify' _nActives (1 +)--}-{--  -- | O(n) but lightweight remove-and-compact function-  -- __Pre-conditions:__ the clause manager is empty or the clause is stored in it.-  {-# SPECIALIZE INLINE removeClause :: ClauseExtManager -> C.Clause -> IO () #-}-  removeClause ClauseExtManager{..} c = do-    !n <- subtract 1 <$> get' _nActives-    !v <- IORef.readIORef _clauseVector-    !b <- IORef.readIORef _keyVector-    let-      seekIndex :: Int -> IO Int-      seekIndex k = do-        c' <- MV.unsafeRead v k-        if c' == c then return k else seekIndex $ k + 1-    unless (n == -1) $ do-      !i <- seekIndex 0-      MV.unsafeWrite v i =<< MV.unsafeRead v n-      setNth b i =<< getNth b n-      set' _nActives n-  removeNthClause = error "removeNthClause is not implemented on ClauseExtManager"--}---- | sets the expire flag to a clause.-{-# INLINABLE markClause #-}-markClause :: ClauseExtManager -> C.Clause -> IO ()-markClause ClauseExtManager{..} c = do-  !n <- get' _nActives-  !v <- IORef.readIORef _clauseVector-  let-    seekIndex :: Int -> IO ()-    seekIndex k = do-      c' <- MV.unsafeRead v k-      if c' == c then MV.unsafeWrite v k C.NullClause else seekIndex $ k + 1-  unless (n == 0) $ do-    seekIndex 0-    set' _purged True--{-# INLINABLE purifyManager #-}-purifyManager :: ClauseExtManager -> IO ()-purifyManager ClauseExtManager{..} = do-  diry <- get' _purged-  when diry $ do-    n <- get' _nActives-    vec <- IORef.readIORef _clauseVector-    keys <- IORef.readIORef _keyVector-    let-      loop :: Int -> Int -> IO Int-      loop ((< n) -> False) n' = return n'-      loop i j = do-        c <- getNth vec i-        if c /= C.NullClause-          then do-              unless (i == j) $ do-                setNth vec j c-                setNth keys j =<< getNth keys i-              loop (i + 1) (j + 1)-          else loop (i + 1) j-    set' _nActives =<< loop 0 0-    set' _purged False---- | returns the associated Int vector, which holds /blocking literals/.-{-# INLINE getKeyVector #-}-getKeyVector :: ClauseExtManager -> IO (UVector Int)-getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector---- | O(1) inserter-{-# INLINABLE pushClauseWithKey #-}-pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO ()-pushClauseWithKey !ClauseExtManager{..} !c k = do-  -- checkConsistency m c-  !n <- get' _nActives-  !v <- IORef.readIORef _clauseVector-  !b <- IORef.readIORef _keyVector-  if MV.length v - 1 <= n-    then do-        let len = max 8 $ MV.length v-        v' <- MV.unsafeGrow v len-        b' <- growBy b len-        MV.unsafeWrite v' n c-        setNth b' n k-        IORef.writeIORef _clauseVector v'-        IORef.writeIORef _keyVector b'-    else MV.unsafeWrite v n c >> setNth b n k-  modify' _nActives (1 +)---- | 'ClauseExtManager' is a collection of 'C.Clause'-instance VecFamily ClauseExtManager C.Clause where-  getNth = error "no getNth method for ClauseExtManager"-  setNth = error "no setNth method for ClauseExtManager"-  {-# SPECIALIZE INLINE reset :: ClauseExtManager -> IO () #-}-  reset m = set' (_nActives m) 0-{--  dump mes ClauseExtManager{..} = do-    n <- get' _nActives-    if n == 0-      then return $ mes ++ "empty ClauseExtManager"-      else do-          l <- take n <$> (asList =<< IORef.readIORef _clauseVector)-          sts <- mapM (dump ",") (l :: [C.Clause])-          return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts)--}---------------------------------------------------------------------------------- WatcherList---- | Immutable Vector of 'ClauseExtManager'-type WatcherList = V.Vector ClauseExtManager---- | /n/ is the number of 'Var', /m/ is default size of each watcher list.--- | For /n/ vars, we need [0 .. 2 + 2 * n - 1] slots, namely /2 * (n + 1)/-length vector-newWatcherList :: Int -> Int -> IO WatcherList-newWatcherList n m = V.fromList <$> mapM (\_ -> newManager m) [0 .. int2lit (negate n) + 1]---- | returns the watcher List for "Literal" /l/.-{-# INLINE getNthWatcher #-}-getNthWatcher :: WatcherList -> Lit -> ClauseExtManager-getNthWatcher = V.unsafeIndex---- | 'WatcherList' is an 'Lit'-indexed collection of 'C.Clause'.-instance VecFamily WatcherList C.Clause where-  getNth = error "no getNth method for WatcherList" -- getNthWatcher is a pure function-  setNth = error "no setNth method for WatcherList"-  {-# SPECIALIZE INLINE reset :: WatcherList -> IO () #-}-  reset = V.mapM_ purifyManager---  dump _ _ = (mes ++) . concat <$> mapM (\i -> dump ("\n" ++ show (lit2int i) ++ "' watchers:") (getNthWatcher wl i)) [1 .. V.length wl - 1]

@@ -1,817 +0,0 @@-{-# LANGUAGE-    BangPatterns-  , RecordWildCards-  , ScopedTypeVariables-  , ViewPatterns-  #-}-{-# LANGUAGE Safe #-}---- | This is a part of MIOS; main heuristics.-module SAT.Mios.Main-       (-         simplifyDB-       , solve-       )-        where--import Control.Monad (unless, void, when)-import Data.Bits-import Data.Foldable (foldrM)-import SAT.Mios.Types-import SAT.Mios.Clause-import SAT.Mios.ClauseManager-import SAT.Mios.Solver---- | returns a rank of 'Clause'. Smaller value is better.-{-# INLINE rankOf #-}-rankOf :: Clause -> IO Int-rankOf = get'---- | #114: __RemoveWatch__-{-# INLINABLE removeWatch #-}-removeWatch :: Solver -> Clause -> IO ()-removeWatch (watches -> w) c = do-  let lvec = asUVector c-  l1 <- negateLit <$> getNth lvec 0-  markClause (getNthWatcher w l1) c-  l2 <- negateLit <$> getNth lvec 1-  markClause (getNthWatcher w l2) c------------------------------------------------------------------------------------- Operations on 'Clause'------------------------------------------------------------------------------------- | __Fig. 8. (p.12)__ creates a new LEARNT clause and adds it to watcher lists.--- This is a strippped-down version of 'newClause' in Solver.-{-# INLINABLE newLearntClause #-}-newLearntClause :: Solver -> Stack -> IO ()-newLearntClause s@Solver{..} ps = do-  good <- get' ok-  when good $ do-    -- ps is a 'SizedVectorInt'; ps[0] is the number of active literals-    -- Since this solver must generate only healthy learnt clauses, we need not to run misc check in 'newClause'-    k <- get' ps-    case k of-     1 -> do-       l <- getNth ps 1-       unsafeEnqueue s l NullClause-     _ -> do-       -- allocate clause:-       c <- newClauseFromStack True ps-       let vec = asUVector c-       -- Pick a second literal to watch:-       let-         findMax :: Int -> Int -> Int -> IO Int-         findMax ((< k) -> False) j _ = return j-         findMax i j val = do-           v <- lit2var <$> getNth vec i-           a <- getNth assigns v-           b <- getNth level v-           if (a /= lBottom) && (val < b)-             then findMax (i + 1) i b-             else findMax (i + 1) j val-       swapBetween vec 1 =<< findMax 0 0 0 -- Let @max_i@ be the index of the literal with highest decision level-       -- Bump, enqueue, store clause:-       set' (activity c) . fromIntegral =<< decisionLevel s -- newly learnt clauses should be considered active-       -- Add clause to all managers-       pushTo learnts c-       l <- getNth vec 0-       pushClauseWithKey (getNthWatcher watches (negateLit l)) c 0-       l1 <- negateLit <$> getNth vec 1-       pushClauseWithKey (getNthWatcher watches l1) c 0-       -- update the solver state by @l@-       unsafeEnqueue s l c-       -- Since unsafeEnqueue updates the 1st literal's level, setLBD should be called after unsafeEnqueue-       -- setRank s c-       set' (protected c) True---- | __Simplify.__ At the top-level, a constraint may be given the opportunity to--- simplify its representation (returns @False@) or state that the constraint is--- satisfied under the current assignment and can be removed (returns @True@).--- A constraint must /not/ be simplifiable to produce unit information or to be--- conflicting; in that case the propagation has not been correctly defined.------ MIOS NOTE: the original doesn't update watchers; only checks its satisfiabiliy.-{-# INLINABLE simplify #-}-simplify :: Solver -> Clause -> IO Bool-simplify s c = do-  n <- get' c-  let-    lvec = asUVector c-    loop ::Int -> IO Bool-    loop ((< n) -> False) = return False-    loop i = do-      v <- valueLit s =<< getNth lvec i-      if v == 1 then return True else loop (i + 1)-  loop 0------------------------------------------------------------------------------------- MIOS NOTE on Minor methods:------ * no (meaningful) 'newVar' in mios--- * 'assume' is defined in 'Solver'--- * `cancelUntil` is defined in 'Solver'------------------------------------------------------------------------------------- Major methods---- | M114: __Fig. 10. (p.15)__------ analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel :: int&) -> [void]------ __Description:_----   Analzye confilct and produce a reason clause.------ __Pre-conditions:__---   * 'out_learnt' is assumed to be cleared.---   * Corrent decision level must be greater than root level.------ __Post-conditions:__---   * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.---   * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the---     rest of literals. There may be others from the same level though.------ @analyze@ is invoked from @search@-{-# INLINABLE analyze #-}-analyze :: Solver -> Clause -> IO Int-analyze s@Solver{..} confl = do-  -- litvec-  reset litsLearnt-  pushTo litsLearnt 0 -- reserve the first place for the unassigned literal-  dl <- decisionLevel s-  let-    litsVec = asUVector litsLearnt-    trailVec = asUVector trail-    loopOnClauseChain :: Clause -> Lit -> Int -> Int -> Int -> IO Int-    loopOnClauseChain c p ti bl pathC = do -- p : literal, ti = trail index, bl = backtrack level-      when (learnt c) $ do-        claBumpActivity s c-{--        -- update LBD like #Glucose4.0-        d <- get' (lbd c)-        when (2 < d) $ do-          nblevels <- lbdOf s c-          when (nblevels + 1 < d) $ do -- improve the LBD-            when (d <= 30) $ set' (protected c) True -- 30 is `lbLBDFrozenClause`-            -- seems to be interesting: keep it fro the next round-            set' (lbd c) nblevels    -- Update it--}-      sc <- get' c-      let-        lvec = asUVector c-        loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int)-        loopOnLiterals ((< sc) -> False) b pc = return (b, pc) -- b = btLevel, pc = pathC-        loopOnLiterals j b pc = do-          (q :: Lit) <- getNth lvec j-          let v = lit2var q-          sn <- getNth an'seen v-          l <- getNth level v-          if sn == 0 && 0 < l-            then do-                varBumpActivity s v-                setNth an'seen v 1-                if dl <= l      -- cancelUntil doesn't clear level of cancelled literals-                  then do-                      -- glucose heuristics-                      r <- getNth reason v-                      when (r /= NullClause && learnt r) $ pushTo an'lastDL q-                      -- end of glucose heuristics-                      loopOnLiterals (j + 1) b (pc + 1)-                  else pushTo litsLearnt q >> loopOnLiterals (j + 1) (max b l) pc-            else loopOnLiterals (j + 1) b pc-      (b', pathC') <- loopOnLiterals (if p == bottomLit then 0 else 1) bl pathC-      let-        -- select next clause to look at-        nextPickedUpLit :: Int -> IO Int-        nextPickedUpLit i = do-          x <- getNth an'seen . lit2var =<< getNth trailVec i-          if x == 0 then nextPickedUpLit $ i - 1 else return i-      ti' <- nextPickedUpLit ti-      nextP <- getNth trailVec ti'-      let nextV = lit2var nextP-      confl' <- getNth reason nextV-      setNth an'seen nextV 0-      if 1 < pathC'-        then loopOnClauseChain confl' nextP (ti' - 1) b' (pathC' - 1)-        else setNth litsVec 0 (negateLit nextP) >> return b'-  ti <- subtract 1 <$> get' trail-  levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0-  -- Simplify phase (implemented only @expensive_ccmin@ path)-  n <- get' litsLearnt-  reset an'stack           -- analyze_stack.clear();-  reset an'toClear         -- out_learnt.copyTo(analyze_toclear);-  pushTo an'toClear =<< getNth litsVec 0-  let-    merger :: Int -> Int -> IO Int-    merger ((< n) -> False) b = return b-    merger i b = do-      l <- getNth litsVec i-      pushTo an'toClear l-      -- restrict the search depth (range) to 32-      merger (i + 1) . setBit b . (31 .&.) =<< getNth level (lit2var l)-  levels <- merger 1 0-  let-    loopOnLits :: Int -> Int -> IO ()-    loopOnLits ((< n) -> False) n' = shrinkBy litsLearnt $ n - n'-    loopOnLits i j = do-      l <- getNth litsVec i-      c1 <- (NullClause ==) <$> getNth reason (lit2var l)-      if c1-        then setNth litsVec j l >> loopOnLits (i + 1) (j + 1)-        else do-           c2 <- not <$> analyzeRemovable s l levels-           if c2-             then setNth litsVec j l >> loopOnLits (i + 1) (j + 1)-             else loopOnLits (i + 1) j-  loopOnLits 1 1                -- the first literal is specail-  -- glucose heuristics-  nld <- get' an'lastDL-  r <- get' litsLearnt -- this is not the right value-  let-    vec = asUVector an'lastDL-    loopOnLastDL :: Int -> IO ()-    loopOnLastDL ((< nld) -> False) = return ()-    loopOnLastDL i = do-      v <- lit2var <$> getNth vec i-      r' <- rankOf =<< getNth reason v-      when (r < r') $ varBumpActivity s v-      loopOnLastDL $ i + 1-  loopOnLastDL 0-  reset an'lastDL-  -- Clear seen-  k <- get' an'toClear-  let-    vec' = asUVector an'toClear-    cleaner :: Int -> IO ()-    cleaner ((< k) -> False) = return ()-    cleaner i = do-      v <- lit2var <$> getNth vec' i-      setNth an'seen v 0-      cleaner $ i + 1-  cleaner 0-  return levelToReturn---- | #M114--- Check if 'p' can be removed, 'abstract_levels' is used to abort early if the algorithm is--- visiting literals at levels that cannot be removed later.------ Implementation memo:------ *  @an'toClear@ is initialized by @ps@ in @analyze@ (a copy of 'learnt').---   This is used only in this function and @analyze@.----{-# INLINABLE analyzeRemovable #-}-analyzeRemovable :: Solver -> Lit -> Int -> IO Bool-analyzeRemovable Solver{..} p minLevel = do-  -- assert (reason[var(p)]!= NullCaulse);-  reset an'stack      -- analyze_stack.clear()-  pushTo an'stack p   -- analyze_stack.push(p);-  top <- get' an'toClear-  let-    loopOnStack :: IO Bool-    loopOnStack = do-      k <- get' an'stack  -- int top = analyze_toclear.size();-      if 0 == k-        then return True-        else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL);-            sl <- lastOf an'stack-            popFrom an'stack             -- analyze_stack.pop();-            c <- getNth reason (lit2var sl) -- getRoot sl-            nl <- get' c-            let-              cvec = asUVector c-              loopOnLit :: Int -> IO Bool -- loopOnLit (int i = 1; i < c.size(); i++){-              loopOnLit ((< nl) -> False) = loopOnStack-              loopOnLit i = do-                p' <- getNth cvec i              -- valid range is [0 .. nl - 1]-                let v' = lit2var p'-                l' <- getNth level v'-                c1 <- (1 /=) <$> getNth an'seen v'-                if c1 && (0 /= l')   -- if (!analyze_seen[var(p)] && level[var(p)] != 0){-                  then do-                      c3 <- (NullClause /=) <$> getNth reason v'-                      if c3 && testBit minLevel (l' .&. 31) -- if (reason[var(p)] != GClause_NULL && ((1 << (level[var(p)] & 31)) & min_level) != 0){-                        then do-                            setNth an'seen v' 1        -- analyze_seen[var(p)] = 1;-                            pushTo an'stack p'    -- analyze_stack.push(p);-                            pushTo an'toClear p'  -- analyze_toclear.push(p);-                            loopOnLit $ i + 1-                        else do-                            -- loopOnLit (int j = top; j < analyze_toclear.size(); j++) analyze_seen[var(analyze_toclear[j])] = 0;-                            top' <- get' an'toClear-                            let-                              vec = asUVector an'toClear-                              clearAll :: Int -> IO ()-                              clearAll ((< top') -> False) = return ()-                              clearAll j = do x <- getNth vec j; setNth an'seen (lit2var x) 0; clearAll (j + 1)-                            clearAll top-                            -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop-                            shrinkBy an'toClear $ top' - top-                            return False-                  else loopOnLit $ i + 1-            loopOnLit 1-  loopOnStack---- | #114--- analyzeFinal : (confl : Clause *) (skip_first : boot) -> [void]------ __Description:__---   Specialized analysis proceduce to express the final conflict in terms of assumptions.---   'root_level' is allowed to point beyond end of trace (useful if called after conflict while---   making assumptions). If 'skip_first' is TRUE, the first literal of 'confl' is ignored (needed---   if conflict arose before search even started).----{-# INLINABLE analyzeFinal #-}-analyzeFinal :: Solver -> Clause -> Bool -> IO ()-analyzeFinal Solver{..} confl skipFirst = do-  reset conflicts-  rl <- get' rootLevel-  unless (rl == 0) $ do-    n <- get' confl-    let-      lvec = asUVector confl-      loopOnConfl :: Int -> IO ()-      loopOnConfl ((< n) -> False) = return ()-      loopOnConfl i = do-        (x :: Var) <- lit2var <$> getNth lvec i-        lvl <- getNth level x-        when (0 < lvl) $ setNth an'seen x 1-        loopOnConfl $ i + 1-    loopOnConfl $ if skipFirst then 1 else 0-    tls <- get' trailLim-    trs <- get' trail-    tlz <- getNth (asUVector trailLim) 0-    let-      trailVec = asUVector trail-      loopOnTrail :: Int -> IO ()-      loopOnTrail ((tlz <=) -> False) = return ()-      loopOnTrail i = do-        (l :: Lit) <- getNth trailVec i-        let (x :: Var) = lit2var l-        saw <- getNth an'seen x-        when (saw == 1) $ do-          (r :: Clause) <- getNth reason x-          if r == NullClause-            then pushTo conflicts (negateLit l)-            else do-                k <- get' r-                let-                  cvec = asUVector r-                  loopOnLits :: Int -> IO ()-                  loopOnLits ((< k) -> False) = return ()-                  loopOnLits j = do-                    (v :: Var) <- lit2var <$> getNth cvec j-                    lv <- getNth level v-                    when (0 < lv) $ setNth an'seen v 1-                    loopOnLits $ i + 1-                loopOnLits 1-        setNth an'seen x 0-        loopOnTrail $ i - 1-    loopOnTrail =<< if tls <= rl then return (trs - 1) else getNth (asUVector trailLim) rl---- | M114:--- propagate : [void] -> [Clause+]------ __Description:__---   Porpagates all enqueued facts. If a conflict arises, the conflicting clause is returned.---   otherwise CRef_undef.------ __Post-conditions:__---   * the propagation queue is empty, even if there was a conflict.------ memo: @propagate@ is invoked by @search@,`simpleDB` and `solve`-{-# INLINABLE propagate #-}-propagate :: Solver -> IO Clause-propagate s@Solver{..} = do-  -- myVal <- getNth stats (fromEnum NumOfBackjump)-  let-{--    myVal = 0-    bumpAllVar :: IO ()         -- not in use-    bumpAllVar = do-      let-        loop :: Int -> IO ()-        loop ((<= nVars) -> False) = return ()-        loop i = do-          c <- getNth pr'seen i-          when (c == myVal) $ varBumpActivity s i-          loop $ i + 1-      loop 1--}-    trailVec = asUVector trail-    while :: Clause -> Bool -> IO Clause-    while confl False = {- bumpAllVar >> -} return confl-    while confl True = do-      (p :: Lit) <- getNth trailVec =<< get' qHead-      modify' qHead (+ 1)-      let (ws :: ClauseExtManager) = getNthWatcher watches p-      end <- get' ws-      cvec <- getClauseVector ws-      bvec <- getKeyVector ws---      rc <- getNth reason $ lit2var p---      byGlue <- if (rc /= NullClause) && learnt rc then (== 2) <$> get' (lbd rc) else return False-      let-{--        checkAllLiteralsIn :: Clause -> IO () -- not in use-        checkAllLiteralsIn c = do-          nc <- sizeOfClause c-          let-            vec = asuVector c-            loop :: Int -> IO ()-            loop((< nc) -> False) = return ()-            loop i = do-              (v :: Var) <- lit2var <$> getNth vec i-              setNth pr'seen v myVal-              loop $ i + 1-          loop 0--}-        forClause :: Clause -> Int -> Int -> IO Clause-        forClause confl i@((< end) -> False) j = do-          shrinkBy ws (i - j)-          while confl =<< ((<) <$> get' qHead <*> get' trail)-        forClause confl i j = do-          (l :: Lit) <- getNth bvec i-          bv <- if l == 0 then return lFalse else valueLit s l-          if bv == lTrue-            then do-                 unless (i == j) $ do -- NOTE: if i == j, the path doesn't require accesses to cvec!-                   (c :: Clause) <- getNth cvec i-                   setNth cvec j c-                   setNth bvec j l-                 forClause confl (i + 1) (j + 1)-            else do-                -- checkAllLiteralsIn c-                (c :: Clause) <- getNth cvec i-                let-                  lits = asUVector c-                  falseLit = negateLit p-                -- Make sure the false literal is data[1]-                ((falseLit ==) <$> getNth lits 0) >>= (`when` swapBetween lits 0 1)-                -- if 0th watch is true, then clause is already satisfied.-                (first :: Lit) <- getNth lits 0-                val <- valueLit s first-                if val == lTrue-                  then setNth cvec j c >> setNth bvec j first >> forClause confl (i + 1) (j + 1)-                  else do-                      -- Look for new watch-                      cs <- get' c-                      let-                        forLit :: Int -> IO Clause-                        forLit ((< cs) -> False) = do-                          -- Did not find watch; clause is unit under assignment:-                          setNth cvec j c-                          setNth bvec j 0-                          result <- enqueue s first c-                          if not result-                            then do-                                ((== 0) <$> decisionLevel s) >>= (`when` set' ok False)-                                -- #BBCP-                                set' qHead =<< get' trail-                                -- Copy the remaining watches:-                                let-                                  copy i'@((< end) -> False) j' = forClause c i' j'-                                  copy i' j' = do-                                    setNth cvec j' =<< getNth cvec i'-                                    setNth bvec j' =<< getNth bvec i'-                                    copy (i' + 1) (j' + 1)-                                copy (i + 1) (j + 1)-                            else forClause confl (i + 1) (j + 1)-                        forLit k = do-                          (l :: Lit) <- getNth lits k-                          lv <- valueLit s l-                          if lv /= lFalse-                            then do-                                swapBetween lits 1 k-                                pushClauseWithKey (getNthWatcher watches (negateLit l)) c l-                                forClause confl (i + 1) j-                            else forLit $ k + 1-                      forLit 2-      forClause confl 0 0-  while NullClause =<< ((<) <$> get' qHead <*> get' trail)---- | #M22--- reduceDB: () -> [void]------ __Description:__---   Remove half of the learnt clauses, minus the clauses locked by the current assigmnent. Locked---   clauses are clauses that are reason to some assignment. Binary clauses are never removed.-{-# INLINABLE reduceDB #-}-reduceDB :: Solver -> IO ()-reduceDB s@Solver{..} = do-  n <- nLearnts s-  vec <- getClauseVector learnts-  let-    loop :: Int -> IO ()-    loop ((< n) -> False) = return ()-    loop i = (removeWatch s =<< getNth vec i) >> loop (i + 1)-  k <- sortClauses s learnts (div n 2) -- k is the number of clauses not to be purged-  loop k                               -- CAVEAT: `vec` is a zero-based vector-  reset watches-  shrinkBy learnts (n - k)---- | (Good to Bad) Quick sort the key vector based on their activities and returns number of privileged clauses.--- this function uses the same metrix as reduceDB_lt in glucose 4.0:--- 1. binary clause--- 2. smaller rank--- 3. larger activity defined in MiniSat--- , where smaller value is better.------ they are coded into an Int as the following layout:------ * 14 bit: LBD or 0 for preserved clauses--- * 19 bit: converted activity--- * remain: clauseVector index----(rankWidth :: Int, activityWidth :: Int, indexWidth :: Int) = (l, a, w - (l + a + 1))-  where-    w = finiteBitSize (0:: Int)-    (l, a) = case () of-      _ | 64 <= w -> (8, 25)   -- 30 bit =>   1G clauses-      _ | 60 <= w -> (8, 24)   -- 26 bit =>  64M clauses-      _ | 32 <= w -> (6,  7)   -- 18 bit => 256K clauses-      _ | 29 <= w -> (6,  5)   -- 17 bit => 128K clauses---      _ -> error "Int on your CPU doesn't have sufficient bit width."--{-# INLINABLE sortClauses #-}-sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int-sortClauses s cm nneeds = do-  -- constants-  let-    rankMax :: Int-    rankMax = 2 ^ rankWidth - 1-    activityMax :: Int-    activityMax = 2 ^ activityWidth - 1-    activityScale :: Double-    activityScale = fromIntegral activityMax-    indexMax :: Int-    indexMax = (2 ^ indexWidth - 1) -- 67,108,863 for 26-  n <- get' cm-  -- when (indexMax < n) $ error $ "## The number of learnt clauses " ++ show n ++ " exceeds mios's " ++ show indexWidth ++" bit manage capacity"-  vec <- getClauseVector cm-  keys <- getKeyVector cm-  -- 1: assign keys-  let-    assignKey :: Int -> Int -> IO Int-    assignKey ((< n) -> False) m = return m-    assignKey i m = do-      c <- getNth vec i-      k <- (\k -> if k == 2 then return k else fromEnum <$> get' (protected c)) =<< get' c-      case k of-        1 -> set' (protected c) False >> setNth keys i (shiftL 2 indexWidth + i) >> assignKey (i + 1) (m + 1)-        2 -> setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1)-        _ -> do-            l <- locked s c      -- this is expensive-            if l-              then setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1)-              else do-                  d <- rankOf c-                  b <- floor . (activityScale *) . (1 -) . logBase claActivityThreshold . max 1 <$> get' (activity c)-                  setNth keys i $ shiftL (min rankMax d) (activityWidth + indexWidth) + shiftL b indexWidth + i-                  assignKey (i + 1) m-  limit <- min n . (+ nneeds) <$> assignKey 0 0-  -- 2: sort keyVector-  let-    sortOnRange :: Int -> Int -> IO ()-    sortOnRange left right-      | limit < left = return ()-      | left >= right = return ()-      | left + 1 == right = do-          a <- getNth keys left-          b <- getNth keys right-          unless (a < b) $ swapBetween keys left right-      | otherwise = do-          let p = div (left + right) 2-          pivot <- getNth keys p-          swapBetween keys p left -- set a sentinel for r'-          let-            nextL :: Int -> IO Int-            nextL i@((<= right) -> False) = return i-            nextL i = do v <- getNth keys i; if v < pivot then nextL (i + 1) else return i-            nextR :: Int -> IO Int-            nextR i = do v <- getNth keys i; if pivot < v then nextR (i - 1) else return i-            divide :: Int -> Int -> IO Int-            divide l r = do-              l' <- nextL l-              r' <- nextR r-              if l' < r' then swapBetween keys l' r' >> divide (l' + 1) (r' - 1) else return r'-          m <- divide (left + 1) right-          swapBetween keys left m-          sortOnRange left (m - 1)-          sortOnRange (m + 1) right-  sortOnRange 0 (n - 1)-  -- 3: place clauses-  let-    seek :: Int -> IO ()-    seek ((< limit) -> False) = return ()-    seek i = do-      bits <- getNth keys i-      when (indexMax < bits) $ do-        c <- getNth vec i-        let-          sweep k = do-            k' <- (indexMax .&.) <$> getNth keys k-            setNth keys k k-            if k' == i-              then setNth vec k c-              else getNth vec k' >>= setNth vec k >> sweep k'-        sweep i-      seek $ i + 1-  seek 0-  return limit---- | #M22------ simplify : [void] -> [bool]------ __Description:__---   Simplify the clause database according to the current top-level assigment. Currently, the only---   thing done here is the removal of satisfied clauses, but more things can be put here.----{-# INLINABLE simplifyDB #-}-simplifyDB :: Solver -> IO Bool-simplifyDB s@Solver{..} = do-  good <- get' ok-  if good-    then do-      p <- propagate s-      if p /= NullClause-        then set' ok False >> return False-        else do-            -- Clear watcher lists:-            n <- get' trail-            let-              vec = asUVector trail-              loopOnLit ((< n) -> False) = return ()-              loopOnLit i = do-                l <- getNth vec i-                reset . getNthWatcher watches $ l-                reset . getNthWatcher watches $ negateLit l-                loopOnLit $ i + 1-            loopOnLit 0-            -- Remove satisfied clauses:-            let-              for :: Int -> IO Bool-              for ((< 2) -> False) = return True-              for t = do-                let ptr = if t == 0 then learnts else clauses-                vec' <- getClauseVector ptr-                n' <- get' ptr-                let-                  loopOnVector :: Int -> Int -> IO Bool-                  loopOnVector ((< n') -> False) j = shrinkBy ptr (n' - j) >> return True-                  loopOnVector i j = do-                        c <- getNth vec' i-                        l <- locked s c-                        r <- simplify s c-                        if not l && r-                          then removeWatch s c >> loopOnVector (i + 1) j-                          else setNth vec' j c >> loopOnVector (i + 1) (j + 1)-                loopOnVector 0 0-            ret <- for 0-            reset watches-            return ret-    else return False---- | #M22------ search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]------ __Description:__---   Search for a model the specified number of conflicts.---   NOTE: Use negative value for 'nof_conflicts' indicate infinity.------ __Output:__---   'l_True' if a partial assigment that is consistent with respect to the clause set is found. If---   all variables are decision variables, that means that the clause set is satisfiable. 'l_False'---   if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.-{-# INLINABLE search #-}-search :: Solver -> Int -> Int -> IO Int-search s@Solver{..} nOfConflicts nOfLearnts = do-  -- clear model-  let-    loop :: Int -> IO Int-    loop conflictC = do-      !confl <- propagate s-      d <- decisionLevel s-      if confl /= NullClause-        then do-            -- CONFLICT-            incrementStat s NumOfBackjump 1-            r <- get' rootLevel-            if d == r-              then do-                  -- Contradiction found:-                  analyzeFinal s confl False-                  return lFalse-              else do---                  u <- (== 0) . (flip mod 5000) <$> getNth stats (fromEnum NumOfBackjump)---                  when u $ do---                    d <- get' varDecay---                    when (d < 0.95) $ modify' varDecay (+ 0.01)-                  backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself-                  (s `cancelUntil`) . max backtrackLevel =<< get' rootLevel-                  newLearntClause s litsLearnt-                  k <- get' litsLearnt-                  when (k == 1) $ do-                    (v :: Var) <- lit2var <$> getNth (asUVector litsLearnt) 0-                    setNth level v 0-                  varDecayActivity s-                  -- claDecayActivity s-                  loop $ conflictC + 1-        else do                 -- NO CONFLICT-            -- Simplify the set of problem clauses:-            when (d == 0) . void $ simplifyDB s -- our simplifier cannot return @False@ here-            k1 <- get' learnts-            k2 <- nAssigns s-            when (k1 - k2 >= nOfLearnts) $ reduceDB s -- Reduce the set of learnt clauses-            case () of-             _ | k2 == nVars -> do-                   -- Model found:-                   let-                     toInt :: Var -> IO Lit-                     toInt v = (\p -> if lTrue == p then v else negate v) <$> valueVar s v-                     setModel :: Int -> IO ()-                     setModel ((<= nVars) -> False) = return ()-                     setModel v = (setNth model v =<< toInt v) >> setModel (v + 1)-                   setModel 1-                   return lTrue-             _ | conflictC >= nOfConflicts -> do-                   -- Reached bound on number of conflicts-                   (s `cancelUntil`) =<< get' rootLevel -- force a restart-                   claRescaleActivityAfterRestart s-                   incrementStat s NumOfRestart 1-                   return lBottom-             _ -> do-               -- New variable decision:-               v <- select s -- many have heuristic for polarity here-               -- << #phasesaving-               oldVal <- getNth phases v-               unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@-               -- >> #phasesaving-               loop conflictC-  good <- get' ok-  if good then loop 0 else return lFalse---- | __Fig. 16. (p.20)__--- Main solve method.------ __Pre-condition:__ If assumptions are used, 'simplifyDB' must be--- called right before using this method. If not, a top-level conflict (resulting in a--- non-usable internal state) cannot be distinguished from a conflict under assumptions.-{-# INLINABLE solve #-}-solve :: (Foldable t) => Solver -> t Lit -> IO Bool-solve s@Solver{..} assumps = do-  -- PUSH INCREMENTAL ASSUMPTIONS:-  let-    injector :: Lit -> Bool -> IO Bool-    injector _ False = return False-    injector a True = do-      b <- assume s a-      if not b-        then do                 -- conflict analyze-            (confl :: Clause) <- getNth reason (lit2var a)-            analyzeFinal s confl True-            pushTo conflicts (negateLit a)-            cancelUntil s 0-            return False-        else do-            confl <- propagate s-            if confl /= NullClause-              then do-                  analyzeFinal s confl True-                  cancelUntil s 0-                  return False-              else return True-  good <- simplifyDB s-  x <- if good then foldrM injector True assumps else return False-  if not x-    then return False-    else do-        set' rootLevel =<< decisionLevel s-        -- SOLVE:-        nc <- fromIntegral <$> nClauses s-        let-          while :: Double -> Double -> IO Bool-          while nOfConflicts nOfLearnts = do-            status <- search s (floor nOfConflicts) (floor nOfLearnts)-            if status == lBottom-              then while (1.5 * nOfConflicts) (1.1 * nOfLearnts)-              else cancelUntil s 0 >> return (status == lTrue)-        while 100 (nc / 3.0)---- | Though 'enqueue' is defined in 'Solver', most functions in M114 use @unsafeEnqueue@.-{-# INLINABLE unsafeEnqueue #-}-unsafeEnqueue :: Solver -> Lit -> Clause -> IO ()-unsafeEnqueue s@Solver{..} p from = do-  let v = lit2var p-  setNth assigns v $! if positiveLit p then lTrue else lFalse-  setNth level v =<< decisionLevel s-  setNth reason v from     -- NOTE: @from@ might be NULL!-  pushTo trail p---- | __Pre-condition:__ propagation queue is empty.-{-# INLINE unsafeAssume #-}-unsafeAssume :: Solver -> Lit -> IO ()-unsafeAssume s@Solver{..} p = do-  pushTo trailLim =<< get' trail-  unsafeEnqueue s p NullClause

@@ -1,132 +0,0 @@-{-# LANGUAGE Safe #-}---- | command line option parser for mios-module SAT.Mios.OptionParser-       (-         MiosConfiguration (..)-       , defaultConfiguration-       , MiosProgramOption (..)-       , miosDefaultOption-       , miosOptions-       , miosUsage-       , miosParseOptions-       , miosParseOptionsFromArgs-       , toMiosConf-       )-       where--import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo)-import System.Environment (getArgs)-import SAT.Mios.Types (MiosConfiguration (..), defaultConfiguration)---- | configuration swithces-data MiosProgramOption = MiosProgramOption-                     {-                       _targetFile :: Maybe String-                     , _outputFile :: Maybe String-                     , _confVariableDecayRate :: !Double---                     , _confClauseDecayRate :: Double---                     , _confRandomDecisionRate :: Int-                     , _confCheckAnswer :: !Bool-                     , _confVerbose :: !Bool-                     , _confTimeProbe :: !Bool-                     , _confStatProbe :: !Bool-                     , _confNoAnswer :: !Bool-                     , _validateAssignment :: !Bool-                     , _displayHelp :: !Bool-                     , _displayVersion :: !Bool-                     }---- | default option settings-miosDefaultOption :: MiosProgramOption-miosDefaultOption = MiosProgramOption-  {-    _targetFile = Just ""-  , _outputFile = Nothing-  , _confVariableDecayRate = variableDecayRate defaultConfiguration---  , _confClauseDecayRate = clauseDecayRate defaultConfiguration---  , _confRandomDecisionRate = randomDecisionRate defaultConfiguration-  , _confCheckAnswer = False-  , _confVerbose = False-  , _confTimeProbe = False-  , _confStatProbe = False-  , _confNoAnswer = False-  , _validateAssignment = False-  , _displayHelp = False-  , _displayVersion = False-  }---- | definition of mios option-miosOptions :: [OptDescr (MiosProgramOption -> MiosProgramOption)]-miosOptions =-  [-    Option ['d'] ["variable-decay-rate"]-    (ReqArg (\v c -> c { _confVariableDecayRate = read v }) (show (_confVariableDecayRate miosDefaultOption)))-    "[solver] variable activity decay rate (0.0 - 1.0)"---  , Option ['c'] ["clause-decay-rate"]---    (ReqArg (\v c -> c { _confClauseDecayRate = read v }) (show (_confClauseDecayRate miosDefaultOption)))---    "[solver] clause activity decay rate (0.0 - 1.0)"---  , Option ['r'] ["random-decision-rate"]---    (ReqArg (\v c -> c { _confRandomDecisionRate = read v }) (show (_confRandomDecisionRate miosDefaultOption)))---    "[solver] random selection rate (0 - 1000)"-  , Option [':'] ["validate-assignment"]-    (NoArg (\c -> c { _validateAssignment = True }))-    "[solver] read an assignment from STDIN and validate it"-  , Option [] ["validate"]-    (NoArg (\c -> c { _confCheckAnswer = True }))-    "[solver] self-check the (satisfied) answer"-  , Option ['o'] ["output"]-    (ReqArg (\v c -> c { _outputFile = Just v })"file")-    "[option] filename to store the result"-{--  , Option [] ["stdin"]-    (NoArg (\c -> c { _targetFile = Nothing }))-    "[option] read a CNF from STDIN instead of a file"--}-  , Option ['v'] ["verbose"]-    (NoArg (\c -> c { _confVerbose = True }))-    "[option] display misc information"-  , Option ['X'] ["hide-solution"]-    (NoArg (\c -> c { _confNoAnswer = True }))-    "[option] hide the solution"-  , Option [] ["time"]-    (NoArg (\c -> c { _confTimeProbe = True }))-    "[option] display execution time"-  , Option [] ["stat"]-    (NoArg (\c -> c { _confStatProbe = True }))-    "[option] display statistics information"-  , Option ['h'] ["help"]-    (NoArg (\c -> c { _displayHelp = True }))-    "[misc] display this help message"-  , Option [] ["version"]-    (NoArg (\c -> c { _displayVersion = True }))-    "[misc] display program ID"-  ]---- | generates help message-miosUsage :: String -> String-miosUsage mes = usageInfo mes miosOptions---- | builds "MiosProgramOption" from string given as command option-miosParseOptions :: String -> [String] -> IO MiosProgramOption-miosParseOptions mes argv =-    case getOpt Permute miosOptions argv of-      (o, [], []) -> do-        return $ foldl (flip id) miosDefaultOption o-      (o, (n:_), []) -> do-        let conf = foldl (flip id) miosDefaultOption o-        return $ conf { _targetFile = Just n }-      (_, _, errs) -> ioError (userError (concat errs ++ miosUsage mes))---- | builds "MiosProgramOption" from a String-miosParseOptionsFromArgs :: String -> IO MiosProgramOption-miosParseOptionsFromArgs mes = miosParseOptions mes =<< getArgs---- | converts "MiosProgramOption" into "SIHConfiguration"-toMiosConf :: MiosProgramOption -> MiosConfiguration-toMiosConf opts = MiosConfiguration-                 {-                   variableDecayRate = _confVariableDecayRate opts---                 , clauseDecayRate = _confClauseDecayRate opts---                 , randomDecisionRate = _confRandomDecisionRate opts-                 }

@@ -1,633 +0,0 @@-{-# LANGUAGE-    BangPatterns-  , RecordWildCards-  , ScopedTypeVariables-  , TupleSections-  , ViewPatterns-  #-}-{-# LANGUAGE Safe #-}---- | This is a part of MIOS; main data-module SAT.Mios.Solver-       (-         -- * Solver-         Solver (..)-       , VarHeap-       , newSolver-       , getModel-         -- * Misc Accessors-       , nAssigns-       , nClauses-       , nLearnts-       , decisionLevel-       , valueVar-       , valueLit---       , oldLit-       , locked-         -- * State Modifiers-       , addClause-       , enqueue-       , assume-       , cancelUntil-         -- * Activities-       , claBumpActivity---       , claDecayActivity-       , claRescaleActivityAfterRestart-       , varBumpActivity-       , varDecayActivity-       , claActivityThreshold-         -- * Stats-       , StatIndex (..)-       , getStat-       , setStat-       , incrementStat-       , getStats-       )-        where--import Control.Monad (unless, when)-import SAT.Mios.Types-import SAT.Mios.Clause-import SAT.Mios.ClauseManager---- | __Fig. 2.(p.9)__ Internal State of the solver-data Solver = Solver-              {-{-            Public Interface -}-                model      :: !(Vec Int)         -- ^ If found, this vector has the model-              , conflicts  :: !Stack             -- ^ Set of literals in the case of conflicts-{-            Clause Database -}-              , clauses    :: !ClauseExtManager  -- ^ List of problem constraints.-              , learnts    :: !ClauseExtManager  -- ^ List of learnt clauses.-              , watches    :: !WatcherList       -- ^ list of constraint wathing 'p', literal-indexed-{-            Assignment Management -}-              , assigns    :: !(Vec Int)         -- ^ The current assignments indexed on variables-              , phases     :: !(Vec Int)         -- ^ The last assignments indexed on variables-              , trail      :: !Stack             -- ^ List of assignments in chronological order-              , trailLim   :: !Stack             -- ^ Separator indices for different decision levels in 'trail'.-              , qHead      :: !Int'              -- ^ 'trail' is divided at qHead; assignment part and queue part-              , reason     :: !ClauseVector      -- ^ For each variable, the constraint that implied its value-              , level      :: !(Vec Int)         -- ^ For each variable, the decision level it was assigned-{-            Variable Order -}-              , activities :: !(Vec Double)      -- ^ Heuristic measurement of the activity of a variable-              , order      :: !VarHeap           -- ^ Keeps track of the dynamic variable order.-{-            Configuration -}-              , config     :: !MiosConfiguration -- ^ search paramerters-              , nVars      :: !Int               -- ^ number of variables-{--              -- , claInc     :: !Double'           -- ^ Clause activity increment amount to bump with.-              -- , varDecay   :: !Double'           -- ^ used to set 'varInc'--}-              , varInc     :: !Double'           -- ^ Variable activity increment amount to bump with.-              , rootLevel  :: !Int'              -- ^ Separates incremental and search assumptions.-{-            Working Memory -}-              , ok         :: !Bool'             -- ^ /return value/ holder-              , an'seen    :: !(Vec Int)         -- ^ used in 'SAT.Mios.Main.analyze'-              , an'toClear :: !Stack             -- ^ used in 'SAT.Mios.Main.analyze'-              , an'stack   :: !Stack             -- ^ used in 'SAT.Mios.Main.analyze'-              , an'lastDL  :: !Stack             -- ^ last decision level used in 'SAT.Mios.Main.analyze'-              , litsLearnt :: !Stack             -- ^ used in 'SAT.Mios.Main.analyze' and 'SAT.Mios.Main.search' to create a learnt clause--{--              -- , pr'seen    :: !(Vec Int)         -- ^ used in 'SAT.Mios.Main.propagate'--}-              , stats      :: !(UVector Int)     -- ^ statistics information holder-{--              , lbd'seen   :: !Vec               -- ^ used in lbd computation-              , lbd'key    :: !Int'              -- ^ used in lbd computation--}-              }---- | returns an everything-is-initialized solver from the arguments.-newSolver :: MiosConfiguration -> CNFDescription -> IO Solver-newSolver conf (CNFDescription nv nc _) = do-  Solver-    -- Public Interface-    <$> newVec nv 0                        -- model-    <*> newStack nv                        -- coflict-    -- Clause Database-    <*> newManager nc                      -- clauses-    <*> newManager nc                      -- learnts-    <*> newWatcherList nv 2                -- watches-    -- Assignment Management-    <*> newVec nv lBottom                  -- assigns-    <*> newVec nv lBottom                  -- phases-    <*> newStack nv                        -- trail-    <*> newStack nv                        -- trailLim-    <*> new' 0                             -- qHead-    <*> newClauseVector (nv + 1)           -- reason-    <*> newVec nv (-1)                     -- level-    -- Variable Order-    <*> newVec nv 0                        -- activities-    <*> newVarHeap nv                      -- order-    -- Configuration-    <*> return conf                        -- config-    <*> return nv                          -- nVars---  <*> new' 1.0                           -- claInc---  <*> new' (variableDecayRate conf)      -- varDecay-    <*> new' 1.0                           -- varInc-    <*> new' 0                             -- rootLevel-    -- Working Memory-    <*> new' True                          -- ok-    <*> newVec nv 0                        -- an'seen-    <*> newStack nv                        -- an'toClear-    <*> newStack nv                        -- an'stack---    <*> newVec nv (-1)                     -- pr'seen-    <*> newStack nv                        -- litsLearnt-    <*> newStack nv                        -- lastDL-    <*> newVec (fromEnum EndOfStatIndex) 0 -- stats-{----    <*> newVec nv                        -- lbd'seen---    <*> newInt 0                         -- lbd'key--}------------------------------------------------------------------------------------- Accessors---- | returns the number of current assigments.-{-# INLINE nAssigns #-}-nAssigns :: Solver -> IO Int-nAssigns = get' . trail---- | returns the number of constraints (clauses).-{-# INLINE nClauses #-}-nClauses :: Solver -> IO Int-nClauses = get' . clauses---- | returns the number of learnt clauses.-{-# INLINE nLearnts #-}-nLearnts :: Solver -> IO Int-nLearnts = get' . learnts---- | returns the model as a list of literal.-getModel :: Solver -> IO [Int]-getModel = asList . model---- | returns the current decision level.-{-# INLINE decisionLevel #-}-decisionLevel :: Solver -> IO Int-decisionLevel = get' . trailLim---- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Var'.-{-# INLINE valueVar #-}-valueVar :: Solver -> Var -> IO Int-valueVar = getNth . assigns---- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Lit'.-{-# INLINE valueLit #-}-valueLit :: Solver -> Lit -> IO Int-valueLit (assigns -> a) p = (\x -> if positiveLit p then x else negate x) <$> getNth a (lit2var p)--{---- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Lit' in phases.-{-# INLINE oldLit #-}-oldLit :: Solver -> Lit -> IO Lit-oldLit (phases -> a) (lit2var -> v) = (var2lit v . (== 1)) <$> getNth a v--}---- | __Fig. 7. (p.11)__--- returns @True@ if the clause is locked (used as a reason). __Learnt clauses only__-{-# INLINE locked #-}-locked :: Solver -> Clause -> IO Bool-locked s c = (c ==) <$> (getNth (reason s) . lit2var =<< getNth (lits c) 1)---------------------------------------------------------------------------------- Statistics---- | stat index-data StatIndex =-    NumOfBackjump               -- ^ the number of backjump-  | NumOfRestart                -- ^ the number of restart-  | EndOfStatIndex              -- ^ Don't use this dummy.-  deriving (Bounded, Enum, Eq, Ord, Read, Show)---- | returns the value of 'StatIndex'.-{-# INLINE getStat #-}-getStat :: Solver -> StatIndex -> IO Int-getStat (stats -> v) (fromEnum -> i) = getNth v i---- | sets to 'StatIndex'.-{-# INLINE setStat #-}-setStat :: Solver -> StatIndex -> Int -> IO ()-setStat (stats -> v) (fromEnum -> i) x = setNth v i x---- | increments a stat data corresponding to 'StatIndex'.-{-# INLINE incrementStat #-}-incrementStat :: Solver -> StatIndex -> Int -> IO ()-incrementStat (stats -> v) (fromEnum -> i) k = modifyNth v (+ k) i---- | returns the statistics as a list.-{-# INLINABLE getStats #-}-getStats :: Solver -> IO [(StatIndex, Int)]-getStats (stats -> v) = mapM (\i -> (i, ) <$> getNth v (fromEnum i)) [minBound .. maxBound :: StatIndex]---------------------------------------------------------------------------------- State Modifiers---- | returns @False@ if a conflict has occured.--- This function is called only before the solving phase to register the given clauses.-{-# INLINABLE addClause #-}-addClause :: Solver -> Stack -> IO Bool-addClause s@Solver{..} vecLits = do-  result <- clauseNew s vecLits False-  case result of-   Left b  -> return b   -- No new clause was returned becaues a confilct occured or the clause is a literal-   Right c -> pushTo clauses c >> return True---- | __Fig. 8. (p.12)__ create a new clause and adds it to watcher lists.--- Constructor function for clauses. Returns @False@ if top-level conflict is determined.--- @outClause@ may be set to Null if the new clause is already satisfied under the current--- top-level assignment.------ __Post-condition:__ @ps@ is cleared. For learnt clauses, all--- literals will be false except @lits[0]@ (this by design of the 'analyze' method).--- For the propagation to work, the second watch must be put on the literal which will--- first be unbound by backtracking. (Note that none of the learnt-clause specific things--- needs to done for a user defined contraint type.)------ * @Left False@ if the clause is in a confilct--- * @Left True@ if the clause is satisfied--- * @Right clause@ if the clause is enqueued successfully-{-# INLINABLE clauseNew #-}-clauseNew :: Solver -> Stack -> Bool -> IO (Either Bool Clause)-clauseNew s@Solver{..} ps isLearnt = do-  -- now ps[0] is the number of living literals-  exit <- do-    let-      handle :: Int -> Int -> Int -> IO Bool-      handle j l n      -- removes duplicates, but returns @True@ if this clause is satisfied-        | j > n = return False-        | otherwise = do-            y <- getNth ps j-            case () of-             _ | y == l -> do             -- finds a duplicate-                   swapBetween ps j n-                   modifyNth ps (subtract 1) 0-                   handle j l (n - 1)-             _ | - y == l -> reset ps >> return True -- p and negateLit p occurs in ps-             _ -> handle (j + 1) l n-      loopForLearnt :: Int -> IO Bool-      loopForLearnt i = do-        n <- get' ps-        if n < i-          then return False-          else do-              l <- getNth ps i-              sat <- handle (i + 1) l n-              if sat-                then return True-                else loopForLearnt $ i + 1-      loop :: Int -> IO Bool-      loop i = do-        n <- get' ps-        if n < i-          then return False-          else do-              l <- getNth ps i     -- check the i-th literal's satisfiability-              sat <- valueLit s l  -- any literal in ps is true-              case sat of-               1  -> reset ps >> return True-               -1 -> do-                 swapBetween ps i n-                 modifyNth ps (subtract 1) 0-                 loop i-               _ -> do-                 sat' <- handle (i + 1) l n-                 if sat'-                   then return True-                   else loop $ i + 1-    if isLearnt then loopForLearnt 1 else loop 1-  k <- get' ps-  case k of-   0 -> return (Left exit)-   1 -> do-     l <- getNth ps 1-     Left <$> enqueue s l NullClause-   _ -> do-    -- allocate clause:-     c <- newClauseFromStack isLearnt ps-     let vec = asUVector c-     when isLearnt $ do-       -- Pick a second literal to watch:-       let-         findMax :: Int -> Int -> Int -> IO Int-         findMax ((< k) -> False) j _ = return j-         findMax i j val = do-           v' <- lit2var <$> getNth vec i-           varBumpActivity s v' -- this is a just good chance to bump activities of literals in this clause-           a <- getNth assigns v'-           b <- getNth level v'-           if (a /= lBottom) && (val < b)-             then findMax (i + 1) i b-             else findMax (i + 1) j val-       -- Let @max_i@ be the index of the literal with highest decision level-       max_i <- findMax 0 0 0-       swapBetween vec 1 max_i-       -- check literals occurences-       -- x <- asList c-       -- unless (length x == length (nub x)) $ error "new clause contains a element doubly"-       -- Bumping:-       claBumpActivity s c -- newly learnt clauses should be considered active-     -- Add clause to watcher lists:-     l0 <- negateLit <$> getNth vec 0-     pushClauseWithKey (getNthWatcher watches l0) c 0-     l1 <- negateLit <$> getNth vec 1-     pushClauseWithKey (getNthWatcher watches l1) c 0-     return (Right c)---- | __Fig. 9 (p.14)__--- Puts a new fact on the propagation queue, as well as immediately updating the variable's value--- in the assignment vector. If a conflict arises, @False@ is returned and the propagation queue is--- cleared. The parameter 'from' contains a reference to the constraint from which 'p' was--- propagated (defaults to @Nothing@ if omitted).-{-# INLINABLE enqueue #-}-enqueue :: Solver -> Lit -> Clause -> IO Bool-enqueue s@Solver{..} p from = do-{--  -- bump psedue lbd of @from@-  when (from /= NullClause && learnt from) $ do-    l <- get' (lbd from)-    k <- (12 +) <$> decisionLevel s-    when (k < l) $ set' (lbd from) k--}-  let signumP = if positiveLit p then lTrue else lFalse-  let v = lit2var p-  val <- valueVar s v-  if val /= lBottom-    then do -- Existing consistent assignment -- don't enqueue-        return $ val == signumP-    else do-        -- New fact, store it-        setNth assigns v signumP-        setNth level v =<< decisionLevel s-        setNth reason v from     -- NOTE: @from@ might be NULL!-        pushTo trail p-        return True---- | __Fig. 12 (p.17)__--- returns @False@ if immediate conflict.------ __Pre-condition:__ propagation queue is empty-{-# INLINE assume #-}-assume :: Solver -> Lit -> IO Bool-assume s p = do-  pushTo (trailLim s) =<< get' (trail s)-  enqueue s p NullClause---- | #M22: Revert to the states at given level (keeping all assignment at 'level' but not beyond).-{-# INLINABLE cancelUntil #-}-cancelUntil :: Solver -> Int -> IO ()-cancelUntil s@Solver{..} lvl = do-  dl <- decisionLevel s-  when (lvl < dl) $ do-    let tr = asUVector trail-    let tl = asUVector trailLim-    lim <- getNth tl lvl-    ts <- get' trail-    ls <- get' trailLim-    let-      loopOnTrail :: Int -> IO ()-      loopOnTrail ((lim <=) -> False) = return ()-      loopOnTrail c = do-        x <- lit2var <$> getNth tr c-        setNth phases x =<< getNth assigns x-        setNth assigns x lBottom-        -- #reason to set reason Null-        -- if we don't clear @reason[x] :: Clause@ here, @reason[x]@ remains as locked.-        -- This means we can't reduce it from clause DB and affects the performance.-        setNth reason x NullClause -- 'analyze` uses reason without checking assigns-        -- FIXME: #polarity https://github.com/shnarazk/minisat/blosb/master/core/Solver.cc#L212-        undo s x-        -- insertHeap s x              -- insertVerOrder-        loopOnTrail $ c - 1-    loopOnTrail $ ts - 1-    shrinkBy trail (ts - lim)-    shrinkBy trailLim (ls - lvl)-    set' qHead =<< get' trail---------------------------------------------------------------------------------- VarOrder---- | Interfate to select a decision var based on variable activity.-instance VarOrder Solver where-{--  -- | __Fig. 6. (p.10)__-  -- Creates a new SAT variable in the solver.-  newVar _ = return 0-    -- i <- nVars s-    -- Version 0.4:: push watches =<< newVec      -- push'-    -- Version 0.4:: push watches =<< newVec      -- push'-    -- push undos =<< newVec        -- push'-    -- push reason NullClause       -- push'-    -- push assigns lBottom-    -- push level (-1)-    -- push activities (0.0 :: Double)-    -- newVar order-    -- growQueueSized (i + 1) propQ-    -- return i--}-  {-# SPECIALIZE INLINE update :: Solver -> Var -> IO () #-}-  update = increaseHeap-  {-# SPECIALIZE INLINE undo :: Solver -> Var -> IO () #-}-  undo s v = inHeap s v >>= (`unless` insertHeap s v)-  {-# SPECIALIZE INLINE select :: Solver -> IO Var #-}-  select s = do-    let-      asg = assigns s-      -- | returns the most active var (heap-based implementation)-      loop :: IO Var-      loop = do-        n <- numElementsInHeap s-        if n == 0-          then return 0-          else do-              v <- getHeapRoot s-              x <- getNth asg v-              if x == lBottom then return v else loop-    loop---------------------------------------------------------------------------------- Activities--varActivityThreshold :: Double-varActivityThreshold = 1e100---- | value for rescaling clause activity.-claActivityThreshold :: Double-claActivityThreshold = 1e20---- | __Fig. 14 (p.19)__ Bumping of clause activity-{-# INLINE varBumpActivity #-}-varBumpActivity :: Solver -> Var -> IO ()-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---- | __Fig. 14 (p.19)__-{-# INLINABLE varDecayActivity #-}-varDecayActivity :: Solver -> IO ()-varDecayActivity Solver{..} = modify' varInc (/ variableDecayRate config)--- varDecayActivity Solver{..} = modifyDouble varInc . (flip (/)) =<< getDouble varDecay---- | __Fig. 14 (p.19)__-{-# INLINABLE varRescaleActivity #-}-varRescaleActivity :: Solver -> IO ()-varRescaleActivity Solver{..} = do-  let-    loop ((<= nVars) -> False) = return ()-    loop i = modifyNth activities (/ varActivityThreshold) i >> loop (i + 1)-  loop 1-  modify' varInc (/ varActivityThreshold)---- | __Fig. 14 (p.19)__-{-# INLINE claBumpActivity #-}-claBumpActivity :: Solver -> Clause -> IO ()-claBumpActivity s Clause{..} = do-  dl <- decisionLevel s-  a <- (fromIntegral dl +) <$> get' activity-  set' activity a-  -- set' protected True-  when (claActivityThreshold <= a) $ claRescaleActivity s--{---- | __Fig. 14 (p.19)__-{-# INLINE claDecayActivity #-}-claDecayActivity :: Solver -> IO ()-claDecayActivity Solver{..} = modifyDouble claInc (/ clauseDecayRate config)--}---- | __Fig. 14 (p.19)__-{-# INLINABLE claRescaleActivity #-}-claRescaleActivity :: Solver -> IO ()-claRescaleActivity Solver{..} = do-  vec <- getClauseVector learnts-  n <- get' learnts-  let-    loopOnVector :: Int -> IO ()-    loopOnVector ((< n) -> False) = return ()-    loopOnVector i = do-      c <- getNth vec i-      modify' (activity c) (/ claActivityThreshold)-      loopOnVector $ i + 1-  loopOnVector 0-  -- modifyDouble claInc (/ claActivityThreshold)---- | __Fig. 14 (p.19)__-{-# INLINABLE claRescaleActivityAfterRestart #-}-claRescaleActivityAfterRestart :: Solver -> IO ()-claRescaleActivityAfterRestart Solver{..} = do-  vec <- getClauseVector learnts-  n <- get' learnts-  let-    loopOnVector :: Int -> IO ()-    loopOnVector ((< n) -> False) = return ()-    loopOnVector i = do-      c <- getNth vec i-      d <- get' c-      if d < 9-        then modify' (activity c) sqrt-        else set' (activity c) 0-      set' (protected c) False-      loopOnVector $ i + 1-  loopOnVector 0---------------------------------------------------------------------------------- VarHeap---- | A heap tree built from two 'Vec'.--- This implementation is identical wtih that in Minisat-1.14.--- Note: the zero-th element of @heap@ is used for holding the number of elements.--- Note: VarHeap itself is not a @VarOrder@, because it requires a pointer to solver.-data VarHeap = VarHeap-                {-                  heap :: !Stack  -- order to var-                , idxs :: !Stack  -- var to order (index)-                }--newVarHeap :: Int -> IO VarHeap-newVarHeap n = do-  v1 <- newVec n 0-  v2 <- newVec n 0-  let-    loop :: Int -> IO ()-    loop ((<= n) -> False) = set' v1 n >> set' v2 n-    loop i = setNth v1 i i >> setNth v2 i i >> loop (i + 1)-  loop 1-  return $ VarHeap v1 v2--{-# INLINE numElementsInHeap #-}-numElementsInHeap :: Solver -> IO Int-numElementsInHeap = get' . heap . order--{-# INLINE inHeap #-}-inHeap :: Solver -> Var -> IO Bool-inHeap (order -> idxs -> at) n = (/= 0) <$> getNth at n--{-# INLINE increaseHeap #-}-increaseHeap :: Solver -> Int -> IO ()-increaseHeap s@(order -> idxs -> at) n = inHeap s n >>= (`when` (percolateUp s =<< getNth at n))--{-# INLINABLE percolateUp #-}-percolateUp :: Solver -> Int -> IO ()-percolateUp Solver{..} start = do-  let VarHeap to at = order-  v <- getNth to start-  ac <- getNth activities v-  let-    loop :: Int -> IO ()-    loop i = do-      let iP = div i 2          -- parent-      if iP == 0-        then setNth to i v >> setNth at v i -- end-        else do-            v' <- getNth to iP-            acP <- getNth activities v'-            if ac > acP-              then setNth to i v' >> setNth at v' i >> loop iP -- loop-              else setNth to i v >> setNth at v i              -- end-  loop start--{-# INLINABLE percolateDown #-}-percolateDown :: Solver -> Int -> IO ()-percolateDown Solver{..} start = do-  let (VarHeap to at) = order-  n <- getNth to 0-  v <- getNth to start-  ac <- getNth activities v-  let-    loop :: Int -> IO ()-    loop i = do-      let iL = 2 * i            -- left-      if iL <= n-        then do-            let iR = iL + 1     -- right-            l <- getNth to iL-            r <- getNth to iR-            acL <- getNth activities l-            acR <- getNth activities r-            let (ci, child, ac') = if iR <= n && acL < acR then (iR, r, acR) else (iL, l, acL)-            if ac' > ac-              then setNth to i child >> setNth at child i >> loop ci-              else setNth to i v >> setNth at v i -- end-        else setNth to i v >> setNth at v i       -- end-  loop start--{-# INLINABLE insertHeap #-}-insertHeap :: Solver -> Var -> IO ()-insertHeap s@(order -> VarHeap to at) v = do-  n <- (1 +) <$> getNth to 0-  setNth at v n-  setNth to n v-  set' to n-  percolateUp s n---- | returns the value on the root (renamed from @getmin@).-{-# INLINABLE getHeapRoot #-}-getHeapRoot :: Solver -> IO Int-getHeapRoot s@(order -> VarHeap to at) = do-  r <- getNth to 1-  l <- getNth to =<< getNth to 0 -- the last element's value-  setNth to 1 l-  setNth at l 1-  setNth at r 0-  modifyNth to (subtract 1) 0 -- pop-  n <- getNth to 0-  when (1 < n) $ percolateDown s 1-  return r

@@ -1,257 +0,0 @@-{-# LANGUAGE-    BangPatterns-  , MultiParamTypeClasses-  #-}-{-# LANGUAGE Safe #-}---- | Basic data types used throughout mios.-module SAT.Mios.Types-       (-         module SAT.Mios.Vec-         -- *  Variable-       , Var-       , bottomVar-       , int2var-         -- * Internal encoded Literal-       , Lit-       , lit2int-       , int2lit-       , bottomLit---       , newLit-       , positiveLit-       , lit2var-       , var2lit-       , negateLit-         -- * Assignment on the lifted Bool domain---       , LiftedBool (..)---       , lbool-       , lFalse-       , lTrue-       , lBottom-       , VarOrder (..)-         -- * CNF-       , CNFDescription (..)-         -- * Solver Configuration-       , MiosConfiguration (..)-       , defaultConfiguration-       )-       where--import Data.Bits-import SAT.Mios.Vec---- | represents "Var".-type Var = Int---- | Special constant in 'Var' (p.7)-bottomVar :: Var-bottomVar = 0---- | converts a usual Int as literal to an internal 'Var' presentation.------ >>> int2var 1--- 1  -- the first literal is the first variable--- >>> int2var 2--- 2  -- literal @2@ is variable 2--- >>> int2var (-2)--- 2 -- literal @-2@ is corresponding to variable 2----{-# INLINE int2var #-}-int2var :: Int -> Int-int2var = abs---- | The literal data has an 'index' method which converts the literal to--- a "small" integer suitable for array indexing. The 'var'  method returns--- the underlying variable of the literal, and the 'sign' method if the literal--- is signed (False for /x/ and True for /-x/).-type Lit = Int---- | Special constant in 'Lit' (p.7)-bottomLit :: Lit-bottomLit = 0--{---- | converts "Var" into 'Lit'-newLit :: Var -> Lit-newLit = error "newLit undefined"--}---- | returns @True@ if the literal is positive-{-# INLINE positiveLit #-}-positiveLit :: Lit -> Bool-positiveLit = even---- | negates literal------ >>> negateLit 2--- 3--- >>> negateLit 3--- 2--- >>> negateLit 4--- 5--- >>> negateLit 5--- 4-{-# INLINE negateLit #-}-negateLit :: Lit -> Lit-negateLit l = complementBit l 0 -- if even l then l + 1 else l - 1------------------------------------------------------------ Var--------------------------------------------- | converts 'Lit' into 'Var'.------ >>> lit2var 2--- 1--- >>> lit2var 3--- 1--- >>> lit2var 4--- 2--- >>> lit2var 5--- 2-{-# INLINE lit2var #-}-lit2var :: Lit -> Var-lit2var !n = shiftR n 1---- | converts a 'Var' to the corresponing literal.------ >>> var2lit 1 True--- 2--- >>> var2lit 1 False--- 3--- >>> var2lit 2 True--- 4--- >>> var2lit 2 False--- 5-{-# INLINE var2lit #-}-var2lit :: Var -> Bool -> Lit-var2lit !v True = shiftL v 1-var2lit !v _ = shiftL v 1 + 1------------------------------------------------------------ Int--------------------------------------------- | converts 'Int' into 'Lit' as @lit2int . int2lit == id@.------ >>> int2lit 1--- 2--- >>> int2lit (-1)--- 3--- >>> int2lit 2--- 4--- >>> int2lit (-2)--- 5----{-# INLINE int2lit #-}-int2lit :: Int -> Lit-int2lit n-  | 0 < n = 2 * n-  | otherwise = -2 * n + 1---- | converts `Lit' into 'Int' as @int2lit . lit2int == id@.------ >>> lit2int 2--- 1--- >>> lit2int 3--- -1--- >>> lit2int 4--- 2--- >>> lit2int 5--- -2-{-# INLINE lit2int #-}-lit2int :: Lit -> Int-lit2int l = case divMod l 2 of-  (i, 0) -> i-  (i, _) -> - i--{---- | Lifted Boolean domain (p.7) that extends 'Bool' with "⊥" means /undefined/--- design note: _|_ should be null = 0; True literals are coded to even numbers. So it should be 2.-data LiftedBool = Bottom | LFalse | LTrue-  deriving (Bounded, Eq, Ord, Read, Show)--instance Enum LiftedBool where-  {-# SPECIALIZE INLINE toEnum :: Int -> LiftedBool #-}-  toEnum        1 = LTrue-  toEnum     (-1) = LFalse-  toEnum        _ = Bottom-  {-# SPECIALIZE INLINE fromEnum :: LiftedBool -> Int #-}-  fromEnum Bottom = 0-  fromEnum LFalse = 1-  fromEnum LTrue  = 2---- | converts 'Bool' into 'LBool'-{-# INLINE lbool #-}-lbool :: Bool -> LiftedBool-lbool True = LTrue-lbool False = LFalse--}---- | /FALSE/ on the Lifted Bool domain-lFalse:: Int-lFalse = -1---- | /TRUE/ on the Lifted Bool domain-lTrue :: Int-lTrue = 1---- | /UNDEFINED/ on the Lifted Bool domain-lBottom :: Int-lBottom = 0---- | Assisting ADT for the dynamic variable ordering of the solver.--- The constructor takes references to the assignment vector and the activity--- vector of the solver. The method 'select' will return the unassigned variable--- with the highest activity.-class VarOrder o where-{--  -- | constructor-  newVarOrder :: (VecFamily v1 Bool, VecFamily v2 Double) => v1 -> v2 -> IO o-  newVarOrder _ _ = error "newVarOrder undefined"--  -- | Called when a new variable is created.-  newVar :: o -> IO Var-  newVar = error "newVar undefined"--}-  -- | should be called when a variable has increased in activity.-  update :: o -> Var -> IO ()-  update _  = error "update undefined"-{--  -- | should be called when all variables have been assigned.-  updateAll :: o -> IO ()-  updateAll = error "updateAll undefined"--}-  -- | should be called when a variable becomes unbound (may be selected again).-  undo :: o -> Var -> IO ()-  undo _ _  = error "undo undefined"--  -- | returns a new, unassigned var as the next decision.-  select :: o -> IO Var-  select    = error "select undefined"---- | Misc information on a CNF-data CNFDescription = CNFDescription-  {-    _numberOfVariables :: !Int           -- ^ the number of variables-  , _numberOfClauses :: !Int             -- ^ the number of clauses-  , _pathname :: Maybe FilePath          -- ^ given filename-  }-  deriving (Eq, Ord, Show)---- | Solver's parameters; random decision rate was dropped.-data MiosConfiguration = MiosConfiguration-                         {-                           variableDecayRate  :: !Double  -- ^ decay rate for variable activity---                         , clauseDecayRate    :: !Double  -- ^ decay rate for clause activity-                         }---- | dafault configuration------ * Minisat-1.14 uses @(0.95, 0.999, 0.2 = 20 / 1000)@.--- * Minisat-2.20 uses @(0.95, 0.999, 0)@.--- * Gulcose-4.0  uses @(0.8 , 0.999, 0)@.--- * Mios-1.2     uses @(0.95, 0.999, 0)@.----defaultConfiguration :: MiosConfiguration-defaultConfiguration = MiosConfiguration 0.95 {- 0.999 -} {- 0 -}

@@ -1,244 +0,0 @@-{-# LANGUAGE BangPatterns, FlexibleInstances, ViewPatterns, UndecidableInstances #-}-{-# LANGUAGE Safe #-}---- | Boolean Expression module to build CNF from arbitrary expressions--- Tseitin translation: http://en.wikipedia.org/wiki/Tseitin_transformation-module SAT.Mios.Util.BoolExp-       (-         -- * Class & Type-         BoolComponent (..)-       , BoolForm (..)-         -- * Expression contructors-       , (-|-)-       , (-&-)-       , (-=-)-       , (-!-)-       , (->-)-       , neg-         -- * List Operation-       , disjunctionOf-       , (-|||-)-       , conjunctionOf-       , (-&&&-)-         -- * Convert function-       , asList-       , asList_-       , asLatex-       , asLatex_-       , numberOfVariables-       , numberOfClauses-       , tseitinBase-       )-       where--import Data.List (foldl', intercalate)---- | the start index for the generated variables by Tseitin encoding-tseitinBase :: Int-tseitinBase = 1600000--data L = L Int---- | class of objects that can be interpeted as a bool expression-class BoolComponent a where-  toBF :: a -> BoolForm   -- lift to BoolForm---- | CNF expression-data BoolForm = Cnf (Int, Int) [[Int]]-    deriving (Eq, Show)--instance BoolComponent Int where-  toBF a = Cnf (abs a, max tseitinBase (abs a)) [[a]]--instance BoolComponent L where-  toBF (L a) = Cnf (abs a, max tseitinBase (abs a)) [[a]]--instance BoolComponent [Char] where-  toBF (read -> a) = Cnf (abs a, max tseitinBase (abs a)) [[a]]--instance BoolComponent BoolForm where-  toBF = id---- | returns the number of variables in the 'BoolForm'-numberOfVariables :: BoolForm -> Int-numberOfVariables (Cnf (a, b) _) = a + b - tseitinBase---- | returns the number of clauses in the 'BoolForm'-numberOfClauses :: BoolForm -> Int-numberOfClauses (Cnf _ l) = length l--boolFormTrue = Cnf (-1, 1) []-boolFormFalse = Cnf (-1, -1) []--instance BoolComponent Bool where-  toBF True = boolFormTrue-  toBF False = boolFormFalse--isTrue :: BoolForm -> Bool-isTrue = (== boolFormTrue)--isFalse :: BoolForm -> Bool-isFalse = (== boolFormFalse)---- | return a 'clause' list only if it contains some real clause (not a literal)-clausesOf :: BoolForm -> [[Int]]-clausesOf cnf@(Cnf _ [[]]) = []-clausesOf cnf@(Cnf _ [[x]]) = []-clausesOf cnf@(Cnf _ l) = l--maxRank :: BoolForm -> Int-maxRank (Cnf (n, _) _) = n---- | returns the number of valiable used as the output of this expression.--- and returns itself it the expression is a literal.--- Otherwise the number is a integer larger than 'tseitinBase'.--- Therefore @1 + max tseitinBase the-returned-value@ is the next literal variable for future.-tseitinNumber :: BoolForm -> Int-tseitinNumber (Cnf (m, n) [[x]]) = x-tseitinNumber (Cnf (_, n) _) = n--renumber :: Int -> BoolForm -> (BoolForm, Int)-renumber base (Cnf (m, n) l)-  | l == [] = (Cnf (m, n) l, 0)-  | tseitinBase < base = (Cnf (m, n') l', n')-  | otherwise = (Cnf (n', tseitinBase) l', n')-  where-    l' = map (map f) l-    n' = maximum $ map maximum l'-    offset = base - tseitinBase - 1-    f x = if abs x < tseitinBase then x else signum x * (abs x + offset)--instance Ord BoolForm where-  compare (Cnf _ a) (Cnf _ b) = compare a b---- | disjunction constructor------ >>> asList $ "3" -|- "4"--- [[3,4,-5],[-3,5],[-4,5]]------ >>> asList (("3" -|- "4") -|- "-1")--- [[3,4,-5],[-3,5],[-4,5],[5,-1,-6],[-5,6],[1,6]]----(-|-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm-(toBF -> e1) -|- (toBF -> e2')-  | isTrue e1 || isTrue e2' = boolFormTrue-  | isFalse e1 && isFalse e2' = boolFormFalse-  | isFalse e1 = e2'-  | isFalse e2' = e1-  | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[a, b, - c], [- a, c], [- b, c]]-  where-    a = tseitinNumber e1-    (e2, b) = renumber (1 + max tseitinBase a) e2'-    m = max (maxRank e1) (maxRank e2)-    c = 1 + max tseitinBase (max a b)---- | conjunction constructor------ >>> asList $ "3" -&- "-2"--- [[-3,2,4],[3,-4],[-2,-4]]------ >>> asList $ "3" -|- ("1" -&- "2")--- [[-1,-2,4],[1,-4],[2,-4],[3,4,-5],[-3,5],[-4,5]]----(-&-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm-(toBF -> e1) -&- (toBF -> e2')-  | isTrue e1 && isTrue e2' = boolFormTrue-  | isFalse e1 || isFalse e2' = boolFormFalse-  | isTrue e1 = e2'-  | isTrue e2' = e1-  | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[- a, - b, c], [a, - c], [b, - c]]-  where-    a = tseitinNumber e1-    (e2, b) = renumber (1 + max tseitinBase a) e2'-    m = max (maxRank e1) (maxRank e2)-    c = 1 + max tseitinBase (max a b)---- | negate a form------ >>> asList $ neg ("1" -|- "2")--- [[1,2,-3],[-1,3],[-2,3],[-3,-4],[3,4]]-neg :: (BoolComponent a) => a -> BoolForm-neg (toBF -> e) =-  Cnf (m, c) $ clausesOf e ++ [[- a, - c], [a, c]]-  where-    a = tseitinNumber e-    m = maxRank e-    c = 1 + max tseitinBase a---- | equal on BoolForm-(-=-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm-(toBF -> e1) -=- (toBF -> e2) = (e1 -&- e2) -|- (neg e1 -&- neg e2)---- | negation on BoolForm-(-!-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm-(toBF -> e1) -!- (toBF -> e2) = (neg e1 -&- e2) -|- (e1 -&- neg e2)---- | implication as a short cut------ >>> asList ("1" ->- "2")--- [[-1,-3],[1,3],[3,2,-4],[-3,4],[-2,4]]-(->-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm-(toBF -> a) ->- (toBF -> b) = (neg a) -|- b---- | merge [BoolForm] by '(-|-)'-disjunctionOf :: [BoolForm] -> BoolForm-disjunctionOf [] = boolFormFalse-disjunctionOf (x:l) = foldl' (-|-) x l---- | an alias of 'disjunctionOf'-(-|||-) = disjunctionOf---- | merge [BoolForm] by '(-&-)'-conjunctionOf :: [BoolForm] -> BoolForm-conjunctionOf [] = boolFormTrue-conjunctionOf (x:l) = foldl' (-&-) x l---- | an alias of 'conjunctionOf'-(-&&&-) = conjunctionOf---- | converts a BoolForm to "[[Int]]"-asList_ :: BoolForm -> [[Int]]-asList_ cnf@(Cnf (m,_) _)-  | isTrue cnf = []-  | isFalse cnf = [[]]-  | otherwise = l'-  where-    (Cnf _ l', _) = renumber (m + 1) cnf---- | converts a *satisfied* BoolForm to "[[Int]]"-asList :: BoolForm -> [[Int]]-asList cnf@(Cnf (m,n) l)-  | isTrue cnf = []-  | isFalse cnf = [[]]-  | n <= tseitinBase = l-  | otherwise = [m'] : l'-  where-    (Cnf (m', _) l', _) = renumber (m + 1) cnf---- | make latex string from CNF, using 'asList_'------ >>> asLatex $ "3" -|- "4"--- "\\begin{displaymath}\n( x_{3} \\vee x_{4} )\n\\end{displaymath}\n"----asLatex_ :: BoolForm -> String-asLatex_ b = beg ++ s ++ end-  where-    beg = "\\begin{displaymath}\n"-    end = "\n\\end{displaymath}\n"-    s = intercalate " \\wedge " [ makeClause c | c <- asList_ b]-    makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")"-    makeLiteral l-      | 0 < l = " x_{" ++ show l ++ "} "-      | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} "---- | make latex string from CNF, using 'asList'-asLatex :: BoolForm -> String-asLatex b = beg ++ s ++ end-  where-    beg = "\\begin{displaymath}\n"-    end = "\n\\end{displaymath}\n"-    s = intercalate " \\wedge " [ makeClause c | c <- asList b]-    makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")"-    makeLiteral l-      | 0 < l = " x_{" ++ show l ++ "} "-      | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} "

@@ -1,31 +0,0 @@-{-# LANGUAGE Safe #-}---- | Read/Write a CNF file only with ghc standard libraries-module SAT.Mios.Util.DIMACS-       (-         -- * Input-         fromFile-       , clauseListFromFile-       , fromMinisatOutput-       , clauseListFromMinisatOutput-         -- * Output-       , toFile-       , toDIMACSString-       , asDIMACSString-       , asDIMACSString_-         -- * Bool Operation-       , module SAT.Mios.Util.BoolExp-       )-       where-import SAT.Mios.Util.DIMACS.Reader-import SAT.Mios.Util.DIMACS.Writer-import SAT.Mios.Util.DIMACS.MinisatReader-import SAT.Mios.Util.BoolExp---- | String from BoolFrom-asDIMACSString :: BoolForm -> String-asDIMACSString = toDIMACSString . asList---- | String from BoolFrom-asDIMACSString_ :: BoolForm -> String-asDIMACSString_ = toDIMACSString . asList_

@@ -1,73 +0,0 @@-{-# LANGUAGE Safe #-}---- | Read an output file of minisat-module SAT.Mios.Util.DIMACS.MinisatReader-       (-         -- * Interface-         fromMinisatOutput-       , clauseListFromMinisatOutput-       )-       where--- import Control.Applicative ((<$>), (<*>), (<*), (*>))-import Data.Char-import Text.ParserCombinators.ReadP---- parser--- |parse a non-signed integer-{-# INLINE pint #-}-pint = do-  n <- munch isDigit-  return (read n :: Int)--{-# INLINE mint #-}-mint = do-  char '-'-  n <- munch isDigit-  return (- (read n::Int))---- |parse a (signed) integer-{-# INLINE int #-}-int = mint <++ pint---- |return integer list that terminates at zero-{-# INLINE seqNums #-}-seqNums = do-  skipSpaces-  x <- int-  skipSpaces-  if (x == 0) then return []  else (x :) <$> seqNums---- |top level interface for parsing CNF-{-# INLINE parseMinisatOutput #-}-parseMinisatOutput :: ReadP ((Int, Int), [Int])-parseMinisatOutput = do-  string "SAT"-  skipSpaces-  l <- seqNums-  return ((length l,0), l)---- |read a minisat output:--- ((numbefOfVariables, 0), [Literal])------ >>>  fromFile "result"--- ((3, 0), [1, -2, 3])----{-# INLINE fromMinisatOutput #-}-fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int]))-fromMinisatOutput f = do-  c <- readFile f-  case readP_to_S parseMinisatOutput c of-    [(a, _)] -> return $ Just a-    _ -> return Nothing---- | return clauses as [[Int]] from 'file'------ >>> clauseListFromMinisatOutput "result"--- [1,-2,3]----clauseListFromMinisatOutput :: FilePath -> IO [Int]-clauseListFromMinisatOutput l = do-  res <- fromMinisatOutput l-  case res of-    Just p -> return (snd p)-    _ -> return []

@@ -1,130 +0,0 @@-{-# LANGUAGE Safe #-}---- | Read a CNF file without haskell-platform-module SAT.Mios.Util.DIMACS.Reader-       (-         -- * Interface-         fromFile-       , clauseListFromFile-       )-       where-import Control.Applicative ((<$>), (<*>), (<*), (*>))-import Data.Char-import Text.ParserCombinators.ReadP---- parser-{-# INLINE newline #-}-newline = char '\n'--{-# INLINE digit #-}-digit = satisfy isDigit--{-# INLINE spaces #-}-spaces = munch (`elem` " \t")--{-# INLINE noneOf #-}-noneOf s = satisfy (`notElem` s)---- |parse a non-signed integer-{-# INLINE pint #-}-pint = do-  n <- munch isDigit-  return (read n :: Int)--{-# INLINE mint #-}-mint = do-  char '-'-  n <- munch isDigit-  return (- (read n::Int))---- |parse a (signed) integer-{-# INLINE int #-}-int = mint <++ pint---- |Parse something like: p FORMAT VARIABLES CLAUSES-{-# INLINE problemLine #-}-problemLine = do-  char 'p'-  skipSpaces-  (string "cnf" <++ string "CNF")-  skipSpaces-  vars <- pint-  skipSpaces-  clas <- pint-  spaces-  newline-  return (vars, clas)---- |Parse something like: c This in an example of a comment line.-{-# INLINE commentLines #-}-commentLines = do-  l <- look-  if (head l)  == 'c'-    then do-      munch ('\n' /=)-      newline-      commentLines-    else return ()--_commentLines = do-  char 'c'-  munch ('\n' /=)-  newline-  l <- look-  if (head l)  == 'c' then commentLines else return ()---- |Parse the preamble part-{-# INLINE preambleCNF #-}-preambleCNF = do-  commentLines-  problemLine---- |return integer list that terminates at zero-{-# INLINE seqNums #-}-seqNums = do-  skipSpaces-  x <- int-  skipSpaces-  if (x == 0) then return []  else (x :) <$> seqNums---- |Parse something like: 1 -2 0 4 0 -3 0-{-# INLINE parseClauses #-}-parseClauses :: Int -> ReadP [[Int]]-parseClauses n = count n seqNums---- |top level interface for parsing CNF-{-# INLINE parseCNF #-}-parseCNF :: ReadP ((Int, Int), [[Int]])-parseCNF = do-  a <- preambleCNF-  b <- parseClauses (snd a)-  return (a, b)---- |driver:: String -> Either ParseError Int-driver input = readP_to_S (parseClauses 1) input---- |read a CNF file and return:--- ((numbefOfVariables, numberOfClauses), [Literal])------ >>> fromFile "acnf"--- ((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]]----{-# INLINE fromFile #-}-fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]]))-fromFile f = do-  c <- readFile f-  case readP_to_S parseCNF c of-    [(a, _)] -> return $ Just a-    _ -> return Nothing---- | return clauses as [[Int]] from 'file'------ >>> clauseListFromFile "a.cnf"--- [[1, 2], [-2, 3], [-1, 2, -3], [3]]----clauseListFromFile :: FilePath -> IO [[Int]]-clauseListFromFile l = do-  res <- fromFile l-  case res of-    Just (_, l) -> return l-    _ -> return []

@@ -1,58 +0,0 @@-{-# LANGUAGE Safe #-}---- | Write SAT data to DIMACS file-module SAT.Mios.Util.DIMACS.Writer-       (-         -- * Interface-         toFile-       , toDIMACSString-       , toString-       , toLatexString-       )-       where-import Data.List (intercalate, nub, sort)-import System.IO---- | Write the DIMACS to file 'f', using 'toDIMACSString'-toFile :: FilePath -> [[Int]] -> IO ()-toFile f l = writeFile f $ toDIMACSString l---- | Convert [Clause] to String, where Clause is [Int]------ >>> toDIMACSString []--- "p cnf 0 0\n"------ >>> toDIMACSString [[-1, 2], [-3, -4]]--- "p cnf 4 2\n-1 2 0\n-3 -4 0\n"------ >>> toDIMACSString [[1], [-2], [-3, -4], [1,2,3,4]]--- "p cnf 4 4\n1 0\n-2 0\n-3 -4 0\n1 2 3 4 0\n"----toDIMACSString :: [[Int]] -> String-toDIMACSString l = hdr ++ str-  where-    hdr = "p cnf " ++ show numV ++ " " ++ show numC ++ "\n"-    numC = length l-    numV = last $ nub $ sort $ map abs $ concat l-    str = concat [intercalate " " (map show c) ++ " 0\n" | c <- l]---- | converts @[[Int]]@ to a String-toString  :: [[Int]] -> String -> String -> String-toString l and' or' = intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l]-  where-    lit x-      | 0 <= x = "X" ++ show x-      | otherwise = "-X" ++ show (abs x)-    a = pad and'-    o = pad or'-    pad s = " " ++ s ++ " "---- | converts @[[Int]]@ to a LaTeX expression-toLatexString  :: [[Int]] -> String-toLatexString l = "\\begin{eqnarray*}\n" ++ intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l] ++ "\n\\end{eqnarray*}"-  where-    lit x-      | 0 <= x = "X_{" ++ show x ++ "}"-      | otherwise = "\\overline{X_{" ++ show (abs x) ++ "}}"-    a = " \n\\wedge "-    o = " \\vee "

@@ -1,47 +0,0 @@-{-# LANGUAGE-    ViewPatterns-  #-}-{-# LANGUAGE Safe #-}---- | validate an assignment-module SAT.Mios.Validator-       (-         validate-       )-       where--import Data.Foldable (toList)-import SAT.Mios.Types-import SAT.Mios.Clause-import SAT.Mios.ClauseManager-import SAT.Mios.Solver---- | validates the assignment even if the implementation of 'Solver' is wrong; we re-implement some functions here.-validate :: Traversable t => Solver -> t Int -> IO Bool-validate s (toList -> map int2lit -> lst) = do-  assignment <- newVec (1 + nVars s) (0 :: Int) :: IO (Vec Int)-  vec <- getClauseVector (clauses s)-  nc <- get' (clauses s)-  let-    inject :: Lit -> IO ()-    inject l = setNth assignment (lit2var l) $ if positiveLit l then lTrue else lFalse-    -- returns True if the literal is satisfied under the assignment-    satisfied :: Lit -> IO Bool-    satisfied l-      | positiveLit l = (lTrue ==) <$> getNth assignment (lit2var l)-      | otherwise     = (lFalse ==) <$> getNth assignment (lit2var l)-    -- returns True is any literal in the given list-    satAny :: [Lit] -> IO Bool-    satAny [] = return False-    satAny (l:ls) = do-      sat' <- satisfied l-      if sat' then return True else satAny ls-    -- traverses all clauses in 'clauses'-    loopOnVector :: Int -> IO Bool-    loopOnVector ((< nc) -> False) = return True-    loopOnVector i = do-      sat' <- satAny =<< asList =<< getNth vec i-      if sat' then loopOnVector (i + 1) else return False-  if null lst-    then error "validator got an empty assignment."-    else mapM_ inject lst >> loopOnVector 0

@@ -1,276 +0,0 @@-{-# LANGUAGE-    BangPatterns-  , FlexibleContexts-  , FlexibleInstances-  , FunctionalDependencies-  , MultiParamTypeClasses-  , TypeFamilies-  #-}-{-# LANGUAGE Trustworthy #-}---- | Abstraction Layer for Mutable Vectors-module SAT.Mios.Vec-       (-         -- * Vector class-         VecFamily (..)-         -- * Vectors-       , UVector-       , Vec (..)-         -- * SingleStorage-       , SingleStorage (..)-       , Bool'-       , Double'-       , Int'-         -- * Stack-       , StackFamily (..)-       , Stack-       , newStackFromList-       )-       where--import qualified Data.Vector.Unboxed as U-import qualified Data.Vector.Unboxed.Mutable as UV---- | Interface on vectors.-class VecFamily v a | v -> a where-  -- | returns the /n/-th value.-  getNth ::v -> Int -> IO a-  -- | sets the /n/-th value.-  setNth :: v -> Int -> a -> IO ()-  -- | erases all elements in it.-  reset:: v -> IO ()-  -- | converts to an Int vector.-  asUVector :: (a ~ Int) => v -> UVector Int-  -- | returns the /n/-th value (index starts from zero in any case).-  -- | swaps two elements.-  swapBetween :: v -> Int -> Int -> IO ()-  -- | calls the update function.-  modifyNth :: v -> (a -> a) -> Int -> IO ()-  -- | returns a new vector.-  newVec :: Int -> a -> IO v-  -- | sets all elements.-  setAll :: v -> a -> IO ()-  -- | extends the size of stack by /n/; note: values in new elements aren't initialized maybe.-  growBy :: v -> Int -> IO v-  -- | converts to a list.-  asList :: v -> IO [a]-  {-# MINIMAL getNth, setNth #-}-  reset = error "no default method: reset"-  asUVector = error "no default method: asUVector"-  swapBetween = error "no default method: swapBetween"-  modifyNth = error "no default method: modifyNth"-  newVec = error "no default method: newVec"-  setAll = error "no default method: setAll"-  asList = error "no default method: asList"-  growBy = error "no default method: growBy"-{--  -- | (FOR DEBUG) dump the contents.-  dump :: Show a => String -> v -> IO String-  dump msg v = (msg ++) . show <$> asList v--}---------------------------------------------------------------------------------- UVector---- | A thin abstract layer for Mutable unboxed Vector-type UVector a = UV.IOVector a--instance VecFamily (UVector Int) Int where-  {-# SPECIALIZE INLINE getNth :: UVector Int -> Int -> IO Int #-}-  getNth = UV.unsafeRead-  {-# SPECIALIZE INLINE setNth :: UVector Int -> Int -> Int -> IO () #-}-  setNth = UV.unsafeWrite-  {-# SPECIALIZE INLINE modifyNth :: UVector Int -> (Int -> Int) -> Int -> IO () #-}-  modifyNth = UV.unsafeModify-  {-# SPECIALIZE INLINE swapBetween:: UVector Int -> Int -> Int -> IO () #-}-  swapBetween = UV.unsafeSwap-  {-# SPECIALIZE INLINE newVec :: Int -> Int -> IO (UVector Int) #-}-  newVec n 0 = UV.new n-  newVec n x = do-    v <- UV.new n-    UV.set v x-    return v-  {-# SPECIALIZE INLINE setAll :: UVector Int -> Int -> IO () #-}-  setAll = UV.set-  {-# SPECIALIZE INLINE growBy :: UVector Int -> Int -> IO (UVector Int) #-}-  growBy = UV.unsafeGrow-  asList v = mapM (UV.unsafeRead v) [0 .. UV.length v - 1]--instance VecFamily (UVector Double) Double where-  {-# SPECIALIZE INLINE getNth :: UVector Double -> Int -> IO Double #-}-  getNth = UV.unsafeRead-  {-# SPECIALIZE INLINE setNth :: UVector Double -> Int -> Double -> IO () #-}-  setNth = UV.unsafeWrite-  {-# SPECIALIZE INLINE modifyNth :: UVector Double -> (Double -> Double) -> Int -> IO () #-}-  modifyNth = UV.unsafeModify-  {-# SPECIALIZE INLINE swapBetween:: UVector Double -> Int -> Int -> IO () #-}-  swapBetween = UV.unsafeSwap-  {-# SPECIALIZE INLINE newVec :: Int -> Double -> IO (UVector Double) #-}-  newVec n x = do-    v <- UV.new n-    UV.set v x-    return v-  {-# SPECIALIZE INLINE setAll :: UVector Double -> Double -> IO () #-}-  setAll = UV.set-  {-# SPECIALIZE INLINE growBy :: UVector Double -> Int -> IO (UVector Double) #-}-  growBy = UV.unsafeGrow-  asList v = mapM (UV.unsafeRead v) [0 .. UV.length v - 1]---------------------------------------------------------------------------------- Vec---- | Another abstraction layer on 'UVector'.------ __Note__: the 0-th element of @Vec Int@ is reserved for internal tasks. If you want to use it, use @UVector Int@.-newtype Vec a  = Vec (UVector a)--instance VecFamily (Vec Int) Int where-  {-# SPECIALIZE INLINE getNth :: Vec Int -> Int -> IO Int #-}-  getNth (Vec v) = UV.unsafeRead v-  {-# SPECIALIZE INLINE setNth :: Vec Int -> Int -> Int -> IO () #-}-  setNth (Vec v) = UV.unsafeWrite v-  {-# SPECIALIZE INLINE reset :: Vec Int -> IO () #-}-  reset (Vec v) = setNth v 0 0-  {-# SPECIALIZE INLINE asUVector :: Vec Int -> UVector Int #-}-  asUVector (Vec a) = UV.unsafeTail a-  {-# SPECIALIZE INLINE modifyNth :: Vec Int -> (Int -> Int) -> Int -> IO () #-}-  modifyNth (Vec v) = UV.unsafeModify v-  {-# SPECIALIZE INLINE swapBetween :: Vec Int -> Int -> Int -> IO () #-}-  swapBetween (Vec v) = UV.unsafeSwap v-  {-# SPECIALIZE INLINE newVec :: Int -> Int -> IO (Vec Int) #-}-  newVec n x = Vec <$> newVec (n + 1) x-  {-# SPECIALIZE INLINE setAll :: Vec Int -> Int -> IO () #-}-  setAll (Vec v) = UV.set v-  {-# SPECIALIZE INLINE growBy :: Vec Int -> Int -> IO (Vec Int) #-}-  growBy (Vec v) n = Vec <$> UV.unsafeGrow v n-  asList (Vec v) = mapM (getNth v) [1 .. UV.length v - 1]--instance VecFamily (Vec Double) Double where-  {-# SPECIALIZE INLINE getNth :: Vec Double -> Int -> IO Double #-}-  getNth (Vec v) = UV.unsafeRead v-  {-# SPECIALIZE INLINE setNth :: Vec Double -> Int -> Double -> IO () #-}-  setNth (Vec v) = UV.unsafeWrite v-  {-# SPECIALIZE INLINE modifyNth :: Vec Double -> (Double -> Double) -> Int -> IO () #-}-  modifyNth (Vec v) = UV.unsafeModify v-  {-# SPECIALIZE INLINE swapBetween :: Vec Double -> Int -> Int -> IO () #-}-  swapBetween (Vec v) = UV.unsafeSwap v-  {-# SPECIALIZE INLINE newVec :: Int -> Double -> IO (Vec Double) #-}-  newVec n x = Vec <$> newVec (n + 1) x-  {-# SPECIALIZE INLINE setAll :: Vec Double -> Double -> IO () #-}-  setAll (Vec v) = UV.set v-  {-# SPECIALIZE INLINE growBy :: Vec Double -> Int -> IO (Vec Double) #-}-  growBy (Vec v) n = Vec <$> UV.unsafeGrow v n---------------------------------------------------------------------------------- SingleStorage---- | Interface for single mutable data-class SingleStorage s t | s -> t where-  -- | allocates and returns an new data.-  new' :: t -> IO s-  -- | gets the value.-  get' :: s -> IO t-  -- | sets the value.-  set' :: s -> t -> IO ()-  -- | calls an update function on it.-  modify' :: s -> (t -> t) -> IO ()-  {-# MINIMAL get', set' #-}-  new' = undefined-  modify' = undefined---- | Mutable Int--- __Note:__  Int' is the same with 'Stack'-type Int' = UV.IOVector Int--instance SingleStorage Int' Int where-  {-# SPECIALIZE INLINE new' :: Int -> IO Int' #-}-  new' k = do-    s <- UV.new 1-    UV.unsafeWrite s 0 k-    return s-  {-# SPECIALIZE INLINE get' :: Int' -> IO Int #-}-  get' val = UV.unsafeRead val 0-  {-# SPECIALIZE INLINE set' :: Int' -> Int -> IO () #-}-  set' val !x = UV.unsafeWrite val 0 x-  {-# SPECIALIZE INLINE modify' :: Int' -> (Int -> Int) -> IO () #-}-  modify' val f = UV.unsafeModify val f 0---- | Mutable Bool-type Bool' = UV.IOVector Bool--instance SingleStorage Bool' Bool where-  {-# SPECIALIZE INLINE new' :: Bool -> IO Bool' #-}-  new' k = do-    s <- UV.new 1-    UV.unsafeWrite s 0 k-    return s-  {-# SPECIALIZE INLINE get' :: Bool' -> IO Bool #-}-  get' val = UV.unsafeRead val 0-  {-# SPECIALIZE INLINE set' :: Bool' -> Bool -> IO () #-}-  set' val !x = UV.unsafeWrite val 0 x-  {-# SPECIALIZE INLINE modify' :: Bool' -> (Bool -> Bool) -> IO () #-}-  modify' val f = UV.unsafeModify val f 0---- | Mutable Double-type Double' = UV.IOVector Double--instance SingleStorage Double' Double where-  {-# SPECIALIZE INLINE new' :: Double -> IO Double' #-}-  new' k = do-    s <- UV.new 1-    UV.unsafeWrite s 0 k-    return s-  {-# SPECIALIZE INLINE get' :: Double' -> IO Double #-}-  get' val = UV.unsafeRead val 0-  {-# SPECIALIZE INLINE set' :: Double' -> Double -> IO () #-}-  set' val !x = UV.unsafeWrite val 0 x-  {-# SPECIALIZE INLINE modify' :: Double' -> (Double -> Double) -> IO () #-}-  modify' val f = UV.unsafeModify val f 0---------------------------------------------------------------------------------- Stack---- | Interface on stacks-class SingleStorage s Int => StackFamily s t | s -> t where-  -- | returns a new stack.-  newStack :: Int -> IO s-  -- | pushs an value to the tail of the stack.-  pushTo :: s -> t-> IO ()-  -- | pops the last element.-  popFrom :: s -> IO ()-  -- | peeks the last element.-  lastOf :: s -> IO t-  -- | shrinks the stack.-  shrinkBy :: s -> Int -> IO ()-  newStack = undefined-  pushTo = undefined-  popFrom = undefined-  lastOf = undefined-  shrinkBy = undefined---- | Alias of @Vec Int@. The 0-th element holds the number of elements.-type Stack = Vec Int--instance SingleStorage Stack Int where-  {-# SPECIALIZE INLINE get' :: Stack -> IO Int #-}-  get' (Vec v) = UV.unsafeRead v 0-  {-# SPECIALIZE INLINE set' :: Stack -> Int -> IO () #-}-  set' (Vec v) !x = UV.unsafeWrite v 0 x-  {-# SPECIALIZE INLINE modify' :: Stack -> (Int -> Int) -> IO () #-}-  modify' (Vec v) f = UV.unsafeModify v f 0--instance StackFamily Stack Int where-  {-# SPECIALIZE INLINE newStack :: Int -> IO Stack #-}-  newStack n = newVec n 0-  {-# SPECIALIZE INLINE pushTo :: Stack -> Int -> IO () #-}-  pushTo (Vec v) x = do-    i <- (+ 1) <$> UV.unsafeRead v 0-    UV.unsafeWrite v i x-    UV.unsafeWrite v 0 i-  {-# SPECIALIZE INLINE popFrom :: Stack -> IO () #-}-  popFrom (Vec v) = UV.unsafeModify v (subtract 1) 0-  {-# SPECIALIZE INLINE lastOf :: Stack -> IO Int #-}-  lastOf (Vec v) = UV.unsafeRead v =<< UV.unsafeRead v 0-  {-# SPECIALIZE INLINE shrinkBy :: Stack -> Int -> IO () #-}-  shrinkBy (Vec v) k = UV.unsafeModify v (subtract k) 0---- | returns a new 'Stack' from @[Int]@.-{-# INLINABLE newStackFromList #-}-newStackFromList :: [Int] -> IO Stack-newStackFromList !l = Vec <$> U.unsafeThaw (U.fromList (length l : l))

@@ -1,3 +1,6 @@+{-# LANGUAGE+   MultiWayIf+  #-} -- | Executable of 'Minisat Implementation and Optimization Study' module Main        (@@ -7,14 +10,15 @@  import SAT.Mios +usage :: String+usage = miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf"+ -- | main main :: IO ()-main = do-  opts <- miosParseOptionsFromArgs versionId-  case () of-    _ | _displayVersion opts        -> putStrLn versionId-    _ | _displayHelp opts           -> putStrLn $ miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf"-    _ | _targetFile opts == Just "" -> putStrLn $ miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf"-    _ | _validateAssignment opts    -> executeValidator opts-    _ | otherwise                   -> executeSolver opts+main = do opts <- miosParseOptionsFromArgs versionId+          if | _displayVersion opts        -> putStrLn versionId+             | _displayHelp opts           -> putStrLn usage+             | _targetFile opts == Nothing -> putStrLn usage+             | _validateAssignment opts    -> executeValidator opts+             | otherwise                   -> executeSolver opts 

@@ -2,13 +2,12 @@ -- see http://haskell.org/cabal/users-guide/  name:                   mios-version:                1.4.0-synopsis:               A Minisat-based SAT solver in Haskell+version:                1.5.4+synopsis:               A Minisat-based CDCL SAT solver in Haskell description: -  A modern and fast SAT solver written in Haskell, based on Minisat-1.14 and 2.2.-  By using CDCL, watch literals, VSIDS, restart, blocking-literals, LBD and so on.-  The current version is only 2.0 time slower than Minisat-2.2.+  A modern and very fast SAT solver written in Haskell, using CDCL, watch literals, VSIDS,+  blocking-literals, phase saving, LBD, Glucose-like restart and so on.   'Mios' is an abbreviation of 'Minisat-based Implementation and Optimization Study on SAT solver'.   . @@ -20,7 +19,7 @@ category:               Artificial Intelligence, Constraints build-type:             Simple cabal-version:          >=1.16-extra-source-files:  app/sample.hs+extra-source-files:     app/sample.hs  source-repository head   type:                 git@@ -30,38 +29,41 @@   Description:	        Compile with llvm   Default:	        False -Flag lib-  Description:	        Build the solver library-  Default:	        True+Flag MultiConflict+  Description:	        Build tools in MultiConflict+  Default:	        False +Flag utils+  Description:	        Build misc utilities for developer+  Default:	        False+ library-  if flag(lib)-    buildable:	        True-  else-    buildable:	        False+  hs-source-dirs:	src   default-language:	Haskell2010   default-extensions:   Strict-  other-extensions:	    BangPatterns-                            FlexibleContexts-                            FlexibleInstances-                            FunctionalDependencies-                            MagicHash-                            MultiParamTypeClasses-                            RecordWildCards-                            ScopedTypeVariables-                            TypeFamilies-                            Trustworthy-                            TupleSections-                            Safe-                            UndecidableInstances-                            ViewPatterns+  other-extensions:	BangPatterns+                        FlexibleContexts+                        FlexibleInstances+                        FunctionalDependencies+                        MagicHash+                        MultiParamTypeClasses+                        RecordWildCards+                        ScopedTypeVariables+                        TypeFamilies+                        Trustworthy+                        TupleSections+                        Safe+                        UndecidableInstances+                        ViewPatterns   exposed-modules:                         SAT.Mios.Clause                         SAT.Mios.ClauseManager-                        SAT.Mios.Vec+                        SAT.Mios.ClausePool+                        SAT.Mios.Criteria                         SAT.Mios.Main                         SAT.Mios.OptionParser                         SAT.Mios.Solver+                        SAT.Mios.Vec                         SAT.Mios.Types                         SAT.Mios.Validator                         SAT.Mios.Util.DIMACS.MinisatReader@@ -70,29 +72,119 @@                         SAT.Mios.Util.DIMACS                         SAT.Mios.Util.BoolExp                         SAT.Mios-  build-depends:        base ==4.9.*, vector >=0.11, ghc-prim >=0.5, bytestring >=0.10+  build-depends:        base >=4.10 && < 5, vector >=0.12, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6   if flag(llvm)-    ghc-options:	-O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3+    ghc-options:	-O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -fwarn-missing-signatures   else-    ghc-options:	-O2 -ignore-asserts -funbox-strict-fields+    ghc-options:	-O2 -funbox-strict-fields -msse2 -fwarn-missing-signatures -executable mios-  main-is:              app/mios.hs+executable mios-1.5.4+  hs-source-dirs:	app+  main-is:              mios.hs   buildable:	        True   default-language:	Haskell2010-  default-extensions:  Strict-  build-depends:        base ==4.9.*,  vector >=0.11, ghc-prim >=0.5, bytestring >=0.10+  default-extensions:   Strict+  build-depends:        base >=4.10 && < 5, mios   if flag(llvm)-    ghc-options:	-O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3+    ghc-options:	-O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -rtsopts -fwarn-missing-signatures   else+    ghc-options:	-O2 -funbox-strict-fields -msse2 -rtsopts -fwarn-missing-signatures++executable cnf-stat+  hs-source-dirs:	utils+  main-is:              cnf-stat.hs+  if flag(utils)+    buildable:	        True+  else+    buildable:	        False+  default-language:	Haskell2010+  default-extensions:   Strict+  build-depends:        base >=4.10 && < 5, mios, bytestring >=0.10+  ghc-options:	        -O1 -ignore-asserts -funbox-strict-fields++executable mios-mc+  hs-source-dirs:	MultiConflict app+  main-is:              mios.hs+  if flag(MultiConflict)+    buildable:	        True+  else+    buildable:	        False+  default-language:	Haskell2010+  default-extensions:   Strict+  build-depends:        base >=4.10 && < 5, mios, bytestring >=0.10+  if flag(llvm)+    ghc-options:	-O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O2 -optlc-O2+  else     ghc-options:	-O2 -ignore-asserts -funbox-strict-fields-  other-modules:-                        SAT.Mios.Clause-                        SAT.Mios.ClauseManager-                        SAT.Mios.Vec-                        SAT.Mios.Main-                        SAT.Mios.OptionParser-                        SAT.Mios.Solver-                        SAT.Mios.Types-                        SAT.Mios.Validator-                        SAT.Mios++executable mc-dump2csv+  hs-source-dirs:	MultiConflict+  main-is:              utils/dump2csv.hs+  if flag(MultiConflict) && flag(utils)+    buildable:	        True+  else+    buildable:	        False+  default-language:	Haskell2010+  default-extensions:   Strict+  build-depends:        base >=4.10 && < 5, mios, bytestring >=0.10+  ghc-options:	        -O1 -ignore-asserts -funbox-strict-fields++executable mc-averagecsv+  hs-source-dirs:	MultiConflict+  main-is:              utils/averagecsv.hs+  if flag(MultiConflict) && flag(utils)+    buildable:	        True+  else+    buildable:	        False+  default-language:	Haskell2010+  default-extensions:   Strict+  build-depends:        base >=4.10 && < 5, mios, bytestring >=0.10+  ghc-options:	        -O1 -ignore-asserts -funbox-strict-fields++executable mc-summary+  hs-source-dirs:	MultiConflict+  main-is:              utils/summary.hs+  if flag(MultiConflict) && flag(utils)+    buildable:	        True+  else+    buildable:	        False+  default-language:	Haskell2010+  default-extensions:   Strict+  build-depends:        base >=4.10 && < 5, mios, bytestring >=0.10+  ghc-options:	        -O1 -ignore-asserts -funbox-strict-fields++executable mc-stat2csv+  hs-source-dirs:	MultiConflict+  main-is:              utils/stat2csv.hs+  if flag(MultiConflict) && flag(utils)+    buildable:	        True+  else+    buildable:	        False+  default-language:	Haskell2010+  default-extensions:   Strict+  build-depends:        base >=4.10 && < 5, mios, bytestring >=0.10+  ghc-options:	        -O1 -ignore-asserts -funbox-strict-fields++executable mc-pickup+  hs-source-dirs:	MultiConflict+  main-is:              utils/pickup.hs+  if flag(MultiConflict) && flag(utils)+    buildable:	        True+  else+    buildable:	        False+  default-language:	Haskell2010+  default-extensions:   Strict+  build-depends:        base >=4.10 && < 5, mios, bytestring >=0.10+  ghc-options:	        -O1 -ignore-asserts -funbox-strict-fields++executable mc-numbers+  hs-source-dirs:	MultiConflict+  main-is:              utils/numbers.hs+  if flag(MultiConflict) && flag(utils)+    buildable:	        True+  else+    buildable:	        False+  default-language:	Haskell2010+  default-extensions:   Strict+  build-depends:        base >=4.10 && < 5, mios, bytestring >=0.10+  ghc-options:	        -O1 -ignore-asserts -funbox-strict-fields

@@ -0,0 +1,335 @@+-- | (This file is a part of MIOS.)+-- Minisat-based Implementation and Optimization Study on SAT solver+{-# LANGUAGE+    BangPatterns+  , LambdaCase+  , ViewPatterns+#-}+{-# LANGUAGE Safe #-}++module SAT.Mios+       (+         -- * Interface to the core of solver+         versionId+       , CNFDescription (..)+       , module SAT.Mios.OptionParser+       , runSolver+       , solveSAT+       , solveSATWithConfiguration+       , solve+       , SolverResult+       , Certificate (..)+         -- * Assignment Validator+       , validateAssignment+       , validate+         -- * For standalone programs+       , executeSolverOn+       , executeSolver+       , executeValidatorOn+       , executeValidator+         -- * File IO+       , parseCNF+       , injectClausesFromCNF+       , dumpAssigmentAsCNF+       )+       where++import Control.Concurrent (forkIO, killThread, myThreadId, threadDelay+                          , newEmptyMVar, putMVar, readMVar)+import Control.Exception+import Control.Monad ((<=<), unless, void, when)+import Data.Char+import qualified Data.ByteString.Char8 as B+import Numeric (showFFloat)+import System.CPUTime+import System.Exit+import System.IO++import SAT.Mios.Types+import SAT.Mios.Main+import SAT.Mios.OptionParser+import SAT.Mios.Validator++-- | version name+versionId :: String+versionId = "mios-1.5.4 -- https://github.com/shnarazk/mios"++reportElapsedTime :: Bool -> String -> Integer -> IO Integer+reportElapsedTime False _ 0 = return 0+reportElapsedTime False _ _ = getCPUTime+reportElapsedTime True mes t = do+  now <- getCPUTime+  let toSecond = 1000000000000 :: Double+  hPutStr stderr mes+  hPutStrLn stderr $ showFFloat (Just 3) (fromIntegral (now - t) / toSecond) " sec"+  return now++-- | executes a solver on the given CNF file.+-- This is the simplest entry to standalone programs; not for Haskell programs.+executeSolverOn :: FilePath -> IO ()+executeSolverOn path = executeSolver (miosDefaultOption { _targetFile = Just path })++-- | executes a solver on the given 'arg :: MiosConfiguration'.+-- 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+  (desc, cls) <- parseCNF (_targetFile opts)+  -- when (_numberOfVariables desc == 0) $ error $ "couldn't load " ++ show cnfFile+  token <- newEmptyMVar --  :: IO (MVar (Maybe Solver))+  solverId <- myThreadId+  handle (\case+             UserInterrupt -> putStrLn "User interrupt recieved."+             ThreadKilled  -> reportResult opts t0 =<< readMVar token+             e -> print e) $ do+    when (0 < _confBenchmark opts) $+      void $ forkIO $ do let fromMicro = 1000000 :: Int+                         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+    injectClausesFromCNF s desc cls+    void $ reportElapsedTime (_confVerbose opts) ("## [" ++ showPath cnfFile ++ "] Parse: ") t0+    when (0 < _confDumpStat opts) $ dumpSolver DumpCSVHeader s+    result <- solve s []+    putMVar token result+    killThread solverId++executeSolver _ = return ()++-- | print messages on solver's result+-- Note: the last field of benchmark CSV is:+--   * 0 if UNSAT+--   * 1 if satisfiable (by finding an assignment)+--   * other bigger values are used for aborted cases.+reportResult :: MiosProgramOption -> Integer -> SolverResult -> IO ()+-- abnormal cases, catching 'too large CNF', 'timeout' for now.+reportResult opts@(_targetFile -> Just cnfFile) _ (Left flag) =+  putStrLn ("\"" ++ takeWhile (' ' /=) versionId ++ "\","+             ++ show (_confBenchSeq opts) ++ ","+             ++ "\"" ++ cnfFile ++ "\","+             ++ show (_confBenchmark opts) ++ "," ++ show (fromEnum flag))++-- solver terminated normally+reportResult opts@(_targetFile -> Just cnfFile) t0 (Right result) = do+  t2 <- reportElapsedTime (_confVerbose opts) ("## [" ++ showPath cnfFile ++ "] Total: ") t0+  case result of+    _ | 0 <= _confBenchmark opts -> return ()+    SAT _   | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "SATISFIABLE"+    UNSAT _ | _confNoAnswer opts -> when (_confVerbose opts) $ hPutStrLn stderr "UNSATISFIABLE"+    SAT asg -> print asg+    UNSAT t -> do when (_confVerbose opts) $ hPutStrLn stderr "UNSAT" -- contradiction+                  print t+  dumpAssigmentAsCNF (_outputFile opts) result+  valid <- if _confCheckAnswer opts || 0 <= _confBenchmark opts+           then case result of+                  SAT asg -> do (desc, cls) <- parseCNF (_targetFile opts)+                                s' <- newSolver (toMiosConf opts) desc+                                injectClausesFromCNF s' desc cls+                                validate s' asg+                  UNSAT _ -> return True+           else return True+  when (_confCheckAnswer opts) $ do+    if _confVerbose opts+      then hPutStrLn stderr $ if valid then "A vaild answer" else "Internal error: mios returns a wrong answer"+      else unless valid $ hPutStrLn stderr "Internal error: mios returns a wrong answer"+    void $ reportElapsedTime (_confVerbose opts) ("## [" ++ showPath cnfFile ++ "] Validate: ") t2+  when (0 <= _confBenchmark opts) $ do+    let fromPico = 1000000000000 :: Double+        phase = case result of { SAT _   -> 1; UNSAT _ -> 0::Int }+    putStrLn $ "\"" ++ takeWhile (' ' /=) versionId ++ "\","+      ++ show (_confBenchSeq opts) ++ ","+      ++ "\"" ++ cnfFile ++ "\","+      ++ if valid+         then showFFloat (Just 3) (fromIntegral (t2 - t0) / fromPico) "," ++ show phase+         else show (_confBenchmark opts) ++ "," ++ show (fromEnum InternalInconsistent)++reportResult _ _ _ = return ()++-- | new top-level interface that returns:+--+-- * conflicting literal set :: Left [Int]+-- * satisfiable assignment :: Right [Int]+--+runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int])+runSolver m d c = do+  s <- newSolver m d+  mapM_ ((s `addClause`) <=< (newStackFromList . map int2lit)) c+  noConf <- simplifyDB s+  if noConf+    then do+        x <- solve s []+        case x of+          Right (SAT a)   -> return $ Right a+          Right (UNSAT a) -> return $ Left a+          _ -> return $ Left []+    else return $ Left []++-- | The easiest interface for Haskell programs.+-- This returns the result @::[[Int]]@ for a given @(CNFDescription, [[Int]])@.+-- The first argument @target@ can be build by @Just target <- cnfFromFile targetfile@.+-- The second part of the first argument is a list of vector, which 0th element is the number of its real elements.+solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int]+solveSAT = solveSATWithConfiguration defaultConfiguration++-- | solves the problem (2rd arg) under the configuration (1st arg).+-- and returns an assignment as list of literals :: Int.+solveSATWithConfiguration :: Traversable m => MiosConfiguration -> CNFDescription -> m [Int] -> IO [Int]+solveSATWithConfiguration conf desc cls = do+  s <- newSolver conf desc+  -- mapM_ (const (newVar s)) [0 .. _numberOfVariables desc - 1]+  mapM_ ((s `addClause`) <=< (newStackFromList . map int2lit)) cls+  noConf <- simplifyDB s+  if noConf+    then do result <- solve s []+            case result of+              Right (SAT a) -> return a+              _             -> return []+    else return []++-- | validates a given assignment from STDIN for the CNF file (2nd arg).+-- this is the entry point for standalone programs.+executeValidatorOn :: FilePath -> IO ()+executeValidatorOn path = executeValidator (miosDefaultOption { _targetFile = Just path })++-- | validates a given assignment for the problem (2nd arg).+-- This is another entry point for standalone programs; see app/mios.hs.+executeValidator :: MiosProgramOption -> IO ()+executeValidator opts@(_targetFile -> target@(Just cnfFile)) = do+  (desc, cls) <- parseCNF target+  when (_numberOfVariables desc == 0) . error $ "couldn't load " ++ show cnfFile+  s <- newSolver (toMiosConf opts) desc+  injectClausesFromCNF s desc cls+  when (_confVerbose opts) $+    hPutStrLn stderr $ cnfFile ++ " was loaded: #v = " ++ show (_numberOfVariables desc) ++ " #c = " ++ show (_numberOfClauses desc)+  asg <- read <$> getContents+  unless (_confNoAnswer opts) $ print asg+  result <- s `validate` (asg :: [Int])+  if result+    then putStrLn ("It's a valid assignment for " ++ cnfFile ++ ".") >> exitSuccess+    else putStrLn ("It's an invalid assignment for " ++ cnfFile ++ ".") >> exitFailure++executeValidator _  = return ()++-- | returns True if a given assignment (2nd arg) satisfies the problem (1st arg).+-- if you want to check the @answer@ which a @slover@ returned, run @solver `validate` answer@,+-- where 'validate' @ :: Traversable t => Solver -> t Lit -> IO Bool@.+validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool+validateAssignment desc cls asg = do+  s <- newSolver defaultConfiguration desc+  mapM_ ((s `addClause`) <=< (newStackFromList . map int2lit)) cls+  s `validate` asg++-- | dumps an assigment to file.+-- 2nd arg is+--+-- * @True@ if the assigment is satisfiable assigment+--+-- * @False@ if not+--+-- >>> do y <- solve s ... ; dumpAssigmentAsCNF (Just "result.cnf") y <$> model s+--+dumpAssigmentAsCNF :: Maybe FilePath -> Certificate -> IO ()+dumpAssigmentAsCNF Nothing _ = return ()+-- | FIXME: swtich to DRAT+dumpAssigmentAsCNF (Just fname) (UNSAT _) =+  writeFile fname "s UNSAT\n0\n"+dumpAssigmentAsCNF (Just fname) (SAT l) =+  withFile fname WriteMode $ \h -> do hPutStrLn h "s SAT"; hPutStrLn h . (++ " 0") . unwords $ map show l++--------------------------------------------------------------------------------+-- DIMACS CNF Reader+--------------------------------------------------------------------------------++-- | parses the header of a CNF file+parseCNF :: Maybe FilePath -> IO (CNFDescription, B.ByteString)+parseCNF target@(Just cnfFile) = do+  let -- format: p cnf n m, length "p cnf" == 5+      parseP line = case parseInt (skipWhitespace (B.drop 5 line)) of+                      (x, second) -> case B.readInt (skipWhitespace second) of+                                       Just (y, _) -> CNFDescription x y target+      seek :: B.ByteString -> IO (CNFDescription, B.ByteString)+      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+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+  let loop :: Int -> B.ByteString -> IO ()+      loop ((< nc) -> False) _ = return ()+      loop !i !b = loop (i + 1) =<< readClause s buffer polvec 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++-- | skip comment lines+-- __Pre-condition:__ we are on the benngining of a line+{-# INLINE skipComments #-}+skipComments :: B.ByteString -> B.ByteString+skipComments !s+  | c == 'c' = skipComments . B.tail . B.dropWhile (/= '\n') $ s+  | otherwise = s+  where+    c = B.head s++{-# INLINABLE 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"++{-# 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+                                        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

@@ -0,0 +1,129 @@+-- | (This is a part of MIOS.)+-- Clause, supporting pointer-based equality+{-# LANGUAGE+    FlexibleInstances+  , MagicHash+  , MultiParamTypeClasses+  , RecordWildCards+  , ViewPatterns+  #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Mios.Clause+       (+         Clause (..)+       , newClauseFromStack+         -- * Vector of Clause+       , ClauseVector+       , newClauseVector+       )+       where++import GHC.Prim (tagToEnum#, reallyUnsafePtrEquality#)+import qualified Data.Vector as V+import qualified Data.Vector.Mutable as MV+-- import Data.List (intercalate)+import SAT.Mios.Types++-- | __Fig. 7.(p.11)__+-- normal, null (and binary) clause.+-- This matches both of @Clause@ and @GClause@ in MiniSat.+data Clause = Clause+              {+                rank       :: !Int'     -- ^ goodness like LBD; computed in 'Ranking'+              , activity   :: !Double'  -- ^ activity of this clause+--              , protected  :: !Bool'    -- ^ protected from reduce+              , lits       :: !Stack    -- ^ which this clause consists of+              }+  | NullClause                              -- as null pointer+--  | BinaryClause Lit                        -- binary clause consists of only a propagating literal++-- | The equality on 'Clause' is defined with 'reallyUnsafePtrEquality'.+instance Eq Clause where+  {-# SPECIALIZE INLINE (==) :: Clause -> Clause -> Bool #-}+  (==) x y = x `seq` y `seq` tagToEnum# (reallyUnsafePtrEquality# x y)++instance Show Clause where+  show NullClause = "NullClause"+  show _ = "a clause"++-- | 'Clause' is a 'VecFamily' of 'Lit'.+instance VecFamily Clause Lit where+  {-# SPECIALIZE INLINE getNth :: Clause -> Int -> IO Int #-}+  getNth Clause{..} n = error "no getNth for Clause"+  {-# SPECIALIZE INLINE setNth :: Clause -> Int -> Int -> IO () #-}+  setNth Clause{..} n x = error "no setNth for Clause"+  -- | returns a vector of literals in it.+  asList NullClause = return []+  asList Clause{..} = take <$> get' lits <*> (tail <$> asList lits)+  -- dump mes NullClause = return $ mes ++ "Null"+  -- dump mes Clause{..} = return $ mes ++ "a clause"+{-+  dump mes Clause{..} = do+    a <- show <$> get' activity+    n <- get' lits+    l <- asList lits+    return $ mes ++ "C" ++ show n ++ "{" ++ intercalate "," [show learnt, a, show (map lit2int l)] ++ "}"+-}++-- | 'Clause' is a 'SingleStorage' on the number of literals in it.+instance SingleStorage Clause Int where+  -- | returns the number of literals in a clause, even if the given clause is a binary clause+  {-# SPECIALIZE INLINE get' :: Clause -> IO Int #-}+  get' = get' . lits+  -- getSize (BinaryClause _) = return 1+  -- | sets the number of literals in a clause, even if the given clause is a binary clause+  {-# SPECIALIZE INLINE set' :: Clause -> Int -> IO () #-}+  set' c n = set' (lits c) n+  -- getSize (BinaryClause _) = return 1++-- | 'Clause' is a 'Stackfamily'on literals since literals in it will be discared if satisifed at level = 0.+instance StackFamily Clause Lit where+  -- | drop the last /N/ literals in a 'Clause' to eliminate unsatisfied literals+  {-# SPECIALIZE INLINE shrinkBy :: Clause -> Int -> IO () #-}+  shrinkBy c n = modifyNth (lits c) (subtract n) 0++-- coverts a binary clause to normal clause in order to reuse map-on-literals-in-a-clause codes.+-- liftToClause :: Clause -> Clause+-- liftToClause (BinaryClause _) = error "So far I use generic function approach instead of lifting"++-- | copies /vec/ and return a new 'Clause'.+-- Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically.+{-# INLINABLE newClauseFromStack #-}+newClauseFromStack :: Bool -> Stack -> IO Clause+newClauseFromStack l vec = do+  n <- get' vec+  v <- newStack n+  let+    loop ((<= n) -> False) = return ()+    loop i = (setNth v i =<< getNth vec i) >> loop (i + 1)+  loop 0+  Clause <$> new' (if l then 1 else 0) <*> new' 0.0 {- <*> new' False -} <*> return v++-------------------------------------------------------------------------------- Clause Vector++-- | Mutable 'Clause' Vector+type ClauseVector = MV.IOVector Clause++-- | 'ClauseVector' is a vector of 'Clause'.+instance VecFamily ClauseVector Clause where+  {-# SPECIALIZE INLINE getNth :: ClauseVector -> Int -> IO Clause #-}+  getNth = MV.unsafeRead+  {-# SPECIALIZE INLINE setNth :: ClauseVector -> Int -> Clause -> IO () #-}+  setNth = MV.unsafeWrite+  {-# SPECIALIZE INLINE swapBetween :: ClauseVector -> Int -> Int -> IO () #-}+  swapBetween = MV.unsafeSwap+  asList cv = V.toList <$> V.freeze cv -- mapM (asList <=< getNth vec) [0 .. ???]+{-+  dump mes cv = do+    l <- asList cv+    sts <- mapM (dump ",") (l :: [Clause])+    return $ mes ++ tail (concat sts)+-}++-- | returns a new 'ClauseVector'.+newClauseVector  :: Int -> IO ClauseVector+newClauseVector n = do+  v <- MV.new (max 4 n)+  MV.set v NullClause+  return v

@@ -0,0 +1,293 @@+-- | (This is a part of MIOS.)+-- A shrinkable vector of 'C.Clause'+{-# LANGUAGE+    BangPatterns+  , FlexibleInstances+  , MultiParamTypeClasses+  , RecordWildCards+  , ViewPatterns+  #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Mios.ClauseManager+       (+         -- * higher level interface for ClauseVector+         ClauseManager (..)+         -- * Simple Clause Manager+       , ClauseSimpleManager+         -- * Manager with an extra Int (used as sort key or blocking literal)+       , ClauseExtManager+       , pushClauseWithKey+       , getKeyVector+       , markClause+         -- * WatcherList+       , WatcherList+       , newWatcherList+       , getNthWatcher+       )+       where++import Control.Monad (unless, when)+import qualified Data.IORef as IORef+import qualified Data.Vector as V+import qualified Data.Vector.Mutable as MV+import SAT.Mios.Types+import qualified SAT.Mios.Clause as C++-- | Resizable vector of 'C.Clause'.+class ClauseManager a where+  newManager      :: Int -> IO a+  getClauseVector :: a -> IO C.ClauseVector+--  removeClause    :: a -> C.Clause -> IO ()+--  removeNthClause :: a -> Int -> IO ()++--------------------------------------------------------------------------------++-- | Clause + Blocking Literal+data ClauseSimpleManager = ClauseSimpleManager+  {+    _numActives :: !Int'                         -- number of active clause+  , _clsVector  :: IORef.IORef C.ClauseVector    -- clause list+  }++-- | 'ClauseSimpleManager' is a 'SingleStorage` on the number of clauses in it.+instance SingleStorage ClauseSimpleManager Int where+  {-# SPECIALIZE INLINE get' :: ClauseSimpleManager -> IO Int #-}+  get' m = get' (_numActives m)+  {-# SPECIALIZE INLINE set' :: ClauseSimpleManager -> Int -> IO () #-}+  set' m = set' (_numActives m)++-- | 'ClauseSimpleManager' is a 'StackFamily` on clauses.+instance StackFamily ClauseSimpleManager C.Clause where+  {-# SPECIALIZE INLINE shrinkBy :: ClauseSimpleManager -> Int -> IO () #-}+  shrinkBy m k = modify' (_numActives m) (subtract k)+  pushTo ClauseSimpleManager{..} c = do+    -- checkConsistency m c+    !n <- get' _numActives+    !v <- IORef.readIORef _clsVector+    if MV.length v - 1 <= n+      then do+          let len = max 8 $ MV.length v+          v' <- MV.unsafeGrow v len+          MV.unsafeWrite v' n c+          IORef.writeIORef _clsVector v'+      else MV.unsafeWrite v n c+    modify' _numActives (1 +)+  popFrom m = modify' (_numActives m) (subtract 1)+  lastOf ClauseSimpleManager{..} = do+    n <- get' _numActives+    v <- IORef.readIORef _clsVector+    MV.unsafeRead v (n - 1)++-- | 'ClauseSimpleManager' is a 'ClauseManager'+instance ClauseManager ClauseSimpleManager where+  -- | returns a new instance.+  {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseSimpleManager #-}+  newManager initialSize = do+    i <- new' 0+    v <- C.newClauseVector initialSize+    ClauseSimpleManager i <$> IORef.newIORef v+  -- | returns the internal 'C.ClauseVector'.+  {-# SPECIALIZE INLINE getClauseVector :: ClauseSimpleManager -> IO C.ClauseVector #-}+  getClauseVector !m = IORef.readIORef (_clsVector m)++--------------------------------------------------------------------------------++-- | Clause + Blocking Literal+data ClauseExtManager = ClauseExtManager+  {+    _nActives     :: !Int'                         -- number of active clause+  , _purged       :: !Bool'                        -- whether it needs gc+  , _clauseVector :: IORef.IORef C.ClauseVector    -- clause list+  , _keyVector    :: IORef.IORef (Vec [Int])     -- Int list+  }++-- | 'ClauseExtManager' is a 'SingleStorage` on the number of clauses in it.+instance SingleStorage ClauseExtManager Int where+  {-# SPECIALIZE INLINE get' :: ClauseExtManager -> IO Int #-}+  get' m = get' (_nActives m)+  {-# SPECIALIZE INLINE set' :: ClauseExtManager -> Int -> IO () #-}+  set' m = set' (_nActives m)++-- | 'ClauseExtManager' is a 'StackFamily` on clauses.+instance StackFamily ClauseExtManager C.Clause where+  {-# SPECIALIZE INLINE shrinkBy :: ClauseExtManager -> Int -> IO () #-}+  shrinkBy m k = modify' (_nActives m) (subtract k)+  pushTo ClauseExtManager{..} c = do+    -- checkConsistency m c+    !n <- get' _nActives+    !v <- IORef.readIORef _clauseVector+    !b <- IORef.readIORef _keyVector+    if MV.length v - 1 <= n+      then do+          let len = max 8 $ MV.length v+          v' <- MV.unsafeGrow v len+          b' <- growBy b len+          MV.unsafeWrite v' n c+          setNth b' n 0+          IORef.writeIORef _clauseVector v'+          IORef.writeIORef _keyVector b'+      else MV.unsafeWrite v n c >> setNth b n 0+    modify' _nActives (1 +)+  popFrom m = modify' (_nActives m) (subtract 1)+  lastOf ClauseExtManager{..} = do+    n <- get' _nActives+    v <- IORef.readIORef _clauseVector+    MV.unsafeRead v (n - 1)++-- | 'ClauseExtManager' is a 'ClauseManager'+instance ClauseManager ClauseExtManager where+  -- | returns a new instance.+  {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-}+  newManager initialSize = do+    i <- new' 0+    v <- C.newClauseVector initialSize+    b <- newVec (MV.length v) 0+    ClauseExtManager i <$> new' False <*> IORef.newIORef v <*> IORef.newIORef b+  -- | returns the internal 'C.ClauseVector'.+  {-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-}+  getClauseVector !m = IORef.readIORef (_clauseVector m)+{-+  -- | O(1) insertion function+  pushClause !ClauseExtManager{..} !c = do+    -- checkConsistency m c+    !n <- get' _nActives+    !v <- IORef.readIORef _clauseVector+    !b <- IORef.readIORef _keyVector+    if MV.length v - 1 <= n+      then do+          let len = max 8 $ MV.length v+          v' <- MV.unsafeGrow v len+          b' <- growBy b len+          MV.unsafeWrite v' n c+          setNth b' n 0+          IORef.writeIORef _clauseVector v'+          IORef.writeIORef _keyVector b'+      else MV.unsafeWrite v n c >> setNth b n 0+    modify' _nActives (1 +)+-}+{-+  -- | O(n) but lightweight remove-and-compact function+  -- __Pre-conditions:__ the clause manager is empty or the clause is stored in it.+  {-# SPECIALIZE INLINE removeClause :: ClauseExtManager -> C.Clause -> IO () #-}+  removeClause ClauseExtManager{..} c = do+    !n <- subtract 1 <$> get' _nActives+    !v <- IORef.readIORef _clauseVector+    !b <- IORef.readIORef _keyVector+    let+      seekIndex :: Int -> IO Int+      seekIndex k = do+        c' <- MV.unsafeRead v k+        if c' == c then return k else seekIndex $ k + 1+    unless (n == -1) $ do+      !i <- seekIndex 0+      MV.unsafeWrite v i =<< MV.unsafeRead v n+      setNth b i =<< getNth b n+      set' _nActives n+  removeNthClause = error "removeNthClause is not implemented on ClauseExtManager"+-}++-- | sets the expire flag to a clause.+{-# INLINABLE markClause #-}+markClause :: ClauseExtManager -> C.Clause -> IO ()+markClause ClauseExtManager{..} c = do+  !n <- get' _nActives+  !v <- IORef.readIORef _clauseVector+  let+    seekIndex :: Int -> IO ()+    seekIndex k = do+      -- assert (k < n)+      c' <- MV.unsafeRead v k+      if c' == c then MV.unsafeWrite v k C.NullClause else seekIndex $ k + 1+  unless (n == 0) $ do+    seekIndex 0+    set' _purged True++{-# INLINABLE purifyManager #-}+purifyManager :: ClauseExtManager -> IO ()+purifyManager ClauseExtManager{..} = do+  diry <- get' _purged+  when diry $ do+    n <- get' _nActives+    vec <- IORef.readIORef _clauseVector+    keys <- IORef.readIORef _keyVector+    let+      loop :: Int -> Int -> IO Int+      loop ((< n) -> False) n' = return n'+      loop i j = do+        c <- getNth vec i+        if c /= C.NullClause+          then do+              unless (i == j) $ do+                setNth vec j c+                setNth keys j =<< getNth keys i+              loop (i + 1) (j + 1)+          else loop (i + 1) j+    set' _nActives =<< loop 0 0+    set' _purged False++-- | returns the associated Int vector, which holds /blocking literals/.+{-# INLINE getKeyVector #-}+getKeyVector :: ClauseExtManager -> IO (Vec [Int])+getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector++-- | O(1) inserter+{-# INLINABLE pushClauseWithKey #-}+pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO ()+pushClauseWithKey ClauseExtManager{..} !c k = do+  -- checkConsistency m c+  !n <- get' _nActives+  !v <- IORef.readIORef _clauseVector+  !b <- IORef.readIORef _keyVector+  if MV.length v - 1 <= n+    then do+        let len = max 8 $ MV.length v+        v' <- MV.unsafeGrow v len+        b' <- growBy b len+        MV.unsafeWrite v' n c+        setNth b' n k+        IORef.writeIORef _clauseVector v'+        IORef.writeIORef _keyVector b'+    else MV.unsafeWrite v n c >> setNth b n k+  modify' _nActives (1 +)++-- | 'ClauseExtManager' is a collection of 'C.Clause'+instance VecFamily ClauseExtManager C.Clause where+  getNth = error "no getNth method for ClauseExtManager"+  setNth = error "no setNth method for ClauseExtManager"+  {-# SPECIALIZE INLINE reset :: ClauseExtManager -> IO () #-}+  reset m = set' (_nActives m) 0+{-+  dump mes ClauseExtManager{..} = do+    n <- get' _nActives+    if n == 0+      then return $ mes ++ "empty ClauseExtManager"+      else do+          l <- take n <$> (asList =<< IORef.readIORef _clauseVector)+          sts <- mapM (dump ",") (l :: [C.Clause])+          return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts)+-}++-------------------------------------------------------------------------------- WatcherList++-- | Immutable Vector of 'ClauseExtManager'+type WatcherList = V.Vector ClauseExtManager++-- | /n/ is the number of 'Var', /m/ is default size of each watcher list.+-- | For /n/ vars, we need [0 .. 2 + 2 * n - 1] slots, namely /2 * (n + 1)/-length vector+-- FIXME: sometimes n > 1M+newWatcherList :: Int -> Int -> IO WatcherList+newWatcherList n m = V.replicateM (int2lit (negate n) + 2) (newManager m)++-- | returns the watcher List for "Literal" /l/.+{-# INLINE getNthWatcher #-}+getNthWatcher :: WatcherList -> Lit -> ClauseExtManager+getNthWatcher = V.unsafeIndex++-- | 'WatcherList' is an 'Lit'-indexed collection of 'C.Clause'.+instance VecFamily WatcherList C.Clause where+  getNth = error "no getNth method for WatcherList" -- getNthWatcher is a pure function+  setNth = error "no setNth method for WatcherList"+  {-# SPECIALIZE INLINE reset :: WatcherList -> IO () #-}+  reset = V.mapM_ purifyManager+--  dump _ _ = (mes ++) . concat <$> mapM (\i -> dump ("\n" ++ show (lit2int i) ++ "' watchers:") (getNthWatcher wl i)) [1 .. V.length wl - 1]

@@ -0,0 +1,75 @@+-- | (This is a part of MIOS.)+-- Recycling clauses+{-# LANGUAGE+    ViewPatterns+  #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Mios.ClausePool+       (+         ClausePool+       , newClausePool+       , makeClauseFromStack+       , putBackToPool+       )+       where++import Control.Monad (when)+import qualified Data.Vector as V+import SAT.Mios.Vec+import SAT.Mios.Clause+import qualified SAT.Mios.ClauseManager as CM++-- | an immutable Vector of 'ClauseSimpleManager'+type ClausePool = V.Vector CM.ClauseSimpleManager++-- | biclause should be stored into index:0, so the real limit is 64.+storeLimit :: Int+storeLimit = 62++-- | returns a new 'ClausePool'+newClausePool ::Int -> IO ClausePool+newClausePool n = V.fromList <$> mapM (\_ -> CM.newManager n) [0 .. storeLimit]++-- | returns 'CM.ClauseManager' for caluses which have suitable sizes.+{-# INLINE getManager #-}+getManager :: ClausePool -> Int -> CM.ClauseSimpleManager+getManager p n = V.unsafeIndex p n++-- | If a nice candidate as a learnt is stored, return it.+-- Otherwise allocate a new clause in heap then return it.+{-# INLINABLE makeClauseFromStack #-}+makeClauseFromStack :: ClausePool -> Stack -> IO Clause+makeClauseFromStack pool v = do+  let pickup :: Int -> IO Clause+      pickup ((<= storeLimit) -> False) = return NullClause+      pickup i = do+        let mgr = getManager pool i+        nn <- get' mgr+        if 0 < nn+          then do c <- lastOf mgr+                  popFrom mgr+                  return c+          else pickup $ i + 1+  n <- get' v+  c <- pickup (n - 2)+  if c == NullClause+    then newClauseFromStack True v+    else do let lstack = lits c+                loop :: Int -> IO ()+                loop ((<= n) -> False) = return ()+                loop i = (setNth lstack i =<< getNth v i) >> loop (i + 1)+            loop 0+            -- the caller (newLearntClause) should set these slots+            --  - rank+            --  - protected+            set' (activity c) 0.0+            return c++-- | Note: only not-too-large and learnt clauses are recycled.+{-# INLINE putBackToPool #-}+putBackToPool :: ClausePool -> Clause -> IO ()+putBackToPool pool c = do+  l <- get' (rank c)+  when (0 /= l) $ do let n = realLengthOfStack (lits c) - 3+                     when (n <= storeLimit) $ pushTo (getManager pool n) c

@@ -0,0 +1,327 @@+-- | (This is a part of MIOS.)+-- Advanced heuristics library for 'SAT.Mios.Main'+{-# LANGUAGE+    MultiWayIf+  , RecordWildCards+  , ViewPatterns+  #-}+{-# LANGUAGE Safe #-}++module SAT.Mios.Criteria+       (+         -- * Activities+         claBumpActivity+       , claDecayActivity+       , varBumpActivity+       , varDecayActivity+         -- * Clause+       , addClause+         -- * Literal Block Distance+       , lbdOf+         -- * Restart+       , checkRestartCondition+       )+        where++import Control.Monad (when)+import SAT.Mios.Types+import SAT.Mios.Clause+import SAT.Mios.ClauseManager+import SAT.Mios.Solver++-------------------------------------------------------------------------------- Activities++varActivityThreshold :: Double+varActivityThreshold = 1e100++-- | __Fig. 14 (p.19)__ Bumping of clause activity+{-# INLINE varBumpActivity #-}+varBumpActivity :: Solver -> Var -> IO ()+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++-- | __Fig. 14 (p.19)__+{-# INLINABLE varDecayActivity #-}+varDecayActivity :: Solver -> IO ()+varDecayActivity Solver{..} = modify' varInc (/ variableDecayRate config)++-- | __Fig. 14 (p.19)__+{-# INLINABLE varRescaleActivity #-}+varRescaleActivity :: Solver -> IO ()+varRescaleActivity Solver{..} = do+  let+    loop ((<= nVars) -> False) = return ()+    loop i = modifyNth activities (/ varActivityThreshold) i >> loop (i + 1)+  loop 1+  modify' varInc (/ varActivityThreshold)++-- | value for rescaling clause activity.+claActivityThreshold :: Double+claActivityThreshold = 1e20++-- | __Fig. 14 (p.19)__+{-# INLINE claBumpActivity #-}+claBumpActivity :: Solver -> Clause -> IO ()+claBumpActivity s@Solver{..} Clause{..} = do+  a <- (+) <$> get' activity <*> get' claInc+  set' activity a+  when (claActivityThreshold <= a) $ claRescaleActivity s++-- | __Fig. 14 (p.19)__+{-# INLINE claDecayActivity #-}+claDecayActivity :: Solver -> IO ()+claDecayActivity Solver{..} = modify' claInc (/ clauseDecayRate config)++-- | __Fig. 14 (p.19)__+{-# INLINABLE claRescaleActivity #-}+claRescaleActivity :: Solver -> IO ()+claRescaleActivity Solver{..} = do+  vec <- getClauseVector learnts+  n <- get' learnts+  let+    loopOnVector :: Int -> IO ()+    loopOnVector ((< n) -> False) = return ()+    loopOnVector i = do+      c <- getNth vec i+      modify' (activity c) (/ claActivityThreshold)+      loopOnVector $ i + 1+  loopOnVector 0+  modify' claInc (/ claActivityThreshold)++{-+-- | __Fig. 14 (p.19)__+{-# INLINABLE claRescaleActivityAfterRestart #-}+claRescaleActivityAfterRestart :: Solver -> IO ()+claRescaleActivityAfterRestart Solver{..} = do+  vec <- getClauseVector learnts+  n <- get' learnts+  let+    loopOnVector :: Int -> IO ()+    loopOnVector ((< n) -> False) = return ()+    loopOnVector i = do+      c <- getNth vec i+      d <- get' c+      if d < 9+        then modify' (activity c) sqrt+        else set' (activity c) 0+      -- set' (protected c) False+      loopOnVector $ i + 1+  loopOnVector 0+-}++-------------------------------------------------------------------------------- ClauseNew++-- | __Fig. 8. (p.12)__ create a new clause and adds it to watcher lists.+-- Constructor function for clauses. Returns @False@ if top-level conflict is determined.+-- @outClause@ may be set to Null if the new clause is already satisfied under the current+-- top-level assignment.+--+-- __Post-condition:__ @ps@ is cleared. For learnt clauses, all+-- literals will be false except @lits[0]@ (this by design of the 'analyze' method).+-- For the propagation to work, the second watch must be put on the literal which will+-- first be unbound by backtracking. (Note that none of the learnt-clause specific things+-- needs to done for a user defined contraint type.)+--+-- * @Left False@ if the clause is in a confilct+-- * @Left True@ if the clause is satisfied+-- * @Right clause@ if the clause is enqueued successfully+{-# INLINABLE clauseNew #-}+clauseNew :: Solver -> Stack -> Bool -> IO (Either Bool Clause)+clauseNew s@Solver{..} ps isLearnt = do+  -- now ps[0] is the number of living literals+  exit <- do+    let+      handle :: Int -> Int -> Int -> IO Bool+      handle j l n      -- removes duplicates, but returns @True@ if this clause is satisfied+        | j > n = return False+        | otherwise = do+            y <- getNth ps j+            if | y == l    -> do                      -- finds a duplicate+                   swapBetween ps j n+                   modifyNth ps (subtract 1) 0+                   handle j l (n - 1)+               | - y == l  -> reset ps >> return True -- p and negateLit p occurs in ps+               | otherwise -> handle (j + 1) l n+      loopForLearnt :: Int -> IO Bool+      loopForLearnt i = do+        n <- get' ps+        if n < i+          then return False+          else do+              l <- getNth ps i+              sat <- handle (i + 1) l n+              if sat+                then return True+                else loopForLearnt $ i + 1+      loop :: Int -> IO Bool+      loop i = do+        n <- get' ps+        if n < i+          then return False+          else do+              l <- getNth ps i     -- check the i-th literal's satisfiability+              sat <- valueLit s l  -- any literal in ps is true+              case sat of+               1  -> reset ps >> return True+               -1 -> do+                 swapBetween ps i n+                 modifyNth ps (subtract 1) 0+                 loop i+               _ -> do+                 sat' <- handle (i + 1) l n+                 if sat'+                   then return True+                   else loop $ i + 1+    if isLearnt then loopForLearnt 1 else loop 1+  k <- get' ps+  case k of+   0 -> return (Left exit)+   1 -> do+     l <- getNth ps 1+     Left <$> enqueue s l NullClause+   _ -> do+    -- allocate clause:+     c <- newClauseFromStack isLearnt ps+     let lstack = lits c+     when isLearnt $ do+       -- Pick a second literal to watch:+       let+         findMax :: Int -> Int -> Int -> IO Int+         findMax ((<= k) -> False) j _ = return j+         findMax i j val = do+           v' <- lit2var <$> getNth lstack i+           varBumpActivity s v' -- this is a just good chance to bump activities of literals in this clause+           a <- getNth assigns v'+           b <- getNth level v'+           if (a /= LBottom) && (val < b)+             then findMax (i + 1) i b+             else findMax (i + 1) j val+       -- Let @max_i@ be the index of the literal with highest decision level+       max_i <- findMax 1 1 0+       swapBetween lstack 2 max_i+       -- check literals occurences+       -- x <- asList c+       -- unless (length x == length (nub x)) $ error "new clause contains a element doubly"+       -- Bumping:+       claBumpActivity s c -- newly learnt clauses should be considered active+     -- Add clause to watcher lists:+     l1 <- getNth lstack 1+     l2 <- getNth lstack 2+     pushClauseWithKey (getNthWatcher watches (negateLit l1)) c 0+     pushClauseWithKey (getNthWatcher watches (negateLit l2)) c 0+     return (Right c)++-- | returns @False@ if a conflict has occured.+-- This function is called only before the solving phase to register the given clauses.+{-# INLINABLE addClause #-}+addClause :: Solver -> Stack -> IO Bool+addClause s@Solver{..} vecLits = do+  result <- clauseNew s vecLits False+  case result of+   Left b  -> return b   -- No new clause was returned becaues a confilct occured or the clause is a literal+   Right c -> pushTo clauses c >> return True++-------------------------------------------------------------------------------- LBD++-- | returns a POSIVITE value+{-# INLINABLE lbdOf #-}+lbdOf :: Solver -> Stack -> IO Int+lbdOf Solver{..} vec = do+  k <- (\k -> if 1000000 < k then 1 else k + 1) <$> get' lbd'key+  set' lbd'key k                -- store the last used value+  nv <- getNth vec 0+  let loop :: Int -> Int -> IO Int+      loop ((<= nv) -> False) n = return $ max 1 n+      loop i n = do l <- getNth level . lit2var =<< getNth vec i+                    x <- getNth lbd'seen l+                    if x /= k && l /= 0+                      then setNth lbd'seen l k >> loop (i + 1) (n + 1)+                      else loop (i + 1) n+  loop 1 0++{-+{-# INLINE setLBD #-}+setLBD :: Solver -> Clause -> IO ()+setLBD _ NullClause = error "LBD44"+setLBD s c = set' (rank c) =<< lbdOf s (lits c)++-- | update the lbd field of /c/+{-# INLINE updateLBD #-}+updateLBD :: Solver -> Clause -> IO ()+updateLBD s NullClause = error "LBD71"+updateLBD s c@Clause{..} = do+  k <- get' c+--  o <- getInt lbd+  n <- lbdOf s lits+  case () of+    _ | n == 1 -> set' rank (k - 1)+    -- _ | n < o -> setInt lbd n+    _ -> return ()+-}++-------------------------------------------------------------------------------- restart++ema1, ema2, ema3, ema4 :: Double+ema1 = 2 ** (-5)                -- coefficient for fast average of LBD+ema2 = 2 ** (-14)               -- coefficient for slow average of LBD+ema3 = 2 ** (-5)                -- coefficient for fast average of | assignment |+ema4 = 2 ** (-12)               -- coefficient for slow average of | assignment |++ema0 :: Int+ema0 = 2 ^ (14 :: Int)          -- = floor $ 1 / ema2++-- | #62+checkRestartCondition :: Solver -> Int -> IO Bool+checkRestartCondition s@Solver{..} (fromIntegral -> lbd) = do+  k <- getStat s NumOfRestart+  let step = 100+  next <- get' nextRestart+  count <- getStat s NumOfBackjump+  nas <- fromIntegral <$> nAssigns s+  let revise a f x  = do f' <- ((a * x) +) . ((1 - a) *) <$> get' f+                         set' f f'+                         return f'+      gef = 1.1 :: Double       -- geometric expansion factor+  df <- revise ema1 emaDFast lbd+  ds <- revise ema2 emaDSlow lbd+  af <- revise ema3 emaAFast nas+  as <- revise ema4 emaASlow nas+  mode <- get' restartMode+  if | count < next   -> return False+     | mode == 1      -> do+         when (ema0 < count && df < 2.0 * ds) $ set' restartMode 2 -- enter the second mode+         incrementStat s NumOfRestart 1+         incrementStat s NumOfGeometricRestart 1+         k' <- getStat s NumOfGeometricRestart+         set' nextRestart (count + floor (fromIntegral step * gef ** fromIntegral k'))+         when (3 == dumpStat config) $ dumpSolver 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+         return False+     | 1.25 * ds < df -> do+         incrementStat s NumOfRestart 1+         set' nextRestart (count + step)+         when (3 == dumpStat config) $ dumpSolver DumpCSV s+         return True+     | otherwise      -> return False++{-+{-# INLINABLE luby #-}+luby :: Double -> Int -> Double+luby y x_ = loop 1 0+  where+    loop :: Int -> Int -> Double+    loop sz sq+      | sz < x_ + 1 = loop (2 * sz + 1) (sq + 1)+      | otherwise   = loop2 x_ sz sq+    loop2 :: Int -> Int -> Int -> Double+    loop2 x sz sq+      | sz - 1 == x = y ** fromIntegral sq+      | otherwise   = let s = div (sz - 1) 2 in loop2 (mod x s) s (sq - 1)+-}

@@ -0,0 +1,759 @@+-- | (This is a part of MIOS.)+-- Main part of solving satisfiability problem.+{-# LANGUAGE+    BangPatterns+  , MultiWayIf+  , RecordWildCards+  , ScopedTypeVariables+  , ViewPatterns+  #-}+{-# LANGUAGE Safe #-}++module SAT.Mios.Main+       (+         -- * Interface to 'Solver', imported from 'SAT.Mios.Criteria'+         Solver+       , newSolver+       , setAssign+       , addClause+       , dumpSolver+         -- * Main function+       , simplifyDB+       , solve+       )+        where++import Control.Monad (unless, void, when)+import Data.Bits+import Data.Foldable (foldrM)+import Data.Int+import SAT.Mios.Types+import SAT.Mios.Clause+import SAT.Mios.ClauseManager+import SAT.Mios.Solver+import SAT.Mios.ClausePool+import SAT.Mios.Criteria++-- | #114: __RemoveWatch__+{-# INLINABLE removeWatch #-}+removeWatch :: Solver -> Clause -> IO ()+removeWatch Solver{..} c = do+  let lstack = lits c+  l1 <- negateLit <$> getNth lstack 1+  markClause (getNthWatcher watches l1) c+  l2 <- negateLit <$> getNth lstack 2+  markClause (getNthWatcher watches l2) c+  putBackToPool clsPool c++--------------------------------------------------------------------------------+-- Operations on 'Clause'+--------------------------------------------------------------------------------++-- | __Fig. 8. (p.12)__ creates a new LEARNT clause and adds it to watcher lists.+-- This is a strippped-down version of 'newClause' in Solver.+newLearntClause :: Solver -> Stack -> IO Int+newLearntClause s@Solver{..} ps = do+  -- ps is a 'SizedVectorInt'; ps[0] is the number of active literals+  -- Since this solver must generate only healthy learnt clauses, we need not to run misc check in 'newClause'+  k <- get' ps+  case k of+   1 -> do l <- getNth ps 1+           unsafeEnqueue s l NullClause+           return 1+   _ -> do c <- makeClauseFromStack clsPool ps --  newClauseFromStack True ps+           let lstack = lits c+               findMax :: Int -> Int -> Int -> IO Int -- Pick a second literal to watch:+               findMax ((<= k) -> False) j _ = return j+               findMax i j val = do+                 v <- lit2var <$> getNth lstack i+                 a <- getNth assigns v+                 b <- getNth level v+                 if (a /= LBottom) && (val < b)+                   then findMax (i + 1) i b+                   else findMax (i + 1) j val+           swapBetween lstack 2 =<< findMax 1 1 0 -- Let @max_i@ be the index of the literal with highest decision level+           -- Bump, enqueue, store clause:+           claBumpActivity s c+           -- Add clause to all managers+           pushTo learnts c+           l1 <- getNth lstack 1+           l2 <- getNth lstack 2+           pushClauseWithKey (getNthWatcher watches (negateLit l1)) c l2+           pushClauseWithKey (getNthWatcher watches (negateLit l2)) c l1+           -- update the solver state by @l@+           unsafeEnqueue s l1 c+           -- Since unsafeEnqueue updates the 1st literal's level, setLBD should be called after unsafeEnqueue+           lbd <- lbdOf s (lits c)+           set' (rank c) lbd+           -- assert (0 < rank c)+           -- set' (protected c) True+           return lbd++-- | __Simplify.__ At the top-level, a constraint may be given the opportunity to+-- simplify its representation (returns @False@) or state that the constraint is+-- satisfied under the current assignment and can be removed (returns @True@).+-- A constraint must /not/ be simplifiable to produce unit information or to be+-- conflicting; in that case the propagation has not been correctly defined.+--+-- MIOS NOTE: the original doesn't update watchers; only checks its satisfiabiliy.+{-# INLINABLE simplify #-}+simplify :: Solver -> Clause -> IO Bool+simplify s c = do+  n <- get' c+  let lstack = lits c+      loop ::Int -> IO Bool+      loop ((<= n) -> False) = return False+      loop i = do v <- valueLit s =<< getNth lstack i+                  if v == 1 then return True else loop (i + 1)+  loop 1++--------------------------------------------------------------------------------+-- MIOS NOTE on Minor methods:+--+-- * no (meaningful) 'newVar' in mios+-- * 'assume' is defined in 'Solver'+-- * `cancelUntil` is defined in 'Solver'++--------------------------------------------------------------------------------+-- Major methods++-- | M114: __Fig. 10. (p.15)__+--+-- analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel :: int&) -> [void]+--+-- __Description:_-+--   Analzye confilct and produce a reason clause.+--+-- __Pre-conditions:__+--   * 'out_learnt' is assumed to be cleared.+--   * Corrent decision level must be greater than root level.+--+-- __Post-conditions:__+--   * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.+--   * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the+--     rest of literals. There may be others from the same level though.+--+-- @analyze@ is invoked from @search@+analyze :: Solver -> Clause -> IO Int+analyze s@Solver{..} confl = do+  -- litvec+  reset litsLearnt+  pushTo litsLearnt 0 -- reserve the first place for the unassigned literal+  dl <- decisionLevel s+  let loopOnClauseChain :: Clause -> Lit -> Int -> Int -> Int -> IO Int+      loopOnClauseChain c p ti bl pathC = do -- p : literal, ti = trail index, bl = backtrack level+        d <- get' (rank c)+        when (0 /= d) $ claBumpActivity s c+        -- update LBD like #Glucose4.0+        when (2 < d) $ do+          nblevels <- lbdOf s (lits c)+          when (nblevels + 1 < d) $ -- improve the LBD+            -- when (d <= 30) $ set' (protected c) True -- 30 is `lbLBDFrozenClause`+            -- seems to be interesting: keep it fro the next round+            set' (rank c) nblevels    -- Update it+        sc <- get' c+        let lstack = lits c+            loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int)+            loopOnLiterals ((<= sc) -> False) b pc = return (b, pc) -- b = btLevel, pc = pathC+            loopOnLiterals j b pc = do+              (q :: Lit) <- getNth lstack j+              let v = lit2var q+              sn <- getNth an'seen v+              l <- getNth level v+              if sn == 0 && 0 < l+                then do+                    varBumpActivity s v+                    setNth an'seen v 1+                    if dl <= l      -- cancelUntil doesn't clear level of cancelled literals+                      then do+                          -- UPDATEVARACTIVITY: glucose heuristics+                          r <- getNth reason v+                          when (r /= NullClause) $ do+                            ra <- get' (rank r)+                            when (0 /= ra) $ pushTo an'lastDL q+                          -- end of glucose heuristics+                          loopOnLiterals (j + 1) b (pc + 1)+                      else pushTo litsLearnt q >> loopOnLiterals (j + 1) (max b l) pc+                else loopOnLiterals (j + 1) b pc+        (b', pathC') <- loopOnLiterals (if p == bottomLit then 1 else 2) bl pathC+        let nextPickedUpLit :: Int -> IO Int        -- select next clause to look at+            nextPickedUpLit i = do x <- getNth an'seen . lit2var =<< getNth trail i+                                   if x == 0 then nextPickedUpLit (i - 1) else return (i - 1)+        ti' <- nextPickedUpLit (ti + 1)+        nextP <- getNth trail (ti' + 1)+        let nextV = lit2var nextP+        confl' <- getNth reason nextV+        setNth an'seen nextV 0+        if 1 < pathC'+          then loopOnClauseChain confl' nextP (ti' - 1) b' (pathC' - 1)+          else setNth litsLearnt 1 (negateLit nextP) >> return b'+  ti <- subtract 1 <$> get' trail+  levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0+  -- Simplify phase (implemented only @expensive_ccmin@ path)+  n <- get' litsLearnt+  reset an'stack           -- analyze_stack.clear();+  reset an'toClear         -- out_learnt.copyTo(analyze_toclear);+  pushTo an'toClear =<< getNth litsLearnt 1+  let merger :: Int -> Int64 -> IO Int64+      merger ((<= n) -> False) b = return b+      merger i b = do l <- getNth litsLearnt i+                      pushTo an'toClear l+                      -- restrict the search depth (range) to 63+                      merger (i + 1) . setBit b . (63 .&.) =<< getNth level (lit2var l)+  levels <- merger 2 0+  let loopOnLits :: Int -> Int -> IO ()+      loopOnLits ((<= n) -> False) n' = shrinkBy litsLearnt $ n - n' + 1+      loopOnLits i j = do+        l <- getNth litsLearnt i+        c1 <- (NullClause ==) <$> getNth reason (lit2var l)+        if c1+          then setNth litsLearnt j l >> loopOnLits (i + 1) (j + 1)+          else do+             c2 <- not <$> analyzeRemovable s l levels+             if c2+               then setNth litsLearnt j l >> loopOnLits (i + 1) (j + 1)+               else loopOnLits (i + 1) j+  loopOnLits 2 2                -- the first literal is specail+  -- UPDATEVARACTIVITY: glucose heuristics+  nld <- get' an'lastDL+  r <- get' litsLearnt -- this is an estimated LBD value based on the clause size+  let loopOnLastDL :: Int -> IO ()+      loopOnLastDL ((<= nld) -> False) = return ()+      loopOnLastDL i = do v <- lit2var <$> getNth an'lastDL i+                          r' <- get' =<< getNth reason v+                          when (r < r') $ varBumpActivity s v+                          loopOnLastDL $ i + 1+  loopOnLastDL 1+  reset an'lastDL+  -- Clear seen+  k <- get' an'toClear+  let cleaner :: Int -> IO ()+      cleaner ((<= k) -> False) = return ()+      cleaner i = do v <- lit2var <$> getNth an'toClear i+                     setNth an'seen v 0+                     cleaner $ i + 1+  cleaner 1+  return levelToReturn++-- | #M114+-- Check if 'p' can be removed, 'abstract_levels' is used to abort early if the algorithm is+-- visiting literals at levels that cannot be removed later.+--+-- Implementation memo:+--+-- *  @an'toClear@ is initialized by @ps@ in @analyze@ (a copy of 'learnt').+--   This is used only in this function and @analyze@.+--+analyzeRemovable :: Solver -> Lit -> Int64 -> IO Bool+analyzeRemovable Solver{..} p minLevel = do+  -- assert (reason[var(p)] != NullClause);+  reset an'stack      -- analyze_stack.clear()+  pushTo an'stack p   -- analyze_stack.push(p);+  top <- get' an'toClear+  let+    loopOnStack :: IO Bool+    loopOnStack = do+      k <- get' an'stack  -- int top = analyze_toclear.size();+      if 0 == k+        then return True+        else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL);+            sl <- lastOf an'stack+            popFrom an'stack             -- analyze_stack.pop();+            c <- getNth reason (lit2var sl) -- getRoot sl+            nl <- get' c+            let+              lstack = lits c+              loopOnLit :: Int -> IO Bool -- loopOnLit (int i = 1; i < c.size(); i++){+              loopOnLit ((<= nl) -> False) = loopOnStack+              loopOnLit i = do+                p' <- getNth lstack i              -- valid range is [1 .. nl]+                let v' = lit2var p'+                l' <- getNth level v'+                c1 <- (1 /=) <$> getNth an'seen v'+                if c1 && (0 /= l')   -- if (!analyze_seen[var(p)] && level[var(p)] != 0){+                  then do+                      c3 <- (NullClause /=) <$> getNth reason v'+                      if c3 && testBit minLevel (l' .&. 63) -- if (reason[var(p)] != GClause_NULL && ((1 << (level[var(p)] & 31)) & min_level) != 0){+                        then do+                            setNth an'seen v' 1   -- analyze_seen[var(p)] = 1;+                            pushTo an'stack p'    -- analyze_stack.push(p);+                            pushTo an'toClear p'  -- analyze_toclear.push(p);+                            loopOnLit $ i + 1+                        else do+                            -- for (int j = top; j < analyze_toclear.size(); j++) analyze_seen[var(analyze_toclear[j])] = 0;+                            top' <- get' an'toClear+                            let clearAll :: Int -> IO ()+                                clearAll ((<= top') -> False) = return ()+                                clearAll j = do x <- getNth an'toClear j; setNth an'seen (lit2var x) 0; clearAll (j + 1)+                            clearAll $ top + 1+                            -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop+                            shrinkBy an'toClear $ top' - top+                            return False+                  else loopOnLit $ i + 1+            loopOnLit 2+  loopOnStack++-- | #114+-- analyzeFinal : (confl : Clause *) (skip_first : boot) -> [void]+--+-- __Description:__+--   Specialized analysis proceduce to express the final conflict in terms of assumptions.+--   'root_level' is allowed to point beyond end of trace (useful if called after conflict while+--   making assumptions). If 'skip_first' is TRUE, the first literal of 'confl' is ignored (needed+--   if conflict arose before search even started).+--+analyzeFinal :: Solver -> Clause -> Bool -> IO ()+analyzeFinal Solver{..} confl skipFirst = do+  reset conflicts+  rl <- get' rootLevel+  unless (rl == 0) $ do+    n <- get' confl+    let lstack = lits confl+        loopOnConfl :: Int -> IO ()+        loopOnConfl ((<= n) -> False) = return ()+        loopOnConfl i = do+          (x :: Var) <- lit2var <$> getNth lstack i+          lvl <- getNth level x+          when (0 < lvl) $ setNth an'seen x 1+          loopOnConfl $ i + 1+    loopOnConfl $ if skipFirst then 2 else 1+    tls <- get' trailLim+    trs <- get' trail+    tlz <- getNth trailLim 1+    let loopOnTrail :: Int -> IO ()+        loopOnTrail ((tlz <=) -> False) = return ()+        loopOnTrail i = do+          (l :: Lit) <- getNth trail (i + 1)+          let (x :: Var) = lit2var l+          saw <- getNth an'seen x+          when (saw == 1) $ do+            (r :: Clause) <- getNth reason x+            if r == NullClause+              then pushTo conflicts (negateLit l)+              else do+                  k <- get' r+                  let lstack' = lits r+                      loopOnLits :: Int -> IO ()+                      loopOnLits ((<= k) -> False) = return ()+                      loopOnLits j = do+                        (v :: Var) <- lit2var <$> getNth lstack' j+                        lv <- getNth level v+                        when (0 < lv) $ setNth an'seen v 1+                        loopOnLits $ i + 1+                  loopOnLits 2+          setNth an'seen x 0+          loopOnTrail $ i - 1+    loopOnTrail =<< if tls <= rl then return (trs - 1) else getNth trailLim (rl + 1)++-- | M114:+-- propagate : [void] -> [Clause+]+--+-- __Description:__+--   Porpagates all enqueued facts. If a conflict arises, the conflicting clause is returned.+--   otherwise CRef_undef.+--+-- __Post-conditions:__+--   * the propagation queue is empty, even if there was a conflict.+--+-- memo: @propagate@ is invoked by @search@,`simpleDB` and `solve`+propagate :: Solver -> IO Clause+propagate s@Solver{..} = do+  let+    while :: Clause -> Bool -> IO Clause+    while confl False = return confl+    while confl True = do+      (p :: Lit) <- getNth trail . (1 +) =<< get' qHead+      modify' qHead (+ 1)+      incrementStat s NumOfPropagation 1+      let (ws :: ClauseExtManager) = getNthWatcher watches p+          !falseLit = negateLit p+      end <- get' ws+      cvec <- getClauseVector ws+      bvec <- getKeyVector ws+      let copy :: Int -> Int -> IO ()+          copy ((< end) -> False) _ = return ()+          copy !i' !j' = do setNth cvec j' =<< getNth cvec i'+                            setNth bvec j' =<< getNth bvec i'+                            copy (i' + 1) (j' + 1)+      let forClause :: Int -> Int -> IO Clause+          forClause i@((< end) -> False) !j = shrinkBy ws (i - j) >> return confl+          forClause !i !j = do+            (blocker :: Lit) <- getNth bvec i        -- Try to avoid inspecting the clause:+            bv <- if blocker == 0 then return LiftedF else valueLit s blocker+            if bv == LiftedT+              then do unless (i == j) $ do (c :: Clause) <- getNth cvec i+                                           setNth cvec j c+                                           setNth bvec j blocker+                      forClause (i + 1) (j + 1)+              else do                               -- Make sure the false literal is data[1]:+                  (c :: Clause) <- getNth cvec i+                  let !lstack = lits c+                  tmp <- getNth lstack 1+                  first <- if falseLit == tmp+                           then do l2 <- getNth lstack 2+                                   setNth lstack 2 tmp+                                   setNth lstack 1 l2+                                   return l2+                           else return tmp+                  fv <- valueLit s first+                  if fv == LiftedT+                    then do unless (i == j) $ setNth cvec j c+                            setNth bvec j first+                            forClause (i + 1) (j + 1)+                    else do cs <- get' c           -- Look for new watch:+                            let newWatch :: Int -> IO LiftedBool+                                newWatch ((<= cs) -> False) = do -- Did not find watch+                                  setNth cvec j c+                                  setNth bvec j first+                                  if fv == LiftedF+                                    then do ((== 0) <$> decisionLevel s) >>= (`when` set' ok LiftedF)+                                            set' qHead =<< get' trail+                                            copy (i + 1) (j + 1)+                                            return LiftedF                 -- conflict+                                    else do unsafeEnqueue s first c+                                            return LBottom                 -- unit clause+                                newWatch !k = do (l' :: Lit) <- getNth lstack k+                                                 lv <- valueLit s l'+                                                 if lv /= LiftedF+                                                   then do setNth lstack 2 l'+                                                           setNth lstack k falseLit+                                                           pushClauseWithKey (getNthWatcher watches (negateLit l')) c first+                                                           return LiftedT  -- found another watch+                                                   else newWatch $! k + 1+                            ret <- newWatch 3+                            case ret of+                              LiftedT -> forClause (i + 1) j               -- found another watch+                              LBottom -> forClause (i + 1) (j + 1)         -- unit clause+                              _       -> shrinkBy ws (i - j) >> return c   -- conflict+      c <- forClause 0 0+      while c =<< ((<) <$> get' qHead <*> get' trail)+  while NullClause =<< ((<) <$> get' qHead <*> get' trail)++-- | #M22+-- reduceDB: () -> [void]+--+-- __Description:__+--   Remove half of the learnt clauses, minus the clauses locked by the current assigmnent. Locked+--   clauses are clauses that are reason to some assignment. Binary clauses are never removed.+reduceDB :: Solver -> IO ()+reduceDB s@Solver{..} = do+  n <- nLearnts s+  cvec <- getClauseVector learnts+  let loop :: Int -> IO ()+      loop ((< n) -> False) = return ()+      loop i = do+        removeWatch s =<< getNth cvec i+        loop $ i + 1+  k <- sortClauses s learnts $ div n 2 -- k is the number of clauses not to be purged+{-+  -- #GLUCOSE3.0 keep more+  t3 <- get' . rank =<< getNth vec (thr -1)+  t5 <- get' . rank =<< getNth vec (lim -1)++  let k = case (t3 <= 3, t5 <= 5) of+            (True, True)   -> min n (thr + 2000)+            (False, False) -> thr+            (_, _)         -> min n (thr + 1000)+  -- let k = div thr 2+-}+  loop k                               -- CAVEAT: `vec` is a zero-based vector+  -- putStrLn $ "reduceDB: purge " ++ show (n - k) ++ " out of " ++ show n+  reset watches+  shrinkBy learnts (n - k)+  incrementStat s NumOfReduction 1++-- constants for sort key layout+rankWidth :: Int+rankWidth = 10+activityWidth :: Int+activityWidth = 50              -- note: the maximum clause activity is 1e20.+indexWidth :: Int+indexWidth = 32                 -- 4G+rankMax :: Int+rankMax = 2 ^ rankWidth - 1+activityMax :: Int+activityMax = 2 ^ activityWidth - 1+indexMax :: Int+indexMax = 2 ^ indexWidth - 1++-- | applies a (good to bad) quick semi-sort to the vector in a 'ClauseExtManager'+-- and returns the number of privileged clauses.+-- This function uses the same criteria as reduceDB_lt in glucose 4.0:+-- 1. binary clause+-- 2. smaller LBD+-- 3. larger activity defined as MiniSat+--+-- they are encoded into two "Int64"s as the following (10+52+32 layout):+--+-- * 10 bits for rank (LBD): 'rankWidth'+-- * 50 bits for converted activity: 'activityWidth'+-- * 32 bits for clauseVector index: 'indexWidth'+--+sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int+sortClauses s cm limit' = do+  n <- get' cm+  -- assert (n < indexMax)+  vec <- getClauseVector cm+  bvec <- getKeyVector cm+  keys <- newVec (2 * n) 0 :: IO (Vec Int)+  at <- (0.1 *) . (/ fromIntegral n) <$> get' (claInc s) -- activity threshold+  -- 1: assign keys+  let shiftLBD = activityWidth+      shiftIndex = shiftL 1 indexWidth+      am = fromIntegral activityMax :: Double+      scaleAct :: Double -> Int+      scaleAct x+        | x < 1e-20 = activityMax+        | otherwise = floor $ am * (1 - logBase 10 (x * 1e20) / 40)+      assignKey :: Int -> Int -> IO Int+      assignKey ((< n) -> False) t = return t+      assignKey i t = do+        setNth keys (2 * i + 1) $ shiftIndex + i+        c <- getNth vec i+        k <- get' c+        if k == 2                  -- Main criteria. Like in MiniSat we keep all binary clauses+          then do setNth keys (2 * i) 0+                  assignKey (i + 1) (t + 1)+          else do a <- get' (activity c)               -- Second one... based on LBD+                  r <- get' (rank c)+                  l <- locked s c+                  let d =if | l -> 0+                            | a < at -> rankMax+                            | otherwise ->  min rankMax r                -- rank can be one+                  setNth keys (2 * i) $ shiftL d shiftLBD + scaleAct a+                  assignKey (i + 1) $ if l then t + 1 else t+  limit <- max limit' <$> assignKey 0 0+  -- 2: sort keyVector+  let limit2 = 2 * limit+      sortOnRange :: Int -> Int -> IO ()+      sortOnRange left right+        | limit2 < left = return ()+        | left >= right = return ()+        | left + 2 == right = do+            a <- getNth keys left+            b <- getNth keys right+            unless (a < b) $ do swapBetween keys left right+                                swapBetween keys (left + 1) (right + 1)+        | otherwise = do+            let p = 2 * div (left + right) 4+            pivot <- getNth keys p+            swapBetween keys p left -- set a sentinel for r'+            swapBetween keys (p + 1) (left + 1)+            let nextL :: Int -> IO Int+                nextL i@((<= right) -> False) = return i+                nextL i = do v <- getNth keys i; if v < pivot then nextL (i + 2) else return i+                nextR :: Int -> IO Int+                nextR i = do v <- getNth keys i; if pivot < v then nextR (i - 2) else return i+                divide :: Int -> Int -> IO Int+                divide l r = do+                  l' <- nextL l+                  r' <- nextR r+                  if l' < r'+                    then do swapBetween keys l' r'+                            swapBetween keys (l' + 1) (r' + 1)+                            divide (l' + 2) (r' - 2)+                    else return r'+            m <- divide (left + 2) right+            swapBetween keys left m+            swapBetween keys (left + 1) (m + 1)+            sortOnRange left (m - 2)+            sortOnRange (m + 2) right+  sortOnRange 0 $ 2 * (n - 1)+  -- 3: place clauses in 'vec' based on the order stored in 'keys'.+  -- To recycle existing clauses, we must reserve all clauses for now.+  let seek :: Int -> IO ()+      seek ((< n) -> False) = return ()+      seek i = do+        bits <- getNth keys (2 * i + 1)+        when (indexMax < bits) $ do+          c <- getNth vec i+          d <- getNth bvec i+          -- setNth keys i i+          let sweep k = do k' <- (indexMax .&.) <$> getNth keys (2 * k + 1)+                           setNth keys (2 * k + 1) (indexMax .&. k)+                           if k' == i+                             then do setNth vec k c+                                     setNth bvec k d+                             else do getNth vec k' >>= setNth vec k+                                     getNth bvec k' >>= setNth bvec k+                                     sweep k'+          sweep i -- (indexMax .&. bits)+        seek $ i + 1+  seek 0+  return limit++-- | #M22+--+-- simplify : [void] -> [bool]+--+-- __Description:__+--   Simplify the clause database according to the current top-level assigment. Currently, the only+--   thing done here is the removal of satisfied clauses, but more things can be put here.+--+simplifyDB :: Solver -> IO Bool+simplifyDB s@Solver{..} = do+  good <- (LiftedT ==) <$> get' ok+  if good+    then do+      p <- propagate s+      if p /= NullClause+        then set' ok LiftedF >> return False+        else do+            -- Remove satisfied clauses and their watcher lists:+            let+              for :: ClauseExtManager -> IO ()+              for mgr = do+                vec' <- getClauseVector mgr+                n' <- get' mgr+                let+                  loopOnVector :: Int -> Int -> IO ()+                  loopOnVector ((< n') -> False) j = shrinkBy mgr (n' - j)+                  loopOnVector i j = do+                        c <- getNth vec' i+                        l <- locked s c+                        r <- if l then return False else simplify s c+                        if r+                          then removeWatch s c >> loopOnVector (i + 1) j+                          else unless (i == j) (setNth vec' j c) >> loopOnVector (i + 1) (j + 1)+                loopOnVector 0 0+            for clauses+            for learnts+            reset watches+            return True+    else return False++-- | #M22+--+-- search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]+--+-- __Description:__+--   Search for a model the specified number of conflicts.+--   NOTE: Use negative value for 'nof_conflicts' indicate infinity.+--+-- __Output:__+--   * 'True' if a partial assigment that is consistent with respect to the clause set is found.+--      If all variables are decision variables, that means that the clause set is satisfiable.+--   * 'False' if the clause set is unsatisfiable or some error occured.+search :: Solver -> IO Bool+search s@Solver{..} = do+  -- clear model+  let loop :: Bool -> IO Bool+      loop restart = do+        confl <- propagate s+        d <- decisionLevel s+        if confl /= NullClause  -- CONFLICT+          then do incrementStat s NumOfBackjump 1+                  r <- get' rootLevel+                  if d == r                       -- Contradiction found:+                    then analyzeFinal s confl False >> return False+                    else do backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself+                            (s `cancelUntil`) . max backtrackLevel =<< get' rootLevel+                            lbd' <- newLearntClause s litsLearnt+                            k <- get' litsLearnt+                            when (k == 1) $ do+                              (v :: Var) <- lit2var <$> getNth litsLearnt 1+                              setNth level v 0+                            varDecayActivity s+                            claDecayActivity s+                            -- learnt DB Size Adjustment+                            modify' learntSCnt (subtract 1)+                            cnt <- get' learntSCnt+                            when (cnt == 0) $ do+                              t' <- (* 1.5) <$> get' learntSAdj+                              set' learntSAdj t'+                              set' learntSCnt $ floor t'+                              -- modify' maxLearnts (* 1.1)+                              modify' maxLearnts (+ 300)+                            loop =<< checkRestartCondition s lbd'+          else do when (d == 0) . void $ simplifyDB s -- Simplify the set of problem clauses+                  k1 <- get' learnts+                  k2 <- nAssigns s+                  nl <- floor <$> get' maxLearnts+                  when (nl < k1 - k2) $ do+                    reduceDB s    -- Reduce the set of learnt clauses.+                    when (2 == dumpStat config) $ dumpSolver DumpCSV s+                  if | k2 == nVars -> return True     -- Model found+                     | restart -> do                  -- Reached bound on number of conflicts+                         (s `cancelUntil`) =<< get' rootLevel -- force a restart+                         -- claRescaleActivityAfterRestart s+{-+                         let toggle :: Int -> Int+                             toggle LiftedT = LiftedF+                             toggle LiftedF = LiftedT+                             toggle x = x+                             nv = nVars+                             toggleAt :: Int -> IO ()+                             toggleAt ((<= nv) -> False) = return ()+                             toggleAt i = modifyNth phases toggle i >> toggleAt (i + 1)+                         rm <- get' restartMode+                         when (rm == 1) $ toggleAt 1+-}+                         loop False+                     | otherwise -> do                -- New variable decision+                         v <- select s+                         -- #phasesaving <<<<  many have heuristic for polarity here+                         oldVal <- getNth phases v+                         unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@+                         -- #phasesaving >>>>+                         loop False+  loop False++-- | __Fig. 16. (p.20)__+-- Main solve method.+--+-- __Pre-condition:__ If assumptions are used, 'simplifyDB' must be+-- called right before using this method. If not, a top-level conflict (resulting in a+-- non-usable internal state) cannot be distinguished from a conflict under assumptions.+solve :: (Foldable t) => Solver -> t Lit -> IO SolverResult+solve s@Solver{..} assumps = do+  -- PUSH INCREMENTAL ASSUMPTIONS:+  let inject :: Lit -> Bool -> IO Bool+      inject _ False = return False+      inject a True = do+        b <- assume s a+        if not b                  -- conflict analyze+          then do (confl :: Clause) <- getNth reason (lit2var a)+                  analyzeFinal s confl True+                  pushTo conflicts (negateLit a)+                  cancelUntil s 0+                  return False+          else do confl <- propagate s+                  if confl /= NullClause+                    then do analyzeFinal s confl True+                            cancelUntil s 0+                            return False+                    else return True+  good <- simplifyDB s+  x <- if good then foldrM inject True assumps else return False+  if x+    then do set' rootLevel =<< decisionLevel s+            status <- search s+            -- post-proccesing should be done here+            let toInt :: Var -> IO Lit+                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+            cancelUntil s 0     -- reset solver+            flag <- get' ok+            if | status && flag == LiftedT     -> return $ Right (SAT asg1)+               | not status && flag == LiftedF -> return $ Right (UNSAT asg2)+               | otherwise                     -> return $ Left InternalInconsistent+    else return $ Right (UNSAT [])++-- | Though 'enqueue' is defined in 'Solver', most functions in M114 use @unsafeEnqueue@.+{-# INLINABLE unsafeEnqueue #-}+unsafeEnqueue :: Solver -> Lit -> Clause -> IO ()+unsafeEnqueue s@Solver{..} p from = do+  let v = lit2var p+  setNth assigns v $ lit2lbool p+  setNth level v =<< decisionLevel s+  setNth reason v from     -- NOTE: @from@ might be NULL!+  pushTo trail p++-- | __Pre-condition:__ propagation queue is empty.+{-# INLINE unsafeAssume #-}+unsafeAssume :: Solver -> Lit -> IO ()+unsafeAssume s@Solver{..} p = do+  pushTo trailLim =<< get' trail+  unsafeEnqueue s p NullClause

@@ -0,0 +1,145 @@+-- | (This is a part of MIOS.)+-- Command line option parser+{-# LANGUAGE Safe #-}++module SAT.Mios.OptionParser+       (+         MiosConfiguration (..)+       , defaultConfiguration+       , MiosProgramOption (..)+       , miosDefaultOption+       , miosOptions+       , miosUsage+       , miosParseOptions+       , miosParseOptionsFromArgs+       , toMiosConf+       )+       where++import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo)+import System.Environment (getArgs)+import SAT.Mios.Types (MiosConfiguration (..), defaultConfiguration)++-- | configuration swithces+data MiosProgramOption = MiosProgramOption+                     {+                       _targetFile :: Maybe String+                     , _targets :: [String]+                     , _outputFile :: Maybe String+                     , _confVariableDecayRate :: !Double+                     , _confClauseDecayRate :: Double+--                     , _confRandomDecisionRate :: Int+                     , _confMaxSize :: !Int+                     , _confCheckAnswer :: !Bool+                     , _confVerbose :: !Bool+                     , _confBenchmark :: Integer+                     , _confBenchSeq :: !Int+                     , _confNoAnswer :: !Bool+                     , _confDumpStat :: !Int+                     , _validateAssignment :: !Bool+                     , _displayHelp :: !Bool+                     , _displayVersion :: !Bool+                     }++-- | default option settings+miosDefaultOption :: MiosProgramOption+miosDefaultOption = MiosProgramOption+  {+    _targetFile = Nothing+  , _targets = []+  , _outputFile = Nothing+  , _confVariableDecayRate = variableDecayRate defaultConfiguration+  , _confClauseDecayRate = clauseDecayRate defaultConfiguration+--  , _confRandomDecisionRate = randomDecisionRate defaultConfiguration+  , _confMaxSize = 4000000    -- 4,000,000 = 4M+  , _confCheckAnswer = False+  , _confVerbose = False+  , _confBenchmark = -1+  , _confBenchSeq = 0+  , _confNoAnswer = False+  , _confDumpStat = dumpStat defaultConfiguration+  , _validateAssignment = False+  , _displayHelp = False+  , _displayVersion = False+  }++-- | definition of mios option+miosOptions :: [OptDescr (MiosProgramOption -> MiosProgramOption)]+miosOptions =+  [+    Option ['d'] ["variable-decay-rate"]+    (ReqArg (\v c -> c { _confVariableDecayRate = read v }) (show (_confVariableDecayRate miosDefaultOption)))+    "[solver] variable activity decay rate (0.0 - 1.0)"+  , Option ['c'] ["clause-decay-rate"]+    (ReqArg (\v c -> c { _confClauseDecayRate = read v }) (show (_confClauseDecayRate miosDefaultOption)))+    "[solver] clause activity decay rate (0.0 - 1.0)"+--  , Option ['r'] ["random-decision-rate"]+--    (ReqArg (\v c -> c { _confRandomDecisionRate = read v }) (show (_confRandomDecisionRate miosDefaultOption)))+--    "[solver] random selection rate (0 - 1000)"+  , Option [] ["maxsize"]+    (ReqArg (\v c -> c { _confMaxSize = read v }) (show (_confMaxSize miosDefaultOption)))+    "[solver] limit of the number of variables"+  , Option [':'] ["validate-assignment"]+    (NoArg (\c -> c { _validateAssignment = True }))+    "[solver] read an assignment from STDIN and validate it"+  , Option [] ["validate"]+    (NoArg (\c -> c { _confCheckAnswer = True }))+    "[solver] self-check (satisfiable) assignment"+  , Option ['o'] ["output"]+    (ReqArg (\v c -> c { _outputFile = Just v }) "file")+    "[option] filename to store result"+{-+  , Option [] ["stdin"]+    (NoArg (\c -> c { _targetFile = Nothing }))+    "[option] read a CNF from STDIN instead of a file"+-}+  , Option ['v'] ["verbose"]+    (NoArg (\c -> c { _confVerbose = True }))+    "[option] display misc information"+  , Option ['X'] ["hide-solution"]+    (NoArg (\c -> c { _confNoAnswer = True }))+    "[option] hide solution"+  , Option [] ["benchmark"]+    (ReqArg (\v c -> c { _confBenchmark = read v }) "-1/0/N")+    "[devel] No/Exhaustive/N-second timeout benchmark"+  , Option [] ["sequence"]+    (ReqArg (\v c -> c { _confBenchSeq = read v }) "NUM")+    "[devel] set 2nd field of a CSV generated by benchmark"+  , Option [] ["dump"]+    (ReqArg (\v c -> c { _confDumpStat = read v }) (show (dumpStat defaultConfiguration)))+    "[devel] dump level; 1:solved, 2:reduction, 3:restart"+  , Option ['h'] ["help"]+    (NoArg (\c -> c { _displayHelp = True }))+    "[misc] display this message"+  , Option [] ["version"]+    (NoArg (\c -> c { _displayVersion = True }))+    "[misc] display program ID"+  ]++-- | generates help message+miosUsage :: String -> String+miosUsage mes = usageInfo mes miosOptions++-- | builds "MiosProgramOption" from string given as command option+miosParseOptions :: String -> [String] -> IO MiosProgramOption+miosParseOptions mes argv =+    case getOpt Permute miosOptions argv of+      (o, [], []) -> return $ foldl (flip id) miosDefaultOption o+      (o, l, []) -> do+        let conf = foldl (flip id) miosDefaultOption o+        return $ conf { _targetFile = Just (head l), _targets = l }+      (_, _, errs) -> ioError (userError (concat errs ++ miosUsage mes))++-- | builds "MiosProgramOption" from a String+miosParseOptionsFromArgs :: String -> IO MiosProgramOption+miosParseOptionsFromArgs mes = miosParseOptions mes =<< getArgs++-- | converts "MiosProgramOption" into "SIHConfiguration"+toMiosConf :: MiosProgramOption -> MiosConfiguration+toMiosConf opts = MiosConfiguration+                 {+                   variableDecayRate = _confVariableDecayRate opts+                 , clauseDecayRate = _confClauseDecayRate opts+--                 , randomDecisionRate = _confRandomDecisionRate opts+                 , dumpStat = _confDumpStat opts+                 }

@@ -0,0 +1,454 @@+-- | (This is a part of MIOS.)+-- Solver, the main data structure+{-# LANGUAGE+    MultiWayIf+  , RecordWildCards+  , ScopedTypeVariables+  , TupleSections+  , ViewPatterns+  #-}+{-# LANGUAGE Safe #-}++module SAT.Mios.Solver+       (+         -- * Solver+         Solver (..)+       , newSolver+         -- * Misc Accessors+       , nAssigns+       , nClauses+       , nLearnts+       , decisionLevel+       , valueVar+       , valueLit+       , locked+         -- * State Modifiers+       , setAssign+       , enqueue+       , assume+       , cancelUntil+         -- * Stats+       , StatIndex (..)+       , getStat+       , setStat+       , incrementStat+       , getStats+       , dumpSolver+       )+        where++import Control.Monad (unless, when)+import Data.List (intercalate)+import Numeric (showFFloat)+import SAT.Mios.Types+import SAT.Mios.Clause+import SAT.Mios.ClauseManager+import SAT.Mios.ClausePool++-- | __Fig. 2.(p.9)__ Internal State of the solver+data Solver = Solver+              {+                -------- Database+                clauses    :: !ClauseExtManager  -- ^ List of problem constraints.+              , learnts    :: !ClauseExtManager  -- ^ List of learnt clauses.+              , watches    :: !WatcherList       -- ^ list of constraint wathing 'p', literal-indexed+                -------- Assignment Management+              , assigns    :: !(Vec Int)         -- ^ The current assignments indexed on variables+              , phases     :: !(Vec Int)         -- ^ The last assignments indexed on variables+              , trail      :: !Stack             -- ^ List of assignments in chronological order+              , trailLim   :: !Stack             -- ^ Separator indices for different decision levels in 'trail'.+              , qHead      :: !Int'              -- ^ 'trail' is divided at qHead; assignment part and queue part+              , reason     :: !ClauseVector      -- ^ For each variable, the constraint that implied its value+              , level      :: !(Vec Int)         -- ^ For each variable, the decision level it was assigned+              , conflicts  :: !Stack             -- ^ Set of literals in the case of conflicts+                -------- Variable Order+              , activities :: !(Vec Double)      -- ^ Heuristic measurement of the activity of a variable+              , order      :: !VarHeap           -- ^ Keeps track of the dynamic variable order.+                -------- Configuration+              , config     :: !MiosConfiguration -- ^ search paramerters+              , nVars      :: !Int               -- ^ number of variables+              , claInc     :: !Double'           -- ^ Clause activity increment amount to bump with.+              , varInc     :: !Double'           -- ^ Variable activity increment amount to bump with.+              , rootLevel  :: !Int'              -- ^ Separates incremental and search assumptions.+                -------- DB Size Adjustment+              , learntSAdj :: Double'            -- ^ used in 'SAT.Mios.Main.search'+              , learntSCnt :: Int'               -- ^ used in 'SAT.Mios.Main.search'+              , maxLearnts :: Double'            -- ^ used in 'SAT.Mios.Main.search'+                -------- Working Memory+              , ok         :: !Int'              -- ^ internal flag+              , an'seen    :: !(Vec Int)         -- ^ used in 'SAT.Mios.Main.analyze'+              , an'toClear :: !Stack             -- ^ used in 'SAT.Mios.Main.analyze'+              , an'stack   :: !Stack             -- ^ used in 'SAT.Mios.Main.analyze'+              , an'lastDL  :: !Stack             -- ^ last decision level used in 'SAT.Mios.Main.analyze'+              , clsPool    :: ClausePool         -- ^ clause recycler+              , litsLearnt :: !Stack             -- ^ used in 'SAT.Mios.Main.analyze' and 'SAT.Mios.Main.search' to create a learnt clause+              , stats      :: !(Vec [Int])       -- ^ statistics information holder+              , lbd'seen   :: !(Vec Int)         -- ^ used in lbd computation+              , lbd'key    :: !Int'              -- ^ used in lbd computation+                -------- restart heuristics #62+              , emaDFast    :: !Double'          -- ^ fast ema value of LBD+              , emaDSlow    :: !Double'          -- ^ slow ema value of LBD+              , emaAFast    :: !Double'          -- ^ fast ema value of assignment+              , emaASlow    :: !Double'          -- ^ slow ema value of assignment+              , nextRestart :: !Int'             -- ^ next restart in number of conflict+              , restartMode :: Int'              -- ^ mode of restart+              }++-- | returns an everything-is-initialized solver from the arguments.+newSolver :: MiosConfiguration -> CNFDescription -> IO Solver+newSolver conf (CNFDescription nv dummy_nc _) =+  Solver+    -- Clause Database+    <$> newManager dummy_nc                -- clauses+    <*> newManager 2000                    -- learnts+    <*> newWatcherList nv 2                -- watches+    -- Assignment Management+    <*> newVec nv LBottom                  -- assigns+    <*> newVec nv LBottom                  -- phases+    <*> newStack nv                        -- trail+    <*> newStack nv                        -- trailLim+    <*> new' 0                             -- qHead+    <*> newClauseVector (nv + 1)           -- reason+    <*> newVec nv (-1)                     -- level+    <*> newStack nv                        -- conflicts+    -- Variable Order+    <*> newVec nv 0                        -- activities+    <*> newVarHeap nv                      -- order+    -- Configuration+    <*> return conf                        -- config+    <*> return nv                          -- nVars+    <*> new' 1.0                           -- claInc+    <*> new' 1.0                           -- varInc+    <*> new' 0                             -- rootLevel+    -- Learnt DB Size Adjustment+    <*> new' 100                           -- learntSAdj+    <*> new' 100                           -- learntSCnt+    <*> new' 2000                          -- maxLearnts+    -- Working Memory+    <*> new' LiftedT                       -- ok+    <*> newVec nv 0                        -- an'seen+    <*> newStack nv                        -- an'toClear+    <*> newStack nv                        -- an'stack+    <*> newStack nv                        -- an'lastDL+    <*> newClausePool 10                   -- clsPool+    <*> newStack nv                        -- litsLearnt+    <*> newVec (fromEnum EndOfStatIndex) 0 -- stats+    <*> newVec nv 0                        -- lbd'seen+    <*> new' 0                             -- lbd'key+    -- restart heuristics #62+    <*> new' 0.0                           -- emaDFast+    <*> new' 0.0                           -- emaDSlow+    <*> new' 0.0                           -- emaAFast+    <*> new' 0.0                           -- emaASlow+    <*> new' 100                           -- nextRestart+    <*> new' 1                             -- restartMode++--------------------------------------------------------------------------------+-- Accessors++-- | returns the number of current assigments.+{-# INLINE nAssigns #-}+nAssigns :: Solver -> IO Int+nAssigns = get' . trail++-- | returns the number of constraints (clauses).+{-# INLINE nClauses #-}+nClauses :: Solver -> IO Int+nClauses = get' . clauses++-- | returns the number of learnt clauses.+{-# INLINE nLearnts #-}+nLearnts :: Solver -> IO Int+nLearnts = get' . learnts++-- | returns the current decision level.+{-# INLINE decisionLevel #-}+decisionLevel :: Solver -> IO Int+decisionLevel = get' . trailLim++-- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Var'.+{-# INLINE valueVar #-}+valueVar :: Solver -> Var -> IO Int+valueVar = getNth . assigns++-- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Lit'.+{-# INLINE valueLit #-}+valueLit :: Solver -> Lit -> IO Int+valueLit (assigns -> a) p = (\x -> if positiveLit p then x else negate x) <$> getNth a (lit2var p)++-- | __Fig. 7. (p.11)__+-- returns @True@ if the clause is locked (used as a reason). __Learnt clauses only__+{-# INLINE locked #-}+locked :: Solver -> Clause -> IO Bool+locked s c = (c ==) <$> (getNth (reason s) . lit2var =<< getNth (lits c) 1)++-------------------------------------------------------------------------------- Statistics++-- | returns the value of 'StatIndex'.+{-# INLINE getStat #-}+getStat :: Solver -> StatIndex -> IO Int+getStat (stats -> v) (fromEnum -> i) = getNth v i++-- | sets to 'StatIndex'.+{-# INLINE setStat #-}+setStat :: Solver -> StatIndex -> Int -> IO ()+setStat (stats -> v) (fromEnum -> i) x = setNth v i x++-- | increments a stat data corresponding to 'StatIndex'.+{-# INLINE incrementStat #-}+incrementStat :: Solver -> StatIndex -> Int -> IO ()+incrementStat (stats -> v) (fromEnum -> i) k = modifyNth v (+ k) i++-- | returns the statistics as a list.+{-# INLINABLE getStats #-}+getStats :: Solver -> IO [(StatIndex, Int)]+getStats (stats -> v) = mapM (\i -> (i, ) <$> getNth v (fromEnum i)) [minBound .. maxBound :: StatIndex]++-------------------------------------------------------------------------------- State Modifiers++-- | assigns a value to the /n/-th variable+setAssign :: Solver -> Int -> LiftedBool -> IO ()+setAssign Solver{..} v x = setNth assigns v x++-- | __Fig. 9 (p.14)__+-- Puts a new fact on the propagation queue, as well as immediately updating the variable's value+-- in the assignment vector. If a conflict arises, @False@ is returned and the propagation queue is+-- cleared. The parameter 'from' contains a reference to the constraint from which 'p' was+-- propagated (defaults to @Nothing@ if omitted).+{-# INLINABLE enqueue #-}+enqueue :: Solver -> Lit -> Clause -> IO Bool+enqueue s@Solver{..} p from = do+{-+  -- bump psedue lbd of @from@+  when (from /= NullClause && learnt from) $ do+    l <- get' (lbd from)+    k <- (12 +) <$> decisionLevel s+    when (k < l) $ set' (lbd from) k+-}+  let signumP = lit2lbool p+  let v = lit2var p+  val <- valueVar s v+  if val /= LBottom+    then return $ val == signumP     -- Existing consistent assignment -- don't enqueue+    else do setNth assigns v signumP -- New fact, store it+            setNth level v =<< decisionLevel s+            setNth reason v from     -- NOTE: @from@ might be NULL!+            pushTo trail p+            return True++-- | __Fig. 12 (p.17)__+-- returns @False@ if immediate conflict.+--+-- __Pre-condition:__ propagation queue is empty+{-# INLINE assume #-}+assume :: Solver -> Lit -> IO Bool+assume s p = do+  pushTo (trailLim s) =<< get' (trail s)+  enqueue s p NullClause++-- | #M22: Revert to the states at given level (keeping all assignment at 'level' but not beyond).+{-# INLINABLE cancelUntil #-}+cancelUntil :: Solver -> Int -> IO ()+cancelUntil s@Solver{..} lvl = do+  dl <- decisionLevel s+  when (lvl < dl) $ do+    lim <- getNth trailLim (lvl + 1)+    ts <- get' trail+    ls <- get' trailLim+    let+      loopOnTrail :: Int -> IO ()+      loopOnTrail ((lim <) -> False) = return ()+      loopOnTrail c = do+        x <- lit2var <$> getNth trail c+        setNth phases x =<< getNth assigns x+        setNth assigns x LBottom+        -- #reason to set reason Null+        -- if we don't clear @reason[x] :: Clause@ here, @reason[x]@ remains as locked.+        -- This means we can't reduce it from clause DB and affects the performance.+        setNth reason x NullClause -- 'analyze` uses reason without checking assigns+        -- FIXME: #polarity https://github.com/shnarazk/minisat/blosb/master/core/Solver.cc#L212+        undo s x+        -- insertHeap s x              -- insertVerOrder+        loopOnTrail $ c - 1+    loopOnTrail ts+    shrinkBy trail (ts - lim)+    shrinkBy trailLim (ls - lvl)+    set' qHead =<< get' trail++-------------------------------------------------------------------------------- VarOrder++-- | Interfate to select a decision var based on variable activity.+instance VarOrder Solver where+{-+  -- | __Fig. 6. (p.10)__+  -- Creates a new SAT variable in the solver.+  newVar _ = return 0+    -- i <- nVars s+    -- Version 0.4:: push watches =<< newVec      -- push'+    -- Version 0.4:: push watches =<< newVec      -- push'+    -- push undos =<< newVec        -- push'+    -- push reason NullClause       -- push'+    -- push assigns LBottom+    -- push level (-1)+    -- push activities (0.0 :: Double)+    -- newVar order+    -- growQueueSized (i + 1) propQ+    -- return i+-}+  {-# SPECIALIZE INLINE update :: Solver -> Var -> IO () #-}+  update = increaseHeap+  {-# SPECIALIZE INLINE undo :: Solver -> Var -> IO () #-}+  undo s v = inHeap s v >>= (`unless` insertHeap s v)+  {-# SPECIALIZE INLINE select :: Solver -> IO Var #-}+  select s = do+    let+      asg = assigns s+      -- | returns the most active var (heap-based implementation)+      loop :: IO Var+      loop = do+        n <- numElementsInHeap s+        if n == 0+          then return 0+          else do+              v <- getHeapRoot s+              x <- getNth asg v+              if x == LBottom then return v else loop+    loop++-------------------------------------------------------------------------------- VarHeap++-- | A heap tree built from two 'Vec'.+-- This implementation is identical wtih that in Minisat-1.14.+-- Note: the zero-th element of @heap@ is used for holding the number of elements.+-- Note: VarHeap itself is not a @VarOrder@, because it requires a pointer to solver.+data VarHeap = VarHeap+                {+                  heap :: !Stack  -- order to var+                , idxs :: !Stack  -- var to order (index)+                }++newVarHeap :: Int -> IO VarHeap+newVarHeap n = do+  v1 <- newVec n 0+  v2 <- newVec n 0+  let+    loop :: Int -> IO ()+    loop ((<= n) -> False) = set' v1 n >> set' v2 n+    loop i = setNth v1 i i >> setNth v2 i i >> loop (i + 1)+  loop 1+  return $ VarHeap v1 v2++{-# INLINE numElementsInHeap #-}+numElementsInHeap :: Solver -> IO Int+numElementsInHeap = get' . heap . order++{-# INLINE inHeap #-}+inHeap :: Solver -> Var -> IO Bool+inHeap Solver{..} n = case idxs order of at -> (/= 0) <$> getNth at n++{-# INLINE increaseHeap #-}+increaseHeap :: Solver -> Int -> IO ()+increaseHeap s@Solver{..} n = case idxs order of+                                at -> inHeap s n >>= (`when` (percolateUp s =<< getNth at n))++{-# INLINABLE percolateUp #-}+percolateUp :: Solver -> Int -> IO ()+percolateUp Solver{..} start = do+  let VarHeap to at = order+  v <- getNth to start+  ac <- getNth activities v+  let+    loop :: Int -> IO ()+    loop i = do+      let iP = div i 2          -- parent+      if iP == 0+        then setNth to i v >> setNth at v i -- end+        else do+            v' <- getNth to iP+            acP <- getNth activities v'+            if ac > acP+              then setNth to i v' >> setNth at v' i >> loop iP -- loop+              else setNth to i v >> setNth at v i              -- end+  loop start++{-# INLINABLE percolateDown #-}+percolateDown :: Solver -> Int -> IO ()+percolateDown Solver{..} start = do+  let (VarHeap to at) = order+  n <- getNth to 0+  v <- getNth to start+  ac <- getNth activities v+  let+    loop :: Int -> IO ()+    loop i = do+      let iL = 2 * i            -- left+      if iL <= n+        then do+            let iR = iL + 1     -- right+            l <- getNth to iL+            r <- getNth to iR+            acL <- getNth activities l+            acR <- getNth activities r+            let (ci, child, ac') = if iR <= n && acL < acR then (iR, r, acR) else (iL, l, acL)+            if ac' > ac+              then setNth to i child >> setNth at child i >> loop ci+              else setNth to i v >> setNth at v i -- end+        else setNth to i v >> setNth at v i       -- end+  loop start++{-# INLINABLE insertHeap #-}+insertHeap :: Solver -> Var -> IO ()+insertHeap s@(order -> VarHeap to at) v = do+  n <- (1 +) <$> getNth to 0+  setNth at v n+  setNth to n v+  set' to n+  percolateUp s n++-- | returns the value on the root (renamed from @getmin@).+{-# INLINABLE getHeapRoot #-}+getHeapRoot :: Solver -> IO Int+getHeapRoot s@(order -> VarHeap to at) = do+  r <- getNth to 1+  l <- getNth to =<< getNth to 0 -- the last element's value+  setNth to 1 l+  setNth at l 1+  setNth at r 0+  modifyNth to (subtract 1) 0 -- pop+  n <- getNth to 0+  when (1 < n) $ percolateDown s 1+  return r++-------------------------------------------------------------------------------- dump++{-# INLINABLE dumpSolver #-}+-- | print statatistic data to stdio. This should be called after each restart.+dumpSolver :: DumpMode -> Solver -> IO ()++dumpSolver NoDump _ = return ()++dumpSolver DumpCSVHeader s@Solver{..} = do+  sts <- init <$> getStats s+  let labels = map (show . fst) sts  ++ ["emaDFast", "emaDSlow", "emaAFast", "emaASlow"]+  putStrLn $ intercalate "," labels++dumpSolver DumpCSV s@Solver{..} = do+  -- First update the stat data+  df <- get' emaDFast+  ds <- get' emaDSlow+  af <- get' emaAFast+  as <- get' emaASlow+  sts <- init <$> getStats s+  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+  -- Additional data which type is Double+  let emas = [("emaDFast", df), ("emaDSlow", ds), ("emaAFast", af), ("emaASlow", as)]+      fs x = showFFloat (Just 3) x ""+      vals = map (show . snd) sts ++ map (fs . snd) emas+  putStrLn $ intercalate "," vals++-- | FIXME: use Util/Stat+dumpSolver DumpJSON _ = return ()                -- mode 2: JSON

@@ -0,0 +1,337 @@+-- | (This is a part of MIOS.)+-- Basic data types used throughout mios.+{-# LANGUAGE+    BangPatterns+  , PatternSynonyms+  #-}+{-# LANGUAGE Safe #-}++module SAT.Mios.Types+       (+         -- * Interface to caller+         SolverResult+       , Certificate (..)+       , SolverException (..)+       , CNFDescription (..)+         -- * Solver Configuration+       , MiosConfiguration (..)+       , defaultConfiguration+         -- * internal structure+       ,  module SAT.Mios.Vec+         -- *  Variable+       , Var+       , bottomVar+       , int2var+         -- * Internal encoded Literal+       , Lit+       , lit2int+       , int2lit+       , bottomLit+       , positiveLit+       , lit2var+       , var2lit+       , negateLit+         -- * Assignment on the lifted Bool domain+       , LiftedBool+       , lit2lbool+       , Int (LiftedF, LiftedT, LBottom, Conflict)+       -- a heap+       , VarOrder (..)+         -- * statistics+       , StatIndex (..)+       , DumpMode (..)+{-+         -- * dump statistics+       , DumpTag (..)+       , DumpedValue+       , MiosStats (..)+       , QuadLearntC (..)+       , MiosDump (..)+-}+       )+       where++import Data.Bits+import SAT.Mios.Vec++-- | terminate and find an SAT/UNSAT answer+data Certificate+  = SAT [Int]+  | UNSAT [Int]                 -- FIXME: replace with DRAT+  deriving (Eq, Ord, Read, Show)++-- | abnormal termination flags+data SolverException+  = StateUNSAT                  -- 0+  | StateSAT                    -- 1+  | OutOfMemory                 -- 2+  | TimeOut                     -- 3+  | InternalInconsistent        -- 4+  | UndescribedError            -- 5+  deriving (Bounded, Enum, Eq, Ord, Show)++-- | the type that Mios returns+-- This captures the following three cases:+--  * solved with a satisfiable assigment,+--  * proved that it's an unsatisfiable problem, and+--  * aborted due to Mios specification or an internal error+type SolverResult = Either SolverException Certificate++-- | represents "Var".+type Var = Int++-- | Special constant in 'Var' (p.7)+bottomVar :: Var+bottomVar = 0++-- | converts a usual Int as literal to an internal 'Var' presentation.+--+-- >>> int2var 1+-- 1  -- the first literal is the first variable+-- >>> int2var 2+-- 2  -- literal @2@ is variable 2+-- >>> int2var (-2)+-- 2 -- literal @-2@ is corresponding to variable 2+--+{-# INLINE int2var #-}+int2var :: Int -> Int+int2var = abs++-- | The literal data has an 'index' method which converts the literal to+-- a "small" integer suitable for array indexing. The 'var'  method returns+-- the underlying variable of the literal, and the 'sign' method if the literal+-- is signed (False for /x/ and True for /-x/).+type Lit = Int++-- | Special constant in 'Lit' (p.7)+bottomLit :: Lit+bottomLit = 0++{-+-- | converts "Var" into 'Lit'+newLit :: Var -> Lit+newLit = error "newLit undefined"+-}++-- | returns @True@ if the literal is positive+{-# INLINE positiveLit #-}+positiveLit :: Lit -> Bool+positiveLit = even++-- | negates literal+--+-- >>> negateLit 2+-- 3+-- >>> negateLit 3+-- 2+-- >>> negateLit 4+-- 5+-- >>> negateLit 5+-- 4+{-# INLINE negateLit #-}+negateLit :: Lit -> Lit+negateLit l = complementBit l 0 -- if even l then l + 1 else l - 1++----------------------------------------+----------------- Var+----------------------------------------++-- | converts 'Lit' into 'Var'.+--+-- >>> lit2var 2+-- 1+-- >>> lit2var 3+-- 1+-- >>> lit2var 4+-- 2+-- >>> lit2var 5+-- 2+{-# INLINE lit2var #-}+lit2var :: Lit -> Var+lit2var !n = shiftR n 1++-- | converts a 'Var' to the corresponing literal.+--+-- >>> var2lit 1 True+-- 2+-- >>> var2lit 1 False+-- 3+-- >>> var2lit 2 True+-- 4+-- >>> var2lit 2 False+-- 5+{-# INLINE var2lit #-}+var2lit :: Var -> Bool -> Lit+var2lit !v True = shiftL v 1+var2lit !v _ = shiftL v 1 + 1++----------------------------------------+----------------- Int+----------------------------------------++-- | converts 'Int' into 'Lit' as @lit2int . int2lit == id@.+--+-- >>> int2lit 1+-- 2+-- >>> int2lit (-1)+-- 3+-- >>> int2lit 2+-- 4+-- >>> int2lit (-2)+-- 5+--+{-# INLINE int2lit #-}+int2lit :: Int -> Lit+int2lit n+  | 0 < n = 2 * n+  | otherwise = -2 * n + 1++-- | converts `Lit' into 'Int' as @int2lit . lit2int == id@.+--+-- >>> lit2int 2+-- 1+-- >>> lit2int 3+-- -1+-- >>> lit2int 4+-- 2+-- >>> lit2int 5+-- -2+{-# INLINE lit2int #-}+lit2int :: Lit -> Int+lit2int l = case divMod l 2 of+  (i, 0) -> i+  (i, _) -> - i++-- | Lifted Boolean domain (p.7) that extends 'Bool' with "⊥" means /undefined/+-- design note: _|_ should be null = 0; True literals are coded to even numbers. So it should be 2.+type LiftedBool = Int++-- | /FALSE/ on the Lifted Bool domain+pattern LiftedF :: Int+pattern LiftedF = -1++-- | /TRUE/ on the Lifted Bool domain+pattern LiftedT :: Int+pattern LiftedT = 1++-- | /UNDEFINED/ on the Lifted Bool domain+pattern LBottom :: Int+pattern LBottom = 0++-- | /CONFLICT/ on the Lifted Bool domain+pattern Conflict :: Int+pattern Conflict = 2++-- | returns the value of a literal as a 'LiftedBool'+{-# INLINE lit2lbool #-}+lit2lbool :: Lit -> LiftedBool+lit2lbool l = if positiveLit l then LiftedT else LiftedF++{-+-- | converts 'Bool' into 'LBool'+{-# INLINE lbool #-}+lbool :: Bool -> LiftedBool+lbool True = LTrue+lbool False = LFalse+-}++-- | Assisting ADT for the dynamic variable ordering of the solver.+-- The constructor takes references to the assignment vector and the activity+-- vector of the solver. The method 'select' will return the unassigned variable+-- with the highest activity.+class VarOrder o where+{-+  -- | constructor+  newVarOrder :: (VecFamily v1 Bool, VecFamily v2 Double) => v1 -> v2 -> IO o+  newVarOrder _ _ = error "newVarOrder undefined"++  -- | Called when a new variable is created.+  newVar :: o -> IO Var+  newVar = error "newVar undefined"+-}+  -- | should be called when a variable has increased in activity.+  update :: o -> Var -> IO ()+  update _  = error "update undefined"+{-+  -- | should be called when all variables have been assigned.+  updateAll :: o -> IO ()+  updateAll = error "updateAll undefined"+-}+  -- | should be called when a variable becomes unbound (may be selected again).+  undo :: o -> Var -> IO ()+  undo _ _  = error "undo undefined"++  -- | returns a new, unassigned var as the next decision.+  select :: o -> IO Var+  select    = error "select undefined"++-- | Misc information on a CNF+data CNFDescription = CNFDescription+  {+    _numberOfVariables :: !Int           -- ^ the number of variables+  , _numberOfClauses :: !Int             -- ^ the number of clauses+  , _pathname :: Maybe FilePath          -- ^ given filename+  }+  deriving (Eq, Ord, Read, Show)++-- | Solver's parameters; random decision rate was dropped.+data MiosConfiguration = MiosConfiguration+                         {+                           variableDecayRate  :: !Double  -- ^ decay rate for variable activity+                         , clauseDecayRate    :: !Double  -- ^ decay rate for clause activity+                         , dumpStat           :: !Int     -- ^ dump stats data during solving+                         }+  deriving (Eq, Ord, Read, Show)++-- | dafault configuration+--+-- * Minisat-1.14 uses @(0.95, 0.999, 0.2 = 20 / 1000)@.+-- * Minisat-2.20 uses @(0.95, 0.999, 0)@.+-- * Gulcose-4.0  uses @(0.8 , 0.999, 0)@.+-- * Mios-1.2     uses @(0.95, 0.999, 0)@.+--+defaultConfiguration :: MiosConfiguration+defaultConfiguration = MiosConfiguration 0.95 0.999 0++-------------------------------------------------------------------------------- Statistics++-- | stat index+data StatIndex =+    NumOfBackjump               -- ^ the number of backjump+  | NumOfRestart                -- ^ the number of restart+  | NumOfBlockRestart           -- ^ the number of blacking start+  | NumOfGeometricRestart       -- ^ the number of classic restart+  | NumOfPropagation            -- ^ the number of propagation+  | NumOfReduction              -- ^ the number of reduction+  | NumOfClause                 -- ^ the number of 'alive' given clauses+  | NumOfLearnt                 -- ^ the number of 'alive' learnt clauses+  | NumOfVariable               -- ^ the number of 'alive' variables+  | NumOfAssigned               -- ^ the number of assigned variables+  | EndOfStatIndex              -- ^ Don't use this dummy.+  deriving (Bounded, Enum, Eq, Ord, Read, Show)++-- | formats of state dump+data DumpMode = NoDump | DumpCSVHeader | DumpCSV | DumpJSON+  deriving (Bounded, Enum, Eq, Ord, Read, Show)++data DumpTag = TerminateS+             | PropagationS+             | ConflictS+             | LearntS+             | BackjumpS+             | RestartS+             | LearningRateS+             | ExtraS+             deriving (Bounded, Enum, Eq, Ord, Read, Show)++type DumpedValue = (DumpTag, Either Double Int)++newtype MiosStats = MiosStats [DumpedValue]+  deriving (Eq, Ord, Read, Show)++data MiosDump =+  MiosDump { _dumpedConf ::  (String, MiosConfiguration)+           , _dupmedCNFDesc :: CNFDescription+           , _dumpedStat :: MiosStats+           }+  deriving (Eq, Ord, Read, Show)

@@ -0,0 +1,249 @@+{-# LANGUAGE BangPatterns, FlexibleInstances, ViewPatterns, UndecidableInstances #-}+{-# LANGUAGE Safe #-}++-- | Boolean Expression module to build CNF from arbitrary expressions+-- Tseitin translation: http://en.wikipedia.org/wiki/Tseitin_transformation+module SAT.Mios.Util.BoolExp+       (+         -- * Class & Type+         BoolComponent (..)+       , BoolForm (..)+         -- * Expression contructors+       , (-|-)+       , (-&-)+       , (-=-)+       , (-!-)+       , (->-)+       , neg+         -- * List Operation+       , disjunctionOf+       , (-|||-)+       , conjunctionOf+       , (-&&&-)+         -- * Convert function+       , asList+       , asList_+       , asLatex+       , asLatex_+       , numberOfVariables+       , numberOfClauses+       , tseitinBase+       )+       where++import Data.List (foldl', intercalate)++-- | the start index for the generated variables by Tseitin encoding+tseitinBase :: Int+tseitinBase = 1600000++data L = L Int++-- | class of objects that can be interpeted as a bool expression+class BoolComponent a where+  toBF :: a -> BoolForm   -- lift to BoolForm++-- | CNF expression+data BoolForm = Cnf (Int, Int) [[Int]]+    deriving (Eq, Show)++instance BoolComponent Int where+  toBF a = Cnf (abs a, max tseitinBase (abs a)) [[a]]++instance BoolComponent L where+  toBF (L a) = Cnf (abs a, max tseitinBase (abs a)) [[a]]++instance BoolComponent [Char] where+  toBF (read -> a) = Cnf (abs a, max tseitinBase (abs a)) [[a]]++instance BoolComponent BoolForm where+  toBF = id++-- | returns the number of variables in the 'BoolForm'+numberOfVariables :: BoolForm -> Int+numberOfVariables (Cnf (a, b) _) = a + b - tseitinBase++-- | returns the number of clauses in the 'BoolForm'+numberOfClauses :: BoolForm -> Int+numberOfClauses (Cnf _ l) = length l++boolFormTrue :: BoolForm+boolFormTrue = Cnf (-1, 1) []++boolFormFalse :: BoolForm+boolFormFalse = Cnf (-1, -1) []++instance BoolComponent Bool where+  toBF True = boolFormTrue+  toBF False = boolFormFalse++isTrue :: BoolForm -> Bool+isTrue = (== boolFormTrue)++isFalse :: BoolForm -> Bool+isFalse = (== boolFormFalse)++-- | return a 'clause' list only if it contains some real clause (not a literal)+clausesOf :: BoolForm -> [[Int]]+clausesOf cnf@(Cnf _ [[]]) = []+clausesOf cnf@(Cnf _ [[x]]) = []+clausesOf cnf@(Cnf _ l) = l++maxRank :: BoolForm -> Int+maxRank (Cnf (n, _) _) = n++-- | returns the number of valiable used as the output of this expression.+-- and returns itself it the expression is a literal.+-- Otherwise the number is a integer larger than 'tseitinBase'.+-- Therefore @1 + max tseitinBase the-returned-value@ is the next literal variable for future.+tseitinNumber :: BoolForm -> Int+tseitinNumber (Cnf (m, n) [[x]]) = x+tseitinNumber (Cnf (_, n) _) = n++renumber :: Int -> BoolForm -> (BoolForm, Int)+renumber base (Cnf (m, n) l)+  | l == [] = (Cnf (m, n) l, 0)+  | tseitinBase < base = (Cnf (m, n') l', n')+  | otherwise = (Cnf (n', tseitinBase) l', n')+  where+    l' = map (map f) l+    n' = maximum $ map maximum l'+    offset = base - tseitinBase - 1+    f x = if abs x < tseitinBase then x else signum x * (abs x + offset)++instance Ord BoolForm where+  compare (Cnf _ a) (Cnf _ b) = compare a b++-- | disjunction constructor+--+-- >>> asList $ "3" -|- "4"+-- [[3,4,-5],[-3,5],[-4,5]]+--+-- >>> asList (("3" -|- "4") -|- "-1")+-- [[3,4,-5],[-3,5],[-4,5],[5,-1,-6],[-5,6],[1,6]]+--+(-|-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm+(toBF -> e1) -|- (toBF -> e2')+  | isTrue e1 || isTrue e2' = boolFormTrue+  | isFalse e1 && isFalse e2' = boolFormFalse+  | isFalse e1 = e2'+  | isFalse e2' = e1+  | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[a, b, - c], [- a, c], [- b, c]]+  where+    a = tseitinNumber e1+    (e2, b) = renumber (1 + max tseitinBase a) e2'+    m = max (maxRank e1) (maxRank e2)+    c = 1 + max tseitinBase (max a b)++-- | conjunction constructor+--+-- >>> asList $ "3" -&- "-2"+-- [[-3,2,4],[3,-4],[-2,-4]]+--+-- >>> asList $ "3" -|- ("1" -&- "2")+-- [[-1,-2,4],[1,-4],[2,-4],[3,4,-5],[-3,5],[-4,5]]+--+(-&-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm+(toBF -> e1) -&- (toBF -> e2')+  | isTrue e1 && isTrue e2' = boolFormTrue+  | isFalse e1 || isFalse e2' = boolFormFalse+  | isTrue e1 = e2'+  | isTrue e2' = e1+  | otherwise = Cnf (m, c) $ clausesOf e1 ++ clausesOf e2 ++ [[- a, - b, c], [a, - c], [b, - c]]+  where+    a = tseitinNumber e1+    (e2, b) = renumber (1 + max tseitinBase a) e2'+    m = max (maxRank e1) (maxRank e2)+    c = 1 + max tseitinBase (max a b)++-- | negate a form+--+-- >>> asList $ neg ("1" -|- "2")+-- [[1,2,-3],[-1,3],[-2,3],[-3,-4],[3,4]]+neg :: (BoolComponent a) => a -> BoolForm+neg (toBF -> e) =+  Cnf (m, c) $ clausesOf e ++ [[- a, - c], [a, c]]+  where+    a = tseitinNumber e+    m = maxRank e+    c = 1 + max tseitinBase a++-- | equal on BoolForm+(-=-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm+(toBF -> e1) -=- (toBF -> e2) = (e1 -&- e2) -|- (neg e1 -&- neg e2)++-- | negation on BoolForm+(-!-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm+(toBF -> e1) -!- (toBF -> e2) = (neg e1 -&- e2) -|- (e1 -&- neg e2)++-- | implication as a short cut+--+-- >>> asList ("1" ->- "2")+-- [[-1,-3],[1,3],[3,2,-4],[-3,4],[-2,4]]+(->-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm+(toBF -> a) ->- (toBF -> b) = (neg a) -|- b++-- | merge [BoolForm] by '(-|-)'+disjunctionOf :: [BoolForm] -> BoolForm+disjunctionOf [] = boolFormFalse+disjunctionOf (x:l) = foldl' (-|-) x l++-- | an alias of 'disjunctionOf'+(-|||-) :: [BoolForm] -> BoolForm+(-|||-) = disjunctionOf++-- | merge [BoolForm] by '(-&-)'+conjunctionOf :: [BoolForm] -> BoolForm+conjunctionOf [] = boolFormTrue+conjunctionOf (x:l) = foldl' (-&-) x l++-- | an alias of 'conjunctionOf'+(-&&&-) :: [BoolForm] -> BoolForm+(-&&&-) = conjunctionOf++-- | converts a BoolForm to "[[Int]]"+asList_ :: BoolForm -> [[Int]]+asList_ cnf@(Cnf (m,_) _)+  | isTrue cnf = []+  | isFalse cnf = [[]]+  | otherwise = l'+  where+    (Cnf _ l', _) = renumber (m + 1) cnf++-- | converts a *satisfied* BoolForm to "[[Int]]"+asList :: BoolForm -> [[Int]]+asList cnf@(Cnf (m,n) l)+  | isTrue cnf = []+  | isFalse cnf = [[]]+  | n <= tseitinBase = l+  | otherwise = [m'] : l'+  where+    (Cnf (m', _) l', _) = renumber (m + 1) cnf++-- | make latex string from CNF, using 'asList_'+--+-- >>> asLatex $ "3" -|- "4"+-- "\\begin{displaymath}\n( x_{3} \\vee x_{4} )\n\\end{displaymath}\n"+--+asLatex_ :: BoolForm -> String+asLatex_ b = beg ++ s ++ end+  where+    beg = "\\begin{displaymath}\n"+    end = "\n\\end{displaymath}\n"+    s = intercalate " \\wedge " [ makeClause c | c <- asList_ b]+    makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")"+    makeLiteral l+      | 0 < l = " x_{" ++ show l ++ "} "+      | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} "++-- | make latex string from CNF, using 'asList'+asLatex :: BoolForm -> String+asLatex b = beg ++ s ++ end+  where+    beg = "\\begin{displaymath}\n"+    end = "\n\\end{displaymath}\n"+    s = intercalate " \\wedge " [ makeClause c | c <- asList b]+    makeClause c = "(" ++ intercalate "\\vee" [makeLiteral l | l <- c] ++ ")"+    makeLiteral l+      | 0 < l = " x_{" ++ show l ++ "} "+      | otherwise = " \\neg " ++ "x_{" ++ show (negate l) ++ "} "

@@ -0,0 +1,31 @@+{-# LANGUAGE Safe #-}++-- | Read/Write a CNF file only with ghc standard libraries+module SAT.Mios.Util.DIMACS+       (+         -- * Input+         fromFile+       , clauseListFromFile+       , fromMinisatOutput+       , clauseListFromMinisatOutput+         -- * Output+       , toFile+       , toDIMACSString+       , asDIMACSString+       , asDIMACSString_+         -- * Bool Operation+       , module SAT.Mios.Util.BoolExp+       )+       where+import SAT.Mios.Util.DIMACS.Reader+import SAT.Mios.Util.DIMACS.Writer+import SAT.Mios.Util.DIMACS.MinisatReader+import SAT.Mios.Util.BoolExp++-- | String from BoolFrom+asDIMACSString :: BoolForm -> String+asDIMACSString = toDIMACSString . asList++-- | String from BoolFrom+asDIMACSString_ :: BoolForm -> String+asDIMACSString_ = toDIMACSString . asList_

@@ -0,0 +1,77 @@+{-# LANGUAGE Safe #-}++-- | Read an output file of minisat+module SAT.Mios.Util.DIMACS.MinisatReader+       (+         -- * Interface+         fromMinisatOutput+       , clauseListFromMinisatOutput+       )+       where+-- import Control.Applicative ((<$>), (<*>), (<*), (*>))+import Data.Char+import Text.ParserCombinators.ReadP++-- parser+-- |parse a non-signed integer+{-# INLINE pint #-}+pint :: ReadP Int+pint = do+  n <- munch isDigit+  return (read n :: Int)++{-# INLINE mint #-}+mint :: ReadP Int+mint = do+  char '-'+  n <- munch isDigit+  return (- (read n::Int))++-- |parse a (signed) integer+{-# INLINE int #-}+int :: ReadP Int+int = mint <++ pint++-- |return integer list that terminates at zero+{-# INLINE seqNums #-}+seqNums :: ReadP [Int]+seqNums = do+  skipSpaces+  x <- int+  skipSpaces+  if x == 0 then return []  else (x :) <$> seqNums++-- |top level interface for parsing CNF+{-# INLINE parseMinisatOutput #-}+parseMinisatOutput :: ReadP ((Int, Int), [Int])+parseMinisatOutput = do+  string "SAT"+  skipSpaces+  l <- seqNums+  return ((length l,0), l)++-- |read a minisat output:+-- ((numbefOfVariables, 0), [Literal])+--+-- >>>  fromFile "result"+-- ((3, 0), [1, -2, 3])+--+{-# INLINE fromMinisatOutput #-}+fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int]))+fromMinisatOutput f = do+  c <- readFile f+  case readP_to_S parseMinisatOutput c of+    [(a, _)] -> return $ Just a+    _ -> return Nothing++-- | return clauses as [[Int]] from 'file'+--+-- >>> clauseListFromMinisatOutput "result"+-- [1,-2,3]+--+clauseListFromMinisatOutput :: FilePath -> IO [Int]+clauseListFromMinisatOutput l = do+  res <- fromMinisatOutput l+  case res of+    Just p -> return (snd p)+    _ -> return []

@@ -0,0 +1,143 @@+{-# LANGUAGE Safe #-}++-- | Read a CNF file without haskell-platform+module SAT.Mios.Util.DIMACS.Reader+       (+         -- * Interface+         fromFile+       , clauseListFromFile+       )+       where+import Control.Applicative ((<$>), (<*>), (<*), (*>))+import Data.Char+import Text.ParserCombinators.ReadP++-- parser+{-# INLINE newline #-}+newline :: ReadP Char+newline = char '\n'++{-# INLINE digit #-}+digit :: ReadP Char+digit = satisfy isDigit++{-# INLINE spaces #-}+spaces :: ReadP String+spaces = munch (`elem` " \t")++{-# INLINE noneOf #-}+noneOf :: Foldable t => t Char -> ReadP Char+noneOf s = satisfy (`notElem` s)++-- |parse a non-signed integer+{-# INLINE pint #-}+pint :: ReadP Int+pint = do+  n <- munch isDigit+  return (read n :: Int)++{-# INLINE mint #-}+mint :: ReadP Int+mint = do+  char '-'+  n <- munch isDigit+  return (- (read n::Int))++-- |parse a (signed) integer+{-# INLINE int #-}+int :: ReadP Int+int = mint <++ pint++-- |Parse something like: p FORMAT VARIABLES CLAUSES+{-# INLINE problemLine #-}+problemLine :: ReadP (Int, Int)+problemLine = do+  char 'p'+  skipSpaces+  (string "cnf" <++ string "CNF")+  skipSpaces+  vars <- pint+  skipSpaces+  clas <- pint+  spaces+  newline+  return (vars, clas)++-- |Parse something like: c This in an example of a comment line.+{-# INLINE commentLines #-}+commentLines :: ReadP ()+commentLines = do+  l <- look+  if (head l)  == 'c'+    then do+      munch ('\n' /=)+      newline+      commentLines+    else return ()++_commentLines :: ReadP ()+_commentLines = do+  char 'c'+  munch ('\n' /=)+  newline+  l <- look+  if (head l)  == 'c' then commentLines else return ()++-- |Parse the preamble part+{-# INLINE preambleCNF #-}+preambleCNF :: ReadP (Int, Int)+preambleCNF = do+  commentLines+  problemLine++-- |return integer list that terminates at zero+{-# INLINE seqNums #-}+seqNums :: ReadP [Int]+seqNums = do+  skipSpaces+  x <- int+  skipSpaces+  if (x == 0) then return []  else (x :) <$> seqNums++-- |Parse something like: 1 -2 0 4 0 -3 0+{-# INLINE parseClauses #-}+parseClauses :: Int -> ReadP [[Int]]+parseClauses n = count n seqNums++-- |top level interface for parsing CNF+{-# INLINE parseCNF #-}+parseCNF :: ReadP ((Int, Int), [[Int]])+parseCNF = do+  a <- preambleCNF+  b <- parseClauses (snd a)+  return (a, b)++-- |driver:: String -> Either ParseError Int+driver :: String -> [([[Int]], String)]+driver input = readP_to_S (parseClauses 1) input++-- |read a CNF file and return:+-- ((numbefOfVariables, numberOfClauses), [Literal])+--+-- >>> fromFile "acnf"+-- ((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]]+--+{-# INLINE fromFile #-}+fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]]))+fromFile f = do+  c <- readFile f+  case readP_to_S parseCNF c of+    [(a, _)] -> return $ Just a+    _ -> return Nothing++-- | return clauses as [[Int]] from 'file'+--+-- >>> clauseListFromFile "a.cnf"+-- [[1, 2], [-2, 3], [-1, 2, -3], [3]]+--+clauseListFromFile :: FilePath -> IO [[Int]]+clauseListFromFile l = do+  res <- fromFile l+  case res of+    Just (_, l) -> return l+    _ -> return []

@@ -0,0 +1,58 @@+{-# LANGUAGE Safe #-}++-- | Write SAT data to DIMACS file+module SAT.Mios.Util.DIMACS.Writer+       (+         -- * Interface+         toFile+       , toDIMACSString+       , toString+       , toLatexString+       )+       where+import Data.List (intercalate, nub, sort)+import System.IO++-- | Write the DIMACS to file 'f', using 'toDIMACSString'+toFile :: FilePath -> [[Int]] -> IO ()+toFile f l = writeFile f $ toDIMACSString l++-- | Convert [Clause] to String, where Clause is [Int]+--+-- >>> toDIMACSString []+-- "p cnf 0 0\n"+--+-- >>> toDIMACSString [[-1, 2], [-3, -4]]+-- "p cnf 4 2\n-1 2 0\n-3 -4 0\n"+--+-- >>> toDIMACSString [[1], [-2], [-3, -4], [1,2,3,4]]+-- "p cnf 4 4\n1 0\n-2 0\n-3 -4 0\n1 2 3 4 0\n"+--+toDIMACSString :: [[Int]] -> String+toDIMACSString l = hdr ++ str+  where+    hdr = "p cnf " ++ show numV ++ " " ++ show numC ++ "\n"+    numC = length l+    numV = last $ nub $ sort $ map abs $ concat l+    str = concat [intercalate " " (map show c) ++ " 0\n" | c <- l]++-- | converts @[[Int]]@ to a String+toString  :: [[Int]] -> String -> String -> String+toString l and' or' = intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l]+  where+    lit x+      | 0 <= x = "X" ++ show x+      | otherwise = "-X" ++ show (abs x)+    a = pad and'+    o = pad or'+    pad s = " " ++ s ++ " "++-- | converts @[[Int]]@ to a LaTeX expression+toLatexString  :: [[Int]] -> String+toLatexString l = "\\begin{eqnarray*}\n" ++ intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l] ++ "\n\\end{eqnarray*}"+  where+    lit x+      | 0 <= x = "X_{" ++ show x ++ "}"+      | otherwise = "\\overline{X_{" ++ show (abs x) ++ "}}"+    a = " \n\\wedge "+    o = " \\vee "

@@ -0,0 +1,69 @@+-- | (This is a part of MIOS.)+-- Validate an assignment+{-# LANGUAGE+    RecordWildCards+  , ViewPatterns+  #-}+{-# LANGUAGE Safe #-}++module SAT.Mios.Validator+       (+         validate+--       , checkUniqueness+       )+       where++import Control.Monad (when)+import Data.Foldable (toList)+import Data.List (sort)+import SAT.Mios.Types+import SAT.Mios.Clause+import SAT.Mios.ClauseManager+import SAT.Mios.Solver++-- | validates the assignment even if the implementation of 'Solver' is wrong; we re-implement some functions here.+validate :: Traversable t => Solver -> t Int -> IO Bool+validate s t = do+  assignment <- newVec (1 + nVars s) (0 :: Int) :: IO (Vec Int)+  vec <- getClauseVector (clauses s)+  nc <- get' (clauses s)+  let+    lst = map int2lit $ toList t+    inject :: Lit -> IO ()+    inject l = setNth assignment (lit2var l) $ lit2lbool l+    -- returns True if the literal is satisfied under the assignment+    satisfied :: Lit -> IO Bool+    satisfied l+      | positiveLit l = (LiftedT ==) <$> getNth assignment (lit2var l)+      | otherwise     = (LiftedF ==) <$> getNth assignment (lit2var l)+    -- returns True is any literal in the given list+    satAny :: [Lit] -> IO Bool+    satAny [] = return False+    satAny (l:ls) = do+      sat' <- satisfied l+      if sat' then return True else satAny ls+    -- traverses all clauses in 'clauses'+    loopOnVector :: Int -> IO Bool+    loopOnVector ((< nc) -> False) = return True+    loopOnVector i = do+      sat' <- satAny =<< asList =<< getNth vec i+      if sat' then loopOnVector (i + 1) else return False+  if null lst+    then error "validator got an empty assignment."+    else mapM_ inject lst >> loopOnVector 0++-- | checks uniqueness of learnts+checkUniqueness :: Solver -> Clause -> IO ()+checkUniqueness Solver{..} c = do+  n <- get' learnts+  cvec <- getClauseVector learnts+  cls <- sort <$> asList c+  let+    loop :: Int -> IO ()+    loop ((< n) -> False) = return ()+    loop i = do+      c' <- getNth cvec i+      cls' <- sort <$> asList c'+      when (cls' == cls) $ errorWithoutStackTrace "reinsert a same clause"+      loop (i + 1)+  loop 0

@@ -0,0 +1,359 @@+-- | (This is a part of MIOS.)+-- Abstraction Layer for Mutable Vectors+{-# LANGUAGE+    BangPatterns+  , FlexibleContexts+  , FlexibleInstances+  , FunctionalDependencies+  , MultiParamTypeClasses+  , TypeFamilies+  #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Mios.Vec+       (+         -- * Vector class and type+         VecFamily (..)+       , Vec (..)+         -- * SingleStorage+       , SingleStorage (..)+       , Bool'+       , Double'+       , Int'+         -- * Stack+       , StackFamily (..)+       , Stack+       , newStackFromList+       , realLengthOfStack+       , sortStack+       )+       where++import qualified Data.Vector.Unboxed.Mutable as UV+import qualified Data.Primitive.ByteArray as BA+import Control.Monad.Primitive++-------------------------------------------------------------------------------- VecFamily+-- | The interface on vectors.+class VecFamily v a | v -> a where+  -- | returns the /n/-th value.+  getNth ::v -> Int -> IO a+  -- | sets the /n/-th value.+  setNth :: v -> Int -> a -> IO ()+  -- | erases all elements in it.+  reset:: v -> IO ()+  -- | returns the /n/-th value (index starts from zero in any case).+  -- | swaps two elements.+  swapBetween :: v -> Int -> Int -> IO ()+  -- | calls the update function.+  modifyNth :: v -> (a -> a) -> Int -> IO ()+  -- | returns a new vector.+  newVec :: Int -> a -> IO v+  -- | sets all elements.+  setAll :: v -> a -> IO ()+  -- | extends the size of stack by /n/; note: values in new elements aren't initialized maybe.+  growBy :: v -> Int -> IO v+  -- | converts to a list.+  asList :: v -> IO [a]+  {-# MINIMAL getNth, setNth #-}+  reset = errorWithoutStackTrace "no default method: reset"+  swapBetween = errorWithoutStackTrace "no default method: swapBetween"+  modifyNth = errorWithoutStackTrace "no default method: modifyNth"+  newVec = errorWithoutStackTrace "no default method: newVec"+  setAll = errorWithoutStackTrace "no default method: setAll"+  asList = errorWithoutStackTrace "no default method: asList"+  growBy = errorWithoutStackTrace "no default method: growBy"+  -- | (FOR DEBUG) dump the contents.+  -- dump :: Show a => String -> v -> IO String+  -- dump msg v = (msg ++) . show <$> asList v++-------------------------------------------------------------------------------- Vec+-- | Another abstraction layer on 'Vector' which reserves zero element for internal use.+-- __Note__: If you want to use the 0-th element, use @UVector Int@.++data family Vec a;++-------------------------------------------------------------------------------- UVector++-- | A thin abstract layer for mutable unboxed Vector+type UVector a = UV.IOVector a++instance VecFamily (UVector Int) Int where+  {-# SPECIALIZE INLINE getNth :: UVector Int -> Int -> IO Int #-}+  getNth = UV.unsafeRead+  {-# SPECIALIZE INLINE setNth :: UVector Int -> Int -> Int -> IO () #-}+  setNth = UV.unsafeWrite+  {-# SPECIALIZE INLINE modifyNth :: UVector Int -> (Int -> Int) -> Int -> IO () #-}+  modifyNth = UV.unsafeModify+  {-# SPECIALIZE INLINE swapBetween:: UVector Int -> Int -> Int -> IO () #-}+  swapBetween = UV.unsafeSwap+  {-# SPECIALIZE INLINE newVec :: Int -> Int -> IO (UVector Int) #-}+  newVec n 0 = UV.new n+  newVec n x = do v <- UV.new n+                  UV.set v x+                  return v+  {-# SPECIALIZE INLINE setAll :: UVector Int -> Int -> IO () #-}+  setAll = UV.set+  {-# SPECIALIZE INLINE growBy :: UVector Int -> Int -> IO (UVector Int) #-}+  growBy = UV.unsafeGrow+  asList v = mapM (UV.unsafeRead v) [0 .. UV.length v - 1]++-- Note: type @[Int]@ is selected for 'UVector' not to export it.+data instance Vec [Int] = Vec (UVector Int)++instance VecFamily (Vec [Int]) Int where+  {-# SPECIALIZE INLINE getNth :: Vec [Int] -> Int -> IO Int #-}+  getNth (Vec v) = UV.unsafeRead v+  {-# SPECIALIZE INLINE setNth :: Vec [Int] -> Int -> Int -> IO () #-}+  setNth (Vec v) = UV.unsafeWrite v+  {-# SPECIALIZE INLINE reset :: Vec [Int] -> IO () #-}+  reset (Vec v) = setNth v 0 0+  {-# SPECIALIZE INLINE modifyNth :: Vec [Int] -> (Int -> Int) -> Int -> IO () #-}+  modifyNth (Vec v) = UV.unsafeModify v+  {-# SPECIALIZE INLINE swapBetween :: Vec [Int] -> Int -> Int -> IO () #-}+  swapBetween (Vec v) = UV.unsafeSwap v+  {-# SPECIALIZE INLINE newVec :: Int -> Int -> IO (Vec [Int]) #-}+  newVec n x = Vec <$> newVec (n + 1) x+  {-# SPECIALIZE INLINE setAll :: Vec [Int] -> Int -> IO () #-}+  setAll (Vec v) = UV.set v+  {-# SPECIALIZE INLINE growBy :: Vec [Int] -> Int -> IO (Vec [Int]) #-}+  growBy (Vec v) n = Vec <$> UV.unsafeGrow v n+  asList (Vec v) = mapM (getNth v) [0 .. UV.length v - 1]++{- NOT IN USE+data instance Vec [Double] = Vec (UVector Double)++instance VecFamily (UVector Double) Double where+  {-# SPECIALIZE INLINE getNth :: UVector Double -> Int -> IO Double #-}+  getNth = UV.unsafeRead+  {-# SPECIALIZE INLINE setNth :: UVector Double -> Int -> Double -> IO () #-}+  setNth = UV.unsafeWrite+  {-# SPECIALIZE INLINE modifyNth :: UVector Double -> (Double -> Double) -> Int -> IO () #-}+  modifyNth = UV.unsafeModify+  {-# SPECIALIZE INLINE swapBetween:: UVector Double -> Int -> Int -> IO () #-}+  swapBetween = UV.unsafeSwap+  {-# SPECIALIZE INLINE newVec :: Int -> Double -> IO (UVector Double) #-}+  newVec n x = do v <- UV.new n+                  UV.set v x+                  return v+  {-# SPECIALIZE INLINE setAll :: UVector Double -> Double -> IO () #-}+  setAll = UV.set+  {-# SPECIALIZE INLINE growBy :: UVector Double -> Int -> IO (UVector Double) #-}+  growBy = UV.unsafeGrow+  asList v = mapM (UV.unsafeRead v) [0 .. UV.length v - 1]++instance VecFamily (Vec Double) Double where+  {-# SPECIALIZE INLINE getNth :: Vec Double -> Int -> IO Double #-}+  getNth (Vec v) = UV.unsafeRead v+  {-# SPECIALIZE INLINE setNth :: Vec Double -> Int -> Double -> IO () #-}+  setNth (Vec v) = UV.unsafeWrite v+  {-# SPECIALIZE INLINE modifyNth :: Vec Double -> (Double -> Double) -> Int -> IO () #-}+  modifyNth (Vec v) = UV.unsafeModify v+  {-# SPECIALIZE INLINE swapBetween :: Vec Double -> Int -> Int -> IO () #-}+  swapBetween (Vec v) = UV.unsafeSwap v+  {-# SPECIALIZE INLINE newVec :: Int -> Double -> IO (Vec Double) #-}+  newVec n x = Vec <$> newVec (n + 1) x+  {-# SPECIALIZE INLINE setAll :: Vec Double -> Double -> IO () #-}+  setAll (Vec v) = UV.set v+  {-# SPECIALIZE INLINE growBy :: Vec Double -> Int -> IO (Vec Double) #-}+  growBy (Vec v) n = Vec <$> UV.unsafeGrow v n+-}++-------------------------------------------------------------------------------- ByteArray++data instance Vec Int = ByteArrayInt (BA.MutableByteArray RealWorld)+data instance Vec Double = ByteArrayDouble (BA.MutableByteArray RealWorld)++type ByteArrayInt = Vec Int+type ByteArrayDouble = Vec Double++instance VecFamily ByteArrayInt Int where+  {-# SPECIALIZE INLINE getNth :: ByteArrayInt -> Int -> IO Int #-}+  getNth (ByteArrayInt v) i = BA.readByteArray v i+  {-# SPECIALIZE INLINE setNth :: ByteArrayInt -> Int -> Int -> IO () #-}+  setNth (ByteArrayInt v) i x = BA.writeByteArray v i x+  {-# SPECIALIZE INLINE modifyNth :: ByteArrayInt -> (Int -> Int) -> Int -> IO () #-}+  modifyNth (ByteArrayInt v) f i = BA.writeByteArray v i . f =<< BA.readByteArray v i+  {-# SPECIALIZE INLINE swapBetween:: ByteArrayInt -> Int -> Int -> IO () #-}+  swapBetween (ByteArrayInt v) i j = do x <- BA.readByteArray v i+                                        y <- BA.readByteArray v j+                                        BA.writeByteArray v i (y :: Int)+                                        BA.writeByteArray v j (x :: Int)+  {-# SPECIALIZE INLINE reset :: ByteArrayInt -> IO () #-}+  reset (ByteArrayInt v) = BA.writeByteArray v 0 (0 :: Int)+  newVec n k = do v <- BA.newByteArray (8 * (n + 1))+                  BA.writeByteArray v 0 (0 :: Int)+                  BA.setByteArray v 1 n k+                  return $ ByteArrayInt v+  asList (ByteArrayInt v) = mapM (BA.readByteArray v) [0 .. div (BA.sizeofMutableByteArray v) 8 - 1]++instance VecFamily ByteArrayDouble Double where+  {-# SPECIALIZE INLINE getNth :: ByteArrayDouble -> Int -> IO Double #-}+  getNth (ByteArrayDouble v) i = BA.readByteArray v i+  {-# SPECIALIZE INLINE setNth :: ByteArrayDouble -> Int -> Double -> IO () #-}+  setNth (ByteArrayDouble v) i x = BA.writeByteArray v i x+  {-# SPECIALIZE INLINE modifyNth :: ByteArrayDouble -> (Double -> Double) -> Int -> IO () #-}+  modifyNth (ByteArrayDouble v) f i = BA.writeByteArray v i . f =<< BA.readByteArray v i+  {-# SPECIALIZE INLINE swapBetween:: ByteArrayDouble -> Int -> Int -> IO () #-}+  swapBetween (ByteArrayDouble v) i j = do x <- BA.readByteArray v i+                                           y <- BA.readByteArray v j+                                           BA.writeByteArray v i (y :: Int)+                                           BA.writeByteArray v j (x :: Int)+  {-# SPECIALIZE INLINE reset :: ByteArrayDouble -> IO () #-}+  reset (ByteArrayDouble v) = BA.writeByteArray v 0 (0 :: Double)+  newVec n k = do v <- BA.newByteArray (8 * (n + 1))+                  BA.writeByteArray v 0 (0 :: Double)+                  BA.setByteArray v 1 n k+                  return $ ByteArrayDouble v+  asList (ByteArrayDouble v) = mapM (BA.readByteArray v) [0 .. div (BA.sizeofMutableByteArray v) 8 - 1]++-------------------------------------------------------------------------------- SingleStorage++-- | Interface for single (one-length vector) mutable data+class SingleStorage s t | s -> t where+  -- | allocates and returns an new data.+  new' :: t -> IO s+  -- | gets the value.+  get' :: s -> IO t+  -- | sets the value.+  set' :: s -> t -> IO ()+  -- | calls an update function on it.+  modify' :: s -> (t -> t) -> IO ()+  {-# MINIMAL get', set' #-}+  new' = undefined+  modify' = undefined++-- | Mutable Bool+type Bool' = UV.IOVector Bool++instance SingleStorage Bool' Bool where+  {-# SPECIALIZE INLINE new' :: Bool -> IO Bool' #-}+  new' k = do s <- UV.new 1+              UV.unsafeWrite s 0 k+              return s+  {-# SPECIALIZE INLINE get' :: Bool' -> IO Bool #-}+  get' val = UV.unsafeRead val 0+  {-# SPECIALIZE INLINE set' :: Bool' -> Bool -> IO () #-}+  set' val !x = UV.unsafeWrite val 0 x+  {-# SPECIALIZE INLINE modify' :: Bool' -> (Bool -> Bool) -> IO () #-}+  modify' val f = UV.unsafeModify val f 0++-- | Mutable Int+-- __Note:__  Int' is identical to 'Stack'+type Int' = ByteArrayInt++instance SingleStorage ByteArrayInt Int where+  {-# SPECIALIZE INLINE new' :: Int -> IO ByteArrayInt #-}+  new' k = do s <- BA.newByteArray 8+              BA.writeByteArray s 0 k+              return $ ByteArrayInt s+  {-# SPECIALIZE INLINE get' :: ByteArrayInt -> IO Int #-}+  get' (ByteArrayInt v) = BA.readByteArray v 0+  {-# SPECIALIZE INLINE set' :: ByteArrayInt -> Int -> IO () #-}+  set' (ByteArrayInt v) !x = BA.writeByteArray v 0 x+  {-# SPECIALIZE INLINE modify' :: ByteArrayInt -> (Int -> Int) -> IO () #-}+  modify' (ByteArrayInt v) f = BA.writeByteArray v 0 . f =<< BA.readByteArray v 0++-- | Mutable Double+type Double' = ByteArrayDouble++instance SingleStorage ByteArrayDouble Double where+  {-# SPECIALIZE INLINE new' :: Double -> IO ByteArrayDouble #-}+  new' k = do s <- BA.newByteArray 8+              BA.writeByteArray s 0 k+              return $ ByteArrayDouble s+  {-# SPECIALIZE INLINE get' :: ByteArrayDouble -> IO Double #-}+  get' (ByteArrayDouble v) = BA.readByteArray v 0+  {-# SPECIALIZE INLINE set' :: ByteArrayDouble -> Double -> IO () #-}+  set' (ByteArrayDouble v) !x = BA.writeByteArray v 0 x+  {-# SPECIALIZE INLINE modify' :: ByteArrayDouble -> (Double -> Double) -> IO () #-}+  modify' (ByteArrayDouble v) f = BA.writeByteArray v 0 . f =<< BA.readByteArray v 0++-------------------------------------------------------------------------------- Stack++-- | Interface on stacks+class SingleStorage s Int => StackFamily s t | s -> t where+  -- | returns a new stack.+  newStack :: Int -> IO s+  -- | pushs an value to the tail of the stack.+  pushTo :: s -> t-> IO ()+  -- | pops the last element.+  popFrom :: s -> IO ()+  -- | peeks the last element.+  lastOf :: s -> IO t+  -- | shrinks the stack.+  shrinkBy :: s -> Int -> IO ()+  newStack = undefined+  pushTo = undefined+  popFrom = undefined+  lastOf = undefined+  shrinkBy = undefined++-- | Stack of Int, an alias of @Vec Int@+type Stack = Vec Int++instance StackFamily ByteArrayInt Int where+  {-# SPECIALIZE INLINE newStack :: Int -> IO ByteArrayInt #-}+  newStack n = do s <- newVec (2 * n) 0+                  setNth s 0 (0::Int)+                  return s+  {-# SPECIALIZE INLINE pushTo :: ByteArrayInt -> Int -> IO () #-}+  pushTo (ByteArrayInt v) x = do i <- (+ 1) <$> (BA.readByteArray v 0 :: IO Int)+                                 BA.writeByteArray v i x+                                 BA.writeByteArray v 0 i+  {-# SPECIALIZE INLINE popFrom :: ByteArrayInt -> IO () #-}+  popFrom (ByteArrayInt v) = BA.writeByteArray v 0 . subtract 1 =<< (BA.readByteArray v 0 :: IO Int)+  {-# SPECIALIZE INLINE lastOf :: ByteArrayInt -> IO Int #-}+  lastOf (ByteArrayInt v) = BA.readByteArray v =<< BA.readByteArray v 0+  {-# SPECIALIZE INLINE shrinkBy :: ByteArrayInt -> Int -> IO () #-}+  shrinkBy (ByteArrayInt v) k = BA.writeByteArray v 0 . subtract k =<< (BA.readByteArray v 0 :: IO Int)++-- | returns a new 'Stack' from @[Int]@.+{-# INLINABLE newStackFromList #-}+newStackFromList :: [Int] -> IO Stack+newStackFromList l = do+  v <- BA.newByteArray (8 * (length l + 1))+  let loop :: [Int] -> Int -> IO Stack+      loop [] _ = return $ ByteArrayInt v+      loop (x:l') i = BA.writeByteArray v i x >> loop l' (i + 1)+  loop (length l : l) 0++-- | returns the number of allocated slots+{-# INLINE realLengthOfStack #-}+realLengthOfStack :: Stack -> Int+realLengthOfStack (ByteArrayInt v) = div (BA.sizeofMutableByteArray v) 8++-- | sort the content of a stack, in small-to-large order.+{-# INLINABLE sortStack #-}+sortStack :: Stack -> IO ()+sortStack vec = do+  n <- get' vec+  let sortOnRange :: Int -> Int -> IO ()+      sortOnRange left right+        | n < left = return ()+        | right < 1 = return ()+        | left >= right = return ()+        | left + 1 == right = do+            a <- getNth vec left+            b <- getNth vec right+            if a < b then return () else swapBetween vec left right+        | otherwise = do+            let p = div (left + right) 2+            pivot <- getNth vec p+            swapBetween vec p left -- set a sentinel for r'+            let nextL :: Int -> IO Int+                nextL i+                  | i <= right = do v <- getNth vec i; if v < pivot then nextL (i + 1) else return i+                  | otherwise = return i+                nextR :: Int -> IO Int+                nextR i = do v <- getNth vec i; if pivot < v then nextR (i - 1) else return i+                divide :: Int -> Int -> IO Int+                divide l r = do+                  l' <- nextL l+                  r' <- nextR r+                  if l' < r' then swapBetween vec l' r' >> divide (l' + 1) (r' - 1) else return r'+            m <- divide (left + 1) right+            swapBetween vec left m+            sortOnRange left (m - 1)+            sortOnRange (m + 1) right+  sortOnRange 1 n