{-# 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
    LitTable s (Vec s Watch)
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

    [Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
0 .. Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] ((Int -> ST s ()) -> ST s ()) -> (Int -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
        Vec s Watch
vec <- Int -> ST s (Vec s Watch)
forall s a. Int -> ST s (Vec s a)
newVec Int
16
        LitTable s (Vec s Watch) -> Lit -> Vec s Watch -> ST s ()
forall s a. LitTable s a -> Lit -> a -> ST s ()
writeLitTable LitTable s (Vec s Watch)
arr (Int -> Lit
MkLit Int
i) Vec s Watch
vec

    ClauseDB s -> ST s (ClauseDB s)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (LitTable s (Vec s Watch) -> ClauseDB s
forall s. LitTable s (Vec s Watch) -> ClauseDB s
CDB LitTable s (Vec s Watch)
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.
    Int
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
newSize = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
newSize' Int
4096
    if Int
newSize Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
oldSize
    then ClauseDB s -> ST s (ClauseDB s)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ClauseDB s
cdb
    else do
        String -> ST s ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> ST s ()) -> String -> ST s ()
forall a b. (a -> b) -> a -> b
$ String
"resize" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
newSize
        LitTable s (Vec s Watch)
new <- Int -> Vec s Watch -> ST s (LitTable s (Vec s Watch))
forall a s. Int -> a -> ST s (LitTable s a)
newLitTable Int
newSize Vec s Watch
forall a. HasCallStack => a
undefined

        [Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
0 .. Int
newSize Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] ((Int -> ST s ()) -> ST s ()) -> (Int -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
            if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
oldSize
            then do
                Vec s Watch
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)
                LitTable s (Vec s Watch) -> Lit -> Vec s Watch -> ST s ()
forall s a. LitTable s a -> Lit -> a -> ST s ()
writeLitTable LitTable s (Vec s Watch)
new (Int -> Lit
MkLit Int
i) Vec s Watch
x
            else do
                Vec s Watch
vec <- Int -> ST s (Vec s Watch)
forall s a. Int -> ST s (Vec s a)
newVec Int
16
                LitTable s (Vec s Watch) -> Lit -> Vec s Watch -> ST s ()
forall s a. LitTable s a -> Lit -> a -> ST s ()
writeLitTable LitTable s (Vec s Watch)
new (Int -> Lit
MkLit Int
i) Vec s Watch
vec

        ClauseDB s -> ST s (ClauseDB s)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (LitTable s (Vec s Watch) -> ClauseDB s
forall s. LitTable s (Vec s Watch) -> ClauseDB s
CDB LitTable s (Vec s Watch)
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
    Vec s Watch
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
    Vec s Watch
ws' <- Vec s Watch -> Watch -> ST s (Vec s Watch)
forall s a. Vec s a -> a -> ST s (Vec s a)
insertVec Vec s Watch
ws Watch
w
    LitTable s (Vec s Watch) -> Lit -> Vec s Watch -> ST s ()
forall s a. LitTable s a -> Lit -> a -> ST s ()
writeLitTable LitTable s (Vec s Watch)
cdb Lit
l Vec s Watch
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
    Vec s Watch
v <- Int -> ST s (Vec s Watch)
forall s a. Int -> ST s (Vec s a)
newVec Int
0
    LitTable s (Vec s Watch) -> Lit -> Vec s Watch -> ST s ()
forall s a. LitTable s a -> Lit -> a -> ST s ()
writeLitTable LitTable s (Vec s Watch)
cdb Lit
l Vec s Watch
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
    STRef s Bool
ok         <- Bool -> ST s (STRef s Bool)
forall a s. a -> ST s (STRef s a)
newSTRef Bool
True
    STRef s Int
nextLit    <- Int -> ST s (STRef s Int)
forall a s. a -> ST s (STRef s a)
newSTRef Int
0
    Stats s
statistics <- ST s (Stats s)
forall s. ST s (Stats s)
newStats

    STRef s (Levels s)
zeroLevels <- Int -> ST s (Levels s)
forall s. Int -> ST s (Levels s)
newLevels Int
1024 ST s (Levels s)
-> (Levels s -> ST s (STRef s (Levels s)))
-> ST s (STRef s (Levels 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
>>= Levels s -> ST s (STRef s (Levels s))
forall a s. a -> ST s (STRef s a)
newSTRef
    STRef s (VarSet s)
zeroVars   <- ST s (VarSet s)
forall s. ST s (VarSet s)
newVarSet ST s (VarSet s)
-> (VarSet s -> ST s (STRef s (VarSet s)))
-> ST s (STRef s (VarSet 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 (STRef s (VarSet s))
forall a s. a -> ST s (STRef s a)
newSTRef
    STRef s (PartialAssignment s)
zeroPA     <- Int -> ST s (PartialAssignment s)
forall s. Int -> ST s (PartialAssignment s)
newPartialAssignment Int
1024 ST s (PartialAssignment s)
-> (PartialAssignment s -> ST s (STRef s (PartialAssignment s)))
-> ST s (STRef s (PartialAssignment 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
>>= PartialAssignment s -> ST s (STRef s (PartialAssignment s))
forall a s. a -> ST s (STRef s a)
newSTRef
    PrimVar s Int
zeroHead   <- Int -> ST s (PrimVar (PrimState (ST s)) Int)
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
a -> m (PrimVar (PrimState m) a)
newPrimVar Int
0
    STRef s (Trail s)
zeroTrail  <- Int -> ST s (Trail s)
forall s. Int -> ST s (Trail s)
newTrail Int
1024 ST s (Trail s)
-> (Trail s -> ST s (STRef s (Trail s)))
-> ST s (STRef s (Trail 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
>>= Trail s -> ST s (STRef s (Trail s))
forall a s. a -> ST s (STRef s a)
newSTRef

    STRef s (PartialAssignment s)
prevPA     <- Int -> ST s (PartialAssignment s)
forall s. Int -> ST s (PartialAssignment s)
newPartialAssignment Int
1024 ST s (PartialAssignment s)
-> (PartialAssignment s -> ST s (STRef s (PartialAssignment s)))
-> ST s (STRef s (PartialAssignment 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
>>= PartialAssignment s -> ST s (STRef s (PartialAssignment s))
forall a s. a -> ST s (STRef s a)
newSTRef

#ifdef TWO_WATCHED_LITERALS
    STRef s (ClauseDB s)
clauses    <- Int -> ST s (ClauseDB s)
forall s. Int -> ST s (ClauseDB s)
newClauseDB Int
0 ST s (ClauseDB s)
-> (ClauseDB s -> ST s (STRef s (ClauseDB s)))
-> ST s (STRef s (ClauseDB 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
>>= ClauseDB s -> ST s (STRef s (ClauseDB s))
forall a s. a -> ST s (STRef s a)
newSTRef
#else
    clauses    <- newSTRef []
#endif
    LCG s
lcg        <- Word64 -> ST s (LCG s)
forall s. Word64 -> ST s (LCG s)
newLCG Word64
44
    Solver s -> ST s (Solver s)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return 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 :: 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
ok :: STRef s Bool
nextLit :: STRef s Int
statistics :: Stats s
zeroLevels :: STRef s (Levels s)
zeroVars :: STRef s (VarSet s)
zeroPA :: STRef s (PartialAssignment s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
..}

-- | 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
    Int
l' <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
nextLit
    let n :: Int
n = Int
l' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2
    STRef s Int -> Int -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Int
nextLit Int
n
    let l :: Lit
l = Int -> Lit
MkLit Int
l'

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

    Levels s
levels <- STRef s (Levels s) -> ST s (Levels s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (Levels s)
zeroLevels
    Levels s
levels' <- Levels s -> Int -> ST s (Levels s)
forall s. Levels s -> Int -> ST s (Levels s)
extendLevels Levels s
levels Int
n
    STRef s (Levels s) -> Levels s -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s (Levels s)
zeroLevels Levels s
levels'

    PartialAssignment s
pa <- STRef s (PartialAssignment s) -> ST s (PartialAssignment s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (PartialAssignment s)
zeroPA
    PartialAssignment s
pa' <- PartialAssignment s -> ST s (PartialAssignment s)
forall s. PartialAssignment s -> ST s (PartialAssignment s)
extendPartialAssignment PartialAssignment s
pa
    STRef s (PartialAssignment s) -> PartialAssignment s -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s (PartialAssignment s)
zeroPA PartialAssignment s
pa'

    Trail s
trail <- STRef s (Trail s) -> ST s (Trail s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (Trail s)
zeroTrail
    Trail s
trail' <- Trail s -> Int -> ST s (Trail s)
forall s. Trail s -> Int -> ST s (Trail s)
extendTrail Trail s
trail Int
n
    STRef s (Trail s) -> Trail s -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s (Trail s)
zeroTrail Trail s
trail'

    -- add unsolved variable.
    VarSet s
vars <- STRef s (VarSet s) -> ST s (VarSet s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (VarSet s)
zeroVars
    VarSet s
vars' <- Int -> VarSet s -> ST s (VarSet s)
forall s. Int -> VarSet s -> ST s (VarSet s)
extendVarSet Int
n VarSet s
vars
    STRef s (VarSet s) -> VarSet s -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s (VarSet s)
zeroVars VarSet s
vars'

#ifdef TWO_WATCHED_LITERALS
    ClauseDB s
clauseDB  <- STRef s (ClauseDB s) -> ST s (ClauseDB s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (ClauseDB s)
clauses
    ClauseDB s
clauseDB' <- ClauseDB s -> Int -> ST s (ClauseDB s)
forall s. ClauseDB s -> Int -> ST s (ClauseDB s)
extendClauseDB ClauseDB s
clauseDB Int
n
    STRef s (ClauseDB s) -> ClauseDB s -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s (ClauseDB s)
clauses ClauseDB s
clauseDB'
#endif

    Var -> VarSet s -> ST s ()
forall s. Var -> VarSet s -> ST s ()
insertVarSet (Lit -> Var
litToVar Lit
l) VarSet s
vars'

    Lit -> ST s Lit
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Lit
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
    VarSet s
vars <- STRef s (VarSet s) -> ST s (VarSet s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (VarSet s)
zeroVars
    Var -> (Word -> Word) -> VarSet s -> ST s ()
forall s. Var -> (Word -> Word) -> VarSet s -> ST s ()
weightVarSet (Lit -> Var
litToVar Lit
l) Word -> Word
boost VarSet s
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
    PartialAssignment s
pa <- STRef s (PartialAssignment s) -> ST s (PartialAssignment s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (PartialAssignment s)
zeroPA
    Satisfied
s <- PartialAssignment s -> Clause -> ST s Satisfied
forall s. PartialAssignment s -> Clause -> ST s Satisfied
satisfied PartialAssignment s
pa Clause
clause
    case Satisfied
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 s
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 Bool
_ Lit
l1 Lit
l2 PrimArray Lit
_ = Clause2
c
            Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
forall s. Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
insertClauseDB Lit
l1 Lit
l2 Clause2
c ClauseDB s
clauseDB
#else
            writeSTRef clauses (c : clauseDB)
#endif

            Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

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

            ClauseDB s
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
qhead = PrimVar s Int
zeroHead

            Levels s
levels <- STRef s (Levels s) -> ST s (Levels s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (Levels s)
zeroLevels
            Trail s
trail  <- STRef s (Trail s) -> ST s (Trail s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (Trail s)
zeroTrail
            VarSet s
vars   <- STRef s (VarSet s) -> ST s (VarSet s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (VarSet s)
zeroVars

            -- insert new literal
            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
l

            -- propagate
            Bool
res <- 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

            if Bool
res
            then Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            else Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
unsat Solver s
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 s
clauseDB <- STRef s (ClauseDB s) -> ST s (ClauseDB s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (ClauseDB s)
clauses

    Int
litCount <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
nextLit
    PrimVar s Level
level    <- Level -> ST s (PrimVar (PrimState (ST s)) Level)
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
a -> m (PrimVar (PrimState m) a)
newPrimVar (Int -> Level
Level Int
0)
    LitSet s
sandbox  <- Int -> ST s (LitSet s)
forall s. Int -> ST s (LitSet s)
newLitSet Int
litCount
    LitTable s Clause2
reasons  <- Int -> Clause2 -> ST s (LitTable s Clause2)
forall a s. Int -> a -> ST s (LitTable s a)
newLitTable Int
litCount Clause2
nullClause

    PartialAssignment s
zero     <- STRef s (PartialAssignment s) -> ST s (PartialAssignment s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (PartialAssignment s)
zeroPA

    Levels s
levels   <- STRef s (Levels s) -> ST s (Levels s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (Levels s)
zeroLevels
    PrimVar s Int
qhead    <- 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
zeroHead ST s Int -> (Int -> ST s (PrimVar s Int)) -> ST s (PrimVar s Int)
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
>>= Int -> ST s (PrimVar s Int)
Int -> ST s (PrimVar (PrimState (ST s)) Int)
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
a -> m (PrimVar (PrimState m) a)
newPrimVar
    VarSet s
vars     <- 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 (VarSet s)) -> ST s (VarSet 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 (VarSet s)
forall s. VarSet s -> ST s (VarSet s)
cloneVarSet
    PartialAssignment s
pa       <- STRef s (PartialAssignment s) -> ST s (PartialAssignment s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (PartialAssignment s)
zeroPA ST s (PartialAssignment s)
-> (PartialAssignment s -> ST s (PartialAssignment s))
-> ST s (PartialAssignment 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
>>= PartialAssignment s -> ST s (PartialAssignment s)
forall s. PartialAssignment s -> ST s (PartialAssignment s)
clonePartialAssignment
    Trail s
trail    <- STRef s (Trail s) -> ST s (Trail s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (Trail s)
zeroTrail ST s (Trail s) -> (Trail s -> ST s (Trail s)) -> ST s (Trail 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
>>= Trail s -> ST s (Trail s)
forall s. Trail s -> ST s (Trail s)
cloneTrail

    PartialAssignment s
prev     <- Int -> ST s (PartialAssignment s)
forall s. Int -> ST s (PartialAssignment s)
newPartialAssignment Int
litCount
    
    let stats :: Stats s
stats = Stats s
statistics

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

    let 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 :: 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
..}

    Self s -> ST s Bool
forall s. Self s -> ST s Bool
solveLoop Self s
self ST s Bool -> (Bool -> 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
        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
    Int
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
    Int -> Int -> ST s ()
go Int
0 Int
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
        Int
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
        Var -> (Word -> Word) -> VarSet s -> ST s ()
forall s. Var -> (Word -> Word) -> VarSet s -> ST s ()
weightVarSet (Lit -> Var
litToVar (Int -> Lit
MkLit Int
l)) Word -> Word
boost VarSet s
vars
        Int -> Int -> ST s ()
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
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
    Int
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
    Int
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
qhead

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

    if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n
    then do
        -- traceM $ "i < n: " ++ show (i, n)
        -- traceTrail reasons levels trail
        Lit
l <- Trail s -> Int -> ST s Lit
forall s. Trail s -> Int -> ST s Lit
indexTrail Trail s
trail Int
i

        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
1)
        Self s -> Lit -> ST s Bool
forall s. Self s -> Lit -> ST s Bool
unitPropagate Self s
self Lit
l
    else
        ST s Bool
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
        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
lvl' = Level -> Level
forall a. Enum a => a -> a
succ Level
lvl
        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
lvl'

        Lit
l' <- Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l PartialAssignment s
prev ST s LBool -> (LBool -> Lit) -> ST s Lit
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            LBool
LTrue  -> Lit -> Lit
neg Lit
l
            LBool
LFalse -> Lit
l
            LBool
LUndef -> Lit
l

        Self s -> Lit -> Level -> Clause2 -> ST s ()
forall s. Self s -> Lit -> Level -> Clause2 -> ST s ()
enqueue Self s
self Lit
l' Level
lvl' Clause2
nullClause

        -- solve loop
        PrimVar (PrimState (ST s)) Int -> (Int -> Int) -> ST s ()
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> (a -> a) -> m ()
modifyPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
qhead ((Int -> Int) -> ST s ()) -> (Int -> Int) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Int
i -> Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
        Self s -> Lit -> ST s Bool
forall s. Self s -> Lit -> ST s Bool
unitPropagate Self s
self Lit
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)

    Vec s Watch
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
    Int
size <- Vec s Watch -> ST s Int
forall s a. Vec s a -> ST s Int
sizeofVec Vec s Watch
watches
    Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches Int
0 Int
0 Int
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

                    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
                    Self s -> Lit -> Level -> Clause2 -> ST s ()
forall s. Self s -> Lit -> Level -> Clause2 -> ST s ()
enqueue Self s
self Lit
u Level
lvl Clause2
c
                    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

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

    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
    Clause
xs <- LitSet s -> ST s Clause
forall s. LitSet s -> ST s Clause
elemsLitSet LitSet s
sandbox
    String -> ST s ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM (String -> ST s ()) -> String -> ST s ()
forall a b. (a -> b) -> a -> b
$ String
"current cause " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Clause -> String
forall a. Show a => a -> String
show Clause
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
            Level
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 Level
d Level -> Level -> Bool
forall a. Ord a => a -> a -> Bool
> Level
d2 then Level -> Level -> Int -> ST s r
go Level
d2 Level
d (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
            else if Level
d Level -> Level -> Bool
forall a. Ord a => a -> a -> Bool
> Level
d1 then Level -> Level -> Int -> ST s r
go Level
d Level
d2 (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
            else Level -> Level -> Int -> ST s r
go Level
d1 Level
d2 (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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
    Int
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
    LitSet s -> ST s ()
forall s. LitSet s -> ST s ()
clearLitSet LitSet s
sandbox
    Clause2 -> (Lit -> ST s ()) -> ST s ()
forall s. Clause2 -> (Lit -> ST s ()) -> ST s ()
forLitInClause2_ Clause2
cause Lit -> ST s ()
insertSandbox
    Int
conflictSize <- LitSet s -> ST s Int
forall s. LitSet s -> ST s Int
sizeofLitSet LitSet s
sandbox

    LitSet s
-> Int -> Levels s -> (Level -> Level -> ST s Level) -> ST s Level
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 Level) -> ST s Level)
-> (Level -> Level -> ST s Level) -> ST s Level
forall a b. (a -> b) -> a -> b
$ \Level
d1 Level
d2 -> do
        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
        if (Level
d1 Level -> Level -> Bool
forall a. Ord a => a -> a -> Bool
< Level
lvl) then Level -> ST s Level
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Level
d1 else if (Level
d2 Level -> Level -> Bool
forall a. Ord a => a -> a -> Bool
< Level
lvl) then Level -> ST s Level
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Level
d2 else MutablePrimArray s Lit -> Int -> Int -> ST s Level
go MutablePrimArray s Lit
lits Int
n (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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
            Lit
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
            Clause2
c <- LitTable s Clause2 -> Lit -> ST s Clause2
forall s a. LitTable s a -> Lit -> ST s a
readLitTable LitTable s Clause2
reasons Lit
l


            if Clause2 -> Bool
isNullClause Clause2
c
            then do
                TRACING(traceM $ ">>> decided " ++ show (l, c))
                Bool
b <- LitSet s -> Lit -> ST s Bool
forall s. LitSet s -> Lit -> ST s Bool
memberLitSet LitSet s
sandbox (Lit -> Lit
neg Lit
l)
                if Bool
b
                then do
                    TRACING(traceM $ ">>> decided stop: " ++ show (l, c))
                    PartialAssignment s -> ST s ()
forall s. PartialAssignment s -> ST s ()
tracePartialAssignment PartialAssignment s
zero
                    LitSet s -> ST s ()
forall s. LitSet s -> ST s ()
traceCause LitSet s
sandbox
                    LitTable s Clause2 -> Levels s -> Trail s -> ST s ()
forall s. LitTable s Clause2 -> Levels s -> Trail s -> ST s ()
traceTrail LitTable s Clause2
reasons Levels s
levels Trail s
trail
                    String -> ST s Level
forall a. HasCallStack => String -> a
error (String -> ST s Level) -> String -> ST s Level
forall a b. (a -> b) -> a -> b
$ String
"decision variable" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Bool, Int, Int, Lit, Clause2, Clause2) -> String
forall a. Show a => a -> String
show (Bool
b, Int
n, Int
i, Lit
l, Clause2
c, Clause2
cause)
                else do 
                    TRACING(traceM $ ">>> decided skip: " ++ show (l, c))
                    MutablePrimArray s Lit -> Int -> Int -> ST s Level
go MutablePrimArray s Lit
lits Int
n (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
            else do
                Bool
b <- LitSet s -> Lit -> ST s Bool
forall s. LitSet s -> Lit -> ST s Bool
memberLitSet LitSet s
sandbox (Lit -> Lit
neg Lit
l)
                if Bool
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
                    Clause2 -> (Lit -> ST s ()) -> ST s ()
forall s. Clause2 -> (Lit -> ST s ()) -> ST s ()
forLitInClause2_ Clause2
c Lit -> ST s ()
insertSandbox
                    Lit -> LitSet s -> ST s ()
forall s. Lit -> LitSet s -> ST s ()
deleteLitSet Lit
l       LitSet s
sandbox
                    Lit -> LitSet s -> ST s ()
forall s. Lit -> LitSet s -> ST s ()
deleteLitSet (Lit -> Lit
neg Lit
l) LitSet s
sandbox

                    TRACING(traceCause sandbox)
                    Int
conflictSize <- LitSet s -> ST s Int
forall s. LitSet s -> ST s Int
sizeofLitSet LitSet s
sandbox

                    LitSet s
-> Int -> Levels s -> (Level -> Level -> ST s Level) -> ST s Level
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 Level) -> ST s Level)
-> (Level -> Level -> ST s Level) -> ST s Level
forall a b. (a -> b) -> a -> b
$ \Level
d1 Level
d2 -> do
                        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
                        -- traceM $ "UIP? " ++ show (lvl, d1, d2)
                        if (Level
d1 Level -> Level -> Bool
forall a. Ord a => a -> a -> Bool
< Level
lvl) then Level -> ST s Level
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Level
d1 else if (Level
d2 Level -> Level -> Bool
forall a. Ord a => a -> a -> Bool
< Level
lvl) then Level -> ST s Level
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Level
d2 else MutablePrimArray s Lit -> Int -> Int -> ST s Level
go MutablePrimArray s Lit
lits Int
n (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
                else do
                    TRACING(traceM $ ">>> decuced skip" ++ show (l, c))
                    MutablePrimArray s Lit -> Int -> Int -> ST s Level
go MutablePrimArray s Lit
lits Int
n (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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

    Int
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
    Int -> ST s Bool
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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
            Lit
l <- Trail s -> Int -> ST s Lit
forall s. Trail s -> Int -> ST s Lit
indexTrail Trail s
trail Int
i
            Level
dlvl <- Levels s -> Lit -> ST s Level
forall s. Levels s -> Lit -> ST s Level
getLevel Levels s
levels Lit
l
            if Level
dlvl Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
== Level
zeroLevel
            then Int -> ST s Bool
done (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
            else do
                Self s -> Lit -> ST s ()
forall s. Self s -> Lit -> ST s ()
unsetLiteral Self s
self Lit
l
                Int -> ST s Bool
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        | Bool
otherwise = Int -> ST s Bool
done Int
0

    done :: Int -> ST s Bool
    done :: Int -> ST s Bool
done Int
i = do
        Int
conflictSize <- LitSet s -> ST s Int
forall s. LitSet s -> ST s Int
sizeofLitSet LitSet s
sandbox
        Lit
u <- case Int
conflictSize of
            Int
1 -> LitSet s -> ST s Lit
forall s. LitSet s -> ST s Lit
unsingletonLitSet LitSet s
sandbox
            Int
_ -> do
                Clause2
conflictCause <- LitSet s -> ST s Clause2
forall s. LitSet s -> ST s Clause2
litSetToClause LitSet s
sandbox
                PartialAssignment s
-> Clause2 -> (Satisfied_ -> ST s Lit) -> ST s Lit
forall s r.
PartialAssignment s -> Clause2 -> (Satisfied_ -> ST s r) -> ST s r
satisfied2_ PartialAssignment s
pa Clause2
conflictCause ((Satisfied_ -> ST s Lit) -> ST s Lit)
-> (Satisfied_ -> ST s Lit) -> ST s Lit
forall a b. (a -> b) -> a -> b
$ \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)

        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
        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
1)
        Self s -> Lit -> Level -> Clause2 -> ST s ()
forall s. Self s -> Lit -> Level -> Clause2 -> ST s ()
enqueue Self s
self Lit
u Level
zeroLevel Clause2
nullClause

        Bool
res <- ClauseDB s
-> PrimVar s Int
-> Trail s
-> Levels s
-> PartialAssignment s
-> VarSet s
-> Lit
-> ST s Bool
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
u
        if Bool
res
        then Self s -> ST s Bool
forall s. Self s -> ST s Bool
solveLoop Self s
self
        else Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
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
    Int
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
    PrimVar s Int -> Int -> ST s Bool
go PrimVar s Int
sizeVar (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  where
    go :: PrimVar s Int -> Int -> ST s Bool
go PrimVar s Int
sizeVar Int
i = do
        Lit
l <- Trail s -> Int -> ST s Lit
forall s. Trail s -> Int -> ST s Lit
indexTrail Trail s
trail Int
i
        Level
dlvl <- Levels s -> Lit -> ST s Level
forall s. Levels s -> Lit -> ST s Level
getLevel Levels s
levels Lit
l

        if Level
dlvl Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
== Level
conflictLevel
        then do
            TRACING(traceM $ ">>> JUMP: " ++ show (i, l, dlvl, conflictLevel))
            Int
conflictSize <- LitSet s -> ST s Int
forall s. LitSet s -> ST s Int
sizeofLitSet LitSet s
sandbox
            ASSERTING(assertST "conflict size >= 2" $ conflictSize >= 2)

            Clause2
conflictClause <- LitSet s -> ST s Clause2
forall s. LitSet s -> ST s Clause2
litSetToClause LitSet s
sandbox
            TRACING(traceM $ "JUMPED: " ++ show (i, l, dlvl, conflictLevel, conflictClause))

            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
conflictClause ((Satisfied_ -> ST s Bool) -> ST s Bool)
-> (Satisfied_ -> ST s Bool) -> ST s Bool
forall a b. (a -> b) -> a -> b
$ \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))
            Self s -> Lit -> ST s ()
forall s. Self s -> Lit -> ST s ()
unsetLiteral Self s
self Lit
l
            PrimVar s Int -> Int -> ST s Bool
go PrimVar s Int
sizeVar (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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)
    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
    Int
conflictSize <- LitSet s -> ST s Int
forall s. LitSet s -> ST s Int
sizeofLitSet LitSet s
sandbox
    Bool -> ST s () -> ST s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
conflictSize Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ do
        Clause2
conflictClause <- LitSet s -> ST s Clause2
forall s. LitSet s -> ST s Clause2
litSetToClause LitSet s
sandbox
        Stats s -> ST s ()
forall s. Stats s -> ST s ()
incrStatsLearnt Stats s
stats
        Stats s -> Int -> ST s ()
forall s. Stats s -> Int -> ST s ()
incrStatsLearntLiterals Stats s
stats Int
conflictSize

        case Clause2
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
    Self s -> ST s ()
forall s. Self s -> ST s ()
boostSandbox Self s
self

    if Level
clvl Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Level
Level Int
0
    then Self s -> ST s Bool
forall s. Self s -> ST s Bool
backjump0 Self s
self
    else Self s -> Level -> ST s Bool
forall s. Self s -> Level -> ST s Bool
backjump Self s
self Level
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
    Int
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
    Int
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
qhead

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

    if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n
    then do
        -- traceM $ "i < n: " ++ show (i, n)
        -- traceTrail reasons levels trail
        Lit
l <- Trail s -> Int -> ST s Lit
forall s. Trail s -> Int -> ST s Lit
indexTrail Trail s
trail Int
i

        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
1)
        ClauseDB s
-> PrimVar s Int
-> Trail s
-> Levels s
-> PartialAssignment s
-> VarSet s
-> Lit
-> ST s Bool
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

    else Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
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
    Vec s Watch
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
    Int
size <- Vec s Watch -> ST s Int
forall s a. Vec s a -> ST s Int
sizeofVec Vec s Watch
watches
    TRACING(traceM ("initialUnitPropagate watches: " ++ show size))
    Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches Int
0 Int
0 Int
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
    Int
n <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
nextLit
    Int -> ST s Int
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Int -> Int
forall a. Bits a => a -> Int -> a
unsafeShiftR Int
n Int
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
    PartialAssignment s
pa <- STRef s (PartialAssignment s) -> ST s (PartialAssignment s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (PartialAssignment s)
prevPA
    Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l PartialAssignment s
pa ST s LBool -> (LBool -> Bool) -> ST s Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
        LBool
LUndef -> Bool
False
        LBool
LTrue  -> Bool
True
        LBool
LFalse -> Bool
False