mios 1.2.1 → 1.3.0

raw patch · 41 files changed

+3654/−3760 lines, 41 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• SAT/Mios.hs +297/−0
• SAT/Mios/Clause.hs +144/−0
• SAT/Mios/ClauseManager.hs +326/−0
• SAT/Mios/Data/Singleton.hs +105/−0
• SAT/Mios/Data/Stack.hs +90/−0
• SAT/Mios/Data/Vec.hs +86/−0
• SAT/Mios/Data/VecBool.hs +55/−0
• SAT/Mios/Data/VecDouble.hs +53/−0
• SAT/Mios/Internal.hs +33/−0
• SAT/Mios/Main.hs +810/−0
• SAT/Mios/OptionParser.hs +133/−0
• SAT/Mios/Solver.hs +611/−0
• SAT/Mios/Types.hs +269/−0
• SAT/Mios/Util/BoolExp.hs +244/−0
• SAT/Mios/Util/CNFIO.hs +31/−0
• SAT/Mios/Util/CNFIO/MinisatReader.hs +73/−0
• SAT/Mios/Util/CNFIO/Reader.hs +130/−0
• SAT/Mios/Util/CNFIO/Writer.hs +58/−0
• SAT/Mios/Validator.hs +48/−0
• SAT/Solver/Mios.hs +0/−298
• SAT/Solver/Mios/Clause.hs +0/−144
• SAT/Solver/Mios/ClauseManager.hs +0/−324
• SAT/Solver/Mios/Data/Singleton.hs +0/−196
• SAT/Solver/Mios/Data/Stack.hs +0/−93
• SAT/Solver/Mios/Data/Vec.hs +0/−86
• SAT/Solver/Mios/Data/VecBool.hs +0/−55
• SAT/Solver/Mios/Data/VecDouble.hs +0/−53
• SAT/Solver/Mios/Glucose.hs +0/−72
• SAT/Solver/Mios/Internal.hs +0/−34
• SAT/Solver/Mios/M114.hs +0/−816
• SAT/Solver/Mios/OptionParser.hs +0/−132
• SAT/Solver/Mios/Solver.hs +0/−554
• SAT/Solver/Mios/Types.hs +0/−269
• SAT/Solver/Mios/Validator.hs +0/−47
• SAT/Util/BoolExp.hs +0/−244
• SAT/Util/CNFIO.hs +0/−31
• SAT/Util/CNFIO/MinisatReader.hs +0/−73
• SAT/Util/CNFIO/Reader.hs +0/−130
• SAT/Util/CNFIO/Writer.hs +0/−58
• app/mios.hs +1/−1
• mios.cabal +57/−50

@@ -0,0 +1,297 @@+-- | Minisat-based Implementation and Optimization Study on SAT solver+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE Trustworthy #-}++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.Internal+import SAT.Mios.Solver+import SAT.Mios.Main+import SAT.Mios.OptionParser+import SAT.Mios.Validator++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`) <=< (newSizedVecIntFromList . map int2lit)) c+  noConf <- simplifyDB s+  if noConf+    then do+        x <- solve s []+        if x+            then Right <$> getModel s+            else Left .  map lit2int <$> asList (conflict 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`) <=< (newSizedVecIntFromList . 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`) <=< (newSizedVecIntFromList . 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 -> do+    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+  polvec <- newVecBool (maxLit + 1) False+  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 <- getNthBool polvec $ var2lit v True+      n <- getNthBool polvec $ var2lit v False+      when (p == False || n == False) $ setNth asg v $ if p then lTrue else lFalse+      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 -> Vec -> VecBool -> B.ByteString -> IO B.ByteString+readClause s buffer pvec 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+            addClause s buffer+            return b'+        else do+            let l = int2lit k+            setNth buffer i l+            setNthBool pvec l True+            loop (i + 1) b'+  loop 1 . skipComments . skipWhitespace $ stream+++showPath :: FilePath -> String+showPath str+  | elem '/' str =  take (len - length basename) (repeat ' ') ++ basename+  |  otherwise = take (len - length basename') (repeat ' ') ++ basename'+  where+    len = 50+    basename = reverse . takeWhile (/= '/') . reverse $ str+    basename' = take len str

