-- | (This is a part of MIOS.)
-- Main part of solving satisfiability problem.
{-# LANGUAGE
    BangPatterns
  , MultiWayIf
  , RecordWildCards
  , ScopedTypeVariables
  , ViewPatterns
  #-}
{-# LANGUAGE Safe #-}

module SAT.Mios.Main
       (
         -- * Interface to 'Solver', imported from 'SAT.Mios.Criteria'
         Solver
       , newSolver
       , setAssign
       , addClause
       , dumpSolver
         -- * Main function
       , simplifyDB
       , solve
       )
        where

import Control.Monad (unless, void, when)
import Data.Bits
import Data.Foldable (foldrM)
import Data.Int
import SAT.Mios.Types
import SAT.Mios.Clause
import SAT.Mios.ClauseManager
import SAT.Mios.Solver
import SAT.Mios.ClausePool
import SAT.Mios.Criteria

-- | #114: __RemoveWatch__
{-# INLINABLE removeWatch #-}
removeWatch :: Solver -> Clause -> IO ()
removeWatch Solver{..} c = do
  let lstack = lits c
  l1 <- negateLit <$> getNth lstack 1
  markClause (getNthWatcher watches l1) c
  l2 <- negateLit <$> getNth lstack 2
  markClause (getNthWatcher watches l2) c
  putBackToPool clsPool c

--------------------------------------------------------------------------------
-- Operations on 'Clause'
--------------------------------------------------------------------------------

-- | __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.
newLearntClause :: Solver -> Stack -> IO Int
newLearntClause s@Solver{..} ps = 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 <- get' ps
  case k of
   1 -> do l <- getNth ps 1
           unsafeEnqueue s l NullClause
           return 1
   _ -> do c <- makeClauseFromStack clsPool ps --  newClauseFromStack True ps
           let lstack = lits c
               findMax :: Int -> Int -> Int -> IO Int -- Pick a second literal to watch:
               findMax ((<= k) -> False) j _ = return j
               findMax i j val = do
                 v <- lit2var <$> getNth lstack i
                 a <- getNth assigns v
                 b <- getNth level v
                 if (a /= LBottom) && (val < b)
                   then findMax (i + 1) i b
                   else findMax (i + 1) j val
           swapBetween lstack 2 =<< findMax 1 1 0 -- Let @max_i@ be the index of the literal with highest decision level
           -- Bump, enqueue, store clause:
           claBumpActivity s c
           -- Add clause to all managers
           pushTo learnts c
           l1 <- getNth lstack 1
           l2 <- getNth lstack 2
           pushClauseWithKey (getNthWatcher watches (negateLit l1)) c l2
           pushClauseWithKey (getNthWatcher watches (negateLit l2)) c l1
           -- update the solver state by @l@
           unsafeEnqueue s l1 c
           -- Since unsafeEnqueue updates the 1st literal's level, setLBD should be called after unsafeEnqueue
           lbd <- lbdOf s (lits c)
           set' (rank c) lbd
           -- assert (0 < rank c)
           -- set' (protected c) True
           return lbd

-- | __Simplify.__ At the top-level, a constraint may be given the opportunity to
-- simplify its representation (returns @False@) or state that the constraint is
-- satisfied under the current assignment and can be removed (returns @True@).
-- A constraint must /not/ be simplifiable to produce unit information or to be
-- conflicting; in that case the propagation has not been correctly defined.
--
-- MIOS NOTE: the original doesn't update watchers; only checks its satisfiabiliy.
{-# INLINABLE simplify #-}
simplify :: Solver -> Clause -> IO Bool
simplify s c = do
  n <- get' c
  let lstack = lits c
      loop ::Int -> IO Bool
      loop ((<= n) -> False) = return False
      loop i = do v <- valueLit s =<< getNth lstack i
                  if v == 1 then return True else loop (i + 1)
  loop 1

--------------------------------------------------------------------------------
-- MIOS NOTE on Minor methods:
--
-- * no (meaningful) 'newVar' in mios
-- * 'assume' is defined in 'Solver'
-- * `cancelUntil` is defined in 'Solver'

--------------------------------------------------------------------------------
-- Major methods

-- | M114: __Fig. 10. (p.15)__
--
-- analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel :: int&) -> [void]
--
-- __Description:_-
--   Analzye confilct and produce a reason clause.
--
-- __Pre-conditions:__
--   * 'out_learnt' is assumed to be cleared.
--   * Corrent decision level must be greater than root level.
--
-- __Post-conditions:__
--   * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
--   * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the
--     rest of literals. There may be others from the same level though.
--
-- @analyze@ is invoked from @search@
analyze :: Solver -> Clause -> IO Int
analyze s@Solver{..} confl = do
  -- litvec
  reset litsLearnt
  pushTo litsLearnt 0 -- reserve the first place for the unassigned literal
  dl <- decisionLevel s
  let loopOnClauseChain :: Clause -> Lit -> Int -> Int -> Int -> IO Int
      loopOnClauseChain c p ti bl pathC = do -- p : literal, ti = trail index, bl = backtrack level
        d <- get' (rank c)
        when (0 /= d) $ claBumpActivity s c
        -- update LBD like #Glucose4.0
        when (2 < d) $ do
          nblevels <- lbdOf s (lits c)
          when (nblevels + 1 < d) $ -- improve the LBD
            -- when (d <= 30) $ set' (protected c) True -- 30 is `lbLBDFrozenClause`
            -- seems to be interesting: keep it fro the next round
            set' (rank c) nblevels    -- Update it
        sc <- get' c
        let lstack = lits c
            loopOnLiterals :: Int -> Int -> Int -> IO (Int, Int)
            loopOnLiterals ((<= sc) -> False) b pc = return (b, pc) -- b = btLevel, pc = pathC
            loopOnLiterals j b pc = do
              (q :: Lit) <- getNth lstack j
              let v = lit2var q
              sn <- getNth an'seen v
              l <- getNth level v
              if sn == 0 && 0 < l
                then do
                    varBumpActivity s v
                    setNth an'seen v 1
                    if dl <= l      -- cancelUntil doesn't clear level of cancelled literals
                      then do
                          -- UPDATEVARACTIVITY: glucose heuristics
                          r <- getNth reason v
                          when (r /= NullClause) $ do
                            ra <- get' (rank r)
                            when (0 /= ra) $ pushTo an'lastDL q
                          -- end of glucose heuristics
                          loopOnLiterals (j + 1) b (pc + 1)
                      else pushTo litsLearnt q >> loopOnLiterals (j + 1) (max b l) pc
                else loopOnLiterals (j + 1) b pc
        (b', pathC') <- loopOnLiterals (if p == bottomLit then 1 else 2) bl pathC
        let nextPickedUpLit :: Int -> IO Int        -- select next clause to look at
            nextPickedUpLit i = do x <- getNth an'seen . lit2var =<< getNth trail i
                                   if x == 0 then nextPickedUpLit (i - 1) else return (i - 1)
        ti' <- nextPickedUpLit (ti + 1)
        nextP <- getNth trail (ti' + 1)
        let nextV = lit2var nextP
        confl' <- getNth reason nextV
        setNth an'seen nextV 0
        if 1 < pathC'
          then loopOnClauseChain confl' nextP (ti' - 1) b' (pathC' - 1)
          else setNth litsLearnt 1 (negateLit nextP) >> return b'
  ti <- subtract 1 <$> get' trail
  levelToReturn <- loopOnClauseChain confl bottomLit ti 0 0
  -- Simplify phase (implemented only @expensive_ccmin@ path)
  n <- get' litsLearnt
  reset an'stack           -- analyze_stack.clear();
  reset an'toClear         -- out_learnt.copyTo(analyze_toclear);
  pushTo an'toClear =<< getNth litsLearnt 1
  let merger :: Int -> Int64 -> IO Int64
      merger ((<= n) -> False) b = return b
      merger i b = do l <- getNth litsLearnt i
                      pushTo an'toClear l
                      -- restrict the search depth (range) to 63
                      merger (i + 1) . setBit b . (63 .&.) =<< getNth level (lit2var l)
  levels <- merger 2 0
  let loopOnLits :: Int -> Int -> IO ()
      loopOnLits ((<= n) -> False) n' = shrinkBy litsLearnt $ n - n' + 1
      loopOnLits i j = do
        l <- getNth litsLearnt i
        c1 <- (NullClause ==) <$> getNth reason (lit2var l)
        if c1
          then setNth litsLearnt j l >> loopOnLits (i + 1) (j + 1)
          else do
             c2 <- not <$> analyzeRemovable s l levels
             if c2
               then setNth litsLearnt j l >> loopOnLits (i + 1) (j + 1)
               else loopOnLits (i + 1) j
  loopOnLits 2 2                -- the first literal is specail
  -- UPDATEVARACTIVITY: glucose heuristics
  nld <- get' an'lastDL
  r <- get' litsLearnt -- this is an estimated LBD value based on the clause size
  let loopOnLastDL :: Int -> IO ()
      loopOnLastDL ((<= nld) -> False) = return ()
      loopOnLastDL i = do v <- lit2var <$> getNth an'lastDL i
                          r' <- get' =<< getNth reason v
                          when (r < r') $ varBumpActivity s v
                          loopOnLastDL $ i + 1
  loopOnLastDL 1
  reset an'lastDL
  -- Clear seen
  k <- get' an'toClear
  let cleaner :: Int -> IO ()
      cleaner ((<= k) -> False) = return ()
      cleaner i = do v <- lit2var <$> getNth an'toClear i
                     setNth an'seen v 0
                     cleaner $ i + 1
  cleaner 1
  return levelToReturn

-- | #M114
-- Check if 'p' can be removed, 'abstract_levels' is used to abort early if the algorithm is
-- visiting literals at levels that cannot be removed later.
--
-- Implementation memo:
--
-- *  @an'toClear@ is initialized by @ps@ in @analyze@ (a copy of 'learnt').
--   This is used only in this function and @analyze@.
--
analyzeRemovable :: Solver -> Lit -> Int64 -> IO Bool
analyzeRemovable Solver{..} p minLevel = do
  -- assert (reason[var(p)] != NullClause);
  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 <- 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 <- lastOf an'stack
            popFrom an'stack             -- analyze_stack.pop();
            c <- getNth reason (lit2var sl) -- getRoot sl
            nl <- get' c
            let
              lstack = lits c
              loopOnLit :: Int -> IO Bool -- loopOnLit (int i = 1; i < c.size(); i++){
              loopOnLit ((<= nl) -> False) = loopOnStack
              loopOnLit i = do
                p' <- getNth lstack i              -- valid range is [1 .. nl]
                let v' = lit2var p'
                l' <- getNth level v'
                c1 <- (1 /=) <$> getNth an'seen v'
                if c1 && (0 /= l')   -- if (!analyze_seen[var(p)] && level[var(p)] != 0){
                  then do
                      c3 <- (NullClause /=) <$> getNth reason v'
                      if c3 && testBit minLevel (l' .&. 63) -- 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;
                            pushTo an'stack p'    -- analyze_stack.push(p);
                            pushTo an'toClear p'  -- analyze_toclear.push(p);
                            loopOnLit $ i + 1
                        else do
                            -- for (int j = top; j < analyze_toclear.size(); j++) analyze_seen[var(analyze_toclear[j])] = 0;
                            top' <- get' an'toClear
                            let clearAll :: Int -> IO ()
                                clearAll ((<= top') -> False) = return ()
                                clearAll j = do x <- getNth an'toClear j; setNth an'seen (lit2var x) 0; clearAll (j + 1)
                            clearAll $ top + 1
                            -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop
                            shrinkBy an'toClear $ top' - top
                            return False
                  else loopOnLit $ i + 1
            loopOnLit 2
  loopOnStack

-- | #114
-- analyzeFinal : (confl : Clause *) (skip_first : boot) -> [void]
--
-- __Description:__
--   Specialized analysis proceduce to express the final conflict in terms of assumptions.
--   'root_level' is allowed to point beyond end of trace (useful if called after conflict while
--   making assumptions). If 'skip_first' is TRUE, the first literal of 'confl' is ignored (needed
--   if conflict arose before search even started).
--
analyzeFinal :: Solver -> Clause -> Bool -> IO ()
analyzeFinal Solver{..} confl skipFirst = do
  reset conflicts
  rl <- get' rootLevel
  unless (rl == 0) $ do
    n <- get' confl
    let lstack = lits confl
        loopOnConfl :: Int -> IO ()
        loopOnConfl ((<= n) -> False) = return ()
        loopOnConfl i = do
          (x :: Var) <- lit2var <$> getNth lstack i
          lvl <- getNth level x
          when (0 < lvl) $ setNth an'seen x 1
          loopOnConfl $ i + 1
    loopOnConfl $ if skipFirst then 2 else 1
    tls <- get' trailLim
    trs <- get' trail
    tlz <- getNth trailLim 1
    let loopOnTrail :: Int -> IO ()
        loopOnTrail ((tlz <=) -> False) = return ()
        loopOnTrail i = do
          (l :: Lit) <- getNth trail (i + 1)
          let (x :: Var) = lit2var l
          saw <- getNth an'seen x
          when (saw == 1) $ do
            (r :: Clause) <- getNth reason x
            if r == NullClause
              then pushTo conflicts (negateLit l)
              else do
                  k <- get' r
                  let lstack' = lits r
                      loopOnLits :: Int -> IO ()
                      loopOnLits ((<= k) -> False) = return ()
                      loopOnLits j = do
                        (v :: Var) <- lit2var <$> getNth lstack' j
                        lv <- getNth level v
                        when (0 < lv) $ setNth an'seen v 1
                        loopOnLits $ i + 1
                  loopOnLits 2
          setNth an'seen x 0
          loopOnTrail $ i - 1
    loopOnTrail =<< if tls <= rl then return (trs - 1) else getNth trailLim (rl + 1)

-- | M114:
-- propagate : [void] -> [Clause+]
--
-- __Description:__
--   Porpagates all enqueued facts. If a conflict arises, the conflicting clause is returned.
--   otherwise CRef_undef.
--
-- __Post-conditions:__
--   * the propagation queue is empty, even if there was a conflict.
--
-- memo: @propagate@ is invoked by @search@,`simpleDB` and `solve`
propagate :: Solver -> IO Clause
propagate s@Solver{..} = do
  let
    while :: Clause -> Bool -> IO Clause
    while confl False = return confl
    while confl True = do
      (p :: Lit) <- getNth trail . (1 +) =<< get' qHead
      modify' qHead (+ 1)
      incrementStat s NumOfPropagation 1
      let (ws :: ClauseExtManager) = getNthWatcher watches p
          !falseLit = negateLit p
      end <- get' ws
      cvec <- getClauseVector ws
      bvec <- getKeyVector ws
      let copy :: Int -> Int -> IO ()
          copy ((< end) -> False) _ = return ()
          copy !i' !j' = do setNth cvec j' =<< getNth cvec i'
                            setNth bvec j' =<< getNth bvec i'
                            copy (i' + 1) (j' + 1)
      let forClause :: Int -> Int -> IO Clause
          forClause i@((< end) -> False) !j = shrinkBy ws (i - j) >> return confl
          forClause !i !j = do
            (blocker :: Lit) <- getNth bvec i        -- Try to avoid inspecting the clause:
            bv <- if blocker == 0 then return LiftedF else valueLit s blocker
            if bv == LiftedT
              then do unless (i == j) $ do (c :: Clause) <- getNth cvec i
                                           setNth cvec j c
                                           setNth bvec j blocker
                      forClause (i + 1) (j + 1)
              else do                               -- Make sure the false literal is data[1]:
                  (c :: Clause) <- getNth cvec i
                  let !lstack = lits c
                  tmp <- getNth lstack 1
                  first <- if falseLit == tmp
                           then do l2 <- getNth lstack 2
                                   setNth lstack 2 tmp
                                   setNth lstack 1 l2
                                   return l2
                           else return tmp
                  fv <- valueLit s first
                  if fv == LiftedT
                    then do unless (i == j) $ setNth cvec j c
                            setNth bvec j first
                            forClause (i + 1) (j + 1)
                    else do cs <- get' c           -- Look for new watch:
                            let newWatch :: Int -> IO LiftedBool
                                newWatch ((<= cs) -> False) = do -- Did not find watch
                                  setNth cvec j c
                                  setNth bvec j first
                                  if fv == LiftedF
                                    then do ((== 0) <$> decisionLevel s) >>= (`when` set' ok LiftedF)
                                            set' qHead =<< get' trail
                                            copy (i + 1) (j + 1)
                                            return LiftedF                 -- conflict
                                    else do unsafeEnqueue s first c
                                            return LBottom                 -- unit clause
                                newWatch !k = do (l' :: Lit) <- getNth lstack k
                                                 lv <- valueLit s l'
                                                 if lv /= LiftedF
                                                   then do setNth lstack 2 l'
                                                           setNth lstack k falseLit
                                                           pushClauseWithKey (getNthWatcher watches (negateLit l')) c first
                                                           return LiftedT  -- found another watch
                                                   else newWatch $! k + 1
                            ret <- newWatch 3
                            case ret of
                              LiftedT -> forClause (i + 1) j               -- found another watch
                              LBottom -> forClause (i + 1) (j + 1)         -- unit clause
                              _       -> shrinkBy ws (i - j) >> return c   -- conflict
      c <- forClause 0 0
      while c =<< ((<) <$> get' qHead <*> get' trail)
  while NullClause =<< ((<) <$> get' qHead <*> get' trail)

-- | #M22
-- reduceDB: () -> [void]
--
-- __Description:__
--   Remove half of the learnt clauses, minus the clauses locked by the current assigmnent. Locked
--   clauses are clauses that are reason to some assignment. Binary clauses are never removed.
reduceDB :: Solver -> IO ()
reduceDB s@Solver{..} = do
  n <- nLearnts s
  cvec <- getClauseVector learnts
  let loop :: Int -> IO ()
      loop ((< n) -> False) = return ()
      loop i = do
        removeWatch s =<< getNth cvec i
        loop $ i + 1
  k <- sortClauses s learnts $ div n 2 -- k is the number of clauses not to be purged
{-
  -- #GLUCOSE3.0 keep more
  t3 <- get' . rank =<< getNth vec (thr -1)
  t5 <- get' . rank =<< getNth vec (lim -1)

  let k = case (t3 <= 3, t5 <= 5) of
            (True, True)   -> min n (thr + 2000)
            (False, False) -> thr
            (_, _)         -> min n (thr + 1000)
  -- let k = div thr 2
-}
  loop k                               -- CAVEAT: `vec` is a zero-based vector
  -- putStrLn $ "reduceDB: purge " ++ show (n - k) ++ " out of " ++ show n
  reset watches
  shrinkBy learnts (n - k)
  incrementStat s NumOfReduction 1

-- constants for sort key layout
rankWidth :: Int
rankWidth = 10
activityWidth :: Int
activityWidth = 50              -- note: the maximum clause activity is 1e20.
indexWidth :: Int
indexWidth = 32                 -- 4G
rankMax :: Int
rankMax = 2 ^ rankWidth - 1
activityMax :: Int
activityMax = 2 ^ activityWidth - 1
indexMax :: Int
indexMax = 2 ^ indexWidth - 1

-- | applies a (good to bad) quick semi-sort to the vector in a 'ClauseExtManager'
-- and returns the number of privileged clauses.
-- This function uses the same criteria as reduceDB_lt in glucose 4.0:
-- 1. binary clause
-- 2. smaller LBD
-- 3. larger activity defined as MiniSat
--
-- they are encoded into two "Int64"s as the following (10+52+32 layout):
--
-- * 10 bits for rank (LBD): 'rankWidth'
-- * 50 bits for converted activity: 'activityWidth'
-- * 32 bits for clauseVector index: 'indexWidth'
--
sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int
sortClauses s cm limit' = do
  n <- get' cm
  -- assert (n < indexMax)
  vec <- getClauseVector cm
  bvec <- getKeyVector cm
  keys <- newVec (2 * n) 0 :: IO (Vec Int)
  at <- (0.1 *) . (/ fromIntegral n) <$> get' (claInc s) -- activity threshold
  -- 1: assign keys
  let shiftLBD = activityWidth
      shiftIndex = shiftL 1 indexWidth
      am = fromIntegral activityMax :: Double
      scaleAct :: Double -> Int
      scaleAct x
        | x < 1e-20 = activityMax
        | otherwise = floor $ am * (1 - logBase 10 (x * 1e20) / 40)
      assignKey :: Int -> Int -> IO Int
      assignKey ((< n) -> False) t = return t
      assignKey i t = do
        setNth keys (2 * i + 1) $ shiftIndex + i
        c <- getNth vec i
        k <- get' c
        if k == 2                  -- Main criteria. Like in MiniSat we keep all binary clauses
          then do setNth keys (2 * i) 0
                  assignKey (i + 1) (t + 1)
          else do a <- get' (activity c)               -- Second one... based on LBD
                  r <- get' (rank c)
                  l <- locked s c
                  let d =if | l -> 0
                            | a < at -> rankMax
                            | otherwise ->  min rankMax r                -- rank can be one
                  setNth keys (2 * i) $ shiftL d shiftLBD + scaleAct a
                  assignKey (i + 1) $ if l then t + 1 else t
  limit <- max limit' <$> assignKey 0 0
  -- 2: sort keyVector
  let limit2 = 2 * limit
      sortOnRange :: Int -> Int -> IO ()
      sortOnRange left right
        | limit2 < left = return ()
        | left >= right = return ()
        | left + 2 == right = do
            a <- getNth keys left
            b <- getNth keys right
            unless (a < b) $ do swapBetween keys left right
                                swapBetween keys (left + 1) (right + 1)
        | otherwise = do
            let p = 2 * div (left + right) 4
            pivot <- getNth keys p
            swapBetween keys p left -- set a sentinel for r'
            swapBetween keys (p + 1) (left + 1)
            let nextL :: Int -> IO Int
                nextL i@((<= right) -> False) = return i
                nextL i = do v <- getNth keys i; if v < pivot then nextL (i + 2) else return i
                nextR :: Int -> IO Int
                nextR i = do v <- getNth keys i; if pivot < v then nextR (i - 2) else return i
                divide :: Int -> Int -> IO Int
                divide l r = do
                  l' <- nextL l
                  r' <- nextR r
                  if l' < r'
                    then do swapBetween keys l' r'
                            swapBetween keys (l' + 1) (r' + 1)
                            divide (l' + 2) (r' - 2)
                    else return r'
            m <- divide (left + 2) right
            swapBetween keys left m
            swapBetween keys (left + 1) (m + 1)
            sortOnRange left (m - 2)
            sortOnRange (m + 2) right
  sortOnRange 0 $ 2 * (n - 1)
  -- 3: place clauses in 'vec' based on the order stored in 'keys'.
  -- To recycle existing clauses, we must reserve all clauses for now.
  let seek :: Int -> IO ()
      seek ((< n) -> False) = return ()
      seek i = do
        bits <- getNth keys (2 * i + 1)
        when (indexMax < bits) $ do
          c <- getNth vec i
          d <- getNth bvec i
          -- setNth keys i i
          let sweep k = do k' <- (indexMax .&.) <$> getNth keys (2 * k + 1)
                           setNth keys (2 * k + 1) (indexMax .&. k)
                           if k' == i
                             then do setNth vec k c
                                     setNth bvec k d
                             else do getNth vec k' >>= setNth vec k
                                     getNth bvec k' >>= setNth bvec k
                                     sweep k'
          sweep i -- (indexMax .&. bits)
        seek $ i + 1
  seek 0
  return limit

-- | #M22
--
-- simplify : [void] -> [bool]
--
-- __Description:__
--   Simplify the clause database according to the current top-level assigment. Currently, the only
--   thing done here is the removal of satisfied clauses, but more things can be put here.
--
simplifyDB :: Solver -> IO Bool
simplifyDB s@Solver{..} = do
  good <- (LiftedT ==) <$> get' ok
  if good
    then do
      p <- propagate s
      if p /= NullClause
        then set' ok LiftedF >> return False
        else do
            -- Remove satisfied clauses and their watcher lists:
            let
              for :: ClauseExtManager -> IO ()
              for mgr = do
                vec' <- getClauseVector mgr
                n' <- get' mgr
                let
                  loopOnVector :: Int -> Int -> IO ()
                  loopOnVector ((< n') -> False) j = shrinkBy mgr (n' - j)
                  loopOnVector i j = do
                        c <- getNth vec' i
                        l <- locked s c
                        r <- if l then return False else simplify s c
                        if r
                          then removeWatch s c >> loopOnVector (i + 1) j
                          else unless (i == j) (setNth vec' j c) >> loopOnVector (i + 1) (j + 1)
                loopOnVector 0 0
            for clauses
            for learnts
            reset watches
            return True
    else return False

-- | #M22
--
-- search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]
--
-- __Description:__
--   Search for a model the specified number of conflicts.
--   NOTE: Use negative value for 'nof_conflicts' indicate infinity.
--
-- __Output:__
--   * 'True' if a partial assigment that is consistent with respect to the clause set is found.
--      If all variables are decision variables, that means that the clause set is satisfiable.
--   * 'False' if the clause set is unsatisfiable or some error occured.
search :: Solver -> IO Bool
search s@Solver{..} = do
  -- clear model
  let loop :: Bool -> IO Bool
      loop restart = do
        confl <- propagate s
        d <- decisionLevel s
        if confl /= NullClause  -- CONFLICT
          then do incrementStat s NumOfBackjump 1
                  r <- get' rootLevel
                  if d == r                       -- Contradiction found:
                    then analyzeFinal s confl False >> return False
                    else do backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself
                            (s `cancelUntil`) . max backtrackLevel =<< get' rootLevel
                            lbd' <- newLearntClause s litsLearnt
                            k <- get' litsLearnt
                            when (k == 1) $ do
                              (v :: Var) <- lit2var <$> getNth litsLearnt 1
                              setNth level v 0
                            varDecayActivity s
                            claDecayActivity s
                            -- learnt DB Size Adjustment
                            modify' learntSCnt (subtract 1)
                            cnt <- get' learntSCnt
                            when (cnt == 0) $ do
                              t' <- (* 1.5) <$> get' learntSAdj
                              set' learntSAdj t'
                              set' learntSCnt $ floor t'
                              -- modify' maxLearnts (* 1.1)
                              modify' maxLearnts (+ 300)
                            loop =<< checkRestartCondition s lbd'
          else do when (d == 0) . void $ simplifyDB s -- Simplify the set of problem clauses
                  k1 <- get' learnts
                  k2 <- nAssigns s
                  nl <- floor <$> get' maxLearnts
                  when (nl < k1 - k2) $ do
                    reduceDB s    -- Reduce the set of learnt clauses.
                    when (2 == dumpStat config) $ dumpSolver DumpCSV s
                  if | k2 == nVars -> return True     -- Model found
                     | restart -> do                  -- Reached bound on number of conflicts
                         (s `cancelUntil`) =<< get' rootLevel -- force a restart
                         -- claRescaleActivityAfterRestart s
{-
                         let toggle :: Int -> Int
                             toggle LiftedT = LiftedF
                             toggle LiftedF = LiftedT
                             toggle x = x
                             nv = nVars
                             toggleAt :: Int -> IO ()
                             toggleAt ((<= nv) -> False) = return ()
                             toggleAt i = modifyNth phases toggle i >> toggleAt (i + 1)
                         rm <- get' restartMode
                         when (rm == 1) $ toggleAt 1
-}
                         loop False
                     | otherwise -> do                -- New variable decision
                         v <- select s
                         -- #phasesaving <<<<  many have heuristic for polarity here
                         oldVal <- getNth phases v
                         unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@
                         -- #phasesaving >>>>
                         loop False
  loop False

-- | __Fig. 16. (p.20)__
-- Main solve method.
--
-- __Pre-condition:__ If assumptions are used, 'simplifyDB' must be
-- called right before using this method. If not, a top-level conflict (resulting in a
-- non-usable internal state) cannot be distinguished from a conflict under assumptions.
solve :: (Foldable t) => Solver -> t Lit -> IO SolverResult
solve s@Solver{..} assumps = do
  -- PUSH INCREMENTAL ASSUMPTIONS:
  let inject :: Lit -> Bool -> IO Bool
      inject _ False = return False
      inject a True = do
        b <- assume s a
        if not b                  -- conflict analyze
          then do (confl :: Clause) <- getNth reason (lit2var a)
                  analyzeFinal s confl True
                  pushTo conflicts (negateLit a)
                  cancelUntil s 0
                  return False
          else do confl <- propagate s
                  if confl /= NullClause
                    then do analyzeFinal s confl True
                            cancelUntil s 0
                            return False
                    else return True
  good <- simplifyDB s
  x <- if good then foldrM inject True assumps else return False
  if x
    then do set' rootLevel =<< decisionLevel s
            status <- search s
            -- post-proccesing should be done here
            let toInt :: Var -> IO Lit
                toInt v = (\p -> if LiftedT == p then v else negate v) <$> valueVar s v
            asg1 <- mapM toInt [1 .. nVars]
            asg2 <- map lit2int <$> asList conflicts
            when (0 < dumpStat config) $ dumpSolver DumpCSV s
            cancelUntil s 0     -- reset solver
            flag <- get' ok
            if | status && flag == LiftedT     -> return $ Right (SAT asg1)
               | not status && flag == LiftedF -> return $ Right (UNSAT asg2)
               | otherwise                     -> return $ Left InternalInconsistent
    else return $ Right (UNSAT [])

-- | 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 $ lit2lbool p
  setNth level v =<< decisionLevel s
  setNth reason v from     -- NOTE: @from@ might be NULL!
  pushTo trail p

-- | __Pre-condition:__ propagation queue is empty.
{-# INLINE unsafeAssume #-}
unsafeAssume :: Solver -> Lit -> IO ()
unsafeAssume s@Solver{..} p = do
  pushTo trailLim =<< get' trail
  unsafeEnqueue s p NullClause