{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
{-# LANGUAGE BangPatterns, ScopedTypeVariables, CPP, DeriveDataTypeable #-}
#ifdef __GLASGOW_HASKELL__
{-# LANGUAGE UnboxedTuples, MagicHash #-}
#endif
#if __GLASGOW_HASKELL__ < 706
{-# LANGUAGE DoRec #-}
#else
{-# LANGUAGE RecursiveDo #-}
#endif
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT
-- Copyright   :  (c) Masahiro Sakai 2012-2014
-- License     :  BSD-style
-- 
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable (BangPatterns, ScopedTypeVariables, CPP, DeriveDataTypeable, RecursiveDo)
--
-- 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
  (
  -- * The @Solver@ type
    Solver
  , newSolver

  -- * Basic data structures
  , Var
  , Lit
  , literal
  , litNot
  , litVar
  , litPolarity
  , Clause

  -- * Problem specification
  , newVar
  , newVars
  , newVars_
  , resizeVarCapacity
  , addClause
  , addAtLeast
  , addAtMost
  , addExactly
  , addPBAtLeast
  , addPBAtMost
  , addPBExactly
  , addPBAtLeastSoft
  , addPBAtMostSoft
  , addPBExactlySoft
  , addXORClause
  , addXORClauseSoft
  , setTheory

  -- * Solving
  , solve
  , solveWith
  , BudgetExceeded (..)

  -- * Extract results
  , Model
  , getModel
  , getFailedAssumptions

  -- * Solver configulation
  , RestartStrategy (..)
  , setRestartStrategy
  , defaultRestartStrategy
  , setRestartFirst
  , defaultRestartFirst
  , setRestartInc
  , defaultRestartInc
  , setLearntSizeFirst
  , defaultLearntSizeFirst
  , setLearntSizeInc
  , defaultLearntSizeInc
  , setCCMin
  , defaultCCMin
  , LearningStrategy (..)
  , setLearningStrategy
  , defaultLearningStrategy
  , setEnablePhaseSaving
  , getEnablePhaseSaving
  , defaultEnablePhaseSaving
  , setEnableForwardSubsumptionRemoval
  , getEnableForwardSubsumptionRemoval
  , defaultEnableForwardSubsumptionRemoval
  , setEnableBackwardSubsumptionRemoval
  , getEnableBackwardSubsumptionRemoval
  , defaultEnableBackwardSubsumptionRemoval
  , setVarPolarity
  , setLogger
  , setCheckModel
  , setRandomFreq
  , defaultRandomFreq
  , setRandomGen
  , getRandomGen
  , setConfBudget
  , PBHandlerType (..)
  , setPBHandlerType
  , defaultPBHandlerType
  , setPBSplitClausePart
  , getPBSplitClausePart
  , defaultPBSplitClausePart

  -- * Read state
  , getNVars
  , getNConstraints
  , getNLearntConstraints
  , getVarFixed
  , getLitFixed

  -- * Read state (deprecated)
  , nVars
  , nAssigns
  , nConstraints
  , nLearnt  

  -- * Internal API
  , varBumpActivity
  , varDecayActivity
  ) where

import Prelude hiding (log)
import Control.Loop
import Control.Monad
import Control.Exception
#if MIN_VERSION_array(0,5,0)
import Data.Array.IO
#else
import Data.Array.IO hiding (unsafeFreeze)
#endif
import Data.Array.Unsafe (unsafeFreeze)
import Data.Array.Base (unsafeRead, unsafeWrite)
#if MIN_VERSION_hashable(1,2,0)
import Data.Bits (xor) -- for defining 'combine' function
#endif
import Data.Function (on)
import Data.Hashable
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import Data.IORef
import Data.List
import Data.Maybe
import Data.Ord
import qualified Data.IntMap 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.Time
import Data.Typeable
import System.CPUTime
import qualified System.Random 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.Types
import ToySolver.SAT.TheorySolver

{--------------------------------------------------------------------
  internal data structures
--------------------------------------------------------------------}

type Level = Int

levelRoot :: Level
levelRoot = 0

data VarData
  = VarData
  { vdPolarity   :: !(IORef Bool)
  , vdPosLitData :: !LitData
  , vdNegLitData :: !LitData
  -- | will be invoked once when the variable is assigned
  , vdWatches    :: !(IORef [SomeConstraintHandler])
  , vdActivity   :: !(IOURef VarActivity)
  , vdValue :: !(IORef LBool)
  , vdTrailIndex :: !(IOURef Int)
  , vdLevel :: !(IOURef Level)
  , vdReason :: !(IORef (Maybe SomeConstraintHandler))
  , vdOnUnassigned :: !(IORef [SomeConstraintHandler])
  }

data LitData
  = LitData
  { -- | will be invoked when this literal is falsified
    ldWatches   :: !(IORef [SomeConstraintHandler])
  , ldOccurList :: !(IORef (HashSet SomeConstraintHandler))
  }

newVarData :: IO VarData
newVarData = do
  polarity <- newIORef True
  pos <- newLitData
  neg <- newLitData
  watches <- newIORef []
  activity <- newIOURef 0

  val <- newIORef lUndef
  idx <- newIOURef maxBound
  lv <- newIOURef maxBound
  reason <- newIORef Nothing
  onUnassigned <- newIORef []

  return $
    VarData
    { vdPolarity = polarity
    , vdPosLitData = pos
    , vdNegLitData = neg
    , vdWatches = watches
    , vdActivity = activity
    , vdValue = val
    , vdTrailIndex = idx
    , vdLevel = lv
    , vdReason = reason
    , vdOnUnassigned = onUnassigned
    }

newLitData :: IO LitData
newLitData = do
  ws <- newIORef []
  occ <- newIORef HashSet.empty
  return $ LitData ws occ

varData :: Solver -> Var -> IO VarData
varData solver !v = Vec.unsafeRead (svVarData solver) (v-1)

litData :: Solver -> Lit -> IO LitData
litData solver !l =
  -- litVar による heap allocation を避けるために、
  -- litPolarityによる分岐後にvarDataを呼ぶ。
  if litPolarity l then do
    vd <- varData solver l
    return $ vdPosLitData vd
  else do
    vd <- varData solver (negate l)
    return $ vdNegLitData vd

{-# INLINE varValue #-}
varValue :: Solver -> Var -> IO LBool
varValue solver !v = do
  vd <- varData solver v
  readIORef (vdValue vd)

{-# INLINE litValue #-}
litValue :: Solver -> Lit -> IO LBool
litValue solver !l = do
  -- litVar による heap allocation を避けるために、
  -- litPolarityによる分岐後にvarDataを呼ぶ。
  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
  vd <- varData solver v
  lv <- readIOURef (vdLevel vd)
  if lv == levelRoot then
    readIORef (vdValue vd)
  else
    return lUndef

getLitFixed :: Solver -> Var -> IO LBool
getLitFixed solver !l = do
  -- litVar による heap allocation を避けるために、
  -- litPolarityによる分岐後にvarDataを呼ぶ。
  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

varLevel :: Solver -> Var -> IO Level
varLevel solver !v = do
  vd <- varData solver v
  val <- readIORef (vdValue vd)
  when (val == lUndef) $ error ("ToySolver.SAT.varLevel: unassigned var " ++ show v)
  readIOURef (vdLevel vd)

litLevel :: Solver -> Lit -> IO Level
litLevel solver l = varLevel solver (litVar l)

varReason :: Solver -> Var -> IO (Maybe SomeConstraintHandler)
varReason solver !v = do
  vd <- varData solver v
  val <- readIORef (vdValue vd)
  when (val == lUndef) $ error ("ToySolver.SAT.varReason: unassigned var " ++ show v)
  readIORef (vdReason vd)

varAssignNo :: Solver -> Var -> IO Int
varAssignNo solver !v = do
  vd <- varData solver v
  val <- readIORef (vdValue vd)
  when (val == lUndef) $ error ("ToySolver.SAT.varAssignNo: unassigned var " ++ show v)
  readIOURef (vdTrailIndex vd)

-- | Solver instance
data Solver
  = Solver
  { svOk           :: !(IORef Bool)

  , svVarQueue     :: !PQ.PriorityQueue
  , svTrail        :: !(Vec.UVec Lit)
  , svTrailLimit   :: !(Vec.UVec Lit)
  , svTrailNPropagated :: !(IOURef Int)

  , svVarData      :: !(Vec.Vec VarData)
  , svConstrDB     :: !(IORef [SomeConstraintHandler])
  , svLearntDB     :: !(IORef (Int,[SomeConstraintHandler]))

  -- Theory
  , svTheorySolver  :: !(IORef (Maybe TheorySolver))
  , svTheoryChecked :: !(IOURef Int)

  -- Result
  , svModel        :: !(IORef (Maybe Model))
  , svFailedAssumptions :: !(IORef [Lit])

  -- Statistics
  , svNDecision    :: !(IOURef Int)
  , svNRandomDecision :: !(IOURef Int)
  , svNConflict    :: !(IOURef Int)
  , svNRestart     :: !(IOURef Int)
  , svNLearntGC    :: !(IOURef Int)
  , svNRemovedConstr :: !(IOURef Int)

  -- Configulation

  -- | Inverse of the variable activity decay factor. (default 1 / 0.95)
  , svVarDecay     :: !(IOURef Double)

  -- | Amount to bump next variable with.
  , svVarInc       :: !(IOURef Double)

  -- | Inverse of the constraint activity decay factor. (1 / 0.999)
  , svConstrDecay  :: !(IOURef Double)

  -- | Amount to bump next constraint with.
  , svConstrInc    :: !(IOURef Double)

  , svRestartStrategy :: !(IORef RestartStrategy)

  -- | The initial restart limit. (default 100)
  , svRestartFirst :: !(IORef Int)

  -- | The factor with which the restart limit is multiplied in each restart. (default 1.5)
  , svRestartInc :: !(IORef Double)

  -- | The initial limit for learnt constraints.
  , svLearntSizeFirst :: !(IORef Int)

  -- | The limit for learnt constraints is multiplied with this factor periodically. (default 1.1)
  , svLearntSizeInc :: !(IORef Double)

  -- | Controls conflict constraint minimization (0=none, 1=local, 2=recursive)
  , svCCMin :: !(IORef Int)

  , svEnablePhaseSaving :: !(IORef Bool)
  , svEnableForwardSubsumptionRemoval :: !(IORef Bool)

  , svLearningStrategy :: !(IORef LearningStrategy)

  , svPBHandlerType :: !(IORef PBHandlerType)
  , svPBSplitClausePart :: !(IORef Bool)

  , svEnableBackwardSubsumptionRemoval :: !(IORef Bool)

  , svCheckModel :: !(IORef Bool)

  , svRandomFreq :: !(IORef Double)

  , svRandomGen  :: !(IORef Rand.StdGen)

  , svConfBudget :: !(IOURef Int)

  -- Logging
  , svLogger :: !(IORef (Maybe (String -> IO ())))
  , svStartWC    :: !(IORef UTCTime)
  , svLastStatWC :: !(IORef UTCTime)

  -- Working spaces
  , svAssumptions     :: !(Vec.UVec Lit)
  , svLearntLim       :: !(IORef Int)
  , svLearntLimAdjCnt :: !(IORef Int)
  , svLearntLimSeq    :: !(IORef [(Int,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
  vd <- varData solver (litVar lit)
  let val = liftBool (litPolarity lit)

  val0 <- readIORef (vdValue vd)
  if val0 /= lUndef then do    
    return $ val == val0
  else do
    idx <- Vec.getSize (svTrail solver)
    lv <- getDecisionLevel solver

    writeIORef (vdValue vd) val
    writeIOURef (vdTrailIndex vd) idx
    writeIOURef (vdLevel vd) lv
    writeIORef (vdReason vd) reason

    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
  vd <- varData solver v
  val <- readIORef (vdValue vd)
  when (val == lUndef) $ error "unassign: should not happen"

  flag <- getEnablePhaseSaving solver
  when flag $ writeIORef (vdPolarity vd) $! fromJust (unliftBool val)

  writeIORef (vdValue vd) lUndef
  writeIOURef (vdTrailIndex vd) maxBound
  writeIOURef (vdLevel vd) maxBound
  writeIORef (vdReason vd) Nothing

  let !l = if val == lTrue then v else -v
  cs <- readIORef (vdOnUnassigned vd)
  writeIORef (vdOnUnassigned vd) []
  forM_ cs $ \c ->
    constrOnUnassigned solver c c l

  PQ.enqueue (svVarQueue solver) v

addOnUnassigned :: Solver -> SomeConstraintHandler -> Lit -> IO ()
addOnUnassigned solver constr !l = do
  vd <- varData solver (litVar l)
  val <- readIORef (vdValue vd)
  when (val == lUndef) $ error "addOnUnassigned: should not happen"
  modifyIORef (vdOnUnassigned vd) (constr :)

-- | Register the constraint to be notified when the literal becames false.
watchLit :: Solver -> Lit -> SomeConstraintHandler -> IO ()
watchLit solver !lit c = do
  ld <- litData solver lit
  modifyIORef (ldWatches ld) (c : )

-- | Register the constraint to be notified when the variable is assigned.
watchVar :: Solver -> Var -> SomeConstraintHandler -> IO ()
watchVar solver !var c = do
  vd <- varData solver var
  modifyIORef (vdWatches vd) (c : )

unwatchLit :: Solver -> Lit -> SomeConstraintHandler -> IO ()
unwatchLit solver !lit c = do
  ld <- litData solver lit
  modifyIORef (ldWatches ld) (delete c)

unwatchVar :: Solver -> Lit -> SomeConstraintHandler -> IO ()
unwatchVar solver !lit c = do
  vd <- varData solver lit
  modifyIORef (vdWatches vd) (delete c)

-- | Returns list of constraints that are watching the literal.
watches :: Solver -> Lit -> IO [SomeConstraintHandler]
watches solver !lit = do
  ld <- litData solver lit
  readIORef (ldWatches ld)

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
       ld <- litData solver lit
       modifyIORef' (ldOccurList ld) (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 = do
  vd <- varData solver v
  readIOURef (vdActivity vd)

varDecayActivity :: Solver -> IO ()
varDecayActivity solver = do
  d <- readIOURef (svVarDecay solver)
  modifyIOURef (svVarInc solver) (d*)

varBumpActivity :: Solver -> Var -> IO ()
varBumpActivity solver !v = do
  inc <- readIOURef (svVarInc solver)
  vd <- varData solver v
  modifyIOURef (vdActivity vd) (+inc)
  PQ.update (svVarQueue solver) v
  aval <- readIOURef (vdActivity vd)
  when (aval > 1e20) $
    -- Rescale
    varRescaleAllActivity solver

varRescaleAllActivity :: Solver -> IO ()
varRescaleAllActivity solver = do
  vs <- variables solver
  forM_ vs $ \v -> do
    vd <- varData solver v
    modifyIOURef (vdActivity vd) (* 1e-20)
  modifyIOURef (svVarInc solver) (* 1e-20)

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 (svVarData solver)

{-# DEPRECATED nVars "Use getNVars instead" #-}
-- | number of variables of the problem.
nVars :: Solver -> IO Int
nVars = getNVars

-- | number of assigned 
getNAssigned :: Solver -> IO Int
getNAssigned solver = Vec.getSize (svTrail solver)

{-# DEPRECATED nAssigns "nAssigns is deprecated" #-}
-- | number of assigned variables.
nAssigns :: Solver -> IO Int
nAssigns = getNAssigned

-- | number of constraints.
getNConstraints :: Solver -> IO Int
getNConstraints solver = do
  xs <- readIORef (svConstrDB solver)
  return $ length xs

{-# DEPRECATED nConstraints "Use getNConstraints instead" #-}
-- | number of constraints.
nConstraints :: Solver -> IO Int
nConstraints = getNConstraints

-- | number of learnt constrints.
getNLearntConstraints :: Solver -> IO Int
getNLearntConstraints solver = do
  (n,_) <- readIORef (svLearntDB solver)
  return n

{-# DEPRECATED nLearnt "Use getNLearntConstraints instead" #-}
-- | number of learnt constrints.
nLearnt :: Solver -> IO Int
nLearnt = getNLearntConstraints

learntConstraints :: Solver -> IO [SomeConstraintHandler]
learntConstraints solver = do
  (_,cs) <- readIORef (svLearntDB solver)
  return cs

{--------------------------------------------------------------------
  Solver
--------------------------------------------------------------------}

-- | Create a new Solver instance.
newSolver :: IO Solver
newSolver = do
 rec
  ok   <- newIORef True
  trail <- Vec.new
  trail_lim <- Vec.new
  trail_nprop <- newIOURef 0
  vars <- Vec.new
  vqueue <- PQ.newPriorityQueueBy (ltVar solver)
  db  <- newIORef []
  db2 <- newIORef (0,[])
  as  <- Vec.new
  m   <- newIORef Nothing
  ndecision <- newIOURef 0
  nranddec  <- newIOURef 0
  nconflict <- newIOURef 0
  nrestart  <- newIOURef 0
  nlearntgc <- newIOURef 0
  nremoved  <- newIOURef 0

  constrDecay <- newIOURef (1 / 0.999)
  constrInc   <- newIOURef 1
  varDecay <- newIOURef (1 / 0.95)
  varInc   <- newIOURef 1
  restartStrat <- newIORef defaultRestartStrategy
  restartFirst <- newIORef defaultRestartFirst
  restartInc <- newIORef defaultRestartInc
  learning <- newIORef defaultLearningStrategy
  learntSizeFirst <- newIORef defaultLearntSizeFirst
  learntSizeInc <- newIORef defaultLearntSizeInc
  ccMin <- newIORef defaultCCMin
  checkModel <- newIORef False
  pbHandlerType <- newIORef defaultPBHandlerType
  pbSplitClausePart <- newIORef defaultPBSplitClausePart
  enablePhaseSaving <- newIORef defaultEnablePhaseSaving
  enableForwardSubsumptionRemoval <- newIORef defaultEnableForwardSubsumptionRemoval
  enableBackwardSubsumptionRemoval <- newIORef defaultEnableBackwardSubsumptionRemoval

  learntLim       <- newIORef undefined
  learntLimAdjCnt <- newIORef (-1)
  learntLimSeq    <- newIORef undefined

  logger <- newIORef Nothing
  startWC    <- newIORef undefined
  lastStatWC <- newIORef undefined

  randfreq <- newIORef defaultRandomFreq
  randgen  <- newIORef =<< Rand.newStdGen

  failed <- newIORef []

  confBudget <- newIOURef (-1)

  tsolver <- newIORef Nothing
  tchecked <- newIOURef 0

  let solver =
        Solver
        { svOk = ok
        , svVarQueue   = vqueue
        , svTrail      = trail
        , svTrailLimit = trail_lim
        , svTrailNPropagated = trail_nprop
        , svVarData    = vars
        , svConstrDB   = db
        , svLearntDB   = db2

        -- Theory
        , svTheorySolver  = tsolver
        , svTheoryChecked = tchecked

        -- Result
        , svModel      = m
        , svFailedAssumptions = failed

        -- Statistics        
        , svNDecision  = ndecision
        , svNRandomDecision = nranddec
        , svNConflict  = nconflict
        , svNRestart   = nrestart
        , svNLearntGC  = nlearntgc
        , svNRemovedConstr = nremoved

        -- Configulation
        , svVarDecay    = varDecay
        , svVarInc      = varInc
        , svConstrDecay = constrDecay
        , svConstrInc   = constrInc
        , svRestartStrategy = restartStrat
        , svRestartFirst = restartFirst
        , svRestartInc   = restartInc
        , svLearningStrategy = learning
        , svLearntSizeFirst = learntSizeFirst
        , svLearntSizeInc = learntSizeInc
        , svCCMin = ccMin
        , svEnablePhaseSaving = enablePhaseSaving
        , svEnableForwardSubsumptionRemoval = enableForwardSubsumptionRemoval
        , svPBHandlerType   = pbHandlerType
        , svPBSplitClausePart = pbSplitClausePart
        , svEnableBackwardSubsumptionRemoval = enableBackwardSubsumptionRemoval
        , svCheckModel = checkModel
        , svRandomFreq = randfreq
        , svRandomGen  = randgen
        , svConfBudget = confBudget

        -- Logging
        , svLogger = logger
        , svStartWC    = startWC
        , svLastStatWC = lastStatWC

        -- Working space
        , svAssumptions     = as
        , svLearntLim       = learntLim
        , svLearntLimAdjCnt = learntLimAdjCnt
        , svLearntLimSeq    = learntLimSeq
        }
 return solver

ltVar :: Solver -> Var -> Var -> IO Bool
ltVar solver v1 v2 = do
  a1 <- varActivity solver v1
  a2 <- varActivity solver v2
  return $! a1 > a2

{--------------------------------------------------------------------
  Problem specification
--------------------------------------------------------------------}

-- |Add a new variable
newVar :: Solver -> IO Var
newVar solver = do
  n <- Vec.getSize (svVarData solver)
  let v = n + 1
  vd <- newVarData
  Vec.push (svVarData solver) vd
  PQ.enqueue (svVarQueue solver) v
  return v

-- |Add variables. @newVars solver n = replicateM n (newVar solver)@
newVars :: Solver -> Int -> IO [Var]
newVars solver n = do
  nv <- getNVars solver
  resizeVarCapacity solver (nv+n)
  replicateM n (newVar solver)

-- |Add variables. @newVars_ solver n = newVars solver n >> return ()@
newVars_ :: Solver -> Int -> IO ()
newVars_ solver n = do
  nv <- getNVars solver
  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 (svVarData solver) n
  PQ.resizeHeapCapacity (svVarQueue solver) n
  PQ.resizeTableCapacity (svVarQueue solver) (n+1)

-- |Add a clause to the solver.
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 ()

-- | Add a cardinality constraints /atleast({l1,l2,..},n)/.
addAtLeast :: Solver -- ^ The 'Solver' argument.
           -> [Lit]  -- ^ set of literals /{l1,l2,..}/ (duplicated elements are ignored)
           -> Int    -- ^ /n/.
           -> 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 ()

-- | Add a cardinality constraints /atmost({l1,l2,..},n)/.
addAtMost :: Solver -- ^ The 'Solver' argument
          -> [Lit]  -- ^ set of literals /{l1,l2,..}/ (duplicated elements are ignored)
          -> Int    -- ^ /n/
          -> IO ()
addAtMost solver lits n =
  addAtLeast solver (map litNot lits) (length lits - n)

-- | Add a cardinality constraints /exactly({l1,l2,..},n)/.
addExactly :: Solver -- ^ The 'Solver' argument
           -> [Lit]  -- ^ set of literals /{l1,l2,..}/ (duplicated elements are ignored)
           -> Int    -- ^ /n/
           -> IO ()
addExactly solver lits n = do
  addAtLeast solver lits n
  addAtMost solver lits n

-- | Add a pseudo boolean constraints /c1*l1 + c2*l2 + … ≥ n/.
addPBAtLeast :: Solver          -- ^ The 'Solver' argument.
             -> [(Integer,Lit)] -- ^ set of terms @[(c1,l1),(c2,l2),…]@
             -> Integer         -- ^ /n/
             -> 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 <- getPBSplitClausePart 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

-- | See documentation of 'setPBSplitClausePart'.
pbSplitClausePart :: Solver -> ([(Integer,Lit)], Integer) -> IO ([(Integer,Lit)], Integer)
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)

-- | Add a pseudo boolean constraints /c1*l1 + c2*l2 + … ≤ n/.
addPBAtMost :: Solver          -- ^ The 'Solver' argument.
            -> [(Integer,Lit)] -- ^ list of @[(c1,l1),(c2,l2),…]@
            -> Integer         -- ^ /n/
            -> IO ()
addPBAtMost solver ts n = addPBAtLeast solver [(-c,l) | (c,l) <- ts] (negate n)

-- | Add a pseudo boolean constraints /c1*l1 + c2*l2 + … = n/.
addPBExactly :: Solver          -- ^ The 'Solver' argument.
             -> [(Integer,Lit)] -- ^ list of terms @[(c1,l1),(c2,l2),…]@
             -> Integer         -- ^ /n/
             -> IO ()
addPBExactly solver ts n = do
  (ts2,n2) <- liftM normalizePBLinExactly $ instantiatePBLinExactly (getLitFixed solver) (ts,n)
  addPBAtLeast solver ts2 n2
  addPBAtMost solver ts2 n2

-- | Add a soft pseudo boolean constraints /sel ⇒ c1*l1 + c2*l2 + … ≥ n/.
addPBAtLeastSoft
  :: Solver          -- ^ The 'Solver' argument.
  -> Lit             -- ^ Selector literal @sel@
  -> [(Integer,Lit)] -- ^ set of terms @[(c1,l1),(c2,l2),…]@
  -> Integer         -- ^ /n/
  -> IO ()
addPBAtLeastSoft solver sel lhs rhs = do
  (lhs', rhs') <- liftM normalizePBLinAtLeast $ instantiatePBLinAtLeast (getLitFixed solver) (lhs,rhs)
  addPBAtLeast solver ((rhs', litNot sel) : lhs') rhs'

-- | Add a soft pseudo boolean constraints /sel ⇒ c1*l1 + c2*l2 + … ≤ n/.
addPBAtMostSoft
  :: Solver          -- ^ The 'Solver' argument.
  -> Lit             -- ^ Selector literal @sel@
  -> [(Integer,Lit)] -- ^ set of terms @[(c1,l1),(c2,l2),…]@
  -> Integer         -- ^ /n/
  -> IO ()
addPBAtMostSoft solver sel lhs rhs =
  addPBAtLeastSoft solver sel [(negate c, lit) | (c,lit) <- lhs] (negate rhs)

-- | Add a soft pseudo boolean constraints /sel ⇒ c1*l1 + c2*l2 + … = n/.
addPBExactlySoft
  :: Solver          -- ^ The 'Solver' argument.
  -> Lit             -- ^ Selector literal @sel@
  -> [(Integer,Lit)] -- ^ set of terms @[(c1,l1),(c2,l2),…]@
  -> Integer         -- ^ /n/
  -> 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

-- | Add a parity constraint /l1 ⊕ l2 ⊕ … ⊕ ln = rhs/
addXORClause
  :: Solver -- ^ The 'Solver' argument.
  -> [Lit]  -- ^ literals @[l1, l2, …, ln]@
  -> Bool   -- ^ /rhs/
  -> 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 ()

-- | Add a soft parity constraint /sel ⇒ l1 ⊕ l2 ⊕ … ⊕ ln = rhs/
addXORClauseSoft
  :: Solver -- ^ The 'Solver' argument.
  -> Lit    -- ^ Selector literal @sel@
  -> [Lit]  -- ^ literals @[l1, l2, …, ln]@
  -> Bool   -- ^ /rhs/
  -> IO ()
addXORClauseSoft solver sel lits rhs = do
  reified <- newVar solver
  addXORClause solver (litNot reified : lits) rhs
  addClause solver [litNot sel, reified] -- sel ⇒ reified

{--------------------------------------------------------------------
  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
  log solver "Solving starts ..."
  resetStat solver
  writeIORef (svModel solver) Nothing
  writeIORef (svFailedAssumptions solver) []

  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

    restartStrategy <- readIORef (svRestartStrategy solver)
    restartFirst  <- readIORef (svRestartFirst solver)
    restartInc    <- readIORef (svRestartInc solver)
    let restartSeq =
          if restartFirst > 0
          then mkRestartSeq restartStrategy restartFirst restartInc
          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
      learntSizeFirst <- readIORef (svLearntSizeFirst solver)
      learntSizeInc   <- readIORef (svLearntSizeInc solver)
      nc <- getNConstraints solver
      let initialLearntLim = if learntSizeFirst > 0 then learntSizeFirst else max ((nc + nv) `div` 3) 16
          learntSizeSeq    = iterate (ceiling . (learntSizeInc*) . fromIntegral) initialLearntLim
          learntSizeAdjSeq = iterate (\x -> (x * 3) `div` 2) (100::Int)
      writeIORef (svLearntLimSeq solver) (zip learntSizeSeq learntSizeAdjSeq)
      learntSizeAdj

    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 $ Just x
            SRBudgetExceeded -> return Nothing
            SRRestart -> do
              modifyIOURef (svNRestart solver) (+1)
              backtrackTo solver levelRoot
              loop rs

    printStatHeader solver

    startCPU <- getCPUTime
    startWC  <- getCurrentTime
    writeIORef (svStartWC solver) startWC
    result <- loop restartSeq
    endCPU <- getCPUTime
    endWC  <- getCurrentTime

    when (result == Just True) $ do
      checkModel <- readIORef (svCheckModel solver)
      when checkModel $ checkSatisfied solver
      constructModel solver

    backtrackTo solver levelRoot

    when debugMode $ dumpVarActivity solver
    when debugMode $ dumpConstrActivity solver
    printStat solver True
    (log solver . printf "#cpu_time = %.3fs") (fromIntegral (endCPU - startCPU) / 10^(12::Int) :: Double)
    (log solver . printf "#wall_clock_time = %.3fs") (realToFrac (endWC `diffUTCTime` startWC) :: Double)
    (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
      Just x  -> return x
      Nothing -> throw BudgetExceeded

data BudgetExceeded = BudgetExceeded
  deriving (Show, Typeable)

instance Exception BudgetExceeded

data SearchResult
  = SRFinished Bool
  | SRRestart
  | SRBudgetExceeded

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) core
                  return Nothing
                else
                  return (Just l)
      go

    handleConflict :: IORef Int -> SomeConstraintHandler -> IO (Maybe SearchResult)
    handleConflict conflictCounter constr = do
      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)

      when (c `mod` 100 == 0) $ do
        printStat solver False

      if d == levelRoot then do
        markBad solver
        return $ Just (SRFinished False)
      else if confBudget==0 then
        return $ Just SRBudgetExceeded
      else if conflict_lim > 0 && c >= conflict_lim then
        return $ Just SRRestart
      else do
        strat <- readIORef (svLearningStrategy solver)
        case strat 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 constr = toConstraintHandler cl
          addToLearntDB solver constr
          basicAttachClauseHandler solver cl
          assignBy solver lit constr
          constrBumpActivity solver constr

    learnHybrid :: IORef Int -> SomeConstraintHandler -> IO (Maybe SearchResult)
    learnHybrid conflictCounter constr = do
      ((learntClause, clauseLevel), (pb, pbLevel)) <- analyzeConflictHybrid solver constr
      let minLevel = 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 constr = toConstraintHandler cl
          addToLearntDB solver constr
          basicAttachClauseHandler solver cl
          constrBumpActivity solver constr
          when (minLevel == clauseLevel) $ do
            _ <- assignBy solver lit constr -- 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
          let (lhs,rhs) = pb
          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

-- | 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 [Lit]
getFailedAssumptions solver = readIORef (svFailedAssumptions 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 <- getEnableForwardSubsumptionRemoval solver
  if not flag then
    return False
  else do
    withEnablePhaseSaving solver 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 solver flag m =
      bracket
        (getEnablePhaseSaving solver)
        (setEnablePhaseSaving solver)
        (\_ -> setEnablePhaseSaving solver flag >> m)

removeBackwardSubsumedBy :: Solver -> PBLinAtLeast -> IO ()
removeBackwardSubsumedBy solver pb = do
  flag <- getEnableBackwardSubsumptionRemoval 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
    ld <- litData solver lit
    readIORef (ldOccurList ld)
  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 $ pbSubsume 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.
--------------------------------------------------------------------}

setRestartStrategy :: Solver -> RestartStrategy -> IO ()
setRestartStrategy solver s = writeIORef (svRestartStrategy solver) s

-- | default value for @RestartStrategy@.
defaultRestartStrategy :: RestartStrategy
defaultRestartStrategy = MiniSATRestarts

-- | The initial restart limit. (default 100)
-- Zero and negative values are used to disable restart.
setRestartFirst :: Solver -> Int -> IO ()
setRestartFirst solver !n = writeIORef (svRestartFirst solver) n

-- | default value for @RestartFirst@.
defaultRestartFirst :: Int
defaultRestartFirst = 100

-- | The factor with which the restart limit is multiplied in each restart. (default 1.5)
-- 
-- This must be @>1@.
setRestartInc :: Solver -> Double -> IO ()
setRestartInc solver !r
  | r > 1 = writeIORef (svRestartInc solver) r
  | otherwise = error "setRestartInc: RestartInc must be >1"

-- | default value for @RestartInc@.
defaultRestartInc :: Double
defaultRestartInc = 1.5

data LearningStrategy
  = LearningClause
  | LearningHybrid
  deriving (Show, Eq, Ord, Enum, Bounded)

setLearningStrategy :: Solver -> LearningStrategy -> IO ()
setLearningStrategy solver l = writeIORef (svLearningStrategy solver) $! l

defaultLearningStrategy :: LearningStrategy
defaultLearningStrategy = LearningClause

-- | The initial limit for learnt clauses.
-- 
-- Negative value means computing default value from problem instance.
setLearntSizeFirst :: Solver -> Int -> IO ()
setLearntSizeFirst solver !x = writeIORef (svLearntSizeFirst solver) x

-- | default value for @LearntSizeFirst@.
defaultLearntSizeFirst :: Int
defaultLearntSizeFirst = -1

-- | The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)
-- 
-- This must be @>1@.
setLearntSizeInc :: Solver -> Double -> IO ()
setLearntSizeInc solver !r
  | r > 1 = writeIORef (svLearntSizeInc solver) r
  | otherwise = error "setLearntSizeInc: LearntSizeInc must be >1"

-- | default value for @LearntSizeInc@.
defaultLearntSizeInc :: Double
defaultLearntSizeInc = 1.1

-- | Controls conflict clause minimization (0=none, 1=basic, 2=deep)
setCCMin :: Solver -> Int -> IO ()
setCCMin solver !v = writeIORef (svCCMin solver) v

-- | default value for @CCMin@.
defaultCCMin :: Int
defaultCCMin = 2

-- | The default polarity of a variable.
setVarPolarity :: Solver -> Var -> Bool -> IO ()
setVarPolarity solver v val = do
  vd <- varData solver v
  writeIORef (vdPolarity vd) val

setCheckModel :: Solver -> Bool -> IO ()
setCheckModel solver flag = do
  writeIORef (svCheckModel solver) flag

-- | The frequency with which the decision heuristic tries to choose a random variable
setRandomFreq :: Solver -> Double -> IO ()
setRandomFreq solver r = do
  writeIORef (svRandomFreq solver) r

defaultRandomFreq :: Double
defaultRandomFreq = 0.005

-- | Set random generator used by the random variable selection
setRandomGen :: Solver -> Rand.StdGen -> IO ()
setRandomGen solver = writeIORef (svRandomGen solver)

-- | Get random generator used by the random variable selection
getRandomGen :: Solver -> IO Rand.StdGen
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)

data PBHandlerType = PBHandlerTypeCounter | PBHandlerTypePueblo
  deriving (Show, Eq, Ord, Enum, Bounded)

defaultPBHandlerType :: PBHandlerType
defaultPBHandlerType = PBHandlerTypeCounter

setPBHandlerType :: Solver -> PBHandlerType -> IO ()
setPBHandlerType solver ht = do
  writeIORef (svPBHandlerType solver) ht

-- | Split PB-constraints into a PB part and a clause part.
--
-- Example from minisat+ paper:
--
-- * 4 x1 + 4 x2 + 4 x3 + 4 x4 + 2y1 + y2 + y3 ≥ 4
-- 
-- would be split into
--
-- * x1 + x2 + x3 + x4 + ¬z ≥ 1 (clause part)
--
-- * 2 y1 + y2 + y3 + 4 z ≥ 4 (PB part)
--
-- where z is a newly introduced variable, not present in any other constraint.
-- 
-- Reference:
-- 
-- * N . Eéen and N. Sörensson. Translating Pseudo-Boolean Constraints into SAT. JSAT 2:1–26, 2006.
-- 
setPBSplitClausePart :: Solver -> Bool -> IO ()
setPBSplitClausePart solver b =
  writeIORef (svPBSplitClausePart solver) b

-- | See documentation of 'setPBSplitClausePart'.
getPBSplitClausePart :: Solver -> IO Bool
getPBSplitClausePart solver = readIORef (svPBSplitClausePart solver)

-- | See documentation of 'setPBSplitClausePart'.
defaultPBSplitClausePart :: Bool
defaultPBSplitClausePart = False

setEnablePhaseSaving :: Solver -> Bool -> IO ()
setEnablePhaseSaving solver flag = do
  writeIORef (svEnablePhaseSaving solver) flag

getEnablePhaseSaving :: Solver -> IO Bool
getEnablePhaseSaving solver = do
  readIORef (svEnablePhaseSaving solver)

defaultEnablePhaseSaving :: Bool
defaultEnablePhaseSaving = True

setEnableForwardSubsumptionRemoval :: Solver -> Bool -> IO ()
setEnableForwardSubsumptionRemoval solver flag = do
  writeIORef (svEnableForwardSubsumptionRemoval solver) flag

getEnableForwardSubsumptionRemoval :: Solver -> IO Bool
getEnableForwardSubsumptionRemoval solver = do
  readIORef (svEnableForwardSubsumptionRemoval solver)

defaultEnableForwardSubsumptionRemoval :: Bool
defaultEnableForwardSubsumptionRemoval = False

setEnableBackwardSubsumptionRemoval :: Solver -> Bool -> IO ()
setEnableBackwardSubsumptionRemoval solver flag = do
  writeIORef (svEnableBackwardSubsumptionRemoval solver) flag

getEnableBackwardSubsumptionRemoval :: Solver -> IO Bool
getEnableBackwardSubsumptionRemoval solver = do
  readIORef (svEnableBackwardSubsumptionRemoval solver)

defaultEnableBackwardSubsumptionRemoval :: Bool
defaultEnableBackwardSubsumptionRemoval = False

{--------------------------------------------------------------------
  API for implementation of @solve@
--------------------------------------------------------------------}

pickBranchLit :: Solver -> IO Lit
pickBranchLit !solver = do
  let vqueue = svVarQueue solver

  -- Random decision
  let withRandGen :: (Rand.StdGen -> (a, Rand.StdGen)) -> IO a
      withRandGen f = do
        randgen  <- readIORef (svRandomGen solver)
        let (r, randgen') = f randgen
        writeIORef (svRandomGen solver) randgen'
        return r
  !randfreq <- readIORef (svRandomFreq solver)
  !size <- PQ.queueSize vqueue
  !r <- withRandGen Rand.random
  var <-
    if (r < randfreq && size >= 2) then do
      a <- PQ.getHeapArray vqueue
      i <- withRandGen $ Rand.randomR (0, size-1)
      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
    vd <- varData solver var2
    -- TODO: random polarity
    p <- readIORef (vdPolarity vd)
    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 = do
  m <- deduceB solver
  case m of
    Just _ -> return m
    Nothing -> do
      m2 <- deduceT solver
      case m2 of
        Just _ -> return m2
        Nothing -> do
          empty <- bcpIsEmpty solver
          if empty then
            return Nothing
          else
            deduce solver

deduceB :: Solver -> IO (Maybe SomeConstraintHandler)
deduceB solver = loop
  where
    loop :: IO (Maybe SomeConstraintHandler)
    loop = do
      r <- bcpDequeue solver
      case r of
        Nothing -> return Nothing
        Just lit -> do
          ret <- processLit lit
          case ret of
            Just _ -> return ret
            Nothing -> do
              ret <- processVar (litVar lit)
              case ret of
                Just _ -> return ret
                Nothing -> loop

    processLit :: Lit -> IO (Maybe SomeConstraintHandler)
    processLit !lit = do
      let falsifiedLit = litNot lit
      ld <- litData solver falsifiedLit
      let wsref = ldWatches ld
      let loop2 [] = return Nothing
          loop2 (w:ws) = do
            ok <- propagate solver w falsifiedLit
            if ok then
              loop2 ws
            else do
              modifyIORef wsref (++ws)
              return (Just w)
      ws <- readIORef wsref
      writeIORef wsref []
      loop2 ws

    processVar :: Lit -> IO (Maybe SomeConstraintHandler)
    processVar !lit = do
      let falsifiedLit = litNot lit
      vd <- varData solver (litVar lit)
      let wsref = vdWatches vd
      let loop2 [] = return Nothing
          loop2 (w:ws) = do
            ok <- propagate solver w falsifiedLit
            if ok
              then loop2 ws
              else do
                modifyIORef wsref (++ws)
                return (Just w)
      ws <- readIORef wsref
      writeIORef wsref []
      loop2 ws

analyzeConflict :: ConstraintHandler c => Solver -> c -> IO (Clause, Level)
analyzeConflict solver constr = do
  d <- getDecisionLevel solver

  let split :: [Lit] -> IO (LitSet, LitSet)
      split = go (IS.empty, IS.empty)
        where
          go (xs,ys) [] = return (xs,ys)
          go (xs,ys) (l:ls) = do
            lv <- litLevel solver l
            if lv == levelRoot then
              go (xs,ys) ls
            else if lv >= d then
              go (IS.insert l xs, ys) ls
            else
              go (xs, IS.insert l ys) ls

  let loop :: LitSet -> LitSet -> IO LitSet
      loop lits1 lits2
        | sz==1 = do
            return $ lits1 `IS.union` lits2
        | sz>=2 = do
            l <- peekTrail solver
            if litNot l `IS.notMember` lits1 then do
              popTrail solver
              loop lits1 lits2
            else do
              m <- varReason solver (litVar l)
              case m of
                Nothing -> error "analyzeConflict: should not happen"
                Just constr2 -> do
                  constrBumpActivity solver constr2
                  xs <- reasonOf solver constr2 (Just l)
                  forM_ xs $ \lit -> varBumpActivity solver (litVar lit)
                  popTrail solver
                  (ys,zs) <- split xs
                  loop (IS.delete (litNot l) lits1 `IS.union` ys)
                       (lits2 `IS.union` zs)
        | otherwise = error "analyzeConflict: should not happen: reason of current level is empty"
        where
          sz = IS.size lits1

  constrBumpActivity solver constr
  conflictClause <- reasonOf solver constr Nothing
  forM_ conflictClause $ \lit -> varBumpActivity solver (litVar lit)
  (ys,zs) <- split conflictClause
  lits <- loop ys zs

  lits2 <- minimizeConflictClause solver lits

  xs <- liftM (sortBy (flip (comparing snd))) $
    forM (IS.toList lits2) $ \l -> do
      lv <- litLevel solver l
      return (l,lv)

  let level = case xs of
                [] -> error "analyzeConflict: should not happen"
                [_] -> levelRoot
                _:(_,lv):_ -> lv
  return (map fst xs, 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]

analyzeConflictHybrid :: ConstraintHandler c => Solver -> c -> IO ((Clause, Level), (PBLinAtLeast, Level))
analyzeConflictHybrid solver constr = do
  d <- getDecisionLevel solver

  let split :: [Lit] -> IO (LitSet, LitSet)
      split = go (IS.empty, IS.empty)
        where
          go (xs,ys) [] = return (xs,ys)
          go (xs,ys) (l:ls) = do
            lv <- litLevel solver l
            if lv == levelRoot then
              go (xs,ys) ls
            else if lv >= d then
              go (IS.insert l xs, ys) ls
            else
              go (xs, IS.insert l ys) ls

  let loop :: LitSet -> LitSet -> PBLinAtLeast -> IO (LitSet, PBLinAtLeast)
      loop lits1 lits2 pb
        | sz==1 = do
            return $ (lits1 `IS.union` lits2, pb)
        | sz>=2 = do
            l <- peekTrail solver
            m <- varReason solver (litVar l)
            case m of
              Nothing -> error "analyzeConflictHybrid: should not happen"
              Just constr2 -> do
                xs <- reasonOf solver constr2 (Just l)
                (lits1',lits2') <-
                  if litNot l `IS.notMember` lits1 then
                    return (lits1,lits2)
                  else do
                    constrBumpActivity solver constr2
                    forM_ xs $ \lit -> varBumpActivity solver (litVar lit)
                    (ys,zs) <- split xs
                    return  (IS.delete (litNot l) lits1 `IS.union` ys, lits2 `IS.union` zs)

                pb' <- if any (\(_,l2) -> litNot l == l2) (fst pb)
                       then do
                         pb2 <- do
                           b <- isPBRepresentable constr2
                           if not b then do
                             return $ clauseToPBLinAtLeast (l:xs)
                           else do
                             pb2 <- toPBLinAtLeast constr2
                             o <- pbOverSAT solver pb2
                             if o then
                               return $ clauseToPBLinAtLeast (l:xs)
                             else
                               return pb2
                         return $ cutResolve pb pb2 (litVar l)
                       else return pb

                popTrail solver
                loop lits1' lits2' pb'

        | otherwise = error "analyzeConflictHybrid: should not happen: reason of current level is empty"
        where
          sz = IS.size lits1

  constrBumpActivity solver constr
  conflictClause <- reasonOf solver constr Nothing
  pbConfl <- do
    b <- isPBRepresentable constr
    if b then
      toPBLinAtLeast constr
    else
      return (clauseToPBLinAtLeast conflictClause)
  forM_ conflictClause $ \lit -> varBumpActivity solver (litVar lit)
  (ys,zs) <- split conflictClause
  (lits, pb) <- loop ys zs pbConfl

  lits2 <- minimizeConflictClause solver lits

  xs <- liftM (sortBy (flip (comparing snd))) $
    forM (IS.toList lits2) $ \l -> do
      lv <- litLevel solver l
      return (l,lv)

  let level = case xs of
                [] -> error "analyzeConflict: should not happen"
                [_] -> levelRoot
                _:(_,lv):_ -> lv
  pblevel <- pbBacktrackLevel solver pb
  return ((map fst xs, level), (pb, pblevel))

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 $ \(_,lit) -> do
    val <- litValue solver lit
    if val /= lUndef then do
      level <- litLevel solver lit
      return $ IM.singleton level (IM.singleton lit val)
    else
      return $ IM.empty

  let replay [] _ _ = error "pbBacktrackLevel: should not happen"
      replay ((lv,lv_lits) : lvs) lhs slack = do
        let slack_lv = slack - sum [c | (c,lit) <- lhs, IM.lookup lit lv_lits == Just lFalse]
            lhs_lv   = [tm | tm@(_,lit) <- lhs, IM.notMember lit lv_lits]
        if slack_lv < 0 then
          return lv -- CONFLICT
        else if any (\(c,_) -> c > slack_lv) lhs_lv then
          return lv -- UNIT
        else
          replay lvs lhs_lv slack_lv

  let initial_slack = sum [c | (c,_) <- lhs] - rhs
  replay (IM.toList levelToLiterals) lhs initial_slack

minimizeConflictClause :: Solver -> LitSet -> IO LitSet
minimizeConflictClause solver lits = do
  ccmin <- readIORef (svCCMin 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

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
    vd <- varData solver v
    val <- readIORef (vdValue vd)
    writeArray marr v (fromJust (unliftBool val))
  m <- unsafeFreeze marr
  writeIORef (svModel solver) (Just m)

constrDecayActivity :: Solver -> IO ()
constrDecayActivity solver = do
  d <- readIOURef (svConstrDecay 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 <- getCurrentTime
  b <- if force
       then return True
       else do
         lastWC <- readIORef (svLastStatWC solver)
         return $ (nowWC `diffUTCTime` lastWC) > 1
  when b $ do
    startWC   <- readIORef (svStartWC solver)
    let tm = showTimeDiff $ nowWC `diffUTCTime` 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 :: NominalDiffTime -> String
showTimeDiff sec
  | 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 = realToFrac sec

    si :: Integer
    si = round s

    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
      ld <- litData solver lit
      modifyIORef' (ldOccurList ld) (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 -> IOUArray Int Lit -> 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 =<< unsafeRead 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# #)
#if __GLASGOW_HASKELL__ < 708
    go# i end w | i ># end = (# w, -1# #)
#else
    go# i end w | isTrue# (i ># end) = (# w, -1# #)
#endif
    go# i end w =
      case unIO (litValue solver =<< unsafeRead 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 -> IOUArray Int Lit -> 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 =<< unsafeRead 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# #)
#if __GLASGOW_HASKELL__ < 708
    go# i end w | i ># end = (# w, -1# #)
#else
    go# i end w | isTrue# (i ># end) = (# w, -1# #)
#endif
    go# i end w =
      case unIO (litValue solver =<< unsafeRead 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 :: !(IOUArray Int Lit)
  , claActivity :: !(IORef Double)
  , claHash :: !Int
  }

claGetSize :: ClauseHandler -> IO Int
claGetSize cla = do
  (lb,ub) <- getBounds (claLits cla)
  assert (lb == 0) $ return ()
  return $! ub-lb+1

instance Eq ClauseHandler where
  (==) = (==) `on` claLits

instance Hashable ClauseHandler where
  hash = claHash
  hashWithSalt = defaultHashWithSalt

newClauseHandler :: Clause -> Bool -> IO ClauseHandler
newClauseHandler ls learnt = do
  let size = length ls
  a <- newListArray (0, size-1) 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 <- getElems (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 <- unsafeRead (claLits this2) 0
      assignBy solver lit0 this
    else do
      ref <- newIORef 1
      let f i = do
            lit_i <- unsafeRead (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 <- unsafeRead (claLits this2) k
                  unsafeWrite (claLits this2) i lit_k
                  unsafeWrite (claLits this2) k lit_i
                  writeIORef ref $! (k+1)
                  return True

      b <- f 0
      if b then do
        lit0 <- unsafeRead (claLits this2) 0
        watchLit solver lit0 this
        b2 <- f 1
        if b2 then do
          lit1 <- unsafeRead (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 <- unsafeRead (claLits this2) l
            lv <- litLevel solver lit
            return (l,lv)
          lit1 <- unsafeRead (claLits this2) 1
          liti <- unsafeRead (claLits this2) i
          unsafeWrite (claLits this2) 1 liti
          unsafeWrite (claLits this2) i lit1
          watchLit solver liti this
          assignBy solver lit0 this -- should always succeed
      else do -- CONFLICT
        ls <- liftM (map fst . sortBy (flip (comparing snd))) $ forM [0..size-1] $ \l -> do
          lit <- unsafeRead (claLits this2) l
          lv <- litLevel solver lit
          return (l,lv)
        forM_ (zip [0..] ls) $ \(i,lit) -> do
          unsafeWrite (claLits this2) i lit
        lit0 <- unsafeRead (claLits this2) 0
        lit1 <- unsafeRead (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 <- unsafeRead (claLits this2) 0
      lit1 <- unsafeRead (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 <- unsafeRead (claLits this2) 0
      isReasonOf solver this lit

  constrPropagate !solver this this2 !falsifiedLit = do
    preprocess

    !lit0 <- unsafeRead 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 <- unsafeRead a 1
          !liti <- unsafeRead a i
          unsafeWrite a 1 liti
          unsafeWrite a i lit1
          watchLit solver liti this
          return True

    where
      a = claLits this2

      preprocess :: IO ()
      preprocess = do
        !l0 <- unsafeRead a 0
        !l1 <- unsafeRead a 1
        assert (l0==falsifiedLit || l1==falsifiedLit) $ return ()
        when (l0==falsifiedLit) $ do
          unsafeWrite a 0 l1
          unsafeWrite a 1 l0

  constrReasonOf _ this l = do
    lits <- getElems (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 <- getElems (claLits this)
    return ([(1,l) | l <- lits], 1)

  isSatisfied solver this = do
    lits <- getElems (claLits this)
    vals <- mapM (litValue solver) lits
    return $ lTrue `elem` vals

  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 <- getElems (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 :: IOUArray Int Lit
  , 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
  let size = length ls
  a <- newListArray (0, size-1) 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 <- getElems (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
    (lb,ub) <- getBounds a
    assert (lb == 0) $ return ()
    let m = ub - lb + 1
        n = atLeastNum this2

    if m < n then do
      markBad solver
      return False
    else if m == n then do
      let f i = do
            lit <- unsafeRead 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 ub
                if k /= -1 then do
                  -- NOT UNIT
                  lit_n <- unsafeRead a n
                  lit_k <- unsafeRead a k
                  unsafeWrite a n lit_k
                  unsafeWrite 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 <- unsafeRead 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..ub] $ \l -> do
                    lit <- unsafeRead 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 <- unsafeRead a n
                  lit_l <- unsafeRead a l
                  unsafeWrite a n lit_l
                  unsafeWrite 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 <- unsafeRead 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 ub
                  if k /= -1 then do
                    lit_k <- unsafeRead a k
                    unsafeWrite a i lit_k
                    unsafeWrite 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 (flip (comparing snd))) $ forM [i..ub] $ \l -> do
                         lit <- readArray 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..ub] xs) $ \(l,(lit,_lv)) -> do
                         writeArray a l lit
                    forLoop i (<=n) (+1) $ \l -> do
                      lit_l <- readArray 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 <- getElems (atLeastLits this2)
    let n = atLeastNum this2
    when (length lits > n) $ do
      forLoop 0 (<=n) (+1) $ \i -> do
        lit <- unsafeRead (atLeastLits this2) i
        unwatchLit solver lit this

  constrIsLocked solver this this2 = do
    (lb,ub) <- getBounds (atLeastLits this2)
    let size = ub - lb + 1
        n = atLeastNum this2
        loop i
          | i > n = return False
          | otherwise = do
              l <- unsafeRead (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 <- readArray a n
      unless (litn == falsifiedLit) $ error "AtLeastHandler.constrPropagate: should not happen"

    (lb,ub) <- getBounds a
    assert (lb==0) $ return ()
    i <- findForWatch solver a (n+1) ub
    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 i
              | i >= n = return True
              | otherwise = do
                  liti <- unsafeRead a i
                  ret2 <- assignBy solver liti this
                  if ret2
                    then loop (i+1)
                    else return False
        loop 0
      _ -> do
        liti <- unsafeRead a i
        litn <- unsafeRead a n
        unsafeWrite a i litn
        unsafeWrite 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 <- unsafeRead a i
              if (li /= falsifiedLit) then
                loop (i+1)
              else do
                ln <- unsafeRead a n
                unsafeWrite a n li
                unsafeWrite a i ln

  constrReasonOf solver this concl = do
    (lb,ub) <- getBounds (atLeastLits this)
    assert (lb==0) $ return ()
    let n = atLeastNum this
    falsifiedLits <- mapM (readArray (atLeastLits this)) [n..ub] -- 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 <- readArray (atLeastLits this) i
                  val <- litValue solver lit
                  if val == lFalse
                  then return lit
                  else go (i+1)
        lit <- go lb
        return $ lit : falsifiedLits
      Just lit -> do
        when debugMode $ do
          es <- getElems (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 <- getElems (atLeastLits this)
    return ([(1,l) | l <- lits], fromIntegral (atLeastNum this))

  isSatisfied solver this = do
    lits <- getElems (atLeastLits this)
    vals <- mapM (litValue solver) lits
    return $ length [v | v <- vals, v == lTrue] >= atLeastNum this

  constrReadActivity this = readIORef (atLeastActivity this)

  constrWriteActivity this aval = writeIORef (atLeastActivity this) $! aval

basicAttachAtLeastHandler :: Solver -> AtLeastHandler -> IO Bool
basicAttachAtLeastHandler solver this = do
  lits <- getElems (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 <- readIORef (svPBHandlerType 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))

{--------------------------------------------------------------------
  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 (flip compare `on` 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 (flip compare `on` 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
#if MIN_VERSION_containers(0,5,0)
      xs <- liftM (map snd . IM.toDescList) $ foldM f IM.empty (puebloTerms this2)
#else
      xs <- liftM (reverse . map snd . IM.toAscList) $ foldM f IM.empty (puebloTerms this2)
#endif
      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 :: !(IOUArray Int Lit)
  , 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
  let size = length ls
  a <- newListArray (0, size-1) 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 <- getElems (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
    (lb,ub) <- getBounds a
    assert (lb == 0) $ return ()
    let size = ub-lb+1

    if size == 0 then do
      markBad solver
      return False
    else if size == 1 then do
      lit0 <- unsafeRead a 0
      assignBy solver lit0 this
    else do
      ref <- newIORef 1
      let f i = do
            lit_i <- unsafeRead 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 ub
              case k of
                -1 -> do
                  return False
                _ -> do
                  lit_k <- unsafeRead a k
                  unsafeWrite a i lit_k
                  unsafeWrite a k lit_i
                  writeIORef ref $! (k+1)
                  return True

      b <- f 0
      if b then do
        lit0 <- unsafeRead a 0
        watchVar solver (litVar lit0) this
        b2 <- f 1
        if b2 then do
          lit1 <- unsafeRead 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..ub] $ \l -> do
            lit <- unsafeRead a l
            lv <- litLevel solver lit
            return (l,lv)
          lit1 <- unsafeRead a 1
          liti <- unsafeRead a i
          unsafeWrite a 1 liti
          unsafeWrite a i lit1
          watchVar solver (litVar liti) this
          -- lit0 ⊕ y
          y <- do
            ref <- newIORef False
            forLoop 1 (<=ub) (+1) $ \j -> do
              lit_j <- unsafeRead 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 (flip (comparing snd))) $ forM [lb..ub] $ \l -> do
          lit <- unsafeRead a l
          lv <- litLevel solver lit
          return (l,lv)
        forM_ (zip [0..] ls) $ \(i,lit) -> do
          unsafeWrite a i lit
        lit0 <- unsafeRead a 0
        lit1 <- unsafeRead a 1
        watchVar solver (litVar lit0) this
        watchVar solver (litVar lit1) this
        isSatisfied solver this2

  constrDetach solver this this2 = do
    (lb,ub) <- getBounds (xorLits this2)
    let size = ub-lb+1
    when (size >= 2) $ do
      lit0 <- unsafeRead (xorLits this2) 0
      lit1 <- unsafeRead (xorLits this2) 1
      unwatchVar solver (litVar lit0) this
      unwatchVar solver (litVar lit1) this

  constrIsLocked solver this this2 = do
    lit0 <- unsafeRead (xorLits this2) 0
    lit1 <- unsafeRead (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 <- unsafeRead a 0
      (!lb,!ub) <- getBounds a
      assert (lb==0) $ return ()
      i <- findForWatch2 solver a 2 ub
      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 (<=ub) (+1) $ \j -> do
              lit_j <- unsafeRead 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 <- unsafeRead a 1
          !liti <- unsafeRead a i
          unsafeWrite a 1 liti
          unsafeWrite a i lit1
          watchVar solver (litVar liti) this
          return True

    where
      v = litVar falsifiedLit
      a = xorLits this2

      preprocess :: IO ()
      preprocess = do
        !l0 <- unsafeRead a 0
        !l1 <- unsafeRead a 1
        assert (litVar l0 == v || litVar l1 == v) $ return ()
        when (litVar l0 == v) $ do
          unsafeWrite a 0 l1
          unsafeWrite a 1 l0

  constrReasonOf solver this l = do
    lits <- getElems (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 <- getElems (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 <- liftM rangeSize (getBounds (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 <- getElems (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 -> IO (Maybe SomeConstraintHandler)
deduceT solver = do
  mt <- readIORef (svTheorySolver solver)
  case mt of
    Nothing -> return Nothing
    Just t -> do
      n <- Vec.getSize (svTrail solver)
      let h = CHTheory TheoryHandler
          callback l = assignBy solver l h
          loop i = do
            if i < n then do
              l <- Vec.unsafeRead (svTrail solver) i
              ok <- thAssertLit t callback l
              if ok then
                loop (i+1)
              else
                return False
            else do
              return True
      b <- loop =<< readIOURef (svTheoryChecked solver)
      if not b then
        return (Just h)
      else do
        b2 <- thCheck t callback
        if b2 then do
          writeIOURef (svTheoryChecked solver) n
          return Nothing
        else
          return (Just 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)
    thExplain t l

  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
--------------------------------------------------------------------}

data RestartStrategy = MiniSATRestarts | ArminRestarts | LubyRestarts
  deriving (Show, Eq, Ord, Enum, Bounded)

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

#if !MIN_VERSION_base(4,6,0)

modifyIORef' :: IORef a -> (a -> a) -> IO ()
modifyIORef' ref f = do
  x <- readIORef ref
  writeIORef ref $! f x

#endif

shift :: IORef [a] -> IO a
shift ref = do
  (x:xs) <- readIORef ref
  writeIORef ref xs
  return x

defaultHashWithSalt :: Hashable a => Int -> a -> Int
defaultHashWithSalt salt x = salt `combine` hash x
#if MIN_VERSION_hashable(1,2,0)
  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)

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