mios 1.3.0 → 1.4.0

raw patch · 25 files changed

+1219/−1417 lines, 25 filesdep −containersdep −primitivePVP ok

version bump matches the API change (PVP)

Dependencies removed: containers, primitive

API changes (from Hackage documentation)

Files

• SAT/Mios.hs +38/−42
• SAT/Mios/Clause.hs +71/−70
• SAT/Mios/ClauseManager.hs +82/−174
• SAT/Mios/Data/Singleton.hs +0/−105
• SAT/Mios/Data/Stack.hs +0/−90
• SAT/Mios/Data/Vec.hs +0/−86
• SAT/Mios/Data/VecBool.hs +0/−55
• SAT/Mios/Data/VecDouble.hs +0/−53
• SAT/Mios/Internal.hs +0/−33
• SAT/Mios/Main.hs +163/−156
• SAT/Mios/OptionParser.hs +1/−2
• SAT/Mios/Solver.hs +180/−158
• SAT/Mios/Types.hs +54/−66
• SAT/Mios/Util/CNFIO.hs +0/−31
• SAT/Mios/Util/CNFIO/MinisatReader.hs +0/−73
• SAT/Mios/Util/CNFIO/Reader.hs +0/−130
• SAT/Mios/Util/CNFIO/Writer.hs +0/−58
• SAT/Mios/Util/DIMACS.hs +31/−0
• SAT/Mios/Util/DIMACS/MinisatReader.hs +73/−0
• SAT/Mios/Util/DIMACS/Reader.hs +130/−0
• SAT/Mios/Util/DIMACS/Writer.hs +58/−0
• SAT/Mios/Validator.hs +3/−4
• SAT/Mios/Vec.hs +276/−0
• app/sample.hs +26/−0
• mios.cabal +33/−31

