{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE NoFieldSelectors #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE RecordWildCards #-}
module PureSAT.Main (
Solver,
newSolver,
Lit (..),
newLit,
boostScore,
neg,
addClause,
solve,
simplify,
modelValue,
num_vars,
num_clauses,
num_learnts,
num_learnt_literals,
num_conflicts,
num_restarts,
) where
#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
#ifdef TWO_WATCHED_LITERALS
newtype ClauseDB s = CDB (LitTable s (Vec s Watch))
data Watch = W !Lit !Clause2
newClauseDB :: Int -> ST s (ClauseDB s)
newClauseDB :: forall s. Int -> ST s (ClauseDB s)
newClauseDB !Int
size' = do
let size :: Int
size = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
size' Int
40960
arr <- Int -> Vec s Watch -> ST s (LitTable s (Vec s Watch))
forall a s. Int -> a -> ST s (LitTable s a)
newLitTable Int
size Vec s Watch
forall a. HasCallStack => a
undefined
forM_ [0 .. size - 1] $ \Int
i -> do
vec <- Int -> ST s (Vec s Watch)
forall s a. Int -> ST s (Vec s a)
newVec Int
16
writeLitTable arr (MkLit i) vec
return (CDB arr)
extendClauseDB :: ClauseDB s -> Int -> ST s (ClauseDB s)
extendClauseDB :: forall s. ClauseDB s -> Int -> ST s (ClauseDB s)
extendClauseDB cdb :: ClauseDB s
cdb@(CDB LitTable s (Vec s Watch)
old) Int
newSize' = do
oldSize <- LitTable s (Vec s Watch) -> ST s Int
forall s a. LitTable s a -> ST s Int
sizeofLitTable LitTable s (Vec s Watch)
old
let newSize = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
newSize' Int
4096
if newSize <= oldSize
then return cdb
else do
traceM $ "resize" ++ show newSize
new <- newLitTable newSize undefined
forM_ [0 .. newSize - 1] $ \Int
i -> do
if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
oldSize
then do
x <- LitTable s (Vec s Watch) -> Lit -> ST s (Vec s Watch)
forall s a. LitTable s a -> Lit -> ST s a
readLitTable LitTable s (Vec s Watch)
old (Int -> Lit
MkLit Int
i)
writeLitTable new (MkLit i) x
else do
vec <- Int -> ST s (Vec s Watch)
forall s a. Int -> ST s (Vec s a)
newVec Int
16
writeLitTable new (MkLit i) vec
return (CDB new)
insertClauseDB :: Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
insertClauseDB :: forall s. Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
insertClauseDB !Lit
l1 !Lit
l2 !Clause2
clause !ClauseDB s
cdb = do
ASSERTING(assertST "l1" (litInClause l1 clause))
ASSERTING(assertST "l2" (litInClause l2 clause))
Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l1 (Lit -> Clause2 -> Watch
W Lit
l2 Clause2
clause) ClauseDB s
cdb
Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l2 (Lit -> Clause2 -> Watch
W Lit
l1 Clause2
clause) ClauseDB s
cdb
insertWatch :: Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch :: forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch !Lit
l !Watch
w (CDB LitTable s (Vec s Watch)
cdb) = do
ws <- LitTable s (Vec s Watch) -> Lit -> ST s (Vec s Watch)
forall s a. LitTable s a -> Lit -> ST s a
readLitTable LitTable s (Vec s Watch)
cdb Lit
l
ws' <- insertVec ws w
writeLitTable cdb l ws'
lookupClauseDB :: Lit -> ClauseDB s -> ST s (Vec s Watch)
lookupClauseDB :: forall s. Lit -> ClauseDB s -> ST s (Vec s Watch)
lookupClauseDB !Lit
l (CDB LitTable s (Vec s Watch)
arr) = do
LitTable s (Vec s Watch) -> Lit -> ST s (Vec s Watch)
forall s a. LitTable s a -> Lit -> ST s a
readLitTable LitTable s (Vec s Watch)
arr Lit
l
clearClauseDB :: ClauseDB s -> Lit -> ST s ()
clearClauseDB :: forall s. ClauseDB s -> Lit -> ST s ()
clearClauseDB (CDB LitTable s (Vec s Watch)
cdb) Lit
l = do
v <- Int -> ST s (Vec s Watch)
forall s a. Int -> ST s (Vec s a)
newVec Int
0
writeLitTable cdb l v
#else
type ClauseDB s = [Clause2]
insertClauseDB :: Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
insertClauseDB _ _ _ _ = return ()
#endif
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
#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
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)
, 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)
}
newSolver :: ST s (Solver s)
newSolver :: forall s. ST s (Solver s)
newSolver = do
ok <- Bool -> ST s (STRef s Bool)
forall a s. a -> ST s (STRef s a)
newSTRef Bool
True
nextLit <- newSTRef 0
statistics <- newStats
zeroLevels <- newLevels 1024 >>= newSTRef
zeroVars <- newVarSet >>= newSTRef
zeroPA <- newPartialAssignment 1024 >>= newSTRef
zeroHead <- newPrimVar 0
zeroTrail <- newTrail 1024 >>= newSTRef
prevPA <- newPartialAssignment 1024 >>= newSTRef
#ifdef TWO_WATCHED_LITERALS
clauses <- newClauseDB 0 >>= newSTRef
#else
clauses <- newSTRef []
#endif
lcg <- newLCG 44
return Solver {..}
newLit :: Solver s -> ST s Lit
newLit :: forall s. Solver s -> ST s Lit
newLit Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = do
l' <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
nextLit
let n = Int
l' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2
writeSTRef nextLit n
let l = Int -> Lit
MkLit Int
l'
TRACING(traceM $ "!!! newLit " ++ show l)
levels <- readSTRef zeroLevels
levels' <- extendLevels levels n
writeSTRef zeroLevels levels'
pa <- readSTRef zeroPA
pa' <- extendPartialAssignment pa
writeSTRef zeroPA pa'
trail <- readSTRef zeroTrail
trail' <- extendTrail trail n
writeSTRef zeroTrail trail'
vars <- readSTRef zeroVars
vars' <- extendVarSet n vars
writeSTRef zeroVars vars'
#ifdef TWO_WATCHED_LITERALS
clauseDB <- readSTRef clauses
clauseDB' <- extendClauseDB clauseDB n
writeSTRef clauses clauseDB'
#endif
insertVarSet (litToVar l) vars'
return l
boostScore :: Solver s -> Lit -> ST s ()
boostScore :: forall s. Solver s -> Lit -> ST s ()
boostScore Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} Lit
l = do
vars <- STRef s (VarSet s) -> ST s (VarSet s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (VarSet s)
zeroVars
weightVarSet (litToVar l) boost vars
addClause :: Solver s -> [Lit] -> ST s Bool
addClause :: forall s. Solver s -> Clause -> ST s Bool
addClause solver :: Solver s
solver@Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} Clause
clause = STRef s Bool -> ST s Bool -> ST s Bool
forall s. STRef s Bool -> ST s Bool -> ST s Bool
whenOk STRef s Bool
ok (ST s Bool -> ST s Bool) -> ST s Bool -> ST s Bool
forall a b. (a -> b) -> a -> b
$ do
pa <- STRef s (PartialAssignment s) -> ST s (PartialAssignment s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (PartialAssignment s)
zeroPA
s <- satisfied pa clause
case s of
Satisfied
Satisfied ->
Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Satisfied
Conflicting -> do
TRACING(traceM ">>> ADD CLAUSE conflict")
Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
unsat Solver s
solver
Unresolved !Clause2
c -> do
Stats s -> ST s ()
forall s. Stats s -> ST s ()
incrStatsClauses Stats s
statistics
clauseDB <- STRef s (ClauseDB s) -> ST s (ClauseDB s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (ClauseDB s)
clauses
#ifdef TWO_WATCHED_LITERALS
let MkClause2 _ l1 l2 _ = c
insertClauseDB l1 l2 c clauseDB
#else
writeSTRef clauses (c : clauseDB)
#endif
return True
Unit Lit
l -> do
TRACING(traceM $ "addClause unit: " ++ show l)
clauseDB <- STRef s (ClauseDB s) -> ST s (ClauseDB s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (ClauseDB s)
clauses
let qhead = PrimVar s Int
zeroHead
levels <- readSTRef zeroLevels
trail <- readSTRef zeroTrail
vars <- readSTRef zeroVars
initialEnqueue trail pa levels vars l
res <- initialLoop clauseDB qhead trail levels pa vars
if res
then return True
else unsat solver
unsat :: Solver s -> ST s Bool
unsat :: forall s. Solver s -> ST s Bool
unsat Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = do
STRef s Bool -> Bool -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Bool
ok Bool
False
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
data Self s = Self
{ forall s. Self s -> ClauseDB s
clauseDB :: !(ClauseDB s)
, forall s. Self s -> PrimVar s Level
level :: !(PrimVar s Level)
, forall s. Self s -> Levels s
levels :: !(Levels s)
, forall s. Self s -> PartialAssignment s
pa :: !(PartialAssignment s)
, forall s. Self s -> PartialAssignment s
prev :: !(PartialAssignment s)
, forall s. Self s -> PartialAssignment s
zero :: !(PartialAssignment s)
, forall s. Self s -> PrimVar s Int
qhead :: !(PrimVar s Int)
, forall s. Self s -> VarSet s
vars :: !(VarSet s)
, forall s. Self s -> LitTable s Clause2
reasons :: !(LitTable s Clause2)
, forall s. Self s -> LitSet s
sandbox :: !(LitSet s)
, forall s. Self s -> Trail s
trail :: {-# UNPACK #-} !(Trail s)
, forall s. Self s -> Stats s
stats :: !(Stats s)
}
assertSelfInvariants :: Self s -> ST s ()
assertSelfInvariants :: forall s. Self s -> ST s ()
assertSelfInvariants Self s
_ = () -> ST s ()
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
solve :: Solver s -> ST s Bool
solve :: forall s. Solver s -> ST s Bool
solve solver :: Solver s
solver@Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = ST s Bool -> ST s Bool -> ST s Bool
forall s. ST s Bool -> ST s Bool -> ST s Bool
whenOk_ (Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
simplify Solver s
solver) (ST s Bool -> ST s Bool) -> ST s Bool -> ST s Bool
forall a b. (a -> b) -> a -> b
$ do
clauseDB <- STRef s (ClauseDB s) -> ST s (ClauseDB s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (ClauseDB s)
clauses
litCount <- readSTRef nextLit
level <- newPrimVar (Level 0)
sandbox <- newLitSet litCount
reasons <- newLitTable litCount nullClause
zero <- readSTRef zeroPA
levels <- readSTRef zeroLevels
qhead <- readPrimVar zeroHead >>= newPrimVar
vars <- readSTRef zeroVars >>= cloneVarSet
pa <- readSTRef zeroPA >>= clonePartialAssignment
trail <- readSTRef zeroTrail >>= cloneTrail
prev <- newPartialAssignment litCount
let stats = Stats s
statistics
TRACING(sizeofVarSet vars >>= \n -> traceM $ "vars to solve " ++ show n)
TRACING(tracePartialAssignment pa)
let self = Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
sandbox :: LitSet s
reasons :: LitTable s Clause2
zero :: PartialAssignment s
levels :: Levels s
qhead :: PrimVar s Int
vars :: VarSet s
pa :: PartialAssignment s
trail :: Trail s
prev :: PartialAssignment s
stats :: Stats s
..}
solveLoop self >>= \case
Bool
False -> Solver s -> ST s Bool
forall s. Solver s -> ST s Bool
unsat Solver s
solver
Bool
True -> do
STRef s (PartialAssignment s) -> PartialAssignment s -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s (PartialAssignment s)
prevPA PartialAssignment s
pa
Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
initialEnqueue :: Trail s -> PartialAssignment s -> Levels s -> VarSet s -> Lit -> ST s ()
initialEnqueue :: forall s.
Trail s
-> PartialAssignment s -> Levels s -> VarSet s -> Lit -> ST s ()
initialEnqueue Trail s
trail PartialAssignment s
pa Levels s
levels VarSet s
vars Lit
l = do
Lit -> PartialAssignment s -> ST s ()
forall s. Lit -> PartialAssignment s -> ST s ()
insertPartialAssignment Lit
l PartialAssignment s
pa
Var -> VarSet s -> ST s ()
forall s. Var -> VarSet s -> ST s ()
deleteVarSet (Lit -> Var
litToVar Lit
l) VarSet s
vars
Levels s -> Lit -> Level -> ST s ()
forall s. Levels s -> Lit -> Level -> ST s ()
setLevel Levels s
levels Lit
l Level
zeroLevel
Lit -> Trail s -> ST s ()
forall s. Lit -> Trail s -> ST s ()
pushTrail Lit
l Trail s
trail
enqueue :: Self s -> Lit -> Level -> Clause2 -> ST s ()
enqueue :: forall s. Self s -> Lit -> Level -> Clause2 -> ST s ()
enqueue Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} Lit
l Level
d Clause2
c = do
TRACING(traceM $ "enqueue " ++ show (l, d, c))
ASSERTING(assertLiteralUndef l pa)
ASSERTING(assertST "enqueue reason" (isNullClause c || litInClause l c))
Lit -> PartialAssignment s -> ST s ()
forall s. Lit -> PartialAssignment s -> ST s ()
insertPartialAssignment Lit
l PartialAssignment s
pa
Var -> VarSet s -> ST s ()
forall s. Var -> VarSet s -> ST s ()
deleteVarSet (Lit -> Var
litToVar Lit
l) VarSet s
vars
Lit -> Trail s -> ST s ()
forall s. Lit -> Trail s -> ST s ()
pushTrail Lit
l Trail s
trail
Levels s -> Lit -> Level -> ST s ()
forall s. Levels s -> Lit -> Level -> ST s ()
setLevel Levels s
levels Lit
l Level
d
LitTable s Clause2 -> Lit -> Clause2 -> ST s ()
forall s a. LitTable s a -> Lit -> a -> ST s ()
writeLitTable LitTable s Clause2
reasons Lit
l Clause2
c
unsetLiteral :: Self s -> Lit -> ST s ()
unsetLiteral :: forall s. Self s -> Lit -> ST s ()
unsetLiteral Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} Lit
l = do
Lit -> PartialAssignment s -> ST s ()
forall s. Lit -> PartialAssignment s -> ST s ()
deletePartialAssignment Lit
l PartialAssignment s
pa
Var -> VarSet s -> ST s ()
forall s. Var -> VarSet s -> ST s ()
insertVarSet (Lit -> Var
litToVar Lit
l) VarSet s
vars
boostSandbox :: Self s -> ST s ()
boostSandbox :: forall s. Self s -> ST s ()
boostSandbox Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} = do
n <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
size
go 0 n
where
LS SS {PrimVar s Int
MutablePrimArray s Int
size :: PrimVar s Int
dense :: MutablePrimArray s Int
sparse :: MutablePrimArray s Int
sparse :: forall s. SparseSet s -> MutablePrimArray s Int
dense :: forall s. SparseSet s -> MutablePrimArray s Int
size :: forall s. SparseSet s -> PrimVar s Int
..} = LitSet s
sandbox
go :: Int -> Int -> ST s ()
go !Int
i !Int
n = Bool -> ST s () -> ST s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ do
l <- MutablePrimArray s Int -> Int -> ST s Int
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> ST s a
readPrimArray MutablePrimArray s Int
dense Int
i
weightVarSet (litToVar (MkLit l)) boost vars
go (i + 1) n
solveLoop :: forall s. Self s -> ST s Bool
solveLoop :: forall s. Self s -> ST s Bool
solveLoop self :: Self s
self@Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} = do
let Trail PrimVar s Int
sizeVar MutablePrimArray s Lit
_ = Trail s
trail
n <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
sizeVar
i <- readPrimVar qhead
TRACING(traceM $ "!!! SOLVE: " ++ show (i, n))
TRACING(tracePartialAssignment zero)
TRACING(tracePartialAssignment pa)
TRACING(traceTrail reasons levels trail)
if i < n
then do
l <- indexTrail trail i
writePrimVar qhead (i + 1)
unitPropagate self l
else
noUnit
where
noUnit :: ST s Bool
noUnit :: ST s Bool
noUnit = VarSet s -> ST s Bool -> (Var -> ST s Bool) -> ST s Bool
forall s r. VarSet s -> ST s r -> (Var -> ST s r) -> ST s r
minViewVarSet VarSet s
vars ST s Bool
noVar Var -> ST s Bool
yesVar
noVar :: ST s Bool
noVar :: ST s Bool
noVar = do
TRACING(traceM ">>> SOLVE: SAT")
Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
yesVar :: Var -> ST s Bool
yesVar :: Var -> ST s Bool
yesVar !Var
v = do
TRACING(traceM $ ">>> SOLVE: deciding variable " ++ show v)
lvl <- PrimVar (PrimState (ST s)) Level -> ST s Level
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level
let !lvl' = Level -> Level
forall a. Enum a => a -> a
succ Level
lvl
writePrimVar level lvl'
l' <- lookupPartialAssignment l prev <&> \case
LBool
LTrue -> Lit -> Lit
neg Lit
l
LBool
LFalse -> Lit
l
LBool
LUndef -> Lit
l
enqueue self l' lvl' nullClause
modifyPrimVar qhead $ \Int
i -> Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
unitPropagate self l'
where
!l :: Lit
l = Var -> Lit
varToLit Var
v
unitPropagate :: forall s. Self s -> Lit -> ST s Bool
#ifdef TWO_WATCHED_LITERALS
unitPropagate :: forall s. Self s -> Lit -> ST s Bool
unitPropagate self :: Self s
self@Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} !Lit
l = do
TRACING(traceM ("!!! PROPAGATE " ++ show l))
ASSERTING(let Trail sizeVar trailLits = trail)
ASSERTING(n <- readPrimVar sizeVar)
ASSERTING(assertST "trail not empty" $ n > 0)
ASSERTING(q <- readPrimVar qhead)
ASSERTING(assertST "qhead" $ q <= n)
TRACING(traceM $ show q)
ASSERTING(ll <- indexTrail trail (q - 1))
ASSERTING(assertST "end of the trail is the var we propagate" $ l == ll)
watches <- Lit -> ClauseDB s -> ST s (Vec s Watch)
forall s. Lit -> ClauseDB s -> ST s (Vec s Watch)
lookupClauseDB (Lit -> Lit
neg Lit
l) ClauseDB s
clauseDB
size <- sizeofVec watches
go watches 0 0 size
where
go :: Vec s Watch -> Int -> Int -> Int -> ST s Bool
go :: Vec s Watch -> Int -> Int -> Int -> ST s Bool
go !Vec s Watch
watches !Int
i !Int
j !Int
size
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
size
= do
Vec s Watch -> Int -> ST s ()
forall s a. Vec s a -> Int -> ST s ()
shrinkVec Vec s Watch
watches Int
j
Self s -> ST s Bool
forall s. Self s -> ST s Bool
solveLoop Self s
self
| Bool
otherwise
= Vec s Watch -> Int -> ST s Watch
forall s a. Vec s a -> Int -> ST s a
readVec Vec s Watch
watches Int
i ST s Watch -> (Watch -> ST s Bool) -> ST s Bool
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ w :: Watch
w@(W Lit
l' Clause2
c) -> do
let onConflict :: ST s Bool
{-# INLINE onConflict #-}
onConflict :: ST s Bool
onConflict = do
Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w
Vec s Watch -> Int -> Int -> Int -> ST s ()
forall s. Vec s Watch -> Int -> Int -> Int -> ST s ()
copyWatches Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size
Self s -> Clause2 -> ST s Bool
forall s. Self s -> Clause2 -> ST s Bool
backtrack Self s
self Clause2
c
onSatisfied :: ST s Bool
{-# INLINE onSatisfied #-}
onSatisfied :: ST s Bool
onSatisfied = do
Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w
Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size
onUnit :: Lit -> ST s Bool
{-# INLINE onUnit #-}
onUnit :: Lit -> ST s Bool
onUnit Lit
u = do
Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w
lvl <- PrimVar (PrimState (ST s)) Level -> ST s Level
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level
enqueue self u lvl c
go watches (i + 1) (j + 1) size
if Clause2 -> Bool
isBinaryClause2 Clause2
c
then Lit -> PartialAssignment s -> ST s LBool
forall s. Lit -> PartialAssignment s -> ST s LBool
lookupPartialAssignment Lit
l' PartialAssignment s
pa ST s LBool -> (LBool -> ST s Bool) -> ST s Bool
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
LBool
LUndef -> Lit -> ST s Bool
onUnit Lit
l'
LBool
LTrue -> ST s Bool
onSatisfied
LBool
LFalse -> ST s Bool
onConflict
else do
let kontUnitPropagate :: Satisfied_ -> ST s Bool
kontUnitPropagate = \case
Satisfied_
Conflicting_ -> ST s Bool
onConflict
Satisfied_
Satisfied_ -> ST s Bool
onSatisfied
Unit_ Lit
u -> Lit -> ST s Bool
onUnit Lit
u
Unresolved_ Lit
l1 Lit
l2
| Lit
l2 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l', Lit
l2 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l
-> do
Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l2 Watch
w ClauseDB s
clauseDB
Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
j Int
size
| Lit
l1 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l', Lit
l1 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l
-> do
Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l1 Watch
w ClauseDB s
clauseDB
Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
j Int
size
| Bool
otherwise
-> String -> ST s Bool
forall a. HasCallStack => String -> a
error (String
"watch" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Lit, Lit, Lit, Lit) -> String
forall a. Show a => a -> String
show (Lit
l, Lit
l1, Lit
l2, Lit
l'))
{-# INLINE [1] kontUnitPropagate #-}
PartialAssignment s
-> Clause2 -> (Satisfied_ -> ST s Bool) -> ST s Bool
forall s r.
PartialAssignment s -> Clause2 -> (Satisfied_ -> ST s r) -> ST s r
satisfied2_ PartialAssignment s
pa Clause2
c Satisfied_ -> ST s Bool
kontUnitPropagate
copyWatches :: Vec s Watch -> Int -> Int -> Int -> ST s ()
copyWatches :: forall s. Vec s Watch -> Int -> Int -> Int -> ST s ()
copyWatches Vec s Watch
watches Int
i Int
j Int
size = do
if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
size
then do
w' <- Vec s Watch -> Int -> ST s Watch
forall s a. Vec s a -> Int -> ST s a
readVec Vec s Watch
watches Int
i
writeVec watches j w'
copyWatches watches (i + 1) (j + 1) size
else Vec s Watch -> Int -> ST s ()
forall s a. Vec s a -> Int -> ST s ()
shrinkVec Vec s Watch
watches Int
j
#else
unitPropagate self@Self {..} _l = go clauseDB
where
go :: [Clause2] -> ST s Bool
go [] = solveLoop self
go (c:cs) = satisfied2_ pa c $ \case
Conflicting_ -> backtrack self c
Satisfied_ -> go cs
Unit_ u -> do
lvl <- readPrimVar level
enqueue self u lvl c
go cs
Unresolved_ _ _ -> go cs
#endif
traceCause :: LitSet s -> ST s ()
traceCause :: forall s. LitSet s -> ST s ()
traceCause LitSet s
sandbox = do
xs <- LitSet s -> ST s Clause
forall s. LitSet s -> ST s Clause
elemsLitSet LitSet s
sandbox
traceM $ "current cause " ++ show xs
withTwoLargestLevels :: LitSet s -> Int -> Levels s -> (Level -> Level -> ST s r) -> ST s r
withTwoLargestLevels :: forall s r.
LitSet s -> Int -> Levels s -> (Level -> Level -> ST s r) -> ST s r
withTwoLargestLevels !LitSet s
sandbox !Int
conflictSize !Levels s
levels Level -> Level -> ST s r
kont =
Level -> Level -> Int -> ST s r
go Level
zeroLevel Level
zeroLevel Int
0
where
go :: Level -> Level -> Int -> ST s r
go Level
d1 Level
d2 Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
conflictSize = Level -> Level -> ST s r
kont Level
d1 Level
d2
| Bool
otherwise = do
d <- LitSet s -> Int -> ST s Lit
forall s. LitSet s -> Int -> ST s Lit
indexLitSet LitSet s
sandbox Int
i ST s Lit -> (Lit -> ST s Level) -> ST s Level
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Levels s -> Lit -> ST s Level
forall s. Levels s -> Lit -> ST s Level
getLevel Levels s
levels
if d > d2 then go d2 d (i + 1)
else if d > d1 then go d d2 (i + 1)
else go d1 d2 (i + 1)
analyse :: forall s. Self s -> Clause2 -> ST s Level
analyse :: forall s. Self s -> Clause2 -> ST s Level
analyse Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} !Clause2
cause = do
TRACING(traceM $ "!!! ANALYSE: " ++ show cause)
let Trail PrimVar s Int
size MutablePrimArray s Lit
lits = Trail s
trail
n <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
size
clearLitSet sandbox
forLitInClause2_ cause insertSandbox
conflictSize <- sizeofLitSet sandbox
withTwoLargestLevels sandbox conflictSize levels $ \Level
d1 Level
d2 -> do
lvl <- PrimVar (PrimState (ST s)) Level -> ST s Level
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level
if (d1 < lvl) then return d1 else if (d2 < lvl) then return d2 else go lits n (n - 1)
where
insertSandbox :: Lit -> ST s ()
insertSandbox !Lit
l = Lit -> LitSet s -> ST s ()
forall s. Lit -> LitSet s -> ST s ()
insertLitSet Lit
l LitSet s
sandbox
{-# INLINE insertSandbox #-}
go :: MutablePrimArray s Lit -> Int -> Int -> ST s Level
go :: MutablePrimArray s Lit -> Int -> Int -> ST s Level
go !MutablePrimArray s Lit
lits !Int
n !Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = do
l <- MutablePrimArray s Lit -> Int -> ST s Lit
forall a s.
(HasCallStack, Prim a) =>
MutablePrimArray s a -> Int -> ST s a
readPrimArray MutablePrimArray s Lit
lits Int
i
c <- readLitTable reasons l
if isNullClause c
then do
TRACING(traceM $ ">>> decided " ++ show (l, c))
b <- memberLitSet sandbox (neg l)
if b
then do
TRACING(traceM $ ">>> decided stop: " ++ show (l, c))
tracePartialAssignment zero
traceCause sandbox
traceTrail reasons levels trail
error $ "decision variable" ++ show (b, n, i, l, c, cause)
else do
TRACING(traceM $ ">>> decided skip: " ++ show (l, c))
go lits n (i - 1)
else do
b <- memberLitSet sandbox (neg l)
if b
then do
TRACING(traceM $ ">>> deduced undo" ++ show (l, c))
TRACING(traceCause sandbox)
ASSERTING(assertST "literal in reason clause" $ litInClause l c)
forLitInClause2_ c insertSandbox
deleteLitSet l sandbox
deleteLitSet (neg l) sandbox
TRACING(traceCause sandbox)
conflictSize <- sizeofLitSet sandbox
withTwoLargestLevels sandbox conflictSize levels $ \Level
d1 Level
d2 -> do
lvl <- PrimVar (PrimState (ST s)) Level -> ST s Level
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level
if (d1 < lvl) then return d1 else if (d2 < lvl) then return d2 else go lits n (i - 1)
else do
TRACING(traceM $ ">>> decuced skip" ++ show (l, c))
go lits n (i - 1)
| Bool
otherwise
= String -> Bool -> ST s ()
forall s. HasCallStack => String -> Bool -> ST s ()
assertST String
"reached end of trail" Bool
False ST s () -> ST s Level -> ST s Level
forall a b. ST s a -> ST s b -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> ST s Level
forall a. HasCallStack => String -> a
error String
"-"
backjump0 :: forall s. Self s -> ST s Bool
backjump0 :: forall s. Self s -> ST s Bool
backjump0 self :: Self s
self@Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} = do
TRACING(traceM $ "!!! BACKJUMP0")
TRACING(traceCause sandbox)
TRACING(traceTrail reasons levels trail)
ASSERTING(assertSelfInvariants self)
Stats s -> ST s ()
forall s. Stats s -> ST s ()
incrStatsRestarts Stats s
stats
PrimVar (PrimState (ST s)) Level -> Level -> ST s ()
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> a -> m ()
writePrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level Level
zeroLevel
i <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
sizeVar
go (i - 1)
where
Trail PrimVar s Int
sizeVar MutablePrimArray s Lit
_ = Trail s
trail
go :: Int -> ST s Bool
go :: Int -> ST s Bool
go Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = do
l <- Trail s -> Int -> ST s Lit
forall s. Trail s -> Int -> ST s Lit
indexTrail Trail s
trail Int
i
dlvl <- getLevel levels l
if dlvl == zeroLevel
then done (i + 1)
else do
unsetLiteral self l
go (i - 1)
| Bool
otherwise = Int -> ST s Bool
done Int
0
done :: Int -> ST s Bool
done :: Int -> ST s Bool
done Int
i = do
conflictSize <- LitSet s -> ST s Int
forall s. LitSet s -> ST s Int
sizeofLitSet LitSet s
sandbox
u <- case conflictSize of
Int
1 -> LitSet s -> ST s Lit
forall s. LitSet s -> ST s Lit
unsingletonLitSet LitSet s
sandbox
Int
_ -> do
conflictCause <- LitSet s -> ST s Clause2
forall s. LitSet s -> ST s Clause2
litSetToClause LitSet s
sandbox
satisfied2_ pa conflictCause $ \case
Unit_ Lit
l' -> Lit -> ST s Lit
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Lit
l'
Satisfied_
x -> String -> ST s Lit
forall a. HasCallStack => String -> a
error (String -> ST s Lit) -> String -> ST s Lit
forall a b. (a -> b) -> a -> b
$ String
"TODO " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Satisfied_) -> String
forall a. Show a => a -> String
show (Int
conflictSize, Satisfied_
x)
writePrimVar sizeVar i
writePrimVar qhead (i + 1)
enqueue self u zeroLevel nullClause
res <- initialUnitPropagate clauseDB qhead trail levels pa vars u
if res
then solveLoop self
else return False
backjump :: forall s. Self s -> Level -> ST s Bool
backjump :: forall s. Self s -> Level -> ST s Bool
backjump self :: Self s
self@Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} Level
conflictLevel = do
TRACING(traceM $ "!!! BACKJUMP: " ++ show conflictLevel)
TRACING(traceCause sandbox)
TRACING(traceTrail reasons levels trail)
ASSERTING(assertST "backump level > 0" $ conflictLevel > zeroLevel)
PrimVar (PrimState (ST s)) Level -> Level -> ST s ()
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> a -> m ()
writePrimVar PrimVar s Level
PrimVar (PrimState (ST s)) Level
level Level
conflictLevel
let Trail PrimVar s Int
sizeVar MutablePrimArray s Lit
_ = Trail s
trail
i <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
sizeVar
go sizeVar (i - 1)
where
go :: PrimVar s Int -> Int -> ST s Bool
go PrimVar s Int
sizeVar Int
i = do
l <- Trail s -> Int -> ST s Lit
forall s. Trail s -> Int -> ST s Lit
indexTrail Trail s
trail Int
i
dlvl <- getLevel levels l
if dlvl == conflictLevel
then do
TRACING(traceM $ ">>> JUMP: " ++ show (i, l, dlvl, conflictLevel))
conflictSize <- sizeofLitSet sandbox
ASSERTING(assertST "conflict size >= 2" $ conflictSize >= 2)
conflictClause <- litSetToClause sandbox
TRACING(traceM $ "JUMPED: " ++ show (i, l, dlvl, conflictLevel, conflictClause))
satisfied2_ pa conflictClause $ \case
Unit_ Lit
u -> do
PrimVar (PrimState (ST s)) Int -> Int -> ST s ()
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> a -> m ()
writePrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
sizeVar (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
PrimVar (PrimState (ST s)) Int -> Int -> ST s ()
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> a -> m ()
writePrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
qhead (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2)
Self s -> Lit -> Level -> Clause2 -> ST s ()
forall s. Self s -> Lit -> Level -> Clause2 -> ST s ()
enqueue Self s
self Lit
u Level
dlvl Clause2
conflictClause
TRACING(traceM $ ">>> JUMPED: " ++ show (i, l, dlvl, conflictLevel, conflictClause, u))
TRACING(tracePartialAssignment pa)
TRACING(traceTrail reasons levels trail)
Self s -> Lit -> ST s Bool
forall s. Self s -> Lit -> ST s Bool
unitPropagate Self s
self Lit
u
Satisfied_
x -> String -> ST s Bool
forall a. HasCallStack => String -> a
error (String -> ST s Bool) -> String -> ST s Bool
forall a b. (a -> b) -> a -> b
$ String
"TODO _" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Satisfied_) -> String
forall a. Show a => a -> String
show (Int
conflictSize, Satisfied_
x)
else do
TRACING(traceM $ ">>> UNDO: " ++ show (i, l, dlvl))
unsetLiteral self l
go sizeVar (i - 1)
backtrack :: forall s. Self s -> Clause2 -> ST s Bool
backtrack :: forall s. Self s -> Clause2 -> ST s Bool
backtrack self :: Self s
self@Self {PrimVar s Int
PrimVar s Level
PartialAssignment s
LitTable s Clause2
LitSet s
Stats s
Levels s
Trail s
VarSet s
ClauseDB s
clauseDB :: forall s. Self s -> ClauseDB s
level :: forall s. Self s -> PrimVar s Level
levels :: forall s. Self s -> Levels s
pa :: forall s. Self s -> PartialAssignment s
prev :: forall s. Self s -> PartialAssignment s
zero :: forall s. Self s -> PartialAssignment s
qhead :: forall s. Self s -> PrimVar s Int
vars :: forall s. Self s -> VarSet s
reasons :: forall s. Self s -> LitTable s Clause2
sandbox :: forall s. Self s -> LitSet s
trail :: forall s. Self s -> Trail s
stats :: forall s. Self s -> Stats s
clauseDB :: ClauseDB s
level :: PrimVar s Level
levels :: Levels s
pa :: PartialAssignment s
prev :: PartialAssignment s
zero :: PartialAssignment s
qhead :: PrimVar s Int
vars :: VarSet s
reasons :: LitTable s Clause2
sandbox :: LitSet s
trail :: Trail s
stats :: Stats s
..} !Clause2
cause = do
TRACING(traceM $ "!!! CONFLICT " ++ show cause)
TRACING(tracePartialAssignment pa)
TRACING(traceTrail reasons levels trail)
Stats s -> ST s ()
forall s. Stats s -> ST s ()
incrStatsConflicts Stats s
stats
VarSet s -> (Word -> Word) -> ST s ()
forall s. VarSet s -> (Word -> Word) -> ST s ()
scaleVarSet VarSet s
vars Word -> Word
decay
TRACING(lvl <- readPrimVar level)
clvl <- Self s -> Clause2 -> ST s Level
forall s. Self s -> Clause2 -> ST s Level
analyse Self s
self Clause2
cause
TRACING(traceM $ ">>> analysed " ++ show (lvl, clvl, cause))
TRACING(traceCause sandbox)
conflictSize <- sizeofLitSet sandbox
when (conflictSize == 2) $ do
conflictClause <- litSetToClause sandbox
incrStatsLearnt stats
incrStatsLearntLiterals stats conflictSize
case conflictClause of
MkClause2 Bool
_ Lit
l1 Lit
l2 PrimArray Lit
_ -> Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
forall s. Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
insertClauseDB Lit
l1 Lit
l2 Clause2
conflictClause ClauseDB s
clauseDB
boostSandbox self
if clvl == Level 0
then backjump0 self
else backjump self clvl
initialLoop :: forall s. ClauseDB s -> PrimVar s Int -> Trail s -> Levels s -> PartialAssignment s -> VarSet s -> ST s Bool
initialLoop :: forall s.
ClauseDB s
-> PrimVar s Int
-> Trail s
-> Levels s
-> PartialAssignment s
-> VarSet s
-> ST s Bool
initialLoop !ClauseDB s
clauseDB !PrimVar s Int
qhead !Trail s
trail !Levels s
levels !PartialAssignment s
pa !VarSet s
vars = do
let Trail PrimVar s Int
sizeVar MutablePrimArray s Lit
_ = Trail s
trail
n <- PrimVar (PrimState (ST s)) Int -> ST s Int
forall (m :: * -> *) a.
(PrimMonad m, Prim a) =>
PrimVar (PrimState m) a -> m a
readPrimVar PrimVar s Int
PrimVar (PrimState (ST s)) Int
sizeVar
i <- readPrimVar qhead
TRACING(traceM $ "!!! INITIAL: " ++ show (i, n))
TRACING(tracePartialAssignment pa)
if i < n
then do
l <- indexTrail trail i
writePrimVar qhead (i + 1)
initialUnitPropagate clauseDB qhead trail levels pa vars l
else return True
initialUnitPropagate :: forall s. ClauseDB s -> PrimVar s Int -> Trail s -> Levels s -> PartialAssignment s -> VarSet s -> Lit -> ST s Bool
initialUnitPropagate :: forall s.
ClauseDB s
-> PrimVar s Int
-> Trail s
-> Levels s
-> PartialAssignment s
-> VarSet s
-> Lit
-> ST s Bool
initialUnitPropagate !ClauseDB s
clauseDB !PrimVar s Int
qhead !Trail s
trail !Levels s
levels !PartialAssignment s
pa !VarSet s
vars !Lit
l = do
let _unused :: Lit
_unused = Lit
l
TRACING(traceM ("initialUnitPropagate " ++ show l))
#ifdef TWO_WATCHED_LITERALS
watches <- Lit -> ClauseDB s -> ST s (Vec s Watch)
forall s. Lit -> ClauseDB s -> ST s (Vec s Watch)
lookupClauseDB (Lit -> Lit
neg Lit
l) ClauseDB s
clauseDB
size <- sizeofVec watches
TRACING(traceM ("initialUnitPropagate watches: " ++ show size))
go watches 0 0 size
where
go :: Vec s Watch -> Int -> Int -> Int -> ST s Bool
go :: Vec s Watch -> Int -> Int -> Int -> ST s Bool
go !Vec s Watch
watches !Int
i !Int
j !Int
size
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
size
= do
Vec s Watch -> Int -> ST s ()
forall s a. Vec s a -> Int -> ST s ()
shrinkVec Vec s Watch
watches Int
j
ClauseDB s
-> PrimVar s Int
-> Trail s
-> Levels s
-> PartialAssignment s
-> VarSet s
-> ST s Bool
forall s.
ClauseDB s
-> PrimVar s Int
-> Trail s
-> Levels s
-> PartialAssignment s
-> VarSet s
-> ST s Bool
initialLoop ClauseDB s
clauseDB PrimVar s Int
qhead Trail s
trail Levels s
levels PartialAssignment s
pa VarSet s
vars
| Bool
otherwise
= Vec s Watch -> Int -> ST s Watch
forall s a. Vec s a -> Int -> ST s a
readVec Vec s Watch
watches Int
i ST s Watch -> (Watch -> ST s Bool) -> ST s Bool
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ w :: Watch
w@(W Lit
l' Clause2
c) ->
PartialAssignment s
-> Clause2 -> (Satisfied_ -> ST s Bool) -> ST s Bool
forall s r.
PartialAssignment s -> Clause2 -> (Satisfied_ -> ST s r) -> ST s r
satisfied2_ PartialAssignment s
pa Clause2
c (Watch -> Lit -> Satisfied_ -> ST s Bool
kontInitialUnitPropagate Watch
w Lit
l')
where
{-# INLINE [1] kontInitialUnitPropagate #-}
kontInitialUnitPropagate :: Watch -> Lit -> Satisfied_ -> ST s Bool
kontInitialUnitPropagate Watch
w Lit
l' = \case
Satisfied_
Conflicting_ -> do
Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w
Vec s Watch -> Int -> Int -> Int -> ST s ()
forall s. Vec s Watch -> Int -> Int -> Int -> ST s ()
copyWatches Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size
Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Satisfied_
Satisfied_ -> do
Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w
Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size
Unit_ Lit
u -> do
Vec s Watch -> Int -> Watch -> ST s ()
forall s a. Vec s a -> Int -> a -> ST s ()
writeVec Vec s Watch
watches Int
j Watch
w
Trail s
-> PartialAssignment s -> Levels s -> VarSet s -> Lit -> ST s ()
forall s.
Trail s
-> PartialAssignment s -> Levels s -> VarSet s -> Lit -> ST s ()
initialEnqueue Trail s
trail PartialAssignment s
pa Levels s
levels VarSet s
vars Lit
u
Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
size
Unresolved_ Lit
l1 Lit
l2
| Lit
l2 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l', Lit
l2 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l
-> do
Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l2 Watch
w ClauseDB s
clauseDB
Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
j Int
size
| Lit
l1 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l', Lit
l1 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
l
-> do
Lit -> Watch -> ClauseDB s -> ST s ()
forall s. Lit -> Watch -> ClauseDB s -> ST s ()
insertWatch Lit
l1 Watch
w ClauseDB s
clauseDB
Vec s Watch -> Int -> Int -> Int -> ST s Bool
go Vec s Watch
watches (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
j Int
size
| Bool
otherwise
-> String -> ST s Bool
forall a. HasCallStack => String -> a
error (String
"watch" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Lit, Lit, Lit, Lit) -> String
forall a. Show a => a -> String
show (Lit
l, Lit
l1, Lit
l2, Lit
l'))
#else
go clauseDB
where
go [] = initialLoop clauseDB units vars pa
go (c:cs) = satisfied2_ pa c (kontInitialUnitPropagate cs)
{-# INLINE [1] kontInitialUnitPropagate #-}
kontInitialUnitPropagate :: [Clause2] -> Satisfied_ -> ST s Bool
kontInitialUnitPropagate cs = \case
Conflicting_ -> return False
Unresolved_ _ _ -> go cs
Satisfied_ -> go cs
Unit_ u -> do
insertLitSet u units
go cs
#endif
simplify :: 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
num_vars :: Solver s -> ST s Int
num_vars :: forall s. Solver s -> ST s Int
num_vars Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = do
n <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
nextLit
return (unsafeShiftR n 1)
num_clauses :: Solver s -> ST s Int
num_clauses :: forall s. Solver s -> ST s Int
num_clauses Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = Stats s -> ST s Int
forall s. Stats s -> ST s Int
readStatsClauses Stats s
statistics
num_learnts :: Solver s -> ST s Int
num_learnts :: forall s. Solver s -> ST s Int
num_learnts Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = Stats s -> ST s Int
forall s. Stats s -> ST s Int
readStatsLearnt Stats s
statistics
num_learnt_literals :: Solver s -> ST s Int
num_learnt_literals :: forall s. Solver s -> ST s Int
num_learnt_literals Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = Stats s -> ST s Int
forall s. Stats s -> ST s Int
readStatsLearntLiterals Stats s
statistics
num_conflicts :: Solver s -> ST s Int
num_conflicts :: forall s. Solver s -> ST s Int
num_conflicts Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = Stats s -> ST s Int
forall s. Stats s -> ST s Int
readStatsConflicts Stats s
statistics
num_restarts :: Solver s -> ST s Int
num_restarts :: forall s. Solver s -> ST s Int
num_restarts Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} = Stats s -> ST s Int
forall s. Stats s -> ST s Int
readStatsRestarts Stats s
statistics
modelValue :: Solver s -> Lit -> ST s Bool
modelValue :: forall s. Solver s -> Lit -> ST s Bool
modelValue Solver {PrimVar s Int
LCG s
Stats s
STRef s Bool
STRef s Int
STRef s (PartialAssignment s)
STRef s (Levels s)
STRef s (Trail s)
STRef s (VarSet s)
STRef s (ClauseDB s)
ok :: forall s. Solver s -> STRef s Bool
nextLit :: forall s. Solver s -> STRef s Int
zeroLevels :: forall s. Solver s -> STRef s (Levels s)
zeroHead :: forall s. Solver s -> PrimVar s Int
zeroTrail :: forall s. Solver s -> STRef s (Trail s)
zeroPA :: forall s. Solver s -> STRef s (PartialAssignment s)
zeroVars :: forall s. Solver s -> STRef s (VarSet s)
prevPA :: forall s. Solver s -> STRef s (PartialAssignment s)
clauses :: forall s. Solver s -> STRef s (ClauseDB s)
lcg :: forall s. Solver s -> LCG s
statistics :: forall s. Solver s -> Stats s
ok :: STRef s Bool
nextLit :: STRef s Int
zeroLevels :: STRef s (Levels s)
zeroHead :: PrimVar s Int
zeroTrail :: STRef s (Trail s)
zeroPA :: STRef s (PartialAssignment s)
zeroVars :: STRef s (VarSet s)
prevPA :: STRef s (PartialAssignment s)
clauses :: STRef s (ClauseDB s)
lcg :: LCG s
statistics :: Stats s
..} Lit
l = do
pa <- STRef s (PartialAssignment s) -> ST s (PartialAssignment s)
forall s a. STRef s a -> ST s a
readSTRef STRef s (PartialAssignment s)
prevPA
lookupPartialAssignment l pa <&> \case
LBool
LUndef -> Bool
False
LBool
LTrue -> Bool
True
LBool
LFalse -> Bool
False