content: {-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
  {-# OPTIONS_HADDOCK show-extensions #-}
  {-# LANGUAGE BangPatterns #-}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE DeriveDataTypeable #-}
  {-# LANGUAGE InstanceSigs #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE RecursiveDo #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  #ifdef __GLASGOW_HASKELL__
  {-# LANGUAGE MagicHash #-}
  {-# LANGUAGE UnboxedTuples #-}
  #endif
  #include "MachDeps.h"
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  ToySolver.SAT.Solver.CDCL
  -- Copyright   :  (c) Masahiro Sakai 2012-2014
  -- License     :  BSD-style
  --
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  provisional
  -- Portability :  non-portable
  --
  -- A CDCL SAT solver.
  --
  -- It follows the design of MiniSat and SAT4J.
  --
  -- See also:
  --
  -- * <http://hackage.haskell.org/package/funsat>
  --
  -- * <http://hackage.haskell.org/package/incremental-sat-solver>
  --
  -----------------------------------------------------------------------------
  module ToySolver.SAT.Solver.CDCL
    (
    -- * The @Solver@ type
      Solver
    , newSolver
    , newSolverWithConfig
  
    -- * Basic data structures
    , Var
    , Lit
    , literal
    , litNot
    , litVar
    , litPolarity
    , evalLit
  
    -- * Problem specification
    , newVar
    , newVars
    , newVars_
    , resizeVarCapacity
    -- ** Clauses
    , AddClause (..)
    , Clause
    , evalClause
    , PackedClause
    , packClause
    , unpackClause
    -- ** Cardinality constraints
    , AddCardinality (..)
    , AtLeast
    , Exactly
    , evalAtLeast
    , evalExactly
  
    -- ** (Linear) pseudo-boolean constraints
    , AddPBLin (..)
    , PBLinTerm
    , PBLinSum
    , PBLinAtLeast
    , PBLinExactly
    , evalPBLinSum
    , evalPBLinAtLeast
    , evalPBLinExactly
    -- ** XOR clauses
    , AddXORClause (..)
    , XORClause
    , evalXORClause
    -- ** Type-2 SOS constraints
    , addSOS2
    , evalSOS2
    -- ** Theory
    , setTheory
  
    -- * Solving
    , solve
    , solveWith
    , BudgetExceeded (..)
    , cancel
    , Canceled (..)
  
    -- * Extract results
    , IModel (..)
    , Model
    , getModel
    , getFailedAssumptions
    , getAssumptionsImplications
  
    -- * Solver configulation
    , module ToySolver.SAT.Solver.CDCL.Config
    , getConfig
    , setConfig
    , modifyConfig
    , setVarPolarity
    , setRandomGen
    , getRandomGen
    , setConfBudget
  
    -- * Callbacks
    , setLogger
    , clearLogger
    , setTerminateCallback
    , clearTerminateCallback
    , setLearnCallback
    , clearLearnCallback
  
    -- * Read state
    , getNVars
    , getNConstraints
    , getNLearntConstraints
    , getVarFixed
    , getLitFixed
    , getFixedLiterals
  
    -- * Internal API
    , varBumpActivity
    , varDecayActivity
    ) where
  
  import Prelude hiding (log)
  import Control.Loop
  import Control.Monad
  import Control.Monad.IO.Class
  import Control.Monad.Trans
  import Control.Monad.Trans.Except
  import Control.Exception
  import Data.Array.IO
  import Data.Array.Unsafe (unsafeFreeze)
  import Data.Array.Base (unsafeRead, unsafeWrite)
  #if !MIN_VERSION_hashable(1,4,3)
  import Data.Bits (xor) -- for defining 'combine' function
  #endif
  import Data.Coerce
  import Data.Default.Class
  import Data.Either
  import Data.Function (on)
  import Data.Hashable
  import Data.HashSet (HashSet)
  import qualified Data.HashSet as HashSet
  import Data.IORef
  import Data.Int
  import Data.List (delete, find, foldl', maximumBy, partition, sortBy)
  import Data.Maybe
  import Data.Ord
  import qualified Data.IntMap.Strict as IM
  import qualified Data.IntSet as IS
  import qualified Data.Set as Set
  import ToySolver.Internal.Data.IOURef
  import qualified ToySolver.Internal.Data.IndexedPriorityQueue as PQ
  import qualified ToySolver.Internal.Data.Vec as Vec
  import Data.Typeable
  import System.Clock
  import qualified System.Random.MWC as Rand
  import Text.Printf
  
  #ifdef __GLASGOW_HASKELL__
  import GHC.Types (IO (..))
  import GHC.Exts hiding (Constraint)
  #endif
  
  import ToySolver.Data.LBool
  import ToySolver.SAT.Solver.CDCL.Config
  import ToySolver.SAT.Types
  import ToySolver.SAT.TheorySolver
  import ToySolver.Internal.Util (revMapM)
  
  {--------------------------------------------------------------------
    LitArray
  --------------------------------------------------------------------}
  
  newtype LitArray = LitArray (IOUArray Int PackedLit) deriving (Eq)
  
  newLitArray :: [Lit] -> IO LitArray
  newLitArray lits = do
    let size = length lits
    liftM LitArray $ newListArray (0, size-1) (map packLit lits)
  
  readLitArray :: LitArray -> Int -> IO Lit
  #if EXTRA_BOUNDS_CHECKING
  readLitArray (LitArray a) i = liftM unpackLit $ readArray a i
  #else
  readLitArray (LitArray a) i = liftM unpackLit $ unsafeRead a i
  #endif
  
  writeLitArray :: LitArray -> Int -> Lit -> IO ()
  #if EXTRA_BOUNDS_CHECKING
  writeLitArray (LitArray a) i lit = writeArray a i (packLit lit)
  #else
  writeLitArray (LitArray a) i lit = unsafeWrite a i (packLit lit)
  #endif
  
  getLits :: LitArray -> IO [Lit]
  getLits (LitArray a) = liftM (map unpackLit) $ getElems a
  
  getLitArraySize :: LitArray -> IO Int
  getLitArraySize (LitArray a) = do
    (lb,ub) <- getBounds a
    assert (lb == 0) $ return ()
    return $! ub-lb+1
  
  {--------------------------------------------------------------------
    internal data structures
  --------------------------------------------------------------------}
  
  type Level = Int
  
  levelRoot :: Level
  levelRoot = 0
  
  litIndex :: Lit -> Int
  litIndex l = 2 * (litVar l - 1) + (if litPolarity l then 1 else 0)
  
  {-# INLINE varValue #-}
  varValue :: Solver -> Var -> IO LBool
  varValue solver v = liftM coerce $ Vec.unsafeRead (svVarValue solver) (v - 1)
  
  {-# INLINE litValue #-}
  litValue :: Solver -> Lit -> IO LBool
  litValue solver !l = do
    -- litVar による heap allocation を避けるために、
    -- litPolarityによる分岐後にvarValueを呼ぶ。
    if litPolarity l then
      varValue solver l
    else do
      m <- varValue solver (negate l)
      return $! lnot m
  
  getVarFixed :: Solver -> Var -> IO LBool
  getVarFixed solver !v = do
    lv <- Vec.unsafeRead (svVarLevel solver) (v - 1)
    if lv == levelRoot then
      varValue solver v
    else
      return lUndef
  
  getLitFixed :: Solver -> Lit -> IO LBool
  getLitFixed solver !l = do
    -- litVar による heap allocation を避けるために、
    -- litPolarityによる分岐後にvarGetFixedを呼ぶ。
    if litPolarity l then
      getVarFixed solver l
    else do
      m <- getVarFixed solver (negate l)
      return $! lnot m
  
  getNFixed :: Solver -> IO Int
  getNFixed solver = do
    lv <- getDecisionLevel solver
    if lv == levelRoot then
      Vec.getSize (svTrail solver)
    else
      Vec.unsafeRead (svTrailLimit solver) 0
  
  -- | it returns a set of literals that are fixed without any assumptions.
  getFixedLiterals :: Solver -> IO [Lit]
  getFixedLiterals solver = do
    n <- getNFixed solver
    revMapM (Vec.unsafeRead (svTrail solver)) [0..n-1]
  
  varLevel :: Solver -> Var -> IO Level
  varLevel solver !v = do
    val <- varValue solver v
    when (val == lUndef) $ error ("ToySolver.SAT.varLevel: unassigned var " ++ show v)
    Vec.unsafeRead (svVarLevel solver) (v - 1)
  
  litLevel :: Solver -> Lit -> IO Level
  litLevel solver l = varLevel solver (litVar l)
  
  varReason :: Solver -> Var -> IO (Maybe SomeConstraintHandler)
  varReason solver !v = do
    val <- varValue solver v
    when (val == lUndef) $ error ("ToySolver.SAT.varReason: unassigned var " ++ show v)
    Vec.unsafeRead (svVarReason solver) (v - 1)
  
  varAssignNo :: Solver -> Var -> IO Int
  varAssignNo solver !v = do
    val <- varValue solver v
    when (val == lUndef) $ error ("ToySolver.SAT.varAssignNo: unassigned var " ++ show v)
    Vec.unsafeRead (svVarTrailIndex solver) (v - 1)
  
  -- | Solver instance
  data Solver
    = Solver
    { svOk           :: !(IORef Bool)
  
    , svVarQueue     :: !PQ.PriorityQueue
    , svTrail        :: !(Vec.UVec Lit)
    , svTrailLimit   :: !(Vec.UVec Lit)
    , svTrailNPropagated :: !(IOURef Int)
  
    -- variable information
    , svVarValue      :: !(Vec.UVec Int8) -- should be 'Vec.UVec LBool' but it's difficult to define MArray instance
    , svVarPolarity   :: !(Vec.UVec Bool)
    , svVarActivity   :: !(Vec.UVec VarActivity)
    , svVarTrailIndex :: !(Vec.UVec Int)
    , svVarLevel      :: !(Vec.UVec Int)
    -- | will be invoked once when the variable is assigned
    , svVarWatches      :: !(Vec.Vec [SomeConstraintHandler])
    , svVarOnUnassigned :: !(Vec.Vec [SomeConstraintHandler])
    , svVarReason       :: !(Vec.Vec (Maybe SomeConstraintHandler))
    -- | exponential moving average estimate
    , svVarEMAScaled    :: !(Vec.UVec Double)
    -- | When v was last assigned
    , svVarWhenAssigned :: !(Vec.UVec Int)
    -- | The number of learnt clauses v participated in generating since Assigned.
    , svVarParticipated :: !(Vec.UVec Int)
    -- | The number of learnt clauses v reasoned in generating since Assigned.
    , svVarReasoned     :: !(Vec.UVec Int)
  
    -- | will be invoked when this literal is falsified
    , svLitWatches   :: !(Vec.Vec [SomeConstraintHandler])
    , svLitOccurList :: !(Vec.Vec (HashSet SomeConstraintHandler))
  
    , svConstrDB     :: !(IORef [SomeConstraintHandler])
    , svLearntDB     :: !(IORef (Int,[SomeConstraintHandler]))
  
    -- Theory
    , svTheorySolver  :: !(IORef (Maybe TheorySolver))
    , svTheoryChecked :: !(IOURef Int)
  
    -- Result
    , svModel        :: !(IORef (Maybe Model))
    , svFailedAssumptions :: !(IORef LitSet)
    , svAssumptionsImplications :: !(IORef LitSet)
  
    -- Statistics
    , svNDecision    :: !(IOURef Int)
    , svNRandomDecision :: !(IOURef Int)
    , svNConflict    :: !(IOURef Int)
    , svNRestart     :: !(IOURef Int)
    , svNLearntGC    :: !(IOURef Int)
    , svNRemovedConstr :: !(IOURef Int)
  
    -- Configulation
    , svConfig :: !(IORef Config)
    , svRandomGen  :: !(IORef Rand.GenIO)
    , svConfBudget :: !(IOURef Int)
    , svTerminateCallback :: !(IORef (Maybe (IO Bool)))
    , svLearnCallback :: !(IORef (Maybe (Clause -> IO ())))
  
    -- Logging
    , svLogger :: !(IORef (Maybe (String -> IO ())))
    , svStartWC    :: !(IORef TimeSpec)
    , svLastStatWC :: !(IORef TimeSpec)
  
    -- Working spaces
    , svCanceled        :: !(IORef Bool)
    , svAssumptions     :: !(Vec.UVec Lit)
    , svLearntLim       :: !(IORef Int)
    , svLearntLimAdjCnt :: !(IORef Int)
    , svLearntLimSeq    :: !(IORef [(Int,Int)])
    , svSeen :: !(Vec.UVec Bool)
    , svPBLearnt :: !(IORef (Maybe PBLinAtLeast))
  
    -- | Amount to bump next variable with.
    , svVarInc       :: !(IOURef Double)
  
    -- | Amount to bump next constraint with.
    , svConstrInc    :: !(IOURef Double)
  
    -- ERWA / LRB
  
    -- | step-size parameter α
    , svERWAStepSize :: !(IOURef Double)
    , svEMAScale :: !(IOURef Double)
    , svLearntCounter :: !(IOURef Int)
    }
  
  markBad :: Solver -> IO ()
  markBad solver = do
    writeIORef (svOk solver) False
    bcpClear solver
  
  bcpDequeue :: Solver -> IO (Maybe Lit)
  bcpDequeue solver = do
    n <- Vec.getSize (svTrail solver)
    m <- readIOURef (svTrailNPropagated solver)
    if m==n then
      return Nothing
    else do
      -- m < n
      lit <- Vec.unsafeRead (svTrail solver) m
      modifyIOURef (svTrailNPropagated solver) (+1)
      return (Just lit)
  
  bcpIsEmpty :: Solver -> IO Bool
  bcpIsEmpty solver = do
    p <- readIOURef (svTrailNPropagated solver)
    n <- Vec.getSize (svTrail solver)
    return $! n == p
  
  bcpCheckEmpty :: Solver -> IO ()
  bcpCheckEmpty solver = do
    empty <- bcpIsEmpty solver
    unless empty $
      error "BUG: BCP Queue should be empty at this point"
  
  bcpClear :: Solver -> IO ()
  bcpClear solver = do
    m <- Vec.getSize (svTrail solver)
    writeIOURef (svTrailNPropagated solver) m
  
  assignBy :: Solver -> Lit -> SomeConstraintHandler -> IO Bool
  assignBy solver lit c = do
    lv <- getDecisionLevel solver
    let !c2 = if lv == levelRoot
              then Nothing
              else Just c
    assign_ solver lit c2
  
  assign :: Solver -> Lit -> IO Bool
  assign solver lit = assign_ solver lit Nothing
  
  assign_ :: Solver -> Lit -> Maybe SomeConstraintHandler -> IO Bool
  assign_ solver !lit reason = assert (validLit lit) $ do
    let val = liftBool (litPolarity lit)
  
    val0 <- varValue solver (litVar lit)
    if val0 /= lUndef then do
      return $ val == val0
    else do
      idx <- Vec.getSize (svTrail solver)
      lv <- getDecisionLevel solver
  
      Vec.unsafeWrite (svVarValue solver) (litVar lit - 1) (coerce val)
      Vec.unsafeWrite (svVarTrailIndex solver) (litVar lit - 1) idx
      Vec.unsafeWrite (svVarLevel solver) (litVar lit - 1) lv
      Vec.unsafeWrite (svVarReason solver) (litVar lit - 1) reason
      Vec.unsafeWrite (svVarWhenAssigned solver) (litVar lit - 1) =<< readIOURef (svLearntCounter solver)
      Vec.unsafeWrite (svVarParticipated solver) (litVar lit - 1) 0
      Vec.unsafeWrite (svVarReasoned solver) (litVar lit - 1) 0
  
      Vec.push (svTrail solver) lit
  
      when debugMode $ logIO solver $ do
        let r = case reason of
                  Nothing -> ""
                  Just _ -> " by propagation"
        return $ printf "assign(level=%d): %d%s" lv lit r
  
      return True
  
  unassign :: Solver -> Var -> IO ()
  unassign solver !v = assert (validVar v) $ do
    val <- varValue solver v
    when (val == lUndef) $ error "unassign: should not happen"
  
    flag <- configEnablePhaseSaving <$> getConfig solver
    when flag $ Vec.unsafeWrite (svVarPolarity solver) (v - 1) $! fromJust (unliftBool val)
  
    Vec.unsafeWrite (svVarValue solver) (v - 1) (coerce lUndef)
    Vec.unsafeWrite (svVarTrailIndex solver) (v - 1) maxBound
    Vec.unsafeWrite (svVarLevel solver) (v - 1) maxBound
    Vec.unsafeWrite (svVarReason solver) (v - 1) Nothing
  
    -- ERWA / LRB computation
    interval <- do
      t2 <- readIOURef (svLearntCounter solver)
      t1 <- Vec.unsafeRead (svVarWhenAssigned solver) (v - 1)
      return (t2 - t1)
    -- Interval = 0 is possible due to restarts.
    when (interval > 0) $ do
      participated <- Vec.unsafeRead (svVarParticipated solver) (v - 1)
      reasoned <- Vec.unsafeRead (svVarReasoned solver) (v - 1)
      alpha <- readIOURef (svERWAStepSize solver)
      let learningRate = fromIntegral participated / fromIntegral interval
          reasonSideRate = fromIntegral reasoned / fromIntegral interval
      scale <- readIOURef (svEMAScale solver)
      -- ema := (1 - α)ema + α*r
      Vec.unsafeModify (svVarEMAScaled solver) (v - 1) (\orig -> (1 - alpha) * orig + alpha * scale * (learningRate + reasonSideRate))
      -- If v is assigned by random decision, it's possible that v is still in the queue.
      PQ.update (svVarQueue solver) v
  
    let !l = if val == lTrue then v else -v
    cs <- Vec.unsafeRead (svVarOnUnassigned solver) (v - 1)
    Vec.unsafeWrite (svVarOnUnassigned solver) (v - 1) []
    forM_ cs $ \c ->
      constrOnUnassigned solver c c l
  
    PQ.enqueue (svVarQueue solver) v
  
  addOnUnassigned :: Solver -> SomeConstraintHandler -> Lit -> IO ()
  addOnUnassigned solver constr !l = do
    val <- varValue solver (litVar l)
    when (val == lUndef) $ error "addOnUnassigned: should not happen"
    Vec.unsafeModify (svVarOnUnassigned solver) (litVar l - 1) (constr :)
  
  -- | Register the constraint to be notified when the literal becames false.
  watchLit :: Solver -> Lit -> SomeConstraintHandler -> IO ()
  watchLit solver !lit c = Vec.unsafeModify (svLitWatches solver) (litIndex lit) (c : )
  
  -- | Register the constraint to be notified when the variable is assigned.
  watchVar :: Solver -> Var -> SomeConstraintHandler -> IO ()
  watchVar solver !var c = Vec.unsafeModify (svVarWatches solver) (var - 1) (c :)
  
  unwatchLit :: Solver -> Lit -> SomeConstraintHandler -> IO ()
  unwatchLit solver !lit c = Vec.unsafeModify (svLitWatches solver) (litIndex lit) (delete c)
  
  unwatchVar :: Solver -> Lit -> SomeConstraintHandler -> IO ()
  unwatchVar solver !var c = Vec.unsafeModify (svVarWatches solver) (var - 1) (delete c)
  
  addToDB :: ConstraintHandler c => Solver -> c -> IO ()
  addToDB solver c = do
    let c2 = toConstraintHandler c
    modifyIORef (svConstrDB solver) (c2 : )
    when debugMode $ logIO solver $ do
      str <- showConstraintHandler c
      return $ printf "constraint %s is added" str
  
    b <- isPBRepresentable c
    when b $ do
      (lhs,_) <- toPBLinAtLeast c
      forM_ lhs $ \(_,lit) -> do
         Vec.unsafeModify (svLitOccurList solver) (litIndex lit) (HashSet.insert c2)
  
  addToLearntDB :: ConstraintHandler c => Solver -> c -> IO ()
  addToLearntDB solver c = do
    modifyIORef (svLearntDB solver) $ \(n,xs) -> (n+1, toConstraintHandler c : xs)
    when debugMode $ logIO solver $ do
      str <- showConstraintHandler c
      return $ printf "constraint %s is added" str
  
  reduceDB :: Solver -> IO ()
  reduceDB solver = do
    (_,cs) <- readIORef (svLearntDB solver)
  
    xs <- forM cs $ \c -> do
      p <- constrIsProtected solver c
      w <- constrWeight solver c
      actval <- constrReadActivity c
      return (c, (p, w*actval))
  
    -- Note that False <= True
    let ys = sortBy (comparing snd) xs
        (zs,ws) = splitAt (length ys `div` 2) ys
  
    let loop [] ret = return ret
        loop ((c,(isShort,_)) : rest) ret = do
          flag <- if isShort
                  then return True
                  else isLocked solver c
          if flag then
            loop rest (c:ret)
          else do
            detach solver c
            loop rest ret
    zs2 <- loop zs []
  
    let cs2 = zs2 ++ map fst ws
        n2 = length cs2
  
    -- log solver $ printf "learnt constraints deletion: %d -> %d" n n2
    writeIORef (svLearntDB solver) (n2,cs2)
  
  type VarActivity = Double
  
  varActivity :: Solver -> Var -> IO VarActivity
  varActivity solver v = Vec.unsafeRead (svVarActivity solver) (v - 1)
  
  varDecayActivity :: Solver -> IO ()
  varDecayActivity solver = do
    d <- configVarDecay <$> getConfig solver
    modifyIOURef (svVarInc solver) (d*)
  
  varBumpActivity :: Solver -> Var -> IO ()
  varBumpActivity solver !v = do
    inc <- readIOURef (svVarInc solver)
    Vec.unsafeModify (svVarActivity solver) (v - 1) (+inc)
    conf <- getConfig solver
    when (configBranchingStrategy conf == BranchingVSIDS) $ do
      PQ.update (svVarQueue solver) v
    aval <- Vec.unsafeRead (svVarActivity solver) (v - 1)
    when (aval > 1e20) $
      -- Rescale
      varRescaleAllActivity solver
  
  varRescaleAllActivity :: Solver -> IO ()
  varRescaleAllActivity solver = do
    let a = svVarActivity solver
    n <- getNVars solver
    forLoop 0 (<n) (+1) $ \i ->
      Vec.unsafeModify a i (* 1e-20)
    modifyIOURef (svVarInc solver) (* 1e-20)
  
  varEMAScaled :: Solver -> Var -> IO Double
  varEMAScaled solver v = Vec.unsafeRead (svVarEMAScaled solver) (v - 1)
  
  varIncrementParticipated :: Solver -> Var -> IO ()
  varIncrementParticipated solver v = Vec.unsafeModify (svVarParticipated solver) (v - 1) (+1)
  
  varIncrementReasoned :: Solver -> Var -> IO ()
  varIncrementReasoned solver v = Vec.unsafeModify (svVarReasoned solver) (v - 1) (+1)
  
  varEMADecay :: Solver -> IO ()
  varEMADecay solver = do
    config <- getConfig solver
  
    alpha <- readIOURef (svERWAStepSize solver)
    let alphaMin = configERWAStepSizeMin config
    when (alpha > alphaMin) $ do
      writeIOURef (svERWAStepSize solver) (max alphaMin (alpha - configERWAStepSizeDec config))
  
    case configBranchingStrategy config of
      BranchingLRB -> do
        modifyIOURef (svEMAScale solver) (configEMADecay config *)
        scale <- readIOURef (svEMAScale solver)
        when (scale > 1e20) $ do
          n <- getNVars solver
          let a = svVarEMAScaled solver
          forLoop 0 (<n) (+1) $ \i -> Vec.unsafeModify a i (/ scale)
          writeIOURef (svEMAScale solver) 1.0
      _ -> return ()
  
  variables :: Solver -> IO [Var]
  variables solver = do
    n <- getNVars solver
    return [1 .. n]
  
  -- | number of variables of the problem.
  getNVars :: Solver -> IO Int
  getNVars solver = Vec.getSize (svVarValue solver)
  
  -- | number of assigned
  getNAssigned :: Solver -> IO Int
  getNAssigned solver = Vec.getSize (svTrail solver)
  
  -- | number of constraints.
  getNConstraints :: Solver -> IO Int
  getNConstraints solver = do
    xs <- readIORef (svConstrDB solver)
    return $ length xs
  
  -- | number of learnt constrints.
  getNLearntConstraints :: Solver -> IO Int
  getNLearntConstraints solver = do
    (n,_) <- readIORef (svLearntDB solver)
    return n
  
  learntConstraints :: Solver -> IO [SomeConstraintHandler]
  learntConstraints solver = do
    (_,cs) <- readIORef (svLearntDB solver)
    return cs
  
  {--------------------------------------------------------------------
    Solver
  --------------------------------------------------------------------}
  
  -- | Create a new 'Solver' instance.
  newSolver :: IO Solver
  newSolver = newSolverWithConfig def
  
  -- | Create a new 'Solver' instance with a given configulation.
  newSolverWithConfig :: Config -> IO Solver
  newSolverWithConfig config = do
   rec
    ok   <- newIORef True
    trail <- Vec.new
    trail_lim <- Vec.new
    trail_nprop <- newIOURef 0
  
    varValue <- Vec.new
    varPolarity <- Vec.new
    varActivity <- Vec.new
    varTrailIndex <- Vec.new
    varLevel <- Vec.new
    varWatches <- Vec.new
    varOnUnassigned <- Vec.new
    varReason <- Vec.new
    varEMAScaled <- Vec.new
    varWhenAssigned <- Vec.new
    varParticipated <- Vec.new
    varReasoned <- Vec.new
    litWatches <- Vec.new
    litOccurList <- Vec.new
  
    vqueue <- PQ.newPriorityQueueBy (ltVar solver)
    db  <- newIORef []
    db2 <- newIORef (0,[])
    as  <- Vec.new
    m   <- newIORef Nothing
    canceled <- newIORef False
    ndecision <- newIOURef 0
    nranddec  <- newIOURef 0
    nconflict <- newIOURef 0
    nrestart  <- newIOURef 0
    nlearntgc <- newIOURef 0
    nremoved  <- newIOURef 0
  
    constrInc   <- newIOURef 1
    varInc   <- newIOURef 1
  
    configRef <- newIORef config
  
    learntLim       <- newIORef undefined
    learntLimAdjCnt <- newIORef (-1)
    learntLimSeq    <- newIORef undefined
  
    logger <- newIORef Nothing
    startWC    <- newIORef undefined
    lastStatWC <- newIORef undefined
  
    randgen  <- newIORef =<< Rand.create
  
    failed <- newIORef IS.empty
    implied <- newIORef IS.empty
  
    confBudget <- newIOURef (-1)
    terminateCallback <- newIORef Nothing
    learntCallback <- newIORef Nothing
  
    tsolver <- newIORef Nothing
    tchecked <- newIOURef 0
  
    seen <- Vec.new
    pbLearnt <- newIORef Nothing
  
    alpha <- newIOURef 0.4
    emaScale <- newIOURef 1.0
    learntCounter <- newIOURef 0
  
    let solver =
          Solver
          { svOk = ok
          , svVarQueue   = vqueue
          , svTrail      = trail
          , svTrailLimit = trail_lim
          , svTrailNPropagated = trail_nprop
  
          , svVarValue        = varValue
          , svVarPolarity     = varPolarity
          , svVarActivity     = varActivity
          , svVarTrailIndex   = varTrailIndex
          , svVarLevel        = varLevel
          , svVarWatches      = varWatches
          , svVarOnUnassigned = varOnUnassigned
          , svVarReason       = varReason
          , svVarEMAScaled    = varEMAScaled
          , svVarWhenAssigned = varWhenAssigned
          , svVarParticipated = varParticipated
          , svVarReasoned     = varReasoned
          , svLitWatches      = litWatches
          , svLitOccurList    = litOccurList
  
          , svConstrDB   = db
          , svLearntDB   = db2
  
          -- Theory
          , svTheorySolver  = tsolver
          , svTheoryChecked = tchecked
  
          -- Result
          , svModel      = m
          , svFailedAssumptions = failed
          , svAssumptionsImplications = implied
  
          -- Statistics
          , svNDecision  = ndecision
          , svNRandomDecision = nranddec
          , svNConflict  = nconflict
          , svNRestart   = nrestart
          , svNLearntGC  = nlearntgc
          , svNRemovedConstr = nremoved
  
          -- Configulation
          , svConfig     = configRef
          , svRandomGen  = randgen
          , svConfBudget = confBudget
          , svTerminateCallback = terminateCallback
          , svLearnCallback = learntCallback
  
          -- Logging
          , svLogger = logger
          , svStartWC    = startWC
          , svLastStatWC = lastStatWC
  
          -- Working space
          , svCanceled        = canceled
          , svAssumptions     = as
          , svLearntLim       = learntLim
          , svLearntLimAdjCnt = learntLimAdjCnt
          , svLearntLimSeq    = learntLimSeq
          , svVarInc      = varInc
          , svConstrInc   = constrInc
          , svSeen = seen
          , svPBLearnt = pbLearnt
  
          , svERWAStepSize = alpha
          , svEMAScale = emaScale
          , svLearntCounter = learntCounter
          }
   return solver
  
  ltVar :: Solver -> Var -> Var -> IO Bool
  ltVar solver !v1 !v2 = do
    conf <- getConfig solver
    case configBranchingStrategy conf of
      BranchingVSIDS -> do
        a1 <- varActivity solver v1
        a2 <- varActivity solver v2
        return $! a1 > a2
      _ -> do -- BranchingERWA and BranchingLRB
        a1 <- varEMAScaled solver v1
        a2 <- varEMAScaled solver v1
        return $! a1 > a2
  
  {--------------------------------------------------------------------
    Problem specification
  --------------------------------------------------------------------}
  
  instance NewVar IO Solver where
    newVar :: Solver -> IO Var
    newVar solver = do
      n <- Vec.getSize (svVarValue solver)
  #if SIZEOF_HSINT > 4
      when (n == fromIntegral (maxBound :: PackedLit)) $ do
        error "cannot allocate more variables"
  #endif
      let v = n + 1
  
      Vec.push (svVarValue solver) (coerce lUndef)
      Vec.push (svVarPolarity solver) True
      Vec.push (svVarActivity solver) 0
      Vec.push (svVarTrailIndex solver) maxBound
      Vec.push (svVarLevel solver) maxBound
      Vec.push (svVarWatches solver) []
      Vec.push (svVarOnUnassigned solver) []
      Vec.push (svVarReason solver) Nothing
      Vec.push (svVarEMAScaled solver) 0
      Vec.push (svVarWhenAssigned solver) (-1)
      Vec.push (svVarParticipated solver) 0
      Vec.push (svVarReasoned solver) 0
  
      Vec.push (svLitWatches solver) []
      Vec.push (svLitWatches solver) []
      Vec.push (svLitOccurList solver) HashSet.empty
      Vec.push (svLitOccurList solver) HashSet.empty
  
      PQ.enqueue (svVarQueue solver) v
      Vec.push (svSeen solver) False
      return v
  
    newVars :: Solver -> Int -> IO [Var]
    newVars solver n = do
      nv <- getNVars solver
  #if SIZEOF_HSINT > 4
      when (nv + n > fromIntegral (maxBound :: PackedLit)) $ do
        error "cannot allocate more variables"
  #endif
      resizeVarCapacity solver (nv+n)
      replicateM n (newVar solver)
  
    newVars_ :: Solver -> Int -> IO ()
    newVars_ solver n = do
      nv <- getNVars solver
  #if SIZEOF_HSINT > 4
      when (nv + n > fromIntegral (maxBound :: PackedLit)) $ do
        error "cannot allocate more variables"
  #endif
      resizeVarCapacity solver (nv+n)
      replicateM_ n (newVar solver)
  
  -- |Pre-allocate internal buffer for @n@ variables.
  resizeVarCapacity :: Solver -> Int -> IO ()
  resizeVarCapacity solver n = do
    Vec.resizeCapacity (svVarValue solver) n
    Vec.resizeCapacity (svVarPolarity solver) n
    Vec.resizeCapacity (svVarActivity solver) n
    Vec.resizeCapacity (svVarTrailIndex solver) n
    Vec.resizeCapacity (svVarLevel solver) n
    Vec.resizeCapacity (svVarWatches solver) n
    Vec.resizeCapacity (svVarOnUnassigned solver) n
    Vec.resizeCapacity (svVarReason solver) n
    Vec.resizeCapacity (svVarEMAScaled solver) n
    Vec.resizeCapacity (svVarWhenAssigned solver) n
    Vec.resizeCapacity (svVarParticipated solver) n
    Vec.resizeCapacity (svVarReasoned solver) n
    Vec.resizeCapacity (svLitWatches solver) (n*2)
    Vec.resizeCapacity (svLitOccurList solver) (n*2)
    Vec.resizeCapacity (svSeen solver) n
    PQ.resizeHeapCapacity (svVarQueue solver) n
    PQ.resizeTableCapacity (svVarQueue solver) (n+1)
  
  instance AddClause IO Solver where
    addClause :: Solver -> Clause -> IO ()
    addClause solver lits = do
      d <- getDecisionLevel solver
      assert (d == levelRoot) $ return ()
  
      ok <- readIORef (svOk solver)
      when ok $ do
        m <- instantiateClause (getLitFixed solver) lits
        case normalizeClause =<< m of
          Nothing -> return ()
          Just [] -> markBad solver
          Just [lit] -> do
            {- We do not call 'removeBackwardSubsumedBy' here,
               because subsumed constraints will be removed by 'simplify'. -}
            ret <- assign solver lit
            assert ret $ return ()
            ret2 <- deduce solver
            case ret2 of
              Nothing -> return ()
              Just _ -> markBad solver
          Just lits2 -> do
            subsumed <- checkForwardSubsumption solver lits
            unless subsumed $ do
              removeBackwardSubsumedBy solver ([(1,lit) | lit <- lits2], 1)
              clause <- newClauseHandler lits2 False
              addToDB solver clause
              _ <- basicAttachClauseHandler solver clause
              return ()
  
  instance AddCardinality IO Solver where
    addAtLeast :: Solver -> [Lit] -> Int -> IO ()
    addAtLeast solver lits n = do
      d <- getDecisionLevel solver
      assert (d == levelRoot) $ return ()
  
      ok <- readIORef (svOk solver)
      when ok $ do
        (lits',n') <- liftM normalizeAtLeast $ instantiateAtLeast (getLitFixed solver) (lits,n)
        let len = length lits'
  
        if n' <= 0 then return ()
        else if n' > len then markBad solver
        else if n' == 1 then addClause solver lits'
        else if n' == len then do
          {- We do not call 'removeBackwardSubsumedBy' here,
             because subsumed constraints will be removed by 'simplify'. -}
          forM_ lits' $ \l -> do
            ret <- assign solver l
            assert ret $ return ()
          ret2 <- deduce solver
          case ret2 of
            Nothing -> return ()
            Just _ -> markBad solver
        else do -- n' < len
          removeBackwardSubsumedBy solver ([(1,lit) | lit <- lits'], fromIntegral n')
          c <- newAtLeastHandler lits' n' False
          addToDB solver c
          _ <- basicAttachAtLeastHandler solver c
          return ()
  
  instance AddPBLin IO Solver where
    addPBAtLeast :: Solver -> PBLinSum -> Integer -> IO ()
    addPBAtLeast solver ts n = do
      d <- getDecisionLevel solver
      assert (d == levelRoot) $ return ()
  
      ok <- readIORef (svOk solver)
      when ok $ do
        (ts',n') <- liftM normalizePBLinAtLeast $ instantiatePBLinAtLeast (getLitFixed solver) (ts,n)
  
        case pbToAtLeast (ts',n') of
          Just (lhs',rhs') -> addAtLeast solver lhs' rhs'
          Nothing -> do
            let cs = map fst ts'
                slack = sum cs - n'
            if n' <= 0 then return ()
            else if slack < 0 then markBad solver
            else do
              removeBackwardSubsumedBy solver (ts', n')
              (ts'',n'') <- do
                b <- configEnablePBSplitClausePart <$> getConfig solver
                if b
                then pbSplitClausePart solver (ts',n')
                else return (ts',n')
  
              c <- newPBHandler solver ts'' n'' False
              let constr = toConstraintHandler c
              addToDB solver constr
              ret <- attach solver constr
              if not ret then do
                markBad solver
              else do
                ret2 <- deduce solver
                case ret2 of
                  Nothing -> return ()
                  Just _ -> markBad solver
  
    addPBExactly :: Solver -> PBLinSum -> Integer -> IO ()
    addPBExactly solver ts n = do
      (ts2,n2) <- liftM normalizePBLinExactly $ instantiatePBLinExactly (getLitFixed solver) (ts,n)
      addPBAtLeast solver ts2 n2
      addPBAtMost solver ts2 n2
  
    addPBAtLeastSoft :: Solver -> Lit -> PBLinSum -> Integer -> IO ()
    addPBAtLeastSoft solver sel lhs rhs = do
      (lhs', rhs') <- liftM normalizePBLinAtLeast $ instantiatePBLinAtLeast (getLitFixed solver) (lhs,rhs)
      addPBAtLeast solver ((rhs', litNot sel) : lhs') rhs'
  
    addPBExactlySoft :: Solver -> Lit -> PBLinSum -> Integer -> IO ()
    addPBExactlySoft solver sel lhs rhs = do
      (lhs2, rhs2) <- liftM normalizePBLinExactly $ instantiatePBLinExactly (getLitFixed solver) (lhs,rhs)
      addPBAtLeastSoft solver sel lhs2 rhs2
      addPBAtMostSoft solver sel lhs2 rhs2
  
  -- | See documentation of 'setPBSplitClausePart'.
  pbSplitClausePart :: Solver -> PBLinAtLeast -> IO PBLinAtLeast
  pbSplitClausePart solver (lhs,rhs) = do
    let (ts1,ts2) = partition (\(c,_) -> c >= rhs) lhs
    if length ts1 < 2 then
      return (lhs,rhs)
    else do
      sel <- newVar solver
      addClause solver $ -sel : [l | (_,l) <- ts1]
      return ((rhs,sel) : ts2, rhs)
  
  instance AddXORClause IO Solver where
    addXORClause :: Solver -> [Lit] -> Bool -> IO ()
    addXORClause solver lits rhs = do
      d <- getDecisionLevel solver
      assert (d == levelRoot) $ return ()
  
      ok <- readIORef (svOk solver)
      when ok $ do
        xcl <- instantiateXORClause (getLitFixed solver) (lits,rhs)
        case normalizeXORClause xcl of
          ([], True) -> markBad solver
          ([], False) -> return ()
          ([l], b) -> addClause solver [if b then l else litNot l]
          (l:ls, b) -> do
            c <- newXORClauseHandler ((if b then l else litNot l) : ls) False
            addToDB solver c
            _ <- basicAttachXORClauseHandler solver c
            return ()
  
  {--------------------------------------------------------------------
    Problem solving
  --------------------------------------------------------------------}
  
  -- | Solve constraints.
  -- Returns 'True' if the problem is SATISFIABLE.
  -- Returns 'False' if the problem is UNSATISFIABLE.
  solve :: Solver -> IO Bool
  solve solver = do
    Vec.clear (svAssumptions solver)
    solve_ solver
  
  -- | Solve constraints under assuptions.
  -- Returns 'True' if the problem is SATISFIABLE.
  -- Returns 'False' if the problem is UNSATISFIABLE.
  solveWith :: Solver
            -> [Lit]    -- ^ Assumptions
            -> IO Bool
  solveWith solver ls = do
    Vec.clear (svAssumptions solver)
    mapM_ (Vec.push (svAssumptions solver)) ls
    solve_ solver
  
  solve_ :: Solver -> IO Bool
  solve_ solver = do
    config <- getConfig solver
    writeIORef (svAssumptionsImplications solver) IS.empty
  
    log solver "Solving starts ..."
    resetStat solver
    writeIORef (svCanceled solver) False
    writeIORef (svModel solver) Nothing
    writeIORef (svFailedAssumptions solver) IS.empty
  
    ok <- readIORef (svOk solver)
    if not ok then
      return False
    else do
      when debugMode $ dumpVarActivity solver
      d <- getDecisionLevel solver
      assert (d == levelRoot) $ return ()
  
      nv <- getNVars solver
      Vec.resizeCapacity (svTrail solver) nv
  
      unless (configRestartInc config > 1) $ error "RestartInc must be >1"
      let restartSeq =
            if configRestartFirst config  > 0
            then mkRestartSeq (configRestartStrategy config) (configRestartFirst config) (configRestartInc config)
            else repeat 0
  
      let learntSizeAdj = do
            (size,adj) <- shift (svLearntLimSeq solver)
            writeIORef (svLearntLim solver) size
            writeIORef (svLearntLimAdjCnt solver) adj
          onConflict = do
            cnt <- readIORef (svLearntLimAdjCnt solver)
            if (cnt==0)
            then learntSizeAdj
            else writeIORef (svLearntLimAdjCnt solver) $! cnt-1
  
      cnt <- readIORef (svLearntLimAdjCnt solver)
      when (cnt == -1) $ do
        unless (configLearntSizeInc config > 1) $ error "LearntSizeInc must be >1"
        nc <- getNConstraints solver
        let initialLearntLim = if configLearntSizeFirst config > 0 then configLearntSizeFirst config else max ((nc + nv) `div` 3) 16
            learntSizeSeq    = iterate (ceiling . (configLearntSizeInc config *) . fromIntegral) initialLearntLim
            learntSizeAdjSeq = iterate (\x -> (x * 3) `div` 2) (100::Int)
        writeIORef (svLearntLimSeq solver) (zip learntSizeSeq learntSizeAdjSeq)
        learntSizeAdj
  
      unless (0 <= configERWAStepSizeFirst config && configERWAStepSizeFirst config <= 1) $
        error "ERWAStepSizeFirst must be in [0..1]"
      unless (0 <= configERWAStepSizeMin config && configERWAStepSizeFirst config <= 1) $
        error "ERWAStepSizeMin must be in [0..1]"
      unless (0 <= configERWAStepSizeDec config) $
        error "ERWAStepSizeDec must be >=0"
      writeIOURef (svERWAStepSize solver) (configERWAStepSizeFirst config)
  
      let loop [] = error "solve_: should not happen"
          loop (conflict_lim:rs) = do
            printStat solver True
            ret <- search solver conflict_lim onConflict
            case ret of
              SRFinished x -> return $ Right x
              SRBudgetExceeded -> return $ Left (throw BudgetExceeded)
              SRCanceled -> return $ Left (throw Canceled)
              SRRestart -> do
                modifyIOURef (svNRestart solver) (+1)
                backtrackTo solver levelRoot
                loop rs
  
      printStatHeader solver
  
      startCPU <- getTime ProcessCPUTime
      startWC  <- getTime Monotonic
      writeIORef (svStartWC solver) startWC
      result <- loop restartSeq
      endCPU <- getTime ProcessCPUTime
      endWC  <- getTime Monotonic
  
      case result of
        Right True -> do
          when (configCheckModel config) $ checkSatisfied solver
          constructModel solver
          mt <- getTheory solver
          case mt of
            Nothing -> return ()
            Just t -> thConstructModel t
        _ -> return ()
      case result of
        Right False -> return ()
        _ -> saveAssumptionsImplications solver
  
      backtrackTo solver levelRoot
  
      when debugMode $ dumpVarActivity solver
      when debugMode $ dumpConstrActivity solver
      printStat solver True
      let durationSecs :: TimeSpec -> TimeSpec -> Double
          durationSecs start end = fromIntegral (toNanoSecs (end `diffTimeSpec` start)) / 10^(9::Int)
      (log solver . printf "#cpu_time = %.3fs") (durationSecs startCPU endCPU)
      (log solver . printf "#wall_clock_time = %.3fs") (durationSecs startWC endWC)
      (log solver . printf "#decision = %d") =<< readIOURef (svNDecision solver)
      (log solver . printf "#random_decision = %d") =<< readIOURef (svNRandomDecision solver)
      (log solver . printf "#conflict = %d") =<< readIOURef (svNConflict solver)
      (log solver . printf "#restart = %d")  =<< readIOURef (svNRestart solver)
  
      case result of
        Right x  -> return x
        Left m -> m
  
  data BudgetExceeded = BudgetExceeded
    deriving (Show, Typeable)
  
  instance Exception BudgetExceeded
  
  data Canceled = Canceled
    deriving (Show, Typeable)
  
  instance Exception Canceled
  
  data SearchResult
    = SRFinished Bool
    | SRRestart
    | SRBudgetExceeded
    | SRCanceled
  
  search :: Solver -> Int -> IO () -> IO SearchResult
  search solver !conflict_lim onConflict = do
    conflictCounter <- newIORef 0
    let
      loop :: IO SearchResult
      loop = do
        conflict <- deduce solver
        case conflict of
          Just constr -> do
            ret <- handleConflict conflictCounter constr
            case ret of
              Just sr -> return sr
              Nothing -> loop
          Nothing -> do
            lv <- getDecisionLevel solver
            when (lv == levelRoot) $ simplify solver
            checkGC
            r <- pickAssumption
            case r of
              Nothing -> return (SRFinished False)
              Just lit
                | lit /= litUndef -> decide solver lit >> loop
                | otherwise -> do
                    lit2 <- pickBranchLit solver
                    if lit2 == litUndef
                      then return (SRFinished True)
                      else decide solver lit2 >> loop
    loop
  
    where
      checkGC :: IO ()
      checkGC = do
        n <- getNLearntConstraints solver
        m <- getNAssigned solver
        learnt_lim <- readIORef (svLearntLim solver)
        when (learnt_lim >= 0 && n - m > learnt_lim) $ do
          modifyIOURef (svNLearntGC solver) (+1)
          reduceDB solver
  
      pickAssumption :: IO (Maybe Lit)
      pickAssumption = do
        s <- Vec.getSize (svAssumptions solver)
        let go = do
                d <- getDecisionLevel solver
                if not (d < s) then
                  return (Just litUndef)
                else do
                  l <- Vec.unsafeRead (svAssumptions solver) d
                  val <- litValue solver l
                  if val == lTrue then do
                    -- dummy decision level
                    pushDecisionLevel solver
                    go
                  else if val == lFalse then do
                    -- conflict with assumption
                    core <- analyzeFinal solver l
                    writeIORef (svFailedAssumptions solver) (IS.fromList core)
                    return Nothing
                  else
                    return (Just l)
        go
  
      handleConflict :: IORef Int -> SomeConstraintHandler -> IO (Maybe SearchResult)
      handleConflict conflictCounter constr = do
        varEMADecay solver
        varDecayActivity solver
        constrDecayActivity solver
        onConflict
  
        modifyIOURef (svNConflict solver) (+1)
        d <- getDecisionLevel solver
  
        when debugMode $ logIO solver $ do
          str <- showConstraintHandler constr
          return $ printf "conflict(level=%d): %s" d str
  
        modifyIORef' conflictCounter (+1)
        c <- readIORef conflictCounter
  
        modifyIOURef (svConfBudget solver) $ \confBudget ->
          if confBudget > 0 then confBudget - 1 else confBudget
        confBudget <- readIOURef (svConfBudget solver)
  
        terminateCallback' <- readIORef (svTerminateCallback solver)
        case terminateCallback' of
          Nothing -> return ()
          Just terminateCallback -> do
            ret <- terminateCallback
            when ret $ writeIORef (svCanceled solver) True
        canceled <- readIORef (svCanceled solver)
  
        when (c `mod` 100 == 0) $ do
          printStat solver False
  
        if d == levelRoot then do
          callLearnCallback solver []
          markBad solver
          return $ Just (SRFinished False)
        else if confBudget==0 then
          return $ Just SRBudgetExceeded
        else if canceled then
          return $ Just SRCanceled
        else if conflict_lim > 0 && c >= conflict_lim then
          return $ Just SRRestart
        else do
          modifyIOURef (svLearntCounter solver) (+1)
          config <- getConfig solver
          case configLearningStrategy config of
            LearningClause -> learnClause constr >> return Nothing
            LearningHybrid -> learnHybrid conflictCounter constr
  
      learnClause :: SomeConstraintHandler -> IO ()
      learnClause constr = do
        (learntClause, level) <- analyzeConflict solver constr
        backtrackTo solver level
        case learntClause of
          [] -> error "search(LearningClause): should not happen"
          [lit] -> do
            ret <- assign solver lit
            assert ret $ return ()
            return ()
          lit:_ -> do
            cl <- newClauseHandler learntClause True
            let constr2 = toConstraintHandler cl
            addToLearntDB solver constr2
            basicAttachClauseHandler solver cl
            assignBy solver lit constr2
            constrBumpActivity solver constr2
  
      learnHybrid :: IORef Int -> SomeConstraintHandler -> IO (Maybe SearchResult)
      learnHybrid conflictCounter constr = do
        (learntClause, clauseLevel) <- analyzeConflict solver constr
        (pb, minLevel) <- do
          z <- readIORef (svPBLearnt solver)
          case z of
            Nothing -> return (z, clauseLevel)
            Just pb -> do
              pbLevel <- pbBacktrackLevel solver pb
              return (z, min clauseLevel pbLevel)
        backtrackTo solver minLevel
  
        case learntClause of
          [] -> error "search(LearningHybrid): should not happen"
          [lit] -> do
            _ <- assign solver lit -- This should always succeed.
            return ()
          lit:_ -> do
            cl <- newClauseHandler learntClause True
            let constr2 = toConstraintHandler cl
            addToLearntDB solver constr2
            basicAttachClauseHandler solver cl
            constrBumpActivity solver constr2
            when (minLevel == clauseLevel) $ do
              _ <- assignBy solver lit constr2 -- This should always succeed.
              return ()
  
        ret <- deduce solver
        case ret of
          Just conflicted -> do
            handleConflict conflictCounter conflicted
            -- TODO: should also learn the PB constraint?
          Nothing -> do
            case pb of
              Nothing -> return Nothing
              Just (lhs,rhs) -> do
                h <- newPBHandlerPromoted solver lhs rhs True
                case h of
                  CHClause _ -> do
                    {- We don't want to add additional clause,
                       since it would be subsumed by already added one. -}
                    return Nothing
                  _ -> do
                    addToLearntDB solver h
                    ret2 <- attach solver h
                    constrBumpActivity solver h
                    if ret2 then
                      return Nothing
                    else
                      handleConflict conflictCounter h
  
  -- | Cancel exectution of 'solve' or 'solveWith'.
  --
  -- This can be called from other threads.
  cancel :: Solver -> IO ()
  cancel solver = writeIORef (svCanceled solver) True
  
  -- | After 'solve' returns True, it returns an satisfying assignment.
  getModel :: Solver -> IO Model
  getModel solver = do
    m <- readIORef (svModel solver)
    return (fromJust m)
  
  -- | After 'solveWith' returns False, it returns a set of assumptions
  -- that leads to contradiction. In particular, if it returns an empty
  -- set, the problem is unsatisiable without any assumptions.
  getFailedAssumptions :: Solver -> IO LitSet
  getFailedAssumptions solver = readIORef (svFailedAssumptions solver)
  
  -- | __EXPERIMENTAL API__: After 'solveWith' returns True or failed with 'BudgetExceeded' exception,
  -- it returns a set of literals that are implied by assumptions.
  getAssumptionsImplications :: Solver -> IO LitSet
  getAssumptionsImplications solver = readIORef (svAssumptionsImplications solver)
  
  {--------------------------------------------------------------------
    Simplification
  --------------------------------------------------------------------}
  
  -- | Simplify the constraint database according to the current top-level assigment.
  simplify :: Solver -> IO ()
  simplify solver = do
    let loop [] rs !n     = return (rs,n)
        loop (y:ys) rs !n = do
          b1 <- isSatisfied solver y
          b2 <- isLocked solver y
          if b1 && not b2 then do
            detach solver y
            loop ys rs (n+1)
          else loop ys (y:rs) n
  
    -- simplify original constraint DB
    do
      xs <- readIORef (svConstrDB solver)
      (ys,n) <- loop xs [] (0::Int)
      modifyIOURef (svNRemovedConstr solver) (+n)
      writeIORef (svConstrDB solver) ys
  
    -- simplify learnt constraint DB
    do
      (m,xs) <- readIORef (svLearntDB solver)
      (ys,n) <- loop xs [] (0::Int)
      writeIORef (svLearntDB solver) (m-n, ys)
  
  {-
  References:
  L. Zhang, "On subsumption removal and On-the-Fly CNF simplification,"
  Theory and Applications of Satisfiability Testing (2005), pp. 482-489.
  -}
  
  checkForwardSubsumption :: Solver -> Clause -> IO Bool
  checkForwardSubsumption solver lits = do
    flag <- configEnableForwardSubsumptionRemoval <$> getConfig solver
    if not flag then
      return False
    else do
      withEnablePhaseSaving False $ do
        bracket_
          (pushDecisionLevel solver)
          (backtrackTo solver levelRoot) $ do
            b <- allM (\lit -> assign solver (litNot lit)) lits
            if b then
              liftM isJust (deduce solver)
            else do
              when debugMode $ log solver ("forward subsumption: " ++ show lits)
              return True
    where
      withEnablePhaseSaving flag m =
        bracket
          (getConfig solver)
          (\saved -> modifyConfig solver (\config -> config{ configEnablePhaseSaving = configEnablePhaseSaving saved }))
          (\saved -> setConfig solver saved{ configEnablePhaseSaving = flag } >> m)
  
  removeBackwardSubsumedBy :: Solver -> PBLinAtLeast -> IO ()
  removeBackwardSubsumedBy solver pb = do
    flag <- configEnableBackwardSubsumptionRemoval <$> getConfig solver
    when flag $ do
      xs <- backwardSubsumedBy solver pb
      when debugMode $ do
        forM_ (HashSet.toList xs) $ \c -> do
          s <- showConstraintHandler c
          log solver (printf "backward subsumption: %s is subsumed by %s\n" s (show pb))
      removeConstraintHandlers solver xs
  
  backwardSubsumedBy :: Solver -> PBLinAtLeast -> IO (HashSet SomeConstraintHandler)
  backwardSubsumedBy solver pb@(lhs,_) = do
    xs <- forM lhs $ \(_,lit) -> do
      Vec.unsafeRead (svLitOccurList solver) (litIndex lit)
    case xs of
      [] -> return HashSet.empty
      s:ss -> do
        let p c = do
              -- Note that @isPBRepresentable c@ is always True here,
              -- because only such constraints are added to occur list.
              -- See 'addToDB'.
              pb2 <- instantiatePBLinAtLeast (getLitFixed solver) =<< toPBLinAtLeast c
              return $ pbLinSubsume pb pb2
        liftM HashSet.fromList
          $ filterM p
          $ HashSet.toList
          $ foldl' HashSet.intersection s ss
  
  removeConstraintHandlers :: Solver -> HashSet SomeConstraintHandler -> IO ()
  removeConstraintHandlers _ zs | HashSet.null zs = return ()
  removeConstraintHandlers solver zs = do
    let loop [] rs !n     = return (rs,n)
        loop (c:cs) rs !n = do
          if c `HashSet.member` zs then do
            detach solver c
            loop cs rs (n+1)
          else loop cs (c:rs) n
    xs <- readIORef (svConstrDB solver)
    (ys,n) <- loop xs [] (0::Int)
    modifyIOURef (svNRemovedConstr solver) (+n)
    writeIORef (svConstrDB solver) ys
  
  {--------------------------------------------------------------------
    Parameter settings.
  --------------------------------------------------------------------}
  
  {--------------------------------------------------------------------
    Configulation
  --------------------------------------------------------------------}
  
  getConfig :: Solver -> IO Config
  getConfig solver = readIORef $ svConfig solver
  
  setConfig :: Solver -> Config -> IO ()
  setConfig solver conf = do
    orig <- getConfig solver
    writeIORef (svConfig solver) conf
    when (configBranchingStrategy orig /= configBranchingStrategy conf) $ do
      PQ.rebuild (svVarQueue solver)
  
  modifyConfig :: Solver -> (Config -> Config) -> IO ()
  modifyConfig solver f = do
    config <- getConfig solver
    setConfig solver $ f config
  
  -- | The default polarity of a variable.
  setVarPolarity :: Solver -> Var -> Bool -> IO ()
  setVarPolarity solver v val = Vec.unsafeWrite (svVarPolarity solver) (v - 1) val
  
  -- | Set random generator used by the random variable selection
  setRandomGen :: Solver -> Rand.GenIO -> IO ()
  setRandomGen solver = writeIORef (svRandomGen solver)
  
  -- | Get random generator used by the random variable selection
  getRandomGen :: Solver -> IO Rand.GenIO
  getRandomGen solver = readIORef (svRandomGen solver)
  
  setConfBudget :: Solver -> Maybe Int -> IO ()
  setConfBudget solver (Just b) | b >= 0 = writeIOURef (svConfBudget solver) b
  setConfBudget solver _ = writeIOURef (svConfBudget solver) (-1)
  
  -- | Set a callback function used to indicate a termination requirement to the solver.
  --
  -- The solver will periodically call this function and check its return value during
  -- the search. If the callback function returns `True` the solver terminates and throws
  -- 'Canceled' exception.
  --
  -- See also 'clearTerminateCallback' and
  -- [IPASIR](https://github.com/biotomas/ipasir)'s @ipasir_set_terminate()@ function.
  setTerminateCallback :: Solver -> IO Bool -> IO ()
  setTerminateCallback solver callback = writeIORef (svTerminateCallback solver) (Just callback)
  
  -- | Clear a callback function set by `setTerminateCallback`
  clearTerminateCallback :: Solver -> IO ()
  clearTerminateCallback solver = writeIORef (svTerminateCallback solver) Nothing
  
  -- | Set a callback function used to extract learned clauses from the solver.
  -- The solver will call this function for each learned clause.
  --
  -- See also 'clearLearnCallback' and
  -- [IPASIR](https://github.com/biotomas/ipasir)'s @ipasir_set_learn()@ function.
  setLearnCallback :: Solver -> (Clause -> IO ()) -> IO ()
  setLearnCallback solver callback = writeIORef (svLearnCallback solver) (Just callback)
  
  -- | Clear a callback function set by `setLearnCallback`
  clearLearnCallback :: Solver -> IO ()
  clearLearnCallback solver = writeIORef (svLearnCallback solver) Nothing
  
  {--------------------------------------------------------------------
    API for implementation of @solve@
  --------------------------------------------------------------------}
  
  pickBranchLit :: Solver -> IO Lit
  pickBranchLit !solver = do
    gen <- readIORef (svRandomGen solver)
    let vqueue = svVarQueue solver
    !randfreq <- configRandomFreq <$> getConfig solver
    !size <- PQ.queueSize vqueue
    -- System.Random.random produces [0,1), but System.Random.MWC.uniform produces (0,1]
    !r <- liftM (1 -) $ Rand.uniform gen
    var <-
      if (r < randfreq && size >= 2) then do
        a <- PQ.getHeapArray vqueue
        i <- Rand.uniformR (0, size-1) gen
        var <- readArray a i
        val <- varValue solver var
        if val == lUndef then do
          modifyIOURef (svNRandomDecision solver) (1+)
          return var
        else return litUndef
      else
        return litUndef
  
    -- Activity based decision
    let loop :: IO Var
        loop = do
          m <- PQ.dequeue vqueue
          case m of
            Nothing -> return litUndef
            Just var2 -> do
              val2 <- varValue solver var2
              if val2 /= lUndef
                then loop
                else return var2
    var2 <-
      if var==litUndef
      then loop
      else return var
  
    if var2==litUndef then
      return litUndef
    else do
      -- TODO: random polarity
      p <- Vec.unsafeRead (svVarPolarity solver) (var2 - 1)
      return $! literal var2 p
  
  decide :: Solver -> Lit -> IO ()
  decide solver !lit = do
    modifyIOURef (svNDecision solver) (+1)
    pushDecisionLevel solver
    when debugMode $ do
      val <- litValue solver lit
      when (val /= lUndef) $ error "decide: should not happen"
    assign solver lit
    return ()
  
  deduce :: Solver -> IO (Maybe SomeConstraintHandler)
  deduce solver = liftM (either Just (const Nothing)) $ runExceptT $ do
    let loop = do
          deduceB solver
          deduceT solver
          empty <- liftIO $ bcpIsEmpty solver
          unless empty $ loop
    loop
  
  deduceB :: Solver -> ExceptT SomeConstraintHandler IO ()
  deduceB solver = loop
    where
      loop :: ExceptT SomeConstraintHandler IO ()
      loop = do
        r <- liftIO $ bcpDequeue solver
        case r of
          Nothing -> return ()
          Just lit -> do
            processLit lit
            processVar lit
            loop
  
      processLit :: Lit -> ExceptT SomeConstraintHandler IO ()
      processLit !lit = ExceptT $ liftM (maybe (Right ()) Left) $ do
        let falsifiedLit = litNot lit
            a = svLitWatches solver
            idx = litIndex falsifiedLit
        let loop2 [] = return Nothing
            loop2 (w:ws) = do
              ok <- propagate solver w falsifiedLit
              if ok then
                loop2 ws
              else do
                Vec.unsafeModify a idx (++ws)
                return (Just w)
        ws <- Vec.unsafeRead a idx
        Vec.unsafeWrite a idx []
        loop2 ws
  
      processVar :: Lit -> ExceptT SomeConstraintHandler IO ()
      processVar !lit = ExceptT $ liftM (maybe (Right ()) Left) $ do
        let falsifiedLit = litNot lit
            idx = litVar lit - 1
        let loop2 [] = return Nothing
            loop2 (w:ws) = do
              ok <- propagate solver w falsifiedLit
              if ok
                then loop2 ws
                else do
                  Vec.unsafeModify (svVarWatches solver) idx (++ws)
                  return (Just w)
        ws <- Vec.unsafeRead (svVarWatches solver) idx
        Vec.unsafeWrite (svVarWatches solver) idx []
        loop2 ws
  
  analyzeConflict :: ConstraintHandler c => Solver -> c -> IO (Clause, Level)
  analyzeConflict solver constr = do
    config <- getConfig solver
    let isHybrid = configLearningStrategy config == LearningHybrid
  
    d <- getDecisionLevel solver
    (out :: Vec.UVec Lit) <- Vec.new
    Vec.push out 0 -- (leave room for the asserting literal)
    (pathC :: IOURef Int) <- newIOURef 0
  
    pbConstrRef <- newIORef undefined
  
    let f lits = do
          forM_ lits $ \lit -> do
            let !v = litVar lit
            lv <- litLevel solver lit
            b <- Vec.unsafeRead (svSeen solver) (v - 1)
            when (not b && lv > levelRoot) $ do
              varBumpActivity solver v
              varIncrementParticipated solver v
              if lv >= d then do
                Vec.unsafeWrite (svSeen solver) (v - 1) True
                modifyIOURef pathC (+1)
              else do
                Vec.push out lit
  
        processLitHybrid pb constr2 lit getLits = do
          pb2 <- do
            let clausePB = do
                  lits <- getLits
                  return $ clauseToPBLinAtLeast (lit : lits)
            b <- isPBRepresentable constr2
            if not b then do
              clausePB
            else do
              pb2 <- toPBLinAtLeast constr2
              o <- pbOverSAT solver pb2
              if o then do
                clausePB
              else
                return pb2
          let pb3 = cutResolve pb pb2 (litVar lit)
              ls = IS.fromList [l | (_,l) <- fst pb3]
          seq ls $ writeIORef pbConstrRef (ls, pb3)
  
        popUnseen = do
          l <- peekTrail solver
          let !v = litVar l
          b <- Vec.unsafeRead (svSeen solver) (v - 1)
          if b then do
            return ()
          else do
            when isHybrid $ do
              (ls, pb) <- readIORef pbConstrRef
              when (litNot l `IS.member` ls) $ do
                Just constr2 <- varReason solver v
                processLitHybrid pb constr2 l (reasonOf solver constr2 (Just l))
            popTrail solver
            popUnseen
  
        loop = do
          popUnseen
          l <- peekTrail solver
          let !v = litVar l
          Vec.unsafeWrite (svSeen solver) (v - 1) False
          modifyIOURef pathC (subtract 1)
          c <- readIOURef pathC
          if c > 0 then do
            Just constr2 <- varReason solver v
            constrBumpActivity solver constr2
            lits <- reasonOf solver constr2 (Just l)
            f lits
            when isHybrid $ do
              (ls, pb) <- readIORef pbConstrRef
              when (litNot l `IS.member` ls) $ do
                processLitHybrid pb constr2 l (return lits)
            popTrail solver
            loop
          else do
            Vec.unsafeWrite out 0 (litNot l)
  
    constrBumpActivity solver constr
    falsifiedLits <- reasonOf solver constr Nothing
    f falsifiedLits
    when isHybrid $ do
       pb <- do
         b <- isPBRepresentable constr
         if b then
           toPBLinAtLeast constr
         else
           return (clauseToPBLinAtLeast falsifiedLits)
       let ls = IS.fromList [l | (_,l) <- fst pb]
       seq ls $ writeIORef pbConstrRef (ls, pb)
    loop
    lits <- liftM IS.fromList $ Vec.getElems out
  
    lits2 <- minimizeConflictClause solver lits
  
    incrementReasoned solver (IS.toList lits2)
  
    xs <- liftM (sortBy (comparing (Down . snd))) $
      forM (IS.toList lits2) $ \l -> do
        lv <- litLevel solver l
        return (l,lv)
  
    when isHybrid $ do
      (_, pb) <- readIORef pbConstrRef
      case pbToClause pb of
        Just _ -> writeIORef (svPBLearnt solver) Nothing
        Nothing -> writeIORef (svPBLearnt solver) (Just pb)
  
    let level = case xs of
                  [] -> error "analyzeConflict: should not happen"
                  [_] -> levelRoot
                  _:(_,lv):_ -> lv
        clause = map fst xs
    callLearnCallback solver clause
    return (clause, level)
  
  -- { p } ∪ { pにfalseを割り当てる原因のassumption }
  analyzeFinal :: Solver -> Lit -> IO [Lit]
  analyzeFinal solver p = do
    let go :: Int -> VarSet -> [Lit] -> IO [Lit]
        go i seen result
          | i < 0 = return result
          | otherwise = do
              l <- Vec.unsafeRead (svTrail solver) i
              lv <- litLevel solver l
              if lv == levelRoot then
                return result
              else if litVar l `IS.member` seen then do
                r <- varReason solver (litVar l)
                case r of
                  Nothing -> do
                    let seen' = IS.delete (litVar l) seen
                    go (i-1) seen' (l : result)
                  Just constr  -> do
                    c <- reasonOf solver constr (Just l)
                    let seen' = IS.delete (litVar l) seen `IS.union` IS.fromList [litVar l2 | l2 <- c]
                    go (i-1) seen' result
              else
                go (i-1) seen result
    n <- Vec.getSize (svTrail solver)
    go (n-1) (IS.singleton (litVar p)) [p]
  
  callLearnCallback :: Solver -> Clause -> IO ()
  callLearnCallback solver clause = do
    cb <- readIORef (svLearnCallback solver)
    case cb of
      Nothing -> return ()
      Just callback -> callback clause
  
  pbBacktrackLevel :: Solver -> PBLinAtLeast -> IO Level
  pbBacktrackLevel _ ([], rhs) = assert (rhs > 0) $ return levelRoot
  pbBacktrackLevel solver (lhs, rhs) = do
    levelToLiterals <- liftM (IM.unionsWith IM.union) $ forM lhs $ \(c,lit) -> do
      val <- litValue solver lit
      if val /= lUndef then do
        level <- litLevel solver lit
        return $ IM.singleton level (IM.singleton lit (c,val))
      else
        return $ IM.singleton maxBound (IM.singleton lit (c,val))
  
    let replay [] !_ = error "pbBacktrackLevel: should not happen"
        replay ((lv,lv_lits) : lvs) !slack = do
          let slack_lv = slack - sum [c | (_,(c,val)) <- IM.toList lv_lits, val == lFalse]
          if slack_lv < 0 then
            return lv -- CONFLICT
          else if any (\(_, lits2) -> any (\(c,_) -> c > slack_lv) (IM.elems lits2)) lvs then
            return lv -- UNIT
          else
            replay lvs slack_lv
  
    let initial_slack = sum [c | (c,_) <- lhs] - rhs
    if any (\(c,_) -> c > initial_slack) lhs then
      return 0
    else do
      replay (IM.toList levelToLiterals) initial_slack
  
  minimizeConflictClause :: Solver -> LitSet -> IO LitSet
  minimizeConflictClause solver lits = do
    ccmin <- configCCMin <$> getConfig solver
    if ccmin >= 2 then
      minimizeConflictClauseRecursive solver lits
    else if ccmin >= 1 then
      minimizeConflictClauseLocal solver lits
    else
      return lits
  
  minimizeConflictClauseLocal :: Solver -> LitSet -> IO LitSet
  minimizeConflictClauseLocal solver lits = do
    let xs = IS.toAscList lits
    ys <- filterM (liftM not . isRedundant) xs
    when debugMode $ do
      log solver "minimizeConflictClauseLocal:"
      log solver $ show xs
      log solver $ show ys
    return $ IS.fromAscList $ ys
  
    where
      isRedundant :: Lit -> IO Bool
      isRedundant lit = do
        c <- varReason solver (litVar lit)
        case c of
          Nothing -> return False
          Just c2 -> do
            ls <- reasonOf solver c2 (Just (litNot lit))
            allM test ls
  
      test :: Lit -> IO Bool
      test lit = do
        lv <- litLevel solver lit
        return $ lv == levelRoot || lit `IS.member` lits
  
  minimizeConflictClauseRecursive :: Solver -> LitSet -> IO LitSet
  minimizeConflictClauseRecursive solver lits = do
    let
      isRedundant :: Lit -> IO Bool
      isRedundant lit = do
        c <- varReason solver (litVar lit)
        case c of
          Nothing -> return False
          Just c2 -> do
            ls <- reasonOf solver c2 (Just (litNot lit))
            go ls IS.empty
  
      go :: [Lit] -> IS.IntSet -> IO Bool
      go [] _ = return True
      go (lit : ls) seen = do
        lv <- litLevel solver lit
        if lv == levelRoot || lit `IS.member` lits || lit `IS.member` seen then
          go ls seen
        else do
          c <- varReason solver (litVar lit)
          case c of
            Nothing -> return False
            Just c2 -> do
              ls2 <- reasonOf solver c2 (Just (litNot lit))
              go (ls2 ++ ls) (IS.insert lit seen)
  
    let xs = IS.toAscList lits
    ys <- filterM (liftM not . isRedundant) xs
    when debugMode $ do
      log solver "minimizeConflictClauseRecursive:"
      log solver $ show xs
      log solver $ show ys
    return $ IS.fromAscList $ ys
  
  incrementReasoned :: Solver -> Clause -> IO ()
  incrementReasoned solver ls = do
    let f reasonSided l = do
          m <- varReason solver (litVar l)
          case m of
            Nothing -> return reasonSided
            Just constr -> do
              v <- litValue solver l
              unless (v == lFalse) undefined
              xs <- constrReasonOf solver constr (Just (litNot l))
              return $ reasonSided `IS.union` IS.fromList (map litVar xs)
    reasonSided <- foldM f IS.empty ls
    mapM_ (varIncrementReasoned solver) (IS.toList reasonSided)
  
  peekTrail :: Solver -> IO Lit
  peekTrail solver = do
    n <- Vec.getSize (svTrail solver)
    Vec.unsafeRead (svTrail solver) (n-1)
  
  popTrail :: Solver -> IO Lit
  popTrail solver = do
    l <- Vec.unsafePop (svTrail solver)
    unassign solver (litVar l)
    return l
  
  getDecisionLevel ::Solver -> IO Int
  getDecisionLevel solver = Vec.getSize (svTrailLimit solver)
  
  pushDecisionLevel :: Solver -> IO ()
  pushDecisionLevel solver = do
    Vec.push (svTrailLimit solver) =<< Vec.getSize (svTrail solver)
    mt <- getTheory solver
    case mt of
      Nothing -> return ()
      Just t -> thPushBacktrackPoint t
  
  popDecisionLevel :: Solver -> IO ()
  popDecisionLevel solver = do
    n <- Vec.unsafePop (svTrailLimit solver)
    let loop = do
          m <- Vec.getSize (svTrail solver)
          when (m > n) $ do
            popTrail solver
            loop
    loop
    mt <- getTheory solver
    case mt of
      Nothing -> return ()
      Just t -> thPopBacktrackPoint t
  
  -- | Revert to the state at given level
  -- (keeping all assignment at @level@ but not beyond).
  backtrackTo :: Solver -> Int -> IO ()
  backtrackTo solver level = do
    when debugMode $ log solver $ printf "backtrackTo: %d" level
    loop
    bcpClear solver
    mt <- getTheory solver
    case mt of
      Nothing -> return ()
      Just _ -> do
        n <- Vec.getSize (svTrail solver)
        writeIOURef (svTheoryChecked solver) n
    where
      loop :: IO ()
      loop = do
        lv <- getDecisionLevel solver
        when (lv > level) $ do
          popDecisionLevel solver
          loop
  
  constructModel :: Solver -> IO ()
  constructModel solver = do
    n <- getNVars solver
    (marr::IOUArray Var Bool) <- newArray_ (1,n)
    forLoop 1 (<=n) (+1) $ \v -> do
      val <- varValue solver v
      writeArray marr v (fromJust (unliftBool val))
    m <- unsafeFreeze marr
    writeIORef (svModel solver) (Just m)
  
  saveAssumptionsImplications :: Solver -> IO ()
  saveAssumptionsImplications solver = do
    n <- Vec.getSize (svAssumptions solver)
    lv <- getDecisionLevel solver
  
    lim_beg <-
      if lv == 0 then
        return 0
      else
        Vec.read (svTrailLimit solver) 0
    lim_end <-
      if lv > n then
         Vec.read (svTrailLimit solver) n
      else
         Vec.getSize (svTrail solver)
  
    let ref = svAssumptionsImplications solver
    forM_ [lim_beg .. lim_end-1] $ \i -> do
      lit <- Vec.read (svTrail solver) i
      modifyIORef' ref (IS.insert lit)
    forM_ [0..n-1] $ \i -> do
      lit <- Vec.read (svAssumptions solver) i
      modifyIORef' ref (IS.delete lit)
  
  constrDecayActivity :: Solver -> IO ()
  constrDecayActivity solver = do
    d <- configConstrDecay <$> getConfig solver
    modifyIOURef (svConstrInc solver) (d*)
  
  constrBumpActivity :: ConstraintHandler a => Solver -> a -> IO ()
  constrBumpActivity solver this = do
    aval <- constrReadActivity this
    when (aval >= 0) $ do -- learnt clause
      inc <- readIOURef (svConstrInc solver)
      let aval2 = aval+inc
      constrWriteActivity this $! aval2
      when (aval2 > 1e20) $
        -- Rescale
        constrRescaleAllActivity solver
  
  constrRescaleAllActivity :: Solver -> IO ()
  constrRescaleAllActivity solver = do
    xs <- learntConstraints solver
    forM_ xs $ \c -> do
      aval <- constrReadActivity c
      when (aval >= 0) $
        constrWriteActivity c $! (aval * 1e-20)
    modifyIOURef (svConstrInc solver) (* 1e-20)
  
  resetStat :: Solver -> IO ()
  resetStat solver = do
    writeIOURef (svNDecision solver) 0
    writeIOURef (svNRandomDecision solver) 0
    writeIOURef (svNConflict solver) 0
    writeIOURef (svNRestart solver) 0
    writeIOURef (svNLearntGC solver) 0
  
  printStatHeader :: Solver -> IO ()
  printStatHeader solver = do
    log solver $ "============================[ Search Statistics ]============================"
    log solver $ " Time | Restart | Decision | Conflict |      LEARNT     | Fixed    | Removed "
    log solver $ "      |         |          |          |    Limit     GC | Var      | Constra "
    log solver $ "============================================================================="
  
  printStat :: Solver -> Bool -> IO ()
  printStat solver force = do
    nowWC <- getTime Monotonic
    b <- if force
         then return True
         else do
           lastWC <- readIORef (svLastStatWC solver)
           return $ sec (nowWC `diffTimeSpec` lastWC) > 1
    when b $ do
      startWC   <- readIORef (svStartWC solver)
      let tm = showTimeDiff $ nowWC `diffTimeSpec` startWC
      restart   <- readIOURef (svNRestart solver)
      dec       <- readIOURef (svNDecision solver)
      conflict  <- readIOURef (svNConflict solver)
      learntLim <- readIORef (svLearntLim solver)
      learntGC  <- readIOURef (svNLearntGC solver)
      fixed     <- getNFixed solver
      removed   <- readIOURef (svNRemovedConstr solver)
      log solver $ printf "%s | %7d | %8d | %8d | %8d %6d | %8d | %8d"
        tm restart dec conflict learntLim learntGC fixed removed
      writeIORef (svLastStatWC solver) nowWC
  
  showTimeDiff :: TimeSpec -> String
  showTimeDiff t
    | si <  100  = printf "%4.1fs" (fromRational s :: Double)
    | si <= 9999 = printf "%4ds" si
    | mi <  100  = printf "%4.1fm" (fromRational m :: Double)
    | mi <= 9999 = printf "%4dm" mi
    | hi <  100  = printf "%4.1fs" (fromRational h :: Double)
    | otherwise  = printf "%4dh" hi
    where
      s :: Rational
      s = fromIntegral (toNanoSecs t) / 10^(9::Int)
  
      si :: Integer
      si = fromIntegral (sec t)
  
      m :: Rational
      m = s / 60
  
      mi :: Integer
      mi = round m
  
      h :: Rational
      h = m / 60
  
      hi :: Integer
      hi = round h
  
  {--------------------------------------------------------------------
    constraint implementation
  --------------------------------------------------------------------}
  
  class (Eq a, Hashable a) => ConstraintHandler a where
    toConstraintHandler :: a -> SomeConstraintHandler
  
    showConstraintHandler :: a -> IO String
  
    constrAttach :: Solver -> SomeConstraintHandler -> a -> IO Bool
  
    constrDetach :: Solver -> SomeConstraintHandler -> a -> IO ()
  
    constrIsLocked :: Solver -> SomeConstraintHandler -> a -> IO Bool
  
    -- | invoked with the watched literal when the literal is falsified.
    -- 'watch' で 'toConstraint' を呼び出して heap allocation が発生するのを
    -- 避けるために、元の 'SomeConstraintHandler' も渡しておく。
    constrPropagate :: Solver -> SomeConstraintHandler -> a -> Lit -> IO Bool
  
    -- | deduce a clause C∨l from the constraint and return C.
    -- C and l should be false and true respectively under the current
    -- assignment.
    constrReasonOf :: Solver -> a -> Maybe Lit -> IO Clause
  
    constrOnUnassigned :: Solver -> SomeConstraintHandler -> a -> Lit -> IO ()
  
    isPBRepresentable :: a -> IO Bool
    toPBLinAtLeast :: a -> IO PBLinAtLeast
  
    isSatisfied :: Solver -> a -> IO Bool
  
    constrIsProtected :: Solver -> a -> IO Bool
    constrIsProtected _ _ = return False
  
    constrWeight :: Solver -> a -> IO Double
    constrWeight _ _ = return 1.0
  
    constrReadActivity :: a -> IO Double
  
    constrWriteActivity :: a -> Double -> IO ()
  
  attach :: Solver -> SomeConstraintHandler -> IO Bool
  attach solver c = constrAttach solver c c
  
  detach :: Solver -> SomeConstraintHandler -> IO ()
  detach solver c = do
    constrDetach solver c c
    b <- isPBRepresentable c
    when b $ do
      (lhs,_) <- toPBLinAtLeast c
      forM_ lhs $ \(_,lit) -> do
        Vec.unsafeModify (svLitOccurList solver) (litIndex lit) (HashSet.delete c)
  
  -- | invoked with the watched literal when the literal is falsified.
  propagate :: Solver -> SomeConstraintHandler -> Lit -> IO Bool
  propagate solver c l = constrPropagate solver c c l
  
  -- | deduce a clause C∨l from the constraint and return C.
  -- C and l should be false and true respectively under the current
  -- assignment.
  reasonOf :: ConstraintHandler a => Solver -> a -> Maybe Lit -> IO Clause
  reasonOf solver c x = do
    when debugMode $
      case x of
        Nothing -> return ()
        Just lit -> do
          val <- litValue solver lit
          unless (lTrue == val) $ do
            str <- showConstraintHandler c
            error (printf "reasonOf: value of literal %d should be True but %s (constrReasonOf %s %s)" lit (show val) str (show x))
    cl <- constrReasonOf solver c x
    when debugMode $ do
      forM_ cl $ \lit -> do
        val <- litValue solver lit
        unless (lFalse == val) $ do
          str <- showConstraintHandler c
          error (printf "reasonOf: value of literal %d should be False but %s (constrReasonOf %s %s)" lit (show val) str (show x))
    return cl
  
  isLocked :: Solver -> SomeConstraintHandler -> IO Bool
  isLocked solver c = constrIsLocked solver c c
  
  data SomeConstraintHandler
    = CHClause !ClauseHandler
    | CHAtLeast !AtLeastHandler
    | CHPBCounter !PBHandlerCounter
    | CHPBPueblo !PBHandlerPueblo
    | CHXORClause !XORClauseHandler
    | CHTheory !TheoryHandler
    deriving Eq
  
  instance Hashable SomeConstraintHandler where
    hashWithSalt s (CHClause c)    = s `hashWithSalt` (0::Int) `hashWithSalt` c
    hashWithSalt s (CHAtLeast c)   = s `hashWithSalt` (1::Int) `hashWithSalt` c
    hashWithSalt s (CHPBCounter c) = s `hashWithSalt` (2::Int) `hashWithSalt` c
    hashWithSalt s (CHPBPueblo c)  = s `hashWithSalt` (3::Int) `hashWithSalt` c
    hashWithSalt s (CHXORClause c) = s `hashWithSalt` (4::Int) `hashWithSalt` c
    hashWithSalt s (CHTheory c)    = s `hashWithSalt` (5::Int) `hashWithSalt` c
  
  instance ConstraintHandler SomeConstraintHandler where
    toConstraintHandler = id
  
    showConstraintHandler (CHClause c)    = showConstraintHandler c
    showConstraintHandler (CHAtLeast c)   = showConstraintHandler c
    showConstraintHandler (CHPBCounter c) = showConstraintHandler c
    showConstraintHandler (CHPBPueblo c)  = showConstraintHandler c
    showConstraintHandler (CHXORClause c) = showConstraintHandler c
    showConstraintHandler (CHTheory c)    = showConstraintHandler c
  
    constrAttach solver this (CHClause c)    = constrAttach solver this c
    constrAttach solver this (CHAtLeast c)   = constrAttach solver this c
    constrAttach solver this (CHPBCounter c) = constrAttach solver this c
    constrAttach solver this (CHPBPueblo c)  = constrAttach solver this c
    constrAttach solver this (CHXORClause c) = constrAttach solver this c
    constrAttach solver this (CHTheory c)    = constrAttach solver this c
  
    constrDetach solver this (CHClause c)    = constrDetach solver this c
    constrDetach solver this (CHAtLeast c)   = constrDetach solver this c
    constrDetach solver this (CHPBCounter c) = constrDetach solver this c
    constrDetach solver this (CHPBPueblo c)  = constrDetach solver this c
    constrDetach solver this (CHXORClause c) = constrDetach solver this c
    constrDetach solver this (CHTheory c)    = constrDetach solver this c
  
    constrIsLocked solver this (CHClause c)    = constrIsLocked solver this c
    constrIsLocked solver this (CHAtLeast c)   = constrIsLocked solver this c
    constrIsLocked solver this (CHPBCounter c) = constrIsLocked solver this c
    constrIsLocked solver this (CHPBPueblo c)  = constrIsLocked solver this c
    constrIsLocked solver this (CHXORClause c) = constrIsLocked solver this c
    constrIsLocked solver this (CHTheory c)    = constrIsLocked solver this c
  
    constrPropagate solver this (CHClause c)  lit   = constrPropagate solver this c lit
    constrPropagate solver this (CHAtLeast c) lit   = constrPropagate solver this c lit
    constrPropagate solver this (CHPBCounter c) lit = constrPropagate solver this c lit
    constrPropagate solver this (CHPBPueblo c) lit  = constrPropagate solver this c lit
    constrPropagate solver this (CHXORClause c) lit = constrPropagate solver this c lit
    constrPropagate solver this (CHTheory c) lit    = constrPropagate solver this c lit
  
    constrReasonOf solver (CHClause c)  l   = constrReasonOf solver c l
    constrReasonOf solver (CHAtLeast c) l   = constrReasonOf solver c l
    constrReasonOf solver (CHPBCounter c) l = constrReasonOf solver c l
    constrReasonOf solver (CHPBPueblo c) l  = constrReasonOf solver c l
    constrReasonOf solver (CHXORClause c) l = constrReasonOf solver c l
    constrReasonOf solver (CHTheory c) l    = constrReasonOf solver c l
  
    constrOnUnassigned solver this (CHClause c)  l   = constrOnUnassigned solver this c l
    constrOnUnassigned solver this (CHAtLeast c) l   = constrOnUnassigned solver this c l
    constrOnUnassigned solver this (CHPBCounter c) l = constrOnUnassigned solver this c l
    constrOnUnassigned solver this (CHPBPueblo c) l  = constrOnUnassigned solver this c l
    constrOnUnassigned solver this (CHXORClause c) l = constrOnUnassigned solver this c l
    constrOnUnassigned solver this (CHTheory c) l    = constrOnUnassigned solver this c l
  
    isPBRepresentable (CHClause c)    = isPBRepresentable c
    isPBRepresentable (CHAtLeast c)   = isPBRepresentable c
    isPBRepresentable (CHPBCounter c) = isPBRepresentable c
    isPBRepresentable (CHPBPueblo c)  = isPBRepresentable c
    isPBRepresentable (CHXORClause c) = isPBRepresentable c
    isPBRepresentable (CHTheory c)    = isPBRepresentable c
  
    toPBLinAtLeast (CHClause c)    = toPBLinAtLeast c
    toPBLinAtLeast (CHAtLeast c)   = toPBLinAtLeast c
    toPBLinAtLeast (CHPBCounter c) = toPBLinAtLeast c
    toPBLinAtLeast (CHPBPueblo c)  = toPBLinAtLeast c
    toPBLinAtLeast (CHXORClause c) = toPBLinAtLeast c
    toPBLinAtLeast (CHTheory c)    = toPBLinAtLeast c
  
    isSatisfied solver (CHClause c)    = isSatisfied solver c
    isSatisfied solver (CHAtLeast c)   = isSatisfied solver c
    isSatisfied solver (CHPBCounter c) = isSatisfied solver c
    isSatisfied solver (CHPBPueblo c)  = isSatisfied solver c
    isSatisfied solver (CHXORClause c) = isSatisfied solver c
    isSatisfied solver (CHTheory c)    = isSatisfied solver c
  
    constrIsProtected solver (CHClause c)    = constrIsProtected solver c
    constrIsProtected solver (CHAtLeast c)   = constrIsProtected solver c
    constrIsProtected solver (CHPBCounter c) = constrIsProtected solver c
    constrIsProtected solver (CHPBPueblo c)  = constrIsProtected solver c
    constrIsProtected solver (CHXORClause c) = constrIsProtected solver c
    constrIsProtected solver (CHTheory c)    = constrIsProtected solver c
  
    constrReadActivity (CHClause c)    = constrReadActivity c
    constrReadActivity (CHAtLeast c)   = constrReadActivity c
    constrReadActivity (CHPBCounter c) = constrReadActivity c
    constrReadActivity (CHPBPueblo c)  = constrReadActivity c
    constrReadActivity (CHXORClause c) = constrReadActivity c
    constrReadActivity (CHTheory c)    = constrReadActivity c
  
    constrWriteActivity (CHClause c)    aval = constrWriteActivity c aval
    constrWriteActivity (CHAtLeast c)   aval = constrWriteActivity c aval
    constrWriteActivity (CHPBCounter c) aval = constrWriteActivity c aval
    constrWriteActivity (CHPBPueblo c)  aval = constrWriteActivity c aval
    constrWriteActivity (CHXORClause c) aval = constrWriteActivity c aval
    constrWriteActivity (CHTheory c)    aval = constrWriteActivity c aval
  
  isReasonOf :: Solver -> SomeConstraintHandler -> Lit -> IO Bool
  isReasonOf solver c lit = do
    val <- litValue solver lit
    if val == lUndef then
      return False
    else do
      m <- varReason solver (litVar lit)
      case m of
        Nothing -> return False
        Just c2  -> return $! c == c2
  
  -- To avoid heap-allocation Maybe value, it returns -1 when not found.
  findForWatch :: Solver -> LitArray -> Int -> Int -> IO Int
  #ifndef __GLASGOW_HASKELL__
  findForWatch solver a beg end = go beg end
    where
      go :: Int -> Int -> IO Int
      go i end | i > end = return (-1)
      go i end = do
        val <- litValue s =<< readLitArray a i
        if val /= lFalse
          then return i
          else go (i+1) end
  #else
  {- We performed worker-wrapper transfomation manually, since the worker
     generated by GHC has type
     "Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int #)",
     not "Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int# #)".
     We want latter one to avoid heap-allocating Int value. -}
  findForWatch solver a (I# beg) (I# end) = IO $ \w ->
    case go# beg end w of
      (# w2, ret #) -> (# w2, I# ret #)
    where
      go# :: Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int# #)
      go# i end' w | isTrue# (i ># end') = (# w, -1# #)
      go# i end' w =
        case unIO (litValue solver =<< readLitArray a (I# i)) w of
          (# w2, val #) ->
            if val /= lFalse
              then (# w2, i #)
              else go# (i +# 1#) end' w2
  
      unIO (IO f) = f
  #endif
  
  -- To avoid heap-allocating Maybe value, it returns -1 when not found.
  findForWatch2 :: Solver -> LitArray -> Int -> Int -> IO Int
  #ifndef __GLASGOW_HASKELL__
  findForWatch2 solver a beg end = go beg end
    where
      go :: Int -> Int -> IO Int
      go i end | i > end = return (-1)
      go i end = do
        val <- litValue s =<< readLitArray a i
        if val == lUndef
          then return i
          else go (i+1) end
  #else
  {- We performed worker-wrapper transfomation manually, since the worker
     generated by GHC has type
     "Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int #)",
     not "Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int# #)".
     We want latter one to avoid heap-allocating Int value. -}
  findForWatch2 solver a (I# beg) (I# end) = IO $ \w ->
    case go# beg end w of
      (# w2, ret #) -> (# w2, I# ret #)
    where
      go# :: Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int# #)
      go# i end w | isTrue# (i ># end) = (# w, -1# #)
      go# i end w =
        case unIO (litValue solver =<< readLitArray a (I# i)) w of
          (# w2, val #) ->
            if val == lUndef
              then (# w2, i #)
              else go# (i +# 1#) end w2
  
      unIO (IO f) = f
  #endif
  
  {--------------------------------------------------------------------
    Clause
  --------------------------------------------------------------------}
  
  data ClauseHandler
    = ClauseHandler
    { claLits :: !LitArray
    , claActivity :: !(IORef Double)
    , claHash :: !Int
    }
  
  claGetSize :: ClauseHandler -> IO Int
  claGetSize cla = getLitArraySize (claLits cla)
  
  instance Eq ClauseHandler where
    (==) = (==) `on` claLits
  
  instance Hashable ClauseHandler where
    hash = claHash
    hashWithSalt = defaultHashWithSalt
  
  newClauseHandler :: Clause -> Bool -> IO ClauseHandler
  newClauseHandler ls learnt = do
    a <- newLitArray ls
    act <- newIORef $! (if learnt then 0 else -1)
    return (ClauseHandler a act (hash ls))
  
  instance ConstraintHandler ClauseHandler where
    toConstraintHandler = CHClause
  
    showConstraintHandler this = do
      lits <- getLits (claLits this)
      return (show lits)
  
    constrAttach solver this this2 = do
      -- BCP Queue should be empty at this point.
      -- If not, duplicated propagation happens.
      bcpCheckEmpty solver
  
      size <- claGetSize this2
      if size == 0 then do
        markBad solver
        return False
      else if size == 1 then do
        lit0 <- readLitArray (claLits this2) 0
        assignBy solver lit0 this
      else do
        ref <- newIORef 1
        let f i = do
              lit_i <- readLitArray (claLits this2) i
              val_i <- litValue solver lit_i
              if val_i /= lFalse then
                return True
              else do
                j <- readIORef ref
                k <- findForWatch solver (claLits this2) j (size - 1)
                case k of
                  -1 -> do
                    return False
                  _ -> do
                    lit_k <- readLitArray (claLits this2) k
                    writeLitArray (claLits this2) i lit_k
                    writeLitArray (claLits this2) k lit_i
                    writeIORef ref $! (k+1)
                    return True
  
        b <- f 0
        if b then do
          lit0 <- readLitArray (claLits this2) 0
          watchLit solver lit0 this
          b2 <- f 1
          if b2 then do
            lit1 <- readLitArray (claLits this2) 1
            watchLit solver lit1 this
            return True
          else do -- UNIT
            -- We need to watch the most recently falsified literal
            (i,_) <- liftM (maximumBy (comparing snd)) $ forM [1..size-1] $ \l -> do
              lit <- readLitArray (claLits this2) l
              lv <- litLevel solver lit
              return (l,lv)
            lit1 <- readLitArray (claLits this2) 1
            liti <- readLitArray (claLits this2) i
            writeLitArray (claLits this2) 1 liti
            writeLitArray (claLits this2) i lit1
            watchLit solver liti this
            assignBy solver lit0 this -- should always succeed
        else do -- CONFLICT
          ls <- liftM (map fst . sortBy (comparing (Down . snd))) $ forM [0..size-1] $ \l -> do
            lit <- readLitArray (claLits this2) l
            lv <- litLevel solver lit
            return (l,lv)
          forM_ (zip [0..] ls) $ \(i,lit) -> do
            writeLitArray (claLits this2) i lit
          lit0 <- readLitArray (claLits this2) 0
          lit1 <- readLitArray (claLits this2) 1
          watchLit solver lit0 this
          watchLit solver lit1 this
          return False
  
    constrDetach solver this this2 = do
      size <- claGetSize this2
      when (size >= 2) $ do
        lit0 <- readLitArray (claLits this2) 0
        lit1 <- readLitArray (claLits this2) 1
        unwatchLit solver lit0 this
        unwatchLit solver lit1 this
  
    constrIsLocked solver this this2 = do
      size <- claGetSize this2
      if size < 2 then
        return False
      else do
        lit <- readLitArray (claLits this2) 0
        isReasonOf solver this lit
  
    constrPropagate !solver this this2 !falsifiedLit = do
      preprocess
  
      !lit0 <- readLitArray a 0
      !val0 <- litValue solver lit0
      if val0 == lTrue then do
        watchLit solver falsifiedLit this
        return True
      else do
        size <- claGetSize this2
        i <- findForWatch solver a 2 (size - 1)
        case i of
          -1 -> do
            when debugMode $ logIO solver $ do
               str <- showConstraintHandler this
               return $ printf "constrPropagate: %s is unit" str
            watchLit solver falsifiedLit this
            assignBy solver lit0 this
          _  -> do
            !lit1 <- readLitArray a 1
            !liti <- readLitArray a i
            writeLitArray a 1 liti
            writeLitArray a i lit1
            watchLit solver liti this
            return True
  
      where
        a = claLits this2
  
        preprocess :: IO ()
        preprocess = do
          !l0 <- readLitArray a 0
          !l1 <- readLitArray a 1
          assert (l0==falsifiedLit || l1==falsifiedLit) $ return ()
          when (l0==falsifiedLit) $ do
            writeLitArray a 0 l1
            writeLitArray a 1 l0
  
    constrReasonOf _ this l = do
      lits <- getLits (claLits this)
      case l of
        Nothing -> return lits
        Just lit -> do
          assert (lit == head lits) $ return ()
          return $ tail lits
  
    constrOnUnassigned _solver _this _this2 _lit = return ()
  
    isPBRepresentable _ = return True
  
    toPBLinAtLeast this = do
      lits <- getLits (claLits this)
      return ([(1,l) | l <- lits], 1)
  
    isSatisfied solver this = do
      n <- getLitArraySize (claLits this)
      liftM isLeft $ runExceptT $ forLoop 0 (<n) (+1) $ \i -> do
        v <- lift $ litValue solver =<< readLitArray (claLits this) i
        when (v == lTrue) $ throwE ()
  
    constrIsProtected _ this = do
      size <- claGetSize this
      return $! size <= 2
  
    constrReadActivity this = readIORef (claActivity this)
  
    constrWriteActivity this aval = writeIORef (claActivity this) $! aval
  
  basicAttachClauseHandler :: Solver -> ClauseHandler -> IO Bool
  basicAttachClauseHandler solver this = do
    let constr = toConstraintHandler this
    lits <- getLits (claLits this)
    case lits of
      [] -> do
        markBad solver
        return False
      [l1] -> do
        assignBy solver l1 constr
      l1:l2:_ -> do
        watchLit solver l1 constr
        watchLit solver l2 constr
        return True
  
  {--------------------------------------------------------------------
    Cardinality Constraint
  --------------------------------------------------------------------}
  
  data AtLeastHandler
    = AtLeastHandler
    { atLeastLits :: !LitArray
    , atLeastNum :: !Int
    , atLeastActivity :: !(IORef Double)
    , atLeastHash :: !Int
    }
  
  instance Eq AtLeastHandler where
    (==) = (==) `on` atLeastLits
  
  instance Hashable AtLeastHandler where
    hash = atLeastHash
    hashWithSalt = defaultHashWithSalt
  
  newAtLeastHandler :: [Lit] -> Int -> Bool -> IO AtLeastHandler
  newAtLeastHandler ls n learnt = do
    a <- newLitArray ls
    act <- newIORef $! (if learnt then 0 else -1)
    return (AtLeastHandler a n act (hash (ls,n)))
  
  instance ConstraintHandler AtLeastHandler where
    toConstraintHandler = CHAtLeast
  
    showConstraintHandler this = do
      lits <- getLits (atLeastLits this)
      return $ show lits ++ " >= " ++ show (atLeastNum this)
  
    -- FIXME: simplify implementation
    constrAttach solver this this2 = do
      -- BCP Queue should be empty at this point.
      -- If not, duplicated propagation happens.
      bcpCheckEmpty solver
  
      let a = atLeastLits this2
      m <- getLitArraySize a
      let n = atLeastNum this2
  
      if m < n then do
        markBad solver
        return False
      else if m == n then do
        let f i = do
              lit <- readLitArray a i
              assignBy solver lit this
        allM f [0..n-1]
      else do -- m > n
        let f !i !j
              | i == n = do
                  -- NOT VIOLATED: n literals (0 .. n-1) are watched
                  k <- findForWatch solver a j (m - 1)
                  if k /= -1 then do
                    -- NOT UNIT
                    lit_n <- readLitArray a n
                    lit_k <- readLitArray a k
                    writeLitArray a n lit_k
                    writeLitArray a k lit_n
                    watchLit solver lit_k this
                    -- n+1 literals (0 .. n) are watched.
                  else do
                    -- UNIT
                    forLoop 0 (<n) (+1) $ \l -> do
                      lit <- readLitArray a l
                      _ <- assignBy solver lit this -- should always succeed
                      return ()
                    -- We need to watch the most recently falsified literal
                    (l,_) <- liftM (maximumBy (comparing snd)) $ forM [n..m-1] $ \l -> do
                      lit <- readLitArray a l
                      lv <- litLevel solver lit
                      when debugMode $ do
                        val <- litValue solver lit
                        unless (val == lFalse) $ error "AtLeastHandler.attach: should not happen"
                      return (l,lv)
                    lit_n <- readLitArray a n
                    lit_l <- readLitArray a l
                    writeLitArray a n lit_l
                    writeLitArray a l lit_n
                    watchLit solver lit_l this
                    -- n+1 literals (0 .. n) are watched.
                  return True
              | otherwise = do
                  assert (i < n && n <= j) $ return ()
                  lit_i <- readLitArray a i
                  val_i <- litValue solver lit_i
                  if val_i /= lFalse then do
                    watchLit solver lit_i this
                    f (i+1) j
                  else do
                    k <- findForWatch solver a j (m - 1)
                    if k /= -1 then do
                      lit_k <- readLitArray a k
                      writeLitArray a i lit_k
                      writeLitArray a k lit_i
                      watchLit solver lit_k this
                      f (i+1) (k+1)
                    else do
                      -- CONFLICT
                      -- We need to watch unassigned literals or most recently falsified literals.
                      do xs <- liftM (sortBy (comparing (Down . snd))) $ forM [i..m-1] $ \l -> do
                           lit <- readLitArray a l
                           val <- litValue solver lit
                           if val == lFalse then do
                             lv <- litLevel solver lit
                             return (lit, lv)
                           else do
                             return (lit, maxBound)
                         forM_ (zip [i..m-1] xs) $ \(l,(lit,_lv)) -> do
                           writeLitArray a l lit
                      forLoop i (<=n) (+1) $ \l -> do
                        lit_l <- readLitArray a l
                        watchLit solver lit_l this
                      -- n+1 literals (0 .. n) are watched.
                      return False
        f 0 n
  
    constrDetach solver this this2 = do
      lits <- getLits (atLeastLits this2)
      let n = atLeastNum this2
      when (length lits > n) $ do
        forLoop 0 (<=n) (+1) $ \i -> do
          lit <- readLitArray (atLeastLits this2) i
          unwatchLit solver lit this
  
    constrIsLocked solver this this2 = do
      size <- getLitArraySize (atLeastLits this2)
      let n = atLeastNum this2
          loop i
            | i > n = return False
            | otherwise = do
                l <- readLitArray (atLeastLits this2) i
                b <- isReasonOf solver this l
                if b then return True else loop (i+1)
      if size >= n+1 then
        loop 0
      else
        return False
  
    constrPropagate solver this this2 falsifiedLit = do
      preprocess
  
      when debugMode $ do
        litn <- readLitArray a n
        unless (litn == falsifiedLit) $ error "AtLeastHandler.constrPropagate: should not happen"
  
      m <- getLitArraySize a
      i <- findForWatch solver a (n+1) (m-1)
      case i of
        -1 -> do
          when debugMode $ logIO solver $ do
            str <- showConstraintHandler this
            return $ printf "constrPropagate: %s is unit" str
          watchLit solver falsifiedLit this
          let loop :: Int -> IO Bool
              loop j
                | j >= n = return True
                | otherwise = do
                    litj <- readLitArray a j
                    ret2 <- assignBy solver litj this
                    if ret2
                      then loop (j+1)
                      else return False
          loop 0
        _ -> do
          liti <- readLitArray a i
          litn <- readLitArray a n
          writeLitArray a i litn
          writeLitArray a n liti
          watchLit solver liti this
          return True
  
      where
        a = atLeastLits this2
        n = atLeastNum this2
  
        preprocess :: IO ()
        preprocess = loop 0
          where
            loop :: Int -> IO ()
            loop i
              | i >= n = return ()
              | otherwise = do
                li <- readLitArray a i
                if (li /= falsifiedLit) then
                  loop (i+1)
                else do
                  ln <- readLitArray a n
                  writeLitArray a n li
                  writeLitArray a i ln
  
    constrReasonOf solver this concl = do
      m <- getLitArraySize (atLeastLits this)
      let n = atLeastNum this
      falsifiedLits <- mapM (readLitArray (atLeastLits this)) [n..m-1] -- drop first n elements
      when debugMode $ do
        forM_ falsifiedLits $ \lit -> do
          val <- litValue solver lit
          unless (val == lFalse) $ do
            error $ printf "AtLeastHandler.constrReasonOf: %d is %s (lFalse expected)" lit (show val)
      case concl of
        Nothing -> do
          let go :: Int -> IO Lit
              go i
                | i >= n = error $ printf "AtLeastHandler.constrReasonOf: cannot find falsified literal in first %d elements" n
                | otherwise = do
                    lit <- readLitArray (atLeastLits this) i
                    val <- litValue solver lit
                    if val == lFalse
                    then return lit
                    else go (i+1)
          lit <- go 0
          return $ lit : falsifiedLits
        Just lit -> do
          when debugMode $ do
            es <- getLits (atLeastLits this)
            unless (lit `elem` take n es) $
              error $ printf "AtLeastHandler.constrReasonOf: cannot find %d in first %d elements" n
          return falsifiedLits
  
    constrOnUnassigned _solver _this _this2 _lit = return ()
  
    isPBRepresentable _ = return True
  
    toPBLinAtLeast this = do
      lits <- getLits (atLeastLits this)
      return ([(1,l) | l <- lits], fromIntegral (atLeastNum this))
  
    isSatisfied solver this = do
      m <- getLitArraySize (atLeastLits this)
      liftM isLeft $ runExceptT $ numLoopState 0 (m-1) 0 $ \(!n) i -> do
        v <- lift $ litValue solver =<< readLitArray (atLeastLits this) i
        if v /= lTrue then do
          return n
        else do
          let n' = n + 1
          when (n' >= atLeastNum this) $ throwE ()
          return n'
  
    constrReadActivity this = readIORef (atLeastActivity this)
  
    constrWriteActivity this aval = writeIORef (atLeastActivity this) $! aval
  
  basicAttachAtLeastHandler :: Solver -> AtLeastHandler -> IO Bool
  basicAttachAtLeastHandler solver this = do
    lits <- getLits (atLeastLits this)
    let m = length lits
        n = atLeastNum this
        constr = toConstraintHandler this
    if m < n then do
      markBad solver
      return False
    else if m == n then do
      allM (\l -> assignBy solver l constr) lits
    else do -- m > n
      forM_ (take (n+1) lits) $ \l -> watchLit solver l constr
      return True
  
  {--------------------------------------------------------------------
    Pseudo Boolean Constraint
  --------------------------------------------------------------------}
  
  newPBHandler :: Solver -> PBLinSum -> Integer -> Bool -> IO SomeConstraintHandler
  newPBHandler solver ts degree learnt = do
    config <- configPBHandlerType <$> getConfig solver
    case config of
      PBHandlerTypeCounter -> do
        c <- newPBHandlerCounter ts degree learnt
        return (toConstraintHandler c)
      PBHandlerTypePueblo -> do
        c <- newPBHandlerPueblo ts degree learnt
        return (toConstraintHandler c)
  
  newPBHandlerPromoted :: Solver -> PBLinSum -> Integer -> Bool -> IO SomeConstraintHandler
  newPBHandlerPromoted solver lhs rhs learnt = do
    case pbToAtLeast (lhs,rhs) of
      Nothing -> newPBHandler solver lhs rhs learnt
      Just (lhs2, rhs2) -> do
        if rhs2 /= 1 then do
          h <- newAtLeastHandler lhs2 rhs2 learnt
          return $ toConstraintHandler h
        else do
          h <- newClauseHandler lhs2 learnt
          return $ toConstraintHandler h
  
  pbOverSAT :: Solver -> PBLinAtLeast -> IO Bool
  pbOverSAT solver (lhs, rhs) = do
    ss <- forM lhs $ \(c,l) -> do
      v <- litValue solver l
      if v /= lFalse
        then return c
        else return 0
    return $! sum ss > rhs
  
  pbToAtLeast :: PBLinAtLeast -> Maybe AtLeast
  pbToAtLeast (lhs, rhs) = do
    let cs = [c | (c,_) <- lhs]
    guard $ Set.size (Set.fromList cs) == 1
    let c = head cs
    return $ (map snd lhs, fromInteger ((rhs+c-1) `div` c))
  
  pbToClause :: PBLinAtLeast -> Maybe Clause
  pbToClause pb = do
    (lhs, rhs) <- pbToAtLeast pb
    guard $ rhs == 1
    return lhs
  
  {--------------------------------------------------------------------
    Pseudo Boolean Constraint (Counter)
  --------------------------------------------------------------------}
  
  data PBHandlerCounter
    = PBHandlerCounter
    { pbTerms    :: !PBLinSum -- sorted in the decending order on coefficients.
    , pbDegree   :: !Integer
    , pbCoeffMap :: !(LitMap Integer)
    , pbMaxSlack :: !Integer
    , pbSlack    :: !(IORef Integer)
    , pbActivity :: !(IORef Double)
    , pbHash     :: !Int
    }
  
  instance Eq PBHandlerCounter where
    (==) = (==) `on` pbSlack
  
  instance Hashable PBHandlerCounter where
    hash = pbHash
    hashWithSalt = defaultHashWithSalt
  
  newPBHandlerCounter :: PBLinSum -> Integer -> Bool -> IO PBHandlerCounter
  newPBHandlerCounter ts degree learnt = do
    let ts' = sortBy (comparing (Down . fst)) ts
        slack = sum (map fst ts) - degree
        m = IM.fromList [(l,c) | (c,l) <- ts]
    s <- newIORef slack
    act <- newIORef $! (if learnt then 0 else -1)
    return (PBHandlerCounter ts' degree m slack s act (hash (ts,degree)))
  
  instance ConstraintHandler PBHandlerCounter where
    toConstraintHandler = CHPBCounter
  
    showConstraintHandler this = do
      return $ show (pbTerms this) ++ " >= " ++ show (pbDegree this)
  
    constrAttach solver this this2 = do
      -- BCP queue should be empty at this point.
      -- It is important for calculating slack.
      bcpCheckEmpty solver
      s <- liftM sum $ forM (pbTerms this2) $ \(c,l) -> do
        watchLit solver l this
        val <- litValue solver l
        if val == lFalse then do
          addOnUnassigned solver this l
          return 0
        else do
          return c
      let slack = s - pbDegree this2
      writeIORef (pbSlack this2) $! slack
      if slack < 0 then
        return False
      else do
        flip allM (pbTerms this2) $ \(c,l) -> do
          val <- litValue solver l
          if c > slack && val == lUndef then do
            assignBy solver l this
          else
            return True
  
    constrDetach solver this this2 = do
      forM_ (pbTerms this2) $ \(_,l) -> do
        unwatchLit solver l this
  
    constrIsLocked solver this this2 = do
      anyM (\(_,l) -> isReasonOf solver this l) (pbTerms this2)
  
    constrPropagate solver this this2 falsifiedLit = do
      watchLit solver falsifiedLit this
      let c = pbCoeffMap this2 IM.! falsifiedLit
      modifyIORef' (pbSlack this2) (subtract c)
      addOnUnassigned solver this falsifiedLit
      s <- readIORef (pbSlack this2)
      if s < 0 then
        return False
      else do
        forM_ (takeWhile (\(c1,_) -> c1 > s) (pbTerms this2)) $ \(_,l1) -> do
          v <- litValue solver l1
          when (v == lUndef) $ do
            assignBy solver l1 this
            return ()
        return True
  
    constrReasonOf solver this l = do
      case l of
        Nothing -> do
          let p _ = return True
          f p (pbMaxSlack this) (pbTerms this)
        Just lit -> do
          idx <- varAssignNo solver (litVar lit)
          -- PB制約の場合には複数回unitになる可能性があり、
          -- litへの伝播以降に割り当てられたリテラルを含まないよう注意が必要
          let p lit2 =do
                idx2 <- varAssignNo solver (litVar lit2)
                return $ idx2 < idx
          let c = pbCoeffMap this IM.! lit
          f p (pbMaxSlack this - c) (pbTerms this)
      where
        {-# INLINE f #-}
        f :: (Lit -> IO Bool) -> Integer -> PBLinSum -> IO [Lit]
        f p s xs = go s xs []
          where
            go :: Integer -> PBLinSum -> [Lit] -> IO [Lit]
            go s _ ret | s < 0 = return ret
            go _ [] _ = error "PBHandlerCounter.constrReasonOf: should not happen"
            go s ((c,lit):xs) ret = do
              val <- litValue solver lit
              if val == lFalse then do
                b <- p lit
                if b
                then go (s - c) xs (lit:ret)
                else go s xs ret
              else do
                go s xs ret
  
    constrOnUnassigned _solver _this this2 lit = do
      let c = pbCoeffMap this2 IM.! (- lit)
      modifyIORef' (pbSlack this2) (+ c)
  
    isPBRepresentable _ = return True
  
    toPBLinAtLeast this = do
      return (pbTerms this, pbDegree this)
  
    isSatisfied solver this = do
      xs <- forM (pbTerms this) $ \(c,l) -> do
        v <- litValue solver l
        if v == lTrue
          then return c
          else return 0
      return $ sum xs >= pbDegree this
  
    constrWeight _ _ = return 0.5
  
    constrReadActivity this = readIORef (pbActivity this)
  
    constrWriteActivity this aval = writeIORef (pbActivity this) $! aval
  
  {--------------------------------------------------------------------
    Pseudo Boolean Constraint (Pueblo)
  --------------------------------------------------------------------}
  
  data PBHandlerPueblo
    = PBHandlerPueblo
    { puebloTerms     :: !PBLinSum
    , puebloDegree    :: !Integer
    , puebloMaxSlack  :: !Integer
    , puebloWatches   :: !(IORef LitSet)
    , puebloWatchSum  :: !(IORef Integer)
    , puebloActivity  :: !(IORef Double)
    , puebloHash      :: !Int
    }
  
  instance Eq PBHandlerPueblo where
    (==) = (==) `on` puebloWatchSum
  
  instance Hashable PBHandlerPueblo where
    hash = puebloHash
    hashWithSalt = defaultHashWithSalt
  
  puebloAMax :: PBHandlerPueblo -> Integer
  puebloAMax this =
    case puebloTerms this of
      (c,_):_ -> c
      [] -> 0 -- should not happen?
  
  newPBHandlerPueblo :: PBLinSum -> Integer -> Bool -> IO PBHandlerPueblo
  newPBHandlerPueblo ts degree learnt = do
    let ts' = sortBy (comparing (Down . fst)) ts
        slack = sum [c | (c,_) <- ts'] - degree
    ws   <- newIORef IS.empty
    wsum <- newIORef 0
    act  <- newIORef $! (if learnt then 0 else -1)
    return $ PBHandlerPueblo ts' degree slack ws wsum act (hash (ts,degree))
  
  puebloGetWatchSum :: PBHandlerPueblo -> IO Integer
  puebloGetWatchSum pb = readIORef (puebloWatchSum pb)
  
  puebloWatch :: Solver -> SomeConstraintHandler -> PBHandlerPueblo -> PBLinTerm -> IO ()
  puebloWatch solver constr !pb (c, lit) = do
    watchLit solver lit constr
    modifyIORef' (puebloWatches pb) (IS.insert lit)
    modifyIORef' (puebloWatchSum pb) (+c)
  
  puebloUnwatch :: Solver -> PBHandlerPueblo -> PBLinTerm -> IO ()
  puebloUnwatch _solver pb (c, lit) = do
    modifyIORef' (puebloWatches pb) (IS.delete lit)
    modifyIORef' (puebloWatchSum pb) (subtract c)
  
  instance ConstraintHandler PBHandlerPueblo where
    toConstraintHandler = CHPBPueblo
  
    showConstraintHandler this = do
      return $ show (puebloTerms this) ++ " >= " ++ show (puebloDegree this)
  
    constrAttach solver this this2 = do
      bcpCheckEmpty solver
      ret <- puebloPropagate solver this this2
  
      -- register to watch recently falsified literals to recover
      -- "WatchSum >= puebloDegree this + puebloAMax this" when backtrack is performed.
      wsum <- puebloGetWatchSum this2
      unless (wsum >= puebloDegree this2 + puebloAMax this2) $ do
        let f m tm@(_,lit) = do
              val <- litValue solver lit
              if val == lFalse then do
                idx <- varAssignNo solver (litVar lit)
                return (IM.insert idx tm m)
              else
                return m
        xs <- liftM (map snd . IM.toDescList) $ foldM f IM.empty (puebloTerms this2)
        let g !_ [] = return ()
            g !s ((c,l):ts) = do
              addOnUnassigned solver this l
              if s+c >= puebloDegree this2 + puebloAMax this2 then return ()
              else g (s+c) ts
        g wsum xs
  
      return ret
  
    constrDetach solver this this2 = do
      ws <- readIORef (puebloWatches this2)
      forM_ (IS.toList ws) $ \l -> do
        unwatchLit solver l this
  
    constrIsLocked solver this this2 = do
      anyM (\(_,l) -> isReasonOf solver this l) (puebloTerms this2)
  
    constrPropagate solver this this2 falsifiedLit = do
      let t = fromJust $ find (\(_,l) -> l==falsifiedLit) (puebloTerms this2)
      puebloUnwatch solver this2 t
      ret <- puebloPropagate solver this this2
      wsum <- puebloGetWatchSum this2
      unless (wsum >= puebloDegree this2 + puebloAMax this2) $
        addOnUnassigned solver this falsifiedLit
      return ret
  
    constrReasonOf solver this l = do
      case l of
        Nothing -> do
          let p _ = return True
          f p (puebloMaxSlack this) (puebloTerms this)
        Just lit -> do
          idx <- varAssignNo solver (litVar lit)
          -- PB制約の場合には複数回unitになる可能性があり、
          -- litへの伝播以降に割り当てられたリテラルを含まないよう注意が必要
          let p lit2 =do
                idx2 <- varAssignNo solver (litVar lit2)
                return $ idx2 < idx
          let c = fst $ fromJust $ find (\(_,l) -> l == lit) (puebloTerms this)
          f p (puebloMaxSlack this - c) (puebloTerms this)
      where
        {-# INLINE f #-}
        f :: (Lit -> IO Bool) -> Integer -> PBLinSum -> IO [Lit]
        f p s xs = go s xs []
          where
            go :: Integer -> PBLinSum -> [Lit] -> IO [Lit]
            go s _ ret | s < 0 = return ret
            go _ [] _ = error "PBHandlerPueblo.constrReasonOf: should not happen"
            go s ((c,lit):xs) ret = do
              val <- litValue solver lit
              if val == lFalse then do
                b <- p lit
                if b
                then go (s - c) xs (lit:ret)
                else go s xs ret
              else do
                go s xs ret
  
    constrOnUnassigned solver this this2 lit = do
      let t = fromJust $ find (\(_,l) -> l == - lit) (puebloTerms this2)
      puebloWatch solver this this2 t
  
    isPBRepresentable _ = return True
  
    toPBLinAtLeast this = do
      return (puebloTerms this, puebloDegree this)
  
    isSatisfied solver this = do
      xs <- forM (puebloTerms this) $ \(c,l) -> do
        v <- litValue solver l
        if v == lTrue
          then return c
          else return 0
      return $ sum xs >= puebloDegree this
  
    constrWeight _ _ = return 0.5
  
    constrReadActivity this = readIORef (puebloActivity this)
  
    constrWriteActivity this aval = writeIORef (puebloActivity this) $! aval
  
  puebloPropagate :: Solver -> SomeConstraintHandler -> PBHandlerPueblo -> IO Bool
  puebloPropagate solver constr this = do
    puebloUpdateWatchSum solver constr this
    watchsum <- puebloGetWatchSum this
    if puebloDegree this + puebloAMax this <= watchsum then
      return True
    else if watchsum < puebloDegree this then do
      -- CONFLICT
      return False
    else do -- puebloDegree this <= watchsum < puebloDegree this + puebloAMax this
      -- UNIT PROPAGATION
      let f [] = return True
          f ((c,lit) : ts) = do
            watchsum' <- puebloGetWatchSum this
            if watchsum' - c >= puebloDegree this then
              return True
            else do
              val <- litValue solver lit
              when (val == lUndef) $ do
                b <- assignBy solver lit constr
                assert b $ return ()
              f ts
      f $ puebloTerms this
  
  puebloUpdateWatchSum :: Solver -> SomeConstraintHandler -> PBHandlerPueblo -> IO ()
  puebloUpdateWatchSum solver constr this = do
    let f [] = return ()
        f (t@(_,lit):ts) = do
          watchSum <- puebloGetWatchSum this
          if watchSum >= puebloDegree this + puebloAMax this then
            return ()
          else do
            val <- litValue solver lit
            watched <- liftM (lit `IS.member`) $ readIORef (puebloWatches this)
            when (val /= lFalse && not watched) $ do
              puebloWatch solver constr this t
            f ts
    f (puebloTerms this)
  
  {--------------------------------------------------------------------
    XOR Clause
  --------------------------------------------------------------------}
  
  data XORClauseHandler
    = XORClauseHandler
    { xorLits :: !LitArray
    , xorActivity :: !(IORef Double)
    , xorHash :: !Int
    }
  
  instance Eq XORClauseHandler where
    (==) = (==) `on` xorLits
  
  instance Hashable XORClauseHandler where
    hash = xorHash
    hashWithSalt = defaultHashWithSalt
  
  newXORClauseHandler :: [Lit] -> Bool -> IO XORClauseHandler
  newXORClauseHandler ls learnt = do
    a <- newLitArray ls
    act <- newIORef $! (if learnt then 0 else -1)
    return (XORClauseHandler a act (hash ls))
  
  instance ConstraintHandler XORClauseHandler where
    toConstraintHandler = CHXORClause
  
    showConstraintHandler this = do
      lits <- getLits (xorLits this)
      return ("XOR " ++ show lits)
  
    constrAttach solver this this2 = do
      -- BCP Queue should be empty at this point.
      -- If not, duplicated propagation happens.
      bcpCheckEmpty solver
  
      let a = xorLits this2
      size <- getLitArraySize a
  
      if size == 0 then do
        markBad solver
        return False
      else if size == 1 then do
        lit0 <- readLitArray a 0
        assignBy solver lit0 this
      else do
        ref <- newIORef 1
        let f i = do
              lit_i <- readLitArray a i
              val_i <- litValue solver lit_i
              if val_i == lUndef then
                return True
              else do
                j <- readIORef ref
                k <- findForWatch2 solver a j (size - 1)
                case k of
                  -1 -> do
                    return False
                  _ -> do
                    lit_k <- readLitArray a k
                    writeLitArray a i lit_k
                    writeLitArray a k lit_i
                    writeIORef ref $! (k+1)
                    return True
  
        b <- f 0
        if b then do
          lit0 <- readLitArray a 0
          watchVar solver (litVar lit0) this
          b2 <- f 1
          if b2 then do
            lit1 <- readLitArray a 1
            watchVar solver (litVar lit1) this
            return True
          else do -- UNIT
            -- We need to watch the most recently falsified literal
            (i,_) <- liftM (maximumBy (comparing snd)) $ forM [1..size-1] $ \l -> do
              lit <- readLitArray a l
              lv <- litLevel solver lit
              return (l,lv)
            lit1 <- readLitArray a 1
            liti <- readLitArray a i
            writeLitArray a 1 liti
            writeLitArray a i lit1
            watchVar solver (litVar liti) this
            -- lit0 ⊕ y
            y <- do
              ref' <- newIORef False
              forLoop 1 (<size) (+1) $ \j -> do
                lit_j <- readLitArray a j
                val_j <- litValue solver lit_j
                modifyIORef' ref' (/= fromJust (unliftBool val_j))
              readIORef ref'
            assignBy solver (if y then litNot lit0 else lit0) this -- should always succeed
        else do
          ls <- liftM (map fst . sortBy (comparing (Down . snd))) $ forM [0..size-1] $ \l -> do
            lit <- readLitArray a l
            lv <- litLevel solver lit
            return (l,lv)
          forM_ (zip [0..] ls) $ \(i,lit) -> do
            writeLitArray a i lit
          lit0 <- readLitArray a 0
          lit1 <- readLitArray a 1
          watchVar solver (litVar lit0) this
          watchVar solver (litVar lit1) this
          isSatisfied solver this2
  
    constrDetach solver this this2 = do
      size <- getLitArraySize (xorLits this2)
      when (size >= 2) $ do
        lit0 <- readLitArray (xorLits this2) 0
        lit1 <- readLitArray (xorLits this2) 1
        unwatchVar solver (litVar lit0) this
        unwatchVar solver (litVar lit1) this
  
    constrIsLocked solver this this2 = do
      lit0 <- readLitArray (xorLits this2) 0
      lit1 <- readLitArray (xorLits this2) 1
      b0 <- isReasonOf solver this lit0
      b1 <- isReasonOf solver this lit1
      return $ b0 || b1
  
    constrPropagate !solver this this2 !falsifiedLit = do
      b <- constrIsLocked solver this this2
      if b then
        return True
      else do
        preprocess
  
        !lit0 <- readLitArray a 0
        !size <- getLitArraySize (xorLits this2)
        i <- findForWatch2 solver a 2 (size - 1)
        case i of
          -1 -> do
            when debugMode $ logIO solver $ do
               str <- showConstraintHandler this
               return $ printf "constrPropagate: %s is unit" str
            watchVar solver v this
            -- lit0 ⊕ y
            y <- do
              ref <- newIORef False
              forLoop 1 (<size) (+1) $ \j -> do
                lit_j <- readLitArray a j
                val_j <- litValue solver lit_j
                modifyIORef' ref (/= fromJust (unliftBool val_j))
              readIORef ref
            assignBy solver (if y then litNot lit0 else lit0) this
          _  -> do
            !lit1 <- readLitArray a 1
            !liti <- readLitArray a i
            writeLitArray a 1 liti
            writeLitArray a i lit1
            watchVar solver (litVar liti) this
            return True
  
      where
        v = litVar falsifiedLit
        a = xorLits this2
  
        preprocess :: IO ()
        preprocess = do
          !l0 <- readLitArray a 0
          !l1 <- readLitArray a 1
          assert (litVar l0 == v || litVar l1 == v) $ return ()
          when (litVar l0 == v) $ do
            writeLitArray a 0 l1
            writeLitArray a 1 l0
  
    constrReasonOf solver this l = do
      lits <- getLits (xorLits this)
      xs <-
        case l of
          Nothing -> mapM f lits
          Just lit -> do
           case lits of
             l1:ls -> do
               assert (litVar lit == litVar l1) $ return ()
               mapM f ls
             _ -> error "XORClauseHandler.constrReasonOf: should not happen"
      return xs
      where
        f :: Lit -> IO Lit
        f lit = do
          let v = litVar lit
          val <- varValue solver v
          return $ literal v (not (fromJust (unliftBool val)))
  
    constrOnUnassigned _solver _this _this2 _lit = return ()
  
    isPBRepresentable _ = return False
  
    toPBLinAtLeast _ = error "XORClauseHandler does not support toPBLinAtLeast"
  
    isSatisfied solver this = do
      lits <- getLits (xorLits this)
      vals <- mapM (litValue solver) lits
      let f x y
            | x == lUndef || y == lUndef = lUndef
            | otherwise = liftBool (x /= y)
      return $ foldl' f lFalse vals == lTrue
  
    constrIsProtected _ this = do
      size <- getLitArraySize (xorLits this)
      return $! size <= 2
  
    constrReadActivity this = readIORef (xorActivity this)
  
    constrWriteActivity this aval = writeIORef (xorActivity this) $! aval
  
  basicAttachXORClauseHandler :: Solver -> XORClauseHandler -> IO Bool
  basicAttachXORClauseHandler solver this = do
    lits <- getLits (xorLits this)
    let constr = toConstraintHandler this
    case lits of
      [] -> do
        markBad solver
        return False
      [l1] -> do
        assignBy solver l1 constr
      l1:l2:_ -> do
        watchVar solver (litVar l1) constr
        watchVar solver (litVar l2) constr
        return True
  
  {--------------------------------------------------------------------
    Arbitrary Boolean Theory
  --------------------------------------------------------------------}
  
  setTheory :: Solver -> TheorySolver -> IO ()
  setTheory solver tsolver = do
    d <- getDecisionLevel solver
    assert (d == levelRoot) $ return ()
  
    m <- readIORef (svTheorySolver solver)
    case m of
      Just _ -> do
        error $ "ToySolver.SAT.setTheory: cannot replace TheorySolver"
      Nothing -> do
        writeIORef (svTheorySolver solver) (Just tsolver)
        ret <- deduce solver
        case ret of
          Nothing -> return ()
          Just _ -> markBad solver
  
  getTheory :: Solver -> IO (Maybe TheorySolver)
  getTheory solver = readIORef (svTheorySolver solver)
  
  deduceT :: Solver -> ExceptT SomeConstraintHandler IO ()
  deduceT solver = do
    mt <- liftIO $ readIORef (svTheorySolver solver)
    case mt of
      Nothing -> return ()
      Just t -> do
        n <- liftIO $ Vec.getSize (svTrail solver)
        let h = CHTheory TheoryHandler
            callback l = assignBy solver l h
            loop i = do
              when (i < n) $ do
                l <- liftIO $ Vec.unsafeRead (svTrail solver) i
                ok <- liftIO $ thAssertLit t callback l
                if ok then
                  loop (i+1)
                else
                  throwE h
        loop =<< liftIO (readIOURef (svTheoryChecked solver))
        b2 <- liftIO $ thCheck t callback
        if b2 then do
          liftIO $ writeIOURef (svTheoryChecked solver) n
        else
          throwE h
  
  data TheoryHandler = TheoryHandler deriving (Eq)
  
  instance Hashable TheoryHandler where
    hash _ = hash ()
    hashWithSalt = defaultHashWithSalt
  
  instance ConstraintHandler TheoryHandler where
    toConstraintHandler = CHTheory
  
    showConstraintHandler _this = return "TheoryHandler"
  
    constrAttach _solver _this _this2 = error "TheoryHandler.constrAttach"
  
    constrDetach _solver _this _this2 = return ()
  
    constrIsLocked _solver _this _this2 = return True
  
    constrPropagate _solver _this _this2 _falsifiedLit =  error "TheoryHandler.constrPropagate"
  
    constrReasonOf solver _this l = do
      Just t <- readIORef (svTheorySolver solver)
      lits <- thExplain t l
      return $ [-lit | lit <- lits]
  
    constrOnUnassigned _solver _this _this2 _lit = return ()
  
    isPBRepresentable _this = return False
  
    toPBLinAtLeast _this = error "TheoryHandler.toPBLinAtLeast"
  
    isSatisfied _solver _this = error "TheoryHandler.isSatisfied"
  
    constrIsProtected _solver _this = error "TheoryHandler.constrIsProtected"
  
    constrReadActivity _this = return 0
  
    constrWriteActivity _this _aval = return ()
  
  {--------------------------------------------------------------------
    Restart strategy
  --------------------------------------------------------------------}
  
  mkRestartSeq :: RestartStrategy -> Int -> Double -> [Int]
  mkRestartSeq MiniSATRestarts = miniSatRestartSeq
  mkRestartSeq ArminRestarts   = arminRestartSeq
  mkRestartSeq LubyRestarts    = lubyRestartSeq
  
  miniSatRestartSeq :: Int -> Double -> [Int]
  miniSatRestartSeq start inc = iterate (ceiling . (inc *) . fromIntegral) start
  
  {-
  miniSatRestartSeq :: Int -> Double -> [Int]
  miniSatRestartSeq start inc = map round $ iterate (inc*) (fromIntegral start)
  -}
  
  arminRestartSeq :: Int -> Double -> [Int]
  arminRestartSeq start inc = go (fromIntegral start) (fromIntegral start)
    where
      go !inner !outer = round inner : go inner' outer'
        where
          (inner',outer') =
            if inner >= outer
            then (fromIntegral start, outer * inc)
            else (inner * inc, outer)
  
  lubyRestartSeq :: Int -> Double -> [Int]
  lubyRestartSeq start inc = map (ceiling . (fromIntegral start *) . luby inc) [0..]
  
  {-
    Finite subsequences of the Luby-sequence:
  
    0: 1
    1: 1 1 2
    2: 1 1 2 1 1 2 4
    3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
    ...
  
  
  -}
  luby :: Double -> Integer -> Double
  luby y x = go2 size1 sequ1 x
    where
      -- Find the finite subsequence that contains index 'x', and the
      -- size of that subsequence:
      (size1, sequ1) = go 1 0
  
      go :: Integer -> Integer -> (Integer, Integer)
      go size sequ
        | size < x+1 = go (2*size+1) (sequ+1)
        | otherwise  = (size, sequ)
  
      go2 :: Integer -> Integer -> Integer -> Double
      go2 size sequ x2
        | size-1 /= x2 = let size' = (size-1) `div` 2 in go2 size' (sequ - 1) (x2 `mod` size')
        | otherwise = y ^ sequ
  
  
  {--------------------------------------------------------------------
    utility
  --------------------------------------------------------------------}
  
  allM :: Monad m => (a -> m Bool) -> [a] -> m Bool
  allM p = go
    where
      go [] = return True
      go (x:xs) = do
        b <- p x
        if b
          then go xs
          else return False
  
  anyM :: Monad m => (a -> m Bool) -> [a] -> m Bool
  anyM p = go
    where
      go [] = return False
      go (x:xs) = do
        b <- p x
        if b
          then return True
          else go xs
  
  shift :: IORef [a] -> IO a
  shift ref = do
    (x:xs) <- readIORef ref
    writeIORef ref xs
    return x
  
  #if !MIN_VERSION_hashable(1,4,3)
  
  defaultHashWithSalt :: Hashable a => Int -> a -> Int
  defaultHashWithSalt salt x = salt `combine` hash x
    where
      combine :: Int -> Int -> Int
      combine h1 h2 = (h1 * 16777619) `xor` h2
  
  #endif
  
  {--------------------------------------------------------------------
    debug
  --------------------------------------------------------------------}
  
  debugMode :: Bool
  debugMode = False
  
  checkSatisfied :: Solver -> IO ()
  checkSatisfied solver = do
    cls <- readIORef (svConstrDB solver)
    forM_ cls $ \c -> do
      b <- isSatisfied solver c
      unless b $ do
        s <- showConstraintHandler c
        log solver $ "BUG: " ++ s ++ " is violated"
  
  dumpVarActivity :: Solver -> IO ()
  dumpVarActivity solver = do
    log solver "Variable activity:"
    vs <- variables solver
    forM_ vs $ \v -> do
      activity <- varActivity solver v
      log solver $ printf "activity(%d) = %d" v activity
  
  dumpConstrActivity :: Solver -> IO ()
  dumpConstrActivity solver = do
    log solver "Learnt constraints activity:"
    xs <- learntConstraints solver
    forM_ xs $ \c -> do
      s <- showConstraintHandler c
      aval <- constrReadActivity c
      log solver $ printf "activity(%s) = %f" s aval
  
  -- | set callback function for receiving messages.
  setLogger :: Solver -> (String -> IO ()) -> IO ()
  setLogger solver logger = do
    writeIORef (svLogger solver) (Just logger)
  
  -- | Clear logger function set by 'setLogger'.
  clearLogger :: Solver -> IO ()
  clearLogger solver = do
    writeIORef (svLogger solver) Nothing
  
  log :: Solver -> String -> IO ()
  log solver msg = logIO solver (return msg)
  
  logIO :: Solver -> IO String -> IO ()
  logIO solver action = do
    m <- readIORef (svLogger solver)
    case m of
      Nothing -> return ()
      Just logger -> action >>= logger
  