@@ -1,7 +1,7 @@--- | Minisat-based Implementation and Optimization Study on SAT solver {-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE Safe #-} +-- | Minisat-based Implementation and Optimization Study on SAT solver module SAT.Mios        (          -- * Interface to the core of solver@@ -36,12 +36,15 @@ 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 +-- | version name+versionId :: String+versionId = "mios 1.4.0 -- https://github.com/shnarazk/mios"+ reportElapsedTime :: Bool -> String -> Integer -> IO Integer reportElapsedTime False _ _ = return 0 reportElapsedTime _ _ 0 = getCPUTime@@ -52,13 +55,13 @@   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+-- | 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.+-- | 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@@ -102,7 +105,7 @@  executeSolver _ = return () --- | new top-level interface that returns+-- | new top-level interface that returns: -- -- * conflicting literal set :: Left [Int] -- * satisfiable assignment :: Right [Int]@@ -110,31 +113,30 @@ 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+  mapM_ ((s `addClause`) <=< (newStackFromList . map int2lit)) c   noConf <- simplifyDB s   if noConf     then do         x <- solve s []         if x             then Right <$> getModel s-            else Left .  map lit2int <$> asList (conflict s)+            else Left .  map lit2int <$> asList (conflicts s)     else return $ Left [] ---- | the easiest interface for Haskell programs--- This returns the result @::[[Int]]@ for a given @(CNFDescription, [[Int]])@+-- | The 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+-- 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+-- | 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+  mapM_ ((s `addClause`) <=< (newStackFromList . map int2lit)) cls   noConf <- simplifyDB s   if noConf     then do@@ -144,13 +146,13 @@             else return []     else return [] --- | validates a given assignment from STDIN for the CNF file (2nd arg)--- this is the entry point for standalone programs+-- | 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+-- | 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@@ -172,13 +174,13 @@  executeValidator _  = return () --- | returns True if a given assignment (2nd arg) satisfies the problem (1st arg)+-- | 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@+-- 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+  mapM_ ((s `addClause`) <=< (newStackFromList . map int2lit)) cls   s `validate` asg  -- | dumps an assigment to file.@@ -192,13 +194,10 @@ -- dumpAssigmentAsCNF :: FilePath -> Bool -> [Int] -> IO () dumpAssigmentAsCNF fname False _ = do-  withFile fname WriteMode $ \h -> do-    hPutStrLn h "UNSAT"+  withFile fname WriteMode $ \h -> hPutStrLn h "UNSAT"  dumpAssigmentAsCNF fname True l = do-  withFile fname WriteMode $ \h -> do-    hPutStrLn h "SAT"-    hPutStrLn h . unwords $ map show l+  withFile fname WriteMode $ \h -> do hPutStrLn h "SAT"; hPutStrLn h . unwords $ map show l  -------------------------------------------------------------------------------- -- DIMACS CNF Reader@@ -218,8 +217,8 @@ 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+  buffer <- newVec (maxLit + 1) 0+  polvec <- newVec (maxLit + 1) 0   let     loop :: Int -> B.ByteString -> IO ()     loop ((< nc) -> False) _ = return ()@@ -231,9 +230,9 @@     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+      p <- getNth polvec $ var2lit v True+      n <- getNth polvec $ var2lit v False+      when (p == lFalse || n == lFalse) $ setNth asg v p       checkPolarity $ v + 1   checkPolarity 1 @@ -267,8 +266,8 @@     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+readClause :: Solver -> Stack -> Vec Int -> B.ByteString -> IO B.ByteString+readClause s buffer bvec stream = do   let     loop :: Int -> B.ByteString -> IO B.ByteString     loop i b = do@@ -277,20 +276,17 @@         then do             -- putStrLn . ("clause: " ++) . show . map lit2int =<< asList stack             setNth buffer 0 $ i - 1-            addClause s buffer+            void $ addClause s buffer             return b'         else do             let l = int2lit k             setNth buffer i l-            setNthBool pvec l True+            setNth bvec l lTrue             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'+showPath str = replicate (len - length basename) ' ' ++ if elem '/' str then basename else basename'   where     len = 50     basename = reverse . takeWhile (/= '/') . reverse $ str

@@ -14,37 +14,29 @@          Clause (..) --       , isLit --       , getLit-       , shrinkClause-       , newClauseFromVec-       , sizeOfClause+       , newClauseFromStack          -- * 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 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?+-- normal, null (and binary) clause.+-- This matches both of @Clause@ and @GClause@ in MiniSat. data Clause = Clause               {-                learnt     :: !Bool            -- ^ whether this is a learnt clause---              , rank       :: !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+                learnt     :: !Bool     -- ^ whether this is a learnt clause+--              , rank     :: !Int'     -- ^ goodness like LBD; computed in 'Ranking'+              , activity   :: !Double'  -- ^ activity of this clause+              , protected  :: !Bool'    -- ^ protected from reduce+              , lits       :: !Stack    -- ^ which this clause consists of               }   | NullClause                              -- as null pointer --  | BinaryClause Lit                        -- binary clause consists of only a propagating literal@@ -58,87 +50,96 @@   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] #-}+-- | 'Clause' is a 'VecFamily' of 'Lit'.+instance VecFamily Clause Lit where+  {-# SPECIALIZE INLINE getNth :: Clause -> Int -> IO Int #-}+  getNth Clause{..} n = error "no getNth for Clause"+  {-# SPECIALIZE INLINE setNth :: Clause -> Int -> Int -> IO () #-}+  setNth Clause{..} n x = error "no setNth for Clause"+  -- | returns a vector of literals in it.+  {-# SPECIALIZE INLINE asUVector :: Clause -> UVector Int #-}+  asUVector = asUVector . lits   asList NullClause = return []-  asList Clause{..} = do-    (n : ls)  <- asList lits-    return $ take n ls+  asList Clause{..} = take <$> get' lits <*> asList lits+  -- dump mes NullClause = return $ mes ++ "Null"+  -- dump mes Clause{..} = return $ mes ++ "a clause"+{-+  dump mes Clause{..} = do+    a <- show <$> get' activity+    n <- get' lits+    l <- asList lits+    return $ mes ++ "C" ++ show n ++ "{" ++ intercalate "," [show learnt, a, show (map lit2int l)] ++ "}"+-} --- returns True if it is a 'BinaryClause'+-- | 'Clause' is a 'SingleStorage' on the number of literals in it.+instance SingleStorage Clause Int where+  -- | returns the number of literals in a clause, even if the given clause is a binary clause+  {-# SPECIALIZE INLINE get' :: Clause -> IO Int #-}+  get' = get' . lits+  -- getSize (BinaryClause _) = return 1+  -- | sets the number of literals in a clause, even if the given clause is a binary clause+  {-# SPECIALIZE INLINE set' :: Clause -> Int -> IO () #-}+  set' c n = set' (lits c) n+  -- getSize (BinaryClause _) = return 1++-- | 'Clause' is a 'Stackfamily'on literals since literals in it will be discared if satisifed at level = 0.+instance StackFamily Clause Lit where+  -- | drop the last /N/ literals in a 'Clause' to eliminate unsatisfied literals+  {-# SPECIALIZE INLINE shrinkBy :: Clause -> Int -> IO () #-}+  shrinkBy c n = modifyNth (lits c) (subtract n) 0++-- returns True if it is a 'BinaryClause'. -- FIXME: this might be discarded in minisat 2.2 -- isLit :: Clause -> Bool -- isLit (BinaryClause _) = True -- isLit _ = False --- returns the literal in a BinaryClause+-- 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+-- 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'+-- | 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+{-# INLINABLE newClauseFromStack #-}+newClauseFromStack :: Bool -> Stack -> IO Clause+newClauseFromStack l vec = do+  n <- get' vec+  v <- newStack n+  let+    loop ((<= n) -> False) = return ()+    loop i = (setNth v i =<< getNth vec i) >> loop (i + 1)+  loop 0+  Clause l <$> {- new' 0 <*> -} new' 0.0 <*> new' False <*> return v ---------------------------------------------------------------------------------+-------------------------------------------------------------------------------- Clause Vector  -- | Mutable 'Clause' Vector type ClauseVector = MV.IOVector Clause -instance VectorFamily ClauseVector Clause where+-- | 'ClauseVector' is a vector of 'Clause'.+instance VecFamily ClauseVector Clause where+  {-# SPECIALIZE INLINE getNth :: ClauseVector -> Int -> IO Clause #-}+  getNth = MV.unsafeRead+  {-# SPECIALIZE INLINE setNth :: ClauseVector -> Int -> Clause -> IO () #-}+  setNth = MV.unsafeWrite+  {-# SPECIALIZE INLINE swapBetween :: ClauseVector -> Int -> Int -> IO () #-}+  swapBetween = MV.unsafeSwap   asList cv = V.toList <$> V.freeze cv+{-   dump mes cv = do     l <- asList cv     sts <- mapM (dump ",") (l :: [Clause])     return $ mes ++ tail (concat sts)+-} --- | returns a new 'ClauseVector'+-- | 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,6 +1,5 @@ {-# LANGUAGE     BangPatterns-  , DuplicateRecordFields   , FlexibleInstances   , MultiParamTypeClasses   , RecordWildCards@@ -13,8 +12,6 @@        (          -- * higher level interface for ClauseVector          ClauseManager (..)---       -- * vector of clauses---       , SimpleManager          -- * Manager with an extra Int (used as sort key or blocking literal)        , ClauseExtManager        , pushClauseWithKey@@ -25,152 +22,99 @@        , WatcherList        , newWatcherList        , getNthWatcher-       , garbageCollect---       , numberOfRegisteredClauses        )        where -import Control.Monad (forM, unless, when)+import Control.Monad (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+-- | Resizable vector of 'C.Clause'. 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+--------------------------------------------------------------------------------++-- | Clause + Blocking Literal+data ClauseExtManager = ClauseExtManager   {-    _nActives     :: IntSingleton               -- number of active clause-  , _clauseVector :: IORef.IORef C.ClauseVector -- clause list+    _nActives     :: !Int'                         -- number of active clause+  , _purged       :: !Bool'                        -- whether it needs gc+  , _clauseVector :: IORef.IORef C.ClauseVector    -- clause list+  , _keyVector    :: IORef.IORef (UVector Int)     -- Int list   } -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+-- | 'ClauseExtManager' is a 'SingleStorage` on the numeber of clauses in it.+instance SingleStorage ClauseExtManager Int where+  {-# SPECIALIZE INLINE get' :: ClauseExtManager -> IO Int #-}+  get' m = get' (_nActives m)+  {-# SPECIALIZE INLINE set' :: ClauseExtManager -> Int -> IO () #-}+  set' m = set' (_nActives m)++-- | 'ClauseExtManager' is a 'StackFamily` on clauses.+instance StackFamily ClauseExtManager C.Clause where+  {-# SPECIALIZE INLINE shrinkBy :: ClauseExtManager -> Int -> IO () #-}+  shrinkBy m k = modify' (_nActives m) (subtract k)+  pushTo ClauseExtManager{..} c = do+    -- checkConsistency m c+    !n <- get' _nActives     !v <- IORef.readIORef _clauseVector+    !b <- IORef.readIORef _keyVector     if MV.length v - 1 <= n       then do-          v' <- MV.unsafeGrow v (max 8 (MV.length v))-          -- forM_ [n  .. MV.length v' - 1] $ \i -> MV.unsafeWrite v' i C.NullClause+          let len = max 8 $ MV.length v+          v' <- MV.unsafeGrow v len+          b' <- growBy b len           MV.unsafeWrite v' n c+          setNth b' n 0           IORef.writeIORef _clauseVector v'-      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-  }+          IORef.writeIORef _keyVector b'+      else MV.unsafeWrite v n c >> setNth b n 0+    modify' _nActives (1 +) +-- | 'ClauseExtManager' is a 'ClauseManager' instance ClauseManager ClauseExtManager where+  -- | returns a new instance.   {-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-}   newManager initialSize = do-    i <- newInt 0+    i <- new' 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)+    b <- newVec (MV.length v) 0+    ClauseExtManager i <$> new' False <*> IORef.newIORef v <*> IORef.newIORef b+  -- | returns the internal 'C.ClauseVector'.   {-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-}   getClauseVector !m = IORef.readIORef (_clauseVector m)+{-   -- | O(1) insertion function-  {-# SPECIALIZE INLINE pushClause :: ClauseExtManager -> C.Clause -> IO () #-}   pushClause !ClauseExtManager{..} !c = do     -- checkConsistency m c-    !n <- getInt _nActives+    !n <- get' _nActives     !v <- IORef.readIORef _clauseVector     !b <- IORef.readIORef _keyVector     if MV.length v - 1 <= n       then do           let len = max 8 $ MV.length v           v' <- MV.unsafeGrow v len-          b' <- vecGrow b len+          b' <- growBy b len           MV.unsafeWrite v' n c           setNth b' n 0           IORef.writeIORef _clauseVector v'           IORef.writeIORef _keyVector b'       else MV.unsafeWrite v n c >> setNth b n 0-    modifyInt _nActives (1 +)+    modify' _nActives (1 +)+-} {-   -- | O(n) but lightweight remove-and-compact function   -- __Pre-conditions:__ the clause manager is empty or the clause is stored in it.   {-# SPECIALIZE INLINE removeClause :: ClauseExtManager -> C.Clause -> IO () #-}   removeClause ClauseExtManager{..} c = do-    !n <- subtract 1 <$> getInt _nActives+    !n <- subtract 1 <$> get' _nActives     !v <- IORef.readIORef _clauseVector     !b <- IORef.readIORef _keyVector     let@@ -182,15 +126,15 @@       !i <- seekIndex 0       MV.unsafeWrite v i =<< MV.unsafeRead v n       setNth b i =<< getNth b n-      setInt _nActives n+      set' _nActives n   removeNthClause = error "removeNthClause is not implemented on ClauseExtManager" -} --- | sets the expire flag to a clause-{-# INLINE markClause #-}+-- | sets the expire flag to a clause.+{-# INLINABLE markClause #-} markClause :: ClauseExtManager -> C.Clause -> IO () markClause ClauseExtManager{..} c = do-  !n <- getInt _nActives+  !n <- get' _nActives   !v <- IORef.readIORef _clauseVector   let     seekIndex :: Int -> IO ()@@ -199,128 +143,92 @@       if c' == c then MV.unsafeWrite v k C.NullClause else seekIndex $ k + 1   unless (n == 0) $ do     seekIndex 0-    setBool _purged True+    set' _purged True -{-# INLINE purifyManager #-}+{-# INLINABLE purifyManager #-} purifyManager :: ClauseExtManager -> IO () purifyManager ClauseExtManager{..} = do-  diry <- getBool _purged+  diry <- get' _purged   when diry $ do-    n <- getInt _nActives+    n <- get' _nActives     vec <- IORef.readIORef _clauseVector     keys <- IORef.readIORef _keyVector     let       loop :: Int -> Int -> IO Int       loop ((< n) -> False) n' = return n'       loop i j = do-        c <- C.getNthClause vec i+        c <- getNth vec i         if c /= C.NullClause           then do               unless (i == j) $ do-                C.setNthClause vec j c+                setNth 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+    set' _nActives =<< loop 0 0+    set' _purged False --- | returns the associated Int vector+-- | returns the associated Int vector, which holds /blocking literals/. {-# INLINE getKeyVector #-}-getKeyVector :: ClauseExtManager -> IO Vec+getKeyVector :: ClauseExtManager -> IO (UVector Int) getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector  -- | O(1) inserter-{-# INLINE pushClauseWithKey #-}+{-# INLINABLE pushClauseWithKey #-} pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO () pushClauseWithKey !ClauseExtManager{..} !c k = do   -- checkConsistency m c-  !n <- getInt _nActives+  !n <- get' _nActives   !v <- IORef.readIORef _clauseVector   !b <- IORef.readIORef _keyVector   if MV.length v - 1 <= n     then do         let len = max 8 $ MV.length v         v' <- MV.unsafeGrow v len-        b' <- vecGrow b len+        b' <- growBy b len         MV.unsafeWrite v' n c         setNth b' n k         IORef.writeIORef _clauseVector v'         IORef.writeIORef _keyVector b'     else MV.unsafeWrite v n c >> setNth b n k-  modifyInt _nActives (1 +)+  modify' _nActives (1 +) -instance VectorFamily ClauseExtManager C.Clause where+-- | 'ClauseExtManager' is a collection of 'C.Clause'+instance VecFamily ClauseExtManager C.Clause where+  getNth = error "no getNth method for ClauseExtManager"+  setNth = error "no setNth method for ClauseExtManager"+  {-# SPECIALIZE INLINE reset :: ClauseExtManager -> IO () #-}+  reset m = set' (_nActives m) 0+{-   dump mes ClauseExtManager{..} = do-    n <- getInt _nActives+    n <- get' _nActives     if n == 0       then return $ mes ++ "empty ClauseExtManager"       else do           l <- take n <$> (asList =<< IORef.readIORef _clauseVector)           sts <- mapM (dump ",") (l :: [C.Clause])           return $ mes ++ "[" ++ show n ++ "]" ++ tail (concat sts)+-}  -------------------------------------------------------------------------------- WatcherList --- | Vector of 'ClauseExtManager'+-- | Immutable Vector of 'ClauseExtManager' type WatcherList = V.Vector ClauseExtManager --- | /n/ is the number of 'Var', /m/ is default size of each watcher list+-- | /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)+newWatcherList n m = V.fromList <$> mapM (\_ -> newManager m) [0 .. int2lit (negate n) + 1] --- | returns the watcher List :: "ClauseManager" for "Literal" /l/+-- | returns the watcher List 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"--}+-- | 'WatcherList' is an 'Lit'-indexed collection of 'C.Clause'.+instance VecFamily WatcherList C.Clause where+  getNth = error "no getNth method for WatcherList" -- getNthWatcher is a pure function+  setNth = error "no setNth method for WatcherList"+  {-# SPECIALIZE INLINE reset :: WatcherList -> IO () #-}+  reset = V.mapM_ purifyManager+--  dump _ _ = (mes ++) . concat <$> mapM (\i -> dump ("\n" ++ show (lit2int i) ++ "' watchers:") (getNthWatcher wl i)) [1 .. V.length wl - 1]

@@ -1,105 +0,0 @@-{-# 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

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

@@ -1,86 +0,0 @@--- | 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

@@ -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.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

@@ -1,53 +0,0 @@--- | 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

@@ -1,33 +0,0 @@--- | 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 -}

@@ -6,7 +6,7 @@   #-} {-# LANGUAGE Safe #-} --- | This is a part of MIOS; main heuristics+-- | This is a part of MIOS; main heuristics. module SAT.Mios.Main        (          simplifyDB@@ -14,27 +14,24 @@        )         where -import Control.Monad (forM_, unless, void, when)+import Control.Monad (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+-- | returns a rank of 'Clause'. Smaller value is better.+{-# INLINE rankOf #-}+rankOf :: Clause -> IO Int+rankOf = get'  -- | #114: __RemoveWatch__ {-# INLINABLE removeWatch #-} removeWatch :: Solver -> Clause -> IO () removeWatch (watches -> w) c = do-  let lvec = asVec c+  let lvec = asUVector c   l1 <- negateLit <$> getNth lvec 0   markClause (getNthWatcher w l1) c   l2 <- negateLit <$> getNth lvec 1@@ -44,40 +41,40 @@ -- 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+-- | __Fig. 8. (p.12)__ creates a new LEARNT clause and adds it to watcher lists.+-- This is a strippped-down version of 'newClause' in Solver. {-# INLINABLE newLearntClause #-}-newLearntClause :: Solver -> Vec -> IO ()+newLearntClause :: Solver -> Stack -> IO () newLearntClause s@Solver{..} ps = do-  good <- getBool ok+  good <- get' ok   when good $ do     -- ps is a 'SizedVectorInt'; ps[0] is the number of active literals     -- Since this solver must generate only healthy learnt clauses, we need not to run misc check in 'newClause'-    k <- getNth ps 0+    k <- get' ps     case k of      1 -> do        l <- getNth ps 1        unsafeEnqueue s l NullClause      _ -> do        -- allocate clause:-       c <- newClauseFromVec True ps-       let vec = asVec c+       c <- newClauseFromStack True ps+       let vec = asUVector c        -- Pick a second literal to watch:        let          findMax :: Int -> Int -> Int -> IO Int          findMax ((< k) -> False) j _ = return j          findMax i j val = do-           v' <- lit2var <$> getNth vec i-           a <- getNth assigns v'-           b <- getNth level v'+           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+       set' (activity c) . fromIntegral =<< decisionLevel s -- newly learnt clauses should be considered active        -- Add clause to all managers-       pushClause learnts c+       pushTo learnts c        l <- getNth vec 0        pushClauseWithKey (getNthWatcher watches (negateLit l)) c 0        l1 <- negateLit <$> getNth vec 1@@ -86,7 +83,7 @@        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+       set' (protected c) True  -- | __Simplify.__ At the top-level, a constraint may be given the opportunity to -- simplify its representation (returns @False@) or state that the constraint is@@ -98,9 +95,9 @@ {-# INLINABLE simplify #-} simplify :: Solver -> Clause -> IO Bool simplify s c = do-  n <- sizeOfClause c+  n <- get' c   let-    lvec = asVec c+    lvec = asUVector c     loop ::Int -> IO Bool     loop ((< n) -> False) = return False     loop i = do@@ -135,33 +132,33 @@ --     rest of literals. There may be others from the same level though. -- -- @analyze@ is invoked from @search@--- {-# INLINEABLE analyze #-}+{-# INLINABLE 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+  reset litsLearnt+  pushTo litsLearnt 0 -- reserve the first place for the unassigned literal   dl <- decisionLevel s   let-    litsVec = asVec litsLearnt-    trailVec = asVec trail+    litsVec = asUVector litsLearnt+    trailVec = asUVector trail     loopOnClauseChain :: Clause -> Lit -> Int -> Int -> Int -> IO Int     loopOnClauseChain c p ti bl pathC = do -- p : literal, ti = trail index, bl = backtrack level       when (learnt c) $ do         claBumpActivity s c {-         -- update LBD like #Glucose4.0-        d <- getInt (lbd c)+        d <- get' (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`+            when (d <= 30) $ set' (protected c) True -- 30 is `lbLBDFrozenClause`             -- seems to be interesting: keep it fro the next round-            setInt (lbd c) nblevels    -- Update it+            set' (lbd c) nblevels    -- Update it -}-      sc <- sizeOfClause c+      sc <- get' c       let-        lvec = asVec c+        lvec = asUVector c         loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int)         loopOnLiterals ((< sc) -> False) b pc = return (b, pc) -- b = btLevel, pc = pathC         loopOnLiterals j b pc = do@@ -176,11 +173,11 @@                 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+                      r <- getNth reason v+                      when (r /= NullClause && learnt r) $ pushTo an'lastDL q                       -- end of glucose heuristics                       loopOnLiterals (j + 1) b (pc + 1)-                  else pushToStack litsLearnt q >> loopOnLiterals (j + 1) (max b l) pc+                  else pushTo litsLearnt q >> loopOnLiterals (j + 1) (max b l) pc             else loopOnLiterals (j + 1) b pc       (b', pathC') <- loopOnLiterals (if p == bottomLit then 0 else 1) bl pathC       let@@ -192,33 +189,33 @@       ti' <- nextPickedUpLit ti       nextP <- getNth trailVec ti'       let nextV = lit2var nextP-      confl' <- getNthClause reason nextV+      confl' <- getNth reason nextV       setNth an'seen nextV 0       if 1 < pathC'         then loopOnClauseChain confl' nextP (ti' - 1) b' (pathC' - 1)         else setNth litsVec 0 (negateLit nextP) >> return b'-  ti <- subtract 1 <$> sizeOfStack trail+  ti <- subtract 1 <$> get' 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+  n <- get' litsLearnt+  reset an'stack           -- analyze_stack.clear();+  reset an'toClear         -- out_learnt.copyTo(analyze_toclear);+  pushTo an'toClear =<< getNth litsVec 0   let     merger :: Int -> Int -> IO Int     merger ((< n) -> False) b = return b     merger i b = do       l <- getNth litsVec i-      pushToStack an'toClear l+      pushTo an'toClear l       -- restrict the search depth (range) to 32       merger (i + 1) . setBit b . (31 .&.) =<< getNth level (lit2var l)   levels <- merger 1 0   let     loopOnLits :: Int -> Int -> IO ()-    loopOnLits ((< n) -> False) n' = shrinkStack litsLearnt $ n - n'+    loopOnLits ((< n) -> False) n' = shrinkBy litsLearnt $ n - n'     loopOnLits i j = do       l <- getNth litsVec i-      c1 <- (NullClause ==) <$> getNthClause reason (lit2var l)+      c1 <- (NullClause ==) <$> getNth reason (lit2var l)       if c1         then setNth litsVec j l >> loopOnLits (i + 1) (j + 1)         else do@@ -228,23 +225,23 @@              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+  nld <- get' an'lastDL+  r <- get' litsLearnt -- this is not the right value   let-    vec = asVec lastDL+    vec = asUVector an'lastDL     loopOnLastDL :: Int -> IO ()     loopOnLastDL ((< nld) -> False) = return ()     loopOnLastDL i = do       v <- lit2var <$> getNth vec i-      r' <- ranking' =<< getNthClause reason v+      r' <- rankOf =<< getNth reason v       when (r < r') $ varBumpActivity s v       loopOnLastDL $ i + 1   loopOnLastDL 0-  clearStack lastDL+  reset an'lastDL   -- Clear seen-  k <- sizeOfStack an'toClear+  k <- get' an'toClear   let-    vec' = asVec an'toClear+    vec' = asUVector an'toClear     cleaner :: Int -> IO ()     cleaner ((< k) -> False) = return ()     cleaner i = do@@ -263,26 +260,26 @@ -- *  @an'toClear@ is initialized by @ps@ in @analyze@ (a copy of 'learnt'). --   This is used only in this function and @analyze@. ---{-# INLINEABLE analyzeRemovable #-}+{-# INLINABLE 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+  reset an'stack      -- analyze_stack.clear()+  pushTo an'stack p   -- analyze_stack.push(p);+  top <- get' an'toClear   let     loopOnStack :: IO Bool     loopOnStack = do-      k <- sizeOfStack an'stack  -- int top = analyze_toclear.size();+      k <- get' an'stack  -- int top = analyze_toclear.size();       if 0 == k         then return True         else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL);-            sl <- lastOfStack an'stack-            popFromStack an'stack             -- analyze_stack.pop();-            c <- getNthClause reason (lit2var sl) -- getRoot sl-            nl <- sizeOfClause c+            sl <- lastOf an'stack+            popFrom an'stack             -- analyze_stack.pop();+            c <- getNth reason (lit2var sl) -- getRoot sl+            nl <- get' c             let-              cvec = asVec c+              cvec = asUVector c               loopOnLit :: Int -> IO Bool -- loopOnLit (int i = 1; i < c.size(); i++){               loopOnLit ((< nl) -> False) = loopOnStack               loopOnLit i = do@@ -292,20 +289,24 @@                 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'+                      c3 <- (NullClause /=) <$> getNth reason v'                       if c3 && testBit minLevel (l' .&. 31) -- if (reason[var(p)] != GClause_NULL && ((1 << (level[var(p)] & 31)) & min_level) != 0){                         then do                             setNth an'seen v' 1        -- analyze_seen[var(p)] = 1;-                            pushToStack an'stack p'    -- analyze_stack.push(p);-                            pushToStack an'toClear p'  -- analyze_toclear.push(p);+                            pushTo an'stack p'    -- analyze_stack.push(p);+                            pushTo an'toClear p'  -- analyze_toclear.push(p);                             loopOnLit $ i + 1                         else do                             -- loopOnLit (int j = top; j < analyze_toclear.size(); j++) analyze_seen[var(analyze_toclear[j])] = 0;-                            top' <- sizeOfStack an'toClear-                            let vec = asVec an'toClear-                            forM_ [top .. top' - 1] $ \j -> do x <- getNth vec j; setNth an'seen (lit2var x) 0+                            top' <- get' an'toClear+                            let+                              vec = asUVector an'toClear+                              clearAll :: Int -> IO ()+                              clearAll ((< top') -> False) = return ()+                              clearAll j = do x <- getNth vec j; setNth an'seen (lit2var x) 0; clearAll (j + 1)+                            clearAll top                             -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop-                            shrinkStack an'toClear $ top' - top+                            shrinkBy an'toClear $ top' - top                             return False                   else loopOnLit $ i + 1             loopOnLit 1@@ -320,14 +321,15 @@ --   making assumptions). If 'skip_first' is TRUE, the first literal of 'confl' is ignored (needed --   if conflict arose before search even started). --+{-# INLINABLE analyzeFinal #-} analyzeFinal :: Solver -> Clause -> Bool -> IO () analyzeFinal Solver{..} confl skipFirst = do-  clearStack conflict-  rl <- getInt rootLevel+  reset conflicts+  rl <- get' rootLevel   unless (rl == 0) $ do-    n <- sizeOfClause confl+    n <- get' confl     let-      lvec = asVec confl+      lvec = asUVector confl       loopOnConfl :: Int -> IO ()       loopOnConfl ((< n) -> False) = return ()       loopOnConfl i = do@@ -336,11 +338,11 @@         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+    tls <- get' trailLim+    trs <- get' trail+    tlz <- getNth (asUVector trailLim) 0     let-      trailVec = asVec trail+      trailVec = asUVector trail       loopOnTrail :: Int -> IO ()       loopOnTrail ((tlz <=) -> False) = return ()       loopOnTrail i = do@@ -348,13 +350,13 @@         let (x :: Var) = lit2var l         saw <- getNth an'seen x         when (saw == 1) $ do-          (r :: Clause) <- getNthClause reason x+          (r :: Clause) <- getNth reason x           if r == NullClause-            then pushToStack conflict (negateLit l)+            then pushTo conflicts (negateLit l)             else do-                k <- sizeOfClause r+                k <- get' r                 let-                  cvec = asVec r+                  cvec = asUVector r                   loopOnLits :: Int -> IO ()                   loopOnLits ((< k) -> False) = return ()                   loopOnLits j = do@@ -365,7 +367,7 @@                 loopOnLits 1         setNth an'seen x 0         loopOnTrail $ i - 1-    loopOnTrail =<< if tls <= rl then return (trs - 1) else getNth (asVec trailLim) rl+    loopOnTrail =<< if tls <= rl then return (trs - 1) else getNth (asUVector trailLim) rl  -- | M114: -- propagate : [void] -> [Clause+]@@ -396,25 +398,25 @@           loop $ i + 1       loop 1 -}-    trailVec = asVec trail+    trailVec = asUVector 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)+      (p :: Lit) <- getNth trailVec =<< get' qHead+      modify' qHead (+ 1)       let (ws :: ClauseExtManager) = getNthWatcher watches p-      end <- numberOfClauses ws+      end <- get' 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+--      rc <- getNth reason $ lit2var p+--      byGlue <- if (rc /= NullClause) && learnt rc then (== 2) <$> get' (lbd rc) else return False       let {-         checkAllLiteralsIn :: Clause -> IO () -- not in use         checkAllLiteralsIn c = do           nc <- sizeOfClause c           let-            vec = asVec c+            vec = asuVector c             loop :: Int -> IO ()             loop((< nc) -> False) = return ()             loop i = do@@ -425,23 +427,23 @@ -}         forClause :: Clause -> Int -> Int -> IO Clause         forClause confl i@((< end) -> False) j = do-          shrinkManager ws (i - j)-          while confl =<< ((<) <$> getInt qHead <*> sizeOfStack trail)+          shrinkBy ws (i - j)+          while confl =<< ((<) <$> get' qHead <*> get' trail)         forClause confl i j = do           (l :: Lit) <- getNth bvec i           bv <- if l == 0 then return lFalse else valueLit s l           if bv == lTrue             then do                  unless (i == j) $ do -- NOTE: if i == j, the path doesn't require accesses to cvec!-                   (c :: Clause) <- getNthClause cvec i-                   setNthClause cvec j c+                   (c :: Clause) <- getNth cvec i+                   setNth cvec j c                    setNth bvec j l                  forClause confl (i + 1) (j + 1)             else do                 -- checkAllLiteralsIn c-                (c :: Clause) <- getNthClause cvec i+                (c :: Clause) <- getNth cvec i                 let-                  lits = asVec c+                  lits = asUVector c                   falseLit = negateLit p                 -- Make sure the false literal is data[1]                 ((falseLit ==) <$> getNth lits 0) >>= (`when` swapBetween lits 0 1)@@ -449,27 +451,27 @@                 (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)+                  then setNth cvec j c >> setNth bvec j first >> forClause confl (i + 1) (j + 1)                   else do                       -- Look for new watch-                      cs <- sizeOfClause c+                      cs <- get' c                       let                         forLit :: Int -> IO Clause                         forLit ((< cs) -> False) = do                           -- Did not find watch; clause is unit under assignment:-                          setNthClause cvec j c+                          setNth cvec j c                           setNth bvec j 0                           result <- enqueue s first c                           if not result                             then do-                                ((== 0) <$> decisionLevel s) >>= (`when` setBool ok False)+                                ((== 0) <$> decisionLevel s) >>= (`when` set' ok False)                                 -- #BBCP-                                setInt qHead =<< sizeOfStack trail+                                set' qHead =<< get' 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 cvec j' =<< getNth cvec i'                                     setNth bvec j' =<< getNth bvec i'                                     copy (i' + 1) (j' + 1)                                 copy (i + 1) (j + 1)@@ -485,7 +487,7 @@                             else forLit $ k + 1                       forLit 2       forClause confl 0 0-  while NullClause =<< ((<) <$> getInt qHead <*> sizeOfStack trail)+  while NullClause =<< ((<) <$> get' qHead <*> get' trail)  -- | #M22 -- reduceDB: () -> [void]@@ -501,11 +503,11 @@   let     loop :: Int -> IO ()     loop ((< n) -> False) = return ()-    loop i = (removeWatch s =<< getNthClause vec i) >> loop (i + 1)+    loop i = (removeWatch s =<< getNth vec i) >> loop (i + 1)   k <- sortClauses s learnts (div n 2) -- k is the number of clauses not to be purged   loop k                               -- CAVEAT: `vec` is a zero-based vector-  garbageCollect watches-  shrinkManager learnts (n - k)+  reset watches+  shrinkBy learnts (n - k)  -- | (Good to Bad) Quick sort the key vector based on their activities and returns number of privileged clauses. -- this function uses the same metrix as reduceDB_lt in glucose 4.0:@@ -543,7 +545,7 @@     activityScale = fromIntegral activityMax     indexMax :: Int     indexMax = (2 ^ indexWidth - 1) -- 67,108,863 for 26-  n <- numberOfClauses cm+  n <- get' cm   -- when (indexMax < n) $ error $ "## The number of learnt clauses " ++ show n ++ " exceeds mios's " ++ show indexWidth ++" bit manage capacity"   vec <- getClauseVector cm   keys <- getKeyVector cm@@ -552,18 +554,18 @@     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+      c <- getNth vec i+      k <- (\k -> if k == 2 then return k else fromEnum <$> get' (protected c)) =<< get' c       case k of-        1 -> setBool (protected c) False >> setNth keys i (shiftL 2 indexWidth + i) >> assignKey (i + 1) (m + 1)+        1 -> set' (protected c) False >> setNth keys i (shiftL 2 indexWidth + i) >> assignKey (i + 1) (m + 1)         2 -> setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1)         _ -> do             l <- locked s c      -- this is expensive             if l               then setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1)               else do-                  d <- ranking' c-                  b <- floor . (activityScale *) . (1 -) . logBase claActivityThreshold . max 1 <$> getDouble (activity c)+                  d <- rankOf c+                  b <- floor . (activityScale *) . (1 -) . logBase claActivityThreshold . max 1 <$> get' (activity c)                   setNth keys i $ shiftL (min rankMax d) (activityWidth + indexWidth) + shiftL b indexWidth + i                   assignKey (i + 1) m   limit <- min n . (+ nneeds) <$> assignKey 0 0@@ -604,14 +606,14 @@     seek i = do       bits <- getNth keys i       when (indexMax < bits) $ do-        c <- getNthClause vec i+        c <- getNth 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'+              then setNth vec k c+              else getNth vec k' >>= setNth vec k >> sweep k'         sweep i       seek $ i + 1   seek 0@@ -628,22 +630,22 @@ {-# INLINABLE simplifyDB #-} simplifyDB :: Solver -> IO Bool simplifyDB s@Solver{..} = do-  good <- getBool ok+  good <- get' ok   if good     then do       p <- propagate s       if p /= NullClause-        then setBool ok False >> return False+        then set' ok False >> return False         else do             -- Clear watcher lists:-            n <- sizeOfStack trail+            n <- get' trail             let-              vec = asVec trail+              vec = asUVector trail               loopOnLit ((< n) -> False) = return ()               loopOnLit i = do                 l <- getNth vec i-                clearManager . getNthWatcher watches $ l-                clearManager . getNthWatcher watches $ negateLit l+                reset . getNthWatcher watches $ l+                reset . getNthWatcher watches $ negateLit l                 loopOnLit $ i + 1             loopOnLit 0             -- Remove satisfied clauses:@@ -653,20 +655,20 @@               for t = do                 let ptr = if t == 0 then learnts else clauses                 vec' <- getClauseVector ptr-                n' <- numberOfClauses ptr+                n' <- get' ptr                 let                   loopOnVector :: Int -> Int -> IO Bool-                  loopOnVector ((< n') -> False) j = shrinkManager ptr (n' - j) >> return True+                  loopOnVector ((< n') -> False) j = shrinkBy ptr (n' - j) >> return True                   loopOnVector i j = do-                        c <- getNthClause vec' i+                        c <- getNth vec' i                         l <- locked s c                         r <- simplify s c                         if not l && r                           then removeWatch s c >> loopOnVector (i + 1) j-                          else setNthClause vec' j c >> loopOnVector (i + 1) (j + 1)+                          else setNth vec' j c >> loopOnVector (i + 1) (j + 1)                 loopOnVector 0 0             ret <- for 0-            garbageCollect watches+            reset watches             return ret     else return False @@ -683,11 +685,11 @@ --   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 :: Solver -> Int -> Int -> IO Int search s@Solver{..} nOfConflicts nOfLearnts = do   -- clear model   let-    loop :: Int -> IO LiftedBool+    loop :: Int -> IO Int     loop conflictC = do       !confl <- propagate s       d <- decisionLevel s@@ -695,23 +697,23 @@         then do             -- CONFLICT             incrementStat s NumOfBackjump 1-            r <- getInt rootLevel+            r <- get' rootLevel             if d == r               then do                   -- Contradiction found:                   analyzeFinal s confl False-                  return LFalse+                  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)+--                    d <- get' varDecay+--                    when (d < 0.95) $ modify' 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+                  (s `cancelUntil`) . max backtrackLevel =<< get' rootLevel+                  newLearntClause s litsLearnt+                  k <- get' litsLearnt                   when (k == 1) $ do-                    (v :: Var) <- lit2var <$> getNth (asVec litsLearnt) 0+                    (v :: Var) <- lit2var <$> getNth (asUVector litsLearnt) 0                     setNth level v 0                   varDecayActivity s                   -- claDecayActivity s@@ -719,20 +721,26 @@         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+            k1 <- get' learnts             k2 <- nAssigns s             when (k1 - k2 >= nOfLearnts) $ reduceDB s -- Reduce the set of learnt clauses             case () of              _ | k2 == nVars -> do                    -- Model found:-                   forM_ [0 .. nVars - 1] $ \i -> setNthBool model i . (lTrue ==) =<< getNth assigns (i + 1)-                   return LTrue+                   let+                     toInt :: Var -> IO Lit+                     toInt v = (\p -> if lTrue == p then v else negate v) <$> valueVar s v+                     setModel :: Int -> IO ()+                     setModel ((<= nVars) -> False) = return ()+                     setModel v = (setNth model v =<< toInt v) >> setModel (v + 1)+                   setModel 1+                   return lTrue              _ | conflictC >= nOfConflicts -> do                    -- Reached bound on number of conflicts-                   (s `cancelUntil`) =<< getInt rootLevel -- force a restart+                   (s `cancelUntil`) =<< get' rootLevel -- force a restart                    claRescaleActivityAfterRestart s                    incrementStat s NumOfRestart 1-                   return Bottom+                   return lBottom              _ -> do                -- New variable decision:                v <- select s -- many have heuristic for polarity here@@ -741,8 +749,8 @@                unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@                -- >> #phasesaving                loop conflictC-  good <- getBool ok-  if good then loop 0 else return LFalse+  good <- get' ok+  if good then loop 0 else return lFalse  -- | __Fig. 16. (p.20)__ -- Main solve method.@@ -750,6 +758,7 @@ -- __Pre-condition:__ If assumptions are used, 'simplifyDB' must be -- called right before using this method. If not, a top-level conflict (resulting in a -- non-usable internal state) cannot be distinguished from a conflict under assumptions.+{-# INLINABLE solve #-} solve :: (Foldable t) => Solver -> t Lit -> IO Bool solve s@Solver{..} assumps = do   -- PUSH INCREMENTAL ASSUMPTIONS:@@ -760,9 +769,9 @@       b <- assume s a       if not b         then do                 -- conflict analyze-            (confl :: Clause) <- getNthClause reason (lit2var a)+            (confl :: Clause) <- getNth reason (lit2var a)             analyzeFinal s confl True-            pushToStack conflict (negateLit a)+            pushTo conflicts (negateLit a)             cancelUntil s 0             return False         else do@@ -778,33 +787,31 @@   if not x     then return False     else do-        setInt rootLevel =<< decisionLevel s+        set' rootLevel =<< decisionLevel s         -- SOLVE:         nc <- fromIntegral <$> nClauses s         let           while :: Double -> Double -> IO Bool           while nOfConflicts nOfLearnts = do             status <- search s (floor nOfConflicts) (floor nOfLearnts)-            if status == Bottom+            if status == lBottom               then while (1.5 * nOfConflicts) (1.1 * nOfLearnts)-              else cancelUntil s 0 >> return (status == LTrue)+              else cancelUntil s 0 >> return (status == lTrue)         while 100 (nc / 3.0) ------ 'enqueue' is defined in 'Solver'; most functions in M114 use 'unsafeEnqueue'---+-- | Though 'enqueue' is defined in 'Solver', most functions in M114 use @unsafeEnqueue@. {-# INLINABLE unsafeEnqueue #-} unsafeEnqueue :: Solver -> Lit -> Clause -> IO () unsafeEnqueue s@Solver{..} p from = do   let v = lit2var p   setNth assigns v $! if positiveLit p then lTrue else lFalse   setNth level v =<< decisionLevel s-  setNthClause reason v from     -- NOTE: @from@ might be NULL!-  pushToStack trail p+  setNth reason v from     -- NOTE: @from@ might be NULL!+  pushTo trail p --- __Pre-condition:__ propagation queue is empty+-- | __Pre-condition:__ propagation queue is empty. {-# INLINE unsafeAssume #-} unsafeAssume :: Solver -> Lit -> IO () unsafeAssume s@Solver{..} p = do-  pushToStack trailLim =<< sizeOfStack trail+  pushTo trailLim =<< get' trail   unsafeEnqueue s p NullClause

@@ -1,4 +1,3 @@-{-# LANGUAGE BangPatterns #-} {-# LANGUAGE Safe #-}  -- | command line option parser for mios@@ -18,7 +17,7 @@  import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo) import System.Environment (getArgs)-import SAT.Mios.Internal (MiosConfiguration (..), defaultConfiguration)+import SAT.Mios.Types (MiosConfiguration (..), defaultConfiguration)  -- | configuration swithces data MiosProgramOption = MiosProgramOption

@@ -12,7 +12,9 @@        (          -- * Solver          Solver (..)+       , VarHeap        , newSolver+       , getModel          -- * Misc Accessors        , nAssigns        , nClauses@@ -20,13 +22,13 @@        , decisionLevel        , valueVar        , valueLit+--       , oldLit        , locked          -- * State Modifiers        , addClause        , enqueue        , assume        , cancelUntil-       , getModel          -- * Activities        , claBumpActivity --       , claDecayActivity@@ -43,165 +45,177 @@        )         where -import Control.Monad ((<=<), forM_, unless, when)+import Control.Monad (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+{-            Public Interface -}+                model      :: !(Vec Int)         -- ^ If found, this vector has the model+              , conflicts  :: !Stack             -- ^ Set of literals in the case of conflicts+{-            Clause Database -}               , clauses    :: !ClauseExtManager  -- ^ List of problem constraints.               , learnts    :: !ClauseExtManager  -- ^ List of learnt clauses.-              , watches    :: !WatcherList       -- ^ 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+              , watches    :: !WatcherList       -- ^ list of constraint wathing 'p', literal-indexed+{-            Assignment Management -}+              , assigns    :: !(Vec Int)         -- ^ The current assignments indexed on variables+              , phases     :: !(Vec Int)         -- ^ The last assignments indexed on variables+              , trail      :: !Stack             -- ^ List of assignments in chronological order               , trailLim   :: !Stack             -- ^ Separator indices for different decision levels in 'trail'.-              , qHead      :: !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+              , qHead      :: !Int'              -- ^ 'trail' is divided at qHead; assignment part and queue part+              , reason     :: !ClauseVector      -- ^ For each variable, the constraint that implied its value+              , level      :: !(Vec Int)         -- ^ For each variable, the decision level it was assigned+{-            Variable Order -}+              , activities :: !(Vec Double)      -- ^ Heuristic measurement of the activity of a variable               , order      :: !VarHeap           -- ^ Keeps track of the dynamic variable order.-                -- Configuration+{-            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 {-+              -- , claInc     :: !Double'           -- ^ Clause activity increment amount to bump with.+              -- , varDecay   :: !Double'           -- ^ used to set 'varInc'+-}+              , varInc     :: !Double'           -- ^ Variable activity increment amount to bump with.+              , rootLevel  :: !Int'              -- ^ Separates incremental and search assumptions.+{-            Working Memory -}+              , ok         :: !Bool'             -- ^ /return value/ holder+              , an'seen    :: !(Vec Int)         -- ^ used in 'SAT.Mios.Main.analyze'+              , an'toClear :: !Stack             -- ^ used in 'SAT.Mios.Main.analyze'+              , an'stack   :: !Stack             -- ^ used in 'SAT.Mios.Main.analyze'+              , an'lastDL  :: !Stack             -- ^ last decision level used in 'SAT.Mios.Main.analyze'+              , litsLearnt :: !Stack             -- ^ used in 'SAT.Mios.Main.analyze' and 'SAT.Mios.Main.search' to create a learnt clause++{-+              -- , pr'seen    :: !(Vec Int)         -- ^ used in 'SAT.Mios.Main.propagate'+-}+              , stats      :: !(UVector Int)     -- ^ statistics information holder+{-               , lbd'seen   :: !Vec               -- ^ used in lbd computation-              , lbd'key    :: !IntSingleton      -- ^ used in lbd computation+              , lbd'key    :: !Int'              -- ^ used in lbd computation -}               } --- | returns an everything-is-initialized solver from the arguments+-- | 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+    <$> newVec nv 0                        -- model+    <*> newStack nv                        -- coflict     -- Clause Database-    <*> newManager nc                                 -- clauses-    <*> newManager nc                                 -- learnts-    <*> newWatcherList nv 2                           -- watches+    <*> 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+    <*> newVec nv lBottom                  -- assigns+    <*> newVec nv lBottom                  -- phases+    <*> newStack nv                        -- trail+    <*> newStack nv                        -- trailLim+    <*> new' 0                             -- qHead+    <*> newClauseVector (nv + 1)           -- reason+    <*> newVec nv (-1)                     -- level     -- Variable Order-    <*> newVecDouble (nv + 1) 0                       -- activities-    <*> newVarHeap nv                                 -- order+    <*> newVec nv 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+    <*> return conf                        -- config+    <*> return nv                          -- nVars+--  <*> new' 1.0                           -- claInc+--  <*> new' (variableDecayRate conf)      -- varDecay+    <*> new' 1.0                           -- varInc+    <*> new' 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+    <*> new' True                          -- ok+    <*> newVec nv 0                        -- an'seen+    <*> newStack nv                        -- an'toClear+    <*> newStack nv                        -- an'stack+--    <*> newVec nv (-1)                     -- pr'seen+    <*> newStack nv                        -- litsLearnt+    <*> newStack nv                        -- lastDL+    <*> newVec (fromEnum EndOfStatIndex) 0 -- stats {----    <*> newVec nv                                     -- lbd'seen---    <*> newInt 0                                      -- lbd'key+--    <*> newVec nv                        -- lbd'seen+--    <*> newInt 0                         -- lbd'key -}  -------------------------------------------------------------------------------- -- Accessors --- | returns the number of current assigments+-- | returns the number of current assigments. {-# INLINE nAssigns #-} nAssigns :: Solver -> IO Int-nAssigns = sizeOfStack . trail+nAssigns = get' . trail --- | returns the number of constraints (clauses)+-- | returns the number of constraints (clauses). {-# INLINE nClauses #-}-nClauses  :: Solver -> IO Int-nClauses = numberOfClauses . clauses+nClauses :: Solver -> IO Int+nClauses = get' . clauses --- | returns the number of learnt clauses+-- | returns the number of learnt clauses. {-# INLINE nLearnts #-} nLearnts :: Solver -> IO Int-nLearnts = numberOfClauses . learnts+nLearnts = get' . learnts --- | return the model as a list of literal+-- | returns 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)+getModel = asList . model --- | returns the current decision level+-- | returns the current decision level. {-# INLINE decisionLevel #-} decisionLevel :: Solver -> IO Int-decisionLevel = sizeOfStack . trailLim+decisionLevel = get' . trailLim --- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Var'+-- | 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'+-- | 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)+valueLit :: Solver -> Lit -> IO Int+valueLit (assigns -> a) p = (\x -> if positiveLit p then x else negate x) <$> getNth a (lit2var p) +{-+-- | returns the assignment (:: 'LiftedBool' = @[-1, 0, -1]@) from 'Lit' in phases.+{-# INLINE oldLit #-}+oldLit :: Solver -> Lit -> IO Lit+oldLit (phases -> a) (lit2var -> v) = (var2lit v . (== 1)) <$> getNth a v+-}+ -- | __Fig. 7. (p.11)__ -- returns @True@ if the clause is locked (used as a reason). __Learnt clauses only__ {-# INLINE locked #-} locked :: Solver -> Clause -> IO Bool-locked s c = (c ==) <$> (getNthClause (reason s) . lit2var =<< getNth (lits c) 1)+locked s c = (c ==) <$> (getNth (reason s) . lit2var =<< getNth (lits c) 1)  -------------------------------------------------------------------------------- Statistics  -- | stat index data StatIndex =-    NumOfBackjump-  | NumOfRestart+    NumOfBackjump               -- ^ the number of backjump+  | NumOfRestart                -- ^ the number of restart+  | EndOfStatIndex              -- ^ Don't use this dummy.   deriving (Bounded, Enum, Eq, Ord, Read, Show) --- | returns the value of 'StatIndex'+-- | returns the value of 'StatIndex'. {-# INLINE getStat #-} getStat :: Solver -> StatIndex -> IO Int getStat (stats -> v) (fromEnum -> i) = getNth v i --- | sets to 'StatIndex'+-- | 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'+-- | 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+-- | returns the statistics as a list. {-# INLINABLE getStats #-} getStats :: Solver -> IO [(StatIndex, Int)] getStats (stats -> v) = mapM (\i -> (i, ) <$> getNth v (fromEnum i)) [minBound .. maxBound :: StatIndex]@@ -211,16 +225,14 @@ -- | 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 :: Solver -> Stack -> 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+   Left b  -> return b   -- No new clause was returned becaues a confilct occured or the clause is a literal+   Right c -> pushTo clauses c >> return True --- | __Fig. 8. (p.12)__ create a new clause and adds it to watcher lists+-- | __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.@@ -230,8 +242,12 @@ -- For the propagation to work, the second watch must be put on the literal which will -- first be unbound by backtracking. (Note that none of the learnt-clause specific things -- needs to done for a user defined contraint type.)+--+-- * @Left False@ if the clause is in a confilct+-- * @Left True@ if the clause is satisfied+-- * @Right clause@ if the clause is enqueued successfully {-# INLINABLE clauseNew #-}-clauseNew :: Solver -> Vec -> Bool -> IO (Bool, Clause)+clauseNew :: Solver -> Stack -> Bool -> IO (Either Bool Clause) clauseNew s@Solver{..} ps isLearnt = do   -- now ps[0] is the number of living literals   exit <- do@@ -246,11 +262,11 @@                    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+             _ | - y == l -> reset ps >> return True -- p and negateLit p occurs in ps              _ -> handle (j + 1) l n       loopForLearnt :: Int -> IO Bool       loopForLearnt i = do-        n <- getNth ps 0+        n <- get' ps         if n < i           then return False           else do@@ -261,14 +277,14 @@                 else loopForLearnt $ i + 1       loop :: Int -> IO Bool       loop i = do-        n <- getNth ps 0+        n <- get' ps         if n < i           then return False           else do               l <- getNth ps i     -- check the i-th literal's satisfiability-              sat <- valueLit s l                                      -- any literal in ps is true+              sat <- valueLit s l  -- any literal in ps is true               case sat of-               1  -> setNth ps 0 0 >> return True+               1  -> reset ps >> return True                -1 -> do                  swapBetween ps i n                  modifyNth ps (subtract 1) 0@@ -279,16 +295,16 @@                    then return True                    else loop $ i + 1     if isLearnt then loopForLearnt 1 else loop 1-  k <- getNth ps 0+  k <- get' ps   case k of-   0 -> return (exit, NullClause)+   0 -> return (Left exit)    1 -> do      l <- getNth ps 1-     (, NullClause) <$> enqueue s l NullClause+     Left <$> enqueue s l NullClause    _ -> do-     -- allocate clause:-     c <- newClauseFromVec isLearnt ps-     let vec = asVec c+    -- allocate clause:+     c <- newClauseFromStack isLearnt ps+     let vec = asUVector c      when isLearnt $ do        -- Pick a second literal to watch:        let@@ -296,6 +312,7 @@          findMax ((< k) -> False) j _ = return j          findMax i j val = do            v' <- lit2var <$> getNth vec i+           varBumpActivity s v' -- this is a just good chance to bump activities of literals in this clause            a <- getNth assigns v'            b <- getNth level v'            if (a /= lBottom) && (val < b)@@ -309,13 +326,12 @@        -- 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)+     return (Right c)  -- | __Fig. 9 (p.14)__ -- Puts a new fact on the propagation queue, as well as immediately updating the variable's value@@ -328,9 +344,9 @@ {-   -- bump psedue lbd of @from@   when (from /= NullClause && learnt from) $ do-    l <- getInt (lbd from)+    l <- get' (lbd from)     k <- (12 +) <$> decisionLevel s-    when (k < l) $ setInt (lbd from) k+    when (k < l) $ set' (lbd from) k -}   let signumP = if positiveLit p then lTrue else lFalse   let v = lit2var p@@ -342,8 +358,8 @@         -- 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+        setNth reason v from     -- NOTE: @from@ might be NULL!+        pushTo trail p         return True  -- | __Fig. 12 (p.17)__@@ -353,7 +369,7 @@ {-# INLINE assume #-} assume :: Solver -> Lit -> IO Bool assume s p = do-  pushToStack (trailLim s) =<< sizeOfStack (trail s)+  pushTo (trailLim s) =<< get' (trail s)   enqueue s p NullClause  -- | #M22: Revert to the states at given level (keeping all assignment at 'level' but not beyond).@@ -362,11 +378,11 @@ cancelUntil s@Solver{..} lvl = do   dl <- decisionLevel s   when (lvl < dl) $ do-    let tr = asVec trail-    let tl = asVec trailLim+    let tr = asUVector trail+    let tl = asUVector trailLim     lim <- getNth tl lvl-    ts <- sizeOfStack trail-    ls <- sizeOfStack trailLim+    ts <- get' trail+    ls <- get' trailLim     let       loopOnTrail :: Int -> IO ()       loopOnTrail ((lim <=) -> False) = return ()@@ -377,20 +393,21 @@         -- #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+        setNth reason x NullClause -- 'analyze` uses reason without checking assigns         -- FIXME: #polarity https://github.com/shnarazk/minisat/blosb/master/core/Solver.cc#L212         undo s x         -- insertHeap s x              -- insertVerOrder         loopOnTrail $ c - 1     loopOnTrail $ ts - 1-    shrinkStack trail (ts - lim)-    shrinkStack trailLim (ls - lvl)-    setInt qHead =<< sizeOfStack trail+    shrinkBy trail (ts - lim)+    shrinkBy trailLim (ls - lvl)+    set' qHead =<< get' trail  -------------------------------------------------------------------------------- VarOrder  -- | Interfate to select a decision var based on variable activity. instance VarOrder Solver where+{-   -- | __Fig. 6. (p.10)__   -- Creates a new SAT variable in the solver.   newVar _ = return 0@@ -405,6 +422,7 @@     -- newVar order     -- growQueueSized (i + 1) propQ     -- return i+-}   {-# SPECIALIZE INLINE update :: Solver -> Var -> IO () #-}   update = increaseHeap   {-# SPECIALIZE INLINE undo :: Solver -> Var -> IO () #-}@@ -430,6 +448,7 @@ varActivityThreshold :: Double varActivityThreshold = 1e100 +-- | value for rescaling clause activity. claActivityThreshold :: Double claActivityThreshold = 1e20 @@ -437,32 +456,35 @@ {-# INLINE varBumpActivity #-} varBumpActivity :: Solver -> Var -> IO () varBumpActivity s@Solver{..} x = do-  !a <- (+) <$> getNthDouble x activities <*> getDouble varInc-  setNthDouble x activities a+  !a <- (+) <$> getNth activities x <*> get' varInc+  setNth activities x a   when (varActivityThreshold < a) $ varRescaleActivity s   update s x                    -- update the position in heap  -- | __Fig. 14 (p.19)__-{-# INLINE varDecayActivity #-}+{-# INLINABLE varDecayActivity #-} varDecayActivity :: Solver -> IO ()-varDecayActivity Solver{..} = modifyDouble varInc (/ variableDecayRate config)+varDecayActivity Solver{..} = modify' varInc (/ variableDecayRate config) -- varDecayActivity Solver{..} = modifyDouble varInc . (flip (/)) =<< getDouble varDecay  -- | __Fig. 14 (p.19)__-{-# INLINE varRescaleActivity #-}+{-# INLINABLE varRescaleActivity #-} varRescaleActivity :: Solver -> IO () varRescaleActivity Solver{..} = do-  forM_ [1 .. nVars] $ \i -> modifyNthDouble i activities (/ varActivityThreshold)-  modifyDouble varInc (/ varActivityThreshold)+  let+    loop ((<= nVars) -> False) = return ()+    loop i = modifyNth activities (/ varActivityThreshold) i >> loop (i + 1)+  loop 1+  modify' varInc (/ varActivityThreshold)  -- | __Fig. 14 (p.19)__ {-# INLINE claBumpActivity #-} claBumpActivity :: Solver -> Clause -> IO () claBumpActivity s Clause{..} = do   dl <- decisionLevel s-  a <- (fromIntegral dl +) <$> getDouble activity-  setDouble activity a-  -- setBool protected True+  a <- (fromIntegral dl +) <$> get' activity+  set' activity a+  -- set' protected True   when (claActivityThreshold <= a) $ claRescaleActivity s  {-@@ -473,66 +495,66 @@ -}  -- | __Fig. 14 (p.19)__-{-# INLINE claRescaleActivity #-}+{-# INLINABLE claRescaleActivity #-} claRescaleActivity :: Solver -> IO () claRescaleActivity Solver{..} = do   vec <- getClauseVector learnts-  n <- numberOfClauses learnts+  n <- get' learnts   let     loopOnVector :: Int -> IO ()     loopOnVector ((< n) -> False) = return ()     loopOnVector i = do-      c <- getNthClause vec i-      modifyDouble (activity c) (/ claActivityThreshold)+      c <- getNth vec i+      modify' (activity c) (/ claActivityThreshold)       loopOnVector $ i + 1   loopOnVector 0   -- modifyDouble claInc (/ claActivityThreshold)  -- | __Fig. 14 (p.19)__-{-# INLINE claRescaleActivityAfterRestart #-}+{-# INLINABLE claRescaleActivityAfterRestart #-} claRescaleActivityAfterRestart :: Solver -> IO () claRescaleActivityAfterRestart Solver{..} = do   vec <- getClauseVector learnts-  n <- numberOfClauses learnts+  n <- get' learnts   let     loopOnVector :: Int -> IO ()     loopOnVector ((< n) -> False) = return ()     loopOnVector i = do-      c <- getNthClause vec i-      d <- sizeOfClause c+      c <- getNth vec i+      d <- get' c       if d < 9-        then modifyDouble (activity c) sqrt-        else setDouble (activity c) 0-      setBool (protected c) False+        then modify' (activity c) sqrt+        else set' (activity c) 0+      set' (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+-- | 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)+                  heap :: !Stack  -- order to var+                , idxs :: !Stack  -- var to order (index)                 }  newVarHeap :: Int -> IO VarHeap newVarHeap n = do-  v1 <- newVec (n + 1)-  v2 <- newVec (n + 1)+  v1 <- newVec n 0+  v2 <- newVec n 0   let     loop :: Int -> IO ()-    loop ((<= n) -> False) = setNth v1 0 n >> setNth v2 0 n+    loop ((<= n) -> False) = set' v1 n >> set' v2 n     loop i = setNth v1 i i >> setNth v2 i i >> loop (i + 1)   loop 1   return $ VarHeap v1 v2  {-# INLINE numElementsInHeap #-} numElementsInHeap :: Solver -> IO Int-numElementsInHeap (order -> heap -> h) = getNth h 0+numElementsInHeap = get' . heap . order  {-# INLINE inHeap #-} inHeap :: Solver -> Var -> IO Bool@@ -547,7 +569,7 @@ percolateUp Solver{..} start = do   let VarHeap to at = order   v <- getNth to start-  ac <- getNthDouble v activities+  ac <- getNth activities v   let     loop :: Int -> IO ()     loop i = do@@ -556,7 +578,7 @@         then setNth to i v >> setNth at v i -- end         else do             v' <- getNth to iP-            acP <- getNthDouble v' activities+            acP <- getNth activities v'             if ac > acP               then setNth to i v' >> setNth at v' i >> loop iP -- loop               else setNth to i v >> setNth at v i              -- end@@ -568,7 +590,7 @@   let (VarHeap to at) = order   n <- getNth to 0   v <- getNth to start-  ac <- getNthDouble v activities+  ac <- getNth activities v   let     loop :: Int -> IO ()     loop i = do@@ -578,8 +600,8 @@             let iR = iL + 1     -- right             l <- getNth to iL             r <- getNth to iR-            acL <- getNthDouble l activities-            acR <- getNthDouble r activities+            acL <- getNth activities l+            acR <- getNth activities r             let (ci, child, ac') = if iR <= n && acL < acR then (iR, r, acR) else (iL, l, acL)             if ac' > ac               then setNth to i child >> setNth at child i >> loop ci@@ -587,17 +609,17 @@         else setNth to i v >> setNth at v i       -- end   loop start -{-# INLINE insertHeap #-}+{-# INLINABLE insertHeap #-} insertHeap :: Solver -> Var -> IO () insertHeap s@(order -> VarHeap to at) v = do   n <- (1 +) <$> getNth to 0   setNth at v n   setNth to n v-  setNth to 0 n+  set' to n   percolateUp s n --- | renamed from 'getmin'-{-# INLINE getHeapRoot #-}+-- | returns the value on the root (renamed from @getmin@).+{-# INLINABLE getHeapRoot #-} getHeapRoot :: Solver -> IO Int getHeapRoot s@(order -> VarHeap to at) = do   r <- getNth to 1

@@ -1,21 +1,13 @@ {-# LANGUAGE     BangPatterns-  , FlexibleContexts-  , FlexibleInstances-  , FunctionalDependencies   , MultiParamTypeClasses   #-}-{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE Safe #-}  -- | 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 (..)+         module SAT.Mios.Vec          -- *  Variable        , Var        , bottomVar@@ -25,64 +17,37 @@        , lit2int        , int2lit        , bottomLit-       , newLit+--       , newLit        , positiveLit        , lit2var        , var2lit        , negateLit-         -- * Assignment-       , LiftedBool (..)-       , lbool+         -- * Assignment on the lifted Bool domain+--       , LiftedBool (..)+--       , lbool        , lFalse        , lTrue        , lBottom        , VarOrder (..)          -- * CNF        , CNFDescription (..)+         -- * Solver Configuration+       , MiosConfiguration (..)+       , defaultConfiguration        )        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+import SAT.Mios.Vec --- | represents "Var"+-- | 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+-- | converts a usual Int as literal to an internal 'Var' presentation. -- -- >>> int2var 1 -- 1  -- the first literal is the first variable@@ -92,6 +57,7 @@ -- 2 -- literal @-2@ is corresponding to variable 2 -- {-# INLINE int2var #-}+int2var :: Int -> Int int2var = abs  -- | The literal data has an 'index' method which converts the literal to@@ -104,9 +70,11 @@ bottomLit :: Lit bottomLit = 0 +{- -- | converts "Var" into 'Lit' newLit :: Var -> Lit newLit = error "newLit undefined"+-}  -- | returns @True@ if the literal is positive {-# INLINE positiveLit #-}@@ -125,13 +93,13 @@ -- 4 {-# INLINE negateLit #-} negateLit :: Lit -> Lit-negateLit !l = complementBit l 0 -- if even l then l + 1 else l - 1+negateLit l = complementBit l 0 -- if even l then l + 1 else l - 1  ---------------------------------------- ----------------- Var ---------------------------------------- --- | converts 'Lit' into 'Var'+-- | converts 'Lit' into 'Var'. -- -- >>> lit2var 2 -- 1@@ -145,7 +113,7 @@ lit2var :: Lit -> Var lit2var !n = shiftR n 1 --- | converts a 'Var' to the corresponing literal+-- | converts a 'Var' to the corresponing literal. -- -- >>> var2lit 1 True -- 2@@ -164,7 +132,7 @@ ----------------- Int ---------------------------------------- --- | converts 'Int' into 'Lit' as @lit2int . int2lit == id@+-- | converts 'Int' into 'Lit' as @lit2int . int2lit == id@. -- -- >>> int2lit 1 -- 2@@ -181,7 +149,7 @@   | 0 < n = 2 * n   | otherwise = -2 * n + 1 --- | converts `Lit' into 'Int' as @int2lit . lit2int == id@+-- | converts `Lit' into 'Int' as @int2lit . lit2int == id@. -- -- >>> lit2int 2 -- 1@@ -197,6 +165,7 @@   (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@@ -217,16 +186,17 @@ lbool :: Bool -> LiftedBool lbool True = LTrue lbool False = LFalse+-} --- | A contant representing False+-- | /FALSE/ on the Lifted Bool domain lFalse:: Int lFalse = -1 --- | A constant representing True+-- | /TRUE/ on the Lifted Bool domain lTrue :: Int lTrue = 1 --- | A constant for "undefined"+-- | /UNDEFINED/ on the Lifted Bool domain lBottom :: Int lBottom = 0 @@ -235,35 +205,53 @@ -- 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 :: (VecFamily v1 Bool, VecFamily v2 Double) => v1 -> v2 -> IO o   newVarOrder _ _ = error "newVarOrder undefined"    -- | Called when a new variable is created.   newVar :: o -> IO Var   newVar = error "newVar undefined"--  -- | Called when variable has increased in activity.+-}+  -- | should be called when a variable has increased in activity.   update :: o -> Var -> IO ()   update _  = error "update undefined"--  -- | Called when all variables have been assigned new activities.+{-+  -- | should be called when all variables have been assigned.   updateAll :: o -> IO ()   updateAll = error "updateAll undefined"--  -- | Called when variable is unbound (may be selected again).+-}+  -- | should be called when a variable becomes unbound (may be selected again).   undo :: o -> Var -> IO ()   undo _ _  = error "undo undefined" -  -- | Called to select a new, unassigned variable.+  -- | returns a new, unassigned var as the next decision.   select :: o -> IO Var   select    = error "select undefined" --- | misc information on CNF+-- | Misc information on a CNF data CNFDescription = CNFDescription   {-    _numberOfVariables :: !Int           -- ^ number of variables-  , _numberOfClauses :: !Int             -- ^ number of clauses+    _numberOfVariables :: !Int           -- ^ the number of variables+  , _numberOfClauses :: !Int             -- ^ the number of clauses   , _pathname :: Maybe FilePath          -- ^ given filename   }   deriving (Eq, Ord, Show)++-- | Solver's parameters; random decision rate was dropped.+data MiosConfiguration = MiosConfiguration+                         {+                           variableDecayRate  :: !Double  -- ^ decay rate for variable activity+--                         , clauseDecayRate    :: !Double  -- ^ decay rate for clause activity+                         }++-- | dafault configuration+--+-- * Minisat-1.14 uses @(0.95, 0.999, 0.2 = 20 / 1000)@.+-- * Minisat-2.20 uses @(0.95, 0.999, 0)@.+-- * Gulcose-4.0  uses @(0.8 , 0.999, 0)@.+-- * Mios-1.2     uses @(0.95, 0.999, 0)@.+--+defaultConfiguration :: MiosConfiguration+defaultConfiguration = MiosConfiguration 0.95 {- 0.999 -} {- 0 -}

@@ -1,31 +0,0 @@-{-# 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_

@@ -1,73 +0,0 @@-{-# 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 []

@@ -1,130 +0,0 @@-{-# 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 []

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

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

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

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

@@ -19,9 +19,9 @@ -- | 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+  assignment <- newVec (1 + nVars s) (0 :: Int) :: IO (Vec Int)   vec <- getClauseVector (clauses s)-  nc <- numberOfClauses (clauses s)+  nc <- get' (clauses s)   let     inject :: Lit -> IO ()     inject l = setNth assignment (lit2var l) $ if positiveLit l then lTrue else lFalse@@ -40,8 +40,7 @@     loopOnVector :: Int -> IO Bool     loopOnVector ((< nc) -> False) = return True     loopOnVector i = do-      c <- getNthClause vec i-      sat' <- satAny =<< asList c+      sat' <- satAny =<< asList =<< getNth vec i       if sat' then loopOnVector (i + 1) else return False   if null lst     then error "validator got an empty assignment."

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

@@ -0,0 +1,26 @@+module Main where+import SAT.Mios (CNFDescription (..), solveSAT)++-- | a sample CNF+clauses :: [[Int]]+clauses =+  [+    [ 1,  2]+  , [ 1,  3]+  , [-1, -2]+  , [1, -2, 3]+  , [-3]+  ]++-- | a property holder+desc :: CNFDescription+desc = CNFDescription           -- :: Int -> Int -> Maybe String -> CNFDescription+       (maximum . map abs . concat $ clauses) -- number of variables+       (length clauses)                       -- number of clauses+       Nothing                                -- Just pathname or Nothing++main :: IO ()+main = do+  -- solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int]+  asg <- solveSAT desc clauses+  putStrLn $ if null asg then "unsatisfiable" else show asg

@@ -2,7 +2,7 @@ -- see http://haskell.org/cabal/users-guide/  name:                   mios-version:                1.3.0+version:                1.4.0 synopsis:               A Minisat-based SAT solver in Haskell description: @@ -20,7 +20,12 @@ category:               Artificial Intelligence, Constraints build-type:             Simple cabal-version:          >=1.16+extra-source-files:  app/sample.hs +source-repository head+  type:                 git+  location:             https://github.com/shnarazk/mios+ Flag llvm   Description:	        Compile with llvm   Default:	        False@@ -35,62 +40,59 @@   else     buildable:	        False   default-language:	Haskell2010-  default-extensions:  Strict+  default-extensions:   Strict+  other-extensions:	    BangPatterns+                            FlexibleContexts+                            FlexibleInstances+                            FunctionalDependencies+                            MagicHash+                            MultiParamTypeClasses+                            RecordWildCards+                            ScopedTypeVariables+                            TypeFamilies+                            Trustworthy+                            TupleSections+                            Safe+                            UndecidableInstances+                            ViewPatterns   exposed-modules:-                        SAT.Mios                         SAT.Mios.Clause                         SAT.Mios.ClauseManager-                        SAT.Mios.Data.VecBool-                        SAT.Mios.Data.VecDouble-                        SAT.Mios.Data.Vec-                        SAT.Mios.Data.Singleton-                        SAT.Mios.Data.Stack-                        SAT.Mios.Internal+                        SAT.Mios.Vec                         SAT.Mios.Main                         SAT.Mios.OptionParser---                        SAT.Mios.Ranking                         SAT.Mios.Solver                         SAT.Mios.Types                         SAT.Mios.Validator-                        SAT.Mios.Util.CNFIO-                        SAT.Mios.Util.CNFIO.MinisatReader-                        SAT.Mios.Util.CNFIO.Reader-                        SAT.Mios.Util.CNFIO.Writer+                        SAT.Mios.Util.DIMACS.MinisatReader+                        SAT.Mios.Util.DIMACS.Reader+                        SAT.Mios.Util.DIMACS.Writer+                        SAT.Mios.Util.DIMACS                         SAT.Mios.Util.BoolExp-  build-depends:        base ==4.9.*, vector >=0.11, containers >=0.5, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6+                        SAT.Mios+  build-depends:        base ==4.9.*, vector >=0.11, ghc-prim >=0.5, bytestring >=0.10   if flag(llvm)     ghc-options:	-O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3   else-    ghc-options:	-O2 -ignore-asserts -funbox-strict-fields -msse4.2+    ghc-options:	-O2 -ignore-asserts -funbox-strict-fields  executable mios   main-is:              app/mios.hs   buildable:	        True   default-language:	Haskell2010   default-extensions:  Strict-  build-depends:        base ==4.9.*, vector >=0.11, containers >=0.5, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6+  build-depends:        base ==4.9.*,  vector >=0.11, ghc-prim >=0.5, bytestring >=0.10   if flag(llvm)     ghc-options:	-O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O3   else-    ghc-options:	-O2 -ignore-asserts -funbox-strict-fields -msse4.2+    ghc-options:	-O2 -ignore-asserts -funbox-strict-fields   other-modules:-                        SAT.Mios                         SAT.Mios.Clause                         SAT.Mios.ClauseManager-                        SAT.Mios.Data.VecBool-                        SAT.Mios.Data.VecDouble-                        SAT.Mios.Data.Vec-                        SAT.Mios.Data.Singleton-                        SAT.Mios.Data.Stack-                        SAT.Mios.Internal+                        SAT.Mios.Vec                         SAT.Mios.Main                         SAT.Mios.OptionParser---                        SAT.Mios.Ranking                         SAT.Mios.Solver                         SAT.Mios.Types                         SAT.Mios.Validator-                        SAT.Mios.Util.CNFIO-                        SAT.Mios.Util.CNFIO.MinisatReader-                        SAT.Mios.Util.CNFIO.Reader-                        SAT.Mios.Util.CNFIO.Writer-                        SAT.Mios.Util.BoolExp+                        SAT.Mios