diff --git a/SAT/Mios.hs b/SAT/Mios.hs --- a/SAT/Mios.hs +++ b/SAT/Mios.hs @@ -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 diff --git a/SAT/Mios/Clause.hs b/SAT/Mios/Clause.hs --- a/SAT/Mios/Clause.hs +++ b/SAT/Mios/Clause.hs @@ -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 diff --git a/SAT/Mios/ClauseManager.hs b/SAT/Mios/ClauseManager.hs --- a/SAT/Mios/ClauseManager.hs +++ b/SAT/Mios/ClauseManager.hs @@ -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] diff --git a/SAT/Mios/Data/Singleton.hs b/SAT/Mios/Data/Singleton.hs deleted file mode 100644 --- a/SAT/Mios/Data/Singleton.hs +++ /dev/null @@ -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 diff --git a/SAT/Mios/Data/Stack.hs b/SAT/Mios/Data/Stack.hs deleted file mode 100644 --- a/SAT/Mios/Data/Stack.hs +++ /dev/null @@ -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 --} diff --git a/SAT/Mios/Data/Vec.hs b/SAT/Mios/Data/Vec.hs deleted file mode 100644 --- a/SAT/Mios/Data/Vec.hs +++ /dev/null @@ -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 diff --git a/SAT/Mios/Data/VecBool.hs b/SAT/Mios/Data/VecBool.hs deleted file mode 100644 --- a/SAT/Mios/Data/VecBool.hs +++ /dev/null @@ -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 diff --git a/SAT/Mios/Data/VecDouble.hs b/SAT/Mios/Data/VecDouble.hs deleted file mode 100644 --- a/SAT/Mios/Data/VecDouble.hs +++ /dev/null @@ -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 diff --git a/SAT/Mios/Internal.hs b/SAT/Mios/Internal.hs deleted file mode 100644 --- a/SAT/Mios/Internal.hs +++ /dev/null @@ -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 -} diff --git a/SAT/Mios/Main.hs b/SAT/Mios/Main.hs --- a/SAT/Mios/Main.hs +++ b/SAT/Mios/Main.hs @@ -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 diff --git a/SAT/Mios/OptionParser.hs b/SAT/Mios/OptionParser.hs --- a/SAT/Mios/OptionParser.hs +++ b/SAT/Mios/OptionParser.hs @@ -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 diff --git a/SAT/Mios/Solver.hs b/SAT/Mios/Solver.hs --- a/SAT/Mios/Solver.hs +++ b/SAT/Mios/Solver.hs @@ -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 diff --git a/SAT/Mios/Types.hs b/SAT/Mios/Types.hs --- a/SAT/Mios/Types.hs +++ b/SAT/Mios/Types.hs @@ -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 -} diff --git a/SAT/Mios/Util/CNFIO.hs b/SAT/Mios/Util/CNFIO.hs deleted file mode 100644 --- a/SAT/Mios/Util/CNFIO.hs +++ /dev/null @@ -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_ diff --git a/SAT/Mios/Util/CNFIO/MinisatReader.hs b/SAT/Mios/Util/CNFIO/MinisatReader.hs deleted file mode 100644 --- a/SAT/Mios/Util/CNFIO/MinisatReader.hs +++ /dev/null @@ -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 [] diff --git a/SAT/Mios/Util/CNFIO/Reader.hs b/SAT/Mios/Util/CNFIO/Reader.hs deleted file mode 100644 --- a/SAT/Mios/Util/CNFIO/Reader.hs +++ /dev/null @@ -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 [] diff --git a/SAT/Mios/Util/CNFIO/Writer.hs b/SAT/Mios/Util/CNFIO/Writer.hs deleted file mode 100644 --- a/SAT/Mios/Util/CNFIO/Writer.hs +++ /dev/null @@ -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 " diff --git a/SAT/Mios/Util/DIMACS.hs b/SAT/Mios/Util/DIMACS.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Util/DIMACS.hs @@ -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_ diff --git a/SAT/Mios/Util/DIMACS/MinisatReader.hs b/SAT/Mios/Util/DIMACS/MinisatReader.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Util/DIMACS/MinisatReader.hs @@ -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 [] diff --git a/SAT/Mios/Util/DIMACS/Reader.hs b/SAT/Mios/Util/DIMACS/Reader.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Util/DIMACS/Reader.hs @@ -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 [] diff --git a/SAT/Mios/Util/DIMACS/Writer.hs b/SAT/Mios/Util/DIMACS/Writer.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Util/DIMACS/Writer.hs @@ -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 " diff --git a/SAT/Mios/Validator.hs b/SAT/Mios/Validator.hs --- a/SAT/Mios/Validator.hs +++ b/SAT/Mios/Validator.hs @@ -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." diff --git a/SAT/Mios/Vec.hs b/SAT/Mios/Vec.hs new file mode 100644 --- /dev/null +++ b/SAT/Mios/Vec.hs @@ -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)) diff --git a/app/sample.hs b/app/sample.hs new file mode 100644 --- /dev/null +++ b/app/sample.hs @@ -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 diff --git a/mios.cabal b/mios.cabal --- a/mios.cabal +++ b/mios.cabal @@ -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