{-# LANGUAGE
    BangPatterns
  , RecordWildCards
  , ScopedTypeVariables
  , ViewPatterns
  #-}
{-# LANGUAGE Safe #-}

-- | This is a part of MIOS; main heuristics
module SAT.Mios.Main
       (
         simplifyDB
       , solve
       )
        where

import Control.Monad (forM_, unless, void, when)
import Data.Bits
import Data.Foldable (foldrM)
import SAT.Mios.Types
import SAT.Mios.Internal
import SAT.Mios.Clause
import SAT.Mios.ClauseManager
import SAT.Mios.Solver
-- import SAT.Mios.Ranking

-------------------------------------------------------------------------------- Ranking
-- | a special version of ranking
{-# INLINE ranking' #-}
ranking' :: Clause -> IO Int
ranking' = sizeOfClause

-- | #114: __RemoveWatch__
{-# INLINABLE removeWatch #-}
removeWatch :: Solver -> Clause -> IO ()
removeWatch (watches -> w) c = do
  let lvec = asVec c
  l1 <- negateLit <$> getNth lvec 0
  markClause (getNthWatcher w l1) c
  l2 <- negateLit <$> getNth lvec 1
  markClause (getNthWatcher w l2) c

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

-- | __Fig. 8. (p.12)__ create a new LEARNT clause and adds it to watcher lists
-- This is a strippped-down version of 'newClause' in Solver
{-# INLINABLE newLearntClause #-}
newLearntClause :: Solver -> Vec -> IO ()
newLearntClause s@Solver{..} ps = do
  good <- getBool ok
  when good $ do
    -- ps is a 'SizedVectorInt'; ps[0] is the number of active literals
    -- Since this solver must generate only healthy learnt clauses, we need not to run misc check in 'newClause'
    k <- getNth ps 0
    case k of
     1 -> do
       l <- getNth ps 1
       unsafeEnqueue s l NullClause
     _ -> do
       -- allocate clause:
       c <- newClauseFromVec True ps
       let vec = asVec c
       -- Pick a second literal to watch:
       let
         findMax :: Int -> Int -> Int -> IO Int
         findMax ((< k) -> False) j _ = return j
         findMax i j val = do
           v' <- lit2var <$> getNth vec i
           a <- getNth assigns v'
           b <- getNth level v'
           if (a /= lBottom) && (val < b)
             then findMax (i + 1) i b
             else findMax (i + 1) j val
       swapBetween vec 1 =<< findMax 0 0 0 -- Let @max_i@ be the index of the literal with highest decision level
       -- Bump, enqueue, store clause:
       setDouble (activity c) . fromIntegral =<< decisionLevel s -- newly learnt clauses should be considered active
       -- Add clause to all managers
       pushClause learnts c
       l <- getNth vec 0
       pushClauseWithKey (getNthWatcher watches (negateLit l)) c 0
       l1 <- negateLit <$> getNth vec 1
       pushClauseWithKey (getNthWatcher watches l1) c 0
       -- update the solver state by @l@
       unsafeEnqueue s l c
       -- Since unsafeEnqueue updates the 1st literal's level, setLBD should be called after unsafeEnqueue
       -- setRank s c
       setBool (protected c) True

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

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

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

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

-- | #M114
-- Check if 'p' can be removed, 'abstract_levels' is used to abort early if the algorithm is
-- visiting literals at levels that cannot be removed later.
--
-- Implementation memo:
--
-- *  @an'toClear@ is initialized by @ps@ in @analyze@ (a copy of 'learnt').
--   This is used only in this function and @analyze@.
--
{-# INLINEABLE analyzeRemovable #-}
analyzeRemovable :: Solver -> Lit -> Int -> IO Bool
analyzeRemovable Solver{..} p minLevel = do
  -- assert (reason[var(p)]!= NullCaulse);
  clearStack an'stack      -- analyze_stack.clear()
  pushToStack an'stack p   -- analyze_stack.push(p);
  top <- sizeOfStack an'toClear
  let
    loopOnStack :: IO Bool
    loopOnStack = do
      k <- sizeOfStack an'stack  -- int top = analyze_toclear.size();
      if 0 == k
        then return True
        else do -- assert(reason[var(analyze_stack.last())] != GClause_NULL);
            sl <- lastOfStack an'stack
            popFromStack an'stack             -- analyze_stack.pop();
            c <- getNthClause reason (lit2var sl) -- getRoot sl
            nl <- sizeOfClause c
            let
              cvec = asVec c
              loopOnLit :: Int -> IO Bool -- loopOnLit (int i = 1; i < c.size(); i++){
              loopOnLit ((< nl) -> False) = loopOnStack
              loopOnLit i = do
                p' <- getNth cvec i              -- valid range is [0 .. nl - 1]
                let v' = lit2var p'
                l' <- getNth level v'
                c1 <- (1 /=) <$> getNth an'seen v'
                if c1 && (0 /= l')   -- if (!analyze_seen[var(p)] && level[var(p)] != 0){
                  then do
                      c3 <- (NullClause /=) <$> getNthClause reason v'
                      if c3 && testBit minLevel (l' .&. 31) -- if (reason[var(p)] != GClause_NULL && ((1 << (level[var(p)] & 31)) & min_level) != 0){
                        then do
                            setNth an'seen v' 1        -- analyze_seen[var(p)] = 1;
                            pushToStack an'stack p'    -- analyze_stack.push(p);
                            pushToStack an'toClear p'  -- analyze_toclear.push(p);
                            loopOnLit $ i + 1
                        else do
                            -- loopOnLit (int j = top; j < analyze_toclear.size(); j++) analyze_seen[var(analyze_toclear[j])] = 0;
                            top' <- sizeOfStack an'toClear
                            let vec = asVec an'toClear
                            forM_ [top .. top' - 1] $ \j -> do x <- getNth vec j; setNth an'seen (lit2var x) 0
                            -- analyze_toclear.shrink(analyze_toclear.size() - top); note: shrink n == repeat n pop
                            shrinkStack an'toClear $ top' - top
                            return False
                  else loopOnLit $ i + 1
            loopOnLit 1
  loopOnStack

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

-- | M114:
-- propagate : [void] -> [Clause+]
--
-- __Description:__
--   Porpagates all enqueued facts. If a conflict arises, the conflicting clause is returned.
--   otherwise CRef_undef.
--
-- __Post-conditions:__
--   * the propagation queue is empty, even if there was a conflict.
--
-- memo: @propagate@ is invoked by @search@,`simpleDB` and `solve`
{-# INLINABLE propagate #-}
propagate :: Solver -> IO Clause
propagate s@Solver{..} = do
  -- myVal <- getNth stats (fromEnum NumOfBackjump)
  let
{-
    myVal = 0
    bumpAllVar :: IO ()         -- not in use
    bumpAllVar = do
      let
        loop :: Int -> IO ()
        loop ((<= nVars) -> False) = return ()
        loop i = do
          c <- getNth pr'seen i
          when (c == myVal) $ varBumpActivity s i
          loop $ i + 1
      loop 1
-}
    trailVec = asVec trail
    while :: Clause -> Bool -> IO Clause
    while confl False = {- bumpAllVar >> -} return confl
    while confl True = do
      (p :: Lit) <- getNth trailVec =<< getInt qHead
      modifyInt qHead (+ 1)
      let (ws :: ClauseExtManager) = getNthWatcher watches p
      end <- numberOfClauses ws
      cvec <- getClauseVector ws
      bvec <- getKeyVector ws
--      rc <- getNthClause reason $ lit2var p
--      byGlue <- if (rc /= NullClause) && learnt rc then (== 2) <$> getInt (lbd rc) else return False
      let
{-
        checkAllLiteralsIn :: Clause -> IO () -- not in use
        checkAllLiteralsIn c = do
          nc <- sizeOfClause c
          let
            vec = asVec c
            loop :: Int -> IO ()
            loop((< nc) -> False) = return ()
            loop i = do
              (v :: Var) <- lit2var <$> getNth vec i
              setNth pr'seen v myVal
              loop $ i + 1
          loop 0
-}
        forClause :: Clause -> Int -> Int -> IO Clause
        forClause confl i@((< end) -> False) j = do
          shrinkManager ws (i - j)
          while confl =<< ((<) <$> getInt qHead <*> sizeOfStack trail)
        forClause confl i j = do
          (l :: Lit) <- getNth bvec i
          bv <- if l == 0 then return lFalse else valueLit s l
          if bv == lTrue
            then do
                 unless (i == j) $ do -- NOTE: if i == j, the path doesn't require accesses to cvec!
                   (c :: Clause) <- getNthClause cvec i
                   setNthClause cvec j c
                   setNth bvec j l
                 forClause confl (i + 1) (j + 1)
            else do
                -- checkAllLiteralsIn c
                (c :: Clause) <- getNthClause cvec i
                let
                  lits = asVec c
                  falseLit = negateLit p
                -- Make sure the false literal is data[1]
                ((falseLit ==) <$> getNth lits 0) >>= (`when` swapBetween lits 0 1)
                -- if 0th watch is true, then clause is already satisfied.
                (first :: Lit) <- getNth lits 0
                val <- valueLit s first
                if val == lTrue
                  then setNthClause cvec j c >> setNth bvec j first >> forClause confl (i + 1) (j + 1)
                  else do
                      -- Look for new watch
                      cs <- sizeOfClause c
                      let
                        forLit :: Int -> IO Clause
                        forLit ((< cs) -> False) = do
                          -- Did not find watch; clause is unit under assignment:
                          setNthClause cvec j c
                          setNth bvec j 0
                          result <- enqueue s first c
                          if not result
                            then do
                                ((== 0) <$> decisionLevel s) >>= (`when` setBool ok False)
                                -- #BBCP
                                setInt qHead =<< sizeOfStack trail
                                -- Copy the remaining watches:
                                let
                                  copy i'@((< end) -> False) j' = forClause c i' j'
                                  copy i' j' = do
                                    setNthClause cvec j' =<< getNthClause cvec i'
                                    setNth bvec j' =<< getNth bvec i'
                                    copy (i' + 1) (j' + 1)
                                copy (i + 1) (j + 1)
                            else forClause confl (i + 1) (j + 1)
                        forLit k = do
                          (l :: Lit) <- getNth lits k
                          lv <- valueLit s l
                          if lv /= lFalse
                            then do
                                swapBetween lits 1 k
                                pushClauseWithKey (getNthWatcher watches (negateLit l)) c l
                                forClause confl (i + 1) j
                            else forLit $ k + 1
                      forLit 2
      forClause confl 0 0
  while NullClause =<< ((<) <$> getInt qHead <*> sizeOfStack trail)

-- | #M22
-- reduceDB: () -> [void]
--
-- __Description:__
--   Remove half of the learnt clauses, minus the clauses locked by the current assigmnent. Locked
--   clauses are clauses that are reason to some assignment. Binary clauses are never removed.
{-# INLINABLE reduceDB #-}
reduceDB :: Solver -> IO ()
reduceDB s@Solver{..} = do
  n <- nLearnts s
  vec <- getClauseVector learnts
  let
    loop :: Int -> IO ()
    loop ((< n) -> False) = return ()
    loop i = (removeWatch s =<< getNthClause vec i) >> loop (i + 1)
  k <- sortClauses s learnts (div n 2) -- k is the number of clauses not to be purged
  loop k                               -- CAVEAT: `vec` is a zero-based vector
  garbageCollect watches
  shrinkManager learnts (n - k)

-- | (Good to Bad) Quick sort the key vector based on their activities and returns number of privileged clauses.
-- this function uses the same metrix as reduceDB_lt in glucose 4.0:
-- 1. binary clause
-- 2. smaller rank
-- 3. larger activity defined in MiniSat
-- , where smaller value is better.
--
-- they are coded into an Int as the following layout:
--
-- * 14 bit: LBD or 0 for preserved clauses
-- * 19 bit: converted activity
-- * remain: clauseVector index
--
(rankWidth :: Int, activityWidth :: Int, indexWidth :: Int) = (l, a, w - (l + a + 1))
  where
    w = finiteBitSize (0:: Int)
    (l, a) = case () of
      _ | 64 <= w -> (8, 25)   -- 30 bit =>   1G clauses
      _ | 60 <= w -> (8, 24)   -- 26 bit =>  64M clauses
      _ | 32 <= w -> (6,  7)   -- 18 bit => 256K clauses
      _ | 29 <= w -> (6,  5)   -- 17 bit => 128K clauses
--      _ -> error "Int on your CPU doesn't have sufficient bit width."

{-# INLINABLE sortClauses #-}
sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int
sortClauses s cm nneeds = do
  -- constants
  let
    rankMax :: Int
    rankMax = 2 ^ rankWidth - 1
    activityMax :: Int
    activityMax = 2 ^ activityWidth - 1
    activityScale :: Double
    activityScale = fromIntegral activityMax
    indexMax :: Int
    indexMax = (2 ^ indexWidth - 1) -- 67,108,863 for 26
  n <- numberOfClauses cm
  -- when (indexMax < n) $ error $ "## The number of learnt clauses " ++ show n ++ " exceeds mios's " ++ show indexWidth ++" bit manage capacity"
  vec <- getClauseVector cm
  keys <- getKeyVector cm
  -- 1: assign keys
  let
    assignKey :: Int -> Int -> IO Int
    assignKey ((< n) -> False) m = return m
    assignKey i m = do
      c <- getNthClause vec i
      k <- (\k -> if k == 2 then return k else fromEnum <$> getBool (protected c)) =<< sizeOfClause c
      case k of
        1 -> setBool (protected c) False >> setNth keys i (shiftL 2 indexWidth + i) >> assignKey (i + 1) (m + 1)
        2 -> setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1)
        _ -> do
            l <- locked s c      -- this is expensive
            if l
              then setNth keys i (shiftL 1 indexWidth + i) >> assignKey (i + 1) (m + 1)
              else do
                  d <- ranking' c
                  b <- floor . (activityScale *) . (1 -) . logBase claActivityThreshold . max 1 <$> getDouble (activity c)
                  setNth keys i $ shiftL (min rankMax d) (activityWidth + indexWidth) + shiftL b indexWidth + i
                  assignKey (i + 1) m
  limit <- min n . (+ nneeds) <$> assignKey 0 0
  -- 2: sort keyVector
  let
    sortOnRange :: Int -> Int -> IO ()
    sortOnRange left right
      | limit < left = return ()
      | left >= right = return ()
      | left + 1 == right = do
          a <- getNth keys left
          b <- getNth keys right
          unless (a < b) $ swapBetween keys left right
      | otherwise = do
          let p = div (left + right) 2
          pivot <- getNth keys p
          swapBetween keys p left -- set a sentinel for r'
          let
            nextL :: Int -> IO Int
            nextL i@((<= right) -> False) = return i
            nextL i = do v <- getNth keys i; if v < pivot then nextL (i + 1) else return i
            nextR :: Int -> IO Int
            nextR i = do v <- getNth keys i; if pivot < v then nextR (i - 1) else return i
            divide :: Int -> Int -> IO Int
            divide l r = do
              l' <- nextL l
              r' <- nextR r
              if l' < r' then swapBetween keys l' r' >> divide (l' + 1) (r' - 1) else return r'
          m <- divide (left + 1) right
          swapBetween keys left m
          sortOnRange left (m - 1)
          sortOnRange (m + 1) right
  sortOnRange 0 (n - 1)
  -- 3: place clauses
  let
    seek :: Int -> IO ()
    seek ((< limit) -> False) = return ()
    seek i = do
      bits <- getNth keys i
      when (indexMax < bits) $ do
        c <- getNthClause vec i
        let
          sweep k = do
            k' <- (indexMax .&.) <$> getNth keys k
            setNth keys k k
            if k' == i
              then setNthClause vec k c
              else getNthClause vec k' >>= setNthClause vec k >> sweep k'
        sweep i
      seek $ i + 1
  seek 0
  return limit

-- | #M22
--
-- simplify : [void] -> [bool]
--
-- __Description:__
--   Simplify the clause database according to the current top-level assigment. Currently, the only
--   thing done here is the removal of satisfied clauses, but more things can be put here.
--
{-# INLINABLE simplifyDB #-}
simplifyDB :: Solver -> IO Bool
simplifyDB s@Solver{..} = do
  good <- getBool ok
  if good
    then do
      p <- propagate s
      if p /= NullClause
        then setBool ok False >> return False
        else do
            -- Clear watcher lists:
            n <- sizeOfStack trail
            let
              vec = asVec trail
              loopOnLit ((< n) -> False) = return ()
              loopOnLit i = do
                l <- getNth vec i
                clearManager . getNthWatcher watches $ l
                clearManager . getNthWatcher watches $ negateLit l
                loopOnLit $ i + 1
            loopOnLit 0
            -- Remove satisfied clauses:
            let
              for :: Int -> IO Bool
              for ((< 2) -> False) = return True
              for t = do
                let ptr = if t == 0 then learnts else clauses
                vec' <- getClauseVector ptr
                n' <- numberOfClauses ptr
                let
                  loopOnVector :: Int -> Int -> IO Bool
                  loopOnVector ((< n') -> False) j = shrinkManager ptr (n' - j) >> return True
                  loopOnVector i j = do
                        c <- getNthClause vec' i
                        l <- locked s c
                        r <- simplify s c
                        if not l && r
                          then removeWatch s c >> loopOnVector (i + 1) j
                          else setNthClause vec' j c >> loopOnVector (i + 1) (j + 1)
                loopOnVector 0 0
            ret <- for 0
            garbageCollect watches
            return ret
    else return False

-- | #M22
--
-- search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]
--
-- __Description:__
--   Search for a model the specified number of conflicts.
--   NOTE: Use negative value for 'nof_conflicts' indicate infinity.
--
-- __Output:__
--   'l_True' if a partial assigment that is consistent with respect to the clause set is found. If
--   all variables are decision variables, that means that the clause set is satisfiable. 'l_False'
--   if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
{-# INLINABLE search #-}
search :: Solver -> Int -> Int -> IO LiftedBool
search s@Solver{..} nOfConflicts nOfLearnts = do
  -- clear model
  let
    loop :: Int -> IO LiftedBool
    loop conflictC = do
      !confl <- propagate s
      d <- decisionLevel s
      if confl /= NullClause
        then do
            -- CONFLICT
            incrementStat s NumOfBackjump 1
            r <- getInt rootLevel
            if d == r
              then do
                  -- Contradiction found:
                  analyzeFinal s confl False
                  return LFalse
              else do
--                  u <- (== 0) . (flip mod 5000) <$> getNth stats (fromEnum NumOfBackjump)
--                  when u $ do
--                    d <- getDouble varDecay
--                    when (d < 0.95) $ modifyDouble varDecay (+ 0.01)
                  backtrackLevel <- analyze s confl -- 'analyze' resets litsLearnt by itself
                  (s `cancelUntil`) . max backtrackLevel =<< getInt rootLevel
                  newLearntClause s $ asSizedVec litsLearnt
                  k <- sizeOfStack litsLearnt
                  when (k == 1) $ do
                    (v :: Var) <- lit2var <$> getNth (asVec litsLearnt) 0
                    setNth level v 0
                  varDecayActivity s
                  -- claDecayActivity s
                  loop $ conflictC + 1
        else do                 -- NO CONFLICT
            -- Simplify the set of problem clauses:
            when (d == 0) . void $ simplifyDB s -- our simplifier cannot return @False@ here
            k1 <- numberOfClauses learnts
            k2 <- nAssigns s
            when (k1 - k2 >= nOfLearnts) $ reduceDB s -- Reduce the set of learnt clauses
            case () of
             _ | k2 == nVars -> do
                   -- Model found:
                   forM_ [0 .. nVars - 1] $ \i -> setNthBool model i . (lTrue ==) =<< getNth assigns (i + 1)
                   return LTrue
             _ | conflictC >= nOfConflicts -> do
                   -- Reached bound on number of conflicts
                   (s `cancelUntil`) =<< getInt rootLevel -- force a restart
                   claRescaleActivityAfterRestart s
                   incrementStat s NumOfRestart 1
                   return Bottom
             _ -> do
               -- New variable decision:
               v <- select s -- many have heuristic for polarity here
               -- << #phasesaving
               oldVal <- getNth phases v
               unsafeAssume s $ var2lit v (0 < oldVal) -- cannot return @False@
               -- >> #phasesaving
               loop conflictC
  good <- getBool ok
  if good then loop 0 else return LFalse

-- | __Fig. 16. (p.20)__
-- Main solve method.
--
-- __Pre-condition:__ If assumptions are used, 'simplifyDB' must be
-- called right before using this method. If not, a top-level conflict (resulting in a
-- non-usable internal state) cannot be distinguished from a conflict under assumptions.
solve :: (Foldable t) => Solver -> t Lit -> IO Bool
solve s@Solver{..} assumps = do
  -- PUSH INCREMENTAL ASSUMPTIONS:
  let
    injector :: Lit -> Bool -> IO Bool
    injector _ False = return False
    injector a True = do
      b <- assume s a
      if not b
        then do                 -- conflict analyze
            (confl :: Clause) <- getNthClause reason (lit2var a)
            analyzeFinal s confl True
            pushToStack conflict (negateLit a)
            cancelUntil s 0
            return False
        else do
            confl <- propagate s
            if confl /= NullClause
              then do
                  analyzeFinal s confl True
                  cancelUntil s 0
                  return False
              else return True
  good <- simplifyDB s
  x <- if good then foldrM injector True assumps else return False
  if not x
    then return False
    else do
        setInt rootLevel =<< decisionLevel s
        -- SOLVE:
        nc <- fromIntegral <$> nClauses s
        let
          while :: Double -> Double -> IO Bool
          while nOfConflicts nOfLearnts = do
            status <- search s (floor nOfConflicts) (floor nOfLearnts)
            if status == Bottom
              then while (1.5 * nOfConflicts) (1.1 * nOfLearnts)
              else cancelUntil s 0 >> return (status == LTrue)
        while 100 (nc / 3.0)

--
-- 'enqueue' is defined in 'Solver'; most functions in M114 use 'unsafeEnqueue'
--
{-# INLINABLE unsafeEnqueue #-}
unsafeEnqueue :: Solver -> Lit -> Clause -> IO ()
unsafeEnqueue s@Solver{..} p from = do
  let v = lit2var p
  setNth assigns v $! if positiveLit p then lTrue else lFalse
  setNth level v =<< decisionLevel s
  setNthClause reason v from     -- NOTE: @from@ might be NULL!
  pushToStack trail p

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