mios 1.6.0 → 1.6.2

raw patch · 15 files changed

+768/−611 lines, 15 filesdep +gitrevdep +hspecnew-component:exe:mios162PVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: gitrev, hspec

API changes (from Hackage documentation)

Files

• app/DiscordSecret.hs +6/−0
• app/mios.hs +11/−6
• mios.cabal +61/−32
• src/SAT/Mios.hs +236/−151
• src/SAT/Mios/Clause.hs +31/−8
• src/SAT/Mios/ClauseManager.hs +27/−5
• src/SAT/Mios/ClausePool.hs +7/−13
• src/SAT/Mios/Criteria.hs +171/−149
• src/SAT/Mios/Main.hs +62/−83
• src/SAT/Mios/OptionParser.hs +34/−26
• src/SAT/Mios/Solver.hs +30/−55
• src/SAT/Mios/Types.hs +54/−11
• src/SAT/Mios/Vec.hs +16/−72
• test/MiosSpec.hs +14/−0
• test/Spec.hs +8/−0

@@ -0,0 +1,6 @@+-- join to a server:+-- https://discordapp.com/oauth2/authorize?&client_id=431666856785346560&scope=bot&permissions=0+module DiscordSecret (token) where++token :: String+token = "NDQ4ODM2NDM0MjkyNjM3NzA2.Deb7VA.v1mtGLLwG0GK9kbqNko7D_R14Bc"

