msakai / toysolver / 767

Committed 22 May 2025 12:57PM UTC coverage: 71.847% (-0.06%) from 71.906%

Build # 767

Build Type

push

github

Committed by

web-flow

Commit Message

Merge f4d92f6d1 into c10d256d2

Run Details

11104 of 15455 relevant lines covered (71.85%)

0.72 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

74.45

/src/ToySolver/SAT/Solver/CDCL.hs

{-# OPTIONS_GHC -Wall -fno-warn-unused-do-bind #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE ScopedTypeVariables #-}
#ifdef __GLASGOW_HASKELL__
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}
#endif
#include "MachDeps.h"
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Solver.CDCL
-- Copyright   :  (c) Masahiro Sakai 2012-2014
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- A CDCL SAT solver.
--
-- It follows the design of MiniSat and SAT4J.
--
-- See also:
--
-- * <http://hackage.haskell.org/package/funsat>
--
-- * <http://hackage.haskell.org/package/incremental-sat-solver>
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Solver.CDCL
  (
  -- * The @Solver@ type
    Solver
  , newSolver
  , newSolverWithConfig

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

  -- * Problem specification
  , newVar
  , newVars
  , newVars_
  , resizeVarCapacity
  -- ** Clauses
  , AddClause (..)
  , Clause
  , evalClause
  , PackedClause
  , packClause
  , unpackClause
  -- ** Cardinality constraints
  , AddCardinality (..)
  , AtLeast
  , Exactly
  , evalAtLeast
  , evalExactly

  -- ** (Linear) pseudo-boolean constraints
  , AddPBLin (..)
  , PBLinTerm
  , PBLinSum
  , PBLinAtLeast
  , PBLinExactly
  , evalPBLinSum
  , evalPBLinAtLeast
  , evalPBLinExactly
  -- ** XOR clauses
  , AddXORClause (..)
  , XORClause
  , evalXORClause
  -- ** Type-2 SOS constraints
  , addSOS2
  , evalSOS2
  -- ** Theory
  , setTheory

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

  -- * Extract results
  , IModel (..)
  , Model
  , getModel
  , getFailedAssumptions
  , getAssumptionsImplications

  -- * Solver configulation
  , module ToySolver.SAT.Solver.CDCL.Config
  , getConfig
  , setConfig
  , modifyConfig
  , setVarPolarity
  , setRandomGen
  , getRandomGen
  , setConfBudget

  -- * Callbacks
  , setLogger
  , clearLogger
  , setTerminateCallback
  , clearTerminateCallback
  , setLearnCallback
  , clearLearnCallback

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

  -- * Internal API
  , varBumpActivity
  , varDecayActivity
  ) where

