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

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

  -- * Problem specification
  , newVar
  , newVars
  , newVars_
  , 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
  , setVarPolarity
  , setLogger
  , setCheckModel
  , setRandomFreq
  , defaultRandomFreq
  , setRandomSeed
  , setConfBudget

  -- * Read state
  , nVars
  , nAssigns
  , nClauses
  , nLearnt

  -- * Internal API
  , varBumpActivity
  , varDecayActivity
  ) where

import Prelude hiding (log)
import Control.Monad
import Control.Exception
#if 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)
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 Data.IndexedPriorityQueue as PQ
import qualified Data.SeqQueue as SQ
import Data.Time
import Data.Typeable
import System.CPUTime
import qualified System.Random as Rand
import Text.Printf

import Data.LBool
import SAT.Types

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

type Level = Int

levelRoot :: Level
levelRoot = -1

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

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

newtype LitData
  = LitData
  { -- | will be invoked when this literal is falsified
    ldWatches :: IORef [SomeConstraint]
  }

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 []
  return $ LitData ws

varData :: Solver -> Var -> IO VarData
varData s !v = do
  a <- readIORef (svVarData s)
  unsafeRead a (v-1)

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

{-# INLINE varValue #-}
varValue :: Solver -> Var -> IO LBool
varValue s !v = do
  vd <- varData s 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 s !l = do
  -- litVar による heap allocation を避けるために、
  -- litPolarityによる分岐後にvarDataを呼ぶ。
  if litPolarity l
    then varValue s l
    else do
      m <- varValue s (negate l)
      return $! lnot m

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

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

varReason :: Solver -> Var -> IO (Maybe SomeConstraint)
varReason s !v = do
  vd <- varData s v
  m <- readIORef (vdAssignment vd)
  case m of
    Nothing -> error ("varReason: unassigned var " ++ show v)
    Just a -> return (aReason a)

-- | Solver instance
data Solver
  = Solver
  { svOk           :: !(IORef Bool)
  , svVarQueue     :: !PQ.PriorityQueue
  , svTrail        :: !(IORef [Lit])
  , svVarCounter   :: !(IORef Int)
  , svVarData      :: !(IORef (IOArray Int VarData))
  , svClauseDB     :: !(IORef [SomeConstraint])
  , svLearntDB     :: !(IORef (Int,[SomeConstraint]))
  , 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 clause activity decay factor. (1 / 0.999)
  , svClaDecay     :: !(IORef Double)

  -- | Amount to bump next clause with.
  , svClaInc       :: !(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 clauses.
  , svLearntSizeFirst :: !(IORef Int)

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

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

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

  , svLearningStrategy :: !(IORef LearningStrategy)

  , 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 = writeIORef (svOk solver) False

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

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

assignBy :: Constraint c => Solver -> Lit -> c -> IO Bool
assignBy solver lit c = assign_ solver lit (Just (toConstraint c))

assign :: Solver -> Lit -> IO Bool
assign solver lit = assign_ solver lit Nothing

assign_ :: Solver -> Lit -> Maybe SomeConstraint -> 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
      lv <- readIORef (svLevel solver)
      bt <- newIORef []

      writeIORef (vdAssignment vd) $ Just $
        Assignment
        { aValue  = litPolarity lit
        , 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
      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 :: Constraint 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) (toConstraint c : )

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

addToDB :: Constraint c => Solver -> c -> IO ()
addToDB solver c = do
  modifyIORef (svClauseDB solver) (toConstraint c : )
  when debugMode $ logIO solver $ do
    str <- showConstraint solver c
    return $ printf "constraint %s is added" str
  sanityCheck solver

addToLearntDB :: Constraint c => Solver -> c -> IO ()
addToLearntDB solver c = do
  modifyIORef (svLearntDB solver) $ \(n,xs) -> (n+1, toConstraint c : xs)
  when debugMode $ logIO solver $ do
    str <- showConstraint 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
    actval <- constrActivity solver c
    return (c, (p, 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 clauses.
nClauses :: Solver -> IO Int
nClauses solver = do
  xs <- readIORef (svClauseDB solver)
  return $ length xs

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

learntConstraints :: Solver -> IO [SomeConstraint]
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

  claDecay <- newIORef (1 / 0.999)
  claInc   <- 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

  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
        , svClauseDB   = 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
        , svClaDecay   = claDecay
        , svClaInc     = claInc
        , svRestartStrategy = restartStrat
        , svRestartFirst = restartFirst
        , svRestartInc   = restartInc
        , svLearningStrategy = learning
        , svLearntSizeFirst = learntSizeFirst
        , svLearntSizeInc = learntSizeInc
        , svCCMin = ccMin
        , 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 s = do
  v <- readIORef (svVarCounter s)
  writeIORef (svVarCounter s) (v+1)
  vd <- newVarData

  a <- readIORef (svVarData s)
  (_,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')
      forM_ [1..ub] $ \v2 -> do
        vd2 <- readArray a v2
        writeArray a' v2 vd2
      writeArray a' v vd
      writeIORef (svVarData s) a'

  PQ.enqueue (svVarQueue s) v
  return v

-- |Add variables. @newVars solver n = replicateM n (newVar solver)@
newVars :: Solver -> Int -> IO [Var]
newVars s n = replicateM n (newVar s)

-- |Add variables. @newVars_ solver n >> return () = newVars_ solver n@
newVars_ :: Solver -> Int -> IO ()
newVars_ s n = replicateM_ n (newVar s)

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

  lits2 <- instantiateClause solver lits
  case normalizeClause =<< lits2 of
    Nothing -> return ()
    Just [] -> markBad solver
    Just [lit] -> do
      ret <- assign solver lit
      assert ret $ return ()
      ret2 <- deduce solver
      case ret2 of
        Nothing -> return ()
        Just _ -> markBad solver
    Just lits3 -> do
      clause <- newClauseData lits3 False
      attach solver clause
      addToDB solver clause

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

  (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
      forM_ lits' $ \l -> do
        ret <- assign solver l
        assert ret $ return ()
        ret2 <- deduce solver
        case ret2 of
          Nothing -> return ()
          Just _ -> markBad solver
    else do
      c <- newAtLeastData lits' n' False
      attach solver c
      addToDB solver c

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

  (ts',degree) <- liftM normalizePBAtLeast $ instantiatePB solver (ts,n)
  let cs = map fst ts'
      slack = sum cs - degree

  if degree <= 0 then return ()
    else if slack < 0 then markBad solver
    else if Set.size (Set.fromList cs) == 1 then do
      let c = head cs
      addAtLeast solver (map snd ts') (fromInteger ((degree+c-1) `div` c))
    else do
      c <- newPBAtLeastData ts' degree False
      attach solver c
      addToDB solver c
      ret <- pbPropagate 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 normalizePBExactly $ 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 normalizePBAtLeast $ 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 normalizePBExactly $ 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 <- nClauses 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 $ dumpClaActivity 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 = loop 0
  where
    loop :: Int -> IO SearchResult
    loop !c = do
      sanityCheck solver
      conflict <- deduce solver
      sanityCheck solver

      case conflict of
        Nothing -> do
          lv <- readIORef (svLevel solver)
          when (lv == levelRoot) $ simplify solver

          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

          r <- pickAssumption
          case r of
            Nothing -> return (SRFinished False)
            Just lit
              | lit /= litUndef -> decide solver lit >> loop c
              | otherwise -> do
                  lit2 <- pickBranchLit solver
                  if lit2 == litUndef
                    then return (SRFinished True)
                    else decide solver lit2 >> loop c

        Just constr -> do
          varDecayActivity solver
          constrDecayActivity solver
          onConflict

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

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

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

          modifyIORef' (svConfBudget solver) $ \confBudget ->
            if confBudget > 0 then confBudget - 1 else confBudget
          confBudget <- readIORef (svConfBudget solver)

          if d == levelRoot
            then markBad solver >> return (SRFinished False)
            else if confBudget==0 then
              return SRBudgetExceeded
            else if conflict_lim >= 0 && c+1 >= conflict_lim then
              return SRRestart
            else do
              b <- handleConflict constr
              if b
                then loop (c+1)
                else markBad solver >> return (SRFinished False)

    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 :: SomeConstraint -> IO Bool
    handleConflict constr = do
      strat <- readIORef (svLearningStrategy solver)
      case strat of
        LearningClause -> 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 <- newClauseData learntClause True
              attach solver cl
              addToLearntDB solver cl
              assignBy solver lit cl
              constrBumpActivity solver cl
          return True
        LearningHybrid -> do
          (learntClause, level, pb) <- analyzeConflictHybrid solver constr
          level2 <- pbBacktrackLevel solver pb
          let level3 = min level level2

          pbdata <- newPBAtLeastData (fst pb) (snd pb) True
          attach solver pbdata
          addToLearntDB solver pbdata

          backtrackTo solver level3
          slack <- readIORef (pbSlack pbdata)
          if slack < 0
            then do
              if level3 == levelRoot
               then return False
               else handleConflict (toConstraint pbdata)
            else do
              case learntClause of
                [] -> error "search(LearningHybrid): should not happen"
                [lit] -> do
                  ret <- assign solver lit
                  assert ret $ return ()
                  return ()
                lit:_ -> do
                  cl <- newClauseData learntClause True
                  attach solver cl
                  addToLearntDB solver cl
                  when (level3 == level) $ do
                    assignBy solver lit cl
                    constrBumpActivity solver cl
              pbPropagate solver pbdata
              return True

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

-- | Simplify the clause 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 (svClauseDB solver)
    (ys,n) <- loop xs [] (0::Int)
    modifyIORef' (svNRemovedConstr solver) (+n)
    writeIORef (svClauseDB solver) ys

  -- simplify learnt constraint DB
  do
    (m,xs) <- readIORef (svLearntDB solver)
    (ys,n) <- loop xs [] (0::Int)
    writeIORef (svLearntDB solver) (m-n, 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

-- | Used by the random variable selection
setRandomSeed :: Solver -> Int -> IO ()
setRandomSeed solver seed = do
  writeIORef (svRandomGen solver) (Rand.mkStdGen seed)

setConfBudget :: Solver -> Maybe Int -> IO ()
setConfBudget solver (Just b) | b >= 0 = writeIORef (svConfBudget solver) b
setConfBudget solver _ = writeIORef (svConfBudget solver) (-1)

{--------------------------------------------------------------------
  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 SomeConstraint)
deduce solver = loop
  where
    loop :: IO (Maybe SomeConstraint)
    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 SomeConstraint)
    processLit !lit = do
      let lit2 = litNot lit
      ld <- litData solver lit2
      let wsref = ldWatches ld
      let loop2 [] = return Nothing
          loop2 (w:ws) = do
            ok <- propagate solver w lit2
            if ok
              then loop2 ws
              else do
                modifyIORef wsref (++ws)
                return (Just w)
      ws <- readIORef wsref
      writeIORef wsref []
      loop2 ws

analyzeConflict :: Constraint 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 :: Constraint c => Solver -> c -> IO (Clause, Level, ([(Integer,Lit)], Integer))
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 -> ([(Integer,Lit)],Integer) -> IO (LitSet, ([(Integer,Lit)],Integer))
      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)

                    pb2 <- toPBAtLeast solver constr2
                    o <- pbOverSAT solver pb2
                    let pb3 = if o then ([(1,l2) | l2 <- l:xs],1) else pb2
                    let pb' =
                           if any (\(_,l2) -> litNot l == l2) (fst pb)
                           then cutResolve pb pb3 (litVar l)
                           else 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
  return (map fst xs, level, pb)

pbBacktrackLevel :: Solver -> ([(Integer,Lit)],Integer) -> IO Level
pbBacktrackLevel _ ([], rhs) = assert (rhs > 0) $ return levelRoot
pbBacktrackLevel solver (lhs, rhs) = do
  let go lvs lhs' s = 
        case IS.minView lvs of
          Nothing -> error "pbBacktrackLevel: should not happen"
          Just (lv2, lvs2) -> do
            let s2   = s - sum [c | (c,_,lv3) <- lhs', Just lv2 == lv3]
                lhs2 = [x | x@(_,_,lv3) <- lhs', Just lv2 /= lv3]
            if s2 < 0 then
              return lv2 -- conflict
            else if takeWhile (\(c,_,_) -> c > s) lhs2 /= [] then
              return lv2 --unit
            else
              go lvs2 lhs2 s2

  lhs' <- forM (sortBy (flip (comparing fst)) lhs) $ \(c, lit) -> do
    v <- litValue solver lit
    if v /= lFalse
      then return (c, lit, Nothing)
      else do
        lv <- litLevel solver lit
        return (c, lit, Just lv)

  let lvs = IS.fromList [lv | (_,_,Just lv) <- lhs']
      s0 = sum [c | (c,_) <- lhs] - rhs
  go lvs lhs' s0

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)
  forM_ [1..n] $ \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 (svClaDecay solver)
  modifyIORef' (svClaInc solver) (d*)

constrRescaleAllActivity :: Solver -> IO ()
constrRescaleAllActivity solver = do
  xs <- learntConstraints solver
  forM_ xs $ \c -> constrRescaleActivity solver c
  modifyIORef' (svClaInc 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 Constraint a where
  toConstraint :: a -> SomeConstraint

  showConstraint :: Solver -> a -> IO String

  attach :: Solver -> a -> IO ()

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

  -- | invoked with the watched literal when the literal is falsified.
  -- 'watch' で 'toConstraint' を呼び出して heap allocation が発生するのを
  -- 避けるために、元の 'SomeConstraint' も渡しておく。
  basicPropagate :: Solver -> SomeConstraint -> 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 ([(Integer,Lit)], Integer)

  isSatisfied :: Solver -> a -> IO Bool

  constrIsProtected :: Solver -> a -> IO Bool
  constrIsProtected _ _ = return False

  constrActivity :: Solver -> a -> IO Double

  constrBumpActivity :: Solver -> a -> IO ()
  constrBumpActivity _ _ = return ()

  constrRescaleActivity :: Solver -> a -> IO ()
  constrRescaleActivity _ _ = return ()

detach :: Constraint a => Solver -> a -> IO ()
detach solver c = do
  let c2 = toConstraint c
  lits <- watchedLiterals solver c
  forM_ lits $ \lit -> do
    ld <- litData solver lit
    modifyIORef' (ldWatches ld) (delete c2)

-- | invoked with the watched literal when the literal is falsified.
propagate :: Solver -> SomeConstraint -> 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 :: Constraint 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 <- showConstraint 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 <- showConstraint 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 -> SomeConstraint -> 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 SomeConstraint
  = ConstrClause !ClauseData
  | ConstrAtLeast !AtLeastData
  | ConstrPBAtLeast !PBAtLeastData
  deriving Eq

instance Constraint SomeConstraint where
  toConstraint = id

  showConstraint s (ConstrClause c)    = showConstraint s c
  showConstraint s (ConstrAtLeast c)   = showConstraint s c
  showConstraint s (ConstrPBAtLeast c) = showConstraint s c

  attach s (ConstrClause c)    = attach s c
  attach s (ConstrAtLeast c)   = attach s c
  attach s (ConstrPBAtLeast c) = attach s c

  watchedLiterals s (ConstrClause c)    = watchedLiterals s c
  watchedLiterals s (ConstrAtLeast c)   = watchedLiterals s c
  watchedLiterals s (ConstrPBAtLeast c) = watchedLiterals s c

  basicPropagate s this (ConstrClause c)  lit   = basicPropagate s this c lit
  basicPropagate s this (ConstrAtLeast c) lit   = basicPropagate s this c lit
  basicPropagate s this (ConstrPBAtLeast c) lit = basicPropagate s this c lit

  basicReasonOf s (ConstrClause c)  l   = basicReasonOf s c l
  basicReasonOf s (ConstrAtLeast c) l   = basicReasonOf s c l
  basicReasonOf s (ConstrPBAtLeast c) l = basicReasonOf s c l

  toPBAtLeast s (ConstrClause c)    = toPBAtLeast s c
  toPBAtLeast s (ConstrAtLeast c)   = toPBAtLeast s c
  toPBAtLeast s (ConstrPBAtLeast c) = toPBAtLeast s c

  isSatisfied s (ConstrClause c)    = isSatisfied s c
  isSatisfied s (ConstrAtLeast c)   = isSatisfied s c
  isSatisfied s (ConstrPBAtLeast c) = isSatisfied s c

  constrIsProtected s (ConstrClause c)    = constrIsProtected s c
  constrIsProtected s (ConstrAtLeast c)   = constrIsProtected s c
  constrIsProtected s (ConstrPBAtLeast c) = constrIsProtected s c

  constrActivity s (ConstrClause c)    = constrActivity s c
  constrActivity s (ConstrAtLeast c)   = constrActivity s c
  constrActivity s (ConstrPBAtLeast c) = constrActivity s c

  constrBumpActivity s (ConstrClause c)    = constrBumpActivity s c
  constrBumpActivity s (ConstrAtLeast c)   = constrBumpActivity s c
  constrBumpActivity s (ConstrPBAtLeast c) = constrBumpActivity s c

  constrRescaleActivity s (ConstrClause c)    = constrRescaleActivity s c
  constrRescaleActivity s (ConstrAtLeast c)   = constrRescaleActivity s c
  constrRescaleActivity s (ConstrPBAtLeast c) = constrRescaleActivity s c

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

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

instance Eq ClauseData where
  c1 == c2 = claActivity c1 == claActivity c2

newClauseData :: Clause -> Bool -> IO ClauseData
newClauseData ls learnt = do
  let size = length ls
  a <- newListArray (0, size-1) ls
  act <- newIORef $! (if learnt then 0 else -1)
  return (ClauseData a act)

instance Constraint ClauseData where
  toConstraint = ConstrClause

  showConstraint _ this = do
    lits <- getElems (claLits this)
    return (show lits)

  attach solver this = do
    lits <- getElems (claLits this)
    case lits of
      l1:l2:_ -> do
        watch solver l1 this
        watch solver l2 this
      _ -> return ()

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

  basicPropagate !s this this2 !falsifiedLit = do
    preprocess

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

      -- Maybe を heap allocation するのを避けるために、
      -- 見つからなかったときは -1 を返すことに。
      findForWatch :: Int -> Int -> IO Int
      findForWatch i end | i > end = return (-1)
      findForWatch i end = do
        val <- litValue s =<< unsafeRead a i
        if val /= lFalse
          then return i
          else findForWatch (i+1) end

  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 _ (ClauseData a _) = do
    lits <- getElems a
    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

  constrActivity _ this = do
    let act = claActivity this
    readIORef act

  constrBumpActivity solver this = do
    let act = claActivity this
    aval <- readIORef act
    when (aval >= 0) $ do -- learnt clause
      inc <- readIORef (svClaInc solver)
      let aval2 = aval+inc
      writeIORef act $! aval2
      when (aval2 > 1e20) $
        -- Rescale
        constrRescaleAllActivity solver

  constrRescaleActivity _ this = do
    let act = claActivity this
    aval <- readIORef act
    when (aval >= 0) $ writeIORef act $! (aval * 1e-20)

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

{--------------------------------------------------------------------
  Cardinality Constraint
--------------------------------------------------------------------}

data AtLeastData
  = AtLeastData
  { atLeastLits :: IOUArray Int Lit
  , atLeastNum :: !Int
  , atLeastActivity :: !(IORef Double)
  }
  deriving Eq

newAtLeastData :: [Lit] -> Int -> Bool -> IO AtLeastData
newAtLeastData ls n learnt = do
  let size = length ls
  a <- newListArray (0, size-1) ls
  act <- newIORef $! (if learnt then 0 else -1)
  return (AtLeastData a n act)

instance Constraint AtLeastData where
  toConstraint = ConstrAtLeast

  showConstraint _ this = do
    lits <- getElems (atLeastLits this)
    return $ show lits ++ " >= " ++ show (atLeastNum this)

  attach solver this = do
    lits <- getElems (atLeastLits this)
    let n = atLeastNum this
    let ws = if length lits > n then take (n+1) lits else []
    forM_ ws $ \l -> watch solver l this

  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 s this this2 falsifiedLit = do
    preprocess

    when debugMode $ do
      litn <- readArray a n
      unless (litn == falsifiedLit) $ error "AtLeastData.basicPropagate: should not happen"

    (lb,ub) <- getBounds a
    assert (lb==0) $ return ()
    ret <- findForWatch (n+1) ub
    case ret of
      Nothing -> do
        when debugMode $ logIO s $ do
          str <- showConstraint s this
          return $ printf "basicPropagate: %s is unit" str
        watch s falsifiedLit this
        let loop :: Int -> IO Bool
            loop i
              | i >= n = return True
              | otherwise = do
                  liti <- readArray a i
                  ret2 <- assignBy s liti this
                  if ret2
                    then loop (i+1)
                    else return False
        loop 0
      Just i  -> do
        liti <- readArray a i
        litn <- readArray a n
        writeArray a i litn
        writeArray a n liti
        watch s 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 <- readArray a i
              if (li /= falsifiedLit)
                then loop (i+1)
                else do
                  ln <- readArray a n
                  writeArray a n li
                  writeArray a i ln

      findForWatch :: Int -> Int -> IO (Maybe Int)
      findForWatch i end | i > end = return Nothing
      findForWatch i end = do
        val <- litValue s =<< readArray a i
        if val /= lFalse
          then return (Just i)
          else findForWatch (i+1) end

  basicReasonOf s this concl = do
    lits <- getElems (atLeastLits this)
    let n = atLeastNum this
    case concl of
      Nothing -> do
        let f :: [Lit] -> IO Lit
            f [] = error "AtLeastData.basicReasonOf: should not happen"
            f (l:ls) = do
              val <- litValue s l
              if val == lFalse
                then return l
                else f ls
        lit <- f (take n lits)
        return $ lit : drop n lits
      Just lit -> do
        assert (lit `elem` take n lits) $ return ()
        return $ drop n lits

  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

  constrActivity _ this = do
    let act = atLeastActivity this
    readIORef act

  constrBumpActivity solver this = do
    let act = atLeastActivity this
    aval <- readIORef act
    when (aval >= 0) $ do -- learnt clause
      inc <- readIORef (svClaInc solver)
      let aval2 = aval+inc
      writeIORef act $! aval2
      when (aval2 > 1e20) $
        -- Rescale
        constrRescaleAllActivity solver

  constrRescaleActivity _ this = do
    let act = atLeastActivity this
    aval <- readIORef act
    when (aval >= 0) $ writeIORef act $! (aval * 1e-20)

instantiateAtLeast :: Solver -> ([Lit],Int) -> IO ([Lit],Int)
instantiateAtLeast solver (xs,n) = loop ([],n) xs
  where
    loop :: ([Lit],Int) -> [Lit] -> IO ([Lit],Int)
    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

{--------------------------------------------------------------------
  Pseudo Boolean Constraint
--------------------------------------------------------------------}

data PBAtLeastData
  = PBAtLeastData
  { pbTerms  :: !(LitMap Integer)
  , pbDegree :: !Integer
  , pbSlack  :: !(IORef Integer)
  , pbActivity :: !(IORef Double)
  , pbReasons :: !(IORef (LitMap [(Lit, Integer)]))
  }
  deriving Eq

newPBAtLeastData :: [(Integer,Lit)] -> Integer -> Bool -> IO PBAtLeastData
newPBAtLeastData ts degree learnt = do
  let 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)
  rs <- newIORef IM.empty
  return (PBAtLeastData m degree s act rs)

instance Constraint PBAtLeastData where
  toConstraint = ConstrPBAtLeast

  showConstraint _ this = do
    return $ show [(c,l) | (l,c) <- IM.toList (pbTerms this)] ++ " >= " ++ show (pbDegree this)

  attach solver this = do
    forM_ (IM.keys (pbTerms this)) $ \l -> watch solver l this
    cs <- forM (IM.toList (pbTerms this)) $ \(l,c) -> do
      v <- litValue solver l
      if v == lFalse
        then do
          addBacktrackCB solver (litVar l) $ modifyIORef' (pbSlack this) (+ c)
          return 0
        else return c
    writeIORef (pbSlack this) $! sum cs - pbDegree this

  watchedLiterals _ this = do
    return $ IM.keys $ pbTerms this

  basicPropagate solver this this2 falsifiedLit = do
    watch solver falsifiedLit this
    let c = pbTerms this2 IM.! falsifiedLit
    let slack = pbSlack this2
    modifyIORef' slack (subtract c)
    addBacktrackCB solver (litVar falsifiedLit) $ modifyIORef' slack (+ c)
    pbPropagate solver this2

  basicReasonOf solver this l = do
    let m = pbTerms this
    xs <-
      case l of
        Just lit -> do
          -- 保存しておいたものを使わないと、
          -- その後に割り当てられたものを含んでしまってまずいことがある。
          rs <- readIORef (pbReasons this)
          return $ sortBy (flip (comparing snd)) $ (rs IM.! lit)
        Nothing -> do
          -- 直接のコンフリクトの場合には現在のもので大丈夫なはず
          tmp <- filterM (\(lit,_) -> liftM (lFalse ==) (litValue solver lit)) (IM.toList m)
          return $ sortBy (flip (comparing snd)) $ tmp
    let max_slack = sum (map snd $ IM.toList m) - pbDegree this
    case l of
      Nothing -> return $ f max_slack xs
      Just lit -> return $ f (max_slack - (m IM.! lit)) xs
    where
      f :: Integer -> [(Lit,Integer)] -> [Lit]
      f s xs = go s xs []

      go :: Integer -> [(Lit,Integer)] -> [Lit] -> [Lit]
      go s _ ret | s < 0 = ret
      go _ [] _ = error "PBAtLeastData.basicReasonOf: should not happen"
      go s ((lit,c):xs) ret = go (s - c) xs (lit:ret)

  toPBAtLeast _ this = do
    return ([(c,l) | (l,c) <- IM.toList (pbTerms this)], pbDegree this)

  isSatisfied solver this = do
    xs <- forM (IM.toList (pbTerms this)) $ \(l,c) -> do
      v <- litValue solver l
      if v == lTrue
        then return c
        else return 0
    return $ sum xs >= pbDegree this

  constrActivity _ this = do
    let act = pbActivity this
    readIORef act

  constrBumpActivity solver this = do
    let act = pbActivity this
    aval <- readIORef act
    when (aval >= 0) $ do -- learnt clause
      inc <- readIORef (svClaInc solver)
      let aval2 = aval+inc
      writeIORef act $! aval2
      when (aval2 > 1e20) $
        -- Rescale
        constrRescaleAllActivity solver

  constrRescaleActivity _ this = do
    let act = pbActivity this
    aval <- readIORef act
    when (aval >= 0) $ writeIORef act $! (aval * 1e-20)

instantiatePB :: Solver -> ([(Integer,Lit)],Integer) -> IO ([(Integer,Lit)],Integer)
instantiatePB solver (xs,n) = loop ([],n) xs
  where
    loop :: ([(Integer,Lit)],Integer) -> [(Integer,Lit)] -> IO ([(Integer,Lit)],Integer)
    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

pbPropagate :: Solver -> PBAtLeastData -> IO Bool
pbPropagate solver this = do
  let slack = pbSlack this
  s <- readIORef slack
  if s < 0
    then return False
    else do
      ref <- newIORef Nothing
      let m = do
            x <- readIORef ref
            case x of
              Just r -> return r
              Nothing -> do
                let isFalse (l,_) = liftM (lFalse==) (litValue solver l)
                r <- filterM isFalse $ IM.toAscList $ pbTerms this
                writeIORef ref (Just r)
                return r

      forM_ (IM.toList (pbTerms this)) $ \(l1,c1) -> do
        when (c1 > s) $ do
          v <- litValue solver l1
          when (v == lUndef) $ do
            -- あとでbasicReasonOfで使うために、
            -- その時点でfalseになっているリテラルを保存しておく
            r <- m
            modifyIORef (pbReasons this) (IM.insert l1 r)

            assignBy solver l1 this
            constrBumpActivity solver this
            return ()

      return True

pbOverSAT :: Solver -> ([(Integer,Lit)],Integer) -> 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

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

{--------------------------------------------------------------------
  debug
--------------------------------------------------------------------}

debugMode :: Bool
debugMode = False

checkSatisfied :: Solver -> IO ()
checkSatisfied solver = do
  cls <- readIORef (svClauseDB solver)
  forM_ cls $ \c -> do
    b <- isSatisfied solver c
    unless b $ do
      s <- showConstraint solver c
      log solver $ "BUG: " ++ s ++ " is violated"

sanityCheck :: Solver -> IO ()
sanityCheck _ | not debugMode = return ()
sanityCheck solver = do
  cls <- readIORef (svClauseDB 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

dumpClaActivity :: Solver -> IO ()
dumpClaActivity solver = do
  log solver "Learnt clause activity:"
  xs <- learntConstraints solver
  forM_ xs $ \c -> do
    s <- showConstraint solver c
    aval <- constrActivity solver 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