@@ -0,0 +1,144 @@+{-# LANGUAGE+    BangPatterns+  , FlexibleInstances+  , MagicHash+  , MultiParamTypeClasses+  , RecordWildCards+  , ViewPatterns+  #-}+{-# LANGUAGE Trustworthy #-}++-- | Clause, supporting pointer-based equality+module SAT.Mios.Clause+       (+         Clause (..)+--       , isLit+--       , getLit+       , shrinkClause+       , newClauseFromVec+       , sizeOfClause+         -- * Vector of Clause+       , ClauseVector+       , newClauseVector+       , getNthClause+       , setNthClause+       , swapClauses+       )+       where++import Control.Monad (forM_)+import GHC.Prim (tagToEnum#, reallyUnsafePtrEquality#)+import qualified Data.Vector as V+import qualified Data.Vector.Mutable as MV+import qualified Data.Vector.Unboxed.Mutable as UV+import Data.List (intercalate)+import SAT.Mios.Types++-- | __Fig. 7.(p.11)__+-- clause, null, binary clause.+-- This matches both of @Clause@ and @GClause@ in MiniSat+-- TODO: GADTs is better?+data Clause = Clause+              {+                learnt     :: !Bool            -- ^ whether this is a learnt clause+--              , rank       :: !IntSingleton    -- ^ goodness like LBD; computed in 'Ranking'+              , activity   :: !DoubleSingleton -- ^ activity of this clause+              , protected  :: !BoolSingleton   -- ^ protected from reduce+              , lits       :: !Vec             -- ^ 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"++-- | supports a restricted set of 'VectorFamily' methods+instance VectorFamily Clause Lit where+  dump mes NullClause = return $ mes ++ "Null"+  dump mes Clause{..} = do+    a <- show <$> getDouble activity+    (len:ls) <- asList lits+    return $ mes ++ "C" ++ show len ++ "{" ++ intercalate "," [show learnt, a, show . map lit2int . take len $ ls] ++ "}"+  {-# SPECIALIZE INLINE asVec :: Clause -> Vec #-}+  asVec Clause{..} = UV.unsafeTail lits+  {-# SPECIALIZE INLINE asList :: Clause -> IO [Int] #-}+  asList NullClause = return []+  asList Clause{..} = do+    (n : ls)  <- asList lits+    return $ take n ls++-- 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.+{-# INLINE newClauseFromVec #-}+newClauseFromVec :: Bool -> Vec -> IO Clause+newClauseFromVec l vec = do+  n <- getNth vec 0+  v <- newVec $ n + 1+  forM_ [0 .. n] $ \i -> setNth v i =<< getNth vec i+  Clause l <$> {- newInt 0 <*> -} newDouble 0 <*> newBool False <*> return v++-- | returns the number of literals in a clause, even if the given clause is a binary clause+{-# INLINE sizeOfClause #-}+sizeOfClause :: Clause -> IO Int+-- sizeOfClause (BinaryClause _) = return 1+sizeOfClause !c = getNth (lits c) 0++-- | drop the last /N/ literals in a 'Clause' to eliminate unsatisfied literals+{-# INLINABLE shrinkClause #-}+shrinkClause :: Int -> Clause -> IO ()+shrinkClause n !c = modifyNth (lits c) (subtract n) 0++--------------------------------------------------------------------------------++-- | Mutable 'Clause' Vector+type ClauseVector = MV.IOVector Clause++instance VectorFamily ClauseVector Clause where+  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++-- | returns the nth 'Clause'+{-# INLINE getNthClause #-}+getNthClause :: ClauseVector -> Int -> IO Clause+getNthClause = MV.unsafeRead++-- | sets the nth 'Clause'+{-# INLINE setNthClause #-}+setNthClause :: ClauseVector -> Int -> Clause -> IO ()+setNthClause = MV.unsafeWrite++-- | swaps the two 'Clause's+{-# INLINE swapClauses #-}+swapClauses :: ClauseVector -> Int -> Int -> IO ()+swapClauses = MV.unsafeSwap

@@ -0,0 +1,326 @@+{-# LANGUAGE+    BangPatterns+  , DuplicateRecordFields+  , FlexibleInstances+  , MultiParamTypeClasses+  , RecordWildCards+  , ViewPatterns+  #-}+{-# LANGUAGE Trustworthy #-}++-- | A shrinkable vector of 'C.Clause'+module SAT.Mios.ClauseManager+       (+         -- * higher level interface for ClauseVector+         ClauseManager (..)+--       -- * vector of clauses+--       , SimpleManager+         -- * Manager with an extra Int (used as sort key or blocking literal)+       , ClauseExtManager+       , pushClauseWithKey+       , getKeyVector+       , markClause+--       , purifyManager+         -- * WatcherList+       , WatcherList+       , newWatcherList+       , getNthWatcher+       , garbageCollect+--       , numberOfRegisteredClauses+       )+       where++import Control.Monad (forM, unless, when)+import qualified Data.IORef as IORef+import qualified Data.List as L+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 clause vector+class ClauseManager a where+  newManager      :: Int -> IO a+  numberOfClauses :: a -> IO Int+  clearManager    :: a -> IO ()+  shrinkManager   :: a -> Int -> IO ()+  getClauseVector :: a -> IO C.ClauseVector+  pushClause      :: a -> C.Clause -> IO ()+--  removeClause    :: a -> C.Clause -> IO ()+--  removeNthClause :: a -> Int -> IO ()++{-+-- | The Clause Container+data SimpleManager = SimpleManager+  {+    _nActives     :: IntSingleton               -- number of active clause+  , _clauseVector :: IORef.IORef C.ClauseVector -- clause list+  }++instance ClauseManager SimpleManager where+  {-# SPECIALIZE INLINE newManager :: Int -> IO SimpleManager #-}+  newManager initialSize = do+    i <- newInt 0+    v <- C.newClauseVector initialSize+    SimpleManager i <$> IORef.newIORef v+  {-# SPECIALIZE INLINE numberOfClauses :: SimpleManager -> IO Int #-}+  numberOfClauses SimpleManager{..} = getInt _nActives+  {-# SPECIALIZE INLINE clearManager :: SimpleManager -> IO () #-}+  clearManager SimpleManager{..} = setInt _nActives 0+  {-# SPECIALIZE INLINE shrinkManager :: SimpleManager -> Int -> IO () #-}+  shrinkManager SimpleManager{..} k = modifyInt _nActives (subtract k)+  {-# SPECIALIZE INLINE getClauseVector :: SimpleManager -> IO C.ClauseVector #-}+  getClauseVector SimpleManager{..} = IORef.readIORef _clauseVector+  -- | O(1) inserter+  {-# SPECIALIZE INLINE pushClause :: SimpleManager -> C.Clause -> IO () #-}+  pushClause !SimpleManager{..} !c = do+    !n <- getInt _nActives+    !v <- IORef.readIORef _clauseVector+    if MV.length v - 1 <= n+      then do+          v' <- MV.unsafeGrow v (max 8 (MV.length v))+          -- forM_ [n  .. MV.length v' - 1] $ \i -> MV.unsafeWrite v' i C.NullClause+          MV.unsafeWrite v' n c+          IORef.writeIORef _clauseVector v'+      else MV.unsafeWrite v n c+    modifyInt _nActives (1 +)+  -- | O(1) remove-and-compact function+  {-# SPECIALIZE INLINE removeNthClause :: SimpleManager -> Int -> IO () #-}+  removeNthClause SimpleManager{..} i = do+    !n <- subtract 1 <$> getInt _nActives+    !v <- IORef.readIORef _clauseVector+    MV.unsafeWrite v i =<< MV.unsafeRead v n+    setInt _nActives n+  -- | 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 :: SimpleManager -> C.Clause -> IO () #-}+  removeClause SimpleManager{..} c = do+    -- putStrLn =<< dump "@removeClause| remove " c+    -- putStrLn =<< dump "@removeClause| from " m+    !n <- subtract 1 <$> getInt _nActives+    -- unless (0 <= n) $ error $ "removeClause catches " ++ show n+    !v <- IORef.readIORef _clauseVector+    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+      setInt _nActives n++instance VectorFamily SimpleManager C.Clause where+  dump mes SimpleManager{..} = do+    n <- getInt _nActives+    if n == 0+      then return $ mes ++ "empty clausemanager"+      else do+          l <- take n <$> (asList =<< IORef.readIORef _clauseVector)+          sts <- mapM (dump ",") (l :: [C.Clause])+          return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts)+-}++--------------------------------------------------------------------------------++-- | Clause + Blocking Literal+data ClauseExtManager = ClauseExtManager+  {+    _nActives     :: !IntSingleton               -- number of active clause+  , _purged       :: !BoolSingleton              -- whether it needs gc+  , _clauseVector :: IORef.IORef C.ClauseVector -- clause list+  , _keyVector    :: IORef.IORef Vec            -- Int list+  }++instance ClauseManager ClauseExtManager where+  {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-}+  newManager initialSize = do+    i <- newInt 0+    v <- C.newClauseVector initialSize+    b <- newVec (MV.length v)+    ClauseExtManager i <$> newBool False <*> IORef.newIORef v <*> IORef.newIORef b+  {-# SPECIALIZE INLINE numberOfClauses :: ClauseExtManager -> IO Int #-}+  numberOfClauses !m = getInt (_nActives m)+  {-# SPECIALIZE INLINE clearManager :: ClauseExtManager -> IO () #-}+  clearManager !m = setInt (_nActives m) 0+  {-# SPECIALIZE INLINE shrinkManager :: ClauseExtManager -> Int -> IO () #-}+  shrinkManager !m k = modifyInt (_nActives m) (subtract k)+  {-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-}+  getClauseVector !m = IORef.readIORef (_clauseVector m)+  -- | O(1) insertion function+  {-# SPECIALIZE INLINE pushClause :: ClauseExtManager -> C.Clause -> IO () #-}+  pushClause !ClauseExtManager{..} !c = do+    -- checkConsistency m c+    !n <- getInt _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' <- vecGrow 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+    modifyInt _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 <$> getInt _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+      setInt _nActives n+  removeNthClause = error "removeNthClause is not implemented on ClauseExtManager"+-}++-- | sets the expire flag to a clause+{-# INLINE markClause #-}+markClause :: ClauseExtManager -> C.Clause -> IO ()+markClause ClauseExtManager{..} c = do+  !n <- getInt _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+    setBool _purged True++{-# INLINE purifyManager #-}+purifyManager :: ClauseExtManager -> IO ()+purifyManager ClauseExtManager{..} = do+  diry <- getBool _purged+  when diry $ do+    n <- getInt _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 <- C.getNthClause vec i+        if c /= C.NullClause+          then do+              unless (i == j) $ do+                C.setNthClause vec j c+                setNth keys j =<< getNth keys i+              loop (i + 1) (j + 1)+          else loop (i + 1) j+    setInt _nActives =<< loop 0 0+    setBool _purged False++-- | returns the associated Int vector+{-# INLINE getKeyVector #-}+getKeyVector :: ClauseExtManager -> IO Vec+getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector++-- | O(1) inserter+{-# INLINE pushClauseWithKey #-}+pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO ()+pushClauseWithKey !ClauseExtManager{..} !c k = do+  -- checkConsistency m c+  !n <- getInt _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' <- vecGrow 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+  modifyInt _nActives (1 +)++instance VectorFamily ClauseExtManager C.Clause where+  dump mes ClauseExtManager{..} = do+    n <- getInt _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++-- | 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 <$> forM [0 .. int2lit (negate n) + 1] (\_ -> newManager m)++-- | returns the watcher List :: "ClauseManager" for "Literal" /l/+{-# INLINE getNthWatcher #-}+getNthWatcher :: WatcherList -> Lit -> ClauseExtManager+getNthWatcher = V.unsafeIndex++instance VectorFamily WatcherList C.Clause where+  dump mes wl = (mes ++) . L.concat <$> forM [1 .. V.length wl - 1] (\i -> dump ("\n" ++ show (lit2int i) ++ "' watchers:") (getNthWatcher wl i))++-- | purges all expirable clauses in 'WatcherList'+{-# INLINE garbageCollect #-}+garbageCollect :: WatcherList -> IO ()+garbageCollect = V.mapM_ purifyManager++{-+numberOfRegisteredClauses :: WatcherList -> IO Int+numberOfRegisteredClauses ws = sum <$> V.mapM numberOfClauses ws+-}++{-+-------------------------------------------------------------------------------- debugging stuff++checkConsistency :: ClauseManager a => a -> C.Clause -> IO ()+checkConsistency manager c = do+  nc <- numberOfClauses manager+  vec <- getClauseVector manager+  let+    loop :: Int -> IO ()+    loop i = do+      when (i < nc) $ do+        c' <- MV.unsafeRead vec i+        when (c' == c) $ error "insert a clause to a ClauseMananger twice"+        loop $ i + 1+  loop 0++checkClauseOrder :: ClauseManager a => a -> IO ()+checkClauseOrder manager = do+  putStr "checking..."+  nc <- numberOfClauses manager+  vec <- getClauseVector manager+  let+    nthActivity :: Int -> IO Double+    nthActivity i = getDouble . C.activity =<< MV.unsafeRead vec i+    report :: Int -> Int -> IO ()+    report i j = (putStr . (++ ", ") . show =<< nthActivity i) >> when (i < j) (report (i + 1) j)+    loop :: Int -> Double -> IO ()+    loop i v = do+      when (i < nc) $ do+        c <- MV.unsafeRead vec i+        a <- getDouble (C.activity c)+        when (c == C.NullClause) $ error "null is included"+        when (v < a) $ report 0 i >> error ("unsorted clause vector: " ++ show (nc, i))+        loop (i + 1) a+  loop 0 =<< nthActivity 0+  putStrLn "done"+-}

@@ -0,0 +1,105 @@+{-# LANGUAGE+    BangPatterns+  #-}+{-# LANGUAGE Trustworthy #-}++-- | A fast(est) mutable data based on Data.Vector.Unboxed.Mutable++module SAT.Mios.Data.Singleton+       (+         -- * Bool+         BoolSingleton+       , newBool+       , getBool+       , setBool+       , modifyBool+         -- * Int+       , IntSingleton+       , newInt+       , getInt+       , setInt+       , modifyInt+         -- * Double+       , DoubleSingleton+       , newDouble+       , getDouble+       , setDouble+       , modifyDouble+       )+       where+import qualified Data.Vector.Unboxed.Mutable as UV++-- | mutable Int+type IntSingleton = UV.IOVector Int++-- | returns a new 'IntSingleton'+newInt :: Int -> IO IntSingleton+newInt k = do+  s <- UV.new 1+  UV.unsafeWrite s 0 k+  return s++-- | returns the value+{-# INLINE getInt #-}+getInt :: IntSingleton -> IO Int+getInt val = UV.unsafeRead val 0++-- | sets the value+{-# INLINE setInt #-}+setInt :: IntSingleton -> Int -> IO ()+setInt val !x = UV.unsafeWrite val 0 x++-- | modifies the value+{-# INLINE modifyInt #-}+modifyInt :: IntSingleton -> (Int -> Int) -> IO ()+modifyInt val f = UV.unsafeModify val f 0++-- | mutable Bool+type BoolSingleton = UV.IOVector Bool++-- | returns a new 'BoolSingleton'+newBool :: Bool -> IO BoolSingleton+newBool b = do+  s <- UV.new 1+  UV.unsafeWrite s 0 b+  return s++-- | returns the value+{-# INLINE getBool #-}+getBool :: BoolSingleton -> IO Bool+getBool val = UV.unsafeRead val 0++-- | sets the value+{-# INLINE setBool #-}+setBool :: BoolSingleton -> Bool -> IO ()+setBool val !x = UV.unsafeWrite val 0 x++-- | modifies the value+{-# INLINE modifyBool #-}+modifyBool :: BoolSingleton -> (Bool -> Bool) -> IO ()+modifyBool val f = UV.unsafeModify val f 0++-- | mutable Double+type DoubleSingleton = UV.IOVector Double++-- | returns a new 'DoubleSingleton'+newDouble :: Double -> IO DoubleSingleton+newDouble d = do+  s <- UV.new 1+  UV.unsafeWrite s 0 d+  return s++-- | returns the value+{-# INLINE getDouble #-}+getDouble :: DoubleSingleton -> IO Double+getDouble val = UV.unsafeRead val 0++-- | sets the value+{-# INLINE setDouble #-}+setDouble :: DoubleSingleton -> Double -> IO ()+setDouble val !x = UV.unsafeWrite val 0 x++-- | modifies the value+{-# INLINE modifyDouble #-}+modifyDouble :: DoubleSingleton -> (Double -> Double) -> IO ()+modifyDouble val f = UV.unsafeModify val f 0

@@ -0,0 +1,90 @@+{-# LANGUAGE+    MultiParamTypeClasses+  #-}+{-# LANGUAGE Trustworthy #-}++-- | stack of Int, by adding the length field as the zero-th element to a 'Vec'+module SAT.Mios.Data.Stack+       (+         Stack+       , newStack+       , clearStack+       , sizeOfStack+       , pushToStack+       , popFromStack+       , lastOfStack+       , shrinkStack+       , asSizedVec+--       , isoVec+       )+       where++import qualified Data.Vector.Unboxed.Mutable as UV+import SAT.Mios.Types++-- | Unboxed mutable stack for Int.+newtype Stack = Stack (UV.IOVector Int)++instance VectorFamily Stack Int where+  dump str v = (str ++) . show <$> asList v+  {-# SPECIALIZE INLINE asVec :: Stack -> Vec #-}+  asVec (Stack v) = UV.unsafeTail v+  asList (Stack v) = do+    (n : l) <- asList v+    return $ take n l++-- | returns the number of elements+{-# INLINE sizeOfStack #-}+sizeOfStack :: Stack -> IO Int+sizeOfStack (Stack v) = UV.unsafeRead v 0++-- | clear stack+{-# INLINE clearStack #-}+clearStack :: Stack -> IO ()+clearStack (Stack v) = UV.unsafeWrite v 0 0++-- | returns a new stack which size is @size@+{-# INLINABLE newStack #-}+newStack :: Int -> IO Stack+newStack n = do+  v <- UV.new $ n + 1+  UV.set v 0+  return $ Stack v++-- | pushs an int to 'Stack'+{-# INLINE pushToStack #-}+pushToStack :: Stack -> Int -> IO ()+pushToStack (Stack v) x = do+  i <- (+ 1) <$> UV.unsafeRead v 0+  UV.unsafeWrite v i x+  UV.unsafeWrite v 0 i++-- | drops the first element from 'Stack'+{-# INLINE popFromStack #-}+popFromStack :: Stack -> IO ()+popFromStack (Stack v) = UV.unsafeModify v (subtract 1) 0++-- | peeks the last element in 'Stack'+{-# INLINE lastOfStack #-}+lastOfStack :: Stack -> IO Int+lastOfStack (Stack v) = UV.unsafeRead v =<< UV.unsafeRead v 0++-- | Shrink the stack. The given arg means the number of discards.+-- therefore, shrink s n == for [1 .. n] $ \_ -> pop s+{-# INLINE shrinkStack #-}+shrinkStack :: Stack -> Int -> IO ()+shrinkStack (Stack v) k = UV.unsafeModify v (subtract k) 0++-- | converts Stack to sized Vec; this is the method to get the internal vector+{-# INLINE asSizedVec #-}+asSizedVec :: Stack -> Vec+asSizedVec (Stack v) = v++{-+-- | isomorphic conversion to 'Vec'+--+-- Note: 'asVec' drops the 1st element and no copy (unsafe operation); 'isoVec' really copies the real elements+{-# INLINE isoVec #-}+isoVec :: Stack -> IO Vec+isoVec (Stack v) = UV.clone . flip UV.take v . (1 +) =<< UV.unsafeRead v 0+-}

@@ -0,0 +1,86 @@+-- | The fundamental data structure: Fixed Mutable Unboxed Int Vector+{-# LANGUAGE+    BangPatterns+  #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Mios.Data.Vec+       (+         Vec+       , sizeOfVector+       , getNth+       , setNth+       , swapBetween+       , modifyNth+       , setAll+       , newVec+       , newVecWith+       , newSizedVecIntFromList+       , newSizedVecIntFromUVector+       , vecGrow+       )+       where++import qualified Data.Vector.Unboxed as U+import qualified Data.Vector.Unboxed.Mutable as UV++-- | Costs of all operations are /O/(/1/)+type Vec = UV.IOVector Int++-- | returns the size of 'Vec'+{-# INLINE sizeOfVector #-}+sizeOfVector :: Vec -> IO Int+sizeOfVector v = return $! UV.length v++-- | returns a new 'Vec'+{-# INLINE newVec #-}+newVec :: Int -> IO Vec+newVec = UV.new++-- | returns a new 'Vec' filled with an Int+{-# INLINE newVecWith #-}+newVecWith :: Int -> Int -> IO Vec+newVecWith n x = do+  v <- UV.new n+  UV.set v x+  return v++-- | gets the nth value+{-# INLINE getNth #-}+getNth :: Vec -> Int -> IO Int+getNth = UV.unsafeRead++-- | sets the nth value+{-# INLINE setNth #-}+setNth :: Vec -> Int -> Int -> IO ()+setNth = UV.unsafeWrite++-- | modify the nth value+{-# INLINE modifyNth #-}+modifyNth :: Vec -> (Int -> Int) -> Int -> IO ()+modifyNth = UV.unsafeModify++-- | sets all elements+{-# INLINE setAll #-}+setAll :: Vec -> Int -> IO ()+setAll = UV.set++-- | swaps two elements+{-# INLINE swapBetween #-}+swapBetween:: Vec -> Int -> Int -> IO ()+swapBetween = UV.unsafeSwap++-- | returns a new 'Vec' from a @[Int]@+{-# INLINE newSizedVecIntFromList #-}+newSizedVecIntFromList :: [Int] -> IO Vec+newSizedVecIntFromList !l = U.unsafeThaw $ U.fromList (length l : l)++-- | returns a new 'Vec' from a Unboxed Int Vector+{-# INLINE newSizedVecIntFromUVector #-}+newSizedVecIntFromUVector :: U.Vector Int -> IO Vec+newSizedVecIntFromUVector = U.unsafeThaw++-- | calls @unasfeGrow@+{-# INLINE vecGrow #-}+vecGrow :: Vec -> Int -> IO Vec+vecGrow = UV.unsafeGrow

@@ -0,0 +1,55 @@+-- | Mutable Unboxed Boolean Vector+--+-- * __VecBool@::UV.IOVector Bool@ -- data type that contains a mutable list of elements+--+{-# LANGUAGE+    BangPatterns+  , FlexibleInstances+  , MultiParamTypeClasses+  #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Mios.Data.VecBool+       (+         VecBool+       , newVecBool+       , getNthBool+       , setNthBool+       , modifyNthBool+       )+       where++import Control.Monad (forM)+import qualified Data.Vector.Unboxed.Mutable as UV+import SAT.Mios.Types (VectorFamily(..))++-- | Mutable unboxed Bool Vector+type VecBool = UV.IOVector Bool++-- | provides 'clear' and 'size'+instance VectorFamily VecBool Bool where+  clear _ = error "VecBool.clear"+  asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v+  dump str v = (str ++) . show <$> asList v++-- | returns a new 'VecBool'+newVecBool :: Int -> Bool -> IO VecBool+newVecBool n x = do+  v <- UV.new n+  UV.set v x+  return v++-- | returns the nth value in 'VecBool'+{-# INLINE getNthBool #-}+getNthBool :: VecBool -> Int -> IO Bool+getNthBool = UV.unsafeRead++-- | sets the nth value+{-# INLINE setNthBool #-}+setNthBool :: VecBool -> Int -> Bool -> IO ()+setNthBool = UV.unsafeWrite++-- | sets the nth value+{-# INLINE modifyNthBool #-}+modifyNthBool :: VecBool -> (Bool -> Bool) -> Int -> IO ()+modifyNthBool = UV.unsafeModify

@@ -0,0 +1,53 @@+-- | Mutable Unboxed Double Vector+{-# LANGUAGE+    BangPatterns+  , FlexibleInstances+  , MultiParamTypeClasses+  #-}+{-# LANGUAGE Trustworthy #-}++module SAT.Mios.Data.VecDouble+       (+         VecDouble+       , newVecDouble+       , getNthDouble+       , setNthDouble+       , modifyNthDouble+       )+       where++import Control.Monad (forM)+import Data.List ()+import qualified Data.Vector.Unboxed.Mutable as UV+import SAT.Mios.Types (VectorFamily(..))++-- | Mutable unboxed Double Vector+type VecDouble = UV.IOVector Double++instance VectorFamily VecDouble Double where+  clear _ = error "VecDouble.clear"+  asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v+  dump str v = (str ++) . show <$> asList v++-- | returns a new 'VecDouble'+newVecDouble :: Int -> Double -> IO VecDouble+newVecDouble n 0 = UV.new n+newVecDouble n x = do+  v <- UV.new n+  UV.set v x+  return v++-- | returns the nth value in 'VecDouble'+{-# INLINE getNthDouble #-}+getNthDouble :: Int -> VecDouble -> IO Double+getNthDouble !n v = UV.unsafeRead v n++-- | sets the nth value+{-# INLINE setNthDouble #-}+setNthDouble :: Int -> VecDouble -> Double -> IO ()+setNthDouble !n v !x = UV.unsafeWrite v n x++-- | updates the nth value+{-# INLINE modifyNthDouble #-}+modifyNthDouble :: Int -> VecDouble -> (Double -> Double) -> IO ()+modifyNthDouble !n v !f = UV.unsafeModify v f n

@@ -0,0 +1,33 @@+-- | Mios Internal Settings+module SAT.Mios.Internal+       (+         versionId+       , MiosConfiguration (..)+       , defaultConfiguration+       , module Plumbing+       )+       where+import SAT.Mios.Data.VecBool as Plumbing+import SAT.Mios.Data.VecDouble as Plumbing+import SAT.Mios.Data.Stack as Plumbing++-- | version name+versionId :: String+versionId = "mios 1.3.0 -- https://github.com/shnarazk/mios" -- no more LBD++-- | 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 -}

@@ -0,0 +1,810 @@+{-# 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 (forM_, unless, void, when)+import Data.Bits+import Data.Foldable (foldrM)+import SAT.Mios.Types+import SAT.Mios.Internal+import SAT.Mios.Clause+import SAT.Mios.ClauseManager+import SAT.Mios.Solver+-- import SAT.Mios.Ranking++-------------------------------------------------------------------------------- Ranking+-- | a special version of ranking+{-# INLINE ranking' #-}+ranking' :: Clause -> IO Int+ranking' = sizeOfClause++-- | #114: __RemoveWatch__+{-# INLINABLE removeWatch #-}+removeWatch :: Solver -> Clause -> IO ()+removeWatch (watches -> w) c = do+  let lvec = asVec 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)__ create a new LEARNT clause and adds it to watcher lists+-- This is a strippped-down version of 'newClause' in Solver+{-# INLINABLE newLearntClause #-}+newLearntClause :: Solver -> Vec -> IO ()+newLearntClause s@Solver{..} ps = do+  good <- getBool 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 <- getNth ps 0+    case k of+     1 -> do+       l <- getNth ps 1+       unsafeEnqueue s l NullClause+     _ -> do+       -- allocate clause:+       c <- newClauseFromVec True ps+       let vec = asVec 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:+       setDouble (activity c) . fromIntegral =<< decisionLevel s -- newly learnt clauses should be considered active+       -- Add clause to all managers+       pushClause 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+       setBool (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 <- sizeOfClause c+  let+    lvec = asVec 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@+-- {-# INLINEABLE analyze #-}+analyze :: Solver -> Clause -> IO Int+analyze s@Solver{..} confl = do+  -- litvec+  clearStack litsLearnt+  pushToStack litsLearnt 0 -- reserve the first place for the unassigned literal+  dl <- decisionLevel s+  let+    litsVec = asVec litsLearnt+    trailVec = asVec 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 <- getInt (lbd c)+        when (2 < d) $ do+          nblevels <- lbdOf s c+          when (nblevels + 1 < d) $ do -- improve the LBD+            when (d <= 30) $ setBool (protected c) True -- 30 is `lbLBDFrozenClause`+            -- seems to be interesting: keep it fro the next round+            setInt (lbd c) nblevels    -- Update it+-}+      sc <- sizeOfClause c+      let+        lvec = asVec 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 <- getNthClause reason v+                      when (r /= NullClause && learnt r) $ pushToStack lastDL q+                      -- end of glucose heuristics+                      loopOnLiterals (j + 1) b (pc + 1)+                  else pushToStack 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' <- getNthClause 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 <$> sizeOfStack trail+  levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0+  -- Simplify phase (implemented only @expensive_ccmin@ path)+  n <- sizeOfStack litsLearnt+  clearStack an'stack           -- analyze_stack.clear();+  clearStack an'toClear         -- out_learnt.copyTo(analyze_toclear);+  pushToStack 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+      pushToStack 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' = shrinkStack litsLearnt $ n - n'+    loopOnLits i j = do+      l <- getNth litsVec i+      c1 <- (NullClause ==) <$> getNthClause 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 <- sizeOfStack lastDL+  r <- sizeOfStack litsLearnt -- this is not the right value+  let+    vec = asVec lastDL+    loopOnLastDL :: Int -> IO ()+    loopOnLastDL ((< nld) -> False) = return ()+    loopOnLastDL i = do+      v <- lit2var <$> getNth vec i+      r' <- ranking' =<< getNthClause reason v+      when (r < r') $ varBumpActivity s v+      loopOnLastDL $ i + 1+  loopOnLastDL 0+  clearStack lastDL+  -- Clear seen+  k <- sizeOfStack an'toClear+  let+    vec' = asVec 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@.+--+{-# INLINEABLE analyzeRemovable #-}+analyzeRemovable :: Solver -> Lit -> Int -> IO Bool+analyzeRemovable Solver{..} p minLevel = do+  -- assert (reason[var(p)]!= NullCaulse);+  clearStack an'stack      -- analyze_stack.clear()+  pushToStack an'stack p   -- analyze_stack.push(p);+  top <- sizeOfStack an'toClear+  let+    loopOnStack :: IO Bool+    loopOnStack = do+      k <- sizeOfStack an'stack  -- int top = analyze_toclear.size();+      if 0 == k+        then return True+        else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL);+            sl <- lastOfStack an'stack+            popFromStack an'stack             -- analyze_stack.pop();+            c <- getNthClause reason (lit2var sl) -- getRoot sl+            nl <- sizeOfClause c+            let+              cvec = asVec 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 /=) <$> getNthClause 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;+                            pushToStack an'stack p'    -- analyze_stack.push(p);+                            pushToStack 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' <- sizeOfStack an'toClear+                            let vec = asVec an'toClear+                            forM_ [top .. top' - 1] $ \j -> do x <- getNth vec j; setNth an'seen (lit2var x) 0+                            -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop+                            shrinkStack 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).+--+analyzeFinal :: Solver -> Clause -> Bool -> IO ()+analyzeFinal Solver{..} confl skipFirst = do+  clearStack conflict+  rl <- getInt rootLevel+  unless (rl == 0) $ do+    n <- sizeOfClause confl+    let+      lvec = asVec 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 <- sizeOfStack trailLim+    trs <- sizeOfStack trail+    tlz <- getNth (asVec trailLim) 0+    let+      trailVec = asVec 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) <- getNthClause reason x+          if r == NullClause+            then pushToStack conflict (negateLit l)+            else do+                k <- sizeOfClause r+                let+                  cvec = asVec 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 (asVec 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 = asVec trail+    while :: Clause -> Bool -> IO Clause+    while confl False = {- bumpAllVar >> -} return confl+    while confl True = do+      (p :: Lit) <- getNth trailVec =<< getInt qHead+      modifyInt qHead (+ 1)+      let (ws :: ClauseExtManager) = getNthWatcher watches p+      end <- numberOfClauses ws+      cvec <- getClauseVector ws+      bvec <- getKeyVector ws+--      rc <- getNthClause reason $ lit2var p+--      byGlue <- if (rc /= NullClause) && learnt rc then (== 2) <$> getInt (lbd rc) else return False+      let+{-+        checkAllLiteralsIn :: Clause -> IO () -- not in use+        checkAllLiteralsIn c = do+          nc <- sizeOfClause c+          let+            vec = asVec 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+          shrinkManager ws (i - j)+          while confl =<< ((<) <$> getInt qHead <*> sizeOfStack 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) <- getNthClause cvec i+                   setNthClause cvec j c+                   setNth bvec j l+                 forClause confl (i + 1) (j + 1)+            else do+                -- checkAllLiteralsIn c+                (c :: Clause) <- getNthClause cvec i+                let+                  lits = asVec 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 setNthClause cvec j c >> setNth bvec j first >> forClause confl (i + 1) (j + 1)+                  else do+                      -- Look for new watch+                      cs <- sizeOfClause c+                      let+                        forLit :: Int -> IO Clause+                        forLit ((< cs) -> False) = do+                          -- Did not find watch; clause is unit under assignment:+                          setNthClause cvec j c+                          setNth bvec j 0+                          result <- enqueue s first c+                          if not result+                            then do+                                ((== 0) <$> decisionLevel s) >>= (`when` setBool ok False)+                                -- #BBCP+                                setInt qHead =<< sizeOfStack trail+                                -- Copy the remaining watches:+                                let+                                  copy i'@((< end) -> False) j' = forClause c i' j'+                                  copy i' j' = do+                                    setNthClause cvec j' =<< getNthClause 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 =<< ((<) <$> getInt qHead <*> sizeOfStack 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 =<< getNthClause 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+  garbageCollect watches+  shrinkManager 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 <- numberOfClauses 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 <- getNthClause vec i+      k <- (\k -> if k == 2 then return k else fromEnum <$> getBool (protected c)) =<< sizeOfClause c+      case k of+        1 -> setBool (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 <- ranking' c+                  b <- floor . (activityScale *) . (1 -) . logBase claActivityThreshold . max 1 <$> getDouble (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 <- getNthClause vec i+        let+          sweep k = do+            k' <- (indexMax .&.) <$> getNth keys k+            setNth keys k k+            if k' == i+              then setNthClause vec k c+              else getNthClause vec k' >>= setNthClause 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 <- getBool ok+  if good+    then do+      p <- propagate s+      if p /= NullClause+        then setBool ok False >> return False+        else do+            -- Clear watcher lists:+            n <- sizeOfStack trail+            let+              vec = asVec trail+              loopOnLit ((< n) -> False) = return ()+              loopOnLit i = do+                l <- getNth vec i+                clearManager . getNthWatcher watches $ l+                clearManager . 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' <- numberOfClauses ptr+                let+                  loopOnVector :: Int -> Int -> IO Bool+                  loopOnVector ((< n') -> False) j = shrinkManager ptr (n' - j) >> return True+                  loopOnVector i j = do+                        c <- getNthClause vec' i+                        l <- locked s c+                        r <- simplify s c+                        if not l && r+                          then removeWatch s c >> loopOnVector (i + 1) j+                          else setNthClause vec' j c >> loopOnVector (i + 1) (j + 1)+                loopOnVector 0 0+            ret <- for 0+            garbageCollect 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 LiftedBool+search s@Solver{..} nOfConflicts nOfLearnts = do+  -- clear model+  let+    loop :: Int -> IO LiftedBool+    loop conflictC = do+      !confl <- propagate s+      d <- decisionLevel s+      if confl /= NullClause+        then do+            -- CONFLICT+            incrementStat s NumOfBackjump 1+            r <- getInt 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 <- getDouble varDecay+--                    when (d < 0.95) $ modifyDouble varDecay (+ 0.01)+                  backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself+                  (s `cancelUntil`) . max backtrackLevel =<< getInt rootLevel+                  newLearntClause s $ asSizedVec litsLearnt+                  k <- sizeOfStack litsLearnt+                  when (k == 1) $ do+                    (v :: Var) <- lit2var <$> getNth (asVec 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 <- numberOfClauses learnts+            k2 <- nAssigns s+            when (k1 - k2 >= nOfLearnts) $ reduceDB s -- Reduce the set of learnt clauses+            case () of+             _ | k2 == nVars -> do+                   -- Model found:+                   forM_ [0 .. nVars - 1] $ \i -> setNthBool model i . (lTrue ==) =<< getNth assigns (i + 1)+                   return LTrue+             _ | conflictC >= nOfConflicts -> do+                   -- Reached bound on number of conflicts+                   (s `cancelUntil`) =<< getInt rootLevel -- force a restart+                   claRescaleActivityAfterRestart s+                   incrementStat s NumOfRestart 1+                   return Bottom+             _ -> 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 <- getBool 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.+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) <- getNthClause reason (lit2var a)+            analyzeFinal s confl True+            pushToStack conflict (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+        setInt 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 == Bottom+              then while (1.5 * nOfConflicts) (1.1 * nOfLearnts)+              else cancelUntil s 0 >> return (status == LTrue)+        while 100 (nc / 3.0)++--+-- '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+  setNthClause reason v from     -- NOTE: @from@ might be NULL!+  pushToStack trail p++-- __Pre-condition:__ propagation queue is empty+{-# INLINE unsafeAssume #-}+unsafeAssume :: Solver -> Lit -> IO ()+unsafeAssume s@Solver{..} p = do+  pushToStack trailLim =<< sizeOfStack trail+  unsafeEnqueue s p NullClause

@@ -0,0 +1,133 @@+{-# LANGUAGE BangPatterns #-}+{-# 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.Internal (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+                 }

@@ -0,0 +1,611 @@+{-# LANGUAGE+    BangPatterns+  , RecordWildCards+  , ScopedTypeVariables+  , TupleSections+  , ViewPatterns+  #-}+{-# LANGUAGE Safe #-}++-- | This is a part of MIOS; main data+module SAT.Mios.Solver+       (+         -- * Solver+         Solver (..)+       , newSolver+         -- * Misc Accessors+       , nAssigns+       , nClauses+       , nLearnts+       , decisionLevel+       , valueVar+       , valueLit+       , locked+         -- * State Modifiers+       , addClause+       , enqueue+       , assume+       , cancelUntil+       , getModel+         -- * Activities+       , claBumpActivity+--       , claDecayActivity+       , claRescaleActivityAfterRestart+       , varBumpActivity+       , varDecayActivity+       , claActivityThreshold+         -- * Stats+       , StatIndex (..)+       , getStat+       , setStat+       , incrementStat+       , getStats+       )+        where++import Control.Monad ((<=<), forM_, unless, when)+import SAT.Mios.Types+import SAT.Mios.Internal+import SAT.Mios.Clause+import SAT.Mios.ClauseManager++-- | __Fig. 2.(p.9)__ Internal State of the solver+data Solver = Solver+              {+                -- Public Interface+                model      :: !VecBool           -- ^ If found, this vector has the model+              , conflict   :: !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       -- ^ a list of constraint wathing 'p', literal-indexed+                -- Assignment Management+              , assigns    :: !Vec               -- ^ The current assignments indexed on variables; var-indexed+              , phases     :: !Vec               -- ^ The last assignments indexed on variables; var-indexed+              , trail      :: !Stack             -- ^ List of assignments in chronological order; var-indexed+              , trailLim   :: !Stack             -- ^ Separator indices for different decision levels in 'trail'.+              , qHead      :: !IntSingleton      -- ^ 'trail' is divided at qHead; assignments and queue+              , reason     :: !ClauseVector      -- ^ For each variable, the constraint that implied its value; var-indexed+              , level      :: !Vec               -- ^ For each variable, the decision level it was assigned; var-indexed+                -- Variable Order+              , activities :: !VecDouble         -- ^ Heuristic measurement of the activity of a variable; var-indexed+              , order      :: !VarHeap           -- ^ Keeps track of the dynamic variable order.+                -- Configuration+              , config     :: !MiosConfiguration -- ^ search paramerters+              , nVars      :: !Int               -- ^ number of variables+--            , claInc     :: !DoubleSingleton   -- ^ Clause activity increment amount to bump with.+--            , varDecay   :: !DoubleSingleton   -- ^ used to set 'varInc'+              , varInc     :: !DoubleSingleton   -- ^ Variable activity increment amount to bump with.+              , rootLevel  :: !IntSingleton      -- ^ Separates incremental and search assumptions.+                -- Working Memory+              , ok         :: !BoolSingleton     -- ^ return value holder+              , an'seen    :: !Vec               -- ^ scratch var for 'analyze'; var-indexed+              , an'toClear :: !Stack             -- ^ ditto+              , an'stack   :: !Stack             -- ^ ditto+              , pr'seen    :: !Vec               -- ^ used in propagate+              , litsLearnt :: !Stack             -- ^ used to create a learnt clause+              , lastDL     :: !Stack             -- ^ last decision level used in analyze+              , stats      :: !Vec               -- ^ statistics information holder+{-+              , lbd'seen   :: !Vec               -- ^ used in lbd computation+              , lbd'key    :: !IntSingleton      -- ^ 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+    <$> newVecBool nv False                           -- model+    <*> newStack nv                                   -- coflict+    -- Clause Database+    <*> newManager nc                                 -- clauses+    <*> newManager nc                                 -- learnts+    <*> newWatcherList nv 2                           -- watches+    -- Assignment Management+    <*> newVecWith (nv + 1) lBottom                   -- assigns+    <*> newVecWith (nv + 1) lBottom                   -- phases+    <*> newStack nv                                   -- trail+    <*> newStack nv                                   -- trailLim+    <*> newInt 0                                      -- qHead+    <*> newClauseVector (nv + 1)                      -- reason+    <*> newVecWith (nv + 1) (-1)                      -- level+    -- Variable Order+    <*> newVecDouble (nv + 1) 0                       -- activities+    <*> newVarHeap nv                                 -- order+    -- Configuration+    <*> return conf                                   -- config+    <*> return nv                                     -- nVars+--  <*> newDouble 1.0                                 -- claInc+--  <*> newDouble (variableDecayRate conf)            -- varDecay+    <*> newDouble 1.0                                 -- varInc+    <*> newInt 0                                      -- rootLevel+    -- Working Memory+    <*> newBool True                                  -- ok+    <*> newVec (nv + 1)                               -- an'seen+    <*> newStack nv                                   -- an'toClear+    <*> newStack nv                                   -- an'stack+    <*> newVecWith (nv + 1) (-1)                      -- pr'seen+    <*> newStack nv                                   -- litsLearnt+    <*> newStack nv                                   -- lastDL+    <*> newVec (1 + fromEnum (maxBound :: StatIndex)) -- stats+{-+--    <*> newVec nv                                     -- lbd'seen+--    <*> newInt 0                                      -- lbd'key+-}++--------------------------------------------------------------------------------+-- Accessors++-- | returns the number of current assigments+{-# INLINE nAssigns #-}+nAssigns :: Solver -> IO Int+nAssigns = sizeOfStack . trail++-- | returns the number of constraints (clauses)+{-# INLINE nClauses #-}+nClauses  :: Solver -> IO Int+nClauses = numberOfClauses . clauses++-- | returns the number of learnt clauses+{-# INLINE nLearnts #-}+nLearnts :: Solver -> IO Int+nLearnts = numberOfClauses . learnts++-- | return the model as a list of literal+getModel :: Solver -> IO [Int]+getModel s = zipWith (\n b -> if b then n else negate n) [1 .. ] <$> asList (model s)++-- | returns the current decision level+{-# INLINE decisionLevel #-}+decisionLevel :: Solver -> IO Int+decisionLevel = sizeOfStack . 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 -- FIXME: LiftedBool+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 ==) <$> (getNthClause (reason s) . lit2var =<< getNth (lits c) 1)++-------------------------------------------------------------------------------- Statistics++-- | stat index+data StatIndex =+    NumOfBackjump+  | NumOfRestart+  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 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 -> Vec -> IO Bool+addClause s@Solver{..} vecLits = do+  result <- clauseNew s vecLits False+  case result of+   (False, _) -> return False   -- Conflict occured+   (True, c)  -> do+     unless (c == NullClause) $ pushClause clauses c+     return True                -- No conflict++-- | __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.)+{-# INLINABLE clauseNew #-}+clauseNew :: Solver -> Vec -> Bool -> IO (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 -> setNth ps 0 0 >> return True -- p and negateLit p occurs in ps+             _ -> handle (j + 1) l n+      loopForLearnt :: Int -> IO Bool+      loopForLearnt i = do+        n <- getNth ps 0+        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 <- getNth ps 0+        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  -> setNth ps 0 0 >> 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 <- getNth ps 0+  case k of+   0 -> return (exit, NullClause)+   1 -> do+     l <- getNth ps 1+     (, NullClause) <$> enqueue s l NullClause+   _ -> do+     -- allocate clause:+     c <- newClauseFromVec isLearnt ps+     let vec = asVec 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+           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+       forM_ [0 .. k -1] $ varBumpActivity s . lit2var <=< getNth vec -- variables in conflict clauses are bumped+     -- 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 (True, 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 <- getInt (lbd from)+    k <- (12 +) <$> decisionLevel s+    when (k < l) $ setInt (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+        setNthClause reason v from     -- NOTE: @from@ might be NULL!+        pushToStack 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+  pushToStack (trailLim s) =<< sizeOfStack (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 = asVec trail+    let tl = asVec trailLim+    lim <- getNth tl lvl+    ts <- sizeOfStack trail+    ls <- sizeOfStack 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.+        setNthClause 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+    shrinkStack trail (ts - lim)+    shrinkStack trailLim (ls - lvl)+    setInt qHead =<< sizeOfStack 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++claActivityThreshold :: Double+claActivityThreshold = 1e20++-- | __Fig. 14 (p.19)__ Bumping of clause activity+{-# INLINE varBumpActivity #-}+varBumpActivity :: Solver -> Var -> IO ()+varBumpActivity s@Solver{..} x = do+  !a <- (+) <$> getNthDouble x activities <*> getDouble varInc+  setNthDouble x activities a+  when (varActivityThreshold < a) $ varRescaleActivity s+  update s x                    -- update the position in heap++-- | __Fig. 14 (p.19)__+{-# INLINE varDecayActivity #-}+varDecayActivity :: Solver -> IO ()+varDecayActivity Solver{..} = modifyDouble varInc (/ variableDecayRate config)+-- varDecayActivity Solver{..} = modifyDouble varInc . (flip (/)) =<< getDouble varDecay++-- | __Fig. 14 (p.19)__+{-# INLINE varRescaleActivity #-}+varRescaleActivity :: Solver -> IO ()+varRescaleActivity Solver{..} = do+  forM_ [1 .. nVars] $ \i -> modifyNthDouble i activities (/ varActivityThreshold)+  modifyDouble varInc (/ varActivityThreshold)++-- | __Fig. 14 (p.19)__+{-# INLINE claBumpActivity #-}+claBumpActivity :: Solver -> Clause -> IO ()+claBumpActivity s Clause{..} = do+  dl <- decisionLevel s+  a <- (fromIntegral dl +) <$> getDouble activity+  setDouble activity a+  -- setBool 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)__+{-# INLINE claRescaleActivity #-}+claRescaleActivity :: Solver -> IO ()+claRescaleActivity Solver{..} = do+  vec <- getClauseVector learnts+  n <- numberOfClauses learnts+  let+    loopOnVector :: Int -> IO ()+    loopOnVector ((< n) -> False) = return ()+    loopOnVector i = do+      c <- getNthClause vec i+      modifyDouble (activity c) (/ claActivityThreshold)+      loopOnVector $ i + 1+  loopOnVector 0+  -- modifyDouble claInc (/ claActivityThreshold)++-- | __Fig. 14 (p.19)__+{-# INLINE claRescaleActivityAfterRestart #-}+claRescaleActivityAfterRestart :: Solver -> IO ()+claRescaleActivityAfterRestart Solver{..} = do+  vec <- getClauseVector learnts+  n <- numberOfClauses learnts+  let+    loopOnVector :: Int -> IO ()+    loopOnVector ((< n) -> False) = return ()+    loopOnVector i = do+      c <- getNthClause vec i+      d <- sizeOfClause c+      if d < 9+        then modifyDouble (activity c) sqrt+        else setDouble (activity c) 0+      setBool (protected c) False+      loopOnVector $ i + 1+  loopOnVector 0++-------------------------------------------------------------------------------- VarHeap++-- | 'VarHeap' is 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 :: Vec -- order to var+                , idxs :: Vec -- var to order (index)+                }++newVarHeap :: Int -> IO VarHeap+newVarHeap n = do+  v1 <- newVec (n + 1)+  v2 <- newVec (n + 1)+  let+    loop :: Int -> IO ()+    loop ((<= n) -> False) = setNth v1 0 n >> setNth v2 0 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 (order -> heap -> h) = getNth h 0++{-# 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 <- getNthDouble v activities+  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 <- getNthDouble v' activities+            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 <- getNthDouble v activities+  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 <- getNthDouble l activities+            acR <- getNthDouble r activities+            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++{-# INLINE 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+  setNth to 0 n+  percolateUp s n++-- | renamed from 'getmin'+{-# INLINE 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

@@ -0,0 +1,269 @@+{-# LANGUAGE+    BangPatterns+  , FlexibleContexts+  , FlexibleInstances+  , FunctionalDependencies+  , MultiParamTypeClasses+  #-}+{-# LANGUAGE Trustworthy #-}++-- | Basic data types used throughout mios.+module SAT.Mios.Types+       (+         -- Singleton+         module SAT.Mios.Data.Singleton+         -- Fixed Unboxed Mutable Int Vector+       , module SAT.Mios.Data.Vec+         -- Abstract interfaces+       , VectorFamily (..)+         -- *  Variable+       , Var+       , bottomVar+       , int2var+         -- * Internal encoded Literal+       , Lit+       , lit2int+       , int2lit+       , bottomLit+       , newLit+       , positiveLit+       , lit2var+       , var2lit+       , negateLit+         -- * Assignment+       , LiftedBool (..)+       , lbool+       , lFalse+       , lTrue+       , lBottom+       , VarOrder (..)+         -- * CNF+       , CNFDescription (..)+       )+       where++import Control.Monad (forM)+import Data.Bits+import qualified Data.Vector.Unboxed.Mutable as UV+import SAT.Mios.Data.Singleton+import SAT.Mios.Data.Vec++-- | Public interface as /Container/+class VectorFamily s t | s -> t where+  -- * Size operations+  -- | erases all elements in it+  clear :: s -> IO ()+  clear = error "no default method for clear"+  -- * Debug+  -- | dump the contents+  dump :: Show t => String -> s -> IO String+  dump msg _ = error $ msg ++ ": no defalut method for dump"+  -- | get a raw data+  asVec :: s -> UV.IOVector Int+  asVec = error "asVector undefined"+  -- | converts into a list+  asList :: s -> IO [t]+  asList = error "asList undefined"+  {-# MINIMAL dump #-}++-- | provides 'clear' and 'size'+instance VectorFamily Vec Int where+  clear = error "Vec.clear"+  {-# SPECIALIZE INLINE asList :: Vec -> IO [Int] #-}+  asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v+  dump str v = (str ++) . show <$> asList v+  {-# SPECIALIZE INLINE asVec :: Vec -> Vec #-}+  asVec = id++-- | 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 = 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++-- | A contant representing False+lFalse:: Int+lFalse = -1++-- | A constant representing True+lTrue :: Int+lTrue = 1++-- | A constant for "undefined"+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 :: (VectorFamily v1 Bool, VectorFamily 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"++  -- | Called when variable has increased in activity.+  update :: o -> Var -> IO ()+  update _  = error "update undefined"++  -- | Called when all variables have been assigned new activities.+  updateAll :: o -> IO ()+  updateAll = error "updateAll undefined"++  -- | Called when variable is unbound (may be selected again).+  undo :: o -> Var -> IO ()+  undo _ _  = error "undo undefined"++  -- | Called to select a new, unassigned variable.+  select :: o -> IO Var+  select    = error "select undefined"++-- | misc information on CNF+data CNFDescription = CNFDescription+  {+    _numberOfVariables :: !Int           -- ^ number of variables+  , _numberOfClauses :: !Int             -- ^ number of clauses+  , _pathname :: Maybe FilePath          -- ^ given filename+  }+  deriving (Eq, Ord, Show)

@@ -0,0 +1,244 @@+{-# 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) ++ "} "

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

@@ -0,0 +1,73 @@+{-# LANGUAGE Safe #-}++-- | Read an output file of minisat+module SAT.Mios.Util.CNFIO.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 []

@@ -0,0 +1,130 @@+{-# LANGUAGE Safe #-}++-- | Read a CNF file without haskell-platform+module SAT.Mios.Util.CNFIO.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 []

@@ -0,0 +1,58 @@+{-# LANGUAGE Safe #-}++-- | Write SAT data to CNF file+module SAT.Mios.Util.CNFIO.Writer+       (+         -- * Interface+         toFile+       , toCNFString+       , toString+       , toLatexString+       )+       where+import Data.List (intercalate, nub, sort)+import System.IO++-- | Write the CNF to file 'f', using 'toCNFString'+toFile :: FilePath -> [[Int]] -> IO ()+toFile f l = writeFile f $ toCNFString l++-- | Convert [Clause] to String, where Clause is [Int]+--+-- >>> toCNFString []+-- "p cnf 0 0\n"+--+-- >>> toCNFString [[-1, 2], [-3, -4]]+-- "p cnf 4 2\n-1 2 0\n-3 -4 0\n"+--+-- >>> toCNFString [[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"+--+toCNFString :: [[Int]] -> String+toCNFString 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,48 @@+{-# 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+  vec <- getClauseVector (clauses s)+  nc <- numberOfClauses (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+      c <- getNthClause vec i+      sat' <- satAny =<< asList c+      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,298 +0,0 @@--- | Minisat-based Implementation and Optimization Study on SAT solver-{-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE Trustworthy #-}--module SAT.Solver.Mios-       (-         -- * Interface to the core of solver-         versionId-       , CNFDescription (..)-       , module SAT.Solver.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 qualified Data.Vector.Unboxed as U-import Numeric (showFFloat)-import System.CPUTime-import System.Exit-import System.IO--import SAT.Solver.Mios.Types-import SAT.Solver.Mios.Internal-import SAT.Solver.Mios.Solver-import SAT.Solver.Mios.M114-import SAT.Solver.Mios.OptionParser-import SAT.Solver.Mios.Validator--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 <- solve s []-  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`) <=< (newSizedVecIntFromList . map int2lit)) c-  noConf <- simplifyDB s-  if noConf-    then do-        x <- solve s []-        if x-            then Right <$> getModel s-            else Left .  map lit2int <$> asList (conflict 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`) <=< (newSizedVecIntFromList . 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`) <=< (newSizedVecIntFromList . 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 -> do-    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-  polvec <- newVecBool (maxLit + 1) False-  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 <- getNthBool polvec $ var2lit v True-      n <- getNthBool polvec $ var2lit v False-      when (p == False || n == False) $ setNth asg v $ if p then lTrue else lFalse-      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 -> Vec -> VecBool -> B.ByteString -> IO B.ByteString-readClause s buffer pvec 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-            addClause s buffer-            return b'-        else do-            let l = int2lit k-            setNth buffer i l-            setNthBool pvec l True-            loop (i + 1) b'-  loop 1 . skipComments . skipWhitespace $ stream---showPath :: FilePath -> String-showPath str-  | elem '/' str =  take (len - length basename) (repeat ' ') ++ basename-  |  otherwise = take (len - length basename') (repeat ' ') ++ basename'-  where-    len = 50-    basename = reverse . takeWhile (/= '/') . reverse $ str-    basename' = take len str

@@ -1,144 +0,0 @@--- | Clause, a data supporting pointer-based equality-{-# LANGUAGE-    BangPatterns-  , FlexibleInstances-  , MagicHash-  , MultiParamTypeClasses-  , RecordWildCards-  , ViewPatterns-  #-}-{-# LANGUAGE Trustworthy #-}--module SAT.Solver.Mios.Clause-       (-         Clause (..)---       , isLit---       , getLit-       , shrinkClause-       , newClauseFromVec-       , sizeOfClause-         -- * Vector of Clause-       , ClauseVector-       , newClauseVector-       , getNthClause-       , setNthClause-       , swapClauses-       )-       where--import Control.Monad (forM_)-import GHC.Prim (tagToEnum#, reallyUnsafePtrEquality#)-import qualified Data.Vector as V-import qualified Data.Vector.Mutable as MV-import qualified Data.Vector.Unboxed.Mutable as UV-import Data.List (intercalate)-import SAT.Solver.Mios.Types---- | __Fig. 7.(p.11)__--- clause, null, binary clause.--- This matches both of @Clause@ and @GClause@ in MiniSat--- TODO: GADTs is better?-data Clause = Clause-              {-                learnt     :: !Bool            -- ^ whether this is a learnt clause-              , activity   :: !DoubleSingleton -- ^ activity of this clause-              , protected  :: !BoolSingleton   -- ^ protected from reduce-              , lbd        :: !IntSingleton    -- ^ storing the LBD; values are computed in Solver-              , lits       :: !Vec             -- ^ which this clause consists of-              }---  | BinaryClause Lit                        -- binary clause consists of only a propagating literal-  | NullClause                              -- as null pointer---- | 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"---- | supports a restricted set of 'VectorFamily' methods-instance VectorFamily Clause Lit where-  dump mes NullClause = return $ mes ++ "Null"-  dump mes Clause{..} = do-    a <- show <$> getDouble activity-    (len:ls) <- asList lits-    return $ mes ++ "C" ++ show len ++ "{" ++ intercalate "," [show learnt, a, show . map lit2int . take len $ ls] ++ "}"-  {-# SPECIALIZE INLINE asVec :: Clause -> Vec #-}-  asVec Clause{..} = UV.unsafeTail lits-  {-# SPECIALIZE INLINE asList :: Clause -> IO [Int] #-}-  asList NullClause = return []-  asList Clause{..} = do-    (n : ls)  <- asList lits-    return $ take n ls---- 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"---- | drop the last /N/ literals in a 'Clause' to eliminate unsatisfied literals-{-# INLINABLE shrinkClause #-}-shrinkClause :: Int -> Clause -> IO ()-shrinkClause !n Clause{..} = setNth lits 0 . subtract n =<< getNth lits 0---- | copies /vec/ and return a new 'Clause'--- Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically.-{-# INLINE newClauseFromVec #-}-newClauseFromVec :: Bool -> Vec -> IO Clause-newClauseFromVec l vec = do-  n <- getNth vec 0-  v <- newVec $ n + 1-  forM_ [0 .. n] $ \i -> setNth v i =<< getNth vec i-  Clause l <$> newDouble 0 <*> newBool False <*> newInt n <*> return v---- | returns the number of literals in a clause, even if the given clause is a binary clause-{-# INLINE sizeOfClause #-}-sizeOfClause :: Clause -> IO Int--- sizeOfClause (BinaryClause _) = return 1-sizeOfClause !c = getNth (lits c) 0-------------------------------------------------------------------------------------- | Mutable 'Clause' Vector-type ClauseVector = MV.IOVector Clause--instance VectorFamily ClauseVector Clause where-  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---- | returns the nth 'Clause'-{-# INLINE getNthClause #-}-getNthClause :: ClauseVector -> Int -> IO Clause-getNthClause = MV.unsafeRead---- | sets the nth 'Clause'-{-# INLINE setNthClause #-}-setNthClause :: ClauseVector -> Int -> Clause -> IO ()-setNthClause = MV.unsafeWrite---- | swaps the two 'Clause's-{-# INLINE swapClauses #-}-swapClauses :: ClauseVector -> Int -> Int -> IO ()-swapClauses = MV.unsafeSwap

@@ -1,324 +0,0 @@--- | A shrinkable 'VectorFamily' of 'C.Clause'-{-# LANGUAGE-    BangPatterns-  , DuplicateRecordFields-  , FlexibleInstances-  , MultiParamTypeClasses-  , RecordWildCards-  , ViewPatterns-  #-}-{-# LANGUAGE Trustworthy #-}--module SAT.Solver.Mios.ClauseManager-       (-         -- * higher level interface for ClauseVector-         ClauseManager (..)---       -- * vector of clauses---       , SimpleManager-         -- * Manager with an extra Int (used as sort key or blocking literal)-       , ClauseExtManager-       , pushClauseWithKey-       , getKeyVector-       , markClause---       , purifyManager-         -- * WatcherList-       , WatcherList-       , newWatcherList-       , getNthWatcher-       , garbageCollect---       , numberOfRegisteredClauses-       )-       where--import Control.Monad (forM, unless, when)-import qualified Data.IORef as IORef-import qualified Data.List as L-import qualified Data.Vector as V-import qualified Data.Vector.Mutable as MV-import SAT.Solver.Mios.Types-import qualified SAT.Solver.Mios.Clause as C---- | resizable clause vector-class ClauseManager a where-  newManager      :: Int -> IO a-  numberOfClauses :: a -> IO Int-  clearManager    :: a -> IO ()-  shrinkManager   :: a -> Int -> IO ()-  getClauseVector :: a -> IO C.ClauseVector-  pushClause      :: a -> C.Clause -> IO ()---  removeClause    :: a -> C.Clause -> IO ()---  removeNthClause :: a -> Int -> IO ()--{---- | The Clause Container-data SimpleManager = SimpleManager-  {-    _nActives     :: IntSingleton               -- number of active clause-  , _clauseVector :: IORef.IORef C.ClauseVector -- clause list-  }--instance ClauseManager SimpleManager where-  {-# SPECIALIZE INLINE newManager :: Int -> IO SimpleManager #-}-  newManager initialSize = do-    i <- newInt 0-    v <- C.newClauseVector initialSize-    SimpleManager i <$> IORef.newIORef v-  {-# SPECIALIZE INLINE numberOfClauses :: SimpleManager -> IO Int #-}-  numberOfClauses SimpleManager{..} = getInt _nActives-  {-# SPECIALIZE INLINE clearManager :: SimpleManager -> IO () #-}-  clearManager SimpleManager{..} = setInt _nActives 0-  {-# SPECIALIZE INLINE shrinkManager :: SimpleManager -> Int -> IO () #-}-  shrinkManager SimpleManager{..} k = modifyInt _nActives (subtract k)-  {-# SPECIALIZE INLINE getClauseVector :: SimpleManager -> IO C.ClauseVector #-}-  getClauseVector SimpleManager{..} = IORef.readIORef _clauseVector-  -- | O(1) inserter-  {-# SPECIALIZE INLINE pushClause :: SimpleManager -> C.Clause -> IO () #-}-  pushClause !SimpleManager{..} !c = do-    !n <- getInt _nActives-    !v <- IORef.readIORef _clauseVector-    if MV.length v - 1 <= n-      then do-          v' <- MV.unsafeGrow v (max 8 (MV.length v))-          -- forM_ [n  .. MV.length v' - 1] $ \i -> MV.unsafeWrite v' i C.NullClause-          MV.unsafeWrite v' n c-          IORef.writeIORef _clauseVector v'-      else MV.unsafeWrite v n c-    modifyInt _nActives (1 +)-  -- | O(1) remove-and-compact function-  {-# SPECIALIZE INLINE removeNthClause :: SimpleManager -> Int -> IO () #-}-  removeNthClause SimpleManager{..} i = do-    !n <- subtract 1 <$> getInt _nActives-    !v <- IORef.readIORef _clauseVector-    MV.unsafeWrite v i =<< MV.unsafeRead v n-    setInt _nActives n-  -- | 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 :: SimpleManager -> C.Clause -> IO () #-}-  removeClause SimpleManager{..} c = do-    -- putStrLn =<< dump "@removeClause| remove " c-    -- putStrLn =<< dump "@removeClause| from " m-    !n <- subtract 1 <$> getInt _nActives-    -- unless (0 <= n) $ error $ "removeClause catches " ++ show n-    !v <- IORef.readIORef _clauseVector-    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-      setInt _nActives n--instance VectorFamily SimpleManager C.Clause where-  dump mes SimpleManager{..} = do-    n <- getInt _nActives-    if n == 0-      then return $ mes ++ "empty clausemanager"-      else do-          l <- take n <$> (asList =<< IORef.readIORef _clauseVector)-          sts <- mapM (dump ",") (l :: [C.Clause])-          return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts)--}-------------------------------------------------------------------------------------- | Clause + Blocking Literal-data ClauseExtManager = ClauseExtManager-  {-    _nActives     :: IntSingleton               -- number of active clause-  , _purged       :: BoolSingleton              -- whether it needs gc-  , _clauseVector :: IORef.IORef C.ClauseVector -- clause list-  , _keyVector    :: IORef.IORef Vec            -- Int list-  }--instance ClauseManager ClauseExtManager where-  {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-}-  newManager initialSize = do-    i <- newInt 0-    v <- C.newClauseVector initialSize-    b <- newVec (MV.length v)-    ClauseExtManager i <$> newBool False <*> IORef.newIORef v <*> IORef.newIORef b-  {-# SPECIALIZE INLINE numberOfClauses :: ClauseExtManager -> IO Int #-}-  numberOfClauses ClauseExtManager{..} = getInt _nActives-  {-# SPECIALIZE INLINE clearManager :: ClauseExtManager -> IO () #-}-  clearManager ClauseExtManager{..} = setInt _nActives 0-  {-# SPECIALIZE INLINE shrinkManager :: ClauseExtManager -> Int -> IO () #-}-  shrinkManager ClauseExtManager{..} k = modifyInt _nActives (subtract k)-  {-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-}-  getClauseVector ClauseExtManager{..} = IORef.readIORef _clauseVector-  -- | O(1) insertion function-  {-# SPECIALIZE INLINE pushClause :: ClauseExtManager -> C.Clause -> IO () #-}-  pushClause !ClauseExtManager{..} !c = do-    -- checkConsistency m c-    !n <- getInt _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' <- vecGrow 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-    modifyInt _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 <$> getInt _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-      setInt _nActives n-  removeNthClause = error "removeNthClause is not implemented on ClauseExtManager"--}---- | sets the expire flag to a clause-{-# INLINE markClause #-}-markClause :: ClauseExtManager -> C.Clause -> IO ()-markClause ClauseExtManager{..} c = do-  !n <- getInt _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-    setBool _purged True--{-# INLINE purifyManager #-}-purifyManager :: ClauseExtManager -> IO ()-purifyManager ClauseExtManager{..} = do-  diry <- getBool _purged-  when diry $ do-    n <- getInt _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 <- C.getNthClause vec i-        if c /= C.NullClause-          then do-              unless (i == j) $ do-                C.setNthClause vec j c-                setNth keys j =<< getNth keys i-              loop (i + 1) (j + 1)-          else loop (i + 1) j-    setInt _nActives =<< loop 0 0-    setBool _purged False---- | returns the associated Int vector-{-# INLINE getKeyVector #-}-getKeyVector :: ClauseExtManager -> IO Vec-getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector---- | O(1) inserter-{-# INLINE pushClauseWithKey #-}-pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO ()-pushClauseWithKey !ClauseExtManager{..} !c k = do-  -- checkConsistency m c-  !n <- getInt _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' <- vecGrow 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-  modifyInt _nActives (1 +)--instance VectorFamily ClauseExtManager C.Clause where-  dump mes ClauseExtManager{..} = do-    n <- getInt _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---- | 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 <$> forM [0 .. int2lit (negate n) + 1] (\_ -> newManager m)---- | returns the watcher List :: "ClauseManager" for "Literal" /l/-{-# INLINE getNthWatcher #-}-getNthWatcher :: WatcherList -> Lit-> ClauseExtManager-getNthWatcher = V.unsafeIndex--instance VectorFamily WatcherList C.Clause where-  dump mes wl = (mes ++) . L.concat <$> forM [1 .. V.length wl - 1] (\i -> dump ("\n" ++ show (lit2int i) ++ "' watchers:") (getNthWatcher wl i))---- | purges all expirable clauses in 'WatcherList'-{-# INLINE garbageCollect #-}-garbageCollect :: WatcherList -> IO ()-garbageCollect wm = V.mapM_ purifyManager wm--numberOfRegisteredClauses :: WatcherList -> IO Int-numberOfRegisteredClauses ws = sum <$> V.mapM numberOfClauses ws--{---------------------------------------------------------------------------------- debugging stuff--checkConsistency :: ClauseManager a => a -> C.Clause -> IO ()-checkConsistency manager c = do-  nc <- numberOfClauses manager-  vec <- getClauseVector manager-  let-    loop :: Int -> IO ()-    loop i = do-      when (i < nc) $ do-        c' <- MV.unsafeRead vec i-        when (c' == c) $ error "insert a clause to a ClauseMananger twice"-        loop $ i + 1-  loop 0--checkClauseOrder :: ClauseManager a => a -> IO ()-checkClauseOrder manager = do-  putStr "checking..."-  nc <- numberOfClauses manager-  vec <- getClauseVector manager-  let-    nthActivity :: Int -> IO Double-    nthActivity i = getDouble . C.activity =<< MV.unsafeRead vec i-    report :: Int -> Int -> IO ()-    report i j = (putStr . (++ ", ") . show =<< nthActivity i) >> when (i < j) (report (i + 1) j)-    loop :: Int -> Double -> IO ()-    loop i v = do-      when (i < nc) $ do-        c <- MV.unsafeRead vec i-        a <- getDouble (C.activity c)-        when (c == C.NullClause) $ error "null is included"-        when (v < a) $ report 0 i >> error ("unsorted clause vector: " ++ show (nc, i))-        loop (i + 1) a-  loop 0 =<< nthActivity 0-  putStrLn "done"--}

@@ -1,196 +0,0 @@--- | A fast(est) mutable data-{-# LANGUAGE-    BangPatterns-  #-}-{-# LANGUAGE Trustworthy #-}--module SAT.Solver.Mios.Data.Singleton-       (-         -- * Bool-         BoolSingleton-       , newBool-       , getBool-       , setBool-       , modifyBool-         -- * Int-       , IntSingleton-       , newInt-       , getInt-       , setInt-       , modifyInt-         -- * Double-       , DoubleSingleton-       , newDouble-       , getDouble-       , setDouble-       , modifyDouble-       )-       where-{--------------------------------------------- Implementation 1. :: IORef-------------------------------------------import Data.IORef--type BoolSingleton = IORef Bool--newBool :: Bool -> IO BoolSingleton-newBool = newIORef--{-# INLINE getBool #-}-getBool :: BoolSingleton -> IO Bool-getBool = readIORef--{-# INLINE setBool #-}-setBool :: BoolSingleton -> Bool -> IO ()-setBool = writeIORef--{-# INLINE modifyBool #-}-modifyBool :: BoolSingleton -> (Bool -> Bool) -> IO ()-modifyBool = modifyIORef'--type IntSingleton = IORef Int--newInt :: Int -> IO IntSingleton-newInt = newIORef--{-# INLINE getInt #-}-getInt :: IntSingleton -> IO Int-getInt = readIORef--{-# INLINE setInt #-}-setInt :: IntSingleton -> Int -> IO ()-setInt = writeIORef--{-# INLINE modifyInt #-}-modifyInt :: IntSingleton -> (Int -> Int) -> IO ()-modifyInt = modifyIORef'--type DoubleSingleton = IORef Double--newDouble :: Double -> IO DoubleSingleton-newDouble = newIORef--{-# INLINE getDouble #-}-getDouble :: DoubleSingleton -> IO Double-getDouble = readIORef--{-# INLINE setDouble #-}-setDouble :: DoubleSingleton -> Double -> IO ()-setDouble = writeIORef--{-# INLINE modifyDouble #-}-modifyDouble :: DoubleSingleton -> (Double -> Double) -> IO ()-modifyDouble = modifyIORef'--}-{--------------------------------------------- Implementation 2. :: Data.Mutable.IOURef-------------------------------------------import qualified Data.Mutable as M--newtype IntSingleton = IntSingleton-                       {-                         mutableInt :: M.IOURef Int-                       }--newInt :: IO IntSingleton-newInt = IntSingleton <$> M.newRef 0--{-# INLINE getInt #-}-getInt :: IntSingleton -> IO Int-getInt !(IntSingleton val) = M.readRef val--{-# INLINE setInt #-}-setInt :: IntSingleton -> Int -> IO ()-setInt !(IntSingleton val) !x = M.writeRef val x--{-# INLINE modifyInt #-}-modifyInt :: IntSingleton -> (Int -> Int) -> IO ()-modifyInt !(IntSingleton val) !f = M.modifyRef' val f--}---- {--------------------------------------------- Implementation 3. :: Data.Vector.Unboxed.Mutable-------------------------------------------import qualified Data.Vector.Unboxed.Mutable as UV---- | mutable Int-type IntSingleton = UV.IOVector Int---- | returns a new 'IntSingleton'-newInt :: Int -> IO IntSingleton-newInt k = do-  s <- UV.new 1-  UV.unsafeWrite s 0 k-  return s---- | returns the value-{-# INLINE getInt #-}-getInt :: IntSingleton -> IO Int-getInt val = UV.unsafeRead val 0---- | sets the value-{-# INLINE setInt #-}-setInt :: IntSingleton -> Int -> IO ()-setInt val !x = UV.unsafeWrite val 0 x---- | modifies the value-{-# INLINE modifyInt #-}-modifyInt :: IntSingleton -> (Int -> Int) -> IO ()-modifyInt val !f = UV.unsafeModify val f 0---- | mutable Bool-type BoolSingleton = UV.IOVector Bool---- | returns a new 'BoolSingleton'-newBool :: Bool -> IO BoolSingleton-newBool b = do-  s <- UV.new 1-  UV.unsafeWrite s 0 b-  return s---- | returns the value-{-# INLINE getBool #-}-getBool :: BoolSingleton -> IO Bool-getBool val = UV.unsafeRead val 0---- | sets the value-{-# INLINE setBool #-}-setBool :: BoolSingleton -> Bool -> IO ()-setBool val !x = UV.unsafeWrite val 0 x---- | modifies the value-{-# INLINE modifyBool #-}-modifyBool :: BoolSingleton -> (Bool -> Bool) -> IO ()-modifyBool val !f = UV.unsafeModify val f 0---- | mutable Double-type DoubleSingleton = UV.IOVector Double---- | returns a new 'DoubleSingleton'-newDouble :: Double -> IO DoubleSingleton-newDouble d = do-  s <- UV.new 1-  UV.unsafeWrite s 0 d-  return s---- | returns the value-{-# INLINE getDouble #-}-getDouble :: DoubleSingleton -> IO Double-getDouble val = UV.unsafeRead val 0---- | sets the value-{-# INLINE setDouble #-}-setDouble :: DoubleSingleton -> Double -> IO ()-setDouble val !x = UV.unsafeWrite val 0 x---- | modifies the value-{-# INLINE modifyDouble #-}-modifyDouble :: DoubleSingleton -> (Double -> Double) -> IO ()-modifyDouble val !f = UV.unsafeModify val f 0--- -}

@@ -1,93 +0,0 @@--- | stack of Int, by adding the length field as the zero-th element to a 'Vec'-{-# LANGUAGE-    BangPatterns-  , FlexibleInstances-  , MultiParamTypeClasses-  #-}-{-# LANGUAGE Trustworthy #-}--module SAT.Solver.Mios.Data.Stack-       (-         Stack-       , newStack-       , clearStack-       , sizeOfStack-       , pushToStack-       , popFromStack-       , lastOfStack-       , shrinkStack-       , asSizedVec-       , isoVec-       )-       where--import qualified Data.Vector.Unboxed.Mutable as UV-import SAT.Solver.Mios.Types---- | Unboxed mutable stack for Int.-newtype Stack = Stack-                  {-                    ivec :: UV.IOVector Int-                  }--instance VectorFamily Stack Int where-  dump str v = (str ++) . show <$> asList v-  {-# SPECIALIZE INLINE asVec :: Stack -> Vec #-}-  asVec (Stack v) = UV.unsafeTail v-  asList (Stack v) = do-    (n : l) <- asList v-    return $ take n l---- | returns the number of elements-{-# INLINE sizeOfStack #-}-sizeOfStack :: Stack -> IO Int-sizeOfStack (Stack v) = UV.unsafeRead v 0---- | clear stack-{-# INLINE clearStack #-}-clearStack :: Stack -> IO ()-clearStack (Stack v) = UV.unsafeWrite v 0 0---- | returns a new stack which size is @size@-{-# INLINABLE newStack #-}-newStack :: Int -> IO Stack-newStack n = do-  v <- UV.new $ n + 1-  UV.set v 0-  return $ Stack v---- | pushs an int to 'Stack'-{-# INLINE pushToStack #-}-pushToStack :: Stack -> Int -> IO ()-pushToStack (Stack v) !x = do-  !i <- (+ 1) <$> UV.unsafeRead v 0-  UV.unsafeWrite v i x-  UV.unsafeWrite v 0 i---- | drops the first element from 'Stack'-{-# INLINE popFromStack #-}-popFromStack :: Stack -> IO ()-popFromStack (Stack v) = UV.unsafeModify v (subtract 1) 0---- | peeks the last element in 'Stack'-{-# INLINE lastOfStack #-}-lastOfStack :: Stack -> IO Int-lastOfStack (Stack v) = UV.unsafeRead v =<< UV.unsafeRead v 0---- | Shrink the stack. The given arg means the number of discards.--- therefore, shrink s n == for [1 .. n] $ \_ -> pop s-{-# INLINE shrinkStack #-}-shrinkStack :: Stack -> Int -> IO ()-shrinkStack (Stack v) k = UV.unsafeModify v (subtract k) 0---- | converts Stack to sized Vec; this is the method to get the internal vector-{-# INLINE asSizedVec #-}-asSizedVec :: Stack -> Vec-asSizedVec (Stack v) = v---- | isomorphic conversion to 'Vec'------ Note: 'asVec' drops the 1st element and no copy (unsafe operation); 'isoVec' really copies the real elements-{-# INLINE isoVec #-}-isoVec :: Stack -> IO Vec-isoVec (Stack v) = UV.clone . flip UV.take v . (1 +) =<< UV.unsafeRead v 0

@@ -1,86 +0,0 @@--- | The fundamental data structure: Fixed Mutable Unboxed Int Vector-{-# LANGUAGE-    BangPatterns-  #-}-{-# LANGUAGE Trustworthy #-}--module SAT.Solver.Mios.Data.Vec-       (-         Vec-       , sizeOfVector-       , getNth-       , setNth-       , swapBetween-       , modifyNth-       , setAll-       , newVec-       , newVecWith-       , newSizedVecIntFromList-       , newSizedVecIntFromUVector-       , vecGrow-       )-       where--import qualified Data.Vector.Unboxed as U-import qualified Data.Vector.Unboxed.Mutable as UV---- | Costs of all operations are /O/(/1/)-type Vec = UV.IOVector Int---- | returns the size of 'Vec'-{-# INLINE sizeOfVector #-}-sizeOfVector :: Vec -> IO Int-sizeOfVector v = return $! UV.length v---- | returns a new 'Vec'-{-# INLINE newVec #-}-newVec :: Int -> IO Vec-newVec = UV.new---- | returns a new 'Vec' filled with an Int-{-# INLINE newVecWith #-}-newVecWith :: Int -> Int -> IO Vec-newVecWith n x = do-  v <- UV.new n-  UV.set v x-  return v---- | gets the nth value-{-# INLINE getNth #-}-getNth :: Vec -> Int -> IO Int-getNth = UV.unsafeRead---- | sets the nth value-{-# INLINE setNth #-}-setNth :: Vec -> Int -> Int -> IO ()-setNth = UV.unsafeWrite---- | modify the nth value-{-# INLINE modifyNth #-}-modifyNth :: Vec -> (Int -> Int) -> Int -> IO ()-modifyNth = UV.unsafeModify---- | sets all elements-{-# INLINE setAll #-}-setAll :: Vec -> Int -> IO ()-setAll = UV.set---- | swaps two elements-{-# INLINE swapBetween #-}-swapBetween:: Vec -> Int -> Int -> IO ()-swapBetween = UV.unsafeSwap---- | returns a new 'Vec' from a @[Int]@-{-# INLINE newSizedVecIntFromList #-}-newSizedVecIntFromList :: [Int] -> IO Vec-newSizedVecIntFromList !l = U.unsafeThaw $ U.fromList (length l : l)---- | returns a new 'Vec' from a Unboxed Int Vector-{-# INLINE newSizedVecIntFromUVector #-}-newSizedVecIntFromUVector :: U.Vector Int -> IO Vec-newSizedVecIntFromUVector = U.unsafeThaw---- | calls @unasfeGrow@-{-# INLINE vecGrow #-}-vecGrow :: Vec -> Int -> IO Vec-vecGrow = UV.unsafeGrow

@@ -1,55 +0,0 @@--- | Mutable Unboxed Boolean Vector------ * __VecBool@::UV.IOVector Bool@ -- data type that contains a mutable list of elements----{-# LANGUAGE-    BangPatterns-  , FlexibleInstances-  , MultiParamTypeClasses-  #-}-{-# LANGUAGE Trustworthy #-}--module SAT.Solver.Mios.Data.VecBool-       (-         VecBool-       , newVecBool-       , getNthBool-       , setNthBool-       , modifyNthBool-       )-       where--import Control.Monad (forM)-import qualified Data.Vector.Unboxed.Mutable as UV-import SAT.Solver.Mios.Types (VectorFamily(..))---- | Mutable unboxed Bool Vector-type VecBool = UV.IOVector Bool---- | provides 'clear' and 'size'-instance VectorFamily VecBool Bool where-  clear _ = error "VecBool.clear"-  asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v-  dump str v = (str ++) . show <$> asList v---- | returns a new 'VecBool'-newVecBool :: Int -> Bool -> IO VecBool-newVecBool n x = do-  v <- UV.new n-  UV.set v x-  return v---- | returns the nth value in 'VecBool'-{-# INLINE getNthBool #-}-getNthBool :: VecBool -> Int -> IO Bool-getNthBool = UV.unsafeRead---- | sets the nth value-{-# INLINE setNthBool #-}-setNthBool :: VecBool -> Int -> Bool -> IO ()-setNthBool = UV.unsafeWrite---- | sets the nth value-{-# INLINE modifyNthBool #-}-modifyNthBool :: VecBool -> (Bool -> Bool) -> Int -> IO ()-modifyNthBool = UV.unsafeModify

@@ -1,53 +0,0 @@--- | Mutable Unboxed Double Vector-{-# LANGUAGE-    BangPatterns-  , FlexibleInstances-  , MultiParamTypeClasses-  #-}-{-# LANGUAGE Trustworthy #-}--module SAT.Solver.Mios.Data.VecDouble-       (-         VecDouble-       , newVecDouble-       , getNthDouble-       , setNthDouble-       , modifyNthDouble-       )-       where--import Control.Monad (forM)-import Data.List ()-import qualified Data.Vector.Unboxed.Mutable as UV-import SAT.Solver.Mios.Types (VectorFamily(..))---- | Mutable unboxed Double Vector-type VecDouble = UV.IOVector Double--instance VectorFamily VecDouble Double where-  clear _ = error "VecDouble.clear"-  asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v-  dump str v = (str ++) . show <$> asList v---- | returns a new 'VecDouble'-newVecDouble :: Int -> Double -> IO VecDouble-newVecDouble n 0 = UV.new n-newVecDouble n x = do-  v <- UV.new n-  UV.set v x-  return v---- | returns the nth value in 'VecDouble'-{-# INLINE getNthDouble #-}-getNthDouble :: Int -> VecDouble -> IO Double-getNthDouble !n v = UV.unsafeRead v n---- | sets the nth value-{-# INLINE setNthDouble #-}-setNthDouble :: Int -> VecDouble -> Double -> IO ()-setNthDouble !n v !x = UV.unsafeWrite v n x---- | updates the nth value-{-# INLINE modifyNthDouble #-}-modifyNthDouble :: Int -> VecDouble -> (Double -> Double) -> IO ()-modifyNthDouble !n v !f = UV.unsafeModify v f n

@@ -1,72 +0,0 @@--- | This is a part of MIOS-{-# LANGUAGE-    BangPatterns-  , RecordWildCards-  , ScopedTypeVariables-  , ViewPatterns-  #-}-{-# LANGUAGE Safe #-}--module SAT.Solver.Mios.Glucose-       (-         computeLBD-       , lbdOf-       , setLBD-       , updateLBD-       , nextReduction-       )-        where--import Control.Monad (when)-import SAT.Solver.Mios.Types-import SAT.Solver.Mios.Clause-import SAT.Solver.Mios.Solver---- | returns the LBD vaule for 'Vec[1 ..]'-computeLBD :: Solver -> Vec -> IO Int-computeLBD Solver{..} vec = do-  key <- (1 +) <$> getInt lbd'key-  setInt lbd'key key-  nv <- getNth vec 0-  let-    loop :: Int -> Int -> IO Int-    loop ((<= nv) -> False) n = return n-    loop !i !n = do-      l <- getNth level . lit2var =<< getNth vec i-      seen <- if l == 0 then return True else (key ==) <$> getNth lbd'seen l-      if seen-        then loop (i + 1) n-        else setNth lbd'seen l key >> loop (i + 1) (n + 1)-  loop 1 0---- | returns the LBD value of 'Clause'-{-# INLINE lbdOf #-}-lbdOf :: Solver -> Clause -> IO Int-lbdOf s (lits -> v) = computeLBD s v---- | update the LBD field in 'Clause'-{-# INLINE setLBD #-}-setLBD :: Solver -> Clause -> IO ()-setLBD s c = setInt (lbd c) =<< lbdOf s c---- | update the lbd field of /c/-{-# INLINE updateLBD #-}-updateLBD :: Solver -> Clause -> IO ()-updateLBD _ NullClause = error "LBD71"-updateLBD _ (learnt -> False) = return ()-updateLBD s c@Clause{..} = setInt lbd =<< lbdOf s c---- | 0 based------ >>> nextReduction 0--- 20000--- >>> nextReduction 1--- 40000 + 200 = 20000 + 20000 + 200--- >>> nextReduction 2--- 6000 + 600 = 20000 + 20200 + 20000 + 400--- >>> nextReduction 3--- 80000 + 1200 = 20000 + 20200 + 20400 + 20000 + 600----nextReduction :: Int -> Int -> Int--- nextReduction _ n = 30000 + 10000 * n-nextReduction b n = b + 300 * n

@@ -1,34 +0,0 @@--- | Internal Settings-module SAT.Solver.Mios.Internal-       (-         versionId-       , MiosConfiguration (..)-       , defaultConfiguration-       , module Plumbing-       )-       where-import SAT.Solver.Mios.Data.VecBool as Plumbing-import SAT.Solver.Mios.Data.VecDouble as Plumbing-import SAT.Solver.Mios.Data.Stack as Plumbing---- | version name-versionId :: String-versionId = "mios 1.2 <https://github.com/shnarazk/mios/>" -- blocking literal + lbd + phase-saving---- | 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-                         , collectStats       :: Bool    -- ^ whether collect and report statistics-                         }---- | 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 -} False

@@ -1,816 +0,0 @@--- | This is a part of MIOS-{-# LANGUAGE-    BangPatterns-  , RecordWildCards-  , ScopedTypeVariables-  , ViewPatterns-  #-}-{-# LANGUAGE Safe #-}--module SAT.Solver.Mios.M114-       (-         simplifyDB-       , solve-       )-        where--import Control.Monad (forM_, unless, void, when)-import Data.Bits-import Data.Foldable (foldrM)-import SAT.Solver.Mios.Types-import SAT.Solver.Mios.Internal-import SAT.Solver.Mios.Clause-import SAT.Solver.Mios.ClauseManager-import SAT.Solver.Mios.Solver-import SAT.Solver.Mios.Glucose---- | #114: __RemoveWatch__-{-# INLINABLE removeWatch #-}-removeWatch :: Solver -> Clause -> IO ()-removeWatch Solver{..} c = do-  let lvec = asVec c-  l1 <- negateLit <$> getNth lvec 0-  markClause (getNthWatcher watches l1) c-  l2 <- negateLit <$> getNth lvec 1-  markClause (getNthWatcher watches l2) c------------------------------------------------------------------------------------- Operations on 'Clause'------------------------------------------------------------------------------------- | __Fig. 8. (p.12)__ create a new LEARNT clause and adds it to watcher lists--- This is a strippped-down version of 'newClause' in Solver-{-# INLINABLE newLearntClause #-}-newLearntClause :: Solver -> Vec -> IO ()-newLearntClause s@Solver{..} ps = do-  good <- getBool 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 <- getNth ps 0-    case k of-     1 -> do-       l <- getNth ps 1-       unsafeEnqueue s l NullClause-     _ -> do-       -- allocate clause:-       c <- newClauseFromVec True ps-       let vec = asVec 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:-       claBumpActivity s c -- newly learnt clauses should be considered active-       -- Add clause to all managers-       pushClause 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-       setLBD s c---- | __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 <- sizeOfClause c-  let-    lvec = asVec 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@--- {-# INLINEABLE analyze #-}-analyze :: Solver -> Clause -> IO Int-analyze s@Solver{..} confl = do-  -- litvec-  clearStack litsLearnt-  pushToStack litsLearnt 0 -- reserve the first place for the unassigned literal-  dl <- decisionLevel s-  let-    litsVec = asVec litsLearnt-    trailVec = asVec 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 <- getInt (lbd c)-        when (2 < d) $ do-          nblevels <- lbdOf s c-          when (nblevels + 1 < d) $ do -- improve the LBD-            when (d <= 30) $ setBool (protected c) True -- 30 is `lbLBDFrozenClause`-            -- seems to be interesting: keep it fro the next round-            setInt (lbd c) nblevels    -- Update it-      sc <- sizeOfClause c-      let-        lvec = asVec 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 <- getNthClause reason v-                      when (r /= NullClause && learnt r) $ pushToStack lastDL q-                      -- end of glucose heuristics-                      loopOnLiterals (j + 1) b (pc + 1)-                  else pushToStack 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' <- getNthClause 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 <$> sizeOfStack trail-  levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0-  -- Simplify phase (implemented only @expensive_ccmin@ path)-  n <- sizeOfStack litsLearnt-  clearStack an'stack           -- analyze_stack.clear();-  clearStack an'toClear         -- out_learnt.copyTo(analyze_toclear);-  pushToStack 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-      pushToStack 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' = shrinkStack litsLearnt $ n - n'-    loopOnLits i j = do-      l <- getNth litsVec i-      c1 <- (NullClause ==) <$> getNthClause 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 <- sizeOfStack lastDL-  lbd' <- computeLBD s $ asSizedVec litsLearnt -- this is not the right value-  let-    vec = asVec lastDL-    loopOnLastDL :: Int -> IO ()-    loopOnLastDL ((< nld) -> False) = return ()-    loopOnLastDL i = do-      v <- lit2var <$> getNth vec i-      d' <- getInt . lbd =<< getNthClause reason v-      when (lbd' < d') $ varBumpActivity s v-      loopOnLastDL $ i + 1-  loopOnLastDL 0-  clearStack lastDL-  -- Clear seen-  k <- sizeOfStack an'toClear-  let-    vec' = asVec 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@.----{-# INLINEABLE analyzeRemovable #-}-analyzeRemovable :: Solver -> Lit -> Int -> IO Bool-analyzeRemovable Solver{..} p minLevel = do-  -- assert (reason[var(p)]!= NullCaulse);-  clearStack an'stack      -- analyze_stack.clear()-  pushToStack an'stack p   -- analyze_stack.push(p);-  top <- sizeOfStack an'toClear-  let-    loopOnStack :: IO Bool-    loopOnStack = do-      k <- sizeOfStack an'stack  -- int top = analyze_toclear.size();-      if 0 == k-        then return True-        else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL);-            sl <- lastOfStack an'stack-            popFromStack an'stack             -- analyze_stack.pop();-            c <- getNthClause reason (lit2var sl) -- getRoot sl-            nl <- sizeOfClause c-            let-              cvec = asVec 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 /=) <$> getNthClause 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;-                            pushToStack an'stack p'    -- analyze_stack.push(p);-                            pushToStack 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' <- sizeOfStack an'toClear-                            let vec = asVec an'toClear-                            forM_ [top .. top' - 1] $ \j -> do x <- getNth vec j; setNth an'seen (lit2var x) 0-                            -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop-                            shrinkStack 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).----analyzeFinal :: Solver -> Clause -> Bool -> IO ()-analyzeFinal Solver{..} confl skipFirst = do-  clearStack conflict-  rl <- getInt rootLevel-  unless (rl == 0) $ do-    n <- sizeOfClause confl-    let-      lvec = asVec 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 <- sizeOfStack trailLim-    trs <- sizeOfStack trail-    tlz <- getNth (asVec trailLim) 0-    let-      trailVec = asVec 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) <- getNthClause reason x-          if r == NullClause-            then pushToStack conflict (negateLit l)-            else do-                k <- sizeOfClause r-                let-                  cvec = asVec 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 (asVec trailLim) rl---- | M114:--- propagate : [void] -> [Clause+]------ __Description:__---   Porpagates all enqueued facts. If a conflict arises, the cornflicting 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 = asVec trail-    while :: Clause -> Bool -> IO Clause-    while confl False = {- bumpAllVar >> -} return confl-    while confl True = do-      (p :: Lit) <- getNth trailVec =<< getInt qHead-      modifyInt qHead (+ 1)-      let (ws :: ClauseExtManager) = getNthWatcher watches p-      end <- numberOfClauses ws-      cvec <- getClauseVector ws-      bvec <- getKeyVector ws---      rc <- getNthClause reason $ lit2var p---      byGlue <- if (rc /= NullClause) && learnt rc then (== 2) <$> getInt (lbd rc) else return False-      let-{--        checkAllLiteralsIn :: Clause -> IO () -- not in use-        checkAllLiteralsIn c = do-          nc <- sizeOfClause c-          let-            vec = asVec 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-          shrinkManager ws (i - j)-          while confl =<< ((<) <$> getInt qHead <*> sizeOfStack 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) <- getNthClause cvec i-                   setNthClause cvec j c-                   setNth bvec j l-                 forClause confl (i + 1) (j + 1)-            else do-                -- checkAllLiteralsIn c-                (c :: Clause) <- getNthClause cvec i-                let-                  lits = asVec 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 setNthClause cvec j c >> setNth bvec j first >> forClause confl (i + 1) (j + 1)-                  else do-                      -- Look for new watch-                      cs <- sizeOfClause c-                      let-                        forLit :: Int -> IO Clause-                        forLit ((< cs) -> False) = do-                          -- Did not find watch; clause is unit under assignment:-                          setNthClause cvec j c-                          setNth bvec j 0-                          result <- enqueue s first c-                          if not result-                            then do-                                ((== 0) <$> decisionLevel s) >>= (`when` setBool ok False)-                                setInt qHead =<< sizeOfStack trail-                                -- Copy the remaining watches:-                                let-                                  copy i'@((< end) -> False) j' = forClause c i' j'-                                  copy i' j' = do-                                    setNthClause cvec j' =<< getNthClause 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 =<< ((<) <$> getInt qHead <*> sizeOfStack 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 =<< getNthClause 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-  garbageCollect watches-  shrinkManager 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 lbd--- 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----(lbdWidth :: Int, activityWidth :: Int, indexWidth :: Int) = (l, a, w - (l + a + 1))-  where-    w = finiteBitSize (0:: Int)-    (l, a) = case () of-      _ | 64 <= w -> (16, 19)   -- 28 bit => 256M clauses-      _ | 60 <= w -> (14, 19)   -- 26 bit =>  32M clauses-      _ | 32 <= w -> ( 7,  6)   -- 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-    lbdMax :: Int-    lbdMax = 2 ^ lbdWidth - 1-    activityMax :: Int-    activityMax = 2 ^ activityWidth - 1-    activityScale :: Double-    activityScale = fromIntegral activityMax-    indexMax :: Int-    indexMax = (2 ^ indexWidth - 1) -- 67,108,863 for 26-  n <- numberOfClauses 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 <- getNthClause vec i-      k <- (\k -> if k == 2 then return k else fromEnum <$> getBool (protected c)) =<< sizeOfClause c-      case k of-        1 -> setBool (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 <- getInt $ lbd c-                  b <- floor . (activityScale *) . (1 -) . logBase 1e100 . max 1 <$> getDouble (activity c)-                  setNth keys i $ shiftL (min lbdMax 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@((left <=) -> False) = return i-            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 <- getNthClause vec i-        let-          sweep k = do-            k' <- (indexMax .&.) <$> getNth keys k-            setNth keys k k-            if k' == i-              then setNthClause vec k c-              else getNthClause vec k' >>= setNthClause 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 <- getBool ok-  if good-    then do-      p <- propagate s-      if p /= NullClause-        then setBool ok False >> return False-        else do-            -- Clear watcher lists:-            n <- sizeOfStack trail-            let-              vec = asVec trail-              loopOnLit ((< n) -> False) = return ()-              loopOnLit i = do-                l <- getNth vec i-                clearManager . getNthWatcher watches $ l-                clearManager . 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' <- numberOfClauses ptr-                let-                  loopOnVector :: Int -> Int -> IO Bool-                  loopOnVector ((< n') -> False) j = shrinkManager ptr (n' - j) >> return True-                  loopOnVector i j = do-                        c <- getNthClause vec' i-                        l <- locked s c-                        r <- simplify s c-                        if not l && r-                          then removeWatch s c >> loopOnVector (i + 1) j-                          else setNthClause vec' j c >> loopOnVector (i + 1) (j + 1)-                loopOnVector 0 0-            ret <- for 0-            garbageCollect 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 LiftedBool-search s@Solver{..} nOfConflicts nOfLearnts = do-  -- clear model-  let-    loop :: Int -> IO LiftedBool-    loop conflictC = do-      !confl <- propagate s-      d <- decisionLevel s-      if confl /= NullClause-        then do-            -- CONFLICT-            incrementStat s NumOfBackjump 1-            r <- getInt 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 <- getDouble varDecay---                    when (d < 0.95) $ modifyDouble varDecay (+ 0.01)-                  backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself-                  (s `cancelUntil`) . max backtrackLevel =<< getInt rootLevel-                  newLearntClause s $ asSizedVec litsLearnt-                  k <- sizeOfStack litsLearnt-                  when (k == 1) $ do-                    (v :: Var) <- lit2var <$> getNth (asVec 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 <- numberOfClauses learnts-            k2 <- nAssigns s-            when (k1 - k2 >= nOfLearnts) $ reduceDB s -- Reduce the set of learnt clauses-            case () of-             _ | k2 == nVars -> do-                   -- Model found:-                   forM_ [0 .. nVars - 1] $ \i -> setNthBool model i . (lTrue ==) =<< getNth assigns (i + 1)-                   return LTrue-             _ | conflictC >= nOfConflicts -> do-                   -- Reached bound on number of conflicts-                   (s `cancelUntil`) =<< getInt rootLevel -- force a restart-                   incrementStat s NumOfRestart 1-                   return Bottom-             _ -> 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 <- getBool 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.-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) <- getNthClause reason (lit2var a)-            analyzeFinal s confl True-            pushToStack conflict (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-        setInt 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 == Bottom-              then while (1.5 * nOfConflicts) (1.1 * nOfLearnts)-              else cancelUntil s 0 >> return (status == LTrue)-        while 100 (nc / 3.0)-------- 'enqueue' is defined in 'Solver'; 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-  setNthClause reason v from     -- NOTE: @from@ might be NULL!-  pushToStack trail p---- __Pre-condition:__ propagation queue is empty-{-# INLINE unsafeAssume #-}-unsafeAssume :: Solver -> Lit -> IO ()-unsafeAssume s@Solver{..} p = do-  pushToStack trailLim =<< sizeOfStack trail-  unsafeEnqueue s p NullClause--{---- | for debug-fromAssigns :: Vec -> IO [Int]-fromAssigns as = zipWith f [1 .. ] . tail <$> asList as-  where-    f n x-      | x == lTrue = n-      | x == lFalse = negate n-      | otherwise = 0---- | for debug-dumpAssignment :: String -> Vec -> IO String-dumpAssignment mes v = (mes ++) . show <$> fromAssigns v--}

@@ -1,132 +0,0 @@-{-# LANGUAGE Safe #-}--- | command line option parser for mios-module SAT.Solver.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.Solver.Mios.Internal (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 = collectStats defaultConfiguration-  , _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-                 , collectStats = _confStatProbe opts-                 }

@@ -1,554 +0,0 @@--- | This is a part of MIOS-{-# LANGUAGE-    BangPatterns-  , RecordWildCards-  , ScopedTypeVariables-  , TupleSections-  , ViewPatterns-  #-}-{-# LANGUAGE Safe #-}--module SAT.Solver.Mios.Solver-       (-         -- * Solver-         Solver (..)-       , newSolver-         -- * Misc Accessors-       , nAssigns-       , nClauses-       , nLearnts-       , decisionLevel-       , valueVar-       , valueLit-       , locked-       , VarHeap-         -- * State Modifiers-       , addClause-       , enqueue-       , assume-       , cancelUntil-       , getModel-         -- * Activities-       , claBumpActivity-       , claDecayActivity-       , varBumpActivity-       , varDecayActivity-         -- * Stats-       , StatIndex (..)-       , incrementStat-       , getStats-       )-        where--import Control.Monad ((<=<), forM_, unless, when)-import SAT.Solver.Mios.Types-import SAT.Solver.Mios.Internal-import SAT.Solver.Mios.Clause-import SAT.Solver.Mios.ClauseManager---- | __Fig. 2.(p.9)__ Internal State of the solver-data Solver = Solver-              {-                -- Public Interface-                model      :: !VecBool           -- ^ If found, this vector has the model-              , conflict   :: !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       -- ^ a list of constraint wathing 'p', literal-indexed-                -- Assignment Management-              , assigns    :: !Vec               -- ^ The current assignments indexed on variables; var-indexed-              , phases     :: !Vec               -- ^ The last assignments indexed on variables; var-indexed-              , trail      :: !Stack             -- ^ List of assignments in chronological order; var-indexed-              , trailLim   :: !Stack             -- ^ Separator indices for different decision levels in 'trail'.-              , qHead      :: !IntSingleton      -- ^ 'trail' is divided at qHead; assignments and queue-              , reason     :: !ClauseVector      -- ^ For each variable, the constraint that implied its value; var-indexed-              , level      :: !Vec               -- ^ For each variable, the decision level it was assigned; var-indexed-                -- Variable Order-              , activities :: !VecDouble         -- ^ Heuristic measurement of the activity of a variable; var-indexed-              , order      :: !VarHeap           -- ^ Keeps track of the dynamic variable order.-                -- Configuration-              , config     :: !MiosConfiguration -- ^ search paramerters-              , nVars      :: !Int               -- ^ number of variables-              , claInc     :: !DoubleSingleton   -- ^ Clause activity increment amount to bump with.---            , varDecay   :: !DoubleSingleton   -- ^ used to set 'varInc'-              , varInc     :: !DoubleSingleton   -- ^ Variable activity increment amount to bump with.-              , rootLevel  :: !IntSingleton      -- ^ Separates incremental and search assumptions.-                -- Working Memory-              , ok         :: !BoolSingleton     -- ^ return value holder-              , an'seen    :: !Vec               -- ^ scratch var for 'analyze'; var-indexed-              , an'toClear :: !Stack             -- ^ ditto-              , an'stack   :: !Stack             -- ^ ditto-              , pr'seen    :: !Vec               -- ^ used in propagate-              , lbd'seen   :: !Vec               -- ^ used in lbd computation-              , lbd'key    :: !IntSingleton      -- ^ used in lbd computation-              , litsLearnt :: !Stack             -- ^ used to create a learnt clause-              , lastDL     :: !Stack             -- ^ last decision level used in analyze-              , stats      :: !Vec               -- ^ statistics information holder-              }---- | returns an everything-is-initialized solver from the arguments-newSolver :: MiosConfiguration -> CNFDescription -> IO Solver-newSolver conf (CNFDescription nv nc _) = do-  Solver-    -- Public Interface-    <$> newVecBool nv False                           -- model-    <*> newStack nv                                   -- coflict-    -- Clause Database-    <*> newManager nc                                 -- clauses-    <*> newManager nc                                 -- learnts-    <*> newWatcherList nv 2                           -- watches-    -- Assignment Management-    <*> newVecWith (nv + 1) lBottom                   -- assigns-    <*> newVecWith (nv + 1) lBottom                   -- phases-    <*> newStack nv                                   -- trail-    <*> newStack nv                                   -- trailLim-    <*> newInt 0                                      -- qHead-    <*> newClauseVector (nv + 1)                      -- reason-    <*> newVecWith (nv + 1) (-1)                      -- level-    -- Variable Order-    <*> newVecDouble (nv + 1) 0                       -- activities-    <*> newVarHeap nv                                 -- order-    -- Configuration-    <*> return conf                                   -- config-    <*> return nv                                     -- nVars-    <*> newDouble 1.0                                 -- claInc---  <*> newDouble (variableDecayRate conf)            -- varDecay-    <*> newDouble 1.0                                 -- varInc-    <*> newInt 0                                      -- rootLevel-    -- Working Memory-    <*> newBool True                                  -- ok-    <*> newVec (nv + 1)                               -- an'seen-    <*> newStack nv                                   -- an'toClear-    <*> newStack nv                                   -- an'stack-    <*> newVecWith (nv + 1) (-1)                      -- pr'seen-    <*> newVec nv                                     -- lbd'seen-    <*> newInt 0                                      -- lbd'key-    <*> newStack nv                                   -- litsLearnt-    <*> newStack nv                                   -- lastDL-    <*> newVec (1 + fromEnum (maxBound :: StatIndex)) -- stats------------------------------------------------------------------------------------- Accessors---- | returns the number of current assigments-{-# INLINE nAssigns #-}-nAssigns :: Solver -> IO Int-nAssigns = sizeOfStack . trail---- | returns the number of constraints (clauses)-{-# INLINE nClauses #-}-nClauses  :: Solver -> IO Int-nClauses = numberOfClauses . clauses---- | returns the number of learnt clauses-{-# INLINE nLearnts #-}-nLearnts :: Solver -> IO Int-nLearnts = numberOfClauses . learnts---- | return the model as a list of literal-getModel :: Solver -> IO [Int]-getModel s = zipWith (\n b -> if b then n else negate n) [1 .. ] <$> asList (model s)---- | returns the current decision level-{-# INLINE decisionLevel #-}-decisionLevel :: Solver -> IO Int-decisionLevel Solver{..} = sizeOfStack trailLim---- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Var'-{-# INLINE valueVar #-}-valueVar :: Solver -> Var -> IO Int-valueVar s !x = getNth (assigns s) x---- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Lit'-{-# INLINE valueLit #-}-valueLit :: Solver -> Lit -> IO Int -- FIXME: LiftedBool-valueLit Solver{..} !p = if positiveLit p then getNth assigns (lit2var p) else negate <$> getNth assigns (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 Solver{..} c@Clause{..} =  (c ==) <$> (getNthClause reason . lit2var =<< getNth lits 1)---- | stats-data StatIndex =-    NumOfBackjump-  | NumOfRestart-  deriving (Bounded, Enum, Eq, Ord, Read, Show)---- | increments a stat data corresponding to 'StatIndex'-incrementStat :: Solver -> StatIndex -> Int -> IO ()-incrementStat (config -> collectStats -> False) _ _ = return ()-incrementStat (stats -> v) (fromEnum -> i) k = modifyNth v (+ k) i---- | returns the statistics as list-getStats :: Solver -> IO [(StatIndex, Int)]-getStats (config -> collectStats -> False) = return []-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 -> Vec -> IO Bool-addClause s@Solver{..} vecLits = do-  result <- clauseNew s vecLits False-  case result of-   (False, _) -> return False   -- Conflict occured-   (True, c)  -> do-     unless (c == NullClause) $ pushClause clauses c-     return True                -- No conflict---- | __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.)-{-# INLINABLE clauseNew #-}-clauseNew :: Solver -> Vec -> Bool -> IO (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 -> setNth ps 0 0 >> return True -- p and negateLit p occurs in ps-             _ -> handle (j + 1) l n-      loopForLearnt :: Int -> IO Bool-      loopForLearnt i = do-        n <- getNth ps 0-        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 <- getNth ps 0-        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  -> setNth ps 0 0 >> 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 <- getNth ps 0-  case k of-   0 -> return (exit, NullClause)-   1 -> do-     l <- getNth ps 1-     (, NullClause) <$> enqueue s l NullClause-   _ -> do-     -- allocate clause:-     c <- newClauseFromVec isLearnt ps-     let vec = asVec 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-           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-       forM_ [0 .. k -1] $ varBumpActivity s . lit2var <=< getNth vec -- variables in conflict clauses are bumped-     -- 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 (True, 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-  -- putStrLn . ("ssigns " ++) . show . map lit2int =<< asList trail-  -- putStrLn =<< dump ("enqueue " ++ show (lit2int p) ++ " ") from-  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-        setNthClause reason v from     -- NOTE: @from@ might be NULL!-        pushToStack 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@Solver{..} p = do-  pushToStack trailLim =<< sizeOfStack trail-  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 = asVec trail-    let tl = asVec trailLim-    lim <- getNth tl lvl-    ts <- sizeOfStack trail-    ls <- sizeOfStack 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.-        setNthClause 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-    shrinkStack trail (ts - lim)-    shrinkStack trailLim (ls - lvl)-    setInt qHead =<< sizeOfStack 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---- | __Fig. 14 (p.19)__ Bumping of clause activity-{-# INLINE varBumpActivity #-}-varBumpActivity :: Solver -> Var -> IO ()-varBumpActivity s@Solver{..} !x = do-  !a <- (+) <$> getNthDouble x activities <*> getDouble varInc-  if 1e100 < a-    then varRescaleActivity s-    else setNthDouble x activities a-  update s x---- | __Fig. 14 (p.19)__-{-# INLINE varDecayActivity #-}-varDecayActivity :: Solver -> IO ()-varDecayActivity Solver{..} = modifyDouble varInc (/ variableDecayRate config)--- varDecayActivity Solver{..} = modifyDouble varInc . (flip (/)) =<< getDouble varDecay---- | __Fig. 14 (p.19)__-{-# INLINE varRescaleActivity #-}-varRescaleActivity :: Solver -> IO ()-varRescaleActivity Solver{..} = do-  forM_ [1 .. nVars] $ \i -> modifyNthDouble i activities (* 1e-100)-  modifyDouble varInc (* 1e-100)---- | __Fig. 14 (p.19)__-{-# INLINE claBumpActivity #-}-claBumpActivity :: Solver -> Clause -> IO ()-claBumpActivity s@Solver{..} Clause{..} = do-  a <- (+) <$> getDouble activity <*> getDouble claInc-  if 1e100 < a-    then claRescaleActivity s-    else setDouble activity a---- | __Fig. 14 (p.19)__-{-# INLINE claDecayActivity #-}-claDecayActivity :: Solver -> IO ()-claDecayActivity Solver{..} = modifyDouble claInc (/ clauseDecayRate config)---- | __Fig. 14 (p.19)__-{-# INLINE claRescaleActivity #-}-claRescaleActivity :: Solver -> IO ()-claRescaleActivity Solver{..} = do-  vec <- getClauseVector learnts-  n <- numberOfClauses learnts-  let-    loopOnVector :: Int -> IO ()-    loopOnVector ((< n) -> False) = return ()-    loopOnVector i = do-      c <- getNthClause vec i-      modifyDouble (activity c) (* 1e-20) -- not 1e-100-      loopOnVector $ i + 1-  loopOnVector 0-  modifyDouble claInc (* 1e-20)           -- not 1e-100---------------------------------------------------------------------------------- VarHeap---- | 'VarHeap' is 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 :: Vec -- order to var-                , idxs :: Vec -- var to order (index)-                }--newVarHeap :: Int -> IO VarHeap-newVarHeap n = VarHeap <$> newSizedVecIntFromList lst <*> newSizedVecIntFromList lst-  where-    lst = [1 .. n]--{-# INLINE numElementsInHeap #-}-numElementsInHeap :: Solver -> IO Int-numElementsInHeap (order -> heap -> h) = getNth h 0--{-# 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 <- getNthDouble v activities-  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 <- getNthDouble v' activities-            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 <- getNthDouble v activities-  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 <- getNthDouble l activities-            acR <- getNthDouble r activities-            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--{-# INLINE 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-  setNth to 0 n-  percolateUp s n---- | renamed from 'getmin'-{-# INLINE 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,269 +0,0 @@--- | Basic data types used throughout mios.-{-# LANGUAGE-    BangPatterns-  , FlexibleContexts-  , FlexibleInstances-  , FunctionalDependencies-  , MultiParamTypeClasses-  #-}-{-# LANGUAGE Trustworthy #-}--module SAT.Solver.Mios.Types-       (-         -- Singleton-         module SAT.Solver.Mios.Data.Singleton-         -- Fixed Unboxed Mutable Int Vector-       , module SAT.Solver.Mios.Data.Vec-         -- Abstract interfaces-       , VectorFamily (..)-         -- *  Variable-       , Var-       , bottomVar-       , int2var-         -- * Internal encoded Literal-       , Lit-       , lit2int-       , int2lit-       , bottomLit-       , newLit-       , positiveLit-       , lit2var-       , var2lit-       , negateLit-         -- * Assignment-       , LiftedBool (..)-       , lbool-       , lFalse-       , lTrue-       , lBottom-       , VarOrder (..)-         -- * CNF-       , CNFDescription (..)-       )-       where--import Control.Monad (forM)-import Data.Bits-import qualified Data.Vector.Unboxed.Mutable as UV-import SAT.Solver.Mios.Data.Singleton-import SAT.Solver.Mios.Data.Vec---- | Public interface as /Container/-class VectorFamily s t | s -> t where-  -- * Size operations-  -- | erases all elements in it-  clear :: s -> IO ()-  clear = error "no default method for clear"-  -- * Debug-  -- | dump the contents-  dump :: Show t => String -> s -> IO String-  dump msg _ = error $ msg ++ ": no defalut method for dump"-  -- | get a raw data-  asVec :: s -> UV.IOVector Int-  asVec = error "asVector undefined"-  -- | converts into a list-  asList :: s -> IO [t]-  asList = error "asList undefined"-  {-# MINIMAL dump #-}---- | provides 'clear' and 'size'-instance VectorFamily Vec Int where-  clear = error "Vec.clear"-  {-# SPECIALIZE INLINE asList :: Vec -> IO [Int] #-}-  asList v = forM [0 .. UV.length v - 1] $ UV.unsafeRead v-  dump str v = (str ++) . show <$> asList v-  {-# SPECIALIZE INLINE asVec :: Vec -> Vec #-}-  asVec = id---- | 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 = 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---- | A contant representing False-lFalse:: Int-lFalse = -1---- | A constant representing True-lTrue :: Int-lTrue = 1---- | A constant for "undefined"-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 :: (VectorFamily v1 Bool, VectorFamily 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"--  -- | Called when variable has increased in activity.-  update :: o -> Var -> IO ()-  update _  = error "update undefined"--  -- | Called when all variables have been assigned new activities.-  updateAll :: o -> IO ()-  updateAll = error "updateAll undefined"--  -- | Called when variable is unbound (may be selected again).-  undo :: o -> Var -> IO ()-  undo _ _  = error "undo undefined"--  -- | Called to select a new, unassigned variable.-  select :: o -> IO Var-  select    = error "select undefined"---- | misc information on CNF-data CNFDescription = CNFDescription-  {-    _numberOfVariables :: !Int           -- ^ number of variables-  , _numberOfClauses :: !Int             -- ^ number of clauses-  , _pathname :: Maybe FilePath          -- ^ given filename-  }-  deriving (Eq, Ord, Show)

@@ -1,47 +0,0 @@--- | validate an assignment-{-# LANGUAGE-    ViewPatterns-  #-}-{-# LANGUAGE Safe #-}-module SAT.Solver.Mios.Validator-       (-         validate-       )-       where--import Data.Foldable (toList)-import SAT.Solver.Mios.Types-import SAT.Solver.Mios.Clause-import SAT.Solver.Mios.ClauseManager-import SAT.Solver.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-  vec <- getClauseVector (clauses s)-  nc <- numberOfClauses (clauses s)-  let-    inject :: Lit -> IO ()-    inject l = setNth assignment (lit2var l) $ if positiveLit l then lTrue else lFalse-    -- return 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)-    -- return 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-    -- traverse all clauses in 'clauses'-    loopOnVector :: Int -> IO Bool-    loopOnVector ((< nc) -> False) = return True-    loopOnVector i = do-      c <- getNthClause vec i-      sat' <- satAny =<< asList c-      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,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.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.Util.CNFIO-       (-         -- * Input-         fromFile-       , clauseListFromFile-       , fromMinisatOutput-       , clauseListFromMinisatOutput-         -- * Output-       , toFile-       , toCNFString-       , asCNFString-       , asCNFString_-         -- * Bool Operation-       , module SAT.Util.BoolExp-       )-       where-import SAT.Util.CNFIO.Reader-import SAT.Util.CNFIO.Writer-import SAT.Util.CNFIO.MinisatReader-import SAT.Util.BoolExp---- | String from BoolFrom-asCNFString :: BoolForm -> String-asCNFString = toCNFString . asList---- | String from BoolFrom-asCNFString_ :: BoolForm -> String-asCNFString_ = toCNFString . asList_

@@ -1,73 +0,0 @@-{-# LANGUAGE Safe #-}---- | Read an output file of minisat-module SAT.Util.CNFIO.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.Util.CNFIO.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 []