{-# LANGUAGE
MultiWayIf
, RecordWildCards
, ScopedTypeVariables
, TupleSections
, ViewPatterns
#-}
{-# LANGUAGE Safe #-}
module SAT.Mios.Solver
(
Solver (..)
, newSolver
, nAssigns
, nClauses
, nLearnts
, decisionLevel
, valueVar
, valueLit
, locked
, setAssign
, enqueue
, assume
, cancelUntil
, StatIndex (..)
, getStat
, setStat
, incrementStat
, getStats
)
where
import Control.Monad (unless, when)
import Data.List (intercalate)
import Numeric (showFFloat)
import SAT.Mios.Types
import SAT.Mios.Clause
import SAT.Mios.ClauseManager
import SAT.Mios.ClausePool
data Solver = Solver
{
clauses :: !ClauseExtManager
, learnts :: !ClauseExtManager
, watches :: !WatcherList
, assigns :: !(Vec Int)
, phases :: !(Vec Int)
, trail :: !Stack
, trailLim :: !Stack
, qHead :: !Int'
, reason :: !ClauseVector
, level :: !(Vec Int)
, ndd :: !(Vec Int)
, conflicts :: !Stack
, activities :: !(Vec Double)
, order :: !VarHeap
, config :: !MiosConfiguration
, nVars :: !Int
, claInc :: !Double'
, varInc :: !Double'
, rootLevel :: !Int'
, learntSAdj :: Double'
, learntSCnt :: Int'
, maxLearnts :: Double'
, ok :: !Int'
, an'seen :: !(Vec Int)
, an'toClear :: !Stack
, an'stack :: !Stack
, an'lastDL :: !Stack
, clsPool :: ClausePool
, litsLearnt :: !Stack
, stats :: !(Vec Int)
, lbd'seen :: !(Vec Int)
, lbd'key :: !Int'
, emaAFast :: !EMA
, emaASlow :: !EMA
, emaBDLvl :: !EMA
, emaCDLvl :: !EMA
, emaDFast :: !EMA
, emaDSlow :: !EMA
, nextRestart :: !Int'
, restartExp :: !Double'
, emaRstBias :: !EMA
}
newSolver :: MiosConfiguration -> CNFDescription -> IO Solver
newSolver conf (CNFDescription nv dummy_nc _) =
Solver
<$> newManager dummy_nc
<*> newManager 2000
<*> newWatcherList nv 1
<*> newVec nv LBottom
<*> newVec nv LBottom
<*> newStack nv
<*> newStack nv
<*> new' 0
<*> newClauseVector (nv + 1)
<*> newVec nv (-1)
<*> newVec (2 * (nv + 1)) 0
<*> newStack nv
<*> newVec nv 0
<*> newVarHeap nv
<*> return conf
<*> return nv
<*> new' 1.0
<*> new' 1.0
<*> new' 0
<*> new' 100
<*> new' 100
<*> new' 2000
<*> new' LiftedT
<*> newVec nv 0
<*> newStack nv
<*> newStack nv
<*> newStack nv
<*> newClausePool 10
<*> newStack nv
<*> newVec (fromEnum EndOfStatIndex) 0
<*> newVec nv 0
<*> new' 0
<*> newEMA False ef
<*> newEMA True es
<*> newEMA True 2
<*> newEMA True 2
<*> newEMA False ef
<*> newEMA True es
<*> new' 100
<*> new' 0.0
<*> newEMA False 100
where
(ef, es) = emaCoeffs conf
{-# INLINE nAssigns #-}
nAssigns :: Solver -> IO Int
nAssigns = get' . trail
{-# INLINE nClauses #-}
nClauses :: Solver -> IO Int
nClauses = get' . clauses
{-# INLINE nLearnts #-}
nLearnts :: Solver -> IO Int
nLearnts = get' . learnts
{-# INLINE decisionLevel #-}
decisionLevel :: Solver -> IO Int
decisionLevel = get' . trailLim
{-# INLINE valueVar #-}
valueVar :: Solver -> Var -> IO Int
valueVar = getNth . assigns
{-# INLINE valueLit #-}
valueLit :: Solver -> Lit -> IO Int
valueLit (assigns -> a) p = (\x -> if positiveLit p then x else negate x) <$> getNth a (lit2var p)
{-# INLINE locked #-}
locked :: Solver -> Clause -> IO Bool
locked s c = (c ==) <$> (getNth (reason s) . lit2var =<< getNth (lits c) 1)
{-# INLINE getStat #-}
getStat :: Solver -> StatIndex -> IO Int
getStat (stats -> v) (fromEnum -> i) = getNth v i
{-# INLINE setStat #-}
setStat :: Solver -> StatIndex -> Int -> IO ()
setStat (stats -> v) (fromEnum -> i) x = setNth v i x
{-# INLINE incrementStat #-}
incrementStat :: Solver -> StatIndex -> Int -> IO ()
incrementStat (stats -> v) (fromEnum -> i) k = modifyNth v (+ k) i
{-# INLINABLE getStats #-}
getStats :: Solver -> IO [(StatIndex, Int)]
getStats (stats -> v) = mapM (\i -> (i, ) <$> getNth v (fromEnum i)) [minBound .. maxBound :: StatIndex]
setAssign :: Solver -> Int -> LiftedBool -> IO ()
setAssign Solver{..} v x = setNth assigns v x
{-# INLINABLE enqueue #-}
enqueue :: Solver -> Lit -> Clause -> IO Bool
enqueue s@Solver{..} p from = do
let signumP = lit2lbool p
let v = lit2var p
val <- valueVar s v
if val /= LBottom
then return $ val == signumP
else do setNth assigns v signumP
setNth level v =<< decisionLevel s
setNth reason v from
pushTo trail p
return True
{-# INLINE assume #-}
assume :: Solver -> Lit -> IO Bool
assume s p = do
pushTo (trailLim s) =<< get' (trail s)
enqueue s p NullClause
{-# INLINABLE cancelUntil #-}
cancelUntil :: Solver -> Int -> IO ()
cancelUntil s@Solver{..} lvl = do
dl <- decisionLevel s
when (lvl < dl) $ do
lim <- getNth trailLim (lvl + 1)
ts <- get' trail
ls <- get' trailLim
let
loopOnTrail :: Int -> IO ()
loopOnTrail ((lim <) -> False) = return ()
loopOnTrail c = do
x <- lit2var <$> getNth trail c
setNth phases x =<< getNth assigns x
setNth assigns x LBottom
setNth reason x NullClause
undoVO s x
loopOnTrail $ c - 1
loopOnTrail ts
shrinkBy trail (ts - lim)
shrinkBy trailLim (ls - lvl)
set' qHead =<< get' trail
instance VarOrder Solver where
{-# SPECIALIZE INLINE updateVO :: Solver -> Var -> IO () #-}
updateVO = increaseHeap
{-# SPECIALIZE INLINE undoVO :: Solver -> Var -> IO () #-}
undoVO s v = inHeap s v >>= (`unless` insertHeap s v)
{-# SPECIALIZE INLINE selectVO :: Solver -> IO Var #-}
selectVO s = do
let
asg = assigns s
loop :: IO Var
loop = do
n <- numElementsInHeap s
if n == 0
then return 0
else do
v <- getHeapRoot s
x <- getNth asg v
if x == LBottom then return v else loop
loop
data VarHeap = VarHeap
{
heap :: !Stack
, idxs :: !Stack
}
newVarHeap :: Int -> IO VarHeap
newVarHeap n = do
v1 <- newVec n 0
v2 <- newVec n 0
let
loop :: Int -> IO ()
loop ((<= n) -> False) = set' v1 n >> set' v2 n
loop i = setNth v1 i i >> setNth v2 i i >> loop (i + 1)
loop 1
return $ VarHeap v1 v2
{-# INLINE numElementsInHeap #-}
numElementsInHeap :: Solver -> IO Int
numElementsInHeap = get' . heap . order
{-# INLINE inHeap #-}
inHeap :: Solver -> Var -> IO Bool
inHeap Solver{..} n = case idxs order of at -> (/= 0) <$> getNth at n
{-# INLINE increaseHeap #-}
increaseHeap :: Solver -> Int -> IO ()
increaseHeap s@Solver{..} n = case idxs order of
at -> inHeap s n >>= (`when` (percolateUp s =<< getNth at n))
{-# INLINABLE percolateUp #-}
percolateUp :: Solver -> Int -> IO ()
percolateUp Solver{..} start = do
let VarHeap to at = order
v <- getNth to start
ac <- getNth activities v
let
loop :: Int -> IO ()
loop i = do
let iP = div i 2
if iP == 0
then setNth to i v >> setNth at v i
else do
v' <- getNth to iP
acP <- getNth activities v'
if ac > acP
then setNth to i v' >> setNth at v' i >> loop iP
else setNth to i v >> setNth at v i
loop start
{-# INLINABLE percolateDown #-}
percolateDown :: Solver -> Int -> IO ()
percolateDown Solver{..} start = do
let (VarHeap to at) = order
n <- getNth to 0
v <- getNth to start
ac <- getNth activities v
let
loop :: Int -> IO ()
loop i = do
let iL = 2 * i
if iL <= n
then do
let iR = iL + 1
l <- getNth to iL
r <- getNth to iR
acL <- getNth activities l
acR <- getNth activities r
let (ci, child, ac') = if iR <= n && acL < acR then (iR, r, acR) else (iL, l, acL)
if ac' > ac
then setNth to i child >> setNth at child i >> loop ci
else setNth to i v >> setNth at v i
else setNth to i v >> setNth at v i
loop start
{-# INLINABLE insertHeap #-}
insertHeap :: Solver -> Var -> IO ()
insertHeap s@(order -> VarHeap to at) v = do
n <- (1 +) <$> getNth to 0
setNth at v n
setNth to n v
set' to n
percolateUp s n
{-# INLINABLE getHeapRoot #-}
getHeapRoot :: Solver -> IO Int
getHeapRoot s@(order -> VarHeap to at) = do
r <- getNth to 1
l <- getNth to =<< getNth to 0
setNth to 1 l
setNth at l 1
setNth at r 0
modifyNth to (subtract 1) 0
n <- getNth to 0
when (1 < n) $ percolateDown s 1
return r