{-# LANGUAGE CPP              #-}
{-# LANGUAGE LambdaCase       #-}
{-# LANGUAGE MagicHash        #-}
{-# LANGUAGE NoFieldSelectors #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE RecordWildCards  #-}
-- {-# OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-all #-}
module PureSAT.Main (
    Solver,
    newSolver,
    Lit (..),
    newLit,
    boostScore,
    neg,
    addClause,
    solve,
    simplify,
    modelValue,
    -- * Statistics
    num_vars,
    num_clauses,
    num_learnts,
    num_learnt_literals,
    num_conflicts,
    num_restarts,
) where

-- #define ENABLE_ASSERTS
-- #define ENABLE_TRACE

#define TWO_WATCHED_LITERALS

import Data.Functor ((<&>))
import Data.List    (nub)
import Data.STRef   (STRef, newSTRef, readSTRef, writeSTRef)

import Data.Primitive.PrimVar   (PrimVar, readPrimVar, writePrimVar, newPrimVar, modifyPrimVar)

import PureSAT.Base
import PureSAT.Boost
import PureSAT.Clause2
import PureSAT.LBool
import PureSAT.Prim
import PureSAT.Level
import PureSAT.LitSet
import PureSAT.LitTable
import PureSAT.LitVar
import PureSAT.PartialAssignment
import PureSAT.Satisfied
import PureSAT.Stats
import PureSAT.Trail
import PureSAT.VarSet
import PureSAT.Utils
import PureSAT.LCG
import PureSAT.SparseSet

#ifdef TWO_WATCHED_LITERALS
import PureSAT.Vec
#endif

#ifdef ENABLE_TRACE
#define TRACING(x) x
#else
#define TRACING(x)
#endif

#ifdef ENABLE_ASSERTS
#define ASSERTING(x) x
#define ASSERTING_BIND(x,y) x <- y
#else
#define ASSERTING(x)
#define ASSERTING_BIND(x,y)
#endif

-------------------------------------------------------------------------------
-- ClauseDB
-------------------------------------------------------------------------------

#ifdef TWO_WATCHED_LITERALS

newtype ClauseDB s = CDB (LitTable s (Vec s Watch))

data Watch = W !Lit !Clause2

newClauseDB :: Int -> ST s (ClauseDB s)
newClauseDB :: forall s. Int -> ST s (ClauseDB s)
newClauseDB !Int
size' = do
    let size :: Int
size = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
size' Int
40960
    arr <- Int -> Vec s Watch -> ST s (LitTable s (Vec s Watch))
forall a s. Int -> a -> ST s (LitTable s a)
newLitTable Int
size Vec s Watch
forall a. HasCallStack => a
undefined

    forM_ [0 .. size - 1] $ \Int
i -> do
        vec <- Int -> ST s (Vec s Watch)
forall s a. Int -> ST s (Vec s a)
newVec Int
16
        writeLitTable arr (MkLit i) vec

    return (CDB arr)

extendClauseDB :: ClauseDB s -> Int -> ST s (ClauseDB s)
extendClauseDB :: forall s. ClauseDB s -> Int -> ST s (ClauseDB s)
extendClauseDB cdb :: ClauseDB s
cdb@(CDB LitTable s (Vec s Watch)
old) Int
newSize' = do
    -- TODO: this code is terrible.
    oldSize <- LitTable s (Vec s Watch) -> ST s Int
forall s a. LitTable s a -> ST s Int
sizeofLitTable LitTable s (Vec s Watch)
old
    let newSize = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
newSize' Int
4096
    if newSize <= oldSize
    then return cdb
    else do
        traceM $ "resize" ++ show newSize
        new <- newLitTable newSize undefined

        forM_ [0 .. newSize - 1] $ \Int
i -> do
            if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
oldSize
            then do
                x <- LitTable s (Vec s Watch) -> Lit -> ST s (Vec s Watch)
forall s a. LitTable s a -> Lit -> ST s a
readLitTable LitTable s (Vec s Watch)
old (Int -> Lit
MkLit Int
i)
                writeLitTable new (MkLit i) x
            else do
                vec <- Int -> ST s (Vec s Watch)
forall s a. Int -> ST s (Vec s a)
newVec Int
16
                writeLitTable new (MkLit i) vec

        return (CDB new)

insertClauseDB :: Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
insertClauseDB :: forall s. Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
insertClauseDB !Lit
l1 !Lit
l2 !Clause2
clause !ClauseDB s
cdb = do
    ASSERTING(assertST "l1" (litInClause l1 clause))
    ASSERTING(assertST "l2" (litInClause l2 clause))
    Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l1 (Lit -> Clause2 -> Watch
W Lit
l2 Clause2
clause) ClauseDB s
cdb
    Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l2 (Lit -> Clause2 -> Watch
W Lit
l1 Clause2
clause) ClauseDB s
cdb

insertWatch :: Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch :: forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch !Lit
l !Watch
w (CDB LitTable s (Vec s Watch)
cdb) = do
    ws  <- LitTable s (Vec s Watch) -> Lit -> ST s (Vec s Watch)
forall s a. LitTable s a -> Lit -> ST s a
readLitTable LitTable s (Vec s Watch)
cdb Lit
l
    ws' <- insertVec ws w
    writeLitTable cdb l ws'

lookupClauseDB :: Lit -> ClauseDB s -> ST s (Vec s Watch)
lookupClauseDB :: forall s. Lit -> ClauseDB s -> ST s (Vec s Watch)
lookupClauseDB !Lit
l (CDB LitTable s (Vec s Watch)
arr) = do
    LitTable s (Vec s Watch) -> Lit -> ST s (Vec s Watch)
forall s a. LitTable s a -> Lit -> ST s a
readLitTable LitTable s (Vec s Watch)
arr Lit
l

clearClauseDB :: ClauseDB s -> Lit -> ST s ()
clearClauseDB :: forall s. ClauseDB s -> Lit -> ST s ()
clearClauseDB (CDB LitTable s (Vec s Watch)
cdb) Lit
l = do
    v <- Int -> ST s (Vec s Watch)
forall s a. Int -> ST s (Vec s a)
newVec Int
0
    writeLitTable cdb l v

#else

type ClauseDB s = [Clause2]

-- TODO: this is used in learning code.
insertClauseDB :: Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
insertClauseDB _ _ _ _ = return ()

#endif

-------------------------------------------------------------------------------
-- Clause
-------------------------------------------------------------------------------

type Clause = [Lit]

data Satisfied
    = Satisfied
    | Conflicting
    | Unit !Lit
    | Unresolved !Clause2
  deriving Int -> Satisfied -> String -> String
[Satisfied] -> String -> String
Satisfied -> String
(Int -> Satisfied -> String -> String)
-> (Satisfied -> String)
-> ([Satisfied] -> String -> String)
-> Show Satisfied
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Satisfied -> String -> String
showsPrec :: Int -> Satisfied -> String -> String
$cshow :: Satisfied -> String
show :: Satisfied -> String
$cshowList :: [Satisfied] -> String -> String
showList :: [Satisfied] -> String -> String
Show

satisfied :: PartialAssignment s -> Clause -> ST s Satisfied
satisfied :: forall s. PartialAssignment s -> Clause -> ST s Satisfied
satisfied !PartialAssignment s
pa = Clause -> ST s Satisfied
go0 (Clause -> ST s Satisfied)
-> (Clause -> Clause) -> Clause -> ST s Satisfied
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Clause
forall a. Eq a => [a] -> [a]
nub where
    go0 :: Clause -> ST s Satisfied
go0 []     = Satisfied -> ST s Satisfied
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Satisfied
Conflicting
    go0 (Lit
l:Clause
ls) = Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l PartialAssignment s
pa ST s LBool -> (LBool -> ST s Satisfied) -> ST s Satisfied
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        LBool
LUndef -> Lit -> Clause -> ST s Satisfied
go1 Lit
l Clause
ls
        LBool
LTrue  -> Satisfied -> ST s Satisfied
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Satisfied
Satisfied
        LBool
LFalse -> Clause -> ST s Satisfied
go0 Clause
ls

    go1 :: Lit -> Clause -> ST s Satisfied
go1 !Lit
l1 []     = Satisfied -> ST s Satisfied
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit -> Satisfied
Unit Lit
l1)
    go1 !Lit
l1 (Lit
l:Clause
ls) = Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l PartialAssignment s
pa ST s LBool -> (LBool -> ST s Satisfied) -> ST s Satisfied
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        LBool
LUndef -> Lit -> Lit -> Clause -> Clause -> ST s Satisfied
go2 Lit
l1 Lit
l [] Clause
ls
        LBool
LTrue  -> Satisfied -> ST s Satisfied
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Satisfied
Satisfied
        LBool
LFalse -> Lit -> Clause -> ST s Satisfied
go1 Lit
l1 Clause
ls

    go2 :: Lit -> Lit -> Clause -> Clause -> ST s Satisfied
go2 !Lit
l1 !Lit
l2 Clause
acc []     = Satisfied -> ST s Satisfied
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause2 -> Satisfied
Unresolved (Bool -> Lit -> Lit -> PrimArray Lit -> Clause2
MkClause2 Bool
False Lit
l1 Lit
l2 (Clause -> PrimArray Lit
forall a. Prim a => [a] -> PrimArray a
primArrayFromList Clause
acc)))
    go2 !Lit
l1 !Lit
l2 Clause
acc (Lit
l:Clause
ls) = Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l PartialAssignment s
pa ST s LBool -> (LBool -> ST s Satisfied) -> ST s Satisfied
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        LBool
LUndef -> Lit -> Lit -> Clause -> Clause -> ST s Satisfied
go2 Lit
l1 Lit
l2 (Lit
l Lit -> Clause -> Clause
forall a. a -> [a] -> [a]
: Clause
acc) Clause
ls
        LBool
LTrue  -> Satisfied -> ST s Satisfied
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Satisfied
Satisfied
        LBool
LFalse -> Lit -> Lit -> Clause -> Clause -> ST s Satisfied
go2 Lit
l1 Lit
l2 Clause
acc Clause
ls

-------------------------------------------------------------------------------
-- Clause2
-------------------------------------------------------------------------------

#ifdef ENABLE_ASSERTS
assertClauseConflicting :: PartialAssignment s -> Clause2 -> ST s ()
assertClauseConflicting pa c =
    satisfied2_ pa c $ \case
        Conflicting_ -> return ()
        ot           -> assertST (show ot) False

assertClauseUnit :: PartialAssignment s -> Clause2 -> ST s ()
assertClauseUnit pa c =
    satisfied2_ pa c $ \case
        Unit_ {} -> return ()
        ot       -> assertST (show ot) False

assertClauseSatisfied :: PartialAssignment s -> Clause2 -> ST s ()
assertClauseSatisfied pa c =
    satisfied2_ pa c $ \case
        Satisfied_ {} -> return ()
        ot            -> assertST (show ot) False
#endif

-------------------------------------------------------------------------------
-- Solver
-------------------------------------------------------------------------------

-- | Solver
data Solver s = Solver
    { forall s. Solver s -> STRef s Bool
ok         :: !(STRef s Bool)
    , forall s. Solver s -> STRef s Int
nextLit    :: !(STRef s Int) -- TODO: change to PrimVar
    , forall s. Solver s -> STRef s (Levels s)
zeroLevels :: !(STRef s (Levels s))
    , forall s. Solver s -> PrimVar s Int
zeroHead   :: !(PrimVar s Int)
    , forall s. Solver s -> STRef s (Trail s)
zeroTrail  :: !(STRef s (Trail s))
    , forall s. Solver s -> STRef s (PartialAssignment s)
zeroPA     :: !(STRef s (PartialAssignment s))
    , forall s. Solver s -> STRef s (VarSet s)
zeroVars   :: !(STRef s (VarSet s))
    , forall s. Solver s -> STRef s (PartialAssignment s)
prevPA     :: !(STRef s (PartialAssignment s))
    , forall s. Solver s -> STRef s (ClauseDB s)
clauses    :: !(STRef s (ClauseDB s))
    , forall s. Solver s -> LCG s
lcg        :: !(LCG s)
    , forall s. Solver s -> Stats s
statistics :: !(Stats s)
    }

-- | Create new solver
newSolver :: ST s (Solver s)
newSolver :: forall s. ST s (Solver s)
newSolver = do
    ok         <- Bool -> ST s (STRef s Bool)
forall a s. a -> ST s (STRef s a)
newSTRef Bool
True
    nextLit    <- newSTRef 0
    statistics <- newStats

    zeroLevels <- newLevels 1024 >>= newSTRef
    zeroVars   <- newVarSet >>= newSTRef
    zeroPA     <- newPartialAssignment 1024 >>= newSTRef
    zeroHead   <- newPrimVar 0
    zeroTrail  <- newTrail 1024 >>= newSTRef

    prevPA     <- newPartialAssignment 1024 >>= newSTRef

#ifdef TWO_WATCHED_LITERALS
    clauses    <- newClauseDB 0 >>= newSTRef
#else
    clauses    <- newSTRef []
#endif
    lcg        <- newLCG 44
    return Solver {..}

-- | Create fresh literal
newLit :: Solver s -> ST s Lit
newLit :: forall s. Solver s -> ST s Lit
newLit Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = do
    l' <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
nextLit
    let n = Int
l' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2
    writeSTRef nextLit n
    let l = Int -> Lit
MkLit Int
l'

    TRACING(traceM $ "!!! newLit " ++ show l)

    levels <- readSTRef zeroLevels
    levels' <- extendLevels levels n
    writeSTRef zeroLevels levels'

    pa <- readSTRef zeroPA
    pa' <- extendPartialAssignment pa
    writeSTRef zeroPA pa'

    trail <- readSTRef zeroTrail
    trail' <- extendTrail trail n
    writeSTRef zeroTrail trail'

    -- add unsolved variable.
    vars <- readSTRef zeroVars
    vars' <- extendVarSet n vars
    writeSTRef zeroVars vars'

#ifdef TWO_WATCHED_LITERALS
    clauseDB  <- readSTRef clauses
    clauseDB' <- extendClauseDB clauseDB n
    writeSTRef clauses clauseDB'
#endif

    insertVarSet (litToVar l) vars'

    return l

boostScore :: Solver s -> Lit -> ST s ()
boostScore :: forall s. Solver s -> Lit -> ST s ()
boostScore Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} Lit
l = do
    vars <- STRef s (VarSet s) -> ST s (VarSet s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (VarSet s)
zeroVars
    weightVarSet (litToVar l) boost vars

addClause :: Solver s -> [Lit] -> ST s Bool
addClause :: forall s. Solver s -> Clause -> ST s Bool
addClause solver :: Solver s
solver@Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} Clause
clause = STRef s Bool -> ST s Bool -> ST s Bool
forall s. STRef s Bool -> ST s Bool -> ST s Bool
whenOk STRef s Bool
ok (ST s Bool -> ST s Bool) -> ST s Bool -> ST s Bool
forall a b. (a -> b) -> a -> b
$ do
    pa <- STRef s (PartialAssignment s) -> ST s (PartialAssignment s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (PartialAssignment s)
zeroPA
    s <- satisfied pa clause
    case s of
        Satisfied
Satisfied    ->
            Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            
        Satisfied
Conflicting  -> do
            TRACING(traceM ">>> ADD CLAUSE conflict")
            Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
unsat Solver s
solver

        Unresolved !Clause2
c -> do
            Stats s -> ST s ()
forall s. Stats s -> ST s ()
incrStatsClauses Stats s
statistics

            clauseDB <- STRef s (ClauseDB s) -> ST s (ClauseDB s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (ClauseDB s)
clauses
#ifdef TWO_WATCHED_LITERALS
            let MkClause2 _ l1 l2 _ = c
            insertClauseDB l1 l2 c clauseDB
#else
            writeSTRef clauses (c : clauseDB)
#endif

            return True

        Unit Lit
l -> do
            TRACING(traceM $ "addClause unit: " ++ show l)

            clauseDB <- STRef s (ClauseDB s) -> ST s (ClauseDB s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (ClauseDB s)
clauses
            let qhead = PrimVar s Int
zeroHead

            levels <- readSTRef zeroLevels
            trail  <- readSTRef zeroTrail
            vars   <- readSTRef zeroVars

            -- insert new literal
            initialEnqueue trail pa levels vars l

            -- propagate
            res <- initialLoop clauseDB qhead trail levels pa vars

            if res
            then return True
            else unsat solver

unsat :: Solver s -> ST s Bool
unsat :: forall s. Solver s -> ST s Bool
unsat Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = do
    STRef s Bool -> Bool -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Bool
ok Bool
False
    -- TODO: cleanup clauses
    -- writeSTRef clauses []
    STRef s (VarSet s) -> ST s (VarSet s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (VarSet s)
zeroVars ST s (VarSet s) -> (VarSet s -> ST s ()) -> ST s ()
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VarSet s -> ST s ()
forall s. VarSet s -> ST s ()
clearVarSet
    Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-------------------------------------------------------------------------------
-- Solving
-------------------------------------------------------------------------------

data Self s = Self
    { forall s. Self s -> ClauseDB s
clauseDB :: !(ClauseDB s)
      -- ^ clause database

    -- TODO: add variable size

    , forall s. Self s -> PrimVar s Level
level    :: !(PrimVar s Level)
      -- ^ current decision level

    , forall s. Self s -> Levels s
levels   :: !(Levels s)
      -- ^ decision levels of literals

    , forall s. Self s -> PartialAssignment s
pa       :: !(PartialAssignment s)
      -- ^ current partial assignment

    , forall s. Self s -> PartialAssignment s
prev     :: !(PartialAssignment s)
      -- ^ previous partial assignment

    , forall s. Self s -> PartialAssignment s
zero     :: !(PartialAssignment s)
      -- ^ ground partial assignment

    , forall s. Self s -> PrimVar s Int
qhead    :: !(PrimVar s Int)
      -- ^ unit propsagation head

    , forall s. Self s -> VarSet s
vars     :: !(VarSet s)
      -- ^ undecided variables

    , forall s. Self s -> LitTable s Clause2
reasons  :: !(LitTable s Clause2)
      -- ^ reason clauses

    , forall s. Self s -> LitSet s
sandbox  :: !(LitSet s)
      -- ^ sandbox used to construct conflict clause

    , forall s. Self s -> Trail s
trail :: {-# UNPACK #-} !(Trail s)
      -- ^ solution trail

    , forall s. Self s -> Stats s
stats :: !(Stats s)
    }

assertSelfInvariants :: Self s -> ST s ()
assertSelfInvariants :: forall s. Self s -> ST s ()
assertSelfInvariants Self s
_ = () -> ST s ()
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

solve :: Solver s -> ST s Bool
solve :: forall s. Solver s -> ST s Bool
solve solver :: Solver s
solver@Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = ST s Bool -> ST s Bool -> ST s Bool
forall s. ST s Bool -> ST s Bool -> ST s Bool
whenOk_ (Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
simplify Solver s
solver) (ST s Bool -> ST s Bool) -> ST s Bool -> ST s Bool
forall a b. (a -> b) -> a -> b
$ do
    clauseDB <- STRef s (ClauseDB s) -> ST s (ClauseDB s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (ClauseDB s)
clauses

    litCount <- readSTRef nextLit
    level    <- newPrimVar (Level 0)
    sandbox  <- newLitSet litCount
    reasons  <- newLitTable litCount nullClause

    zero     <- readSTRef zeroPA

    levels   <- readSTRef zeroLevels
    qhead    <- readPrimVar zeroHead >>= newPrimVar
    vars     <- readSTRef zeroVars >>= cloneVarSet
    pa       <- readSTRef zeroPA >>= clonePartialAssignment
    trail    <- readSTRef zeroTrail >>= cloneTrail

    prev     <- newPartialAssignment litCount
    
    let stats = Stats s
statistics

    TRACING(sizeofVarSet vars >>= \n -> traceM $ "vars to solve " ++ show n)
    TRACING(tracePartialAssignment pa)

    let self = Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
sandbox :: LitSet s
reasons :: LitTable s Clause2
zero :: PartialAssignment s
levels :: Levels s
qhead :: PrimVar s Int
vars :: VarSet s
pa :: PartialAssignment s
trail :: Trail s
prev :: PartialAssignment s
stats :: Stats s
..}

    solveLoop self >>= \case
        Bool
False -> Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
unsat Solver s
solver
        Bool
True  -> do
            STRef s (PartialAssignment s) -> PartialAssignment s -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s (PartialAssignment s)
prevPA PartialAssignment s
pa
            Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

initialEnqueue :: Trail s -> PartialAssignment s -> Levels s -> VarSet s -> Lit -> ST s ()
initialEnqueue :: forall s.
Trail s
-> PartialAssignment s -> Levels s -> VarSet s -> Lit -> ST s ()
initialEnqueue Trail s
trail PartialAssignment s
pa Levels s
levels VarSet s
vars Lit
l = do
    Lit -> PartialAssignment s -> ST s ()
forall s. Lit -> PartialAssignment s -> ST s ()
insertPartialAssignment Lit
l PartialAssignment s
pa
    Var -> VarSet s -> ST s ()
forall s. Var -> VarSet s -> ST s ()
deleteVarSet (Lit -> Var
litToVar Lit
l) VarSet s
vars
    Levels s -> Lit -> Level -> ST s ()
forall s. Levels s -> Lit -> Level -> ST s ()
setLevel Levels s
levels Lit
l Level
zeroLevel
    Lit -> Trail s -> ST s ()
forall s. Lit -> Trail s -> ST s ()
pushTrail Lit
l Trail s
trail

enqueue :: Self s -> Lit -> Level -> Clause2 -> ST s ()
enqueue :: forall s. Self s -> Lit -> Level -> Clause2 -> ST s ()
enqueue Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} Lit
l Level
d Clause2
c = do
    TRACING(traceM $ "enqueue " ++ show (l, d, c))
    ASSERTING(assertLiteralUndef l pa)
    ASSERTING(assertST "enqueue reason" (isNullClause c || litInClause l c))

    Lit -> PartialAssignment s -> ST s ()
forall s. Lit -> PartialAssignment s -> ST s ()
insertPartialAssignment Lit
l PartialAssignment s
pa
    Var -> VarSet s -> ST s ()
forall s. Var -> VarSet s -> ST s ()
deleteVarSet (Lit -> Var
litToVar Lit
l) VarSet s
vars
    Lit -> Trail s -> ST s ()
forall s. Lit -> Trail s -> ST s ()
pushTrail Lit
l Trail s
trail
    Levels s -> Lit -> Level -> ST s ()
forall s. Levels s -> Lit -> Level -> ST s ()
setLevel Levels s
levels Lit
l Level
d
    LitTable s Clause2 -> Lit -> Clause2 -> ST s ()
forall s a. LitTable s a -> Lit -> a -> ST s ()
writeLitTable LitTable s Clause2
reasons Lit
l Clause2
c
    

unsetLiteral :: Self s -> Lit -> ST s ()
unsetLiteral :: forall s. Self s -> Lit -> ST s ()
unsetLiteral Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} Lit
l = do
    -- TODO: assert l in pa
    -- TODO: assert (litToVar l) not in vars
    Lit -> PartialAssignment s -> ST s ()
forall s. Lit -> PartialAssignment s -> ST s ()
deletePartialAssignment Lit
l PartialAssignment s
pa
    Var -> VarSet s -> ST s ()
forall s. Var -> VarSet s -> ST s ()
insertVarSet (Lit -> Var
litToVar Lit
l) VarSet s
vars

boostSandbox :: Self s -> ST s ()
boostSandbox :: forall s. Self s -> ST s ()
boostSandbox Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} = do
    n <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
size
    go 0 n
  where
    LS SS {PrimVar s Int
MutablePrimArray s Int
size :: PrimVar s Int
dense :: MutablePrimArray s Int
sparse :: MutablePrimArray s Int
sparse :: forall s. SparseSet s -> MutablePrimArray s Int
dense :: forall s. SparseSet s -> MutablePrimArray s Int
size :: forall s. SparseSet s -> PrimVar s Int
..} = LitSet s
sandbox

    go :: Int -> Int -> ST s ()
go !Int
i !Int
n = Bool -> ST s () -> ST s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ do
        l <- MutablePrimArray s Int -> Int -> ST s Int
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> ST s a
readPrimArray MutablePrimArray s Int
dense Int
i
        weightVarSet (litToVar (MkLit l)) boost vars
        go (i + 1) n

solveLoop :: forall s. Self s -> ST s Bool
solveLoop :: forall s. Self s -> ST s Bool
solveLoop self :: Self s
self@Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} = do
    let Trail PrimVar s Int
sizeVar MutablePrimArray s Lit
_ = Trail s
trail
    n <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
sizeVar
    i <- readPrimVar qhead

    TRACING(traceM $ "!!! SOLVE: " ++ show (i, n))
    TRACING(tracePartialAssignment zero)
    TRACING(tracePartialAssignment pa)
    TRACING(traceTrail reasons levels trail)

    if i < n
    then do
        -- traceM $ "i < n: " ++ show (i, n)
        -- traceTrail reasons levels trail
        l <- indexTrail trail i

        writePrimVar qhead (i + 1)
        unitPropagate self l
    else
        noUnit
  where
    noUnit :: ST s Bool
    noUnit :: ST s Bool
noUnit = VarSet s -> ST s Bool -> (Var -> ST s Bool) -> ST s Bool
forall s r. VarSet s -> ST s r -> (Var -> ST s r) -> ST s r
minViewVarSet VarSet s
vars ST s Bool
noVar Var -> ST s Bool
yesVar

    noVar :: ST s Bool
    noVar :: ST s Bool
noVar = do
        TRACING(traceM ">>> SOLVE: SAT")
        Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

    yesVar :: Var -> ST s Bool
    yesVar :: Var -> ST s Bool
yesVar !Var
v = do
        TRACING(traceM $ ">>> SOLVE: deciding variable " ++ show v)
        -- increase decision level
        lvl <- PrimVar (PrimState (ST s)) Level -> ST s Level
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level
        let !lvl' = Level -> Level
forall a. Enum a => a -> a
succ Level
lvl
        writePrimVar level lvl'

        l' <- lookupPartialAssignment l prev <&> \case
            LBool
LTrue  -> Lit -> Lit
neg Lit
l
            LBool
LFalse -> Lit
l
            LBool
LUndef -> Lit
l

        enqueue self l' lvl' nullClause

        -- solve loop
        modifyPrimVar qhead $ \Int
i -> Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
        unitPropagate self l'
      where
        !l :: Lit
l = Var -> Lit
varToLit Var
v

unitPropagate :: forall s. Self s -> Lit -> ST s Bool

#ifdef TWO_WATCHED_LITERALS

unitPropagate :: forall s. Self s -> Lit -> ST s Bool
unitPropagate self :: Self s
self@Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} !Lit
l  = do
    TRACING(traceM ("!!! PROPAGATE " ++ show l))

    ASSERTING(let Trail sizeVar trailLits = trail)
    ASSERTING(n <- readPrimVar sizeVar)
    ASSERTING(assertST "trail not empty" $ n > 0)
    ASSERTING(q <- readPrimVar qhead)
    ASSERTING(assertST "qhead" $ q <= n)
    TRACING(traceM $ show q)
    ASSERTING(ll <- indexTrail trail (q - 1))
    ASSERTING(assertST "end of the trail is the var we propagate" $ l == ll)

    watches <- Lit -> ClauseDB s -> ST s (Vec s Watch)
forall s. Lit -> ClauseDB s -> ST s (Vec s Watch)
lookupClauseDB (Lit -> Lit
neg Lit
l) ClauseDB s
clauseDB
    size <- sizeofVec watches
    go watches 0 0 size
  where
    go :: Vec s Watch -> Int -> Int -> Int -> ST s Bool
    go :: Vec s Watch -> Int -> Int -> Int -> ST s Bool
go !Vec s Watch
watches !Int
i !Int
j !Int
size
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
size
        = do
            Vec s Watch -> Int -> ST s ()
forall s a. Vec s a -> Int -> ST s ()
shrinkVec Vec s Watch
watches Int
j
            Self s -> ST s Bool
forall s. Self s -> ST s Bool
solveLoop Self s
self

        | Bool
otherwise
        = Vec s Watch -> Int -> ST s Watch
forall s a. Vec s a -> Int -> ST s a
readVec Vec s Watch
watches Int
i ST s Watch -> (Watch -> ST s Bool) -> ST s Bool
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ w :: Watch
w@(W Lit
l' Clause2
c) -> do
            let onConflict :: ST s Bool
                {-# INLINE onConflict #-}
                onConflict :: ST s Bool
onConflict = do
                    Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w
                    Vec s Watch -> Int -> Int -> Int -> ST s ()
forall s. Vec s Watch -> Int -> Int -> Int -> ST s ()
copyWatches Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size
                    Self s -> Clause2 -> ST s Bool
forall s. Self s -> Clause2 -> ST s Bool
backtrack Self s
self Clause2
c

                onSatisfied :: ST s Bool
                {-# INLINE onSatisfied #-}
                onSatisfied :: ST s Bool
onSatisfied = do
                    Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w
                    Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size

                onUnit :: Lit -> ST s Bool
                {-# INLINE onUnit #-}
                onUnit :: Lit -> ST s Bool
onUnit Lit
u = do
                    Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w

                    lvl <- PrimVar (PrimState (ST s)) Level -> ST s Level
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level
                    enqueue self u lvl c
                    go watches (i + 1) (j + 1) size

            if Clause2 -> Bool
isBinaryClause2 Clause2
c
            then Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l' PartialAssignment s
pa ST s LBool -> (LBool -> ST s Bool) -> ST s Bool
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                LBool
LUndef -> Lit -> ST s Bool
onUnit Lit
l'
                LBool
LTrue  -> ST s Bool
onSatisfied
                LBool
LFalse -> ST s Bool
onConflict
            else do
                let kontUnitPropagate :: Satisfied_ -> ST s Bool
kontUnitPropagate = \case
                        Satisfied_
Conflicting_      -> ST s Bool
onConflict
                        Satisfied_
Satisfied_        -> ST s Bool
onSatisfied
                        Unit_ Lit
u           -> Lit -> ST s Bool
onUnit Lit
u
                        Unresolved_ Lit
l1 Lit
l2
                            | Lit
l2 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l', Lit
l2 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l
                            -> do
                                Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l2 Watch
w ClauseDB s
clauseDB
                                Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
j Int
size

                            | Lit
l1 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l', Lit
l1 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l
                            -> do
                                Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l1 Watch
w ClauseDB s
clauseDB
                                Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
j Int
size

                            | Bool
otherwise
                            -> String -> ST s Bool
forall a. HasCallStack => String -> a
error (String
"watch" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Lit, Lit, Lit, Lit) -> String
forall a. Show a => a -> String
show (Lit
l, Lit
l1, Lit
l2, Lit
l'))

                    {-# INLINE [1] kontUnitPropagate #-}

                PartialAssignment s
-> Clause2 -> (Satisfied_ -> ST s Bool) -> ST s Bool
forall s r.
PartialAssignment s -> Clause2 -> (Satisfied_ -> ST s r) -> ST s r
satisfied2_ PartialAssignment s
pa Clause2
c Satisfied_ -> ST s Bool
kontUnitPropagate

copyWatches :: Vec s Watch -> Int -> Int -> Int -> ST s ()
copyWatches :: forall s. Vec s Watch -> Int -> Int -> Int -> ST s ()
copyWatches Vec s Watch
watches Int
i Int
j Int
size = do
    if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
size
    then do
        w' <- Vec s Watch -> Int -> ST s Watch
forall s a. Vec s a -> Int -> ST s a
readVec Vec s Watch
watches Int
i
        writeVec watches j w'
        copyWatches watches (i + 1) (j + 1) size

    else Vec s Watch -> Int -> ST s ()
forall s a. Vec s a -> Int -> ST s ()
shrinkVec Vec s Watch
watches Int
j
#else

unitPropagate self@Self {..} _l = go clauseDB
  where
    go :: [Clause2] -> ST s Bool
    go []     = solveLoop self
    go (c:cs) = satisfied2_ pa c $ \case
        Conflicting_    -> backtrack self c
        Satisfied_      -> go cs
        Unit_ u         -> do
            lvl <- readPrimVar level
            enqueue self u lvl c
            go cs
        Unresolved_ _ _ -> go cs
#endif

traceCause :: LitSet s -> ST s ()
traceCause :: forall s. LitSet s -> ST s ()
traceCause LitSet s
sandbox = do
    xs <- LitSet s -> ST s Clause
forall s. LitSet s -> ST s Clause
elemsLitSet LitSet s
sandbox
    traceM $ "current cause " ++ show xs

withTwoLargestLevels :: LitSet s -> Int -> Levels s -> (Level -> Level -> ST s r) -> ST s r
withTwoLargestLevels :: forall s r.
LitSet s -> Int -> Levels s -> (Level -> Level -> ST s r) -> ST s r
withTwoLargestLevels !LitSet s
sandbox !Int
conflictSize !Levels s
levels Level -> Level -> ST s r
kont =
    Level -> Level -> Int -> ST s r
go Level
zeroLevel Level
zeroLevel Int
0
  where
    go :: Level -> Level -> Int -> ST s r
go Level
d1 Level
d2 Int
i
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
conflictSize = Level -> Level -> ST s r
kont Level
d1 Level
d2
        | Bool
otherwise = do
            d <- LitSet s -> Int -> ST s Lit
forall s. LitSet s -> Int -> ST s Lit
indexLitSet LitSet s
sandbox Int
i ST s Lit -> (Lit -> ST s Level) -> ST s Level
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Levels s -> Lit -> ST s Level
forall s. Levels s -> Lit -> ST s Level
getLevel Levels s
levels
            if d > d2 then go d2 d (i + 1)
            else if d > d1 then go d d2 (i + 1)
            else go d1 d2 (i + 1)

analyse :: forall s. Self s -> Clause2 -> ST s Level
analyse :: forall s. Self s -> Clause2 -> ST s Level
analyse Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} !Clause2
cause = do
    TRACING(traceM $ "!!! ANALYSE: " ++ show cause)
    let Trail PrimVar s Int
size MutablePrimArray s Lit
lits = Trail s
trail
    n <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
size
    clearLitSet sandbox
    forLitInClause2_ cause insertSandbox
    conflictSize <- sizeofLitSet sandbox

    withTwoLargestLevels sandbox conflictSize levels $ \Level
d1 Level
d2 -> do
        lvl <- PrimVar (PrimState (ST s)) Level -> ST s Level
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level
        if (d1 < lvl) then return d1 else if (d2 < lvl) then return d2 else go lits n (n - 1)
  where

    insertSandbox :: Lit -> ST s ()
insertSandbox !Lit
l = Lit -> LitSet s -> ST s ()
forall s. Lit -> LitSet s -> ST s ()
insertLitSet Lit
l LitSet s
sandbox
    {-# INLINE insertSandbox #-}

    go :: MutablePrimArray s Lit -> Int -> Int -> ST s Level
    go :: MutablePrimArray s Lit -> Int -> Int -> ST s Level
go !MutablePrimArray s Lit
lits !Int
n !Int
i
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = do
            l <- MutablePrimArray s Lit -> Int -> ST s Lit
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> ST s a
readPrimArray MutablePrimArray s Lit
lits Int
i
            c <- readLitTable reasons l


            if isNullClause c
            then do
                TRACING(traceM $ ">>> decided " ++ show (l, c))
                b <- memberLitSet sandbox (neg l)
                if b
                then do
                    TRACING(traceM $ ">>> decided stop: " ++ show (l, c))
                    tracePartialAssignment zero
                    traceCause sandbox
                    traceTrail reasons levels trail
                    error $ "decision variable" ++ show (b, n, i, l, c, cause)
                else do 
                    TRACING(traceM $ ">>> decided skip: " ++ show (l, c))
                    go lits n (i - 1)
            else do
                b <- memberLitSet sandbox (neg l)
                if b
                then do
                    TRACING(traceM $ ">>> deduced undo" ++ show (l, c))
                    TRACING(traceCause sandbox)

                    ASSERTING(assertST "literal in reason clause" $ litInClause l c)

                    -- resolution of current conflict with the deduction cause
                    forLitInClause2_ c insertSandbox
                    deleteLitSet l       sandbox
                    deleteLitSet (neg l) sandbox

                    TRACING(traceCause sandbox)
                    conflictSize <- sizeofLitSet sandbox

                    withTwoLargestLevels sandbox conflictSize levels $ \Level
d1 Level
d2 -> do
                        lvl <- PrimVar (PrimState (ST s)) Level -> ST s Level
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level
                        -- traceM $ "UIP? " ++ show (lvl, d1, d2)
                        if (d1 < lvl) then return d1 else if (d2 < lvl) then return d2 else go lits n (i - 1)
                else do
                    TRACING(traceM $ ">>> decuced skip" ++ show (l, c))
                    go lits n (i - 1)

        | Bool
otherwise
        = String -> Bool -> ST s ()
forall s. HasCallStack => String -> Bool -> ST s ()
assertST String
"reached end of trail" Bool
False ST s () -> ST s Level -> ST s Level
forall a b. ST s a -> ST s b -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> ST s Level
forall a. HasCallStack => String -> a
error String
"-"

backjump0 :: forall s. Self s -> ST s Bool
backjump0 :: forall s. Self s -> ST s Bool
backjump0 self :: Self s
self@Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} = do
    TRACING(traceM $ "!!! BACKJUMP0")
    TRACING(traceCause sandbox)
    TRACING(traceTrail reasons levels trail)
    ASSERTING(assertSelfInvariants self)

    Stats s -> ST s ()
forall s. Stats s -> ST s ()
incrStatsRestarts Stats s
stats

    PrimVar (PrimState (ST s)) Level -> Level -> ST s ()
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> a -> m ()
writePrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level Level
zeroLevel

    i <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
sizeVar
    go (i - 1)
  where
    Trail PrimVar s Int
sizeVar MutablePrimArray s Lit
_ = Trail s
trail

    go :: Int -> ST s Bool
    go :: Int -> ST s Bool
go Int
i
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = do
            l <- Trail s -> Int -> ST s Lit
forall s. Trail s -> Int -> ST s Lit
indexTrail Trail s
trail Int
i
            dlvl <- getLevel levels l
            if dlvl == zeroLevel
            then done (i + 1)
            else do
                unsetLiteral self l
                go (i - 1)
        | Bool
otherwise = Int -> ST s Bool
done Int
0

    done :: Int -> ST s Bool
    done :: Int -> ST s Bool
done Int
i = do
        conflictSize <- LitSet s -> ST s Int
forall s. LitSet s -> ST s Int
sizeofLitSet LitSet s
sandbox
        u <- case conflictSize of
            Int
1 -> LitSet s -> ST s Lit
forall s. LitSet s -> ST s Lit
unsingletonLitSet LitSet s
sandbox
            Int
_ -> do
                conflictCause <- LitSet s -> ST s Clause2
forall s. LitSet s -> ST s Clause2
litSetToClause LitSet s
sandbox
                satisfied2_ pa conflictCause $ \case
                    Unit_ Lit
l' -> Lit -> ST s Lit
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Lit
l'
                    Satisfied_
x -> String -> ST s Lit
forall a. HasCallStack => String -> a
error (String -> ST s Lit) -> String -> ST s Lit
forall a b. (a -> b) -> a -> b
$ String
"TODO " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Satisfied_) -> String
forall a. Show a => a -> String
show (Int
conflictSize, Satisfied_
x)

        writePrimVar sizeVar i
        writePrimVar qhead (i + 1)
        enqueue self u zeroLevel nullClause

        res <- initialUnitPropagate clauseDB qhead trail levels pa vars u
        if res
        then solveLoop self
        else return False

backjump :: forall s. Self s -> Level -> ST s Bool
backjump :: forall s. Self s -> Level -> ST s Bool
backjump self :: Self s
self@Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} Level
conflictLevel = do
    TRACING(traceM $ "!!! BACKJUMP: " ++ show conflictLevel)
    TRACING(traceCause sandbox)
    TRACING(traceTrail reasons levels trail)

    ASSERTING(assertST "backump level > 0" $ conflictLevel > zeroLevel)

    PrimVar (PrimState (ST s)) Level -> Level -> ST s ()
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> a -> m ()
writePrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level Level
conflictLevel

    let Trail PrimVar s Int
sizeVar MutablePrimArray s Lit
_ = Trail s
trail
    i <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
sizeVar
    go sizeVar (i - 1)
  where
    go :: PrimVar s Int -> Int -> ST s Bool
go PrimVar s Int
sizeVar Int
i = do
        l <- Trail s -> Int -> ST s Lit
forall s. Trail s -> Int -> ST s Lit
indexTrail Trail s
trail Int
i
        dlvl <- getLevel levels l

        if dlvl == conflictLevel
        then do
            TRACING(traceM $ ">>> JUMP: " ++ show (i, l, dlvl, conflictLevel))
            conflictSize <- sizeofLitSet sandbox
            ASSERTING(assertST "conflict size >= 2" $ conflictSize >= 2)

            conflictClause <- litSetToClause sandbox
            TRACING(traceM $ "JUMPED: " ++ show (i, l, dlvl, conflictLevel, conflictClause))

            satisfied2_ pa conflictClause $ \case
                Unit_ Lit
u -> do
                    PrimVar (PrimState (ST s)) Int -> Int -> ST s ()
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> a -> m ()
writePrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
sizeVar (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                    PrimVar (PrimState (ST s)) Int -> Int -> ST s ()
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> a -> m ()
writePrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
qhead (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2)
                    Self s -> Lit -> Level -> Clause2 -> ST s ()
forall s. Self s -> Lit -> Level -> Clause2 -> ST s ()
enqueue Self s
self Lit
u Level
dlvl Clause2
conflictClause

                    TRACING(traceM $ ">>> JUMPED: " ++ show (i, l, dlvl, conflictLevel, conflictClause, u))
                    TRACING(tracePartialAssignment pa)
                    TRACING(traceTrail reasons levels trail)

                    Self s -> Lit -> ST s Bool
forall s. Self s -> Lit -> ST s Bool
unitPropagate Self s
self Lit
u

                Satisfied_
x -> String -> ST s Bool
forall a. HasCallStack => String -> a
error (String -> ST s Bool) -> String -> ST s Bool
forall a b. (a -> b) -> a -> b
$ String
"TODO _" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Satisfied_) -> String
forall a. Show a => a -> String
show (Int
conflictSize, Satisfied_
x)
        else do
            TRACING(traceM $ ">>> UNDO: " ++ show (i, l, dlvl))
            unsetLiteral self l
            go sizeVar (i - 1)

backtrack :: forall s. Self s -> Clause2 -> ST s Bool
backtrack :: forall s. Self s -> Clause2 -> ST s Bool
backtrack self :: Self s
self@Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} !Clause2
cause = do
    TRACING(traceM $ "!!! CONFLICT " ++ show cause)
    TRACING(tracePartialAssignment pa)
    TRACING(traceTrail reasons levels trail)

    Stats s -> ST s ()
forall s. Stats s -> ST s ()
incrStatsConflicts Stats s
stats
    VarSet s -> (Word -> Word) -> ST s ()
forall s. VarSet s -> (Word -> Word) -> ST s ()
scaleVarSet VarSet s
vars Word -> Word
decay

    TRACING(lvl <- readPrimVar level)
    clvl <- Self s -> Clause2 -> ST s Level
forall s. Self s -> Clause2 -> ST s Level
analyse Self s
self Clause2
cause

    TRACING(traceM $ ">>> analysed " ++ show (lvl, clvl, cause))
    TRACING(traceCause sandbox)

    -- learn binary clauses
    conflictSize <- sizeofLitSet sandbox
    when (conflictSize == 2) $ do
        conflictClause <- litSetToClause sandbox
        incrStatsLearnt stats
        incrStatsLearntLiterals stats conflictSize

        case conflictClause of
            MkClause2 Bool
_     Lit
l1 Lit
l2 PrimArray Lit
_ -> Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
forall s. Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
insertClauseDB Lit
l1 Lit
l2 Clause2
conflictClause ClauseDB s
clauseDB

    -- boost literals in conflict clause
    boostSandbox self

    if clvl == Level 0
    then backjump0 self
    else backjump self clvl

-------------------------------------------------------------------------------
-- initial loop
-------------------------------------------------------------------------------

initialLoop :: forall s. ClauseDB s -> PrimVar s Int -> Trail s -> Levels s -> PartialAssignment s -> VarSet s -> ST s Bool
initialLoop :: forall s.
ClauseDB s
-> PrimVar s Int
-> Trail s
-> Levels s
-> PartialAssignment s
-> VarSet s
-> ST s Bool
initialLoop !ClauseDB s
clauseDB !PrimVar s Int
qhead !Trail s
trail !Levels s
levels !PartialAssignment s
pa !VarSet s
vars = do
    let Trail PrimVar s Int
sizeVar MutablePrimArray s Lit
_ = Trail s
trail
    n <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
sizeVar
    i <- readPrimVar qhead

    TRACING(traceM $ "!!! INITIAL: " ++ show (i, n))
    TRACING(tracePartialAssignment pa)

    if i < n
    then do
        -- traceM $ "i < n: " ++ show (i, n)
        -- traceTrail reasons levels trail
        l <- indexTrail trail i

        writePrimVar qhead (i + 1)
        initialUnitPropagate clauseDB qhead trail levels pa vars l

    else return True

initialUnitPropagate :: forall s. ClauseDB s -> PrimVar s Int -> Trail s -> Levels s -> PartialAssignment s -> VarSet s -> Lit -> ST s Bool
initialUnitPropagate :: forall s.
ClauseDB s
-> PrimVar s Int
-> Trail s
-> Levels s
-> PartialAssignment s
-> VarSet s
-> Lit
-> ST s Bool
initialUnitPropagate !ClauseDB s
clauseDB !PrimVar s Int
qhead !Trail s
trail !Levels s
levels !PartialAssignment s
pa !VarSet s
vars !Lit
l = do
    let _unused :: Lit
_unused = Lit
l
    TRACING(traceM ("initialUnitPropagate " ++ show l))
#ifdef TWO_WATCHED_LITERALS
    watches <- Lit -> ClauseDB s -> ST s (Vec s Watch)
forall s. Lit -> ClauseDB s -> ST s (Vec s Watch)
lookupClauseDB (Lit -> Lit
neg Lit
l) ClauseDB s
clauseDB
    size <- sizeofVec watches
    TRACING(traceM ("initialUnitPropagate watches: " ++ show size))
    go watches 0 0 size
  where
    go :: Vec s Watch -> Int -> Int -> Int -> ST s Bool
    go :: Vec s Watch -> Int -> Int -> Int -> ST s Bool
go !Vec s Watch
watches !Int
i !Int
j !Int
size
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
size
        = do
            Vec s Watch -> Int -> ST s ()
forall s a. Vec s a -> Int -> ST s ()
shrinkVec Vec s Watch
watches Int
j
            ClauseDB s
-> PrimVar s Int
-> Trail s
-> Levels s
-> PartialAssignment s
-> VarSet s
-> ST s Bool
forall s.
ClauseDB s
-> PrimVar s Int
-> Trail s
-> Levels s
-> PartialAssignment s
-> VarSet s
-> ST s Bool
initialLoop ClauseDB s
clauseDB PrimVar s Int
qhead Trail s
trail Levels s
levels PartialAssignment s
pa VarSet s
vars

        | Bool
otherwise
        = Vec s Watch -> Int -> ST s Watch
forall s a. Vec s a -> Int -> ST s a
readVec Vec s Watch
watches Int
i ST s Watch -> (Watch -> ST s Bool) -> ST s Bool
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ w :: Watch
w@(W Lit
l' Clause2
c) ->
          PartialAssignment s
-> Clause2 -> (Satisfied_ -> ST s Bool) -> ST s Bool
forall s r.
PartialAssignment s -> Clause2 -> (Satisfied_ -> ST s r) -> ST s r
satisfied2_ PartialAssignment s
pa Clause2
c (Watch -> Lit -> Satisfied_ -> ST s Bool
kontInitialUnitPropagate Watch
w Lit
l')
      where
        {-# INLINE [1] kontInitialUnitPropagate #-}
        kontInitialUnitPropagate :: Watch -> Lit -> Satisfied_ -> ST s Bool
kontInitialUnitPropagate Watch
w Lit
l' = \case
            Satisfied_
Conflicting_ -> do
                Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w
                Vec s Watch -> Int -> Int -> Int -> ST s ()
forall s. Vec s Watch -> Int -> Int -> Int -> ST s ()
copyWatches Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size
                Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
            Satisfied_
Satisfied_ -> do
                Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w
                Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size
            Unit_ Lit
u -> do
                Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w
                Trail s
-> PartialAssignment s -> Levels s -> VarSet s -> Lit -> ST s ()
forall s.
Trail s
-> PartialAssignment s -> Levels s -> VarSet s -> Lit -> ST s ()
initialEnqueue Trail s
trail PartialAssignment s
pa Levels s
levels VarSet s
vars Lit
u
                Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size
            Unresolved_ Lit
l1 Lit
l2
                | Lit
l2 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l', Lit
l2 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l
                -> do
                    Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l2 Watch
w ClauseDB s
clauseDB
                    Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
j Int
size

                | Lit
l1 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l', Lit
l1 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l
                -> do
                    Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l1 Watch
w ClauseDB s
clauseDB
                    Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
j Int
size

                | Bool
otherwise
                -> String -> ST s Bool
forall a. HasCallStack => String -> a
error (String
"watch" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Lit, Lit, Lit, Lit) -> String
forall a. Show a => a -> String
show (Lit
l, Lit
l1, Lit
l2, Lit
l'))
#else
    go clauseDB
  where
    go [] = initialLoop clauseDB units vars pa
    go (c:cs) = satisfied2_ pa c (kontInitialUnitPropagate cs)

    {-# INLINE [1] kontInitialUnitPropagate #-}
    kontInitialUnitPropagate :: [Clause2] -> Satisfied_ -> ST s Bool
    kontInitialUnitPropagate cs = \case
        Conflicting_    -> return False
        Unresolved_ _ _ -> go cs
        Satisfied_      -> go cs
        Unit_ u         -> do
            insertLitSet u units
            go cs
#endif

-------------------------------------------------------------------------------
-- simplify
-------------------------------------------------------------------------------

-- | Simplify solver
simplify :: Solver s -> ST s Bool
simplify :: forall s. Solver s -> ST s Bool
simplify Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = STRef s Bool -> ST s Bool -> ST s Bool
forall s. STRef s Bool -> ST s Bool -> ST s Bool
whenOk STRef s Bool
ok (ST s Bool -> ST s Bool) -> ST s Bool -> ST s Bool
forall a b. (a -> b) -> a -> b
$ Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
-- TODO: go through clauses:
-- * filter out satisfied clauses
-- * filter out the solved literals from remaining clauses

-------------------------------------------------------------------------------
-- statistics
-------------------------------------------------------------------------------

num_vars :: Solver s -> ST s Int
num_vars :: forall s. Solver s -> ST s Int
num_vars Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = do
    n <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
nextLit
    return (unsafeShiftR n 1)

num_clauses :: Solver s -> ST s Int
num_clauses :: forall s. Solver s -> ST s Int
num_clauses Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = Stats s -> ST s Int
forall s. Stats s -> ST s Int
readStatsClauses Stats s
statistics

num_learnts :: Solver s -> ST s Int
num_learnts :: forall s. Solver s -> ST s Int
num_learnts Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = Stats s -> ST s Int
forall s. Stats s -> ST s Int
readStatsLearnt Stats s
statistics

num_learnt_literals :: Solver s -> ST s Int
num_learnt_literals :: forall s. Solver s -> ST s Int
num_learnt_literals Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = Stats s -> ST s Int
forall s. Stats s -> ST s Int
readStatsLearntLiterals Stats s
statistics

num_conflicts :: Solver s -> ST s Int
num_conflicts :: forall s. Solver s -> ST s Int
num_conflicts Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = Stats s -> ST s Int
forall s. Stats s -> ST s Int
readStatsConflicts Stats s
statistics

num_restarts :: Solver s -> ST s Int
num_restarts :: forall s. Solver s -> ST s Int
num_restarts Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = Stats s -> ST s Int
forall s. Stats s -> ST s Int
readStatsRestarts Stats s
statistics

-------------------------------------------------------------------------------
-- queries
---------------------------------------- ---------------------------------------

-- | Lookup model value
modelValue :: Solver s -> Lit -> ST s Bool
modelValue :: forall s. Solver s -> Lit -> ST s Bool
modelValue Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} Lit
l = do
    pa <- STRef s (PartialAssignment s) -> ST s (PartialAssignment s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (PartialAssignment s)
prevPA
    lookupPartialAssignment l pa <&> \case
        LBool
LUndef -> Bool
False
        LBool
LTrue  -> Bool
True
        LBool
LFalse -> Bool
False