{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module ToySolver.SAT.Solver.MessagePassing.SurveyPropagation
(
Solver
, newSolver
, deleteSolver
, getNVars
, getNConstraints
, getTolerance
, setTolerance
, getIterationLimit
, setIterationLimit
, getNThreads
, setNThreads
, initializeRandom
, initializeRandomDirichlet
, propagate
, getVarProb
, fixLit
, unfixLit
, printInfo
) where
import Control.Concurrent
import Control.Concurrent.STM
import Control.Exception
import Control.Loop
import Control.Monad
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.IORef
import qualified Data.Vector as V
import qualified Data.Vector.Mutable as VM
import qualified Data.Vector.Unboxed as VU
import qualified Data.Vector.Unboxed.Mutable as VUM
import Data.Vector.Generic ((!))
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Generic.Mutable as VGM
import Numeric
import qualified Numeric.Log as L
import qualified System.Random.MWC as Rand
import qualified System.Random.MWC.Distributions as Rand
import qualified ToySolver.SAT.Types as SAT
infixr 8 ^*
(^*) :: Num a => L.Log a -> a -> L.Log a
L.Exp a
a ^* :: Log a -> a -> Log a
^* a
b = a -> Log a
forall a. a -> Log a
L.Exp (a
aa -> a -> a
forall a. Num a => a -> a -> a
*a
b)
comp :: RealFloat a => L.Log a -> L.Log a
comp :: Log a -> Log a
comp (L.Exp a
a) = a -> Log a
forall a. a -> Log a
L.Exp (a -> Log a) -> a -> Log a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Floating a => a -> a
log1p (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Ord a => a -> a -> a
max (-a
1) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Num a => a -> a
negate (a -> a
forall a. Floating a => a -> a
exp a
a)
type ClauseIndex = Int
type EdgeIndex = Int
data Solver
= Solver
{ Solver -> Vector (Vector EdgeIndex)
svVarEdges :: !(V.Vector (VU.Vector EdgeIndex))
, Solver -> IOVector (Log Double)
svVarProbT :: !(VUM.IOVector (L.Log Double))
, Solver -> IOVector (Log Double)
svVarProbF :: !(VUM.IOVector (L.Log Double))
, Solver -> IOVector (Maybe Bool)
svVarFixed :: !(VM.IOVector (Maybe Bool))
, Solver -> Vector (Vector EdgeIndex)
svClauseEdges :: !(V.Vector (VU.Vector EdgeIndex))
, Solver -> Vector Double
svClauseWeight :: !(VU.Vector Double)
, Solver -> Vector EdgeIndex
svEdgeLit :: !(VU.Vector SAT.Lit)
, Solver -> Vector EdgeIndex
svEdgeClause :: !(VU.Vector ClauseIndex)
, Solver -> IOVector (Log Double)
svEdgeSurvey :: !(VUM.IOVector (L.Log Double))
, Solver -> IOVector (Log Double)
svEdgeProbU :: !(VUM.IOVector (L.Log Double))
, Solver -> IORef Double
svTolRef :: !(IORef Double)
, Solver -> IORef (Maybe EdgeIndex)
svIterLimRef :: !(IORef (Maybe Int))
, Solver -> IORef EdgeIndex
svNThreadsRef :: !(IORef Int)
}
newSolver :: Int -> [(Double, SAT.PackedClause)] -> IO Solver
newSolver :: EdgeIndex -> [(Double, PackedClause)] -> IO Solver
newSolver EdgeIndex
nv [(Double, PackedClause)]
clauses = do
let num_clauses :: EdgeIndex
num_clauses = [(Double, PackedClause)] -> EdgeIndex
forall (t :: * -> *) a. Foldable t => t a -> EdgeIndex
length [(Double, PackedClause)]
clauses
num_edges :: EdgeIndex
num_edges = [EdgeIndex] -> EdgeIndex
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [PackedClause -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length PackedClause
c | (Double
_,PackedClause
c) <- [(Double, PackedClause)]
clauses]
IORef (IntMap IntSet)
varEdgesRef <- IntMap IntSet -> IO (IORef (IntMap IntSet))
forall a. a -> IO (IORef a)
newIORef IntMap IntSet
forall a. IntMap a
IntMap.empty
MVector RealWorld (Vector EdgeIndex)
clauseEdgesM <- EdgeIndex -> IO (MVector (PrimState IO) (Vector EdgeIndex))
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
EdgeIndex -> m (v (PrimState m) a)
VGM.new EdgeIndex
num_clauses
(IOVector EdgeIndex
edgeLitM :: VUM.IOVector SAT.Lit) <- EdgeIndex -> IO (MVector (PrimState IO) EdgeIndex)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
EdgeIndex -> m (v (PrimState m) a)
VGM.new EdgeIndex
num_edges
(IOVector EdgeIndex
edgeClauseM :: VUM.IOVector ClauseIndex) <- EdgeIndex -> IO (MVector (PrimState IO) EdgeIndex)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
EdgeIndex -> m (v (PrimState m) a)
VGM.new EdgeIndex
num_edges
IORef EdgeIndex
ref <- EdgeIndex -> IO (IORef EdgeIndex)
forall a. a -> IO (IORef a)
newIORef EdgeIndex
0
[(EdgeIndex, (Double, PackedClause))]
-> ((EdgeIndex, (Double, PackedClause)) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([EdgeIndex]
-> [(Double, PackedClause)]
-> [(EdgeIndex, (Double, PackedClause))]
forall a b. [a] -> [b] -> [(a, b)]
zip [EdgeIndex
0..] [(Double, PackedClause)]
clauses) (((EdgeIndex, (Double, PackedClause)) -> IO ()) -> IO ())
-> ((EdgeIndex, (Double, PackedClause)) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(EdgeIndex
i,(Double
_,PackedClause
c)) -> do
[EdgeIndex]
es <- [EdgeIndex] -> (EdgeIndex -> IO EdgeIndex) -> IO [EdgeIndex]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (PackedClause -> [EdgeIndex]
SAT.unpackClause PackedClause
c) ((EdgeIndex -> IO EdgeIndex) -> IO [EdgeIndex])
-> (EdgeIndex -> IO EdgeIndex) -> IO [EdgeIndex]
forall a b. (a -> b) -> a -> b
$ \EdgeIndex
lit -> do
EdgeIndex
e <- IORef EdgeIndex -> IO EdgeIndex
forall a. IORef a -> IO a
readIORef IORef EdgeIndex
ref
IORef EdgeIndex -> (EdgeIndex -> EdgeIndex) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef EdgeIndex
ref (EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+EdgeIndex
1)
IORef (IntMap IntSet) -> (IntMap IntSet -> IntMap IntSet) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (IntMap IntSet)
varEdgesRef ((IntSet -> IntSet -> IntSet)
-> EdgeIndex -> IntSet -> IntMap IntSet -> IntMap IntSet
forall a. (a -> a -> a) -> EdgeIndex -> a -> IntMap a -> IntMap a
IntMap.insertWith IntSet -> IntSet -> IntSet
IntSet.union (EdgeIndex -> EdgeIndex
forall a. Num a => a -> a
abs EdgeIndex
lit) (EdgeIndex -> IntSet
IntSet.singleton EdgeIndex
e))
MVector (PrimState IO) EdgeIndex -> EdgeIndex -> EdgeIndex -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite IOVector EdgeIndex
MVector (PrimState IO) EdgeIndex
edgeLitM EdgeIndex
e EdgeIndex
lit
MVector (PrimState IO) EdgeIndex -> EdgeIndex -> EdgeIndex -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite IOVector EdgeIndex
MVector (PrimState IO) EdgeIndex
edgeClauseM EdgeIndex
e EdgeIndex
i
EdgeIndex -> IO EdgeIndex
forall (m :: * -> *) a. Monad m => a -> m a
return EdgeIndex
e
MVector (PrimState IO) (Vector EdgeIndex)
-> EdgeIndex -> Vector EdgeIndex -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite MVector RealWorld (Vector EdgeIndex)
MVector (PrimState IO) (Vector EdgeIndex)
clauseEdgesM EdgeIndex
i ([EdgeIndex] -> Vector EdgeIndex
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList [EdgeIndex]
es)
IntMap IntSet
varEdges <- IORef (IntMap IntSet) -> IO (IntMap IntSet)
forall a. IORef a -> IO a
readIORef IORef (IntMap IntSet)
varEdgesRef
Vector (Vector EdgeIndex)
clauseEdges <- Mutable Vector (PrimState IO) (Vector EdgeIndex)
-> IO (Vector (Vector EdgeIndex))
forall (m :: * -> *) (v :: * -> *) a.
(PrimMonad m, Vector v a) =>
Mutable v (PrimState m) a -> m (v a)
VG.unsafeFreeze MVector RealWorld (Vector EdgeIndex)
Mutable Vector (PrimState IO) (Vector EdgeIndex)
clauseEdgesM
Vector EdgeIndex
edgeLit <- Mutable Vector (PrimState IO) EdgeIndex -> IO (Vector EdgeIndex)
forall (m :: * -> *) (v :: * -> *) a.
(PrimMonad m, Vector v a) =>
Mutable v (PrimState m) a -> m (v a)
VG.unsafeFreeze IOVector EdgeIndex
Mutable Vector (PrimState IO) EdgeIndex
edgeLitM
Vector EdgeIndex
edgeClause <- Mutable Vector (PrimState IO) EdgeIndex -> IO (Vector EdgeIndex)
forall (m :: * -> *) (v :: * -> *) a.
(PrimMonad m, Vector v a) =>
Mutable v (PrimState m) a -> m (v a)
VG.unsafeFreeze IOVector EdgeIndex
Mutable Vector (PrimState IO) EdgeIndex
edgeClauseM
IOVector (Log Double)
edgeSurvey <- EdgeIndex -> Log Double -> IO (MVector (PrimState IO) (Log Double))
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
EdgeIndex -> a -> m (v (PrimState m) a)
VGM.replicate EdgeIndex
num_edges Log Double
0.5
IOVector (Log Double)
edgeProbU <- EdgeIndex -> IO (MVector (PrimState IO) (Log Double))
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
EdgeIndex -> m (v (PrimState m) a)
VGM.new EdgeIndex
num_edges
IOVector (Maybe Bool)
varFixed <- EdgeIndex -> Maybe Bool -> IO (MVector (PrimState IO) (Maybe Bool))
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
EdgeIndex -> a -> m (v (PrimState m) a)
VGM.replicate EdgeIndex
nv Maybe Bool
forall a. Maybe a
Nothing
IOVector (Log Double)
varProbT <- EdgeIndex -> IO (MVector (PrimState IO) (Log Double))
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
EdgeIndex -> m (v (PrimState m) a)
VGM.new EdgeIndex
nv
IOVector (Log Double)
varProbF <- EdgeIndex -> IO (MVector (PrimState IO) (Log Double))
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
EdgeIndex -> m (v (PrimState m) a)
VGM.new EdgeIndex
nv
IORef Double
tolRef <- Double -> IO (IORef Double)
forall a. a -> IO (IORef a)
newIORef Double
0.01
IORef (Maybe EdgeIndex)
maxIterRef <- Maybe EdgeIndex -> IO (IORef (Maybe EdgeIndex))
forall a. a -> IO (IORef a)
newIORef (EdgeIndex -> Maybe EdgeIndex
forall a. a -> Maybe a
Just EdgeIndex
1000)
IORef EdgeIndex
nthreadsRef <- EdgeIndex -> IO (IORef EdgeIndex)
forall a. a -> IO (IORef a)
newIORef EdgeIndex
1
let solver :: Solver
solver = Solver :: Vector (Vector EdgeIndex)
-> IOVector (Log Double)
-> IOVector (Log Double)
-> IOVector (Maybe Bool)
-> Vector (Vector EdgeIndex)
-> Vector Double
-> Vector EdgeIndex
-> Vector EdgeIndex
-> IOVector (Log Double)
-> IOVector (Log Double)
-> IORef Double
-> IORef (Maybe EdgeIndex)
-> IORef EdgeIndex
-> Solver
Solver
{ svVarEdges :: Vector (Vector EdgeIndex)
svVarEdges = EdgeIndex
-> (EdgeIndex -> Vector EdgeIndex) -> Vector (Vector EdgeIndex)
forall (v :: * -> *) a.
Vector v a =>
EdgeIndex -> (EdgeIndex -> a) -> v a
VG.generate EdgeIndex
nv ((EdgeIndex -> Vector EdgeIndex) -> Vector (Vector EdgeIndex))
-> (EdgeIndex -> Vector EdgeIndex) -> Vector (Vector EdgeIndex)
forall a b. (a -> b) -> a -> b
$ \EdgeIndex
i ->
case EdgeIndex -> IntMap IntSet -> Maybe IntSet
forall a. EdgeIndex -> IntMap a -> Maybe a
IntMap.lookup (EdgeIndex
iEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+EdgeIndex
1) IntMap IntSet
varEdges of
Maybe IntSet
Nothing -> Vector EdgeIndex
forall (v :: * -> *) a. Vector v a => v a
VG.empty
Just IntSet
es -> EdgeIndex -> [EdgeIndex] -> Vector EdgeIndex
forall (v :: * -> *) a. Vector v a => EdgeIndex -> [a] -> v a
VG.fromListN (IntSet -> EdgeIndex
IntSet.size IntSet
es) (IntSet -> [EdgeIndex]
IntSet.toList IntSet
es)
, svVarProbT :: IOVector (Log Double)
svVarProbT = IOVector (Log Double)
varProbT
, svVarProbF :: IOVector (Log Double)
svVarProbF = IOVector (Log Double)
varProbF
, svVarFixed :: IOVector (Maybe Bool)
svVarFixed = IOVector (Maybe Bool)
varFixed
, svClauseEdges :: Vector (Vector EdgeIndex)
svClauseEdges = Vector (Vector EdgeIndex)
clauseEdges
, svClauseWeight :: Vector Double
svClauseWeight = EdgeIndex -> [Double] -> Vector Double
forall (v :: * -> *) a. Vector v a => EdgeIndex -> [a] -> v a
VG.fromListN (Vector (Vector EdgeIndex) -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length Vector (Vector EdgeIndex)
clauseEdges) (((Double, PackedClause) -> Double)
-> [(Double, PackedClause)] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map (Double, PackedClause) -> Double
forall a b. (a, b) -> a
fst [(Double, PackedClause)]
clauses)
, svEdgeLit :: Vector EdgeIndex
svEdgeLit = Vector EdgeIndex
edgeLit
, svEdgeClause :: Vector EdgeIndex
svEdgeClause = Vector EdgeIndex
edgeClause
, svEdgeSurvey :: IOVector (Log Double)
svEdgeSurvey = IOVector (Log Double)
edgeSurvey
, svEdgeProbU :: IOVector (Log Double)
svEdgeProbU = IOVector (Log Double)
edgeProbU
, svTolRef :: IORef Double
svTolRef = IORef Double
tolRef
, svIterLimRef :: IORef (Maybe EdgeIndex)
svIterLimRef = IORef (Maybe EdgeIndex)
maxIterRef
, svNThreadsRef :: IORef EdgeIndex
svNThreadsRef = IORef EdgeIndex
nthreadsRef
}
Solver -> IO Solver
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
solver
deleteSolver :: Solver -> IO ()
deleteSolver :: Solver -> IO ()
deleteSolver Solver
_solver = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
initializeRandom :: Solver -> Rand.GenIO -> IO ()
initializeRandom :: Solver -> GenIO -> IO ()
initializeRandom Solver
solver GenIO
gen = do
Vector (Vector EdgeIndex) -> (Vector EdgeIndex -> IO ()) -> IO ()
forall (m :: * -> *) (v :: * -> *) a b.
(Monad m, Vector v a) =>
v a -> (a -> m b) -> m ()
VG.forM_ (Solver -> Vector (Vector EdgeIndex)
svClauseEdges Solver
solver) ((Vector EdgeIndex -> IO ()) -> IO ())
-> (Vector EdgeIndex -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Vector EdgeIndex
es -> do
case Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length Vector EdgeIndex
es of
EdgeIndex
0 -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
EdgeIndex
1 -> MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite (Solver -> IOVector (Log Double)
svEdgeSurvey Solver
solver) (Vector EdgeIndex
es Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
0) Log Double
1
EdgeIndex
n -> do
let p :: Double
p :: Double
p = Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ EdgeIndex -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral EdgeIndex
n
Vector EdgeIndex -> (EdgeIndex -> IO ()) -> IO ()
forall (m :: * -> *) (v :: * -> *) a b.
(Monad m, Vector v a) =>
v a -> (a -> m b) -> m ()
VG.forM_ Vector EdgeIndex
es ((EdgeIndex -> IO ()) -> IO ()) -> (EdgeIndex -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \EdgeIndex
e -> do
Double
d <- (Double, Double) -> GenIO -> IO Double
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Double
pDouble -> Double -> Double
forall a. Num a => a -> a -> a
*Double
0.5, Double
pDouble -> Double -> Double
forall a. Num a => a -> a -> a
*Double
1.5) GenIO
gen
MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite (Solver -> IOVector (Log Double)
svEdgeSurvey Solver
solver) EdgeIndex
e (Double -> Log Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac Double
d)
initializeRandomDirichlet :: Solver -> Rand.GenIO -> IO ()
initializeRandomDirichlet :: Solver -> GenIO -> IO ()
initializeRandomDirichlet Solver
solver GenIO
gen = do
Vector (Vector EdgeIndex) -> (Vector EdgeIndex -> IO ()) -> IO ()
forall (m :: * -> *) (v :: * -> *) a b.
(Monad m, Vector v a) =>
v a -> (a -> m b) -> m ()
VG.forM_ (Solver -> Vector (Vector EdgeIndex)
svClauseEdges Solver
solver) ((Vector EdgeIndex -> IO ()) -> IO ())
-> (Vector EdgeIndex -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Vector EdgeIndex
es -> do
case Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length Vector EdgeIndex
es of
EdgeIndex
0 -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
EdgeIndex
1 -> MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite (Solver -> IOVector (Log Double)
svEdgeSurvey Solver
solver) (Vector EdgeIndex
es Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
0) Log Double
1
EdgeIndex
len -> do
(Vector Double
ps :: V.Vector Double) <- Vector Double -> GenIO -> IO (Vector Double)
forall (m :: * -> *) (t :: * -> *).
(PrimMonad m, Traversable t) =>
t Double -> Gen (PrimState m) -> m (t Double)
Rand.dirichlet (EdgeIndex -> Double -> Vector Double
forall (v :: * -> *) a. Vector v a => EdgeIndex -> a -> v a
VG.replicate EdgeIndex
len Double
1) GenIO
gen
EdgeIndex -> EdgeIndex -> (EdgeIndex -> IO ()) -> IO ()
forall a (m :: * -> *).
(Num a, Ord a, Monad m) =>
a -> a -> (a -> m ()) -> m ()
numLoop EdgeIndex
0 (EdgeIndex
lenEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
-EdgeIndex
1) ((EdgeIndex -> IO ()) -> IO ()) -> (EdgeIndex -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \EdgeIndex
i -> do
MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite (Solver -> IOVector (Log Double)
svEdgeSurvey Solver
solver) (Vector EdgeIndex
es Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
i) (Double -> Log Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Vector Double
ps Vector Double -> EdgeIndex -> Double
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
i))
getNVars :: Solver -> IO Int
getNVars :: Solver -> IO EdgeIndex
getNVars Solver
solver = EdgeIndex -> IO EdgeIndex
forall (m :: * -> *) a. Monad m => a -> m a
return (EdgeIndex -> IO EdgeIndex) -> EdgeIndex -> IO EdgeIndex
forall a b. (a -> b) -> a -> b
$ Vector (Vector EdgeIndex) -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length (Solver -> Vector (Vector EdgeIndex)
svVarEdges Solver
solver)
getNConstraints :: Solver -> IO Int
getNConstraints :: Solver -> IO EdgeIndex
getNConstraints Solver
solver = EdgeIndex -> IO EdgeIndex
forall (m :: * -> *) a. Monad m => a -> m a
return (EdgeIndex -> IO EdgeIndex) -> EdgeIndex -> IO EdgeIndex
forall a b. (a -> b) -> a -> b
$ Vector (Vector EdgeIndex) -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length (Solver -> Vector (Vector EdgeIndex)
svClauseEdges Solver
solver)
getNEdges :: Solver -> IO Int
getNEdges :: Solver -> IO EdgeIndex
getNEdges Solver
solver = EdgeIndex -> IO EdgeIndex
forall (m :: * -> *) a. Monad m => a -> m a
return (EdgeIndex -> IO EdgeIndex) -> EdgeIndex -> IO EdgeIndex
forall a b. (a -> b) -> a -> b
$ Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length (Solver -> Vector EdgeIndex
svEdgeLit Solver
solver)
getTolerance :: Solver -> IO Double
getTolerance :: Solver -> IO Double
getTolerance Solver
solver = IORef Double -> IO Double
forall a. IORef a -> IO a
readIORef (Solver -> IORef Double
svTolRef Solver
solver)
setTolerance :: Solver -> Double -> IO ()
setTolerance :: Solver -> Double -> IO ()
setTolerance Solver
solver !Double
tol = IORef Double -> Double -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Double
svTolRef Solver
solver) Double
tol
getIterationLimit :: Solver -> IO (Maybe Int)
getIterationLimit :: Solver -> IO (Maybe EdgeIndex)
getIterationLimit Solver
solver = IORef (Maybe EdgeIndex) -> IO (Maybe EdgeIndex)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Maybe EdgeIndex)
svIterLimRef Solver
solver)
setIterationLimit :: Solver -> Maybe Int -> IO ()
setIterationLimit :: Solver -> Maybe EdgeIndex -> IO ()
setIterationLimit Solver
solver Maybe EdgeIndex
val = IORef (Maybe EdgeIndex) -> Maybe EdgeIndex -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Maybe EdgeIndex)
svIterLimRef Solver
solver) Maybe EdgeIndex
val
getNThreads :: Solver -> IO Int
getNThreads :: Solver -> IO EdgeIndex
getNThreads Solver
solver = IORef EdgeIndex -> IO EdgeIndex
forall a. IORef a -> IO a
readIORef (Solver -> IORef EdgeIndex
svNThreadsRef Solver
solver)
setNThreads :: Solver -> Int -> IO ()
setNThreads :: Solver -> EdgeIndex -> IO ()
setNThreads Solver
solver EdgeIndex
val = IORef EdgeIndex -> EdgeIndex -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef EdgeIndex
svNThreadsRef Solver
solver) EdgeIndex
val
propagate :: Solver -> IO Bool
propagate :: Solver -> IO Bool
propagate Solver
solver = do
EdgeIndex
nthreads <- Solver -> IO EdgeIndex
getNThreads Solver
solver
if EdgeIndex
nthreads EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeIndex
1 then
Solver -> EdgeIndex -> IO Bool
propagateMT Solver
solver EdgeIndex
nthreads
else
Solver -> IO Bool
propagateST Solver
solver
propagateST :: Solver -> IO Bool
propagateST :: Solver -> IO Bool
propagateST Solver
solver = do
Double
tol <- Solver -> IO Double
getTolerance Solver
solver
Maybe EdgeIndex
lim <- Solver -> IO (Maybe EdgeIndex)
getIterationLimit Solver
solver
EdgeIndex
nv <- Solver -> IO EdgeIndex
getNVars Solver
solver
EdgeIndex
nc <- Solver -> IO EdgeIndex
getNConstraints Solver
solver
let max_v_len :: EdgeIndex
max_v_len = Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. (Vector v a, Ord a) => v a -> a
VG.maximum (Vector EdgeIndex -> EdgeIndex) -> Vector EdgeIndex -> EdgeIndex
forall a b. (a -> b) -> a -> b
$ (Vector EdgeIndex -> EdgeIndex)
-> Vector (Vector EdgeIndex) -> Vector EdgeIndex
forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length (Vector (Vector EdgeIndex) -> Vector EdgeIndex)
-> Vector (Vector EdgeIndex) -> Vector EdgeIndex
forall a b. (a -> b) -> a -> b
$ Solver -> Vector (Vector EdgeIndex)
svVarEdges Solver
solver
max_c_len :: EdgeIndex
max_c_len = Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. (Vector v a, Ord a) => v a -> a
VG.maximum (Vector EdgeIndex -> EdgeIndex) -> Vector EdgeIndex -> EdgeIndex
forall a b. (a -> b) -> a -> b
$ (Vector EdgeIndex -> EdgeIndex)
-> Vector (Vector EdgeIndex) -> Vector EdgeIndex
forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length (Vector (Vector EdgeIndex) -> Vector EdgeIndex)
-> Vector (Vector EdgeIndex) -> Vector EdgeIndex
forall a b. (a -> b) -> a -> b
$ Solver -> Vector (Vector EdgeIndex)
svClauseEdges Solver
solver
IOVector (Log Double)
tmp <- EdgeIndex -> IO (MVector (PrimState IO) (Log Double))
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
EdgeIndex -> m (v (PrimState m) a)
VGM.new (EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Ord a => a -> a -> a
max (EdgeIndex
max_v_len EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
* EdgeIndex
2) EdgeIndex
max_c_len)
let loop :: EdgeIndex -> IO Bool
loop !EdgeIndex
i
| Just EdgeIndex
l <- Maybe EdgeIndex
lim, EdgeIndex
i EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
>= EdgeIndex
l = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| Bool
otherwise = do
EdgeIndex -> EdgeIndex -> (EdgeIndex -> IO ()) -> IO ()
forall a (m :: * -> *).
(Num a, Ord a, Monad m) =>
a -> a -> (a -> m ()) -> m ()
numLoop EdgeIndex
1 EdgeIndex
nv ((EdgeIndex -> IO ()) -> IO ()) -> (EdgeIndex -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \EdgeIndex
v -> Solver -> EdgeIndex -> IOVector (Log Double) -> IO ()
updateEdgeProb Solver
solver EdgeIndex
v IOVector (Log Double)
tmp
let f :: Double -> EdgeIndex -> IO Double
f Double
maxDelta EdgeIndex
c = Double -> Double -> Double
forall a. Ord a => a -> a -> a
max Double
maxDelta (Double -> Double) -> IO Double -> IO Double
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> EdgeIndex -> IOVector (Log Double) -> IO Double
updateEdgeSurvey Solver
solver EdgeIndex
c IOVector (Log Double)
tmp
Double
delta <- (Double -> EdgeIndex -> IO Double)
-> Double -> [EdgeIndex] -> IO Double
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Double -> EdgeIndex -> IO Double
f Double
0 [EdgeIndex
0 .. EdgeIndex
ncEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
-EdgeIndex
1]
if Double
delta Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
tol then do
EdgeIndex -> EdgeIndex -> (EdgeIndex -> IO ()) -> IO ()
forall a (m :: * -> *).
(Num a, Ord a, Monad m) =>
a -> a -> (a -> m ()) -> m ()
numLoop EdgeIndex
1 EdgeIndex
nv ((EdgeIndex -> IO ()) -> IO ()) -> (EdgeIndex -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \EdgeIndex
v -> Solver -> EdgeIndex -> IO ()
computeVarProb Solver
solver EdgeIndex
v
Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
else
EdgeIndex -> IO Bool
loop (EdgeIndex
iEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+EdgeIndex
1)
EdgeIndex -> IO Bool
loop EdgeIndex
0
data WorkerCommand
= WCUpdateEdgeProb
| WCUpdateSurvey
| WCComputeVarProb
| WCTerminate
propagateMT :: Solver -> Int -> IO Bool
propagateMT :: Solver -> EdgeIndex -> IO Bool
propagateMT Solver
solver EdgeIndex
nthreads = do
Double
tol <- Solver -> IO Double
getTolerance Solver
solver
Maybe EdgeIndex
lim <- Solver -> IO (Maybe EdgeIndex)
getIterationLimit Solver
solver
EdgeIndex
nv <- Solver -> IO EdgeIndex
getNVars Solver
solver
EdgeIndex
nc <- Solver -> IO EdgeIndex
getNConstraints Solver
solver
((forall a. IO a -> IO a) -> IO Bool) -> IO Bool
forall b. ((forall a. IO a -> IO a) -> IO b) -> IO b
mask (((forall a. IO a -> IO a) -> IO Bool) -> IO Bool)
-> ((forall a. IO a -> IO a) -> IO Bool) -> IO Bool
forall a b. (a -> b) -> a -> b
$ \forall a. IO a -> IO a
restore -> do
TMVar SomeException
ex <- IO (TMVar SomeException)
forall a. IO (TMVar a)
newEmptyTMVarIO
let wait :: STM a -> IO a
wait :: STM a -> IO a
wait STM a
m = IO (IO a) -> IO a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (IO a) -> IO a) -> IO (IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ STM (IO a) -> IO (IO a)
forall a. STM a -> IO a
atomically (STM (IO a) -> IO (IO a)) -> STM (IO a) -> IO (IO a)
forall a b. (a -> b) -> a -> b
$ (a -> IO a) -> STM a -> STM (IO a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return STM a
m STM (IO a) -> STM (IO a) -> STM (IO a)
forall a. STM a -> STM a -> STM a
`orElse` (SomeException -> IO a) -> STM SomeException -> STM (IO a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SomeException -> IO a
forall e a. Exception e => e -> IO a
throwIO (TMVar SomeException -> STM SomeException
forall a. TMVar a -> STM a
takeTMVar TMVar SomeException
ex)
[(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
workers <- do
let mV :: EdgeIndex
mV = (EdgeIndex
nv EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+ EdgeIndex
nthreads EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1) EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Integral a => a -> a -> a
`div` EdgeIndex
nthreads
mC :: EdgeIndex
mC = (EdgeIndex
nc EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+ EdgeIndex
nthreads EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1) EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Integral a => a -> a -> a
`div` EdgeIndex
nthreads
[EdgeIndex]
-> (EdgeIndex
-> IO (ThreadId, MVar WorkerCommand, TMVar (), TMVar Double))
-> IO [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [EdgeIndex
0..EdgeIndex
nthreadsEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
-EdgeIndex
1] ((EdgeIndex
-> IO (ThreadId, MVar WorkerCommand, TMVar (), TMVar Double))
-> IO [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)])
-> (EdgeIndex
-> IO (ThreadId, MVar WorkerCommand, TMVar (), TMVar Double))
-> IO [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
forall a b. (a -> b) -> a -> b
$ \EdgeIndex
i -> do
let lbV :: EdgeIndex
lbV = EdgeIndex
mV EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
* EdgeIndex
i EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+ EdgeIndex
1
ubV :: EdgeIndex
ubV = EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Ord a => a -> a -> a
min (EdgeIndex
lbV EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+ EdgeIndex
mV) (EdgeIndex
nv EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+ EdgeIndex
1)
lbC :: EdgeIndex
lbC = EdgeIndex
mC EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
* EdgeIndex
i
ubC :: EdgeIndex
ubC = EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Ord a => a -> a -> a
min (EdgeIndex
lbC EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+ EdgeIndex
mC) EdgeIndex
nc
let max_v_len :: EdgeIndex
max_v_len = Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. (Vector v a, Ord a) => v a -> a
VG.maximum (Vector EdgeIndex -> EdgeIndex) -> Vector EdgeIndex -> EdgeIndex
forall a b. (a -> b) -> a -> b
$ (Vector EdgeIndex -> EdgeIndex)
-> Vector (Vector EdgeIndex) -> Vector EdgeIndex
forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length (Vector (Vector EdgeIndex) -> Vector EdgeIndex)
-> Vector (Vector EdgeIndex) -> Vector EdgeIndex
forall a b. (a -> b) -> a -> b
$ EdgeIndex
-> EdgeIndex
-> Vector (Vector EdgeIndex)
-> Vector (Vector EdgeIndex)
forall (v :: * -> *) a.
Vector v a =>
EdgeIndex -> EdgeIndex -> v a -> v a
VG.slice (EdgeIndex
lbV EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1) (EdgeIndex
ubV EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
lbV) (Solver -> Vector (Vector EdgeIndex)
svVarEdges Solver
solver)
max_c_len :: EdgeIndex
max_c_len = Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. (Vector v a, Ord a) => v a -> a
VG.maximum (Vector EdgeIndex -> EdgeIndex) -> Vector EdgeIndex -> EdgeIndex
forall a b. (a -> b) -> a -> b
$ (Vector EdgeIndex -> EdgeIndex)
-> Vector (Vector EdgeIndex) -> Vector EdgeIndex
forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length (Vector (Vector EdgeIndex) -> Vector EdgeIndex)
-> Vector (Vector EdgeIndex) -> Vector EdgeIndex
forall a b. (a -> b) -> a -> b
$ EdgeIndex
-> EdgeIndex
-> Vector (Vector EdgeIndex)
-> Vector (Vector EdgeIndex)
forall (v :: * -> *) a.
Vector v a =>
EdgeIndex -> EdgeIndex -> v a -> v a
VG.slice EdgeIndex
lbC (EdgeIndex
ubC EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
lbC) (Solver -> Vector (Vector EdgeIndex)
svClauseEdges Solver
solver)
IOVector (Log Double)
tmp <- EdgeIndex -> IO (MVector (PrimState IO) (Log Double))
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
EdgeIndex -> m (v (PrimState m) a)
VGM.new (EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Ord a => a -> a -> a
max (EdgeIndex
max_v_lenEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
*EdgeIndex
2) EdgeIndex
max_c_len)
MVar WorkerCommand
reqVar <- IO (MVar WorkerCommand)
forall a. IO (MVar a)
newEmptyMVar
TMVar ()
respVar <- IO (TMVar ())
forall a. IO (TMVar a)
newEmptyTMVarIO
TMVar Double
respVar2 <- IO (TMVar Double)
forall a. IO (TMVar a)
newEmptyTMVarIO
ThreadId
th <- IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ do
let loop :: IO ()
loop = do
WorkerCommand
cmd <- MVar WorkerCommand -> IO WorkerCommand
forall a. MVar a -> IO a
takeMVar MVar WorkerCommand
reqVar
case WorkerCommand
cmd of
WorkerCommand
WCTerminate -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
WorkerCommand
WCUpdateEdgeProb -> do
EdgeIndex -> EdgeIndex -> (EdgeIndex -> IO ()) -> IO ()
forall a (m :: * -> *).
(Num a, Ord a, Monad m) =>
a -> a -> (a -> m ()) -> m ()
numLoop EdgeIndex
lbV (EdgeIndex
ubVEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
-EdgeIndex
1) ((EdgeIndex -> IO ()) -> IO ()) -> (EdgeIndex -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \EdgeIndex
v -> Solver -> EdgeIndex -> IOVector (Log Double) -> IO ()
updateEdgeProb Solver
solver EdgeIndex
v IOVector (Log Double)
tmp
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TMVar () -> () -> STM ()
forall a. TMVar a -> a -> STM ()
putTMVar TMVar ()
respVar ()
IO ()
loop
WorkerCommand
WCUpdateSurvey -> do
let f :: Double -> EdgeIndex -> IO Double
f Double
maxDelta EdgeIndex
c = Double -> Double -> Double
forall a. Ord a => a -> a -> a
max Double
maxDelta (Double -> Double) -> IO Double -> IO Double
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> EdgeIndex -> IOVector (Log Double) -> IO Double
updateEdgeSurvey Solver
solver EdgeIndex
c IOVector (Log Double)
tmp
Double
delta <- (Double -> EdgeIndex -> IO Double)
-> Double -> [EdgeIndex] -> IO Double
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Double -> EdgeIndex -> IO Double
f Double
0 [EdgeIndex
lbC .. EdgeIndex
ubCEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
-EdgeIndex
1]
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TMVar Double -> Double -> STM ()
forall a. TMVar a -> a -> STM ()
putTMVar TMVar Double
respVar2 Double
delta
IO ()
loop
WorkerCommand
WCComputeVarProb -> do
EdgeIndex -> EdgeIndex -> (EdgeIndex -> IO ()) -> IO ()
forall a (m :: * -> *).
(Num a, Ord a, Monad m) =>
a -> a -> (a -> m ()) -> m ()
numLoop EdgeIndex
lbV (EdgeIndex
ubVEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
-EdgeIndex
1) ((EdgeIndex -> IO ()) -> IO ()) -> (EdgeIndex -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \EdgeIndex
v -> Solver -> EdgeIndex -> IO ()
computeVarProb Solver
solver EdgeIndex
v
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TMVar () -> () -> STM ()
forall a. TMVar a -> a -> STM ()
putTMVar TMVar ()
respVar ()
IO ()
loop
IO () -> IO ()
forall a. IO a -> IO a
restore IO ()
loop IO () -> (SomeException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` \(SomeException
e :: SomeException) -> STM () -> IO ()
forall a. STM a -> IO a
atomically (TMVar SomeException -> SomeException -> STM Bool
forall a. TMVar a -> a -> STM Bool
tryPutTMVar TMVar SomeException
ex SomeException
e STM Bool -> STM () -> STM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> STM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)
-> IO (ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)
forall (m :: * -> *) a. Monad m => a -> m a
return (ThreadId
th, MVar WorkerCommand
reqVar, TMVar ()
respVar, TMVar Double
respVar2)
let loop :: EdgeIndex -> IO Bool
loop !EdgeIndex
i
| Just EdgeIndex
l <- Maybe EdgeIndex
lim, EdgeIndex
i EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
>= EdgeIndex
l = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| Bool
otherwise = do
((ThreadId, MVar WorkerCommand, TMVar (), TMVar Double) -> IO ())
-> [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
-> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(ThreadId
_,MVar WorkerCommand
reqVar,TMVar ()
_,TMVar Double
_) -> MVar WorkerCommand -> WorkerCommand -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar WorkerCommand
reqVar WorkerCommand
WCUpdateEdgeProb) [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
workers
((ThreadId, MVar WorkerCommand, TMVar (), TMVar Double) -> IO ())
-> [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
-> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(ThreadId
_,MVar WorkerCommand
_,TMVar ()
respVar,TMVar Double
_) -> STM () -> IO ()
forall a. STM a -> IO a
wait (TMVar () -> STM ()
forall a. TMVar a -> STM a
takeTMVar TMVar ()
respVar)) [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
workers
((ThreadId, MVar WorkerCommand, TMVar (), TMVar Double) -> IO ())
-> [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
-> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(ThreadId
_,MVar WorkerCommand
reqVar,TMVar ()
_,TMVar Double
_) -> MVar WorkerCommand -> WorkerCommand -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar WorkerCommand
reqVar WorkerCommand
WCUpdateSurvey) [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
workers
Double
delta <- (Double
-> (ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)
-> IO Double)
-> Double
-> [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
-> IO Double
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Double
delta (ThreadId
_,MVar WorkerCommand
_,TMVar ()
_,TMVar Double
respVar2) -> Double -> Double -> Double
forall a. Ord a => a -> a -> a
max Double
delta (Double -> Double) -> IO Double -> IO Double
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM Double -> IO Double
forall a. STM a -> IO a
wait (TMVar Double -> STM Double
forall a. TMVar a -> STM a
takeTMVar TMVar Double
respVar2)) Double
0 [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
workers
if Double
delta Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
tol then do
((ThreadId, MVar WorkerCommand, TMVar (), TMVar Double) -> IO ())
-> [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
-> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(ThreadId
_,MVar WorkerCommand
reqVar,TMVar ()
_,TMVar Double
_) -> MVar WorkerCommand -> WorkerCommand -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar WorkerCommand
reqVar WorkerCommand
WCComputeVarProb) [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
workers
((ThreadId, MVar WorkerCommand, TMVar (), TMVar Double) -> IO ())
-> [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
-> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(ThreadId
_,MVar WorkerCommand
_,TMVar ()
respVar,TMVar Double
_) -> STM () -> IO ()
forall a. STM a -> IO a
wait (TMVar () -> STM ()
forall a. TMVar a -> STM a
takeTMVar TMVar ()
respVar)) [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
workers
((ThreadId, MVar WorkerCommand, TMVar (), TMVar Double) -> IO ())
-> [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
-> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(ThreadId
_,MVar WorkerCommand
reqVar,TMVar ()
_,TMVar Double
_) -> MVar WorkerCommand -> WorkerCommand -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar WorkerCommand
reqVar WorkerCommand
WCTerminate) [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
workers
Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
else
EdgeIndex -> IO Bool
loop (EdgeIndex
iEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+EdgeIndex
1)
Either SomeException Bool
ret <- IO Bool -> IO (Either SomeException Bool)
forall e a. Exception e => IO a -> IO (Either e a)
try (IO Bool -> IO (Either SomeException Bool))
-> IO Bool -> IO (Either SomeException Bool)
forall a b. (a -> b) -> a -> b
$ IO Bool -> IO Bool
forall a. IO a -> IO a
restore (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ EdgeIndex -> IO Bool
loop EdgeIndex
0
case Either SomeException Bool
ret of
Right Bool
b -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
Left (SomeException
e :: SomeException) -> do
((ThreadId, MVar WorkerCommand, TMVar (), TMVar Double) -> IO ())
-> [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
-> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(ThreadId
th,MVar WorkerCommand
_,TMVar ()
_,TMVar Double
_) -> ThreadId -> IO ()
killThread ThreadId
th) [(ThreadId, MVar WorkerCommand, TMVar (), TMVar Double)]
workers
SomeException -> IO Bool
forall e a. Exception e => e -> IO a
throwIO SomeException
e
updateEdgeProb :: Solver -> SAT.Var -> VUM.IOVector (L.Log Double) -> IO ()
updateEdgeProb :: Solver -> EdgeIndex -> IOVector (Log Double) -> IO ()
updateEdgeProb Solver
solver EdgeIndex
v IOVector (Log Double)
tmp = do
let i :: EdgeIndex
i = EdgeIndex
v EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1
edges :: Vector EdgeIndex
edges = Solver -> Vector (Vector EdgeIndex)
svVarEdges Solver
solver Vector (Vector EdgeIndex) -> EdgeIndex -> Vector EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
i
Maybe Bool
m <- MVector (PrimState IO) (Maybe Bool) -> EdgeIndex -> IO (Maybe Bool)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead (Solver -> IOVector (Maybe Bool)
svVarFixed Solver
solver) EdgeIndex
i
case Maybe Bool
m of
Just Bool
val -> do
Vector EdgeIndex -> (EdgeIndex -> IO ()) -> IO ()
forall (m :: * -> *) (v :: * -> *) a b.
(Monad m, Vector v a) =>
v a -> (a -> m b) -> m ()
VG.forM_ Vector EdgeIndex
edges ((EdgeIndex -> IO ()) -> IO ()) -> (EdgeIndex -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \EdgeIndex
e -> do
let lit :: EdgeIndex
lit = Solver -> Vector EdgeIndex
svEdgeLit Solver
solver Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
e
flag :: Bool
flag = (EdgeIndex
lit EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeIndex
0) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
val
MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite (Solver -> IOVector (Log Double)
svEdgeProbU Solver
solver) EdgeIndex
e (if Bool
flag then Log Double
0 else Log Double
1)
Maybe Bool
Nothing -> do
let f :: EdgeIndex -> Log Double -> Log Double -> IO ()
f !EdgeIndex
k !Log Double
val1_pre !Log Double
val2_pre
| EdgeIndex
k EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
>= Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length Vector EdgeIndex
edges = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = do
let e :: EdgeIndex
e = Vector EdgeIndex
edges Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
k
a :: EdgeIndex
a = Solver -> Vector EdgeIndex
svEdgeClause Solver
solver Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
e
MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite IOVector (Log Double)
MVector (PrimState IO) (Log Double)
tmp (EdgeIndex
kEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
*EdgeIndex
2) Log Double
val1_pre
MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite IOVector (Log Double)
MVector (PrimState IO) (Log Double)
tmp (EdgeIndex
kEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
*EdgeIndex
2EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+EdgeIndex
1) Log Double
val2_pre
Log Double
eta_ai <- MVector (PrimState IO) (Log Double) -> EdgeIndex -> IO (Log Double)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead (Solver -> IOVector (Log Double)
svEdgeSurvey Solver
solver) EdgeIndex
e
let w :: Double
w = Solver -> Vector Double
svClauseWeight Solver
solver Vector Double -> EdgeIndex -> Double
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
a
lit2 :: EdgeIndex
lit2 = Solver -> Vector EdgeIndex
svEdgeLit Solver
solver Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
e
val1_pre' :: Log Double
val1_pre' = if EdgeIndex
lit2 EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeIndex
0 then Log Double
val1_pre Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
eta_ai Log Double -> Double -> Log Double
forall a. Num a => Log a -> a -> Log a
^* Double
w else Log Double
val1_pre
val2_pre' :: Log Double
val2_pre' = if EdgeIndex
lit2 EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeIndex
0 then Log Double
val2_pre else Log Double
val2_pre Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
eta_ai Log Double -> Double -> Log Double
forall a. Num a => Log a -> a -> Log a
^* Double
w
EdgeIndex -> Log Double -> Log Double -> IO ()
f (EdgeIndex
kEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+EdgeIndex
1) Log Double
val1_pre' Log Double
val2_pre'
EdgeIndex -> Log Double -> Log Double -> IO ()
f EdgeIndex
0 Log Double
1 Log Double
1
let g :: EdgeIndex -> Log Double -> Log Double -> IO ()
g !EdgeIndex
k !Log Double
val1_post !Log Double
val2_post
| EdgeIndex
k EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
< EdgeIndex
0 = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = do
let e :: EdgeIndex
e = Vector EdgeIndex
edges Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
k
a :: EdgeIndex
a = Solver -> Vector EdgeIndex
svEdgeClause Solver
solver Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
e
lit2 :: EdgeIndex
lit2 = Solver -> Vector EdgeIndex
svEdgeLit Solver
solver Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
e
Log Double
val1_pre <- MVector (PrimState IO) (Log Double) -> EdgeIndex -> IO (Log Double)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead IOVector (Log Double)
MVector (PrimState IO) (Log Double)
tmp (EdgeIndex
kEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
*EdgeIndex
2)
Log Double
val2_pre <- MVector (PrimState IO) (Log Double) -> EdgeIndex -> IO (Log Double)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead IOVector (Log Double)
MVector (PrimState IO) (Log Double)
tmp (EdgeIndex
kEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
*EdgeIndex
2EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+EdgeIndex
1)
let val1 :: Log Double
val1 = Log Double
val1_pre Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
val1_post
val2 :: Log Double
val2 = Log Double
val2_pre Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
val2_post
Log Double
eta_ai <- MVector (PrimState IO) (Log Double) -> EdgeIndex -> IO (Log Double)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead (Solver -> IOVector (Log Double)
svEdgeSurvey Solver
solver) EdgeIndex
e
let w :: Double
w = Solver -> Vector Double
svClauseWeight Solver
solver Vector Double -> EdgeIndex -> Double
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
a
val1_post' :: Log Double
val1_post' = if EdgeIndex
lit2 EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeIndex
0 then Log Double
val1_post Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
eta_ai Log Double -> Double -> Log Double
forall a. Num a => Log a -> a -> Log a
^* Double
w else Log Double
val1_post
val2_post' :: Log Double
val2_post' = if EdgeIndex
lit2 EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeIndex
0 then Log Double
val2_post else Log Double
val2_post Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
eta_ai Log Double -> Double -> Log Double
forall a. Num a => Log a -> a -> Log a
^* Double
w
let pi_0 :: Log Double
pi_0 = Log Double
val1 Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
val2
pi_u :: Log Double
pi_u = if EdgeIndex
lit2 EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeIndex
0 then Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
val2 Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
val1 else Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
val1 Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
val2
pi_s :: Log Double
pi_s = if EdgeIndex
lit2 EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeIndex
0 then Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
val1 Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
val2 else Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
val2 Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
val1
MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite (Solver -> IOVector (Log Double)
svEdgeProbU Solver
solver) EdgeIndex
e (Log Double
pi_u Log Double -> Log Double -> Log Double
forall a. Fractional a => a -> a -> a
/ [Log Double] -> Log Double
forall a (f :: * -> *).
(RealFloat a, Foldable f) =>
f (Log a) -> Log a
L.sum [Log Double
pi_0, Log Double
pi_u, Log Double
pi_s])
EdgeIndex -> Log Double -> Log Double -> IO ()
g (EdgeIndex
kEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
-EdgeIndex
1) Log Double
val1_post' Log Double
val2_post'
EdgeIndex -> Log Double -> Log Double -> IO ()
g (Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length Vector EdgeIndex
edges EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1) Log Double
1 Log Double
1
updateEdgeSurvey :: Solver -> ClauseIndex -> VUM.IOVector (L.Log Double) -> IO Double
updateEdgeSurvey :: Solver -> EdgeIndex -> IOVector (Log Double) -> IO Double
updateEdgeSurvey Solver
solver EdgeIndex
a IOVector (Log Double)
tmp = do
let edges :: Vector EdgeIndex
edges = Solver -> Vector (Vector EdgeIndex)
svClauseEdges Solver
solver Vector (Vector EdgeIndex) -> EdgeIndex -> Vector EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
a
let f :: EdgeIndex -> Log Double -> IO ()
f !EdgeIndex
k !Log Double
p_pre
| EdgeIndex
k EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
>= Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length Vector EdgeIndex
edges = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = do
let e :: EdgeIndex
e = Vector EdgeIndex
edges Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
k
MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite IOVector (Log Double)
MVector (PrimState IO) (Log Double)
tmp EdgeIndex
k Log Double
p_pre
Log Double
p <- MVector (PrimState IO) (Log Double) -> EdgeIndex -> IO (Log Double)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead (Solver -> IOVector (Log Double)
svEdgeProbU Solver
solver) EdgeIndex
e
EdgeIndex -> Log Double -> IO ()
f (EdgeIndex
kEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
+EdgeIndex
1) (Log Double
p_pre Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
p)
let g :: EdgeIndex -> Log Double -> Double -> IO Double
g !EdgeIndex
k !Log Double
p_post !Double
maxDelta
| EdgeIndex
k EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
< EdgeIndex
0 = Double -> IO Double
forall (m :: * -> *) a. Monad m => a -> m a
return Double
maxDelta
| Bool
otherwise = do
let e :: EdgeIndex
e = Vector EdgeIndex
edges Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
k
Log Double
p_pre <- MVector (PrimState IO) (Log Double) -> EdgeIndex -> IO (Log Double)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead IOVector (Log Double)
MVector (PrimState IO) (Log Double)
tmp EdgeIndex
k
Log Double
p <- MVector (PrimState IO) (Log Double) -> EdgeIndex -> IO (Log Double)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead (Solver -> IOVector (Log Double)
svEdgeProbU Solver
solver) EdgeIndex
e
Log Double
eta_ai <- MVector (PrimState IO) (Log Double) -> EdgeIndex -> IO (Log Double)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead (Solver -> IOVector (Log Double)
svEdgeSurvey Solver
solver) EdgeIndex
e
let eta_ai' :: Log Double
eta_ai' = Log Double
p_pre Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
p_post
MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite (Solver -> IOVector (Log Double)
svEdgeSurvey Solver
solver) EdgeIndex
e Log Double
eta_ai'
let delta :: Double
delta = Double -> Double
forall a. Num a => a -> a
abs (Log Double -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac Log Double
eta_ai' Double -> Double -> Double
forall a. Num a => a -> a -> a
- Log Double -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac Log Double
eta_ai)
EdgeIndex -> Log Double -> Double -> IO Double
g (EdgeIndex
kEdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
-EdgeIndex
1) (Log Double
p_post Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
p) (Double -> Double -> Double
forall a. Ord a => a -> a -> a
max Double
delta Double
maxDelta)
EdgeIndex -> Log Double -> IO ()
f EdgeIndex
0 Log Double
1
EdgeIndex -> Log Double -> Double -> IO Double
g (Vector EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex
VG.length Vector EdgeIndex
edges EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1) Log Double
1 Double
0
computeVarProb :: Solver -> SAT.Var -> IO ()
computeVarProb :: Solver -> EdgeIndex -> IO ()
computeVarProb Solver
solver EdgeIndex
v = do
let i :: EdgeIndex
i = EdgeIndex
v EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1
f :: (Log Double, Log Double)
-> EdgeIndex -> IO (Log Double, Log Double)
f (Log Double
val1,Log Double
val2) EdgeIndex
e = do
let lit :: EdgeIndex
lit = Solver -> Vector EdgeIndex
svEdgeLit Solver
solver Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
e
a :: EdgeIndex
a = Solver -> Vector EdgeIndex
svEdgeClause Solver
solver Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
e
w :: Double
w = Solver -> Vector Double
svClauseWeight Solver
solver Vector Double -> EdgeIndex -> Double
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
a
Log Double
eta_ai <- MVector (PrimState IO) (Log Double) -> EdgeIndex -> IO (Log Double)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead (Solver -> IOVector (Log Double)
svEdgeSurvey Solver
solver) EdgeIndex
e
let val1' :: Log Double
val1' = if EdgeIndex
lit EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeIndex
0 then Log Double
val1 Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
eta_ai Log Double -> Double -> Log Double
forall a. Num a => Log a -> a -> Log a
^* Double
w else Log Double
val1
val2' :: Log Double
val2' = if EdgeIndex
lit EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
< EdgeIndex
0 then Log Double
val2 Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
eta_ai Log Double -> Double -> Log Double
forall a. Num a => Log a -> a -> Log a
^* Double
w else Log Double
val2
(Log Double, Log Double) -> IO (Log Double, Log Double)
forall (m :: * -> *) a. Monad m => a -> m a
return (Log Double
val1',Log Double
val2')
(Log Double
val1,Log Double
val2) <- ((Log Double, Log Double)
-> EdgeIndex -> IO (Log Double, Log Double))
-> (Log Double, Log Double)
-> Vector EdgeIndex
-> IO (Log Double, Log Double)
forall (m :: * -> *) (v :: * -> *) b a.
(Monad m, Vector v b) =>
(a -> b -> m a) -> a -> v b -> m a
VG.foldM' (Log Double, Log Double)
-> EdgeIndex -> IO (Log Double, Log Double)
f (Log Double
1,Log Double
1) (Solver -> Vector (Vector EdgeIndex)
svVarEdges Solver
solver Vector (Vector EdgeIndex) -> EdgeIndex -> Vector EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
i)
let p0 :: Log Double
p0 = Log Double
val1 Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
val2
pp :: Log Double
pp = Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
val1 Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
val2
pn :: Log Double
pn = Log Double -> Log Double
forall a. RealFloat a => Log a -> Log a
comp Log Double
val2 Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
* Log Double
val1
let wp :: Log Double
wp = Log Double
pp Log Double -> Log Double -> Log Double
forall a. Fractional a => a -> a -> a
/ (Log Double
pp Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
+ Log Double
pn Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
+ Log Double
p0)
wn :: Log Double
wn = Log Double
pn Log Double -> Log Double -> Log Double
forall a. Fractional a => a -> a -> a
/ (Log Double
pp Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
+ Log Double
pn Log Double -> Log Double -> Log Double
forall a. Num a => a -> a -> a
+ Log Double
p0)
MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite (Solver -> IOVector (Log Double)
svVarProbT Solver
solver) EdgeIndex
i Log Double
wp
MVector (PrimState IO) (Log Double)
-> EdgeIndex -> Log Double -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite (Solver -> IOVector (Log Double)
svVarProbF Solver
solver) EdgeIndex
i Log Double
wn
getVarProb :: Solver -> SAT.Var -> IO (Double, Double, Double)
getVarProb :: Solver -> EdgeIndex -> IO (Double, Double, Double)
getVarProb Solver
solver EdgeIndex
v = do
Double
pt <- Log Double -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Log Double -> Double) -> IO (Log Double) -> IO Double
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MVector (PrimState IO) (Log Double) -> EdgeIndex -> IO (Log Double)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead (Solver -> IOVector (Log Double)
svVarProbT Solver
solver) (EdgeIndex
v EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1)
Double
pf <- Log Double -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Log Double -> Double) -> IO (Log Double) -> IO Double
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MVector (PrimState IO) (Log Double) -> EdgeIndex -> IO (Log Double)
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> m a
VGM.unsafeRead (Solver -> IOVector (Log Double)
svVarProbF Solver
solver) (EdgeIndex
v EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1)
(Double, Double, Double) -> IO (Double, Double, Double)
forall (m :: * -> *) a. Monad m => a -> m a
return (Double
pt, Double
pf, Double
1 Double -> Double -> Double
forall a. Num a => a -> a -> a
- (Double
pt Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
pf))
fixLit :: Solver -> SAT.Lit -> IO ()
fixLit :: Solver -> EdgeIndex -> IO ()
fixLit Solver
solver EdgeIndex
lit = do
MVector (PrimState IO) (Maybe Bool)
-> EdgeIndex -> Maybe Bool -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite (Solver -> IOVector (Maybe Bool)
svVarFixed Solver
solver) (EdgeIndex -> EdgeIndex
forall a. Num a => a -> a
abs EdgeIndex
lit EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1) (if EdgeIndex
lit EdgeIndex -> EdgeIndex -> Bool
forall a. Ord a => a -> a -> Bool
> EdgeIndex
0 then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True else Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False)
unfixLit :: Solver -> SAT.Lit -> IO ()
unfixLit :: Solver -> EdgeIndex -> IO ()
unfixLit Solver
solver EdgeIndex
lit = do
MVector (PrimState IO) (Maybe Bool)
-> EdgeIndex -> Maybe Bool -> IO ()
forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> EdgeIndex -> a -> m ()
VGM.unsafeWrite (Solver -> IOVector (Maybe Bool)
svVarFixed Solver
solver) (EdgeIndex -> EdgeIndex
forall a. Num a => a -> a
abs EdgeIndex
lit EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1) Maybe Bool
forall a. Maybe a
Nothing
printInfo :: Solver -> IO ()
printInfo :: Solver -> IO ()
printInfo Solver
solver = do
(Vector (Log Double)
surveys :: VU.Vector (L.Log Double)) <- Mutable Vector (PrimState IO) (Log Double)
-> IO (Vector (Log Double))
forall (m :: * -> *) (v :: * -> *) a.
(PrimMonad m, Vector v a) =>
Mutable v (PrimState m) a -> m (v a)
VG.freeze (Solver -> IOVector (Log Double)
svEdgeSurvey Solver
solver)
(Vector (Log Double)
u :: VU.Vector (L.Log Double)) <- Mutable Vector (PrimState IO) (Log Double)
-> IO (Vector (Log Double))
forall (m :: * -> *) (v :: * -> *) a.
(PrimMonad m, Vector v a) =>
Mutable v (PrimState m) a -> m (v a)
VG.freeze (Solver -> IOVector (Log Double)
svEdgeProbU Solver
solver)
let xs :: [(EdgeIndex, EdgeIndex, Log Double, Log Double)]
xs = [(EdgeIndex
clause, EdgeIndex
lit, Log Double
eta, Vector (Log Double)
u Vector (Log Double) -> EdgeIndex -> Log Double
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
e) | (EdgeIndex
e, Log Double
eta) <- [EdgeIndex] -> [Log Double] -> [(EdgeIndex, Log Double)]
forall a b. [a] -> [b] -> [(a, b)]
zip [EdgeIndex
0..] (Vector (Log Double) -> [Log Double]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector (Log Double)
surveys), let lit :: EdgeIndex
lit = Solver -> Vector EdgeIndex
svEdgeLit Solver
solver Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
e, let clause :: EdgeIndex
clause = Solver -> Vector EdgeIndex
svEdgeClause Solver
solver Vector EdgeIndex -> EdgeIndex -> EdgeIndex
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
e]
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"edges: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(EdgeIndex, EdgeIndex, Log Double, Log Double)] -> String
forall a. Show a => a -> String
show [(EdgeIndex, EdgeIndex, Log Double, Log Double)]
xs
(Vector (Log Double)
pt :: VU.Vector (L.Log Double)) <- Mutable Vector (PrimState IO) (Log Double)
-> IO (Vector (Log Double))
forall (m :: * -> *) (v :: * -> *) a.
(PrimMonad m, Vector v a) =>
Mutable v (PrimState m) a -> m (v a)
VG.freeze (Solver -> IOVector (Log Double)
svVarProbT Solver
solver)
(Vector (Log Double)
pf :: VU.Vector (L.Log Double)) <- Mutable Vector (PrimState IO) (Log Double)
-> IO (Vector (Log Double))
forall (m :: * -> *) (v :: * -> *) a.
(PrimMonad m, Vector v a) =>
Mutable v (PrimState m) a -> m (v a)
VG.freeze (Solver -> IOVector (Log Double)
svVarProbF Solver
solver)
EdgeIndex
nv <- Solver -> IO EdgeIndex
getNVars Solver
solver
let xs2 :: [(EdgeIndex, Double, Double, Double)]
xs2 = [(EdgeIndex
v, Log Double -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Vector (Log Double)
pt Vector (Log Double) -> EdgeIndex -> Log Double
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
i) :: Double, Log Double -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Vector (Log Double)
pf Vector (Log Double) -> EdgeIndex -> Log Double
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
i) :: Double, Log Double -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Vector (Log Double)
pt Vector (Log Double) -> EdgeIndex -> Log Double
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
i) Double -> Double -> Double
forall a. Num a => a -> a -> a
- Log Double -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Vector (Log Double)
pf Vector (Log Double) -> EdgeIndex -> Log Double
forall (v :: * -> *) a. Vector v a => v a -> EdgeIndex -> a
! EdgeIndex
i) :: Double) | EdgeIndex
v <- [EdgeIndex
1..EdgeIndex
nv], let i :: EdgeIndex
i = EdgeIndex
v EdgeIndex -> EdgeIndex -> EdgeIndex
forall a. Num a => a -> a -> a
- EdgeIndex
1]
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"vars: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(EdgeIndex, Double, Double, Double)] -> String
forall a. Show a => a -> String
show [(EdgeIndex, Double, Double, Double)]
xs2