{-# 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

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

  -- * Extract results
  , Model
  , model
  , failedAssumptions

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

  -- * Read state
  , 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
import Data.Array.Unsafe (unsafeFreeze)
#elif MIN_VERSION_array(0,4,0)
import Data.Array.IO hiding (unsafeFreeze)
import Data.Array.Unsafe (unsafeFreeze)
#else
import Data.Array.IO
#endif
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 qualified ToySolver.Internal.Data.IndexedPriorityQueue as PQ
import qualified ToySolver.Internal.Data.SeqQueue as SQ
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

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

type Level = Int

levelRoot :: Level
levelRoot = -1

data Assignment
  = Assignment
  { aValue  :: !Bool
  , aIndex  :: {-# UNPACK #-} !Int
  , aLevel  :: {-# UNPACK #-} !Level
  , aReason :: !(Maybe SomeConstraintHandler)
  , aBacktrackCBs :: !(IORef [IO ()])
  }

data VarData
  = VarData
  { vdAssignment :: !(IORef (Maybe Assignment))
  , vdPolarity   :: !(IORef Bool)
  , vdPosLitData :: !LitData
  , vdNegLitData :: !LitData
  , vdActivity   :: !(IORef VarActivity)
  }

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

newVarData :: IO VarData
newVarData = do
  ainfo <- newIORef Nothing
  polarity <- newIORef True
  pos <- newLitData
  neg <- newLitData
  activity <- newIORef 0
  return $ VarData ainfo polarity pos neg activity

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

varData :: Solver -> Var -> IO VarData
varData solver !v = do
  a <- readIORef (svVarData solver)
  unsafeRead a (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
  m <- readIORef (vdAssignment vd)
  case m of
    Nothing -> return lUndef
    Just x -> return $! (liftBool $! aValue x)

{-# 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

varLevel :: Solver -> Var -> IO Level
varLevel solver !v = do
  vd <- varData solver v
  m <- readIORef (vdAssignment vd)
  case m of
    Nothing -> error ("ToySolver.SAT.varLevel: unassigned var " ++ show v)
    Just a -> return (aLevel a)

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
  m <- readIORef (vdAssignment vd)
  case m of
    Nothing -> error ("ToySolver.SAT.varReason: unassigned var " ++ show v)
    Just a -> return (aReason a)

varAssignNo :: Solver -> Var -> IO Int
varAssignNo solver !v = do
  vd <- varData solver v
  m <- readIORef (vdAssignment vd)
  case m of
    Nothing -> error ("ToySolver.SAT.varAssignNo: unassigned var " ++ show v)
    Just a -> return (aIndex a)

-- | Solver instance
data Solver
  = Solver
  { svOk           :: !(IORef Bool)
  , svVarQueue     :: !PQ.PriorityQueue
  , svTrail        :: !(IORef [Lit])
  , svVarCounter   :: !(IORef Int)
  , svVarData      :: !(IORef (IOArray Int VarData))
  , svConstrDB     :: !(IORef [SomeConstraintHandler])
  , svLearntDB     :: !(IORef (Int,[SomeConstraintHandler]))
  , svAssumptions  :: !(IORef (IOUArray Int Lit))
  , svLevel        :: !(IORef Level)
  , svBCPQueue     :: !(SQ.SeqQueue Lit)
  , svModel        :: !(IORef (Maybe Model))
  , svNDecision    :: !(IORef Int)
  , svNRandomDecision :: !(IORef Int)
  , svNConflict    :: !(IORef Int)
  , svNRestart     :: !(IORef Int)
  , svNAssigns     :: !(IORef Int)
  , svNFixed       :: !(IORef Int)
  , svNLearntGC    :: !(IORef Int)
  , svNRemovedConstr :: !(IORef Int)

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

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

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

  -- | Amount to bump next constraint with.
  , svConstrInc    :: !(IORef 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)

  , svLearntLim       :: !(IORef Int)
  , svLearntLimAdjCnt :: !(IORef Int)
  , svLearntLimSeq    :: !(IORef [(Int,Int)])

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

  , svEnableBackwardSubsumptionRemoval :: !(IORef Bool)

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

  , svCheckModel :: !(IORef Bool)

  , svRandomFreq :: !(IORef Double)
  , svRandomGen  :: !(IORef Rand.StdGen)

  , svFailedAssumptions :: !(IORef [Lit])

  , svConfBudget :: !(IORef Int)
  }

markBad :: Solver -> IO ()
markBad solver = do
  writeIORef (svOk solver) False
  SQ.clear (svBCPQueue solver)

bcpEnqueue :: Solver -> Lit -> IO ()
bcpEnqueue solver l = SQ.enqueue (svBCPQueue solver) l

bcpDequeue :: Solver -> IO (Maybe Lit)
bcpDequeue solver = SQ.dequeue (svBCPQueue solver)

bcpCheckEmpty :: Solver -> IO ()
bcpCheckEmpty solver = do
  size <- SQ.queueSize (svBCPQueue solver)
  unless (size == 0) $
    error "BUG: BCP Queue should be empty at this point"

assignBy :: ConstraintHandler c => Solver -> Lit -> c -> IO Bool
assignBy solver lit c = do
  lv <- readIORef (svLevel solver)
  let !c2 = if lv == levelRoot
            then Nothing
            else Just $! toConstraintHandler 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)
  m <- readIORef (vdAssignment vd)
  case m of
    Just a -> return $ litPolarity lit == aValue a
    Nothing -> do
      idx <- readIORef (svNAssigns solver)
      lv <- readIORef (svLevel solver)
      bt <- newIORef []

      writeIORef (vdAssignment vd) $ Just $!
        Assignment
        { aValue  = litPolarity lit
        , aIndex  = idx
        , aLevel  = lv
        , aReason = reason
        , aBacktrackCBs = bt
        }

      modifyIORef (svTrail solver) (lit:)
      modifyIORef' (svNAssigns solver) (+1)
      when (lv == levelRoot) $ modifyIORef' (svNFixed solver) (+1)
      bcpEnqueue 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
  m <- readIORef (vdAssignment vd)
  case m of
    Nothing -> error "unassign: should not happen"
    Just a -> do
      flag <- getEnablePhaseSaving solver
      when flag $ writeIORef (vdPolarity vd) (aValue a)
      readIORef (aBacktrackCBs a) >>= sequence_
  writeIORef (vdAssignment vd) Nothing
  modifyIORef' (svNAssigns solver) (subtract 1)
  PQ.enqueue (svVarQueue solver) v

addBacktrackCB :: Solver -> Var -> IO () -> IO ()
addBacktrackCB solver !v callback = do
  vd <- varData solver v
  m <- readIORef (vdAssignment vd)
  case m of
    Nothing -> error "addBacktrackCB: should not happen"
    Just a -> modifyIORef (aBacktrackCBs a) (callback :)

-- | Register the constraint to be notified when the literal becames false.
watch :: ConstraintHandler c => Solver -> Lit -> c -> IO ()
watch solver !lit c = do
  when debugMode $ do
    lits <- watchedLiterals solver c
    unless (lit `elem` lits) $ error "watch: should not happen"
  ld <- litData solver lit
  modifyIORef (ldWatches ld) (toConstraintHandler 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 solver c
    return $ printf "constraint %s is added" str

  (lhs,_) <- toPBAtLeast solver c
  forM_ lhs $ \(_,lit) -> do
     ld <- litData solver lit
     modifyIORef' (ldOccurList ld) (HashSet.insert c2)

  sanityCheck solver

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 solver c
    return $ printf "constraint %s is added" str
  sanityCheck solver

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
  readIORef (vdActivity vd)

varDecayActivity :: Solver -> IO ()
varDecayActivity solver = do
  d <- readIORef (svVarDecay solver)
  modifyIORef' (svVarInc solver) (d*)

varBumpActivity :: Solver -> Var -> IO ()
varBumpActivity solver !v = do
  inc <- readIORef (svVarInc solver)
  vd <- varData solver v
  modifyIORef' (vdActivity vd) (+inc)
  PQ.update (svVarQueue solver) v
  aval <- readIORef (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
    modifyIORef' (vdActivity vd) (* 1e-20)
  modifyIORef' (svVarInc solver) (* 1e-20)

variables :: Solver -> IO [Var]
variables solver = do
  n <- nVars solver
  return [1 .. n]

-- | number of variables of the problem.
nVars :: Solver -> IO Int
nVars solver = do
  vcnt <- readIORef (svVarCounter solver)
  return $! (vcnt-1)

-- | number of assigned variables.
nAssigns :: Solver -> IO Int
nAssigns solver = readIORef (svNAssigns solver)

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

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

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

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

-- | Create a new Solver instance.
newSolver :: IO Solver
newSolver = do
 rec
  ok   <- newIORef True
  vcnt <- newIORef 1
  trail <- newIORef []
  vars <- newIORef =<< newArray_ (1,0)
  vqueue <- PQ.newPriorityQueueBy (ltVar solver)
  db  <- newIORef []
  db2 <- newIORef (0,[])
  as  <- newIORef =<< newArray_ (0,-1)
  lv  <- newIORef levelRoot
  q   <- SQ.newFifo
  m   <- newIORef Nothing
  ndecision <- newIORef 0
  nranddec  <- newIORef 0
  nconflict <- newIORef 0
  nrestart  <- newIORef 0
  nassigns  <- newIORef 0
  nfixed    <- newIORef 0
  nlearntgc <- newIORef 0
  nremoved  <- newIORef 0

  constrDecay <- newIORef (1 / 0.999)
  constrInc   <- newIORef 1
  varDecay <- newIORef (1 / 0.95)
  varInc   <- newIORef 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
  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 <- newIORef (-1)

  let solver =
        Solver
        { svOk = ok
        , svVarCounter = vcnt
        , svVarQueue   = vqueue
        , svTrail      = trail
        , svVarData    = vars
        , svConstrDB   = db
        , svLearntDB   = db2
        , svAssumptions = as
        , svLevel      = lv
        , svBCPQueue   = q
        , svModel      = m
        , svNDecision  = ndecision
        , svNRandomDecision = nranddec
        , svNConflict  = nconflict
        , svNRestart   = nrestart
        , svNAssigns   = nassigns
        , svNFixed     = nfixed
        , svNLearntGC  = nlearntgc
        , svNRemovedConstr = nremoved
        , 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
        , svEnableBackwardSubsumptionRemoval = enableBackwardSubsumptionRemoval
        , svLearntLim       = learntLim
        , svLearntLimAdjCnt = learntLimAdjCnt
        , svLearntLimSeq    = learntLimSeq
        , svLogger = logger
        , svStartWC    = startWC
        , svLastStatWC = lastStatWC
        , svCheckModel = checkModel
        , svRandomFreq = randfreq
        , svRandomGen  = randgen
        , svFailedAssumptions = failed
        , svConfBudget = confBudget
        }
 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
  v <- readIORef (svVarCounter solver)
  writeIORef (svVarCounter solver) (v+1)
  vd <- newVarData

  a <- readIORef (svVarData solver)
  (_,ub) <- getBounds a
  if v <= ub
    then writeArray a v vd
    else do
      let ub' = max 2 (ub * 3 `div` 2)
      a' <- newArray_ (1,ub')
      forLoop 1 (<=ub) (+1) $ \v2 -> do
        vd2 <- readArray a v2
        writeArray a' v2 vd2
      writeArray a' v vd
      writeIORef (svVarData solver) a'

  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 <- nVars 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 <- nVars solver
  resizeVarCapacity solver (nv+n)
  replicateM_ n (newVar solver)

-- |Pre-allocate internal buffer for @n@ variables.
resizeVarCapacity :: Solver -> Int -> IO ()
resizeVarCapacity solver n = do
  PQ.resizeHeapCapacity (svVarQueue solver) n
  PQ.resizeTableCapacity (svVarQueue solver) (n+1)
  a <- readIORef (svVarData solver)
  (_,ub) <- getBounds a
  when (ub < n) $ do
    a' <- newArray_ (1,n)
    forLoop 1 (<=ub) (+1) $ \v -> do
      vd <- readArray a v
      writeArray a' v vd
    writeIORef (svVarData solver) a'

-- |Add a clause to the solver.
addClause :: Solver -> Clause -> IO ()
addClause solver lits = do
  d <- readIORef (svLevel solver)
  assert (d == levelRoot) $ return ()

  ok <- readIORef (svOk solver)
  when ok $ do
    lits2 <- instantiateClause solver lits
    case normalizeClause =<< lits2 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 lits3 -> do
        subsumed <- checkForwardSubsumption solver lits
        unless subsumed $ do
          removeBackwardSubsumedBy solver ([(1,lit) | lit <- lits3], 1)
          clause <- newClauseHandler lits3 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 <- readIORef (svLevel solver)
  assert (d == levelRoot) $ return ()

  ok <- readIORef (svOk solver)
  when ok $ do
    (lits',n') <- liftM normalizeAtLeast $ instantiateAtLeast 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
      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 lits' (len-n)
  where
    len   = length lits
    lits' = map litNot lits

-- | 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 <- readIORef (svLevel solver)
  assert (d == levelRoot) $ return ()

  ok <- readIORef (svOk solver)
  when ok $ do
    (ts',degree) <- liftM normalizePBLinAtLeast $ instantiatePB solver (ts,n)
  
    case pbToAtLeast (ts',degree) of
      Just (lhs',rhs') -> addAtLeast solver lhs' rhs'
      Nothing -> do
        let cs = map fst ts'
            slack = sum cs - degree
        if degree <= 0 then return ()
        else if slack < 0 then markBad solver
        else do
          removeBackwardSubsumedBy solver (ts', degree)
          c <- newPBHandler solver ts' degree False
          addToDB solver c
          ret <- attach solver c
          if not ret
           then do
             markBad solver
           else do
             ret2 <- deduce solver
             case ret2 of
               Nothing -> return ()
               Just _ -> markBad solver

-- | 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 $ instantiatePB solver (ts,n)
  addPBAtLeast solver ts2 n2
  addPBAtMost solver ts2 n2

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

-- | Add a soft pseudo boolean constraints /lit ⇒ c1*l1 + c2*l2 + … ≤ n/.
addPBAtMostSoft
  :: Solver          -- ^ The 'Solver' argument.
  -> Lit             -- ^ indicator @lit@
  -> [(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 /lit ⇒ c1*l1 + c2*l2 + … = n/.
addPBExactlySoft
  :: Solver          -- ^ The 'Solver' argument.
  -> Lit             -- ^ indicator @lit@
  -> [(Integer,Lit)] -- ^ set of terms @[(c1,l1),(c2,l2),…]@
  -> Integer         -- ^ /n/
  -> IO ()
addPBExactlySoft solver sel lhs rhs = do
  (lhs2, rhs2) <- liftM normalizePBLinExactly $ instantiatePB solver (lhs,rhs)
  addPBAtLeastSoft solver sel lhs2 rhs2
  addPBAtMostSoft solver sel lhs2 rhs2

{--------------------------------------------------------------------
  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
  as <- newArray_ (0,-1)
  writeIORef (svAssumptions solver) as
  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
  as <- newListArray (0, length ls -1) ls
  writeIORef (svAssumptions solver) as
  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 <- readIORef (svLevel solver)
      assert (d == levelRoot) $ return ()

      restartStrategy <- readIORef (svRestartStrategy solver)
      restartFirst  <- readIORef (svRestartFirst solver)
      restartInc    <- readIORef (svRestartInc solver)
      let restartSeq = mkRestartSeq restartStrategy restartFirst restartInc

      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 <- nConstraints solver
        nv <- nVars 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
                modifyIORef' (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") =<< readIORef (svNDecision solver)
      (log solver . printf "#random_decision = %d") =<< readIORef (svNRandomDecision solver)
      (log solver . printf "#conflict = %d") =<< readIORef (svNConflict solver)
      (log solver . printf "#restart = %d")  =<< readIORef (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
      sanityCheck solver
      conflict <- deduce solver
      sanityCheck solver
      case conflict of
        Just constr -> do
          ret <- handleConflict conflictCounter constr
          case ret of
            Just sr -> return sr
            Nothing -> loop
        Nothing -> do
          lv <- readIORef (svLevel 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 <- nLearnt solver
      m <- nAssigns solver
      learnt_lim <- readIORef (svLearntLim solver)
      when (learnt_lim >= 0 && n - m > learnt_lim) $ do
        modifyIORef' (svNLearntGC solver) (+1)
        reduceDB solver

    pickAssumption :: IO (Maybe Lit)
    pickAssumption = do
      !as <- readIORef (svAssumptions solver)
      !b <- getBounds as
      let go = do
              d <- readIORef (svLevel solver)
              if not (inRange b (d+1))
                then return (Just litUndef)
                else do
                  l <- readArray as (d+1)
                  val <- litValue solver l
                  if val == lTrue then do
                     -- dummy decision level
                     modifyIORef' (svLevel solver) (+1)
                     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

      modifyIORef' (svNConflict solver) (+1)
      d <- readIORef (svLevel solver)

      when debugMode $ logIO solver $ do
        str <- showConstraintHandler solver constr
        return $ printf "conflict(level=%d): %s" d str

      modifyIORef' conflictCounter (+1)
      c <- readIORef conflictCounter

      modifyIORef' (svConfBudget solver) $ \confBudget ->
        if confBudget > 0 then confBudget - 1 else confBudget
      confBudget <- readIORef (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
          addToLearntDB solver cl
          basicAttachClauseHandler solver cl
          assignBy solver lit cl
          constrBumpActivity solver cl

    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
          addToLearntDB solver cl
          basicAttachClauseHandler solver cl
          constrBumpActivity solver cl
          when (minLevel == clauseLevel) $ do
            _ <- assignBy solver lit cl -- 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 the model.
model :: Solver -> IO Model
model 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.
failedAssumptions :: Solver -> IO [Lit]
failedAssumptions 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)
    modifyIORef' (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_
        (modifyIORef' (svLevel solver) (+1))
        (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 solver 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
            pb2 <- instantiatePB solver =<< toPBAtLeast solver 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)
  modifyIORef' (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)
-- Negative value is 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)
setRestartInc :: Solver -> Double -> IO ()
setRestartInc solver !r = writeIORef (svRestartInc solver) r

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

data LearningStrategy
  = LearningClause
  | LearningHybrid

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

defaultLearningStrategy :: LearningStrategy
defaultLearningStrategy = LearningClause

-- | The initial limit for learnt clauses.
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)
setLearntSizeInc :: Solver -> Double -> IO ()
setLearntSizeInc solver !r = writeIORef (svLearntSizeInc solver) r

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

-- | The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)
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 = writeIORef (svConfBudget solver) b
setConfBudget solver _ = writeIORef (svConfBudget solver) (-1)

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

defaultPBHandlerType :: PBHandlerType
defaultPBHandlerType = PBHandlerTypeCounter

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

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
         modifyIORef' (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
  modifyIORef' (svNDecision solver) (+1)
  modifyIORef' (svLevel solver) (+1)
  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 = 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 -> 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

analyzeConflict :: ConstraintHandler c => Solver -> c -> IO (Clause, Level)
analyzeConflict solver constr = do
  d <- readIORef (svLevel 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
            ret <- popTrail solver
            case ret of
              Nothing -> do
                error $ printf "analyzeConflict: should not happen: empty trail: loop %s %s"
                               (show lits1) (show lits2)
              Just l -> do
                if litNot l `IS.notMember` lits1
                 then do
                   unassign solver (litVar l)
                   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)
                      unassign solver (litVar l)
                      (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
  lits <- readIORef (svTrail solver)
  let go :: [Lit] -> VarSet -> [Lit] -> IO [Lit]
      go [] _ result = return result
      go (l:ls) seen result = do
        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 ls 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 ls seen' result
         else
           go ls seen result
  go lits (IS.singleton (litVar p)) [p]

analyzeConflictHybrid :: ConstraintHandler c => Solver -> c -> IO ((Clause, Level), (PBLinAtLeast, Level))
analyzeConflictHybrid solver constr = do
  d <- readIORef (svLevel 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
            ret <- popTrail solver
            case ret of
              Nothing -> do
                error $ printf "analyzeConflictHybrid: should not happen: empty trail: loop %s %s"
                               (show lits1) (show lits2)
              Just l -> do
                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 <- toPBAtLeast solver constr2
                             o <- pbOverSAT solver pb2
                             let pb3 = if o then ([(1,l2) | l2 <- l:xs],1) else pb2
                             return $ cutResolve pb pb3 (litVar l)
                           else return pb

                    unassign solver (litVar l)
                    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 <- toPBAtLeast solver constr
  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

popTrail :: Solver -> IO (Maybe Lit)
popTrail solver = do
  m <- readIORef (svTrail solver)
  case m of
    []   -> return Nothing
    l:ls -> do
      writeIORef (svTrail solver) ls
      return $ Just l

-- | 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
  writeIORef (svTrail solver) =<< loop =<< readIORef (svTrail solver)
  SQ.clear (svBCPQueue solver)
  writeIORef (svLevel solver) level
  where
    loop :: [Lit] -> IO [Lit]
    loop [] = return []
    loop lls@(l:ls) = do
      lv <- litLevel solver l
      if lv <= level
        then return lls
        else unassign solver (litVar l) >> loop ls

constructModel :: Solver -> IO ()
constructModel solver = do
  n <- nVars solver
  (marr::IOUArray Var Bool) <- newArray_ (1,n)
  forLoop 1 (<=n) (+1) $ \v -> do
    vd <- varData solver v
    a <- readIORef (vdAssignment vd)
    writeArray marr v (aValue (fromJust a))
  m <- unsafeFreeze marr
  writeIORef (svModel solver) (Just m)

constrDecayActivity :: Solver -> IO ()
constrDecayActivity solver = do
  d <- readIORef (svConstrDecay solver)
  modifyIORef' (svConstrInc solver) (d*)

constrBumpActivity :: ConstraintHandler a => Solver -> a -> IO ()
constrBumpActivity solver this = do
  aval <- constrReadActivity this
  when (aval >= 0) $ do -- learnt clause
    inc <- readIORef (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)
  modifyIORef' (svConstrInc solver) (* 1e-20)

resetStat :: Solver -> IO ()
resetStat solver = do
  writeIORef (svNDecision solver) 0
  writeIORef (svNRandomDecision solver) 0
  writeIORef (svNConflict solver) 0
  writeIORef (svNRestart solver) 0
  writeIORef (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   <- readIORef (svNRestart solver)
    dec       <- readIORef (svNDecision solver)
    conflict  <- readIORef (svNConflict solver)
    learntLim <- readIORef (svLearntLim solver)
    learntGC  <- readIORef (svNLearntGC solver)
    fixed     <- readIORef (svNFixed solver)
    removed   <- readIORef (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 :: Solver -> a -> IO String

  attach :: Solver -> a -> IO Bool

  watchedLiterals :: Solver -> a -> IO [Lit]

  -- | invoked with the watched literal when the literal is falsified.
  -- 'watch' で 'toConstraint' を呼び出して heap allocation が発生するのを
  -- 避けるために、元の 'SomeConstraintHandler' も渡しておく。
  basicPropagate :: 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.
  basicReasonOf :: Solver -> a -> Maybe Lit -> IO Clause

  toPBAtLeast :: Solver -> 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 ()

detach :: ConstraintHandler a => Solver -> a -> IO ()
detach solver c = do
  let c2 = toConstraintHandler c
  lits <- watchedLiterals solver c
  forM_ lits $ \lit -> do
    ld <- litData solver lit
    modifyIORef' (ldWatches ld) (delete c2)
  (lhs,_) <- toPBAtLeast solver c
  forM_ lhs $ \(_,lit) -> do
    ld <- litData solver lit
    modifyIORef' (ldOccurList ld) (HashSet.delete c2)

-- | invoked with the watched literal when the literal is falsified.
propagate :: Solver -> SomeConstraintHandler -> Lit -> IO Bool
propagate solver c l = basicPropagate 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 solver c
          error (printf "reasonOf: value of literal %d should be True but %s (basicReasonOf %s %s)" lit (show val) str (show x))
  cl <- basicReasonOf solver c x
  when debugMode $ do
    forM_ cl $ \lit -> do
      val <- litValue solver lit
      unless (lFalse == val) $ do
        str <- showConstraintHandler solver c
        error (printf "reasonOf: value of literal %d should be False but %s (basicReasonOf %s %s)" lit (show val) str (show x))
  return cl

isLocked :: Solver -> SomeConstraintHandler -> IO Bool
isLocked solver c = anyM p =<< watchedLiterals solver c
  where
    p :: Lit -> IO Bool
    p lit = do
      val <- litValue solver lit
      if val /= lTrue
        then return False
        else do
          m <- varReason solver (litVar lit)
          case m of
            Nothing -> return False
            Just c2 -> return $! c == c2

data SomeConstraintHandler
  = CHClause !ClauseHandler
  | CHAtLeast !AtLeastHandler
  | CHPBCounter !PBHandlerCounter
  | CHPBPueblo !PBHandlerPueblo
  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

instance ConstraintHandler SomeConstraintHandler where
  toConstraintHandler = id

  showConstraintHandler solver (CHClause c)    = showConstraintHandler solver c
  showConstraintHandler solver (CHAtLeast c)   = showConstraintHandler solver c
  showConstraintHandler solver (CHPBCounter c) = showConstraintHandler solver c
  showConstraintHandler solver (CHPBPueblo c)  = showConstraintHandler solver c

  attach solver (CHClause c)    = attach solver c
  attach solver (CHAtLeast c)   = attach solver c
  attach solver (CHPBCounter c) = attach solver c
  attach solver (CHPBPueblo c)  = attach solver c

  watchedLiterals solver (CHClause c)    = watchedLiterals solver c
  watchedLiterals solver (CHAtLeast c)   = watchedLiterals solver c
  watchedLiterals solver (CHPBCounter c) = watchedLiterals solver c
  watchedLiterals solver (CHPBPueblo c)  = watchedLiterals solver c

  basicPropagate solver this (CHClause c)  lit   = basicPropagate solver this c lit
  basicPropagate solver this (CHAtLeast c) lit   = basicPropagate solver this c lit
  basicPropagate solver this (CHPBCounter c) lit = basicPropagate solver this c lit
  basicPropagate solver this (CHPBPueblo c) lit  = basicPropagate solver this c lit

  basicReasonOf solver (CHClause c)  l   = basicReasonOf solver c l
  basicReasonOf solver (CHAtLeast c) l   = basicReasonOf solver c l
  basicReasonOf solver (CHPBCounter c) l = basicReasonOf solver c l
  basicReasonOf solver (CHPBPueblo c) l  = basicReasonOf solver c l

  toPBAtLeast solver (CHClause c)    = toPBAtLeast solver c
  toPBAtLeast solver (CHAtLeast c)   = toPBAtLeast solver c
  toPBAtLeast solver (CHPBCounter c) = toPBAtLeast solver c
  toPBAtLeast solver (CHPBPueblo c)  = toPBAtLeast solver 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

  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

  constrReadActivity (CHClause c)    = constrReadActivity c
  constrReadActivity (CHAtLeast c)   = constrReadActivity c
  constrReadActivity (CHPBCounter c) = constrReadActivity c
  constrReadActivity (CHPBPueblo 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

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

{--------------------------------------------------------------------
  Clause
--------------------------------------------------------------------}

data ClauseHandler
  = ClauseHandler
  { claLits :: !(IOUArray Int Lit)
  , claActivity :: !(IORef Double)
  , claHash :: !Int
  }

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)

  attach solver this = do
    -- BCP Queue should be empty at this point.
    -- If not, duplicated propagation happens.
    bcpCheckEmpty solver

    (lb,ub) <- getBounds (claLits this)
    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 (claLits this) 0
      assignBy solver lit0 this
    else do
      ref <- newIORef 1
      let f i = do
            lit_i <- unsafeRead (claLits this) i
            val_i <- litValue solver lit_i
            if val_i /= lFalse then
              return True
            else do
              j <- readIORef ref
              k <- findForWatch solver (claLits this) j ub
              case k of
                -1 -> do
                  return False
                _ -> do
                  lit_k <- unsafeRead (claLits this) k
                  unsafeWrite (claLits this) i lit_k
                  unsafeWrite (claLits this) k lit_i
                  writeIORef ref $! (k+1)
                  return True

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

  watchedLiterals _ this = do
    lits <- getElems (claLits this)
    case lits of
      l1:l2:_ -> return [l1, l2]
      _ -> return []

  basicPropagate !solver this this2 !falsifiedLit = do
    preprocess

    !lit0 <- unsafeRead a 0
    !val0 <- litValue solver lit0
    if val0 == lTrue
      then do
        watch solver falsifiedLit this
        return True
      else do
        (!lb,!ub) <- getBounds a
        assert (lb==0) $ return ()
        i <- findForWatch solver a 2 ub
        case i of
          -1 -> do
            when debugMode $ logIO solver $ do
               str <- showConstraintHandler solver this
               return $ printf "basicPropagate: %s is unit" str
            watch solver falsifiedLit this
            assignBy solver lit0 this
          _  -> do
            !lit1 <- unsafeRead a 1
            !liti <- unsafeRead a i
            unsafeWrite a 1 liti
            unsafeWrite a i lit1
            watch 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

  basicReasonOf _ this l = do
    lits <- getElems (claLits this)
    case l of
      Nothing -> return lits
      Just lit -> do
        assert (lit == head lits) $ return ()
        return $ tail lits

  toPBAtLeast _ 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 <- liftM rangeSize (getBounds (claLits this))
    return $! size <= 2

  constrReadActivity this = readIORef (claActivity this)

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

instantiateClause :: Solver -> Clause -> IO (Maybe Clause)
instantiateClause solver = loop []
  where
    loop :: [Lit] -> [Lit] -> IO (Maybe Clause)
    loop ret [] = return $ Just ret
    loop ret (l:ls) = do
      val <- litValue solver l
      if val==lTrue then
         return Nothing
       else if val==lFalse then
         loop ret ls
       else
         loop (l : ret) ls

basicAttachClauseHandler :: Solver -> ClauseHandler -> IO Bool
basicAttachClauseHandler solver this = do
  lits <- getElems (claLits this)
  case lits of
    [] -> do
      markBad solver
      return False
    [l1] -> do
      assignBy solver l1 this
    l1:l2:_ -> do
      watch solver l1 this
      watch solver l2 this
      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
  attach solver this = do
    -- BCP Queue should be empty at this point.
    -- If not, duplicated propagation happens.
    bcpCheckEmpty solver

    let a = atLeastLits this
    (lb,ub) <- getBounds a
    assert (lb == 0) $ return ()
    let m = ub - lb + 1
        n = atLeastNum this

    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
                  watch 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
                  watch 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
                  watch 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
                    watch 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
                      watch solver lit_l this
                    -- n+1 literals (0 .. n) are watched.
                    return False
      f 0 n

  watchedLiterals _ this = do
    lits <- getElems (atLeastLits this)
    let n = atLeastNum this
    let ws = if length lits > n then take (n+1) lits else []
    return ws

  basicPropagate solver this this2 falsifiedLit = do
    preprocess

    when debugMode $ do
      litn <- readArray a n
      unless (litn == falsifiedLit) $ error "AtLeastHandler.basicPropagate: 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 solver this
          return $ printf "basicPropagate: %s is unit" str
        watch 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
        watch 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

  basicReasonOf 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.basicReasonOf: %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.basicReasonOf: 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.basicReasonOf: cannot find %d in first %d elements" n
        return falsifiedLits

  toPBAtLeast _ 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

instantiateAtLeast :: Solver -> AtLeast -> IO AtLeast
instantiateAtLeast solver (xs,n) = loop ([],n) xs
  where
    loop :: AtLeast -> [Lit] -> IO AtLeast
    loop ret [] = return ret
    loop (ys,m) (l:ls) = do
      val <- litValue solver l
      if val == lTrue then
         loop (ys, m-1) ls
       else if val == lFalse then
         loop (ys, m) ls
       else
         loop (l:ys, m) ls

basicAttachAtLeastHandler :: Solver -> AtLeastHandler -> IO Bool
basicAttachAtLeastHandler solver this = do
  lits <- getElems (atLeastLits this)
  let m = length lits
      n = atLeastNum this
  if m < n then do
    markBad solver
    return False
  else if m == n then do
    allM (\l -> assignBy solver l this) lits
  else do -- m > n
    forM_ (take (n+1) lits) $ \l -> watch solver l this
    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

instantiatePB :: Solver -> PBLinAtLeast -> IO PBLinAtLeast
instantiatePB solver (xs,n) = loop ([],n) xs
  where
    loop :: PBLinAtLeast -> PBLinSum -> IO PBLinAtLeast
    loop ret [] = return ret
    loop (ys,m) ((c,l):ts) = do
      val <- litValue solver l
      if val == lTrue then
         loop (ys, m-c) ts
       else if val == lFalse then
         loop (ys, m) ts
       else
         loop ((c,l):ys, m) ts

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)

  attach solver this = do
    -- BCP queue should be empty at this point.
    -- It is important for calculating slack.
    bcpCheckEmpty solver
    s <- liftM sum $ forM (pbTerms this) $ \(c,l) -> do
      watch solver l this
      val <- litValue solver l
      if val == lFalse then do
        addBacktrackCB solver (litVar l) $ modifyIORef' (pbSlack this) (+ c)
        return 0
      else do
        return c
    let slack = s - pbDegree this
    writeIORef (pbSlack this) $! slack
    if slack < 0 then
      return False
    else do
      flip allM (pbTerms this) $ \(c,l) -> do
        val <- litValue solver l
        if c > slack && val == lUndef then do
          assignBy solver l this
        else
          return True

  watchedLiterals _ this = do
    return $ map snd $ pbTerms this

  basicPropagate solver this this2 falsifiedLit = do
    watch solver falsifiedLit this
    let c = pbCoeffMap this2 IM.! falsifiedLit
    modifyIORef' (pbSlack this2) (subtract c)
    addBacktrackCB solver (litVar falsifiedLit) $ modifyIORef' (pbSlack this2) (+ c)
    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

  basicReasonOf 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.basicReasonOf: 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

  toPBAtLeast _ 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
  watch 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)

  attach solver this = do
    bcpCheckEmpty solver
    let constr = toConstraintHandler this
    ret <- puebloPropagate solver constr this

    -- register to watch recently falsified literals to recover
    -- "WatchSum >= puebloDegree this + puebloAMax this" when backtrack is performed.
    wsum <- puebloGetWatchSum this
    unless (wsum >= puebloDegree this + puebloAMax this) $ 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 this)
#else
      xs <- liftM (reverse . map snd . IM.toAscList) $ foldM f IM.empty (puebloTerms this)
#endif
      let g !_ [] = return ()
          g !s (t@(c,l):ts) = do
            addBacktrackCB solver (litVar l) $ puebloWatch solver constr this t
            if s+c >= puebloDegree this + puebloAMax this then return ()
            else g (s+c) ts
      g wsum xs

    return ret

  watchedLiterals _ this = liftM IS.toList $ readIORef (puebloWatches this)

  basicPropagate 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) $
      addBacktrackCB solver (litVar falsifiedLit) $ puebloWatch solver this this2 t
    return ret

  basicReasonOf 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.basicReasonOf: 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

  toPBAtLeast _ 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 this
              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)

{--------------------------------------------------------------------
  Restart strategy
--------------------------------------------------------------------}

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

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 solver c
      log solver $ "BUG: " ++ s ++ " is violated"

sanityCheck :: Solver -> IO ()
sanityCheck _ | not debugMode = return ()
sanityCheck solver = do
  cls <- readIORef (svConstrDB solver)
  forM_ cls $ \constr -> do
    lits <- watchedLiterals solver constr
    forM_ lits $ \l -> do
      ws <- watches solver l
      unless (constr `elem` ws) $ error $ printf "sanityCheck:A:%s" (show lits)

  vs <- variables solver
  let lits = [l | v <- vs, l <- [literal v True, literal v False]]
  forM_ lits $ \l -> do
    cs <- watches solver l
    forM_ cs $ \constr -> do
      lits2 <- watchedLiterals solver constr
      unless (l `elem` lits2) $ do
        error $ printf "sanityCheck:C:%d %s" l (show lits2)

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