{-# 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
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
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]
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
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
..}
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'
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
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
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
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 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
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
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)
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
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)
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
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)
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
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
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
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 :: 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
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
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