import Prelude hiding (log)
import Control.Loop
import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.Trans
import Control.Monad.Trans.Except
import Control.Exception
import Data.Array.IO
import Data.Array.Unsafe (unsafeFreeze)
import Data.Array.Base (unsafeRead, unsafeWrite)
#if !MIN_VERSION_hashable(1,4,3)
import Data.Bits (xor) -- for defining 'combine' function
#endif
import Data.Coerce
import Data.Default.Class
import Data.Either
import Data.Function (on)
import Data.Hashable
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import Data.IORef
import Data.Int
import Data.List (delete, find, foldl', maximumBy, partition, sortBy)
import Data.Maybe
import Data.Ord
import qualified Data.IntMap.Strict as IM
import qualified Data.IntSet as IS
import qualified Data.Set as Set
import ToySolver.Internal.Data.IOURef
import qualified ToySolver.Internal.Data.IndexedPriorityQueue as PQ
import qualified ToySolver.Internal.Data.Vec as Vec
import Data.Typeable
import System.Clock
import qualified System.Random.MWC as Rand
import Text.Printf

#ifdef __GLASGOW_HASKELL__
import GHC.Types (IO (..))
import GHC.Exts hiding (Constraint)
#endif

import ToySolver.Data.LBool
import ToySolver.SAT.Solver.CDCL.Config
import ToySolver.SAT.Types
import ToySolver.SAT.TheorySolver
import ToySolver.Internal.Util (revMapM)

{--------------------------------------------------------------------
  LitArray
--------------------------------------------------------------------}

newtype LitArray = LitArray (IOUArray Int PackedLit) deriving (Eq)

newLitArray :: [Lit] -> IO LitArray
newLitArray lits = do
  let size = length lits
  liftM LitArray $ newListArray (0, size-1) (map packLit lits)

readLitArray :: LitArray -> Int -> IO Lit
#if EXTRA_BOUNDS_CHECKING
readLitArray (LitArray a) i = liftM unpackLit $ readArray a i
#else
readLitArray (LitArray a) i = liftM unpackLit $ unsafeRead a i
#endif

writeLitArray :: LitArray -> Int -> Lit -> IO ()
#if EXTRA_BOUNDS_CHECKING
writeLitArray (LitArray a) i lit = writeArray a i (packLit lit)
#else
writeLitArray (LitArray a) i lit = unsafeWrite a i (packLit lit)
#endif

getLits :: LitArray -> IO [Lit]
getLits (LitArray a) = liftM (map unpackLit) $ getElems a

getLitArraySize :: LitArray -> IO Int
getLitArraySize (LitArray a) = do
  (lb,ub) <- getBounds a
  assert (lb == 0) $ return ()
  return $! ub-lb+1

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

type Level = Int

levelRoot :: Level
levelRoot = 0

litIndex :: Lit -> Int
litIndex l = 2 * (litVar l - 1) + (if litPolarity l then 1 else 0)

{-# INLINE varValue #-}
varValue :: Solver -> Var -> IO LBool
varValue solver v = liftM coerce $ Vec.unsafeRead (svVarValue solver) (v - 1)

{-# INLINE litValue #-}
litValue :: Solver -> Lit -> IO LBool
litValue solver !l = do
  -- litVar による heap allocation を避けるために、
  -- litPolarityによる分岐後にvarValueを呼ぶ。
  if litPolarity l then
    varValue solver l
  else do
    m <- varValue solver (negate l)
    return $! lnot m

getVarFixed :: Solver -> Var -> IO LBool
getVarFixed solver !v = do
  lv <- Vec.unsafeRead (svVarLevel solver) (v - 1)
  if lv == levelRoot then
    varValue solver v
  else
    return lUndef

getLitFixed :: Solver -> Lit -> IO LBool
getLitFixed solver !l = do
  -- litVar による heap allocation を避けるために、
  -- litPolarityによる分岐後にvarGetFixedを呼ぶ。
  if litPolarity l then
    getVarFixed solver l
  else do
    m <- getVarFixed solver (negate l)
    return $! lnot m

getNFixed :: Solver -> IO Int
getNFixed solver = do
  lv <- getDecisionLevel solver
  if lv == levelRoot then
    Vec.getSize (svTrail solver)
  else
    Vec.unsafeRead (svTrailLimit solver) 0

-- | it returns a set of literals that are fixed without any assumptions.
getFixedLiterals :: Solver -> IO [Lit]
getFixedLiterals solver = do
  n <- getNFixed solver
  revMapM (Vec.unsafeRead (svTrail solver)) [0..n-1]

varLevel :: Solver -> Var -> IO Level
varLevel solver !v = do
  val <- varValue solver v
  when (val == lUndef) $ error ("ToySolver.SAT.varLevel: unassigned var " ++ show v)
  Vec.unsafeRead (svVarLevel solver) (v - 1)

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

varReason :: Solver -> Var -> IO (Maybe SomeConstraintHandler)
varReason solver !v = do
  val <- varValue solver v
  when (val == lUndef) $ error ("ToySolver.SAT.varReason: unassigned var " ++ show v)
  Vec.unsafeRead (svVarReason solver) (v - 1)

varAssignNo :: Solver -> Var -> IO Int
varAssignNo solver !v = do
  val <- varValue solver v
  when (val == lUndef) $ error ("ToySolver.SAT.varAssignNo: unassigned var " ++ show v)
  Vec.unsafeRead (svVarTrailIndex solver) (v - 1)

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

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

  -- variable information
  , svVarValue      :: !(Vec.UVec Int8) -- should be 'Vec.UVec LBool' but it's difficult to define MArray instance
  , svVarPolarity   :: !(Vec.UVec Bool)
  , svVarActivity   :: !(Vec.UVec VarActivity)
  , svVarTrailIndex :: !(Vec.UVec Int)
  , svVarLevel      :: !(Vec.UVec Int)
  -- | will be invoked once when the variable is assigned
  , svVarWatches      :: !(Vec.Vec [SomeConstraintHandler])
  , svVarOnUnassigned :: !(Vec.Vec [SomeConstraintHandler])
  , svVarReason       :: !(Vec.Vec (Maybe SomeConstraintHandler))
  -- | exponential moving average estimate
  , svVarEMAScaled    :: !(Vec.UVec Double)
  -- | When v was last assigned
  , svVarWhenAssigned :: !(Vec.UVec Int)
  -- | The number of learnt clauses v participated in generating since Assigned.
  , svVarParticipated :: !(Vec.UVec Int)
  -- | The number of learnt clauses v reasoned in generating since Assigned.
  , svVarReasoned     :: !(Vec.UVec Int)

  -- | will be invoked when this literal is falsified
  , svLitWatches   :: !(Vec.Vec [SomeConstraintHandler])
  , svLitOccurList :: !(Vec.Vec (HashSet SomeConstraintHandler))

  , svConstrDB     :: !(IORef [SomeConstraintHandler])
  , svLearntDB     :: !(IORef (Int,[SomeConstraintHandler]))

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

  -- Result
  , svModel        :: !(IORef (Maybe Model))
  , svFailedAssumptions :: !(IORef LitSet)
  , svAssumptionsImplications :: !(IORef LitSet)

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

  -- Configulation
  , svConfig :: !(IORef Config)
  , svRandomGen  :: !(IORef Rand.GenIO)
  , svConfBudget :: !(IOURef Int)
  , svTerminateCallback :: !(IORef (Maybe (IO Bool)))
  , svLearnCallback :: !(IORef (Maybe (Clause -> IO ())))

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

  -- Working spaces
  , svCanceled        :: !(IORef Bool)
  , svAssumptions     :: !(Vec.UVec Lit)
  , svLearntLim       :: !(IORef Int)
  , svLearntLimAdjCnt :: !(IORef Int)
  , svLearntLimSeq    :: !(IORef [(Int,Int)])
  , svSeen :: !(Vec.UVec Bool)
  , svPBLearnt :: !(IORef (Maybe PBLinAtLeast))

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

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

  -- ERWA / LRB

  -- | step-size parameter α
  , svERWAStepSize :: !(IOURef Double)
  , svEMAScale :: !(IOURef Double)
  , svLearntCounter :: !(IOURef Int)
  }

markBad :: Solver -> IO ()
markBad solver = do
  writeIORef (svOk solver) False
  bcpClear solver

bcpDequeue :: Solver -> IO (Maybe Lit)
bcpDequeue solver = do
  n <- Vec.getSize (svTrail solver)
  m <- readIOURef (svTrailNPropagated solver)
  if m==n then
    return Nothing
  else do
    -- m < n
    lit <- Vec.unsafeRead (svTrail solver) m
    modifyIOURef (svTrailNPropagated solver) (+1)
    return (Just lit)

bcpIsEmpty :: Solver -> IO Bool
bcpIsEmpty solver = do
  p <- readIOURef (svTrailNPropagated solver)
  n <- Vec.getSize (svTrail solver)
  return $! n == p

bcpCheckEmpty :: Solver -> IO ()
bcpCheckEmpty solver = do
  empty <- bcpIsEmpty solver
  unless empty $
    error "BUG: BCP Queue should be empty at this point"

bcpClear :: Solver -> IO ()
bcpClear solver = do
  m <- Vec.getSize (svTrail solver)
  writeIOURef (svTrailNPropagated solver) m

assignBy :: Solver -> Lit -> SomeConstraintHandler -> IO Bool
assignBy solver lit c = do
  lv <- getDecisionLevel solver
  let !c2 = if lv == levelRoot
            then Nothing
            else Just c
  assign_ solver lit c2

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

assign_ :: Solver -> Lit -> Maybe SomeConstraintHandler -> IO Bool
assign_ solver !lit reason = assert (validLit lit) $ do
  let val = liftBool (litPolarity lit)

  val0 <- varValue solver (litVar lit)
  if val0 /= lUndef then do
    return $ val == val0
  else do
    idx <- Vec.getSize (svTrail solver)
    lv <- getDecisionLevel solver

    Vec.unsafeWrite (svVarValue solver) (litVar lit - 1) (coerce val)
    Vec.unsafeWrite (svVarTrailIndex solver) (litVar lit - 1) idx
    Vec.unsafeWrite (svVarLevel solver) (litVar lit - 1) lv
    Vec.unsafeWrite (svVarReason solver) (litVar lit - 1) reason
    Vec.unsafeWrite (svVarWhenAssigned solver) (litVar lit - 1) =<< readIOURef (svLearntCounter solver)
    Vec.unsafeWrite (svVarParticipated solver) (litVar lit - 1) 0
    Vec.unsafeWrite (svVarReasoned solver) (litVar lit - 1) 0

    Vec.push (svTrail solver) lit

    when debugMode $ logIO solver $ do
      let r = case reason of
                Nothing -> ""
                Just _ -> " by propagation"
      return $ printf "assign(level=%d): %d%s" lv lit r

    return True

unassign :: Solver -> Var -> IO ()
unassign solver !v = assert (validVar v) $ do
  val <- varValue solver v
  when (val == lUndef) $ error "unassign: should not happen"

  flag <- configEnablePhaseSaving <$> getConfig solver
  when flag $ Vec.unsafeWrite (svVarPolarity solver) (v - 1) $! fromJust (unliftBool val)

  Vec.unsafeWrite (svVarValue solver) (v - 1) (coerce lUndef)
  Vec.unsafeWrite (svVarTrailIndex solver) (v - 1) maxBound
  Vec.unsafeWrite (svVarLevel solver) (v - 1) maxBound
  Vec.unsafeWrite (svVarReason solver) (v - 1) Nothing

  -- ERWA / LRB computation
  interval <- do
    t2 <- readIOURef (svLearntCounter solver)
    t1 <- Vec.unsafeRead (svVarWhenAssigned solver) (v - 1)
    return (t2 - t1)
  -- Interval = 0 is possible due to restarts.
  when (interval > 0) $ do
    participated <- Vec.unsafeRead (svVarParticipated solver) (v - 1)
    reasoned <- Vec.unsafeRead (svVarReasoned solver) (v - 1)
    alpha <- readIOURef (svERWAStepSize solver)
    let learningRate = fromIntegral participated / fromIntegral interval
        reasonSideRate = fromIntegral reasoned / fromIntegral interval
    scale <- readIOURef (svEMAScale solver)
    -- ema := (1 - α)ema + α*r
    Vec.unsafeModify (svVarEMAScaled solver) (v - 1) (\orig -> (1 - alpha) * orig + alpha * scale * (learningRate + reasonSideRate))
    -- If v is assigned by random decision, it's possible that v is still in the queue.
    PQ.update (svVarQueue solver) v

  let !l = if val == lTrue then v else -v
  cs <- Vec.unsafeRead (svVarOnUnassigned solver) (v - 1)
  Vec.unsafeWrite (svVarOnUnassigned solver) (v - 1) []
  forM_ cs $ \c ->
    constrOnUnassigned solver c c l

  PQ.enqueue (svVarQueue solver) v

addOnUnassigned :: Solver -> SomeConstraintHandler -> Lit -> IO ()
addOnUnassigned solver constr !l = do
  val <- varValue solver (litVar l)
  when (val == lUndef) $ error "addOnUnassigned: should not happen"
  Vec.unsafeModify (svVarOnUnassigned solver) (litVar l - 1) (constr :)

-- | Register the constraint to be notified when the literal becames false.
watchLit :: Solver -> Lit -> SomeConstraintHandler -> IO ()
watchLit solver !lit c = Vec.unsafeModify (svLitWatches solver) (litIndex lit) (c : )

-- | Register the constraint to be notified when the variable is assigned.
watchVar :: Solver -> Var -> SomeConstraintHandler -> IO ()
watchVar solver !var c = Vec.unsafeModify (svVarWatches solver) (var - 1) (c :)

unwatchLit :: Solver -> Lit -> SomeConstraintHandler -> IO ()
unwatchLit solver !lit c = Vec.unsafeModify (svLitWatches solver) (litIndex lit) (delete c)

unwatchVar :: Solver -> Lit -> SomeConstraintHandler -> IO ()
unwatchVar solver !var c = Vec.unsafeModify (svVarWatches solver) (var - 1) (delete c)

addToDB :: ConstraintHandler c => Solver -> c -> IO ()
addToDB solver c = do
  let c2 = toConstraintHandler c
  modifyIORef (svConstrDB solver) (c2 : )
  when debugMode $ logIO solver $ do
    str <- showConstraintHandler c
    return $ printf "constraint %s is added" str

  b <- isPBRepresentable c
  when b $ do
    (lhs,_) <- toPBLinAtLeast c
    forM_ lhs $ \(_,lit) -> do
       Vec.unsafeModify (svLitOccurList solver) (litIndex lit) (HashSet.insert c2)

addToLearntDB :: ConstraintHandler c => Solver -> c -> IO ()
addToLearntDB solver c = do
  modifyIORef (svLearntDB solver) $ \(n,xs) -> (n+1, toConstraintHandler c : xs)
  when debugMode $ logIO solver $ do
    str <- showConstraintHandler c
    return $ printf "constraint %s is added" str

reduceDB :: Solver -> IO ()
reduceDB solver = do
  (_,cs) <- readIORef (svLearntDB solver)

  xs <- forM cs $ \c -> do
    p <- constrIsProtected solver c
    w <- constrWeight solver c
    actval <- constrReadActivity c
    return (c, (p, w*actval))

  -- Note that False <= True
  let ys = sortBy (comparing snd) xs
      (zs,ws) = splitAt (length ys `div` 2) ys

  let loop [] ret = return ret
      loop ((c,(isShort,_)) : rest) ret = do
        flag <- if isShort
                then return True
                else isLocked solver c
        if flag then
          loop rest (c:ret)
        else do
          detach solver c
          loop rest ret
  zs2 <- loop zs []

  let cs2 = zs2 ++ map fst ws
      n2 = length cs2

  -- log solver $ printf "learnt constraints deletion: %d -> %d" n n2
  writeIORef (svLearntDB solver) (n2,cs2)

type VarActivity = Double

varActivity :: Solver -> Var -> IO VarActivity
varActivity solver v = Vec.unsafeRead (svVarActivity solver) (v - 1)

varDecayActivity :: Solver -> IO ()
varDecayActivity solver = do
  d <- configVarDecay <$> getConfig solver
  modifyIOURef (svVarInc solver) (d*)

varBumpActivity :: Solver -> Var -> IO ()
varBumpActivity solver !v = do
  inc <- readIOURef (svVarInc solver)
  Vec.unsafeModify (svVarActivity solver) (v - 1) (+inc)
  conf <- getConfig solver
  when (configBranchingStrategy conf == BranchingVSIDS) $ do
    PQ.update (svVarQueue solver) v
  aval <- Vec.unsafeRead (svVarActivity solver) (v - 1)
  when (aval > 1e20) $
    -- Rescale
    varRescaleAllActivity solver

varRescaleAllActivity :: Solver -> IO ()
varRescaleAllActivity solver = do
  let a = svVarActivity solver
  n <- getNVars solver
  forLoop 0 (<n) (+1) $ \i ->
    Vec.unsafeModify a i (* 1e-20)
  modifyIOURef (svVarInc solver) (* 1e-20)

varEMAScaled :: Solver -> Var -> IO Double
varEMAScaled solver v = Vec.unsafeRead (svVarEMAScaled solver) (v - 1)

varIncrementParticipated :: Solver -> Var -> IO ()
varIncrementParticipated solver v = Vec.unsafeModify (svVarParticipated solver) (v - 1) (+1)

varIncrementReasoned :: Solver -> Var -> IO ()
varIncrementReasoned solver v = Vec.unsafeModify (svVarReasoned solver) (v - 1) (+1)

varEMADecay :: Solver -> IO ()
varEMADecay solver = do
  config <- getConfig solver

  alpha <- readIOURef (svERWAStepSize solver)
  let alphaMin = configERWAStepSizeMin config
  when (alpha > alphaMin) $ do
    writeIOURef (svERWAStepSize solver) (max alphaMin (alpha - configERWAStepSizeDec config))

  case configBranchingStrategy config of
    BranchingLRB -> do
      modifyIOURef (svEMAScale solver) (configEMADecay config *)
      scale <- readIOURef (svEMAScale solver)
      when (scale > 1e20) $ do
        n <- getNVars solver
        let a = svVarEMAScaled solver
        forLoop 0 (<n) (+1) $ \i -> Vec.unsafeModify a i (/ scale)
        writeIOURef (svEMAScale solver) 1.0
    _ -> return ()

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

-- | number of variables of the problem.
getNVars :: Solver -> IO Int
getNVars solver = Vec.getSize (svVarValue solver)

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

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

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

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

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

-- | Create a new 'Solver' instance.
newSolver :: IO Solver
newSolver = newSolverWithConfig def

-- | Create a new 'Solver' instance with a given configulation.
newSolverWithConfig :: Config -> IO Solver
newSolverWithConfig config = do
 rec
  ok   <- newIORef True
  trail <- Vec.new
  trail_lim <- Vec.new
  trail_nprop <- newIOURef 0

  varValue <- Vec.new
  varPolarity <- Vec.new
  varActivity <- Vec.new
  varTrailIndex <- Vec.new
  varLevel <- Vec.new
  varWatches <- Vec.new
  varOnUnassigned <- Vec.new
  varReason <- Vec.new
  varEMAScaled <- Vec.new
  varWhenAssigned <- Vec.new
  varParticipated <- Vec.new
  varReasoned <- Vec.new
  litWatches <- Vec.new
  litOccurList <- Vec.new

  vqueue <- PQ.newPriorityQueueBy (ltVar solver)
  db  <- newIORef []
  db2 <- newIORef (0,[])
  as  <- Vec.new
  m   <- newIORef Nothing
  canceled <- newIORef False
  ndecision <- newIOURef 0
  nranddec  <- newIOURef 0
  nconflict <- newIOURef 0
  nrestart  <- newIOURef 0
  nlearntgc <- newIOURef 0
  nremoved  <- newIOURef 0

  constrInc   <- newIOURef 1
  varInc   <- newIOURef 1

  configRef <- newIORef config

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

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

  randgen  <- newIORef =<< Rand.create

  failed <- newIORef IS.empty
  implied <- newIORef IS.empty

  confBudget <- newIOURef (-1)
  terminateCallback <- newIORef Nothing
  learntCallback <- newIORef Nothing

  tsolver <- newIORef Nothing
  tchecked <- newIOURef 0

  seen <- Vec.new
  pbLearnt <- newIORef Nothing

  alpha <- newIOURef 0.4
  emaScale <- newIOURef 1.0
  learntCounter <- newIOURef 0

  let solver =
        Solver
        { svOk = ok
        , svVarQueue   = vqueue
        , svTrail      = trail
        , svTrailLimit = trail_lim
        , svTrailNPropagated = trail_nprop

        , svVarValue        = varValue
        , svVarPolarity     = varPolarity
        , svVarActivity     = varActivity
        , svVarTrailIndex   = varTrailIndex
        , svVarLevel        = varLevel
        , svVarWatches      = varWatches
        , svVarOnUnassigned = varOnUnassigned
        , svVarReason       = varReason
        , svVarEMAScaled    = varEMAScaled
        , svVarWhenAssigned = varWhenAssigned
        , svVarParticipated = varParticipated
        , svVarReasoned     = varReasoned
        , svLitWatches      = litWatches
        , svLitOccurList    = litOccurList

        , svConstrDB   = db
        , svLearntDB   = db2

        -- Theory
        , svTheorySolver  = tsolver
        , svTheoryChecked = tchecked

        -- Result
        , svModel      = m
        , svFailedAssumptions = failed
        , svAssumptionsImplications = implied

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

        -- Configulation
        , svConfig     = configRef
        , svRandomGen  = randgen
        , svConfBudget = confBudget
        , svTerminateCallback = terminateCallback
        , svLearnCallback = learntCallback

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

        -- Working space
        , svCanceled        = canceled
        , svAssumptions     = as
        , svLearntLim       = learntLim
        , svLearntLimAdjCnt = learntLimAdjCnt
        , svLearntLimSeq    = learntLimSeq
        , svVarInc      = varInc
        , svConstrInc   = constrInc
        , svSeen = seen
        , svPBLearnt = pbLearnt

        , svERWAStepSize = alpha
        , svEMAScale = emaScale
        , svLearntCounter = learntCounter
        }
 return solver

ltVar :: Solver -> Var -> Var -> IO Bool
ltVar solver !v1 !v2 = do
  conf <- getConfig solver
  case configBranchingStrategy conf of
    BranchingVSIDS -> do
      a1 <- varActivity solver v1
      a2 <- varActivity solver v2
      return $! a1 > a2
    _ -> do -- BranchingERWA and BranchingLRB
      a1 <- varEMAScaled solver v1
      a2 <- varEMAScaled solver v1
      return $! a1 > a2

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

instance NewVar IO Solver where
  newVar :: Solver -> IO Var
  newVar solver = do
    n <- Vec.getSize (svVarValue solver)
#if SIZEOF_HSINT > 4
    when (n == fromIntegral (maxBound :: PackedLit)) $ do
      error "cannot allocate more variables"
#endif
    let v = n + 1

    Vec.push (svVarValue solver) (coerce lUndef)
    Vec.push (svVarPolarity solver) True
    Vec.push (svVarActivity solver) 0
    Vec.push (svVarTrailIndex solver) maxBound
    Vec.push (svVarLevel solver) maxBound
    Vec.push (svVarWatches solver) []
    Vec.push (svVarOnUnassigned solver) []
    Vec.push (svVarReason solver) Nothing
    Vec.push (svVarEMAScaled solver) 0
    Vec.push (svVarWhenAssigned solver) (-1)
    Vec.push (svVarParticipated solver) 0
    Vec.push (svVarReasoned solver) 0

    Vec.push (svLitWatches solver) []
    Vec.push (svLitWatches solver) []
    Vec.push (svLitOccurList solver) HashSet.empty
    Vec.push (svLitOccurList solver) HashSet.empty

    PQ.enqueue (svVarQueue solver) v
    Vec.push (svSeen solver) False
    return v

  newVars :: Solver -> Int -> IO [Var]
  newVars solver n = do
    nv <- getNVars solver
#if SIZEOF_HSINT > 4
    when (nv + n > fromIntegral (maxBound :: PackedLit)) $ do
      error "cannot allocate more variables"
#endif
    resizeVarCapacity solver (nv+n)
    replicateM n (newVar solver)

  newVars_ :: Solver -> Int -> IO ()
  newVars_ solver n = do
    nv <- getNVars solver
#if SIZEOF_HSINT > 4
    when (nv + n > fromIntegral (maxBound :: PackedLit)) $ do
      error "cannot allocate more variables"
#endif
    resizeVarCapacity solver (nv+n)
    replicateM_ n (newVar solver)

-- |Pre-allocate internal buffer for @n@ variables.
resizeVarCapacity :: Solver -> Int -> IO ()
resizeVarCapacity solver n = do
  Vec.resizeCapacity (svVarValue solver) n
  Vec.resizeCapacity (svVarPolarity solver) n
  Vec.resizeCapacity (svVarActivity solver) n
  Vec.resizeCapacity (svVarTrailIndex solver) n
  Vec.resizeCapacity (svVarLevel solver) n
  Vec.resizeCapacity (svVarWatches solver) n
  Vec.resizeCapacity (svVarOnUnassigned solver) n
  Vec.resizeCapacity (svVarReason solver) n
  Vec.resizeCapacity (svVarEMAScaled solver) n
  Vec.resizeCapacity (svVarWhenAssigned solver) n
  Vec.resizeCapacity (svVarParticipated solver) n
  Vec.resizeCapacity (svVarReasoned solver) n
  Vec.resizeCapacity (svLitWatches solver) (n*2)
  Vec.resizeCapacity (svLitOccurList solver) (n*2)
  Vec.resizeCapacity (svSeen solver) n
  PQ.resizeHeapCapacity (svVarQueue solver) n
  PQ.resizeTableCapacity (svVarQueue solver) (n+1)

instance AddClause IO Solver where
  addClause :: Solver -> Clause -> IO ()
  addClause solver lits = do
    d <- getDecisionLevel solver
    assert (d == levelRoot) $ return ()

    ok <- readIORef (svOk solver)
    when ok $ do
      m <- instantiateClause (getLitFixed solver) lits
      case normalizeClause =<< m of
        Nothing -> return ()
        Just [] -> markBad solver
        Just [lit] -> do
          {- We do not call 'removeBackwardSubsumedBy' here,
             because subsumed constraints will be removed by 'simplify'. -}
          ret <- assign solver lit
          assert ret $ return ()
          ret2 <- deduce solver
          case ret2 of
            Nothing -> return ()
            Just _ -> markBad solver
        Just lits2 -> do
          subsumed <- checkForwardSubsumption solver lits
          unless subsumed $ do
            removeBackwardSubsumedBy solver ([(1,lit) | lit <- lits2], 1)
            clause <- newClauseHandler lits2 False
            addToDB solver clause
            _ <- basicAttachClauseHandler solver clause
            return ()

instance AddCardinality IO Solver where
  addAtLeast :: Solver -> [Lit] -> Int -> IO ()
  addAtLeast solver lits n = do
    d <- getDecisionLevel solver
    assert (d == levelRoot) $ return ()

    ok <- readIORef (svOk solver)
    when ok $ do
      (lits',n') <- liftM normalizeAtLeast $ instantiateAtLeast (getLitFixed solver) (lits,n)
      let len = length lits'

      if n' <= 0 then return ()
      else if n' > len then markBad solver
      else if n' == 1 then addClause solver lits'
      else if n' == len then do
        {- We do not call 'removeBackwardSubsumedBy' here,
           because subsumed constraints will be removed by 'simplify'. -}
        forM_ lits' $ \l -> do
          ret <- assign solver l
          assert ret $ return ()
        ret2 <- deduce solver
        case ret2 of
          Nothing -> return ()
          Just _ -> markBad solver
      else do -- n' < len
        removeBackwardSubsumedBy solver ([(1,lit) | lit <- lits'], fromIntegral n')
        c <- newAtLeastHandler lits' n' False
        addToDB solver c
        _ <- basicAttachAtLeastHandler solver c
        return ()

instance AddPBLin IO Solver where
  addPBAtLeast :: Solver -> PBLinSum -> Integer -> IO ()
  addPBAtLeast solver ts n = do
    d <- getDecisionLevel solver
    assert (d == levelRoot) $ return ()

    ok <- readIORef (svOk solver)
    when ok $ do
      (ts',n') <- liftM normalizePBLinAtLeast $ instantiatePBLinAtLeast (getLitFixed solver) (ts,n)

      case pbToAtLeast (ts',n') of
        Just (lhs',rhs') -> addAtLeast solver lhs' rhs'
        Nothing -> do
          let cs = map fst ts'
              slack = sum cs - n'
          if n' <= 0 then return ()
          else if slack < 0 then markBad solver
          else do
            removeBackwardSubsumedBy solver (ts', n')
            (ts'',n'') <- do
              b <- configEnablePBSplitClausePart <$> getConfig solver
              if b
              then pbSplitClausePart solver (ts',n')
              else return (ts',n')

            c <- newPBHandler solver ts'' n'' False
            let constr = toConstraintHandler c
            addToDB solver constr
            ret <- attach solver constr
            if not ret then do
              markBad solver
            else do
              ret2 <- deduce solver
              case ret2 of
                Nothing -> return ()
                Just _ -> markBad solver

  addPBExactly :: Solver -> PBLinSum -> Integer -> IO ()
  addPBExactly solver ts n = do
    (ts2,n2) <- liftM normalizePBLinExactly $ instantiatePBLinExactly (getLitFixed solver) (ts,n)
    addPBAtLeast solver ts2 n2
    addPBAtMost solver ts2 n2

  addPBAtLeastSoft :: Solver -> Lit -> PBLinSum -> Integer -> IO ()
  addPBAtLeastSoft solver sel lhs rhs = do
    (lhs', rhs') <- liftM normalizePBLinAtLeast $ instantiatePBLinAtLeast (getLitFixed solver) (lhs,rhs)
    addPBAtLeast solver ((rhs', litNot sel) : lhs') rhs'

  addPBExactlySoft :: Solver -> Lit -> PBLinSum -> Integer -> IO ()
  addPBExactlySoft solver sel lhs rhs = do
    (lhs2, rhs2) <- liftM normalizePBLinExactly $ instantiatePBLinExactly (getLitFixed solver) (lhs,rhs)
    addPBAtLeastSoft solver sel lhs2 rhs2
    addPBAtMostSoft solver sel lhs2 rhs2

-- | See documentation of 'setPBSplitClausePart'.
pbSplitClausePart :: Solver -> PBLinAtLeast -> IO PBLinAtLeast
pbSplitClausePart solver (lhs,rhs) = do
  let (ts1,ts2) = partition (\(c,_) -> c >= rhs) lhs
  if length ts1 < 2 then
    return (lhs,rhs)
  else do
    sel <- newVar solver
    addClause solver $ -sel : [l | (_,l) <- ts1]
    return ((rhs,sel) : ts2, rhs)

instance AddXORClause IO Solver where
  addXORClause :: Solver -> [Lit] -> Bool -> IO ()
  addXORClause solver lits rhs = do
    d <- getDecisionLevel solver
    assert (d == levelRoot) $ return ()

    ok <- readIORef (svOk solver)
    when ok $ do
      xcl <- instantiateXORClause (getLitFixed solver) (lits,rhs)
      case normalizeXORClause xcl of
        ([], True) -> markBad solver
        ([], False) -> return ()
        ([l], b) -> addClause solver [if b then l else litNot l]
        (l:ls, b) -> do
          c <- newXORClauseHandler ((if b then l else litNot l) : ls) False
          addToDB solver c
          _ <- basicAttachXORClauseHandler solver c
          return ()

{--------------------------------------------------------------------
  Problem solving
--------------------------------------------------------------------}

-- | Solve constraints.
-- Returns 'True' if the problem is SATISFIABLE.
-- Returns 'False' if the problem is UNSATISFIABLE.
solve :: Solver -> IO Bool
solve solver = do
  Vec.clear (svAssumptions solver)
  solve_ solver

-- | Solve constraints under assuptions.
-- Returns 'True' if the problem is SATISFIABLE.
-- Returns 'False' if the problem is UNSATISFIABLE.
solveWith :: Solver
          -> [Lit]    -- ^ Assumptions
          -> IO Bool
solveWith solver ls = do
  Vec.clear (svAssumptions solver)
  mapM_ (Vec.push (svAssumptions solver)) ls
  solve_ solver

solve_ :: Solver -> IO Bool
solve_ solver = do
  config <- getConfig solver
  writeIORef (svAssumptionsImplications solver) IS.empty

  log solver "Solving starts ..."
  resetStat solver
  writeIORef (svCanceled solver) False
  writeIORef (svModel solver) Nothing
  writeIORef (svFailedAssumptions solver) IS.empty

  ok <- readIORef (svOk solver)
  if not ok then
    return False
  else do
    when debugMode $ dumpVarActivity solver
    d <- getDecisionLevel solver
    assert (d == levelRoot) $ return ()

    nv <- getNVars solver
    Vec.resizeCapacity (svTrail solver) nv

    unless (configRestartInc config > 1) $ error "RestartInc must be >1"
    let restartSeq =
          if configRestartFirst config  > 0
          then mkRestartSeq (configRestartStrategy config) (configRestartFirst config) (configRestartInc config)
          else repeat 0

    let learntSizeAdj = do
          (size,adj) <- shift (svLearntLimSeq solver)
          writeIORef (svLearntLim solver) size
          writeIORef (svLearntLimAdjCnt solver) adj
        onConflict = do
          cnt <- readIORef (svLearntLimAdjCnt solver)
          if (cnt==0)
          then learntSizeAdj
          else writeIORef (svLearntLimAdjCnt solver) $! cnt-1

    cnt <- readIORef (svLearntLimAdjCnt solver)
    when (cnt == -1) $ do
      unless (configLearntSizeInc config > 1) $ error "LearntSizeInc must be >1"
      nc <- getNConstraints solver
      let initialLearntLim = if configLearntSizeFirst config > 0 then configLearntSizeFirst config else max ((nc + nv) `div` 3) 16
          learntSizeSeq    = iterate (ceiling . (configLearntSizeInc config *) . fromIntegral) initialLearntLim
          learntSizeAdjSeq = iterate (\x -> (x * 3) `div` 2) (100::Int)
      writeIORef (svLearntLimSeq solver) (zip learntSizeSeq learntSizeAdjSeq)
      learntSizeAdj

    unless (0 <= configERWAStepSizeFirst config && configERWAStepSizeFirst config <= 1) $
      error "ERWAStepSizeFirst must be in [0..1]"
    unless (0 <= configERWAStepSizeMin config && configERWAStepSizeFirst config <= 1) $
      error "ERWAStepSizeMin must be in [0..1]"
    unless (0 <= configERWAStepSizeDec config) $
      error "ERWAStepSizeDec must be >=0"
    writeIOURef (svERWAStepSize solver) (configERWAStepSizeFirst config)

    let loop [] = error "solve_: should not happen"
        loop (conflict_lim:rs) = do
          printStat solver True
          ret <- search solver conflict_lim onConflict
          case ret of
            SRFinished x -> return $ Right x
            SRBudgetExceeded -> return $ Left (throw BudgetExceeded)
            SRCanceled -> return $ Left (throw Canceled)
            SRRestart -> do
              modifyIOURef (svNRestart solver) (+1)
              backtrackTo solver levelRoot
              loop rs

    printStatHeader solver

    startCPU <- getTime ProcessCPUTime
    startWC  <- getTime Monotonic
    writeIORef (svStartWC solver) startWC
    result <- loop restartSeq
    endCPU <- getTime ProcessCPUTime
    endWC  <- getTime Monotonic

    case result of
      Right True -> do
        when (configCheckModel config) $ checkSatisfied solver
        constructModel solver
        mt <- getTheory solver
        case mt of
          Nothing -> return ()
          Just t -> thConstructModel t
      _ -> return ()
    case result of
      Right False -> return ()
      _ -> saveAssumptionsImplications solver

    backtrackTo solver levelRoot

    when debugMode $ dumpVarActivity solver
    when debugMode $ dumpConstrActivity solver
    printStat solver True
    let durationSecs :: TimeSpec -> TimeSpec -> Double
        durationSecs start end = fromIntegral (toNanoSecs (end `diffTimeSpec` start)) / 10^(9::Int)
    (log solver . printf "#cpu_time = %.3fs") (durationSecs startCPU endCPU)
    (log solver . printf "#wall_clock_time = %.3fs") (durationSecs startWC endWC)
    (log solver . printf "#decision = %d") =<< readIOURef (svNDecision solver)
    (log solver . printf "#random_decision = %d") =<< readIOURef (svNRandomDecision solver)
    (log solver . printf "#conflict = %d") =<< readIOURef (svNConflict solver)
    (log solver . printf "#restart = %d")  =<< readIOURef (svNRestart solver)

    case result of
      Right x  -> return x
      Left m -> m

data BudgetExceeded = BudgetExceeded
  deriving (Show, Typeable)

instance Exception BudgetExceeded

data Canceled = Canceled
  deriving (Show, Typeable)

instance Exception Canceled

data SearchResult
  = SRFinished Bool
  | SRRestart
  | SRBudgetExceeded
  | SRCanceled

search :: Solver -> Int -> IO () -> IO SearchResult
search solver !conflict_lim onConflict = do
  conflictCounter <- newIORef 0
  let
    loop :: IO SearchResult
    loop = do
      conflict <- deduce solver
      case conflict of
        Just constr -> do
          ret <- handleConflict conflictCounter constr
          case ret of
            Just sr -> return sr
            Nothing -> loop
        Nothing -> do
          lv <- getDecisionLevel solver
          when (lv == levelRoot) $ simplify solver
          checkGC
          r <- pickAssumption
          case r of
            Nothing -> return (SRFinished False)
            Just lit
              | lit /= litUndef -> decide solver lit >> loop
              | otherwise -> do
                  lit2 <- pickBranchLit solver
                  if lit2 == litUndef
                    then return (SRFinished True)
                    else decide solver lit2 >> loop
  loop

  where
    checkGC :: IO ()
    checkGC = do
      n <- getNLearntConstraints solver
      m <- getNAssigned solver
      learnt_lim <- readIORef (svLearntLim solver)
      when (learnt_lim >= 0 && n - m > learnt_lim) $ do
        modifyIOURef (svNLearntGC solver) (+1)
        reduceDB solver

    pickAssumption :: IO (Maybe Lit)
    pickAssumption = do
      s <- Vec.getSize (svAssumptions solver)
      let go = do
              d <- getDecisionLevel solver
              if not (d < s) then
                return (Just litUndef)
              else do
                l <- Vec.unsafeRead (svAssumptions solver) d
                val <- litValue solver l
                if val == lTrue then do
                  -- dummy decision level
                  pushDecisionLevel solver
                  go
                else if val == lFalse then do
                  -- conflict with assumption
                  core <- analyzeFinal solver l
                  writeIORef (svFailedAssumptions solver) (IS.fromList core)
                  return Nothing
                else
                  return (Just l)
      go

    handleConflict :: IORef Int -> SomeConstraintHandler -> IO (Maybe SearchResult)
    handleConflict conflictCounter constr = do
      varEMADecay solver
      varDecayActivity solver
      constrDecayActivity solver
      onConflict

      modifyIOURef (svNConflict solver) (+1)
      d <- getDecisionLevel solver

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

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

      modifyIOURef (svConfBudget solver) $ \confBudget ->
        if confBudget > 0 then confBudget - 1 else confBudget
      confBudget <- readIOURef (svConfBudget solver)

      terminateCallback' <- readIORef (svTerminateCallback solver)
      case terminateCallback' of
        Nothing -> return ()
        Just terminateCallback -> do
          ret <- terminateCallback
          when ret $ writeIORef (svCanceled solver) True
      canceled <- readIORef (svCanceled solver)

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

      if d == levelRoot then do
        callLearnCallback solver []
        markBad solver
        return $ Just (SRFinished False)
      else if confBudget==0 then
        return $ Just SRBudgetExceeded
      else if canceled then
        return $ Just SRCanceled
      else if conflict_lim > 0 && c >= conflict_lim then
        return $ Just SRRestart
      else do
        modifyIOURef (svLearntCounter solver) (+1)
        config <- getConfig solver
        case configLearningStrategy config of
          LearningClause -> learnClause constr >> return Nothing
          LearningHybrid -> learnHybrid conflictCounter constr

    learnClause :: SomeConstraintHandler -> IO ()
    learnClause constr = do
      (learntClause, level) <- analyzeConflict solver constr
      backtrackTo solver level
      case learntClause of
        [] -> error "search(LearningClause): should not happen"
        [lit] -> do
          ret <- assign solver lit
          assert ret $ return ()
          return ()
        lit:_ -> do
          cl <- newClauseHandler learntClause True
          let constr2 = toConstraintHandler cl
          addToLearntDB solver constr2
          basicAttachClauseHandler solver cl
          assignBy solver lit constr2
          constrBumpActivity solver constr2

    learnHybrid :: IORef Int -> SomeConstraintHandler -> IO (Maybe SearchResult)
    learnHybrid conflictCounter constr = do
      (learntClause, clauseLevel) <- analyzeConflict solver constr
      (pb, minLevel) <- do
        z <- readIORef (svPBLearnt solver)
        case z of
          Nothing -> return (z, clauseLevel)
          Just pb -> do
            pbLevel <- pbBacktrackLevel solver pb
            return (z, min clauseLevel pbLevel)
      backtrackTo solver minLevel

      case learntClause of
        [] -> error "search(LearningHybrid): should not happen"
        [lit] -> do
          _ <- assign solver lit -- This should always succeed.
          return ()
        lit:_ -> do
          cl <- newClauseHandler learntClause True
          let constr2 = toConstraintHandler cl
          addToLearntDB solver constr2
          basicAttachClauseHandler solver cl
          constrBumpActivity solver constr2
          when (minLevel == clauseLevel) $ do
            _ <- assignBy solver lit constr2 -- This should always succeed.
            return ()

      ret <- deduce solver
      case ret of
        Just conflicted -> do
          handleConflict conflictCounter conflicted
          -- TODO: should also learn the PB constraint?
        Nothing -> do
          case pb of
            Nothing -> return Nothing
            Just (lhs,rhs) -> do
              h <- newPBHandlerPromoted solver lhs rhs True
              case h of
                CHClause _ -> do
                  {- We don't want to add additional clause,
                     since it would be subsumed by already added one. -}
                  return Nothing
                _ -> do
                  addToLearntDB solver h
                  ret2 <- attach solver h
                  constrBumpActivity solver h
                  if ret2 then
                    return Nothing
                  else
                    handleConflict conflictCounter h

-- | Cancel exectution of 'solve' or 'solveWith'.
--
-- This can be called from other threads.
cancel :: Solver -> IO ()
cancel solver = writeIORef (svCanceled solver) True

-- | After 'solve' returns True, it returns an satisfying assignment.
getModel :: Solver -> IO Model
getModel solver = do
  m <- readIORef (svModel solver)
  return (fromJust m)

-- | After 'solveWith' returns False, it returns a set of assumptions
-- that leads to contradiction. In particular, if it returns an empty
-- set, the problem is unsatisiable without any assumptions.
getFailedAssumptions :: Solver -> IO LitSet
getFailedAssumptions solver = readIORef (svFailedAssumptions solver)

-- | __EXPERIMENTAL API__: After 'solveWith' returns True or failed with 'BudgetExceeded' exception,
-- it returns a set of literals that are implied by assumptions.
getAssumptionsImplications :: Solver -> IO LitSet
getAssumptionsImplications solver = readIORef (svAssumptionsImplications solver)

{--------------------------------------------------------------------
  Simplification
--------------------------------------------------------------------}

-- | Simplify the constraint database according to the current top-level assigment.
simplify :: Solver -> IO ()
simplify solver = do
  let loop [] rs !n     = return (rs,n)
      loop (y:ys) rs !n = do
        b1 <- isSatisfied solver y
        b2 <- isLocked solver y
        if b1 && not b2 then do
          detach solver y
          loop ys rs (n+1)
        else loop ys (y:rs) n

  -- simplify original constraint DB
  do
    xs <- readIORef (svConstrDB solver)
    (ys,n) <- loop xs [] (0::Int)
    modifyIOURef (svNRemovedConstr solver) (+n)
    writeIORef (svConstrDB solver) ys

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

{-
References:
L. Zhang, "On subsumption removal and On-the-Fly CNF simplification,"
Theory and Applications of Satisfiability Testing (2005), pp. 482-489.
-}

checkForwardSubsumption :: Solver -> Clause -> IO Bool
checkForwardSubsumption solver lits = do
  flag <- configEnableForwardSubsumptionRemoval <$> getConfig solver
  if not flag then
    return False
  else do
    withEnablePhaseSaving False $ do
      bracket_
        (pushDecisionLevel solver)
        (backtrackTo solver levelRoot) $ do
          b <- allM (\lit -> assign solver (litNot lit)) lits
          if b then
            liftM isJust (deduce solver)
          else do
            when debugMode $ log solver ("forward subsumption: " ++ show lits)
            return True
  where
    withEnablePhaseSaving flag m =
      bracket
        (getConfig solver)
        (\saved -> modifyConfig solver (\config -> config{ configEnablePhaseSaving = configEnablePhaseSaving saved }))
        (\saved -> setConfig solver saved{ configEnablePhaseSaving = flag } >> m)

removeBackwardSubsumedBy :: Solver -> PBLinAtLeast -> IO ()
removeBackwardSubsumedBy solver pb = do
  flag <- configEnableBackwardSubsumptionRemoval <$> getConfig solver
  when flag $ do
    xs <- backwardSubsumedBy solver pb
    when debugMode $ do
      forM_ (HashSet.toList xs) $ \c -> do
        s <- showConstraintHandler c
        log solver (printf "backward subsumption: %s is subsumed by %s\n" s (show pb))
    removeConstraintHandlers solver xs

backwardSubsumedBy :: Solver -> PBLinAtLeast -> IO (HashSet SomeConstraintHandler)
backwardSubsumedBy solver pb@(lhs,_) = do
  xs <- forM lhs $ \(_,lit) -> do
    Vec.unsafeRead (svLitOccurList solver) (litIndex lit)
  case xs of
    [] -> return HashSet.empty
    s:ss -> do
      let p c = do
            -- Note that @isPBRepresentable c@ is always True here,
            -- because only such constraints are added to occur list.
            -- See 'addToDB'.
            pb2 <- instantiatePBLinAtLeast (getLitFixed solver) =<< toPBLinAtLeast c
            return $ pbLinSubsume pb pb2
      liftM HashSet.fromList
        $ filterM p
        $ HashSet.toList
        $ foldl' HashSet.intersection s ss

removeConstraintHandlers :: Solver -> HashSet SomeConstraintHandler -> IO ()
removeConstraintHandlers _ zs | HashSet.null zs = return ()
removeConstraintHandlers solver zs = do
  let loop [] rs !n     = return (rs,n)
      loop (c:cs) rs !n = do
        if c `HashSet.member` zs then do
          detach solver c
          loop cs rs (n+1)
        else loop cs (c:rs) n
  xs <- readIORef (svConstrDB solver)
  (ys,n) <- loop xs [] (0::Int)
  modifyIOURef (svNRemovedConstr solver) (+n)
  writeIORef (svConstrDB solver) ys

{--------------------------------------------------------------------
  Parameter settings.
--------------------------------------------------------------------}

{--------------------------------------------------------------------
  Configulation
--------------------------------------------------------------------}

getConfig :: Solver -> IO Config
getConfig solver = readIORef $ svConfig solver

setConfig :: Solver -> Config -> IO ()
setConfig solver conf = do
  orig <- getConfig solver
  writeIORef (svConfig solver) conf
  when (configBranchingStrategy orig /= configBranchingStrategy conf) $ do
    PQ.rebuild (svVarQueue solver)

modifyConfig :: Solver -> (Config -> Config) -> IO ()
modifyConfig solver f = do
  config <- getConfig solver
  setConfig solver $ f config

-- | The default polarity of a variable.
setVarPolarity :: Solver -> Var -> Bool -> IO ()
setVarPolarity solver v val = Vec.unsafeWrite (svVarPolarity solver) (v - 1) val

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

-- | Get random generator used by the random variable selection
getRandomGen :: Solver -> IO Rand.GenIO
getRandomGen solver = readIORef (svRandomGen solver)

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

-- | Set a callback function used to indicate a termination requirement to the solver.
--
-- The solver will periodically call this function and check its return value during
-- the search. If the callback function returns `True` the solver terminates and throws
-- 'Canceled' exception.
--
-- See also 'clearTerminateCallback' and
-- [IPASIR](https://github.com/biotomas/ipasir)'s @ipasir_set_terminate()@ function.
setTerminateCallback :: Solver -> IO Bool -> IO ()
setTerminateCallback solver callback = writeIORef (svTerminateCallback solver) (Just callback)

-- | Clear a callback function set by `setTerminateCallback`
clearTerminateCallback :: Solver -> IO ()
clearTerminateCallback solver = writeIORef (svTerminateCallback solver) Nothing

-- | Set a callback function used to extract learned clauses from the solver.
-- The solver will call this function for each learned clause.
--
-- See also 'clearLearnCallback' and
-- [IPASIR](https://github.com/biotomas/ipasir)'s @ipasir_set_learn()@ function.
setLearnCallback :: Solver -> (Clause -> IO ()) -> IO ()
setLearnCallback solver callback = writeIORef (svLearnCallback solver) (Just callback)

-- | Clear a callback function set by `setLearnCallback`
clearLearnCallback :: Solver -> IO ()
clearLearnCallback solver = writeIORef (svLearnCallback solver) Nothing

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

pickBranchLit :: Solver -> IO Lit
pickBranchLit !solver = do
  gen <- readIORef (svRandomGen solver)
  let vqueue = svVarQueue solver
  !randfreq <- configRandomFreq <$> getConfig solver
  !size <- PQ.queueSize vqueue
  -- System.Random.random produces [0,1), but System.Random.MWC.uniform produces (0,1]
  !r <- liftM (1 -) $ Rand.uniform gen
  var <-
    if (r < randfreq && size >= 2) then do
      a <- PQ.getHeapArray vqueue
      i <- Rand.uniformR (0, size-1) gen
      var <- readArray a i
      val <- varValue solver var
      if val == lUndef then do
        modifyIOURef (svNRandomDecision solver) (1+)
        return var
      else return litUndef
    else
      return litUndef

  -- Activity based decision
  let loop :: IO Var
      loop = do
        m <- PQ.dequeue vqueue
        case m of
          Nothing -> return litUndef
          Just var2 -> do
            val2 <- varValue solver var2
            if val2 /= lUndef
              then loop
              else return var2
  var2 <-
    if var==litUndef
    then loop
    else return var

  if var2==litUndef then
    return litUndef
  else do
    -- TODO: random polarity
    p <- Vec.unsafeRead (svVarPolarity solver) (var2 - 1)
    return $! literal var2 p

decide :: Solver -> Lit -> IO ()
decide solver !lit = do
  modifyIOURef (svNDecision solver) (+1)
  pushDecisionLevel solver
  when debugMode $ do
    val <- litValue solver lit
    when (val /= lUndef) $ error "decide: should not happen"
  assign solver lit
  return ()

deduce :: Solver -> IO (Maybe SomeConstraintHandler)
deduce solver = liftM (either Just (const Nothing)) $ runExceptT $ do
  let loop = do
        deduceB solver
        deduceT solver
        empty <- liftIO $ bcpIsEmpty solver
        unless empty $ loop
  loop

deduceB :: Solver -> ExceptT SomeConstraintHandler IO ()
deduceB solver = loop
  where
    loop :: ExceptT SomeConstraintHandler IO ()
    loop = do
      r <- liftIO $ bcpDequeue solver
      case r of
        Nothing -> return ()
        Just lit -> do
          processLit lit
          processVar lit
          loop

    processLit :: Lit -> ExceptT SomeConstraintHandler IO ()
    processLit !lit = ExceptT $ liftM (maybe (Right ()) Left) $ do
      let falsifiedLit = litNot lit
          a = svLitWatches solver
          idx = litIndex falsifiedLit
      let loop2 [] = return Nothing
          loop2 (w:ws) = do
            ok <- propagate solver w falsifiedLit
            if ok then
              loop2 ws
            else do
              Vec.unsafeModify a idx (++ws)
              return (Just w)
      ws <- Vec.unsafeRead a idx
      Vec.unsafeWrite a idx []
      loop2 ws

    processVar :: Lit -> ExceptT SomeConstraintHandler IO ()
    processVar !lit = ExceptT $ liftM (maybe (Right ()) Left) $ do
      let falsifiedLit = litNot lit
          idx = litVar lit - 1
      let loop2 [] = return Nothing
          loop2 (w:ws) = do
            ok <- propagate solver w falsifiedLit
            if ok
              then loop2 ws
              else do
                Vec.unsafeModify (svVarWatches solver) idx (++ws)
                return (Just w)
      ws <- Vec.unsafeRead (svVarWatches solver) idx
      Vec.unsafeWrite (svVarWatches solver) idx []
      loop2 ws

analyzeConflict :: ConstraintHandler c => Solver -> c -> IO (Clause, Level)
analyzeConflict solver constr = do
  config <- getConfig solver
  let isHybrid = configLearningStrategy config == LearningHybrid

  d <- getDecisionLevel solver
  (out :: Vec.UVec Lit) <- Vec.new
  Vec.push out 0 -- (leave room for the asserting literal)
  (pathC :: IOURef Int) <- newIOURef 0

  pbConstrRef <- newIORef undefined

  let f lits = do
        forM_ lits $ \lit -> do
          let !v = litVar lit
          lv <- litLevel solver lit
          b <- Vec.unsafeRead (svSeen solver) (v - 1)
          when (not b && lv > levelRoot) $ do
            varBumpActivity solver v
            varIncrementParticipated solver v
            if lv >= d then do
              Vec.unsafeWrite (svSeen solver) (v - 1) True
              modifyIOURef pathC (+1)
            else do
              Vec.push out lit

      processLitHybrid pb constr2 lit getLits = do
        pb2 <- do
          let clausePB = do
                lits <- getLits
                return $ clauseToPBLinAtLeast (lit : lits)
          b <- isPBRepresentable constr2
          if not b then do
            clausePB
          else do
            pb2 <- toPBLinAtLeast constr2
            o <- pbOverSAT solver pb2
            if o then do
              clausePB
            else
              return pb2
        let pb3 = cutResolve pb pb2 (litVar lit)
            ls = IS.fromList [l | (_,l) <- fst pb3]
        seq ls $ writeIORef pbConstrRef (ls, pb3)

      popUnseen = do
        l <- peekTrail solver
        let !v = litVar l
        b <- Vec.unsafeRead (svSeen solver) (v - 1)
        if b then do
          return ()
        else do
          when isHybrid $ do
            (ls, pb) <- readIORef pbConstrRef
            when (litNot l `IS.member` ls) $ do
              Just constr2 <- varReason solver v
              processLitHybrid pb constr2 l (reasonOf solver constr2 (Just l))
          popTrail solver
          popUnseen

      loop = do
        popUnseen
        l <- peekTrail solver
        let !v = litVar l
        Vec.unsafeWrite (svSeen solver) (v - 1) False
        modifyIOURef pathC (subtract 1)
        c <- readIOURef pathC
        if c > 0 then do
          Just constr2 <- varReason solver v
          constrBumpActivity solver constr2
          lits <- reasonOf solver constr2 (Just l)
          f lits
          when isHybrid $ do
            (ls, pb) <- readIORef pbConstrRef
            when (litNot l `IS.member` ls) $ do
              processLitHybrid pb constr2 l (return lits)
          popTrail solver
          loop
        else do
          Vec.unsafeWrite out 0 (litNot l)

  constrBumpActivity solver constr
  falsifiedLits <- reasonOf solver constr Nothing
  f falsifiedLits
  when isHybrid $ do
     pb <- do
       b <- isPBRepresentable constr
       if b then
         toPBLinAtLeast constr
       else
         return (clauseToPBLinAtLeast falsifiedLits)
     let ls = IS.fromList [l | (_,l) <- fst pb]
     seq ls $ writeIORef pbConstrRef (ls, pb)
  loop
  lits <- liftM IS.fromList $ Vec.getElems out

  lits2 <- minimizeConflictClause solver lits

  incrementReasoned solver (IS.toList lits2)

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

  when isHybrid $ do
    (_, pb) <- readIORef pbConstrRef
    case pbToClause pb of
      Just _ -> writeIORef (svPBLearnt solver) Nothing
      Nothing -> writeIORef (svPBLearnt solver) (Just pb)

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

-- { p } ∪ { pにfalseを割り当てる原因のassumption }
analyzeFinal :: Solver -> Lit -> IO [Lit]
analyzeFinal solver p = do
  let go :: Int -> VarSet -> [Lit] -> IO [Lit]
      go i seen result
        | i < 0 = return result
        | otherwise = do
            l <- Vec.unsafeRead (svTrail solver) i
            lv <- litLevel solver l
            if lv == levelRoot then
              return result
            else if litVar l `IS.member` seen then do
              r <- varReason solver (litVar l)
              case r of
                Nothing -> do
                  let seen' = IS.delete (litVar l) seen
                  go (i-1) seen' (l : result)
                Just constr  -> do
                  c <- reasonOf solver constr (Just l)
                  let seen' = IS.delete (litVar l) seen `IS.union` IS.fromList [litVar l2 | l2 <- c]
                  go (i-1) seen' result
            else
              go (i-1) seen result
  n <- Vec.getSize (svTrail solver)
  go (n-1) (IS.singleton (litVar p)) [p]

callLearnCallback :: Solver -> Clause -> IO ()
callLearnCallback solver clause = do
  cb <- readIORef (svLearnCallback solver)
  case cb of
    Nothing -> return ()
    Just callback -> callback clause

pbBacktrackLevel :: Solver -> PBLinAtLeast -> IO Level
pbBacktrackLevel _ ([], rhs) = assert (rhs > 0) $ return levelRoot
pbBacktrackLevel solver (lhs, rhs) = do
  levelToLiterals <- liftM (IM.unionsWith IM.union) $ forM lhs $ \(c,lit) -> do
    val <- litValue solver lit
    if val /= lUndef then do
      level <- litLevel solver lit
      return $ IM.singleton level (IM.singleton lit (c,val))
    else
      return $ IM.singleton maxBound (IM.singleton lit (c,val))

  let replay [] !_ = error "pbBacktrackLevel: should not happen"
      replay ((lv,lv_lits) : lvs) !slack = do
        let slack_lv = slack - sum [c | (_,(c,val)) <- IM.toList lv_lits, val == lFalse]
        if slack_lv < 0 then
          return lv -- CONFLICT
        else if any (\(_, lits2) -> any (\(c,_) -> c > slack_lv) (IM.elems lits2)) lvs then
          return lv -- UNIT
        else
          replay lvs slack_lv

  let initial_slack = sum [c | (c,_) <- lhs] - rhs
  if any (\(c,_) -> c > initial_slack) lhs then
    return 0
  else do
    replay (IM.toList levelToLiterals) initial_slack

minimizeConflictClause :: Solver -> LitSet -> IO LitSet
minimizeConflictClause solver lits = do
  ccmin <- configCCMin <$> getConfig solver
  if ccmin >= 2 then
    minimizeConflictClauseRecursive solver lits
  else if ccmin >= 1 then
    minimizeConflictClauseLocal solver lits
  else
    return lits

minimizeConflictClauseLocal :: Solver -> LitSet -> IO LitSet
minimizeConflictClauseLocal solver lits = do
  let xs = IS.toAscList lits
  ys <- filterM (liftM not . isRedundant) xs
  when debugMode $ do
    log solver "minimizeConflictClauseLocal:"
    log solver $ show xs
    log solver $ show ys
  return $ IS.fromAscList $ ys

  where
    isRedundant :: Lit -> IO Bool
    isRedundant lit = do
      c <- varReason solver (litVar lit)
      case c of
        Nothing -> return False
        Just c2 -> do
          ls <- reasonOf solver c2 (Just (litNot lit))
          allM test ls

    test :: Lit -> IO Bool
    test lit = do
      lv <- litLevel solver lit
      return $ lv == levelRoot || lit `IS.member` lits

minimizeConflictClauseRecursive :: Solver -> LitSet -> IO LitSet
minimizeConflictClauseRecursive solver lits = do
  let
    isRedundant :: Lit -> IO Bool
    isRedundant lit = do
      c <- varReason solver (litVar lit)
      case c of
        Nothing -> return False
        Just c2 -> do
          ls <- reasonOf solver c2 (Just (litNot lit))
          go ls IS.empty

    go :: [Lit] -> IS.IntSet -> IO Bool
    go [] _ = return True
    go (lit : ls) seen = do
      lv <- litLevel solver lit
      if lv == levelRoot || lit `IS.member` lits || lit `IS.member` seen then
        go ls seen
      else do
        c <- varReason solver (litVar lit)
        case c of
          Nothing -> return False
          Just c2 -> do
            ls2 <- reasonOf solver c2 (Just (litNot lit))
            go (ls2 ++ ls) (IS.insert lit seen)

  let xs = IS.toAscList lits
  ys <- filterM (liftM not . isRedundant) xs
  when debugMode $ do
    log solver "minimizeConflictClauseRecursive:"
    log solver $ show xs
    log solver $ show ys
  return $ IS.fromAscList $ ys

incrementReasoned :: Solver -> Clause -> IO ()
incrementReasoned solver ls = do
  let f reasonSided l = do
        m <- varReason solver (litVar l)
        case m of
          Nothing -> return reasonSided
          Just constr -> do
            v <- litValue solver l
            unless (v == lFalse) undefined
            xs <- constrReasonOf solver constr (Just (litNot l))
            return $ reasonSided `IS.union` IS.fromList (map litVar xs)
  reasonSided <- foldM f IS.empty ls
  mapM_ (varIncrementReasoned solver) (IS.toList reasonSided)

peekTrail :: Solver -> IO Lit
peekTrail solver = do
  n <- Vec.getSize (svTrail solver)
  Vec.unsafeRead (svTrail solver) (n-1)

popTrail :: Solver -> IO Lit
popTrail solver = do
  l <- Vec.unsafePop (svTrail solver)
  unassign solver (litVar l)
  return l

getDecisionLevel ::Solver -> IO Int
getDecisionLevel solver = Vec.getSize (svTrailLimit solver)

pushDecisionLevel :: Solver -> IO ()
pushDecisionLevel solver = do
  Vec.push (svTrailLimit solver) =<< Vec.getSize (svTrail solver)
  mt <- getTheory solver
  case mt of
    Nothing -> return ()
    Just t -> thPushBacktrackPoint t

popDecisionLevel :: Solver -> IO ()
popDecisionLevel solver = do
  n <- Vec.unsafePop (svTrailLimit solver)
  let loop = do
        m <- Vec.getSize (svTrail solver)
        when (m > n) $ do
          popTrail solver
          loop
  loop
  mt <- getTheory solver
  case mt of
    Nothing -> return ()
    Just t -> thPopBacktrackPoint t

-- | Revert to the state at given level
-- (keeping all assignment at @level@ but not beyond).
backtrackTo :: Solver -> Int -> IO ()
backtrackTo solver level = do
  when debugMode $ log solver $ printf "backtrackTo: %d" level
  loop
  bcpClear solver
  mt <- getTheory solver
  case mt of
    Nothing -> return ()
    Just _ -> do
      n <- Vec.getSize (svTrail solver)
      writeIOURef (svTheoryChecked solver) n
  where
    loop :: IO ()
    loop = do
      lv <- getDecisionLevel solver
      when (lv > level) $ do
        popDecisionLevel solver
        loop

constructModel :: Solver -> IO ()
constructModel solver = do
  n <- getNVars solver
  (marr::IOUArray Var Bool) <- newArray_ (1,n)
  forLoop 1 (<=n) (+1) $ \v -> do
    val <- varValue solver v
    writeArray marr v (fromJust (unliftBool val))
  m <- unsafeFreeze marr
  writeIORef (svModel solver) (Just m)

saveAssumptionsImplications :: Solver -> IO ()
saveAssumptionsImplications solver = do
  n <- Vec.getSize (svAssumptions solver)
  lv <- getDecisionLevel solver

  lim_beg <-
    if lv == 0 then
      return 0
    else
      Vec.read (svTrailLimit solver) 0
  lim_end <-
    if lv > n then
       Vec.read (svTrailLimit solver) n
    else
       Vec.getSize (svTrail solver)

  let ref = svAssumptionsImplications solver
  forM_ [lim_beg .. lim_end-1] $ \i -> do
    lit <- Vec.read (svTrail solver) i
    modifyIORef' ref (IS.insert lit)
  forM_ [0..n-1] $ \i -> do
    lit <- Vec.read (svAssumptions solver) i
    modifyIORef' ref (IS.delete lit)

constrDecayActivity :: Solver -> IO ()
constrDecayActivity solver = do
  d <- configConstrDecay <$> getConfig solver
  modifyIOURef (svConstrInc solver) (d*)

constrBumpActivity :: ConstraintHandler a => Solver -> a -> IO ()
constrBumpActivity solver this = do
  aval <- constrReadActivity this
  when (aval >= 0) $ do -- learnt clause
    inc <- readIOURef (svConstrInc solver)
    let aval2 = aval+inc
    constrWriteActivity this $! aval2
    when (aval2 > 1e20) $
      -- Rescale
      constrRescaleAllActivity solver

constrRescaleAllActivity :: Solver -> IO ()
constrRescaleAllActivity solver = do
  xs <- learntConstraints solver
  forM_ xs $ \c -> do
    aval <- constrReadActivity c
    when (aval >= 0) $
      constrWriteActivity c $! (aval * 1e-20)
  modifyIOURef (svConstrInc solver) (* 1e-20)

resetStat :: Solver -> IO ()
resetStat solver = do
  writeIOURef (svNDecision solver) 0
  writeIOURef (svNRandomDecision solver) 0
  writeIOURef (svNConflict solver) 0
  writeIOURef (svNRestart solver) 0
  writeIOURef (svNLearntGC solver) 0

printStatHeader :: Solver -> IO ()
printStatHeader solver = do
  log solver $ "============================[ Search Statistics ]============================"
  log solver $ " Time | Restart | Decision | Conflict |      LEARNT     | Fixed    | Removed "
  log solver $ "      |         |          |          |    Limit     GC | Var      | Constra "
  log solver $ "============================================================================="

printStat :: Solver -> Bool -> IO ()
printStat solver force = do
  nowWC <- getTime Monotonic
  b <- if force
       then return True
       else do
         lastWC <- readIORef (svLastStatWC solver)
         return $ sec (nowWC `diffTimeSpec` lastWC) > 1
  when b $ do
    startWC   <- readIORef (svStartWC solver)
    let tm = showTimeDiff $ nowWC `diffTimeSpec` startWC
    restart   <- readIOURef (svNRestart solver)
    dec       <- readIOURef (svNDecision solver)
    conflict  <- readIOURef (svNConflict solver)
    learntLim <- readIORef (svLearntLim solver)
    learntGC  <- readIOURef (svNLearntGC solver)
    fixed     <- getNFixed solver
    removed   <- readIOURef (svNRemovedConstr solver)
    log solver $ printf "%s | %7d | %8d | %8d | %8d %6d | %8d | %8d"
      tm restart dec conflict learntLim learntGC fixed removed
    writeIORef (svLastStatWC solver) nowWC

showTimeDiff :: TimeSpec -> String
showTimeDiff t
  | si <  100  = printf "%4.1fs" (fromRational s :: Double)
  | si <= 9999 = printf "%4ds" si
  | mi <  100  = printf "%4.1fm" (fromRational m :: Double)
  | mi <= 9999 = printf "%4dm" mi
  | hi <  100  = printf "%4.1fs" (fromRational h :: Double)
  | otherwise  = printf "%4dh" hi
  where
    s :: Rational
    s = fromIntegral (toNanoSecs t) / 10^(9::Int)

    si :: Integer
    si = fromIntegral (sec t)

    m :: Rational
    m = s / 60

    mi :: Integer
    mi = round m

    h :: Rational
    h = m / 60

    hi :: Integer
    hi = round h

{--------------------------------------------------------------------
  constraint implementation
--------------------------------------------------------------------}

class (Eq a, Hashable a) => ConstraintHandler a where
  toConstraintHandler :: a -> SomeConstraintHandler

  showConstraintHandler :: a -> IO String

  constrAttach :: Solver -> SomeConstraintHandler -> a -> IO Bool

  constrDetach :: Solver -> SomeConstraintHandler -> a -> IO ()

  constrIsLocked :: Solver -> SomeConstraintHandler -> a -> IO Bool

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

  -- | deduce a clause C∨l from the constraint and return C.
  -- C and l should be false and true respectively under the current
  -- assignment.
  constrReasonOf :: Solver -> a -> Maybe Lit -> IO Clause

  constrOnUnassigned :: Solver -> SomeConstraintHandler -> a -> Lit -> IO ()

  isPBRepresentable :: a -> IO Bool
  toPBLinAtLeast :: a -> IO PBLinAtLeast

  isSatisfied :: Solver -> a -> IO Bool

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

  constrWeight :: Solver -> a -> IO Double
  constrWeight _ _ = return 1.0

  constrReadActivity :: a -> IO Double

  constrWriteActivity :: a -> Double -> IO ()

attach :: Solver -> SomeConstraintHandler -> IO Bool
attach solver c = constrAttach solver c c

detach :: Solver -> SomeConstraintHandler -> IO ()
detach solver c = do
  constrDetach solver c c
  b <- isPBRepresentable c
  when b $ do
    (lhs,_) <- toPBLinAtLeast c
    forM_ lhs $ \(_,lit) -> do
      Vec.unsafeModify (svLitOccurList solver) (litIndex lit) (HashSet.delete c)

-- | invoked with the watched literal when the literal is falsified.
propagate :: Solver -> SomeConstraintHandler -> Lit -> IO Bool
propagate solver c l = constrPropagate solver c c l

-- | deduce a clause C∨l from the constraint and return C.
-- C and l should be false and true respectively under the current
-- assignment.
reasonOf :: ConstraintHandler a => Solver -> a -> Maybe Lit -> IO Clause
reasonOf solver c x = do
  when debugMode $
    case x of
      Nothing -> return ()
      Just lit -> do
        val <- litValue solver lit
        unless (lTrue == val) $ do
          str <- showConstraintHandler c
          error (printf "reasonOf: value of literal %d should be True but %s (constrReasonOf %s %s)" lit (show val) str (show x))
  cl <- constrReasonOf solver c x
  when debugMode $ do
    forM_ cl $ \lit -> do
      val <- litValue solver lit
      unless (lFalse == val) $ do
        str <- showConstraintHandler c
        error (printf "reasonOf: value of literal %d should be False but %s (constrReasonOf %s %s)" lit (show val) str (show x))
  return cl

isLocked :: Solver -> SomeConstraintHandler -> IO Bool
isLocked solver c = constrIsLocked solver c c

data SomeConstraintHandler
  = CHClause !ClauseHandler
  | CHAtLeast !AtLeastHandler
  | CHPBCounter !PBHandlerCounter
  | CHPBPueblo !PBHandlerPueblo
  | CHXORClause !XORClauseHandler
  | CHTheory !TheoryHandler
  deriving Eq

instance Hashable SomeConstraintHandler where
  hashWithSalt s (CHClause c)    = s `hashWithSalt` (0::Int) `hashWithSalt` c
  hashWithSalt s (CHAtLeast c)   = s `hashWithSalt` (1::Int) `hashWithSalt` c
  hashWithSalt s (CHPBCounter c) = s `hashWithSalt` (2::Int) `hashWithSalt` c
  hashWithSalt s (CHPBPueblo c)  = s `hashWithSalt` (3::Int) `hashWithSalt` c
  hashWithSalt s (CHXORClause c) = s `hashWithSalt` (4::Int) `hashWithSalt` c
  hashWithSalt s (CHTheory c)    = s `hashWithSalt` (5::Int) `hashWithSalt` c

instance ConstraintHandler SomeConstraintHandler where
  toConstraintHandler = id

  showConstraintHandler (CHClause c)    = showConstraintHandler c
  showConstraintHandler (CHAtLeast c)   = showConstraintHandler c
  showConstraintHandler (CHPBCounter c) = showConstraintHandler c
  showConstraintHandler (CHPBPueblo c)  = showConstraintHandler c
  showConstraintHandler (CHXORClause c) = showConstraintHandler c
  showConstraintHandler (CHTheory c)    = showConstraintHandler c

  constrAttach solver this (CHClause c)    = constrAttach solver this c
  constrAttach solver this (CHAtLeast c)   = constrAttach solver this c
  constrAttach solver this (CHPBCounter c) = constrAttach solver this c
  constrAttach solver this (CHPBPueblo c)  = constrAttach solver this c
  constrAttach solver this (CHXORClause c) = constrAttach solver this c
  constrAttach solver this (CHTheory c)    = constrAttach solver this c

  constrDetach solver this (CHClause c)    = constrDetach solver this c
  constrDetach solver this (CHAtLeast c)   = constrDetach solver this c
  constrDetach solver this (CHPBCounter c) = constrDetach solver this c
  constrDetach solver this (CHPBPueblo c)  = constrDetach solver this c
  constrDetach solver this (CHXORClause c) = constrDetach solver this c
  constrDetach solver this (CHTheory c)    = constrDetach solver this c

  constrIsLocked solver this (CHClause c)    = constrIsLocked solver this c
  constrIsLocked solver this (CHAtLeast c)   = constrIsLocked solver this c
  constrIsLocked solver this (CHPBCounter c) = constrIsLocked solver this c
  constrIsLocked solver this (CHPBPueblo c)  = constrIsLocked solver this c
  constrIsLocked solver this (CHXORClause c) = constrIsLocked solver this c
  constrIsLocked solver this (CHTheory c)    = constrIsLocked solver this c

  constrPropagate solver this (CHClause c)  lit   = constrPropagate solver this c lit
  constrPropagate solver this (CHAtLeast c) lit   = constrPropagate solver this c lit
  constrPropagate solver this (CHPBCounter c) lit = constrPropagate solver this c lit
  constrPropagate solver this (CHPBPueblo c) lit  = constrPropagate solver this c lit
  constrPropagate solver this (CHXORClause c) lit = constrPropagate solver this c lit
  constrPropagate solver this (CHTheory c) lit    = constrPropagate solver this c lit

  constrReasonOf solver (CHClause c)  l   = constrReasonOf solver c l
  constrReasonOf solver (CHAtLeast c) l   = constrReasonOf solver c l
  constrReasonOf solver (CHPBCounter c) l = constrReasonOf solver c l
  constrReasonOf solver (CHPBPueblo c) l  = constrReasonOf solver c l
  constrReasonOf solver (CHXORClause c) l = constrReasonOf solver c l
  constrReasonOf solver (CHTheory c) l    = constrReasonOf solver c l

  constrOnUnassigned solver this (CHClause c)  l   = constrOnUnassigned solver this c l
  constrOnUnassigned solver this (CHAtLeast c) l   = constrOnUnassigned solver this c l
  constrOnUnassigned solver this (CHPBCounter c) l = constrOnUnassigned solver this c l
  constrOnUnassigned solver this (CHPBPueblo c) l  = constrOnUnassigned solver this c l
  constrOnUnassigned solver this (CHXORClause c) l = constrOnUnassigned solver this c l
  constrOnUnassigned solver this (CHTheory c) l    = constrOnUnassigned solver this c l

  isPBRepresentable (CHClause c)    = isPBRepresentable c
  isPBRepresentable (CHAtLeast c)   = isPBRepresentable c
  isPBRepresentable (CHPBCounter c) = isPBRepresentable c
  isPBRepresentable (CHPBPueblo c)  = isPBRepresentable c
  isPBRepresentable (CHXORClause c) = isPBRepresentable c
  isPBRepresentable (CHTheory c)    = isPBRepresentable c

  toPBLinAtLeast (CHClause c)    = toPBLinAtLeast c
  toPBLinAtLeast (CHAtLeast c)   = toPBLinAtLeast c
  toPBLinAtLeast (CHPBCounter c) = toPBLinAtLeast c
  toPBLinAtLeast (CHPBPueblo c)  = toPBLinAtLeast c
  toPBLinAtLeast (CHXORClause c) = toPBLinAtLeast c
  toPBLinAtLeast (CHTheory c)    = toPBLinAtLeast c

  isSatisfied solver (CHClause c)    = isSatisfied solver c
  isSatisfied solver (CHAtLeast c)   = isSatisfied solver c
  isSatisfied solver (CHPBCounter c) = isSatisfied solver c
  isSatisfied solver (CHPBPueblo c)  = isSatisfied solver c
  isSatisfied solver (CHXORClause c) = isSatisfied solver c
  isSatisfied solver (CHTheory c)    = isSatisfied solver c

  constrIsProtected solver (CHClause c)    = constrIsProtected solver c
  constrIsProtected solver (CHAtLeast c)   = constrIsProtected solver c
  constrIsProtected solver (CHPBCounter c) = constrIsProtected solver c
  constrIsProtected solver (CHPBPueblo c)  = constrIsProtected solver c
  constrIsProtected solver (CHXORClause c) = constrIsProtected solver c
  constrIsProtected solver (CHTheory c)    = constrIsProtected solver c

  constrReadActivity (CHClause c)    = constrReadActivity c
  constrReadActivity (CHAtLeast c)   = constrReadActivity c
  constrReadActivity (CHPBCounter c) = constrReadActivity c
  constrReadActivity (CHPBPueblo c)  = constrReadActivity c
  constrReadActivity (CHXORClause c) = constrReadActivity c
  constrReadActivity (CHTheory c)    = constrReadActivity c

  constrWriteActivity (CHClause c)    aval = constrWriteActivity c aval
  constrWriteActivity (CHAtLeast c)   aval = constrWriteActivity c aval
  constrWriteActivity (CHPBCounter c) aval = constrWriteActivity c aval
  constrWriteActivity (CHPBPueblo c)  aval = constrWriteActivity c aval
  constrWriteActivity (CHXORClause c) aval = constrWriteActivity c aval
  constrWriteActivity (CHTheory c)    aval = constrWriteActivity c aval

isReasonOf :: Solver -> SomeConstraintHandler -> Lit -> IO Bool
isReasonOf solver c lit = do
  val <- litValue solver lit
  if val == lUndef then
    return False
  else do
    m <- varReason solver (litVar lit)
    case m of
      Nothing -> return False
      Just c2  -> return $! c == c2

-- To avoid heap-allocation Maybe value, it returns -1 when not found.
findForWatch :: Solver -> LitArray -> Int -> Int -> IO Int
#ifndef __GLASGOW_HASKELL__
findForWatch solver a beg end = go beg end
  where
    go :: Int -> Int -> IO Int
    go i end | i > end = return (-1)
    go i end = do
      val <- litValue s =<< readLitArray a i
      if val /= lFalse
        then return i
        else go (i+1) end
#else
{- We performed worker-wrapper transfomation manually, since the worker
   generated by GHC has type
   "Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int #)",
   not "Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int# #)".
   We want latter one to avoid heap-allocating Int value. -}
findForWatch solver a (I# beg) (I# end) = IO $ \w ->
  case go# beg end w of
    (# w2, ret #) -> (# w2, I# ret #)
  where
    go# :: Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int# #)
    go# i end' w | isTrue# (i ># end') = (# w, -1# #)
    go# i end' w =
      case unIO (litValue solver =<< readLitArray a (I# i)) w of
        (# w2, val #) ->
          if val /= lFalse
            then (# w2, i #)
            else go# (i +# 1#) end' w2

    unIO (IO f) = f
#endif

-- To avoid heap-allocating Maybe value, it returns -1 when not found.
findForWatch2 :: Solver -> LitArray -> Int -> Int -> IO Int
#ifndef __GLASGOW_HASKELL__
findForWatch2 solver a beg end = go beg end
  where
    go :: Int -> Int -> IO Int
    go i end | i > end = return (-1)
    go i end = do
      val <- litValue s =<< readLitArray a i
      if val == lUndef
        then return i
        else go (i+1) end
#else
{- We performed worker-wrapper transfomation manually, since the worker
   generated by GHC has type
   "Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int #)",
   not "Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int# #)".
   We want latter one to avoid heap-allocating Int value. -}
findForWatch2 solver a (I# beg) (I# end) = IO $ \w ->
  case go# beg end w of
    (# w2, ret #) -> (# w2, I# ret #)
  where
    go# :: Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int# #)
    go# i end w | isTrue# (i ># end) = (# w, -1# #)
    go# i end w =
      case unIO (litValue solver =<< readLitArray a (I# i)) w of
        (# w2, val #) ->
          if val == lUndef
            then (# w2, i #)
            else go# (i +# 1#) end w2

    unIO (IO f) = f
#endif

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

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

claGetSize :: ClauseHandler -> IO Int
claGetSize cla = getLitArraySize (claLits cla)

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

instance Hashable ClauseHandler where
  hash = claHash
  hashWithSalt = defaultHashWithSalt

newClauseHandler :: Clause -> Bool -> IO ClauseHandler
newClauseHandler ls learnt = do
  a <- newLitArray ls
  act <- newIORef $! (if learnt then 0 else -1)
  return (ClauseHandler a act (hash ls))

instance ConstraintHandler ClauseHandler where
  toConstraintHandler = CHClause

  showConstraintHandler this = do
    lits <- getLits (claLits this)
    return (show lits)

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

    size <- claGetSize this2
    if size == 0 then do
      markBad solver
      return False
    else if size == 1 then do
      lit0 <- readLitArray (claLits this2) 0
      assignBy solver lit0 this
    else do
      ref <- newIORef 1
      let f i = do
            lit_i <- readLitArray (claLits this2) i
            val_i <- litValue solver lit_i
            if val_i /= lFalse then
              return True
            else do
              j <- readIORef ref
              k <- findForWatch solver (claLits this2) j (size - 1)
              case k of
                -1 -> do
                  return False
                _ -> do
                  lit_k <- readLitArray (claLits this2) k
                  writeLitArray (claLits this2) i lit_k
                  writeLitArray (claLits this2) k lit_i
                  writeIORef ref $! (k+1)
                  return True

      b <- f 0
      if b then do
        lit0 <- readLitArray (claLits this2) 0
        watchLit solver lit0 this
        b2 <- f 1
        if b2 then do
          lit1 <- readLitArray (claLits this2) 1
          watchLit solver lit1 this
          return True
        else do -- UNIT
          -- We need to watch the most recently falsified literal
          (i,_) <- liftM (maximumBy (comparing snd)) $ forM [1..size-1] $ \l -> do
            lit <- readLitArray (claLits this2) l
            lv <- litLevel solver lit
            return (l,lv)
          lit1 <- readLitArray (claLits this2) 1
          liti <- readLitArray (claLits this2) i
          writeLitArray (claLits this2) 1 liti
          writeLitArray (claLits this2) i lit1
          watchLit solver liti this
          assignBy solver lit0 this -- should always succeed
      else do -- CONFLICT
        ls <- liftM (map fst . sortBy (comparing (Down . snd))) $ forM [0..size-1] $ \l -> do
          lit <- readLitArray (claLits this2) l
          lv <- litLevel solver lit
          return (l,lv)
        forM_ (zip [0..] ls) $ \(i,lit) -> do
          writeLitArray (claLits this2) i lit
        lit0 <- readLitArray (claLits this2) 0
        lit1 <- readLitArray (claLits this2) 1
        watchLit solver lit0 this
        watchLit solver lit1 this
        return False

  constrDetach solver this this2 = do
    size <- claGetSize this2
    when (size >= 2) $ do
      lit0 <- readLitArray (claLits this2) 0
      lit1 <- readLitArray (claLits this2) 1
      unwatchLit solver lit0 this
      unwatchLit solver lit1 this

  constrIsLocked solver this this2 = do
    size <- claGetSize this2
    if size < 2 then
      return False
    else do
      lit <- readLitArray (claLits this2) 0
      isReasonOf solver this lit

  constrPropagate !solver this this2 !falsifiedLit = do
    preprocess

    !lit0 <- readLitArray a 0
    !val0 <- litValue solver lit0
    if val0 == lTrue then do
      watchLit solver falsifiedLit this
      return True
    else do
      size <- claGetSize this2
      i <- findForWatch solver a 2 (size - 1)
      case i of
        -1 -> do
          when debugMode $ logIO solver $ do
             str <- showConstraintHandler this
             return $ printf "constrPropagate: %s is unit" str
          watchLit solver falsifiedLit this
          assignBy solver lit0 this
        _  -> do
          !lit1 <- readLitArray a 1
          !liti <- readLitArray a i
          writeLitArray a 1 liti
          writeLitArray a i lit1
          watchLit solver liti this
          return True

    where
      a = claLits this2

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

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

  constrOnUnassigned _solver _this _this2 _lit = return ()

  isPBRepresentable _ = return True

  toPBLinAtLeast this = do
    lits <- getLits (claLits this)
    return ([(1,l) | l <- lits], 1)

  isSatisfied solver this = do
    n <- getLitArraySize (claLits this)
    liftM isLeft $ runExceptT $ forLoop 0 (<n) (+1) $ \i -> do
      v <- lift $ litValue solver =<< readLitArray (claLits this) i
      when (v == lTrue) $ throwE ()

  constrIsProtected _ this = do
    size <- claGetSize this
    return $! size <= 2

  constrReadActivity this = readIORef (claActivity this)

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

basicAttachClauseHandler :: Solver -> ClauseHandler -> IO Bool
basicAttachClauseHandler solver this = do
  let constr = toConstraintHandler this
  lits <- getLits (claLits this)
  case lits of
    [] -> do
      markBad solver
      return False
    [l1] -> do
      assignBy solver l1 constr
    l1:l2:_ -> do
      watchLit solver l1 constr
      watchLit solver l2 constr
      return True

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

data AtLeastHandler
  = AtLeastHandler
  { atLeastLits :: !LitArray
  , atLeastNum :: !Int
  , atLeastActivity :: !(IORef Double)
  , atLeastHash :: !Int
  }

instance Eq AtLeastHandler where
  (==) = (==) `on` atLeastLits

instance Hashable AtLeastHandler where
  hash = atLeastHash
  hashWithSalt = defaultHashWithSalt

newAtLeastHandler :: [Lit] -> Int -> Bool -> IO AtLeastHandler
newAtLeastHandler ls n learnt = do
  a <- newLitArray ls
  act <- newIORef $! (if learnt then 0 else -1)
  return (AtLeastHandler a n act (hash (ls,n)))

instance ConstraintHandler AtLeastHandler where
  toConstraintHandler = CHAtLeast

  showConstraintHandler this = do
    lits <- getLits (atLeastLits this)
    return $ show lits ++ " >= " ++ show (atLeastNum this)

  -- FIXME: simplify implementation
  constrAttach solver this this2 = do
    -- BCP Queue should be empty at this point.
    -- If not, duplicated propagation happens.
    bcpCheckEmpty solver

    let a = atLeastLits this2
    m <- getLitArraySize a
    let n = atLeastNum this2

    if m < n then do
      markBad solver
      return False
    else if m == n then do
      let f i = do
            lit <- readLitArray a i
            assignBy solver lit this
      allM f [0..n-1]
    else do -- m > n
      let f !i !j
            | i == n = do
                -- NOT VIOLATED: n literals (0 .. n-1) are watched
                k <- findForWatch solver a j (m - 1)
                if k /= -1 then do
                  -- NOT UNIT
                  lit_n <- readLitArray a n
                  lit_k <- readLitArray a k
                  writeLitArray a n lit_k
                  writeLitArray a k lit_n
                  watchLit solver lit_k this
                  -- n+1 literals (0 .. n) are watched.
                else do
                  -- UNIT
                  forLoop 0 (<n) (+1) $ \l -> do
                    lit <- readLitArray a l
                    _ <- assignBy solver lit this -- should always succeed
                    return ()
                  -- We need to watch the most recently falsified literal
                  (l,_) <- liftM (maximumBy (comparing snd)) $ forM [n..m-1] $ \l -> do
                    lit <- readLitArray a l
                    lv <- litLevel solver lit
                    when debugMode $ do
                      val <- litValue solver lit
                      unless (val == lFalse) $ error "AtLeastHandler.attach: should not happen"
                    return (l,lv)
                  lit_n <- readLitArray a n
                  lit_l <- readLitArray a l
                  writeLitArray a n lit_l
                  writeLitArray a l lit_n
                  watchLit solver lit_l this
                  -- n+1 literals (0 .. n) are watched.
                return True
            | otherwise = do
                assert (i < n && n <= j) $ return ()
                lit_i <- readLitArray a i
                val_i <- litValue solver lit_i
                if val_i /= lFalse then do
                  watchLit solver lit_i this
                  f (i+1) j
                else do
                  k <- findForWatch solver a j (m - 1)
                  if k /= -1 then do
                    lit_k <- readLitArray a k
                    writeLitArray a i lit_k
                    writeLitArray a k lit_i
                    watchLit solver lit_k this
                    f (i+1) (k+1)
                  else do
                    -- CONFLICT
                    -- We need to watch unassigned literals or most recently falsified literals.
                    do xs <- liftM (sortBy (comparing (Down . snd))) $ forM [i..m-1] $ \l -> do
                         lit <- readLitArray a l
                         val <- litValue solver lit
                         if val == lFalse then do
                           lv <- litLevel solver lit
                           return (lit, lv)
                         else do
                           return (lit, maxBound)
                       forM_ (zip [i..m-1] xs) $ \(l,(lit,_lv)) -> do
                         writeLitArray a l lit
                    forLoop i (<=n) (+1) $ \l -> do
                      lit_l <- readLitArray a l
                      watchLit solver lit_l this
                    -- n+1 literals (0 .. n) are watched.
                    return False
      f 0 n

  constrDetach solver this this2 = do
    lits <- getLits (atLeastLits this2)
    let n = atLeastNum this2
    when (length lits > n) $ do
      forLoop 0 (<=n) (+1) $ \i -> do
        lit <- readLitArray (atLeastLits this2) i
        unwatchLit solver lit this

  constrIsLocked solver this this2 = do
    size <- getLitArraySize (atLeastLits this2)
    let n = atLeastNum this2
        loop i
          | i > n = return False
          | otherwise = do
              l <- readLitArray (atLeastLits this2) i
              b <- isReasonOf solver this l
              if b then return True else loop (i+1)
    if size >= n+1 then
      loop 0
    else
      return False

  constrPropagate solver this this2 falsifiedLit = do
    preprocess

    when debugMode $ do
      litn <- readLitArray a n
      unless (litn == falsifiedLit) $ error "AtLeastHandler.constrPropagate: should not happen"

    m <- getLitArraySize a
    i <- findForWatch solver a (n+1) (m-1)
    case i of
      -1 -> do
        when debugMode $ logIO solver $ do
          str <- showConstraintHandler this
          return $ printf "constrPropagate: %s is unit" str
        watchLit solver falsifiedLit this
        let loop :: Int -> IO Bool
            loop j
              | j >= n = return True
              | otherwise = do
                  litj <- readLitArray a j
                  ret2 <- assignBy solver litj this
                  if ret2
                    then loop (j+1)
                    else return False
        loop 0
      _ -> do
        liti <- readLitArray a i
        litn <- readLitArray a n
        writeLitArray a i litn
        writeLitArray a n liti
        watchLit solver liti this
        return True

    where
      a = atLeastLits this2
      n = atLeastNum this2

      preprocess :: IO ()
      preprocess = loop 0
        where
          loop :: Int -> IO ()
          loop i
            | i >= n = return ()
            | otherwise = do
              li <- readLitArray a i
              if (li /= falsifiedLit) then
                loop (i+1)
              else do
                ln <- readLitArray a n
                writeLitArray a n li
                writeLitArray a i ln

  constrReasonOf solver this concl = do
    m <- getLitArraySize (atLeastLits this)
    let n = atLeastNum this
    falsifiedLits <- mapM (readLitArray (atLeastLits this)) [n..m-1] -- drop first n elements
    when debugMode $ do
      forM_ falsifiedLits $ \lit -> do
        val <- litValue solver lit
        unless (val == lFalse) $ do
          error $ printf "AtLeastHandler.constrReasonOf: %d is %s (lFalse expected)" lit (show val)
    case concl of
      Nothing -> do
        let go :: Int -> IO Lit
            go i
              | i >= n = error $ printf "AtLeastHandler.constrReasonOf: cannot find falsified literal in first %d elements" n
              | otherwise = do
                  lit <- readLitArray (atLeastLits this) i
                  val <- litValue solver lit
                  if val == lFalse
                  then return lit
                  else go (i+1)
        lit <- go 0
        return $ lit : falsifiedLits
      Just lit -> do
        when debugMode $ do
          es <- getLits (atLeastLits this)
          unless (lit `elem` take n es) $
            error $ printf "AtLeastHandler.constrReasonOf: cannot find %d in first %d elements" n
        return falsifiedLits

  constrOnUnassigned _solver _this _this2 _lit = return ()

  isPBRepresentable _ = return True

  toPBLinAtLeast this = do
    lits <- getLits (atLeastLits this)
    return ([(1,l) | l <- lits], fromIntegral (atLeastNum this))

  isSatisfied solver this = do
    m <- getLitArraySize (atLeastLits this)
    liftM isLeft $ runExceptT $ numLoopState 0 (m-1) 0 $ \(!n) i -> do
      v <- lift $ litValue solver =<< readLitArray (atLeastLits this) i
      if v /= lTrue then do
        return n
      else do
        let n' = n + 1
        when (n' >= atLeastNum this) $ throwE ()
        return n'

  constrReadActivity this = readIORef (atLeastActivity this)

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

basicAttachAtLeastHandler :: Solver -> AtLeastHandler -> IO Bool
basicAttachAtLeastHandler solver this = do
  lits <- getLits (atLeastLits this)
  let m = length lits
      n = atLeastNum this
      constr = toConstraintHandler this
  if m < n then do
    markBad solver
    return False
  else if m == n then do
    allM (\l -> assignBy solver l constr) lits
  else do -- m > n
    forM_ (take (n+1) lits) $ \l -> watchLit solver l constr
    return True

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

newPBHandler :: Solver -> PBLinSum -> Integer -> Bool -> IO SomeConstraintHandler
newPBHandler solver ts degree learnt = do
  config <- configPBHandlerType <$> getConfig solver
  case config of
    PBHandlerTypeCounter -> do
      c <- newPBHandlerCounter ts degree learnt
      return (toConstraintHandler c)
    PBHandlerTypePueblo -> do
      c <- newPBHandlerPueblo ts degree learnt
      return (toConstraintHandler c)

newPBHandlerPromoted :: Solver -> PBLinSum -> Integer -> Bool -> IO SomeConstraintHandler
newPBHandlerPromoted solver lhs rhs learnt = do
  case pbToAtLeast (lhs,rhs) of
    Nothing -> newPBHandler solver lhs rhs learnt
    Just (lhs2, rhs2) -> do
      if rhs2 /= 1 then do
        h <- newAtLeastHandler lhs2 rhs2 learnt
        return $ toConstraintHandler h
      else do
        h <- newClauseHandler lhs2 learnt
        return $ toConstraintHandler h

pbOverSAT :: Solver -> PBLinAtLeast -> IO Bool
pbOverSAT solver (lhs, rhs) = do
  ss <- forM lhs $ \(c,l) -> do
    v <- litValue solver l
    if v /= lFalse
      then return c
      else return 0
  return $! sum ss > rhs

pbToAtLeast :: PBLinAtLeast -> Maybe AtLeast
pbToAtLeast (lhs, rhs) = do
  let cs = [c | (c,_) <- lhs]
  guard $ Set.size (Set.fromList cs) == 1
  let c = head cs
  return $ (map snd lhs, fromInteger ((rhs+c-1) `div` c))

pbToClause :: PBLinAtLeast -> Maybe Clause
pbToClause pb = do
  (lhs, rhs) <- pbToAtLeast pb
  guard $ rhs == 1
  return lhs

{--------------------------------------------------------------------
  Pseudo Boolean Constraint (Counter)
--------------------------------------------------------------------}

data PBHandlerCounter
  = PBHandlerCounter
  { pbTerms    :: !PBLinSum -- sorted in the decending order on coefficients.
  , pbDegree   :: !Integer
  , pbCoeffMap :: !(LitMap Integer)
  , pbMaxSlack :: !Integer
  , pbSlack    :: !(IORef Integer)
  , pbActivity :: !(IORef Double)
  , pbHash     :: !Int
  }

instance Eq PBHandlerCounter where
  (==) = (==) `on` pbSlack

instance Hashable PBHandlerCounter where
  hash = pbHash
  hashWithSalt = defaultHashWithSalt

newPBHandlerCounter :: PBLinSum -> Integer -> Bool -> IO PBHandlerCounter
newPBHandlerCounter ts degree learnt = do
  let ts' = sortBy (comparing (Down . fst)) ts
      slack = sum (map fst ts) - degree
      m = IM.fromList [(l,c) | (c,l) <- ts]
  s <- newIORef slack
  act <- newIORef $! (if learnt then 0 else -1)
  return (PBHandlerCounter ts' degree m slack s act (hash (ts,degree)))

instance ConstraintHandler PBHandlerCounter where
  toConstraintHandler = CHPBCounter

  showConstraintHandler this = do
    return $ show (pbTerms this) ++ " >= " ++ show (pbDegree this)

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

  constrDetach solver this this2 = do
    forM_ (pbTerms this2) $ \(_,l) -> do
      unwatchLit solver l this

  constrIsLocked solver this this2 = do
    anyM (\(_,l) -> isReasonOf solver this l) (pbTerms this2)

  constrPropagate solver this this2 falsifiedLit = do
    watchLit solver falsifiedLit this
    let c = pbCoeffMap this2 IM.! falsifiedLit
    modifyIORef' (pbSlack this2) (subtract c)
    addOnUnassigned solver this falsifiedLit
    s <- readIORef (pbSlack this2)
    if s < 0 then
      return False
    else do
      forM_ (takeWhile (\(c1,_) -> c1 > s) (pbTerms this2)) $ \(_,l1) -> do
        v <- litValue solver l1
        when (v == lUndef) $ do
          assignBy solver l1 this
          return ()
      return True

  constrReasonOf solver this l = do
    case l of
      Nothing -> do
        let p _ = return True
        f p (pbMaxSlack this) (pbTerms this)
      Just lit -> do
        idx <- varAssignNo solver (litVar lit)
        -- PB制約の場合には複数回unitになる可能性があり、
        -- litへの伝播以降に割り当てられたリテラルを含まないよう注意が必要
        let p lit2 =do
              idx2 <- varAssignNo solver (litVar lit2)
              return $ idx2 < idx
        let c = pbCoeffMap this IM.! lit
        f p (pbMaxSlack this - c) (pbTerms this)
    where
      {-# INLINE f #-}
      f :: (Lit -> IO Bool) -> Integer -> PBLinSum -> IO [Lit]
      f p s xs = go s xs []
        where
          go :: Integer -> PBLinSum -> [Lit] -> IO [Lit]
          go s _ ret | s < 0 = return ret
          go _ [] _ = error "PBHandlerCounter.constrReasonOf: should not happen"
          go s ((c,lit):xs) ret = do
            val <- litValue solver lit
            if val == lFalse then do
              b <- p lit
              if b
              then go (s - c) xs (lit:ret)
              else go s xs ret
            else do
              go s xs ret

  constrOnUnassigned _solver _this this2 lit = do
    let c = pbCoeffMap this2 IM.! (- lit)
    modifyIORef' (pbSlack this2) (+ c)

  isPBRepresentable _ = return True

  toPBLinAtLeast this = do
    return (pbTerms this, pbDegree this)

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

  constrWeight _ _ = return 0.5

  constrReadActivity this = readIORef (pbActivity this)

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

{--------------------------------------------------------------------
  Pseudo Boolean Constraint (Pueblo)
--------------------------------------------------------------------}

data PBHandlerPueblo
  = PBHandlerPueblo
  { puebloTerms     :: !PBLinSum
  , puebloDegree    :: !Integer
  , puebloMaxSlack  :: !Integer
  , puebloWatches   :: !(IORef LitSet)
  , puebloWatchSum  :: !(IORef Integer)
  , puebloActivity  :: !(IORef Double)
  , puebloHash      :: !Int
  }

instance Eq PBHandlerPueblo where
  (==) = (==) `on` puebloWatchSum

instance Hashable PBHandlerPueblo where
  hash = puebloHash
  hashWithSalt = defaultHashWithSalt

puebloAMax :: PBHandlerPueblo -> Integer
puebloAMax this =
  case puebloTerms this of
    (c,_):_ -> c
    [] -> 0 -- should not happen?

newPBHandlerPueblo :: PBLinSum -> Integer -> Bool -> IO PBHandlerPueblo
newPBHandlerPueblo ts degree learnt = do
  let ts' = sortBy (comparing (Down . fst)) ts
      slack = sum [c | (c,_) <- ts'] - degree
  ws   <- newIORef IS.empty
  wsum <- newIORef 0
  act  <- newIORef $! (if learnt then 0 else -1)
  return $ PBHandlerPueblo ts' degree slack ws wsum act (hash (ts,degree))

puebloGetWatchSum :: PBHandlerPueblo -> IO Integer
puebloGetWatchSum pb = readIORef (puebloWatchSum pb)

puebloWatch :: Solver -> SomeConstraintHandler -> PBHandlerPueblo -> PBLinTerm -> IO ()
puebloWatch solver constr !pb (c, lit) = do
  watchLit solver lit constr
  modifyIORef' (puebloWatches pb) (IS.insert lit)
  modifyIORef' (puebloWatchSum pb) (+c)

puebloUnwatch :: Solver -> PBHandlerPueblo -> PBLinTerm -> IO ()
puebloUnwatch _solver pb (c, lit) = do
  modifyIORef' (puebloWatches pb) (IS.delete lit)
  modifyIORef' (puebloWatchSum pb) (subtract c)

instance ConstraintHandler PBHandlerPueblo where
  toConstraintHandler = CHPBPueblo

  showConstraintHandler this = do
    return $ show (puebloTerms this) ++ " >= " ++ show (puebloDegree this)

  constrAttach solver this this2 = do
    bcpCheckEmpty solver
    ret <- puebloPropagate solver this this2

    -- register to watch recently falsified literals to recover
    -- "WatchSum >= puebloDegree this + puebloAMax this" when backtrack is performed.
    wsum <- puebloGetWatchSum this2
    unless (wsum >= puebloDegree this2 + puebloAMax this2) $ do
      let f m tm@(_,lit) = do
            val <- litValue solver lit
            if val == lFalse then do
              idx <- varAssignNo solver (litVar lit)
              return (IM.insert idx tm m)
            else
              return m
      xs <- liftM (map snd . IM.toDescList) $ foldM f IM.empty (puebloTerms this2)
      let g !_ [] = return ()
          g !s ((c,l):ts) = do
            addOnUnassigned solver this l
            if s+c >= puebloDegree this2 + puebloAMax this2 then return ()
            else g (s+c) ts
      g wsum xs

    return ret

  constrDetach solver this this2 = do
    ws <- readIORef (puebloWatches this2)
    forM_ (IS.toList ws) $ \l -> do
      unwatchLit solver l this

  constrIsLocked solver this this2 = do
    anyM (\(_,l) -> isReasonOf solver this l) (puebloTerms this2)

  constrPropagate solver this this2 falsifiedLit = do
    let t = fromJust $ find (\(_,l) -> l==falsifiedLit) (puebloTerms this2)
    puebloUnwatch solver this2 t
    ret <- puebloPropagate solver this this2
    wsum <- puebloGetWatchSum this2
    unless (wsum >= puebloDegree this2 + puebloAMax this2) $
      addOnUnassigned solver this falsifiedLit
    return ret

  constrReasonOf solver this l = do
    case l of
      Nothing -> do
        let p _ = return True
        f p (puebloMaxSlack this) (puebloTerms this)
      Just lit -> do
        idx <- varAssignNo solver (litVar lit)
        -- PB制約の場合には複数回unitになる可能性があり、
        -- litへの伝播以降に割り当てられたリテラルを含まないよう注意が必要
        let p lit2 =do
              idx2 <- varAssignNo solver (litVar lit2)
              return $ idx2 < idx
        let c = fst $ fromJust $ find (\(_,l) -> l == lit) (puebloTerms this)
        f p (puebloMaxSlack this - c) (puebloTerms this)
    where
      {-# INLINE f #-}
      f :: (Lit -> IO Bool) -> Integer -> PBLinSum -> IO [Lit]
      f p s xs = go s xs []
        where
          go :: Integer -> PBLinSum -> [Lit] -> IO [Lit]
          go s _ ret | s < 0 = return ret
          go _ [] _ = error "PBHandlerPueblo.constrReasonOf: should not happen"
          go s ((c,lit):xs) ret = do
            val <- litValue solver lit
            if val == lFalse then do
              b <- p lit
              if b
              then go (s - c) xs (lit:ret)
              else go s xs ret
            else do
              go s xs ret

  constrOnUnassigned solver this this2 lit = do
    let t = fromJust $ find (\(_,l) -> l == - lit) (puebloTerms this2)
    puebloWatch solver this this2 t

  isPBRepresentable _ = return True

  toPBLinAtLeast this = do
    return (puebloTerms this, puebloDegree this)

  isSatisfied solver this = do
    xs <- forM (puebloTerms this) $ \(c,l) -> do
      v <- litValue solver l
      if v == lTrue
        then return c
        else return 0
    return $ sum xs >= puebloDegree this

  constrWeight _ _ = return 0.5

  constrReadActivity this = readIORef (puebloActivity this)

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

puebloPropagate :: Solver -> SomeConstraintHandler -> PBHandlerPueblo -> IO Bool
puebloPropagate solver constr this = do
  puebloUpdateWatchSum solver constr this
  watchsum <- puebloGetWatchSum this
  if puebloDegree this + puebloAMax this <= watchsum then
    return True
  else if watchsum < puebloDegree this then do
    -- CONFLICT
    return False
  else do -- puebloDegree this <= watchsum < puebloDegree this + puebloAMax this
    -- UNIT PROPAGATION
    let f [] = return True
        f ((c,lit) : ts) = do
          watchsum' <- puebloGetWatchSum this
          if watchsum' - c >= puebloDegree this then
            return True
          else do
            val <- litValue solver lit
            when (val == lUndef) $ do
              b <- assignBy solver lit constr
              assert b $ return ()
            f ts
    f $ puebloTerms this

puebloUpdateWatchSum :: Solver -> SomeConstraintHandler -> PBHandlerPueblo -> IO ()
puebloUpdateWatchSum solver constr this = do
  let f [] = return ()
      f (t@(_,lit):ts) = do
        watchSum <- puebloGetWatchSum this
        if watchSum >= puebloDegree this + puebloAMax this then
          return ()
        else do
          val <- litValue solver lit
          watched <- liftM (lit `IS.member`) $ readIORef (puebloWatches this)
          when (val /= lFalse && not watched) $ do
            puebloWatch solver constr this t
          f ts
  f (puebloTerms this)

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

data XORClauseHandler
  = XORClauseHandler
  { xorLits :: !LitArray
  , xorActivity :: !(IORef Double)
  , xorHash :: !Int
  }

instance Eq XORClauseHandler where
  (==) = (==) `on` xorLits

instance Hashable XORClauseHandler where
  hash = xorHash
  hashWithSalt = defaultHashWithSalt

newXORClauseHandler :: [Lit] -> Bool -> IO XORClauseHandler
newXORClauseHandler ls learnt = do
  a <- newLitArray ls
  act <- newIORef $! (if learnt then 0 else -1)
  return (XORClauseHandler a act (hash ls))

instance ConstraintHandler XORClauseHandler where
  toConstraintHandler = CHXORClause

  showConstraintHandler this = do
    lits <- getLits (xorLits this)
    return ("XOR " ++ show lits)

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

    let a = xorLits this2
    size <- getLitArraySize a

    if size == 0 then do
      markBad solver
      return False
    else if size == 1 then do
      lit0 <- readLitArray a 0
      assignBy solver lit0 this
    else do
      ref <- newIORef 1
      let f i = do
            lit_i <- readLitArray a i
            val_i <- litValue solver lit_i
            if val_i == lUndef then
              return True
            else do
              j <- readIORef ref
              k <- findForWatch2 solver a j (size - 1)
              case k of
                -1 -> do
                  return False
                _ -> do
                  lit_k <- readLitArray a k
                  writeLitArray a i lit_k
                  writeLitArray a k lit_i
                  writeIORef ref $! (k+1)
                  return True

      b <- f 0
      if b then do
        lit0 <- readLitArray a 0
        watchVar solver (litVar lit0) this
        b2 <- f 1
        if b2 then do
          lit1 <- readLitArray a 1
          watchVar solver (litVar lit1) this
          return True
        else do -- UNIT
          -- We need to watch the most recently falsified literal
          (i,_) <- liftM (maximumBy (comparing snd)) $ forM [1..size-1] $ \l -> do
            lit <- readLitArray a l
            lv <- litLevel solver lit
            return (l,lv)
          lit1 <- readLitArray a 1
          liti <- readLitArray a i
          writeLitArray a 1 liti
          writeLitArray a i lit1
          watchVar solver (litVar liti) this
          -- lit0 ⊕ y
          y <- do
            ref' <- newIORef False
            forLoop 1 (<size) (+1) $ \j -> do
              lit_j <- readLitArray a j
              val_j <- litValue solver lit_j
              modifyIORef' ref' (/= fromJust (unliftBool val_j))
            readIORef ref'
          assignBy solver (if y then litNot lit0 else lit0) this -- should always succeed
      else do
        ls <- liftM (map fst . sortBy (comparing (Down . snd))) $ forM [0..size-1] $ \l -> do
          lit <- readLitArray a l
          lv <- litLevel solver lit
          return (l,lv)
        forM_ (zip [0..] ls) $ \(i,lit) -> do
          writeLitArray a i lit
        lit0 <- readLitArray a 0
        lit1 <- readLitArray a 1
        watchVar solver (litVar lit0) this
        watchVar solver (litVar lit1) this
        isSatisfied solver this2

  constrDetach solver this this2 = do
    size <- getLitArraySize (xorLits this2)
    when (size >= 2) $ do
      lit0 <- readLitArray (xorLits this2) 0
      lit1 <- readLitArray (xorLits this2) 1
      unwatchVar solver (litVar lit0) this
      unwatchVar solver (litVar lit1) this

  constrIsLocked solver this this2 = do
    lit0 <- readLitArray (xorLits this2) 0
    lit1 <- readLitArray (xorLits this2) 1
    b0 <- isReasonOf solver this lit0
    b1 <- isReasonOf solver this lit1
    return $ b0 || b1

  constrPropagate !solver this this2 !falsifiedLit = do
    b <- constrIsLocked solver this this2
    if b then
      return True
    else do
      preprocess

      !lit0 <- readLitArray a 0
      !size <- getLitArraySize (xorLits this2)
      i <- findForWatch2 solver a 2 (size - 1)
      case i of
        -1 -> do
          when debugMode $ logIO solver $ do
             str <- showConstraintHandler this
             return $ printf "constrPropagate: %s is unit" str
          watchVar solver v this
          -- lit0 ⊕ y
          y <- do
            ref <- newIORef False
            forLoop 1 (<size) (+1) $ \j -> do
              lit_j <- readLitArray a j
              val_j <- litValue solver lit_j
              modifyIORef' ref (/= fromJust (unliftBool val_j))
            readIORef ref
          assignBy solver (if y then litNot lit0 else lit0) this
        _  -> do
          !lit1 <- readLitArray a 1
          !liti <- readLitArray a i
          writeLitArray a 1 liti
          writeLitArray a i lit1
          watchVar solver (litVar liti) this
          return True

    where
      v = litVar falsifiedLit
      a = xorLits this2

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

  constrReasonOf solver this l = do
    lits <- getLits (xorLits this)
    xs <-
      case l of
        Nothing -> mapM f lits
        Just lit -> do
         case lits of
           l1:ls -> do
             assert (litVar lit == litVar l1) $ return ()
             mapM f ls
           _ -> error "XORClauseHandler.constrReasonOf: should not happen"
    return xs
    where
      f :: Lit -> IO Lit
      f lit = do
        let v = litVar lit
        val <- varValue solver v
        return $ literal v (not (fromJust (unliftBool val)))

  constrOnUnassigned _solver _this _this2 _lit = return ()

  isPBRepresentable _ = return False

  toPBLinAtLeast _ = error "XORClauseHandler does not support toPBLinAtLeast"

  isSatisfied solver this = do
    lits <- getLits (xorLits this)
    vals <- mapM (litValue solver) lits
    let f x y
          | x == lUndef || y == lUndef = lUndef
          | otherwise = liftBool (x /= y)
    return $ foldl' f lFalse vals == lTrue

  constrIsProtected _ this = do
    size <- getLitArraySize (xorLits this)
    return $! size <= 2

  constrReadActivity this = readIORef (xorActivity this)

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

basicAttachXORClauseHandler :: Solver -> XORClauseHandler -> IO Bool
basicAttachXORClauseHandler solver this = do
  lits <- getLits (xorLits this)
  let constr = toConstraintHandler this
  case lits of
    [] -> do
      markBad solver
      return False
    [l1] -> do
      assignBy solver l1 constr
    l1:l2:_ -> do
      watchVar solver (litVar l1) constr
      watchVar solver (litVar l2) constr
      return True

{--------------------------------------------------------------------
  Arbitrary Boolean Theory
--------------------------------------------------------------------}

setTheory :: Solver -> TheorySolver -> IO ()
setTheory solver tsolver = do
  d <- getDecisionLevel solver
  assert (d == levelRoot) $ return ()

  m <- readIORef (svTheorySolver solver)
  case m of
    Just _ -> do
      error $ "ToySolver.SAT.setTheory: cannot replace TheorySolver"
    Nothing -> do
      writeIORef (svTheorySolver solver) (Just tsolver)
      ret <- deduce solver
      case ret of
        Nothing -> return ()
        Just _ -> markBad solver

getTheory :: Solver -> IO (Maybe TheorySolver)
getTheory solver = readIORef (svTheorySolver solver)

deduceT :: Solver -> ExceptT SomeConstraintHandler IO ()
deduceT solver = do
  mt <- liftIO $ readIORef (svTheorySolver solver)
  case mt of
    Nothing -> return ()
    Just t -> do
      n <- liftIO $ Vec.getSize (svTrail solver)
      let h = CHTheory TheoryHandler
          callback l = assignBy solver l h
          loop i = do
            when (i < n) $ do
              l <- liftIO $ Vec.unsafeRead (svTrail solver) i
              ok <- liftIO $ thAssertLit t callback l
              if ok then
                loop (i+1)
              else
                throwE h
      loop =<< liftIO (readIOURef (svTheoryChecked solver))
      b2 <- liftIO $ thCheck t callback
      if b2 then do
        liftIO $ writeIOURef (svTheoryChecked solver) n
      else
        throwE h

data TheoryHandler = TheoryHandler deriving (Eq)

instance Hashable TheoryHandler where
  hash _ = hash ()
  hashWithSalt = defaultHashWithSalt

instance ConstraintHandler TheoryHandler where
  toConstraintHandler = CHTheory

  showConstraintHandler _this = return "TheoryHandler"

  constrAttach _solver _this _this2 = error "TheoryHandler.constrAttach"

  constrDetach _solver _this _this2 = return ()

  constrIsLocked _solver _this _this2 = return True

  constrPropagate _solver _this _this2 _falsifiedLit =  error "TheoryHandler.constrPropagate"

  constrReasonOf solver _this l = do
    Just t <- readIORef (svTheorySolver solver)
    lits <- thExplain t l
    return $ [-lit | lit <- lits]

  constrOnUnassigned _solver _this _this2 _lit = return ()

  isPBRepresentable _this = return False

  toPBLinAtLeast _this = error "TheoryHandler.toPBLinAtLeast"

  isSatisfied _solver _this = error "TheoryHandler.isSatisfied"

  constrIsProtected _solver _this = error "TheoryHandler.constrIsProtected"

  constrReadActivity _this = return 0

  constrWriteActivity _this _aval = return ()

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

mkRestartSeq :: RestartStrategy -> Int -> Double -> [Int]
mkRestartSeq MiniSATRestarts = miniSatRestartSeq
mkRestartSeq ArminRestarts   = arminRestartSeq
mkRestartSeq LubyRestarts    = lubyRestartSeq

miniSatRestartSeq :: Int -> Double -> [Int]
miniSatRestartSeq start inc = iterate (ceiling . (inc *) . fromIntegral) start

{-
miniSatRestartSeq :: Int -> Double -> [Int]
miniSatRestartSeq start inc = map round $ iterate (inc*) (fromIntegral start)
-}

arminRestartSeq :: Int -> Double -> [Int]
arminRestartSeq start inc = go (fromIntegral start) (fromIntegral start)
  where
    go !inner !outer = round inner : go inner' outer'
      where
        (inner',outer') =
          if inner >= outer
          then (fromIntegral start, outer * inc)
          else (inner * inc, outer)

lubyRestartSeq :: Int -> Double -> [Int]
lubyRestartSeq start inc = map (ceiling . (fromIntegral start *) . luby inc) [0..]

{-
  Finite subsequences of the Luby-sequence:

  0: 1
  1: 1 1 2
  2: 1 1 2 1 1 2 4
  3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
  ...


-}
luby :: Double -> Integer -> Double
luby y x = go2 size1 sequ1 x
  where
    -- Find the finite subsequence that contains index 'x', and the
    -- size of that subsequence:
    (size1, sequ1) = go 1 0

    go :: Integer -> Integer -> (Integer, Integer)
    go size sequ
      | size < x+1 = go (2*size+1) (sequ+1)
      | otherwise  = (size, sequ)

    go2 :: Integer -> Integer -> Integer -> Double
    go2 size sequ x2
      | size-1 /= x2 = let size' = (size-1) `div` 2 in go2 size' (sequ - 1) (x2 `mod` size')
      | otherwise = y ^ sequ


{--------------------------------------------------------------------
  utility
--------------------------------------------------------------------}

allM :: Monad m => (a -> m Bool) -> [a] -> m Bool
allM p = go
  where
    go [] = return True
    go (x:xs) = do
      b <- p x
      if b
        then go xs
        else return False

anyM :: Monad m => (a -> m Bool) -> [a] -> m Bool
anyM p = go
  where
    go [] = return False
    go (x:xs) = do
      b <- p x
      if b
        then return True
        else go xs

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

#if !MIN_VERSION_hashable(1,4,3)

defaultHashWithSalt :: Hashable a => Int -> a -> Int
defaultHashWithSalt salt x = salt `combine` hash x
  where
    combine :: Int -> Int -> Int
    combine h1 h2 = (h1 * 16777619) `xor` h2

#endif

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

debugMode :: Bool
debugMode = False

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

dumpVarActivity :: Solver -> IO ()
dumpVarActivity solver = do
  log solver "Variable activity:"
  vs <- variables solver
  forM_ vs $ \v -> do
    activity <- varActivity solver v
    log solver $ printf "activity(%d) = %d" v activity

dumpConstrActivity :: Solver -> IO ()
dumpConstrActivity solver = do
  log solver "Learnt constraints activity:"
  xs <- learntConstraints solver
  forM_ xs $ \c -> do
    s <- showConstraintHandler c
    aval <- constrReadActivity c
    log solver $ printf "activity(%s) = %f" s aval

-- | set callback function for receiving messages.
setLogger :: Solver -> (String -> IO ()) -> IO ()
setLogger solver logger = do
  writeIORef (svLogger solver) (Just logger)

-- | Clear logger function set by 'setLogger'.
clearLogger :: Solver -> IO ()
clearLogger solver = do
  writeIORef (svLogger solver) Nothing

log :: Solver -> String -> IO ()
log solver msg = logIO solver (return msg)

logIO :: Solver -> IO String -> IO ()
logIO solver action = do
  m <- readIORef (svLogger solver)
  case m of
    Nothing -> return ()
    Just logger -> action >>= logger

msakai / toysolver / 767

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous