{-# LANGUAGE PatternSignatures
            ,MultiParamTypeClasses
            ,FunctionalDependencies
            ,FlexibleInstances
            ,FlexibleContexts
            ,GeneralizedNewtypeDeriving
            ,TypeSynonymInstances
            ,TypeOperators
            ,ParallelListComp
            ,BangPatterns
 #-}
{-# OPTIONS -cpp #-}






{-|

Funsat aims to be a reasonably efficient modern SAT solver that is easy to
integrate as a backend to other projects.  SAT is NP-complete, and thus has
reductions from many other interesting problems.  We hope this implementation
is efficient enough to make it useful to solve medium-size, real-world problem
mapped from another space.  We also aim to test the solver rigorously to
encourage confidence in its output.

One particular nicetie facilitating integration of Funsat into other projects
is the efficient calculation of an /unsatisfiable core/ for unsatisfiable
problems (see the "Funsat.Resolution" module).  In the case a problem is
unsatisfiable, as a by-product of checking the proof of unsatisfiability,
Funsat will generate a minimal set of input clauses that are also
unsatisfiable.

* 07 Jun 2008 21:43:42: N.B. because of the use of mutable arrays in the ST
monad, the solver will actually give _wrong_ answers if you compile without
optimisation.  Which is okay, 'cause that's really slow anyway.

[@Bibliography@]

  * ''Abstract DPLL and DPLL Modulo Theories''

  * ''Chaff: Engineering an Efficient SAT solver''

  * ''An Extensible SAT-solver'' by Niklas Een, Niklas Sorensson

  * ''Efficient Conflict Driven Learning in a Boolean Satisfiability Solver''
by Zhang, Madigan, Moskewicz, Malik

  * ''SAT-MICRO: petit mais costaud!'' by Conchon, Kanig, and Lescuyer

-}
module Funsat.Solver
#ifndef TESTING
        ( -- * Interface
          solve
        , solve1
        , Solution(..)
          -- ** Verification
        , verify
        , VerifyError(..)
          -- ** Configuration
        , DPLLConfig(..)
        , defaultConfig
          -- * Solver statistics
        , Stats(..)
        , ShowWrapped(..)
        , statTable
        , statSummary
        )
#endif
    where

{-
    This file is part of funsat.

    funsat is free software: you can redistribute it and/or modify
    it under the terms of the GNU Lesser General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    funsat is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU Lesser General Public License for more details.

    You should have received a copy of the GNU Lesser General Public License
    along with funsat.  If not, see <http://www.gnu.org/licenses/>.

    Copyright 2008 Denis Bueno
-}


import Control.Arrow( (&&&) )
import Control.Exception( assert )
import Control.Monad.Error hiding ( (>=>), forM_, runErrorT )
import Control.Monad.MonadST( MonadST(..) )
import Control.Monad.ST.Strict
import Control.Monad.State.Lazy hiding ( (>=>), forM_ )
import Data.Array.ST
import Data.Array.Unboxed
import Data.Foldable hiding ( sequence_ )
import Data.Int( Int64 )
import Data.List( intercalate, nub, tails, sortBy, sort )
import Data.Maybe
import Data.Ord( comparing )
import Data.STRef
import Data.Sequence( Seq )
-- import Debug.Trace (trace)
import Funsat.Monad
import Funsat.Utils
import Funsat.Resolution( ResolutionTrace(..), initResolutionTrace )
import Funsat.Types
import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum )
import Funsat.Resolution( ResolutionError(..) )
import Text.Printf( printf )
import qualified Data.Foldable as Fl
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import qualified Funsat.Resolution as Resolution
import qualified Text.Tabular as Tabular

-- * Interface

-- | Run the DPLL-based SAT solver on the given CNF instance.  Returns a
-- solution, along with internal solver statistics and possibly a resolution
-- trace.  The trace is for checking a proof of `Unsat', and thus is only
-- present when the result is `Unsat'.
solve :: DPLLConfig -> CNF -> (Solution, Stats, Maybe ResolutionTrace)
solve cfg fIn =
    -- To solve, we simply take baby steps toward the solution using solveStep,
    -- starting with an initial assignment.
--     trace ("input " ++ show f) $
    either (error "no solution") id $
    runST $
    evalSSTErrMonad
        (do initialAssignment <- liftST $ newSTUArray (V 1, V (numVars f)) 0
            (a, isUnsat) <- initialState initialAssignment
            if isUnsat then reportSolution (Unsat a)
                       else stepToSolution initialAssignment >>= reportSolution)
    SC{ cnf = f{ clauses = Set.empty }, dl = []
      , watches = undefined, learnt = undefined
      , propQ = Seq.empty, trail = [], numConfl = 0, level = undefined
      , numConflTotal = 0, numDecisions = 0, numImpl = 0
      , reason = Map.empty, varOrder = undefined
      , resolutionTrace = PartialResolutionTrace 1 [] [] Map.empty
      , dpllConfig = cfg }
  where
    f = preprocessCNF fIn
    -- If returns True, then problem is unsat.
    initialState :: MAssignment s -> DPLLMonad s (IAssignment, Bool)
    initialState m = do
      initialLevel <- liftST $ newSTUArray (V 1, V (numVars f)) noLevel
      modify $ \s -> s{ level = initialLevel }
      initialWatches <- liftST $ newSTArray (L (- (numVars f)), L (numVars f)) []
      modify $ \s -> s{ watches = initialWatches }
      initialLearnts <- liftST $ newSTArray (L (- (numVars f)), L (numVars f)) []
      modify $ \s -> s{ learnt = initialLearnts }
      initialVarOrder <- liftST $ newSTUArray (V 1, V (numVars f)) initialActivity
      modify $ \s -> s{ varOrder = VarOrder initialVarOrder }

      -- Watch each clause, making sure to bork if we find a contradiction.
      (`catchError`
       (const $ liftST (unsafeFreezeAss m) >>= \a -> return (a,True))) $ do
          forM_ (clauses f)
            (\c -> do cid <- nextTraceId
                      isConsistent <- watchClause m (c, cid) False
                      when (not isConsistent)
                        -- conflict data is ignored here, so safe to fake
                        (do traceClauseId cid ; throwError (L 0, [], 0)))
          a <- liftST (unsafeFreezeAss m)
          return (a, False)


-- | Solve with the default configuration `defaultConfig'.
solve1 :: CNF -> (Solution, Stats, Maybe ResolutionTrace)
solve1 f = solve (defaultConfig f) f

-- | This function applies `solveStep' recursively until SAT instance is
-- solved, starting with the given initial assignment.  It also implements the
-- conflict-based restarting (see `DPLLConfig').
stepToSolution :: MAssignment s -> DPLLMonad s Solution
stepToSolution assignment = do
    step <- solveStep assignment
    useRestarts <- gets (configUseRestarts . dpllConfig)
    isTimeToRestart <- uncurry ((>=)) `liftM`
               gets (numConfl &&& (configRestart . dpllConfig))
    case step of
      Left m -> do when (useRestarts && isTimeToRestart)
                     (do _stats <- extractStats
--                          trace ("Restarting...") $
--                           trace (statSummary stats) $
                         resetState m)
                   stepToSolution m
      Right s -> return s
  where
    resetState m = do
      modify $ \s -> s{ numConfl = 0 }
      -- Require more conflicts before next restart.
      modifySlot dpllConfig $ \s c ->
        s{ dpllConfig = c{ configRestart = ceiling (configRestartBump c
                                                   * fromIntegral (configRestart c))
                           } }
      lvl :: FrozenLevelArray <- gets level >>= liftST . unsafeFreeze
      undoneLits <- takeWhile (\l -> lvl ! (var l) > 0) `liftM` gets trail
      forM_ undoneLits $ const (undoOne m)
      modify $ \s -> s{ dl = [], propQ = Seq.empty }
      compactDB
      unsafeFreezeAss m >>= simplifyDB

reportSolution :: Solution -> DPLLMonad s (Solution, Stats, Maybe ResolutionTrace)
reportSolution s = do
    stats <- extractStats
    case s of
      Sat _   -> return (s, stats, Nothing)
      Unsat _ -> do
          resTrace <- constructResTrace s
          return (s, stats, Just resTrace)


-- | Configuration parameters for the solver.
data DPLLConfig = Cfg
    { configRestart :: !Int64      -- ^ Number of conflicts before a restart.
    , configRestartBump :: !Double -- ^ `configRestart' is altered after each
                                   -- restart by multiplying it by this value.
    , configUseVSIDS :: !Bool      -- ^ If true, use dynamic variable ordering.
    , configUseRestarts :: !Bool }
                  deriving Show

-- | A default configuration based on the formula to solve.
--
--  * restarts every 100 conflicts
--
--  * requires 1.5 as many restarts after restarting as before, each time
--
--  * VSIDS to be enabled
--
--  * restarts to be enabled
defaultConfig :: CNF -> DPLLConfig
defaultConfig _f = Cfg { configRestart = 100 -- fromIntegral $ max (numVars f `div` 10) 100
                      , configRestartBump = 1.5
                      , configUseVSIDS = True
                      , configUseRestarts = True }

-- * Preprocessing

-- | Some kind of preprocessing.
--
--   * remove duplicates
preprocessCNF :: CNF -> CNF
preprocessCNF f = f{clauses = simpClauses (clauses f)}
    where simpClauses = Set.map nub -- rm dups

-- | Simplify the clause database.  Eventually should supersede, probably,
-- `preprocessCNF'.
--
-- Precondition: decision level 0.
simplifyDB :: IAssignment -> DPLLMonad s ()
simplifyDB mFr = do
  -- For each clause in the database, remove it if satisfied; if it contains a
  -- literal whose negation is assigned, delete that literal.
  n <- numVars `liftM` gets cnf
  s <- get
  liftST . forM_ [V 1 .. V n] $ \i -> when (mFr!i /= 0) $ do
    let l = L (mFr!i)
        filterL _i = map (\(p, c, cid) -> (p, filter (/= negate l) c, cid))
    -- Remove unsat literal `negate l' from clauses.
--     modifyArray (watches s) l filterL
    modifyArray (learnt s) l filterL
    -- Clauses containing `l' are Sat.
--     writeArray (watches s) (negate l) []
    writeArray (learnt s) (negate l) []

-- * Internals

-- | The DPLL procedure is modeled as a state transition system.  This
-- function takes one step in that transition system.  Given an unsatisfactory
-- assignment, perform one state transition, producing a new assignment and a
-- new state.
solveStep :: MAssignment s -> DPLLMonad s (Either (MAssignment s) Solution)
solveStep m = do
    unsafeFreezeAss m >>= solveStepInvariants
    conf <- gets dpllConfig
    let selector = if configUseVSIDS conf then select else selectStatic
    maybeConfl <- bcp m
    mFr   <- unsafeFreezeAss m
    voArr <- gets (varOrderArr . varOrder)
    voFr  <- FrozenVarOrder `liftM` liftST (unsafeFreeze voArr)
    s     <- get
    stepForward $ 
          -- Check if unsat.
          unsat maybeConfl s ==> postProcessUnsat maybeConfl
          -- Unit propagation may reveal conflicts; check.
       >< maybeConfl         >=> backJump m
          -- No conflicts.  Decide.
       >< selector mFr voFr  >=> decide m
    where
      -- Take the step chosen by the transition guards above.
      stepForward Nothing     = (Right . Sat) `liftM` unsafeFreezeAss m
      stepForward (Just step) = do
          r <- step
          case r of
            Nothing -> (Right . Unsat) `liftM` liftST (unsafeFreezeAss m)
            Just m  -> return . Left $ m

-- | /Precondition:/ problem determined to be unsat.
--
-- Records id of conflicting clause in trace before failing.  Always returns
-- `Nothing'.
postProcessUnsat :: Maybe (Lit, Clause, ClauseId) -> DPLLMonad s (Maybe a)
postProcessUnsat maybeConfl = do
    traceClauseId $ (thd . fromJust) maybeConfl
    return Nothing
  where
    thd (_,_,i) = i

-- | Check data structure invariants.  Unless @-fno-ignore-asserts@ is passed,
-- this should be optimised away to nothing.
solveStepInvariants :: IAssignment -> DPLLMonad s ()
{-# INLINE solveStepInvariants #-}
solveStepInvariants _m = assert True $ do
    s <- get
    -- no dups in decision list or trail
    assert ((length . dl) s == (length . nub . dl) s) $
     assert ((length . trail) s == (length . nub . trail) s) $
     return ()

             
-- | The solution to a SAT problem.  In each case we return an assignment,
-- which is obviously right in the `Sat' case; in the `Unsat' case, the reason
-- is to assist in the generation of an unsatisfiable core.
data Solution = Sat IAssignment | Unsat IAssignment deriving (Eq)

instance Show Solution where
   show (Sat a)     = "satisfiable: " ++ showAssignment a
   show (Unsat _)   = "unsatisfiable"

finalAssignment :: Solution -> IAssignment
finalAssignment (Sat a)   = a
finalAssignment (Unsat a) = a

-- ** Internals

-- | Value of the `level' array if corresponding variable unassigned.  Had
-- better be less that 0.
noLevel :: Level
noLevel = -1

-- ** State and Phases

data FunsatState s = SC
    { cnf :: CNF                -- ^ The problem.
    , dl :: [Lit]
      -- ^ The decision level (last decided literal on front).

    , watches :: WatchArray s
      -- ^ Invariant: if @l@ maps to @((x, y), c)@, then @x == l || y == l@.

    , learnt :: WatchArray s
      -- ^ Same invariant as `watches', but only contains learned conflict
      -- clauses.

    , propQ :: Seq Lit
      -- ^ A FIFO queue of literals to propagate.  This should not be
      -- manipulated directly; see `enqueue' and `dequeue'.

    , level :: LevelArray s

    , trail :: [Lit]
      -- ^ Chronological trail of assignments, last-assignment-at-head.

    , reason :: ReasonMap
      -- ^ For each variable, the clause that (was unit and) implied its value.

    , numConfl :: !Int64
      -- ^ The number of conflicts that have occurred since the last restart.

    , numConflTotal :: !Int64
      -- ^ The total number of conflicts.

    , numDecisions :: !Int64
      -- ^ The total number of decisions.

    , numImpl :: !Int64
      -- ^ The total number of implications (propagations).

    , varOrder :: VarOrder s

    , resolutionTrace :: PartialResolutionTrace

    , dpllConfig :: DPLLConfig } deriving Show

-- | Our star monad, the DPLL State monad.  We use @ST@ for mutable arrays and
-- references, when necessary.  Most of the state, however, is kept in
-- `FunsatState' and is not mutable.
type DPLLMonad s = SSTErrMonad (Lit, Clause, ClauseId) (FunsatState s) s


-- *** Boolean constraint propagation

-- | Assign a new literal, and enqueue any implied assignments.  If a conflict
-- is detected, return @Just (impliedLit, conflictingClause)@; otherwise
-- return @Nothing@.  The @impliedLit@ is implied by the clause, but conflicts
-- with the assignment.
--
-- If no new clauses are unit (i.e. no implied assignments), simply update
-- watched literals.
bcpLit :: MAssignment s
          -> Lit                -- ^ Assigned literal which might propagate.
          -> DPLLMonad s (Maybe (Lit, Clause, ClauseId))
bcpLit m l = do
    ws <- gets watches ; ls <- gets learnt
    clauses <- liftST $ readArray ws l
    learnts <- liftST $ readArray ls l
    liftST $ do writeArray ws l [] ; writeArray ls l []

    -- Update wather lists for normal & learnt clauses; if conflict is found,
    -- return that and don't update anything else.
    (`catchError` return . Just) $ do
      {-# SCC "bcpWatches" #-} forM_ (tails clauses) (updateWatches
        (\ f l -> liftST $ modifyArray ws l (const f)))
      {-# SCC "bcpLearnts" #-} forM_ (tails learnts) (updateWatches
        (\ f l -> liftST $ modifyArray ls l (const f)))
      return Nothing            -- no conflict
  where
    -- updateWatches: `l' has been assigned, so we look at the clauses in
    -- which contain @negate l@, namely the watcher list for l.  For each
    -- annotated clause, find the status of its watched literals.  If a
    -- conflict is found, the at-fault clause is returned through Left, and
    -- the unprocessed clauses are placed back into the appropriate watcher
    -- list.
    {-# INLINE updateWatches #-}
    updateWatches _ [] = return ()
    updateWatches alter (annCl@(watchRef, c, cid) : restClauses) = do
      mFr <- unsafeFreezeAss m
      q   <- liftST $ do (x, y) <- readSTRef watchRef
                         return $ if x == l then y else x
      -- l,q are the (negated) literals being watched for clause c.
      if negate q `isTrueUnder` mFr -- if other true, clause already sat
       then alter (annCl:) l
       else
         case find (\x -> x /= negate q && x /= negate l
                          && not (x `isFalseUnder` mFr)) c of
           Just l' -> do     -- found unassigned literal, negate l', to watch
             liftST $ writeSTRef watchRef (q, negate l')
             alter (annCl:) (negate l')

           Nothing -> do      -- all other lits false, clause is unit
             modify $ \s -> s{ numImpl = numImpl s + 1 }
             alter (annCl:) l
             isConsistent <- enqueue m (negate q) (Just (c, cid))
             when (not isConsistent) $ do -- unit literal is conflicting
                alter (restClauses ++) l
                clearQueue
                throwError (negate q, c, cid)

-- | Boolean constraint propagation of all literals in `propQ'.  If a conflict
-- is found it is returned exactly as described for `bcpLit'.
bcp :: MAssignment s -> DPLLMonad s (Maybe (Lit, Clause, ClauseId))
bcp m = do
  q <- gets propQ
  if Seq.null q then return Nothing
   else do
     p <- dequeue
     bcpLit m p >>= maybe (bcp m) (return . Just)



-- *** Decisions

-- | Find and return a decision variable.  A /decision variable/ must be (1)
-- undefined under the assignment and (2) it or its negation occur in the
-- formula.
--
-- Select a decision variable, if possible, and return it and the adjusted
-- `VarOrder'.
select :: IAssignment -> FrozenVarOrder -> Maybe Var
{-# INLINE select #-}
select = varOrderGet

selectStatic :: IAssignment -> a -> Maybe Var
{-# INLINE selectStatic #-}
selectStatic m _ = find (`isUndefUnder` m) (range . bounds $ m)

-- | Assign given decision variable.  Records the current assignment before
-- deciding on the decision variable indexing the assignment.
decide :: MAssignment s -> Var -> DPLLMonad s (Maybe (MAssignment s))
decide m v = do
  let ld = L (unVar v)
  (SC{dl=dl}) <- get
--   trace ("decide " ++ show ld) $ return ()
  modify $ \s -> s{ dl = ld:dl
                  , numDecisions = numDecisions s + 1 }
  enqueue m ld Nothing
  return $ Just m



-- *** Backtracking

-- | Non-chronological backtracking.  The current returns the learned clause
-- implied by the first unique implication point cut of the conflict graph.
backJump :: MAssignment s
         -> (Lit, Clause, ClauseId)
            -- ^ @(l, c)@, where attempting to assign @l@ conflicted with
            -- clause @c@.
         -> DPLLMonad s (Maybe (MAssignment s))
backJump m c@(_, _conflict, _) = get >>= \(SC{dl=dl, reason=_reason}) -> do
    _theTrail <- gets trail
--     trace ("********** conflict = " ++ show c) $ return ()
--     trace ("trail = " ++ show _theTrail) $ return ()
--     trace ("dlits (" ++ show (length dl) ++ ") = " ++ show dl) $ return ()
--          ++ "reason: " ++ Map.showTree _reason
--           ) (
    modify $ \s -> s{ numConfl = numConfl s + 1
                    , numConflTotal = numConflTotal s + 1 }
    levelArr :: FrozenLevelArray <- do s <- get
                                       liftST $ unsafeFreeze (level s)
    (learntCl, learntClId, newLevel) <-
        do mFr <- unsafeFreezeAss m
           analyse mFr levelArr dl c
    s <- get
    let numDecisionsToUndo = length dl - newLevel
        dl' = drop numDecisionsToUndo dl
        undoneLits = takeWhile (\lit -> levelArr ! (var lit) > newLevel) (trail s) 
    forM_ undoneLits $ const (undoOne m) -- backtrack
    mFr <- unsafeFreezeAss m
    assert (numDecisionsToUndo > 0) $
     assert (not (null learntCl)) $
     assert (learntCl `isUnitUnder` mFr) $
     modify $ \s -> s{ dl  = dl' } -- undo decisions
    mFr <- unsafeFreezeAss m
--     trace ("new mFr: " ++ showAssignment mFr) $ return ()
    -- TODO once I'm sure this works I don't need getUnit, I can just use the
    -- uip of the cut.
    watchClause m (learntCl, learntClId) True
    enqueue m (getUnit learntCl mFr) (Just (learntCl, learntClId))
      -- learntCl is asserting
    return $ Just m



-- | @doWhile cmd test@ first runs @cmd@, then loops testing @test@ and
-- executing @cmd@.  The traditional @do-while@ semantics, in other words.
doWhile :: (Monad m) => m () -> m Bool -> m ()
doWhile body test = do
  body
  shouldContinue <- test
  when shouldContinue $ doWhile body test

-- | Analyse a the conflict graph and produce a learned clause.  We use the
-- First UIP cut of the conflict graph.
--
-- May undo part of the trail, but not past the current decision level.
analyse :: IAssignment -> FrozenLevelArray -> [Lit] -> (Lit, Clause, ClauseId)
        -> DPLLMonad s (Clause, ClauseId, Int)
           -- ^ learned clause and new decision level
analyse mFr levelArr dlits (cLit, cClause, cCid) = do
    st <- get
--     trace ("mFr: " ++ showAssignment mFr) $ assert True (return ())
--     let (learntCl, newLevel) = cutLearn mFr levelArr firstUIPCut
--         firstUIPCut = uipCut dlits levelArr conflGraph (unLit cLit)
--                       (firstUIP conflGraph)
--         conflGraph = mkConflGraph mFr levelArr (reason st) dlits c
--                      :: Gr CGNodeAnnot ()
--     trace ("graphviz graph:\n" ++ graphviz' conflGraph) $ return ()
--     trace ("cut: " ++ show firstUIPCut) $ return ()
--     trace ("topSort: " ++ show topSortNodes) $ return ()
--     trace ("dlits (" ++ show (length dlits) ++ "): " ++ show dlits) $ return ()
--     trace ("learnt: " ++ show (map (\l -> (l, levelArr!(var l))) learntCl, newLevel)) $ return ()
--     outputConflict "conflict.dot" (graphviz' conflGraph) $ return ()
--     return $ (learntCl, newLevel)
    m <- liftST $ unsafeThawAss mFr
    a <- firstUIPBFS m (numVars . cnf $ st) (reason st)
--     trace ("firstUIPBFS learned: " ++ show a) $ return ()
    return a
  where
    -- BFS by undoing the trail backward.  From Minisat paper.  Returns
    -- conflict clause and backtrack level.
    firstUIPBFS :: MAssignment s -> Int -> ReasonMap
                -> DPLLMonad s (Clause, ClauseId, Int)
    firstUIPBFS m nVars reasonMap =  do
      resolveSourcesR <- liftST $ newSTRef [] -- trace sources
      let addResolveSource clauseId =
              liftST $ modifySTRef resolveSourcesR (clauseId:)
      -- Literals we should process.
      seenArr  <- liftST $ newSTUArray (V 1, V nVars) False
      counterR <- liftST $ newSTRef 0 -- Number of unprocessed current-level
                                      -- lits we know about.
      pR <- liftST $ newSTRef cLit -- Invariant: literal from current dec. lev.
      out_learnedR <- liftST $ newSTRef []
      out_btlevelR <- liftST $ newSTRef 0
      let reasonL l = if l == cLit then (cClause, cCid)
                      else
                        let (r, rid) =
                                Map.findWithDefault (error "analyse: reasonL")
                                (var l) reasonMap
                        in (r `without` l, rid)


      (`doWhile` (liftM (> 0) (liftST $ readSTRef counterR))) $
        do p <- liftST $ readSTRef pR
           let (p_reason, p_rid) = reasonL p
           traceClauseId p_rid
           addResolveSource p_rid
           forM_ p_reason (bump . var)
           -- For each unseen reason,
           -- > from the current level, bump counter
           -- > from lower level, put in learned clause
           liftST . forM_ p_reason $ \q -> do
             seenq <- readArray seenArr (var q)
             when (not seenq) $
               do writeArray seenArr (var q) True
                  if levelL q == currentLevel
                   then modifySTRef counterR (+ 1)
                   else if levelL q > 0
                   then do modifySTRef out_learnedR (q:)
                           modifySTRef out_btlevelR $ max (levelL q)
                   else return ()
           -- Select next literal to look at:
           (`doWhile` (liftST (readSTRef pR >>= readArray seenArr . var)
                       >>= return . not)) $ do
             p <- head `liftM` gets trail -- a dec. var. only if the counter =
                                          -- 1, i.e., loop terminates now
             liftST $ writeSTRef pR p
             undoOne m
           -- Invariant states p is from current level, so when we're done
           -- with it, we've thrown away one lit. from counting toward
           -- counter.
           liftST $ modifySTRef counterR (\c -> c - 1)
      p <- liftST $ readSTRef pR
      liftST $ modifySTRef out_learnedR (negate p:)
      bump . var $ p
      out_learned <- liftST $ readSTRef out_learnedR
      out_btlevel <- liftST $ readSTRef out_btlevelR
      learnedClauseId <- nextTraceId
      storeResolvedSources resolveSourcesR learnedClauseId
      traceClauseId learnedClauseId
      return (out_learned, learnedClauseId, out_btlevel)

    -- helpers
    currentLevel = length dlits
    levelL l = levelArr!(var l)
    storeResolvedSources rsR clauseId = do
      rsReversed <- liftST $ readSTRef rsR
      modifySlot resolutionTrace $ \s rt ->
        s{resolutionTrace =
              rt{resSourceMap =
                     Map.insert clauseId (reverse rsReversed) (resSourceMap rt)}}


-- | Delete the assignment to last-assigned literal.  Undoes the trail, the
-- assignment, sets `noLevel', undoes reason.
--
-- Does /not/ touch `dl'.
undoOne :: MAssignment s -> DPLLMonad s ()
{-# INLINE undoOne #-}
undoOne m = do
    trl <- gets trail
    lvl <- gets level
    case trl of
      []       -> error "undoOne of empty trail"
      (l:trl') -> do
          liftST $ m `unassign` l
          liftST $ writeArray lvl (var l) noLevel
          modify $ \s ->
            s{ trail    = trl'
             , reason   = Map.delete (var l) (reason s) }

-- | Increase the recorded activity of given variable.
bump :: Var -> DPLLMonad s ()
{-# INLINE bump #-}
bump v = varOrderMod v (+ varInc)

-- | Constant amount by which a variable is `bump'ed.
varInc :: Double
varInc = 1.0
  


-- *** Impossible to satisfy

-- | /O(1)/.  Test for unsatisfiability.
--
-- The DPLL paper says, ''A problem is unsatisfiable if there is a conflicting
-- clause and there are no decision literals in @m@.''  But we were deciding
-- on all literals *without* creating a conflicting clause.  So now we also
-- test whether we've made all possible decisions, too.
unsat :: Maybe a -> FunsatState s -> Bool
{-# INLINE unsat #-}
unsat maybeConflict (SC{dl=dl}) = isUnsat
    where isUnsat = (null dl && isJust maybeConflict)
                    -- or BitSet.size bad == numVars cnf



-- ** Helpers

-- *** Clause compaction

-- | Keep the smaller half of the learned clauses.
compactDB :: DPLLMonad s ()
compactDB = do
    n <- numVars `liftM` gets cnf
    lArr <- gets learnt
    clauses <- liftST $ (nub . Fl.concat) `liftM`
                        forM [L (- n) .. L n]
                           (\v -> do val <- readArray lArr v ; writeArray lArr v []
                                     return val)
    let clauses' = take (length clauses `div` 2)
                   $ sortBy (comparing (length . (\(_,s,_) -> s))) clauses
    liftST $ forM_ clauses'
             (\ wCl@(r, _, _) -> do
                (x, y) <- readSTRef r
                modifyArray lArr x $ const (wCl:)
                modifyArray lArr y $ const (wCl:))

-- *** Unit propagation

-- | Add clause to the watcher lists, unless clause is a singleton; if clause
-- is a singleton, `enqueue's fact and returns `False' if fact is in conflict,
-- `True' otherwise.  This function should be called exactly once per clause,
-- per run.  It should not be called to reconstruct the watcher list when
-- propagating.
--
-- Currently the watched literals in each clause are the first two.
--
-- Also adds unique clause ids to trace.
watchClause :: MAssignment s
            -> (Clause, ClauseId)
            -> Bool             -- ^ Is this clause learned?
            -> DPLLMonad s Bool
{-# INLINE watchClause #-}
watchClause m (c, cid) isLearnt = do
    case c of
      [] -> return True
      [l] -> do result <- enqueue m l (Just (c, cid))
                levelArr <- gets level
                liftST $ writeArray levelArr (var l) 0
                when (not isLearnt) (
                  modifySlot resolutionTrace $ \s rt ->
                      s{resolutionTrace=rt{resTraceOriginalSingles=
                                               (c,cid):resTraceOriginalSingles rt}})
                return result
      _ -> do let p = (negate (c !! 0), negate (c !! 1))
                  _insert annCl@(_, cl) list -- avoid watching dup clauses
                      | any (\(_, c) -> cl == c) list = list
                      | otherwise                     = annCl:list
              r <- liftST $ newSTRef p
              let annCl = (r, c, cid)
                  addCl arr = do modifyArray arr (fst p) $ const (annCl:)
                                 modifyArray arr (snd p) $ const (annCl:)
              get >>= liftST . addCl . (if isLearnt then learnt else watches)
              return True

-- | Enqueue literal in the `propQ' and place it in the current assignment.
-- If this conflicts with an existing assignment, returns @False@; otherwise
-- returns @True@.  In case there is a conflict, the assignment is /not/
-- altered.
--
-- Also records decision level, modifies trail, and records reason for
-- assignment.
enqueue :: MAssignment s
        -> Lit
           -- ^ The literal that has been assigned true.
        -> Maybe (Clause, ClauseId)
           -- ^ The reason for enqueuing the literal.  Including a
           -- non-@Nothing@ value here adjusts the `reason' map.
        -> DPLLMonad s Bool
{-# INLINE enqueue #-}
-- enqueue _m l _r | trace ("enqueue " ++ show l) $ False = undefined
enqueue m l r = do
    mFr <- unsafeFreezeAss m
    case l `statusUnder` mFr of
      Right b -> return b         -- conflict/already assigned
      Left () -> do
        liftST $ m `assign` l
        -- assign decision level for literal
        gets (level &&& (length . dl)) >>= \(levelArr, dlInt) ->
          liftST (writeArray levelArr (var l) dlInt)
        modify $ \s -> s{ trail = l : (trail s)
                        , propQ = propQ s Seq.|> l } 
        when (isJust r) $
          modifySlot reason $ \s m -> s{reason = Map.insert (var l) (fromJust r) m}
        return True

-- | Pop the `propQ'.  Error (crash) if it is empty.
dequeue :: DPLLMonad s Lit
{-# INLINE dequeue #-}
dequeue = do
    q <- gets propQ
    case Seq.viewl q of
      Seq.EmptyL -> error "dequeue of empty propQ"
      top Seq.:< q' -> do
        modify $ \s -> s{propQ = q'}
        return top

-- | Clear the `propQ'.
clearQueue :: DPLLMonad s ()
{-# INLINE clearQueue #-}
clearQueue = modify $ \s -> s{propQ = Seq.empty}

-- *** Dynamic variable ordering

-- | Modify priority of variable; takes care of @Double@ overflow.
varOrderMod :: Var -> (Double -> Double) -> DPLLMonad s ()
varOrderMod v f = do
    vo <- varOrderArr `liftM` gets varOrder
    vActivity <- liftST $ readArray vo v
    when (f vActivity > 1e100) $ rescaleActivities vo
    liftST $ writeArray vo v (f vActivity)
  where
    rescaleActivities vo = liftST $ do
        indices <- range `liftM` getBounds vo
        forM_ indices (\i -> modifyArray vo i $ const (* 1e-100))


-- | Retrieve the maximum-priority variable from the variable order.
varOrderGet :: IAssignment -> FrozenVarOrder -> Maybe Var
{-# INLINE varOrderGet #-}
varOrderGet mFr (FrozenVarOrder voFr) =
    -- find highest var undef under mFr, then find one with highest activity
    (`fmap` goUndef highestIndex) $ \start -> goActivity start start
  where
    highestIndex = snd . bounds $ voFr
    maxActivity v v' = if voFr!v > voFr!v' then v else v'

    -- @goActivity current highest@ returns highest-activity var
    goActivity !(V 0) !h   = h
    goActivity !v@(V n) !h = if v `isUndefUnder` mFr
                             then goActivity (V $! n-1) (v `maxActivity` h)
                             else goActivity (V $! n-1) h

    -- returns highest var that is undef under mFr
    goUndef !(V 0) = Nothing
    goUndef !v@(V n) | v `isUndefUnder` mFr = Just v
                     | otherwise            = goUndef (V $! n-1)


-- | Generate a new clause identifier (always unique).
nextTraceId :: DPLLMonad s Int
nextTraceId = do
    counter <- gets (resTraceIdCount . resolutionTrace)
    modifySlot resolutionTrace $ \s rt ->
        s{ resolutionTrace = rt{ resTraceIdCount = succ counter }}
    return $! counter

-- | Add the given clause id to the trace.
traceClauseId :: ClauseId -> DPLLMonad s ()
traceClauseId cid = do
    modifySlot resolutionTrace $ \s rt ->
        s{resolutionTrace = rt{ resTrace = [cid] }}


-- *** Generic state transition notation

-- | Guard a transition action.  If the boolean is true, return the action
-- given as an argument.  Otherwise, return `Nothing'.
(==>) :: (Monad m) => Bool -> m a -> Maybe (m a)
{-# INLINE (==>) #-}
(==>) b amb = guard b >> return amb

infixr 6 ==>

-- | @flip fmap@.
(>=>) :: (Monad m) => Maybe a -> (a -> m b) -> Maybe (m b)
{-# INLINE (>=>) #-}
(>=>) = flip fmap

infixr 6 >=>


-- | Choice of state transitions.  Choose the leftmost action that isn't
-- @Nothing@, or return @Nothing@ otherwise.
(><) :: (Monad m) => Maybe (m a) -> Maybe (m a) -> Maybe (m a)
a1 >< a2 =
    case (a1, a2) of
      (Nothing, Nothing) -> Nothing
      (Just _, _)        -> a1
      _                  -> a2

infixl 5 ><

-- *** Misc
showAssignment a = intercalate " " ([show (a!i) | i <- range . bounds $ a,
                                                  (a!i) /= 0])

initialActivity :: Double
initialActivity = 1.0

instance Error (Lit, Clause, ClauseId) where noMsg = (L 0, [], 0)
instance Error () where noMsg = ()


data VerifyError =
    SatError [(Clause, Either () Bool)]
      -- ^ Indicates a unsatisfactory assignment that was claimed
      -- satisfactory.  Each clause is tagged with its status using
      -- 'Funsat.Types.Model'@.statusUnder@.

    | UnsatError ResolutionError 
      -- ^ Indicates an error in the resultion checking process.

                   deriving (Show)

-- | Verify the solution.  In case of `Sat', checks that the assignment is
-- well-formed and satisfies the CNF problem.  In case of `Unsat', runs a
-- resolution-based checker on a trace of the SAT solver.
verify :: Solution -> Maybe ResolutionTrace -> CNF -> Maybe VerifyError
verify sol maybeRT cnf =
   -- m is well-formed
--    Fl.all (\l -> m!(V l) == l || m!(V l) == negate l || m!(V l) == 0) [1..numVars cnf]
    case sol of
      Sat m ->
          let unsatClauses = toList $
                             Set.filter (not . isTrue . snd) $
                             Set.map (\c -> (c, c `statusUnder` m)) (clauses cnf)
          in if null unsatClauses
             then Nothing
             else Just . SatError $ unsatClauses
      Unsat _ ->
          case Resolution.checkDepthFirst (fromJust maybeRT) of
            Left er -> Just . UnsatError $ er
            Right _ -> Nothing
  where isTrue (Right True) = True
        isTrue _            = False

---------------------------------------
-- Statistics & trace


data Stats = Stats
    { statsNumConfl :: Int64
      -- ^ Number of conflicts since last restart.

    , statsNumConflTotal :: Int64
      -- ^ Number of conflicts since beginning of solving.

    , statsNumLearnt :: Int64
      -- ^ Number of learned clauses currently in DB (fluctuates because DB is
      -- compacted every restart).

    , statsAvgLearntLen :: Double
      -- ^ Avg. number of literals per learnt clause.

    , statsNumDecisions :: Int64
      -- ^ Total number of decisions since beginning of solving.

    , statsNumImpl :: Int64
      -- ^ Total number of unit implications since beginning of solving.
    }

-- |  The show instance uses the wrapped string.
newtype ShowWrapped = WrapString { unwrapString :: String }
instance Show ShowWrapped where show = unwrapString

instance Show Stats where show = show . statTable

-- | Convert statistics to a nice-to-display tabular form.
statTable :: Stats -> Tabular.Table ShowWrapped
statTable s =
    Tabular.mkTable
                   [ [WrapString "Num. Conflicts"
                     ,WrapString $ show (statsNumConflTotal s)]
                   , [WrapString "Num. Learned Clauses"
                     ,WrapString $ show (statsNumLearnt s)]
                   , [WrapString " --> Avg. Lits/Clause"
                     ,WrapString $ show (statsAvgLearntLen s)]
                   , [WrapString "Num. Decisions"
                     ,WrapString $ show (statsNumDecisions s)]
                   , [WrapString "Num. Propagations"
                     ,WrapString $ show (statsNumImpl s)] ]

-- | Converts statistics into a tabular, human-readable summary.
statSummary :: Stats -> String
statSummary s =
     show (Tabular.mkTable
           [[WrapString $ show (statsNumConflTotal s) ++ " Conflicts"
            ,WrapString $ "| " ++ show (statsNumLearnt s) ++ " Learned Clauses"
                      ++ " (avg " ++ printf "%.2f" (statsAvgLearntLen s)
                      ++ " lits/clause)"]])


extractStats :: DPLLMonad s Stats
extractStats = do
  s <- get
  learntArr <- liftST $ unsafeFreezeWatchArray (learnt s)
  let learnts = (nub . Fl.concat)
        [ map (sort . (\(_,c,_) -> c)) (learntArr!i)
        | i <- (range . bounds) learntArr ] :: [Clause]
      stats =
        Stats { statsNumConfl = numConfl s
              , statsNumConflTotal = numConflTotal s
              , statsNumLearnt = fromIntegral $ length learnts
              , statsAvgLearntLen =
                fromIntegral (foldl' (+) 0 (map length learnts))
                / fromIntegral (statsNumLearnt stats)
              , statsNumDecisions = numDecisions s
              , statsNumImpl = numImpl s }
  return stats

unsafeFreezeWatchArray :: WatchArray s -> ST s (Array Lit [WatchedPair s])
unsafeFreezeWatchArray = freeze


constructResTrace :: Solution -> DPLLMonad s ResolutionTrace
constructResTrace sol = do
    s <- get
    watchesIndices <- range `liftM` liftST (getBounds (watches s))
    origClauseMap <-
        foldM (\origMap i -> do
                 clauses <- liftST $ readArray (watches s) i
                 return $
                   foldr (\(_, clause, clauseId) origMap ->
                           Map.insert clauseId clause origMap)
                         origMap
                         clauses)
              Map.empty
              watchesIndices
    let singleClauseMap =
            foldr (\(clause, clauseId) m -> Map.insert clauseId clause m)
                  Map.empty
                  (resTraceOriginalSingles . resolutionTrace $ s)
        anteMap =
            foldr (\l anteMap -> Map.insert (var l) (getAnteId s (var l)) anteMap)
                  Map.empty
                  (litAssignment . finalAssignment $ sol)
    return
      (initResolutionTrace
       (head (resTrace . resolutionTrace $ s))
       (finalAssignment sol))
      { traceSources = resSourceMap . resolutionTrace $ s
      , traceOriginalClauses = origClauseMap `Map.union` singleClauseMap
      , traceAntecedents = anteMap }
  where
    getAnteId s v = snd $
        Map.findWithDefault (error $ "no reason for assigned var " ++ show v)
        v (reason s)