@@ -1,5 +1,6 @@ {-# LANGUAGE-   MultiWayIf+    MultiWayIf+  , TemplateHaskell   #-} -- | Executable of 'Minisat Implementation and Optimization Study' module Main@@ -9,16 +10,20 @@        where  import SAT.Mios+import Development.GitRev +gitId :: String+gitId = "mios " ++ versionId ++ "/commit/" ++ $(gitHash)+ usage :: String-usage = miosUsage $ versionId ++ "\nUsage: mios [OPTIONS] target.cnf"+usage = miosUsage $ gitId ++ "\nUsage: mios [OPTIONS] target.cnf"  -- | main main :: IO () main = do opts <- miosParseOptionsFromArgs versionId-          if | _displayVersion opts        -> putStrLn versionId+          if | _displayVersion opts        -> putStrLn gitId              | _displayHelp opts           -> putStrLn usage-             | _targetFile opts == Nothing -> putStrLn usage-             | _validateAssignment opts    -> executeValidator opts-             | otherwise                   -> executeSolver opts+             | _targetFile opts == Left "" -> putStrLn usage+             | _validateAssignment opts    -> executeValidator opts =<< buildSolver opts+             | otherwise                   -> executeSolver opts =<< buildSolver opts 

@@ -1,11 +1,11 @@--- This file has been generated from package.yaml by hpack version 0.20.0.+-- This file has been generated from package.yaml by hpack version 0.28.2. -- -- see: https://github.com/sol/hpack ----- hash: 1a93fd2f2b1b1d0ba5e203ac6b48c5ca8abd31384c1955776cfb00969c311cbb+-- hash: 5cd432e14ff114a77b46f65cd54a00907c68da1bb380706bdbeb682bf43ff46d  name:           mios-version:        1.6.0+version:        1.6.2 synopsis:       A Minisat-based CDCL SAT solver in Haskell description:    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'. category:       Artificial Intelligence, Constraints@@ -18,7 +18,6 @@ license-file:   LICENSE build-type:     Simple cabal-version:  >= 1.10- extra-source-files:     app/sample.hs @@ -37,21 +36,6 @@   default: False  library-  hs-source-dirs:-      src-  default-extensions: Strict-  build-depends:-      base >=4.7 && <5-    , bytestring >=0.10-    , ghc-prim >=0.5-    , primitive >=0.6-    , vector >=0.12-  if flag(llvm)-    ghc-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -fwarn-missing-signatures-    ghc-prof-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -fprof-auto-  else-    ghc-options: -O2 -funbox-strict-fields -msse2 -fwarn-missing-signatures-    ghc-prof-options: -O2 -funbox-strict-fields -fprof-auto   exposed-modules:       SAT.Mios       SAT.Mios.Clause@@ -71,10 +55,27 @@       SAT.Mios.Vec   other-modules:       Paths_mios+  hs-source-dirs:+      src+  default-extensions: Strict+  build-depends:+      base >=4.7 && <5+    , bytestring >=0.10+    , ghc-prim >=0.5+    , primitive >=0.6+    , vector >=0.12+  if flag(llvm)+    ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -optlc-O3+    ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -fprof-auto+  else+    ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -msse2+    ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fprof-auto   default-language: Haskell2010  executable cnf-stat   main-is: cnf-stat.hs+  other-modules:+      Paths_mios   hs-source-dirs:       utils   default-extensions: Strict@@ -86,21 +87,22 @@     , primitive >=0.6     , vector >=0.12   if flag(llvm)-    ghc-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -fwarn-missing-signatures-    ghc-prof-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -fprof-auto+    ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -optlc-O3+    ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -fprof-auto   else-    ghc-options: -O2 -funbox-strict-fields -msse2 -fwarn-missing-signatures-    ghc-prof-options: -O2 -funbox-strict-fields -fprof-auto+    ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -msse2+    ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fprof-auto   if flag(utils)     buildable: True   else     buildable: False-  other-modules:-      Paths_mios   default-language: Haskell2010 -executable mios-1.6.0+executable mios162   main-is: mios.hs+  other-modules:+      DiscordSecret+      Paths_mios   hs-source-dirs:       app   default-extensions: Strict@@ -108,19 +110,46 @@       base >=4.7 && <5     , bytestring >=0.10     , ghc-prim >=0.5+    , gitrev     , mios     , primitive >=0.6     , vector >=0.12   if flag(llvm)-    ghc-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -fwarn-missing-signatures-    ghc-prof-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -fprof-auto+    ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -optlc-O3+    ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -fprof-auto   else-    ghc-options: -O2 -funbox-strict-fields -msse2 -fwarn-missing-signatures-    ghc-prof-options: -O2 -funbox-strict-fields -fprof-auto+    ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -msse2+    ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fprof-auto   if flag(llvm)-    ghc-prof-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -fprof-auto -rtsopts+    ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -optlc-O3 -rtsopts -with-rtsopts=-M7g+    ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -fprof-auto -rtsopts   else-    ghc-prof-options: -O2 -funbox-strict-fields -fprof-auto -rtsopts+    ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -msse2 -rtsopts -with-rtsopts=-M7g+    ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fprof-auto -rtsopts+  default-language: Haskell2010++test-suite mios-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs   other-modules:+      MiosSpec       Paths_mios+  hs-source-dirs:+      test+  default-extensions: Strict+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.7 && <5+    , bytestring >=0.10+    , ghc-prim >=0.5+    , hspec+    , mios+    , primitive >=0.6+    , vector >=0.12+  if flag(llvm)+    ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -optlc-O3+    ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fllvm -optlo-O3 -fprof-auto+  else+    ghc-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -msse2+    ghc-prof-options: -j -fwarn-missing-signatures -funbox-strict-fields -O2 -fprof-auto   default-language: Haskell2010

@@ -13,29 +13,29 @@          versionId        , CNFDescription (..)        , module SAT.Mios.OptionParser+        -- * Main Interace+       , SolverResult+       , Certificate (..)+       , buildOption+       , buildSolver+       , buildDescription+       , executeSolver+       , executeValidator+         -- * Simple Interface        , runSolver        , solveSAT        , solveSATWithConfiguration-       , solve-       , SolverResult-       , Certificate (..)+       , showAnswerFromString          -- * Assignment Validator-       , validateAssignment        , validate-         -- * For standalone programs-       , executeSolverOn-       , executeSolver-       , executeValidatorOn-       , executeValidator+       , validateAssignment          -- * File IO-       , parseCNF-       , injectClausesFromCNF        , dumpAssigmentAsCNF        )        where -import Control.Concurrent (forkIO, killThread, myThreadId, threadDelay-                          , newEmptyMVar, putMVar, readMVar)+import Control.Concurrent ( newEmptyMVar, putMVar, readMVar, takeMVar+                          , ThreadId, forkIO, killThread, myThreadId, threadDelay) import Control.Exception import Control.Monad ((<=<), unless, void, when) import Data.Char@@ -46,13 +46,14 @@ 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.6.0 -- https://github.com/shnarazk/mios"+versionId = "1.6.2 https://gitlab.com/satisfiability01/mios"  reportElapsedTime :: Bool -> String -> Integer -> IO Integer reportElapsedTime False _ 0 = return 0@@ -64,93 +65,139 @@   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 })+-- | returns a MiosProgramOption for the target+buildOption :: Either FilePath String -> MiosProgramOption+buildOption target = (miosDefaultOption { _targetFile = target }) +-- | returns a new solver injected a problem+buildSolver :: MiosProgramOption -> IO Solver+buildSolver opts = do+  token <- newEmptyMVar --  :: IO (MVar (Maybe Solver))+  (desc, cls) <- parseCNF (_targetFile opts)+  t0 <- reportElapsedTime False "" $ if _confVerbose opts || 0 <= _confBenchmark opts then -1 else 0+  readerId <- forkIO $ do+    s <- newSolver (toMiosConf opts) desc+    when (_numberOfVariables desc == 0) . error $ "couldn't load " ++ (take 100 . show . _targetFile) opts+    injectClausesFromCNF s desc cls+    putMVar token s+  when (0 < _confBenchmark opts) $+    void $ forkIO $ do let -- getCPUTime returns a pico sec. :: Integer, 1000 * 1000 * 1000 * 1000+                           -- threadDelay requires a micro sec. :: Int,  1000 * 1000+                           req = 1000000000000 * fromIntegral (_confBenchmark opts) :: Integer+                           waiting = do+                             elp <- getCPUTime+                             when (elp < req) $ do+                               threadDelay . max 1000000 $ fromIntegral (req - elp) `div` 1000000+                               waiting+                       waiting+                       killThread readerId+                       s' <- newSolver defaultConfiguration (CNFDescription 0 0 "")+                       set' (ok s') LiftedF+                       putMVar token s'+  void $ reportElapsedTime (_confVerbose opts) ("## [" ++ showPathFixed opts ++ "] Parse: ") t0+  takeMVar token++-- | returns the data on a given CNF file. Only solver knows it.+buildDescription :: FilePath -> Solver -> IO CNFDescription+buildDescription target s = CNFDescription (nVars s) <$> nClauses s <*> return target+ -- | 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))+executeSolver :: MiosProgramOption -> Solver -> IO ()+executeSolver opts s = do   solverId <- myThreadId+  token <- newEmptyMVar --  :: IO (MVar (Maybe Solver))+  t0 <- reportElapsedTime False "" $ if _confVerbose opts || 0 <= _confBenchmark opts then -1 else 0   handle (\case-             UserInterrupt -> putStrLn "User interrupt recieved."+             UserInterrupt -> if -1 == _confBenchmark opts+                              then putStrLn "User interrupt (SIGINT) recieved."+                              else reportResult opts t0 (Left TimeOut)              ThreadKilled  -> reportResult opts t0 =<< readMVar token-             e -> print e) $ do+             HeapOverflow  -> if -1 == _confBenchmark opts+                              then putStrLn "Abort: a too large problem or heap exhausted (use '+RTS -M16g' if you need)"+                              else reportResult opts t0 (Left OutOfMemory)+             e -> if -1 == _confBenchmark opts then print e else reportResult opts t0 (Left TimeOut)+         ) $ do     when (0 < _confBenchmark opts) $-      void $ forkIO $ do let fromMicro = 1000000 :: Int-                         threadDelay $ fromMicro * fromIntegral (_confBenchmark opts)+      void $ forkIO $ do let -- getCPUTime returns a pico sec. :: Integer, 1000 * 1000 * 1000 * 1000+                             -- threadDelay requires a micro sec. :: Int,  1000 * 1000+                             req = 1000000000000 * fromIntegral (_confBenchmark opts) :: Integer+                             waiting = do elp <- getCPUTime+                                          when (elp < req) $ do+                                            threadDelay . max 1000000 $ fromIntegral (req - elp) `div` 1000000+                                            waiting+                         waiting                          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+    when (0 < _confDumpStat opts) $ dumpStats 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.+-- TODO: this function shuld return @IO String@ in someday. 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))+reportResult opts t0 (Left OutOfMemory) = do+  t2 <- reportElapsedTime (_confVerbose opts) ("## [" ++ showPathFixed opts ++ "] Total: ") t0+  when (0 <= _confBenchmark opts) $ do+    let fromPico = 1000000000000 :: Double+    putStrLn ("\"" ++ takeWhile (' ' /=) versionId ++ "\","+              ++ show (_confBenchSeq opts) ++ ","+              ++ "\"" ++ showPath opts ++ "\","+              ++ show (_confBenchmark opts) ++ "," ++ show (fromEnum OutOfMemory)+             ) +reportResult opts t0 (Left TimeOut) = do+  t2 <- reportElapsedTime (_confVerbose opts) ("## [" ++ showPathFixed opts ++ "] Total: ") t0+  when (0 <= _confBenchmark opts) $ do+    let fromPico = 1000000000000 :: Double+    putStrLn ("\"" ++ takeWhile (' ' /=) versionId ++ "\","+              ++ show (_confBenchSeq opts) ++ ","+              ++ "\"" ++ showPath opts ++ "\","+              ++ showFFloat (Just 3) (fromIntegral t2 / fromPico) ","+              ++ show (fromEnum TimeOut)+             )+ -- solver terminated normally-reportResult opts@(_targetFile -> Just cnfFile) t0 (Right result) = do-  t2 <- reportElapsedTime (_confVerbose opts) ("## [" ++ showPath cnfFile ++ "] Total: ") t0-  case result of+reportResult opts t0 (Right result) = do+  t2 <- reportElapsedTime (_confVerbose opts) ("## [" ++ showPathFixed opts ++ "] Total: ") t0+  dumpName <- if _confNoAnswer opts then return Nothing else (Just <$> dumpAssigmentAsCNF opts result)+  case (result, dumpName) 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+    (_, Just "")    -> return ()+    (SAT _, Just o)    -> hPutStrLn stderr $ "SATISFIABLE, saved to " ++ o ++ " for " ++ showPathBaseName opts+    (SAT _, Nothing)   -> hPutStrLn stderr $ "SATISFIABLE, " ++ showPathBaseName opts+    (UNSAT _, Just o)  -> hPutStrLn stderr $ "UNSATISFIABLE, saved to " ++ o ++ " for " ++ showPathBaseName opts+    (UNSAT _, Nothing) -> hPutStrLn stderr $ "UNSATISFIABLE, " ++ showPathBaseName opts+  valid <- if _confCheckAnswer opts                     -- or 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+                  SAT asg -> flip validate asg =<< buildSolver opts                   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+    void $ reportElapsedTime (_confVerbose opts) ("## [" ++ showPathFixed opts ++ "] 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)+    putStrLn ("\"" ++ takeWhile (' ' /=) versionId ++ "\","+              ++ show (_confBenchSeq opts) ++ ","+              ++ "\"" ++ showPath opts ++ "\","+              ++ if valid+               then showFFloat (Just 3) (fromIntegral t2 / fromPico) "," ++ show phase+               else show (_confBenchmark opts) ++ "," ++ show (fromEnum InternalInconsistent))  reportResult _ _ _ = return () --- | new top-level interface that returns:+-- | NOT MAINTAINED NOW+-- new top-level interface that returns: -- -- * conflicting literal set :: Left [Int] -- * satisfiable assignment :: Right [Int]@@ -181,7 +228,6 @@ 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@@ -191,21 +237,10 @@               _             -> 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)+executeValidator :: MiosProgramOption -> Solver -> IO ()+executeValidator opts@(_targetFile -> target@(Left cnfFile)) s = do   asg <- read <$> getContents   unless (_confNoAnswer opts) $ print asg   result <- s `validate` (asg :: [Int])@@ -213,7 +248,7 @@     then putStrLn ("It's a valid assignment for " ++ cnfFile ++ ".") >> exitSuccess     else putStrLn ("It's an invalid assignment for " ++ cnfFile ++ ".") >> exitFailure -executeValidator _  = return ()+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@,@@ -233,103 +268,153 @@ -- -- >>> do y <- solve s ... ; dumpAssigmentAsCNF (Just "result.cnf") y <$> model s ---dumpAssigmentAsCNF :: Maybe FilePath -> Certificate -> IO ()-dumpAssigmentAsCNF Nothing _ = return ()+dumpAssigmentAsCNF :: MiosProgramOption -> Certificate -> IO String -- | 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+dumpAssigmentAsCNF opt (UNSAT _) = do+  if _outputFile opt == Just "--"+    then print "[]" >> return ""+    else do let fname = case _outputFile opt of+                  Just x -> x+                  Nothing -> case _targetFile opt of+                               Left f -> ".ans_" ++ (reverse . takeWhile (/= '/') . reverse) f+                               Right _ -> ".ans_mios"+            writeFile fname "s UNSAT\n0\n"+            return fname+dumpAssigmentAsCNF opt (SAT l) = do+  if _outputFile opt == Just "--"+    then print l >> return ""+    else do let fname = case _outputFile opt of+                  Just x -> x+                  Nothing -> case _targetFile opt of+                               Left f -> ".ans_" ++ (reverse . takeWhile (/= '/') . reverse) f+                               Right _ -> ".ans_mios"+            withFile fname WriteMode $ \h -> do+              hPutStrLn h "s SAT"+              hPutStrLn h . (++ " 0") . unwords $ map show l+            return fname +showPath :: MiosProgramOption -> String+showPath (_targetFile -> Left str) = str+showPath _ = "{a cnf embedded}"++showPathBaseName :: MiosProgramOption -> String+showPathBaseName (_targetFile -> Left str) = (reverse . takeWhile (/= '/') . reverse) str+showPathBaseName _ = "aCNF"++showPathFixed :: MiosProgramOption -> String+showPathFixed (_targetFile -> Left str) = replicate (len - length basename) ' ' ++ if elem '/' str then basename else basename'+  where+    len = 50+    basename = reverse . takeWhile (/= '/') . reverse $ str+    basename' = take len str++showPathFixed (_targetFile -> Right _) = replicate (len - length basename) ' ' ++ basename+  where+    len = 50+    basename = "embedded data"+ -------------------------------------------------------------------------------- -- DIMACS CNF Reader --------------------------------------------------------------------------------  -- | parses the header of a CNF file-parseCNF :: Maybe FilePath -> IO (CNFDescription, B.ByteString)-parseCNF target@(Just cnfFile) = do+parseCNF :: Either FilePath String -> IO (CNFDescription, B.ByteString)+parseCNF pathOrData = do   let -- format: p cnf n m, length "p cnf" == 5+      target = case pathOrData of+                 Left str -> str+                 Right _  -> ""       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+      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+  case pathOrData of+    Left cnfFile -> seek =<< B.readFile cnfFile+    Right bdata  -> seek $ B.pack bdata  -- | parses ByteString then injects the clauses in it into a solver+{-# INLINABLE injectClausesFromCNF #-} injectClausesFromCNF :: Solver -> CNFDescription -> B.ByteString -> IO () injectClausesFromCNF s (CNFDescription nv nc _) bs = do   let maxLit = int2lit $ negate nv-  buffer <- newVec (maxLit + 1) 0-  polvec <- newVec (maxLit + 1) 0-  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+  buffer <- newVec (maxLit + 1) 0 :: IO (Vec Int)+  let skipComments :: B.ByteString -> B.ByteString+      skipComments !s = case B.uncons s of -- __Pre-condition:__ we are on the benngining of a line+                          Just ('c', b') -> skipComments . B.tail . B.dropWhile (/= '\n') $ b'+                          _ -> s+      readClause :: Int -> B.ByteString -> IO ()+      readClause ((< nc) -> False) _ = return ()+      readClause !i !stream = do+        let loop :: Int -> B.ByteString -> IO ()+            loop !j !b = case parseInt $ skipWhitespace b of+                           (k, b') -> if k == 0+                                      then do setNth buffer 0 $ j - 1+                                              res <- addClause s buffer+                                              unless res $ set' (ok s) LiftedF+                                              readClause (i + 1) b'+                                      else do setNth buffer j (int2lit k)+                                              loop (j + 1) b'+        loop 1 . skipComments . B.dropWhile (`elem` " \t\n") $ stream+  readClause 0 bs  {-# 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+skipWhitespace !s = B.dropWhile (== ' ') {- (`elem` " \t") -} s -{-# INLINABLE parseInt #-}+{-# INLINE parseInt #-} parseInt :: B.ByteString -> (Int, B.ByteString) parseInt !st = do   let !zero = ord '0'-      loop :: B.ByteString -> Int -> (Int, B.ByteString)-      loop !s !val = case B.head s of-        c | '0' <= c && c <= '9'  -> loop (B.tail s) (val * 10 + ord c - zero)-        _ -> (val, B.tail s)-  case B.head st of-    '-' -> let (k, x) = loop (B.tail st) 0 in (negate k, x)-    '0' -> (0, B.tail st)---    '+' -> loop st (0 :: Int)-    _   -> loop st 0---    c | '0' <= c && c <= '9'  -> loop st 0---    _ -> error "PARSE ERROR! Unexpected char"+      loop :: (Int, B.ByteString) -> (Int, B.ByteString)+      loop (val, s) = case B.uncons s of+        Just (c, s') -> if '0' <= c && c <= '9' then loop (val * 10 + ord c - zero, s') else (val, s')+        -- _ -> error (">>>>" ++ take 80 (B.unpack s))+  case B.uncons st of+    Just ('-', st') -> let (k, x) = loop (0, st') in (negate k, x)+    Just ('0', st') -> (0, st')+    _ -> loop (0, st) -{-# 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+-- | executes a solver on the given 'arg :: MiosConfiguration'.+-- This is another entry point for standalone programs.+showAnswerFromString :: String -> IO String+showAnswerFromString str = do+  let opts = miosDefaultOption { _targetFile = Right str }+  solverId <- myThreadId+  desc <- fst <$> parseCNF (_targetFile opts)+  token <- newEmptyMVar --  :: IO (MVar (Maybe Solver))+  t0 <- reportElapsedTime False "" 0+  s <- buildSolver opts+  handle (\case+             UserInterrupt -> return "User interrupt recieved."+             ThreadKilled  -> makeReport opts t0 =<< readMVar token+             HeapOverflow  -> if -1 == _confBenchmark opts+                              then return "Abort: a too large problem or heap exhausted"+                              else makeReport opts t0 (Left OutOfMemory)+             e -> if -1 == _confBenchmark opts then return "unhandled iterrupt" else makeReport opts t0 (Left TimeOut)+         ) $ do+    when (0 < _confBenchmark opts) $+      void $ forkIO $ do let req = 1000000000000 * fromIntegral (_confBenchmark opts) :: Integer+                             waiting = do elp <- getCPUTime+                                          when (elp < req) $ do+                                            threadDelay $ fromIntegral (req - elp) `div` 1000000+                                            waiting+                         waiting+                         putMVar token (Left TimeOut)+                         killThread solverId+    result <- solve s []+    putMVar token result+    killThread solverId+    return $ show desc++makeReport :: MiosProgramOption -> Integer -> SolverResult -> IO String+makeReport opts t0 (Left OutOfMemory) = return "out of memory"+makeReport opts t0 (Left TimeOut) = return "time out"+makeReport opts t0 (Right (SAT asg)) = return $ show asg+makeReport opts t0 (Right (UNSAT _)) = return "UNSAT"+makeReport _ _ _ = return ""

@@ -13,6 +13,10 @@        (          Clause (..)        , newClauseFromStack+       , getRank+       , setRank+       -- , getActivity+       -- , setActivity          -- * Vector of Clause        , ClauseVector        , newClauseVector@@ -30,10 +34,10 @@ -- This matches both of @Clause@ and @GClause@ in MiniSat. data Clause = Clause               {-                rank       :: !Int'     -- ^ goodness like LBD; computed in 'Ranking'+                lits       :: !Stack    -- ^ literals and rank+              , rank       :: !Int'     -- ^ another metrics of this clause               , activity   :: !Double'  -- ^ activity of this clause---              , protected  :: !Bool'    -- ^ protected from reduce-              , lits       :: !Stack    -- ^ which this clause consists of+--            , protected  :: !Bool'    -- ^ protected from reduce               }   | NullClause                              -- as null pointer --  | BinaryClause Lit                        -- binary clause consists of only a propagating literal@@ -93,12 +97,31 @@ 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)+  v <- newStack (n + 1)+  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 v <$> new' (if l then 1 else 0) <*> new' 0.0++-- | returns the rank, a goodness, of a given clause+{-# INLINE getRank #-}+getRank :: Clause -> IO Int+getRank Clause{..} = get' rank++-- | sets the rank of a given clause+{-# INLINE setRank #-}+setRank :: Clause -> Int -> IO ()+setRank Clause{..} k = set' rank k++{-+{-# INLINE getActivity #-}+getActivity :: Clause -> IO Int+getActivity Clause{..} = do n <- get' lits; getNth lits (n + 2)++{-# INLINE setActivity #-}+setActivity :: Clause -> Int -> IO ()+setActivity Clause{..} k = do n <- get' lits; setNth lits (n + 2) k+-}  -------------------------------------------------------------------------------- Clause Vector 

@@ -20,6 +20,7 @@        , pushClauseWithKey        , getKeyVector        , markClause+--       , allocateKeyVectorSize          -- * WatcherList        , WatcherList        , newWatcherList@@ -29,6 +30,7 @@  import Control.Monad (unless, when) import qualified Data.IORef as IORef+import qualified Data.Primitive.ByteArray as BA import qualified Data.Vector as V import qualified Data.Vector.Mutable as MV import SAT.Mios.Types@@ -99,7 +101,7 @@     _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+  , _keyVector    :: IORef.IORef (Vec Int)         -- Int list   }  -- | 'ClauseExtManager' is a 'SingleStorage` on the number of clauses in it.@@ -120,7 +122,7 @@     !b <- IORef.readIORef _keyVector     if MV.length v - 1 <= n       then do-          let len = max 8 $ MV.length v+          let len = max 8 $ div (MV.length v) 2           v' <- MV.unsafeGrow v len           b' <- growBy b len           MV.unsafeWrite v' n c@@ -228,7 +230,7 @@  -- | returns the associated Int vector, which holds /blocking literals/. {-# INLINE getKeyVector #-}-getKeyVector :: ClauseExtManager -> IO (Vec [Int])+getKeyVector :: ClauseExtManager -> IO (Vec Int) getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector  -- | O(1) inserter@@ -241,7 +243,7 @@   !b <- IORef.readIORef _keyVector   if MV.length v - 1 <= n     then do-        let len = max 8 $ MV.length v+        let len = max 8 $ div (MV.length v) 2         v' <- MV.unsafeGrow v len         b' <- growBy b len         MV.unsafeWrite v' n c@@ -277,7 +279,10 @@ -- | 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)+newWatcherList n m = do let n' = int2lit (negate n) + 2+                        v <- MV.unsafeNew n'+                        mapM_  (\i -> MV.unsafeWrite v i =<< newManager m) [0 .. n' - 1]+                        V.unsafeFreeze v  -- | returns the watcher List for "Literal" /l/. {-# INLINE getNthWatcher #-}@@ -291,3 +296,20 @@   {-# 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]++--------------------------------------------------------------------------------++-- | returns the associated Int vector, which holds /blocking literals/.+{-# INLINE setKeyVector #-}+setKeyVector :: ClauseExtManager -> Vec Int -> IO ()+setKeyVector ClauseExtManager{..} v = IORef.writeIORef _keyVector v++{-# INLINABLE allocateKeyVectorSize #-}+allocateKeyVectorSize :: ClauseExtManager -> Int -> IO (Vec Int)+allocateKeyVectorSize  ClauseExtManager{..} n' = do+  v <- IORef.readIORef _keyVector+  if realLength v < n'          -- never shrink it+    then do v' <- newVec n' 0+            IORef.writeIORef _keyVector v'+            return v'+    else return v

@@ -47,29 +47,23 @@         let mgr = getManager pool i         nn <- get' mgr         if 0 < nn-          then do c <- lastOf mgr-                  popFrom mgr-                  return c+          then do c <- lastOf mgr; popFrom mgr; return c           else pickup $ i + 1   n <- get' v-  c <- pickup (n - 2)+  c <- pickup (n - 2)           -- mapping the number of literals for the smallest clauses to zero   if c == NullClause     then newClauseFromStack True v     else do let lstack = lits c                 loop :: Int -> IO ()-                loop ((<= n) -> False) = return ()+                loop ((<= n) -> False) = set' (activity c) 0.0 -- setActivity c 1                 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+            return c    -- the caller (newLearntClause) should set rank and protected by himself  -- | 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+  n <- subtract 2 <$> get' c    -- the number of literals in a clause >= 2+  l <- getRank c+  when (0 /= l && n <= storeLimit) $ pushTo (getManager pool n) c

@@ -1,7 +1,8 @@ -- | (This is a part of MIOS.) -- Advanced heuristics library for 'SAT.Mios.Main' {-# LANGUAGE-    MultiWayIf+    BangPatterns+  , MultiWayIf   , RecordWildCards   , ViewPatterns   #-}@@ -16,14 +17,21 @@        , varDecayActivity          -- * Clause        , addClause-         -- * Literal Block Distance+         -- * Clause Metrics        , lbdOf+       , updateNDD+       , nddOf          -- * Restart        , checkRestartCondition+         -- * Reporting+       , dumpStats        )         where -import Control.Monad (when)+import Control.Monad (void, when)+import Data.Bits+import Data.List (intercalate)+import Numeric (showFFloat) import SAT.Mios.Types import SAT.Mios.Clause import SAT.Mios.ClauseManager@@ -37,16 +45,18 @@ -- | __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+varBumpActivity s@Solver{..} v = do+  x <- getNth activities v+  y <- fromIntegral <$> getStat s NumOfBackjump+  let a = (x + y) / 2+  setNth activities v a   when (varActivityThreshold < a) $ varRescaleActivity s-  update s x                    -- update the position in heap+  updateVO s v                    -- update the position in heap  -- | __Fig. 14 (p.19)__ {-# INLINABLE varDecayActivity #-} varDecayActivity :: Solver -> IO ()-varDecayActivity Solver{..} = modify' varInc (/ variableDecayRate config)+varDecayActivity Solver{..} = return () -- modify' varInc (/ variableDecayRate config)  -- | __Fig. 14 (p.19)__ {-# INLINABLE varRescaleActivity #-}@@ -129,104 +139,44 @@ -- * @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+clauseNew :: Solver -> Stack -> IO (Either Bool Clause)+clauseNew s@Solver{..} ps = do+  n <- get' ps+  sortStack ps+  let loop :: Int -> Int -> Lit -> IO Bool+      loop ((<= n) -> False) j _ = setNth ps 0 (j - 1) >> return False+      loop !i !j !l' = do l <- getNth ps i -- check the i-th literal's satisfiability+                          sat <- valueLit s l+                          if | sat == LiftedT || negateLit l == l' -> reset ps >> return True+                             | sat /= LiftedF && l /= l' -> setNth ps j l >> loop (i + 1) (j + 1) l+                             | otherwise -> loop (i + 1) j l'+  exit <- loop 1 1 LBottom   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)+   1 -> do l <- getNth ps 1+           Left <$> enqueue s l NullClause+   _ -> do c <- newClauseFromStack False ps+           let lstack = lits c+           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.+-- This function is called only before the solving phase to register the given clauses (not learnt). {-# INLINABLE addClause #-} addClause :: Solver -> Stack -> IO Bool addClause s@Solver{..} vecLits = do-  result <- clauseNew s vecLits False+  result <- clauseNew s vecLits   case result of-   Left b  -> return b   -- No new clause was returned becaues a confilct occured or the clause is a literal+   Left b  -> return b -- No clause is returned becaues a confilct occured or the clause is a literal    Right c -> pushTo clauses c >> return True --------------------------------------------------------------------------------- LBD+-------------------------------------------------------------------------------- Clause Metrics --- | returns a POSIVITE value+-- | returns a POSIVITE value of Literal Block Distance {-# INLINABLE lbdOf #-} lbdOf :: Solver -> Stack -> IO Int lbdOf Solver{..} vec = do@@ -262,66 +212,138 @@     _ -> return () -} --------------------------------------------------------------------------------- restart+-- | returns a vector index of NDD for the nth bit of a var+{-# INLINE varBit2vIndex #-}+varBit2vIndex :: Int -> Int -> Int+varBit2vIndex v ((`mod` 124) -> b)+  | 62 <= b   = 2 * v + 1+  | otherwise = 2 * v -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 |+-- | returns a bit index of NDD for the nth bit of a var+{-# INLINE varBit2bIndex #-}+varBit2bIndex :: Int -> Int -> Int+varBit2bIndex v b = mod b 62 -ema0 :: Int-ema0 = 2 ^ (14 :: Int)          -- = floor $ 1 / ema2+-- | updates a /var/'s ndl, which is assigned by a 'reason' /clause/+{-# INLINE updateNddOf #-}+updateNddOf :: Solver -> Var -> Clause -> IO ()+updateNddOf Solver{..} v NullClause = do+  l <- getNth level v+  setNth ndd (varBit2vIndex v l) $ if l == 0 then 0 else setBit 0 (varBit2bIndex v l) --- | #62-checkRestartCondition :: Solver -> Int -> IO Bool-checkRestartCondition s@Solver{..} (fromIntegral -> lbd) = do-  k <- getStat s NumOfRestart-  let step = 100+updateNddOf Solver{..} v Clause{..} = do+  n <- get' lits+  let iv = varBit2vIndex v 0+  setNth ndd iv 0+  setNth ndd (iv + 1) 0+  let loop :: Int -> Int -> Int -> IO ()+      loop ((<= n) -> False) low high = do setNth ndd iv low+                                           setNth ndd (iv + 1) high+      loop i low high = do v' <- lit2var <$> getNth lits i+                           let jv = varBit2vIndex v' 0+                           low' <- (low .|.) <$> getNth ndd jv+                           high' <- (high .|.) <$> getNth ndd (jv + 1)+                           loop (i + 1) low' high'+  loop 1 0 0++-- | updates all assigned vars' ndl+{-# INLINABLE updateNDD #-}+updateNDD :: Solver -> IO ()+updateNDD s@Solver{..} = do+  n <- get' trail+  let -- thr = if ns == 0 then 0 else floor . logBase 2 $ lv / ns :: Int+      update :: Int -> IO ()+      update ((<= n) -> False) = return ()+      update i = do v <- lit2var <$> getNth trail i+                    updateNddOf s v =<< getNth reason v+                    update (i + 1)+  update 1++-- | returns the NDL+{-# INLINABLE nddOf #-}+nddOf :: Solver -> Stack -> IO Int+nddOf Solver{..} stack = do+  n <- get' stack+  let loop :: Int -> Int -> Int -> IO Int -- var -> #lowbits -> #highbits+      loop ((<= n) -> False) low high = return $ popCount low + popCount high+      loop i low high = do v <- lit2var <$> getNth stack i+                           let iv = varBit2vIndex v 0+                           l <- getNth ndd iv+                           h <- getNth ndd (iv + 1)+                           loop (i + 1) (low .|. l) (high .|. h)+  max 1 <$> loop 1 0 0++-------------------------------------------------------------------------------- restart++-- | #62, #74, #91+checkRestartCondition :: Solver -> Int -> Int -> IO Bool+checkRestartCondition s@Solver{..} (fromIntegral -> lbd) (fromIntegral -> cLv) = do   next <- get' nextRestart-  count <- getStat s NumOfBackjump+  count <- getStat s NumOfBackjump -- it should be > 0   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+  bLv <- fromIntegral <$> decisionLevel s+  df  <- updateEMA emaDFast lbd+  ds  <- updateEMA emaDSlow lbd+  af  <- updateEMA emaAFast nas+  as  <- updateEMA emaASlow nas+  void $ updateEMA emaCDLvl cLv+  nb <- getStat s NumOfBlockRestart+  nf <- getStat s NumOfRestart+  let bias = if | nb <= 10  -> 0+                | nb <= nf  -> 0.1 * (fromIntegral nf / fromIntegral nb) ** 2+                | otherwise -> 0.1 * negate ((fromIntegral nb / fromIntegral nf) ** 2)+      block = 1.25 * as < af+      force = (1.25 + bias) * ds < df+      updateParams ki = do+        gef <- (max 0) . (+ ki) <$> get' restartExp+        set' nextRestart $ count + 100 + ceiling (50 * gef)+        set' restartExp gef+      updateBDL = updateEMA emaBDLvl bLv >> return False+      restartBDL = do+        updateEMA emaBDLvl 0+        -- do z <- get' restartExp; when (0.4 < z) $ print (nb, nf, bias, z)+        when (3 == dumpSolverStatMode config) $ dumpStats DumpCSV s+        return True+  if | count < next -> updateBDL+     | block        -> 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+         updateParams 1.0   >> updateBDL+     | force        -> do          incrementStat s NumOfRestart 1-         set' nextRestart (count + step)-         when (3 == dumpStat config) $ dumpSolver DumpCSV s-         return True-     | otherwise      -> return False+         updateParams (-0.1) >> restartBDL+     | otherwise    -> do+         updateParams (-0.9) >> updateBDL -{--{-# 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)--}+-------------------------------------------------------------------------------- dump++emaLabels :: [(String, Solver -> EMA)]+emaLabels = [ ("emaAFast", emaAFast)+            , ("emaASlow", emaASlow)+            , ("emaBDLvl", emaBDLvl)+            , ("emaCDLvl", emaCDLvl)+            , ("emaDFast", emaDFast)+            , ("emaDSlow", emaDSlow)+            ]++{-# INLINABLE dumpStats #-}+-- | print statatistic data to stdio. This should be called after each restart.+dumpStats :: DumpMode -> Solver -> IO ()+dumpStats NoDump _ = return ()+dumpStats DumpCSVHeader s@Solver{..} = do+  sts <- init <$> getStats s+  putStrLn . intercalate "," $ map (show . fst) sts ++ map fst emaLabels+dumpStats DumpCSV s@Solver{..} = do+  -- update the stat data before dump+  va <- get' trailLim+  setStat s NumOfVariable . (nVars -) =<< if va == 0 then get' trail else getNth trailLim 1+  setStat s NumOfAssigned =<< nAssigns s+  setStat s NumOfClause =<< get' clauses+  setStat s NumOfLearnt =<< get' learnts+  sts <- init <$> getStats s+  let fs :: (Solver -> EMA) -> IO String+      fs e = do x <- getEMA (e s)+                return $ showFFloat (Just 3) x ""+  vals <- mapM (fs . snd) emaLabels+  putStrLn . intercalate "," $ map (show . snd) sts ++ vals+-- | FIXME: use Util/Stat+dumpStats DumpJSON _ = return ()                -- mode 2: JSON

@@ -16,7 +16,7 @@        , newSolver        , setAssign        , addClause-       , dumpSolver+       , dumpStats          -- * Main function        , simplifyDB        , solve@@ -64,14 +64,13 @@            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+               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 -- get the index of the literal with highest level            -- Bump, enqueue, store clause:            claBumpActivity s c            -- Add clause to all managers@@ -84,7 +83,7 @@            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+           setRank c lbd            -- assert (0 < rank c)            -- set' (protected c) True            return lbd@@ -142,7 +141,7 @@   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)+        d <- getRank c         when (0 /= d) $ claBumpActivity s c         -- update LBD like #Glucose4.0         when (2 < d) $ do@@ -150,7 +149,7 @@           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+            setRank c nblevels     --  Update it         sc <- get' c         let lstack = lits c             loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int)@@ -169,7 +168,7 @@                           -- UPDATEVARACTIVITY: glucose heuristics                           r <- getNth reason v                           when (r /= NullClause) $ do-                            ra <- get' (rank r)+                            ra <- getRank r                             when (0 /= ra) $ pushTo an'lastDL q                           -- end of glucose heuristics                           loopOnLiterals (j + 1) b (pc + 1)@@ -198,7 +197,7 @@       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+                      -- restrict the search depth (range) to [0 .. 63]                       merger (i + 1) . setBit b . (63 .&.) =<< getNth level (lit2var l)   levels <- merger 2 0   let loopOnLits :: Int -> Int -> IO ()@@ -439,6 +438,7 @@ reduceDB s@Solver{..} = do   n <- nLearnts s   cvec <- getClauseVector learnts+  n' <- get' trail   let loop :: Int -> IO ()       loop ((< n) -> False) = return ()       loop i = do@@ -464,17 +464,13 @@  -- constants for sort key layout rankWidth :: Int-rankWidth = 10+rankWidth = 11 activityWidth :: Int-activityWidth = 50              -- note: the maximum clause activity is 1e20.-indexWidth :: Int-indexWidth = 32                 -- 4G+activityWidth = 51              -- note: the maximum clause activity is 1e20. 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.@@ -483,23 +479,23 @@ -- 2. smaller LBD -- 3. larger activity defined as MiniSat ----- they are encoded into two "Int64"s as the following (10+52+32 layout):+-- They are encoded into an "Int64" as the following (11+51 layout): ----- * 10 bits for rank (LBD): 'rankWidth'--- * 50 bits for converted activity: 'activityWidth'--- * 32 bits for clauseVector index: 'indexWidth'+-- * 11 bits for rank (LBD): 'rankWidth'+-- * 51 bits for converted activity: 'activityWidth' -- 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)+  kvec <- getKeyVector cm   at <- (0.1 *) . (/ fromIntegral n) <$> get' (claInc s) -- activity threshold   -- 1: assign keys+  updateNDD s+  cl <- getEMA (emaCDLvl s)+  surface <- if cl == 0 then return 0 else (/ cl) <$> getEMA (emaBDLvl s)  -- 0 <=backjumped level / coflict level < 1.0   let shiftLBD = activityWidth-      shiftIndex = shiftL 1 indexWidth       am = fromIntegral activityMax :: Double       scaleAct :: Double -> Int       scaleAct x@@ -508,78 +504,60 @@       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+          then do setNth kvec i 0                   assignKey (i + 1) (t + 1)-          else do a <- get' (activity c)               -- Second one... based on LBD-                  r <- get' (rank c)+          else do a <- get' (activity c)                       -- Second one... based on LBD+                  rLBD <- fromIntegral <$> getRank c           -- above the level+                  rNDD <- fromIntegral <$> nddOf s (lits c)    -- under the level+                  let r = if rNDD == 1                         -- this implies rLBD == 1.+                          then 1+                          else ceiling $ rLBD ** surface * rNDD ** (1 - surface)                   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+                  setNth kvec 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 ()+  let sortOnRange :: Int -> Int -> IO ()       sortOnRange left right-        | limit2 < left = return ()+        | limit < 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)+        | left + 1 == right = do+            a <- getNth kvec left+            b <- getNth kvec right+            unless (a < b) $ do setNth kvec left b+                                setNth kvec right a+                                swapBetween vec left right         | 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 p = div (left + right) 2+            pivot <- getNth kvec p+            swapBetween kvec p left -- set a sentinel for r'+            swapBetween vec p left             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+                nextL i = do v <- getNth kvec 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 - 2) else return i+                nextR i = do v <- getNth kvec 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 do swapBetween keys l' r'-                            swapBetween keys (l' + 1) (r' + 1)-                            divide (l' + 2) (r' - 2)+                    then do swapBetween kvec l' r'+                            swapBetween vec l' r'+                            divide (l' + 1) (r' - 1)                     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+            m <- divide (left + 1) right+            swapBetween kvec left m+            swapBetween vec left m+            sortOnRange left (m - 1)+            sortOnRange (m + 1) right+  sortOnRange 0 (n - 1)   return limit  -- | #M22@@ -637,6 +615,7 @@ search :: Solver -> IO Bool search s@Solver{..} = do   -- clear model+  let delta = (sqrt . fromIntegral) nVars   let loop :: Bool -> IO Bool       loop restart = do         confl <- propagate s@@ -662,16 +641,15 @@                               t' <- (* 1.5) <$> get' learntSAdj                               set' learntSAdj t'                               set' learntSCnt $ floor t'-                              -- modify' maxLearnts (* 1.1)-                              modify' maxLearnts (+ 300)-                            loop =<< checkRestartCondition s lbd'+                              modify' maxLearnts (+ delta)+                            loop =<< checkRestartCondition s lbd' d           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+                    when (2 == dumpSolverStatMode config) $ dumpStats DumpCSV s                   if | k2 == nVars -> return True     -- Model found                      | restart -> do                  -- Reached bound on number of conflicts                          (s `cancelUntil`) =<< get' rootLevel -- force a restart@@ -690,7 +668,7 @@ -}                          loop False                      | otherwise -> do                -- New variable decision-                         v <- select s+                         v <- selectVO s                          -- #phasesaving <<<<  many have heuristic for polarity here                          oldVal <- getNth phases v                          unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@@@ -723,8 +701,9 @@                             cancelUntil s 0                             return False                     else return True+  check_given <- get' ok   good <- simplifyDB s-  x <- if good then foldrM inject True assumps else return False+  x <- if check_given /= LiftedF && good then foldrM inject True assumps else return False   if x     then do set' rootLevel =<< decisionLevel s             status <- search s@@ -733,7 +712,7 @@                 toInt v = (\p -> if LiftedT == p then v else negate v) <$> valueVar s v             asg1 <- mapM toInt [1 .. nVars]             asg2 <- map lit2int <$> asList conflicts-            when (0 < dumpStat config) $ dumpSolver DumpCSV s+            when (0 < dumpSolverStatMode config) $ dumpStats DumpCSV s             cancelUntil s 0     -- reset solver             flag <- get' ok             if | status && flag == LiftedT     -> return $ Right (SAT asg1)

@@ -23,41 +23,43 @@ -- | configuration swithces data MiosProgramOption = MiosProgramOption                      {-                       _targetFile :: Maybe String-                     , _targets :: [String]-                     , _outputFile :: Maybe String-                     , _confVariableDecayRate :: !Double-                     , _confClauseDecayRate :: Double+                       _targetFile            :: Either String String -- path or data+                     , _targets               :: [String]+                     , _outputFile            :: Maybe String+                     , _confVariableDecayRate :: Double+                     , _confClauseDecayRate   :: Double+                     , _confRestartE          :: Double+                     , _confRestartS          :: Double --                     , _confRandomDecisionRate :: Int-                     , _confMaxSize :: !Int-                     , _confCheckAnswer :: !Bool-                     , _confVerbose :: !Bool-                     , _confBenchmark :: Integer-                     , _confBenchSeq :: !Int-                     , _confNoAnswer :: !Bool-                     , _confDumpStat :: !Int-                     , _validateAssignment :: !Bool-                     , _displayHelp :: !Bool-                     , _displayVersion :: !Bool+                     , _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+    _targetFile = Left ""   , _targets = []   , _outputFile = Nothing   , _confVariableDecayRate = variableDecayRate defaultConfiguration   , _confClauseDecayRate = clauseDecayRate defaultConfiguration---  , _confRandomDecisionRate = randomDecisionRate defaultConfiguration-  , _confMaxSize = 4000000    -- 4,000,000 = 4M+  , _confRestartE = restartExpansion defaultConfiguration+  , _confRestartS = restartStep defaultConfiguration+  --, _confRandomDecisionRate = randomDecisionRate defaultConfiguration   , _confCheckAnswer = False   , _confVerbose = False   , _confBenchmark = -1   , _confBenchSeq = 0   , _confNoAnswer = False-  , _confDumpStat = dumpStat defaultConfiguration+  , _confDumpStat = dumpSolverStatMode defaultConfiguration   , _validateAssignment = False   , _displayHelp = False   , _displayVersion = False@@ -73,12 +75,15 @@   , 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 [] ["Re"]+    (ReqArg (\v c -> c { _confRestartE = read v }) (show (_confRestartE miosDefaultOption)))+    "[solver] expansion rate for blocking/forcing restart (>= 1.0)"+  , Option [] ["Rs"]+    (ReqArg (\v c -> c { _confRestartS = read v }) (show (_confRestartS miosDefaultOption)))+    "[solver] a fixed number of conflicts between restarts" --  , 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"@@ -87,7 +92,7 @@     "[solver] self-check (satisfiable) assignment"   , Option ['o'] ["output"]     (ReqArg (\v c -> c { _outputFile = Just v }) "file")-    "[option] filename to store result"+    "[option] filename to store result, '--' for stdout" {-   , Option [] ["stdin"]     (NoArg (\c -> c { _targetFile = Nothing }))@@ -106,7 +111,7 @@     (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)))+    (ReqArg (\v c -> c { _confDumpStat = read v }) (show (dumpSolverStatMode defaultConfiguration)))     "[devel] dump level; 1:solved, 2:reduction, 3:restart"   , Option ['h'] ["help"]     (NoArg (\c -> c { _displayHelp = True }))@@ -127,7 +132,7 @@       (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 }+        return $ conf { _targetFile = Left (head l), _targets = l }       (_, _, errs) -> ioError (userError (concat errs ++ miosUsage mes))  -- | builds "MiosProgramOption" from a String@@ -141,5 +146,8 @@                    variableDecayRate = _confVariableDecayRate opts                  , clauseDecayRate = _confClauseDecayRate opts --                 , randomDecisionRate = _confRandomDecisionRate opts-                 , dumpStat = _confDumpStat opts+                 , dumpSolverStatMode = _confDumpStat opts+                 , emaCoeffs = emaCoeffs defaultConfiguration+                 , restartExpansion = _confRestartE opts+                 , restartStep      = _confRestartS opts                  }

@@ -33,7 +33,6 @@        , setStat        , incrementStat        , getStats-       , dumpSolver        )         where @@ -60,6 +59,7 @@               , 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+              , ndd        :: !(Vec Int)         -- ^ For each variable, the number of depending decisions               , conflicts  :: !Stack             -- ^ Set of literals in the case of conflicts                 -------- Variable Order               , activities :: !(Vec Double)      -- ^ Heuristic measurement of the activity of a variable@@ -82,16 +82,19 @@               , 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+              , 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+                -------- restart heuristics #62, clause evaluation criteria #74+              , emaAFast    :: !EMA              -- ^ Number of Assignments Fast+              , emaASlow    :: !EMA              -- ^ Number of Assignments Slow+              , emaBDLvl    :: !EMA              -- ^ Backjumped and Restart Dicision Level+              , emaCDLvl    :: !EMA              -- ^ Conflicting Level+              , emaDFast    :: !EMA              -- ^ (Literal Block) Distance Fast+              , emaDSlow    :: !EMA              -- ^ (Literal Block) Distance Slow               , nextRestart :: !Int'             -- ^ next restart in number of conflict-              , restartMode :: Int'              -- ^ mode of restart+              , restartExp  :: !Double'          -- ^ incremented by blocking+              , emaRstBias  :: !EMA              -- ^ average phase of restart               }  -- | returns an everything-is-initialized solver from the arguments.@@ -101,7 +104,7 @@     -- Clause Database     <$> newManager dummy_nc                -- clauses     <*> newManager 2000                    -- learnts-    <*> newWatcherList nv 2                -- watches+    <*> newWatcherList nv 1                -- watches     -- Assignment Management     <*> newVec nv LBottom                  -- assigns     <*> newVec nv LBottom                  -- phases@@ -110,6 +113,7 @@     <*> new' 0                             -- qHead     <*> newClauseVector (nv + 1)           -- reason     <*> newVec nv (-1)                     -- level+    <*> newVec (2 * (nv + 1)) 0            -- ndd     <*> newStack nv                        -- conflicts     -- Variable Order     <*> newVec nv 0                        -- activities@@ -136,12 +140,17 @@     <*> 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+    <*> newEMA False ef                    -- emaAFast+    <*> newEMA True es                     -- emaASlow+    <*> newEMA True 2                      -- emaBDLvl+    <*> newEMA True 2                      -- emaCDLvl+    <*> newEMA False ef                    -- emaDFast+    <*> newEMA True es                     -- emaDSlow     <*> new' 100                           -- nextRestart-    <*> new' 1                             -- restartMode+    <*> new' 0.0                           -- restartExp+    <*> newEMA False 100                   -- emaRstBias+  where+    (ef, es) = emaCoeffs conf  -------------------------------------------------------------------------------- -- Accessors@@ -267,7 +276,7 @@         -- 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+        undoVO s x         -- insertHeap s x              -- insertVerOrder         loopOnTrail $ c - 1     loopOnTrail ts@@ -295,12 +304,12 @@     -- 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+  {-# SPECIALIZE INLINE updateVO :: Solver -> Var -> IO () #-}+  updateVO = increaseHeap+  {-# SPECIALIZE INLINE undoVO :: Solver -> Var -> IO () #-}+  undoVO s v = inHeap s v >>= (`unless` insertHeap s v)+  {-# SPECIALIZE INLINE selectVO :: Solver -> IO Var #-}+  selectVO s = do     let       asg = assigns s       -- | returns the most active var (heap-based implementation)@@ -418,37 +427,3 @@   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

@@ -37,6 +37,11 @@        , Int (LiftedF, LiftedT, LBottom, Conflict)        -- a heap        , VarOrder (..)+       -- Exponential Moving Average, EMA+       , EMA+       , newEMA+       , getEMA+       , updateEMA          -- * statistics        , StatIndex (..)        , DumpMode (..)@@ -250,36 +255,72 @@   newVar = error "newVar undefined" -}   -- | should be called when a variable has increased in activity.-  update :: o -> Var -> IO ()-  update _  = error "update undefined"+  updateVO :: o -> Var -> IO ()+  updateVO _  = 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"+  undoVO :: o -> Var -> IO ()+  undoVO _ _  = error "undo undefined"    -- | returns a new, unassigned var as the next decision.-  select :: o -> IO Var-  select    = error "select undefined"+  selectVO :: o -> IO Var+  selectVO    = error "select undefined" +-------------------------------------------------------------------------------- EMA++-- | Exponential Moving Average, EMA+type EMA = (Double', Maybe Double', Double)++-- | returns a new EMA from a flag (slow or fast) and a window size+{-# INLINE newEMA #-}+newEMA :: Bool -> Int -> IO EMA+newEMA True s = do v <- new' 0.0+                   c <- new' 0.0+                   return (v, Just c, 1 / fromIntegral s)+newEMA False s = do v <- new' 0.0; return (v, Nothing, 1 / fromIntegral s)++-- | returns an EMA value+{-# INLINE getEMA #-}+getEMA :: EMA -> IO Double+getEMA (ema, Just cal, _) = do x <- get' ema+                               c <- get' cal+                               return $ if c == 0 then 0 else x / c+getEMA (ema, Nothing, _)  = get' ema++-- | updates an EMA+{-# INLINE updateEMA #-}+updateEMA :: EMA -> Double -> IO Double+updateEMA (ema, Just cal, cof) x = do e <- ((cof * x) +) . ((1 - cof) *) <$> get' ema+                                      set' ema e+                                      c <- ((cof * 1) +) . ((1 - cof) *) <$> get' cal+                                      set' cal c+                                      return $ e / c+updateEMA (ema, Nothing, cof) x = do e <- ((cof * x) +) . ((1 - cof) *) <$> get' ema; set' ema e; return e++-------------------------------------------------------------------------------- CNF+ -- | 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+  , _pathname :: !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+                           variableDecayRate  :: !Double     -- ^ decay rate for variable activity+                         , clauseDecayRate    :: !Double     -- ^ decay rate for clause activity+                         , dumpSolverStatMode :: !Int        -- ^ dump stats data during solving+                         , emaCoeffs          :: !(Int, Int) -- ^ the coefficients for restarts+                         , restartExpansion   :: !Double     -- ^ restart expansion factor+                         , restartStep        :: !Double     -- ^ static Steps between restarts                          }   deriving (Eq, Ord, Read, Show) @@ -291,7 +332,9 @@ -- * Mios-1.2     uses @(0.95, 0.999, 0)@. -- defaultConfiguration :: MiosConfiguration-defaultConfiguration = MiosConfiguration 0.95 0.999 0+defaultConfiguration = MiosConfiguration 0.95 0.999 0 (ef, es) 1.15 100+  where ef = (2 :: Int) ^ ( 5 :: Int)+        es = (2 :: Int) ^ (14 :: Int)  -------------------------------------------------------------------------------- Statistics 

@@ -24,7 +24,7 @@        , StackFamily (..)        , Stack        , newStackFromList-       , realLengthOfStack+       , realLength        , sortStack        )        where@@ -98,67 +98,6 @@   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)@@ -181,10 +120,14 @@                                         BA.writeByteArray v j (x :: Int)   {-# SPECIALIZE INLINE reset :: ByteArrayInt -> IO () #-}   reset (ByteArrayInt v) = BA.writeByteArray v 0 (0 :: Int)+  {-# SPECIALIZE INLINE newVec :: Int -> Int -> IO ByteArrayInt #-}   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+  growBy (ByteArrayInt v) n = do v' <- BA.newByteArray (BA.sizeofMutableByteArray v + 8 * n)+                                 BA.copyMutableByteArray v' 0 v 0 (BA.sizeofMutableByteArray v)+                                 return (ByteArrayInt v')   asList (ByteArrayInt v) = mapM (BA.readByteArray v) [0 .. div (BA.sizeofMutableByteArray v) 8 - 1]  instance VecFamily ByteArrayDouble Double where@@ -201,12 +144,18 @@                                            BA.writeByteArray v j (x :: Int)   {-# SPECIALIZE INLINE reset :: ByteArrayDouble -> IO () #-}   reset (ByteArrayDouble v) = BA.writeByteArray v 0 (0 :: Double)+  {-# SPECIALIZE INLINE newVec :: Int -> Double -> IO ByteArrayDouble #-}   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] +-- | returns the number of allocated slots+{-# INLINE realLength #-}+realLength :: Vec Int -> Int+realLength (ByteArrayInt v) = div (BA.sizeofMutableByteArray v) 8+ -------------------------------------------------------------------------------- SingleStorage  -- | Interface for single (one-length vector) mutable data@@ -318,37 +267,32 @@       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+      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+            if a < b then return () else setNth vec left b >> setNth vec right a         | 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+                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+                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+                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'

@@ -0,0 +1,14 @@+module MiosSpec (spec) where++import System.IO.Unsafe+import Test.Hspec+import SAT.Mios++testRun :: Spec+testRun = do+  describe "SAT problems" $ do+    let res = unsafePerformIO $ solveSAT (CNFDescription 4 5 Nothing) [[1,2,-3], [-1, -4], [2,4], [1,-3,4], [-3,4]]+    it "a simple SAT" $ res `shouldBe` [-1,2,-3,-4]++spec :: Spec+spec = testRun

@@ -0,0 +1,8 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}+-- main :: IO ()+-- main = putStrLn "Test suite not yet implemented"++--import SAT.Mios+--main :: IO ()+--main = do+--  print =<< solveSAT (CNFDescription 4 5 "") [[1,2,-3], [-1, -4], [2,4], [1,-3,4], [-3,4]]