{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module ToySolver.SAT.Solver.SLS.ProbSAT
( Solver
, newSolver
, newSolverWeighted
, getNumVars
, getRandomGen
, setRandomGen
, getBestSolution
, getStatistics
, Options (..)
, Callbacks (..)
, Statistics (..)
, generateUniformRandomSolution
, probsat
, walksat
) where
import Prelude hiding (break)
import Control.Exception
import Control.Loop
import Control.Monad
import Control.Monad.Primitive
import Control.Monad.Trans
import Control.Monad.Trans.Except
import Data.Array.Base (unsafeRead, unsafeWrite, unsafeAt)
import Data.Array.IArray
import Data.Array.IO
import Data.Array.Unboxed
import Data.Array.Unsafe
import Data.Bits
import Data.Default.Class
import qualified Data.Foldable as F
import Data.Int
import Data.IORef
import Data.Maybe
import Data.Sequence ((|>))
import qualified Data.Sequence as Seq
import Data.Typeable
import Data.Word
import System.Clock
import qualified System.Random.MWC as Rand
import qualified System.Random.MWC.Distributions as Rand
import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.Internal.Data.IOURef
import qualified ToySolver.Internal.Data.Vec as Vec
import qualified ToySolver.SAT.Types as SAT
data Solver
= Solver
{ Solver -> Array ClauseId PackedClause
svClauses :: !(Array ClauseId PackedClause)
, Solver -> Array ClauseId Weight
svClauseWeights :: !(Array ClauseId CNF.Weight)
, Solver -> UArray ClauseId Double
svClauseWeightsF :: !(UArray ClauseId Double)
, Solver -> IOUArray ClauseId Int32
svClauseNumTrueLits :: !(IOUArray ClauseId Int32)
, Solver -> IOUArray ClauseId ClauseId
svClauseUnsatClauseIndex :: !(IOUArray ClauseId Int)
, Solver -> UVec ClauseId
svUnsatClauses :: !(Vec.UVec ClauseId)
, Solver -> Array ClauseId (UArray ClauseId ClauseId)
svVarOccurs :: !(Array SAT.Var (UArray Int ClauseId))
, :: !(Array SAT.Var (IOUArray Int Bool))
, Solver -> IOUArray ClauseId Bool
svSolution :: !(IOUArray SAT.Var Bool)
, Solver -> IORef Weight
svObj :: !(IORef CNF.Weight)
, Solver -> IORef GenIO
svRandomGen :: !(IORef Rand.GenIO)
, Solver -> IORef (Weight, Model)
svBestSolution :: !(IORef (CNF.Weight, SAT.Model))
, Solver -> IORef Statistics
svStatistics :: !(IORef Statistics)
}
type ClauseId = Int
type PackedClause = Array Int SAT.Lit
newSolver :: CNF.CNF -> IO Solver
newSolver :: CNF -> IO Solver
newSolver CNF
cnf = do
let wcnf :: WCNF
wcnf =
WCNF :: ClauseId -> ClauseId -> Weight -> [WeightedClause] -> WCNF
CNF.WCNF
{ wcnfNumVars :: ClauseId
CNF.wcnfNumVars = CNF -> ClauseId
CNF.cnfNumVars CNF
cnf
, wcnfNumClauses :: ClauseId
CNF.wcnfNumClauses = CNF -> ClauseId
CNF.cnfNumClauses CNF
cnf
, wcnfTopCost :: Weight
CNF.wcnfTopCost = ClauseId -> Weight
forall a b. (Integral a, Num b) => a -> b
fromIntegral (CNF -> ClauseId
CNF.cnfNumClauses CNF
cnf) Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
+ Weight
1
, wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = [(Weight
1,PackedClause
c) | PackedClause
c <- CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf]
}
WCNF -> IO Solver
newSolverWeighted WCNF
wcnf
newSolverWeighted :: CNF.WCNF -> IO Solver
newSolverWeighted :: WCNF -> IO Solver
newSolverWeighted WCNF
wcnf = do
let m :: SAT.Var -> Bool
m :: ClauseId -> Bool
m ClauseId
_ = Bool
False
nv :: ClauseId
nv = WCNF -> ClauseId
CNF.wcnfNumVars WCNF
wcnf
IORef Weight
objRef <- Weight -> IO (IORef Weight)
forall a. a -> IO (IORef a)
newIORef (Weight
0::Integer)
[(Weight, PackedClause)]
cs <- ([Maybe (Weight, PackedClause)] -> [(Weight, PackedClause)])
-> IO [Maybe (Weight, PackedClause)] -> IO [(Weight, PackedClause)]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Maybe (Weight, PackedClause)] -> [(Weight, PackedClause)]
forall a. [Maybe a] -> [a]
catMaybes (IO [Maybe (Weight, PackedClause)] -> IO [(Weight, PackedClause)])
-> IO [Maybe (Weight, PackedClause)] -> IO [(Weight, PackedClause)]
forall a b. (a -> b) -> a -> b
$ [WeightedClause]
-> (WeightedClause -> IO (Maybe (Weight, PackedClause)))
-> IO [Maybe (Weight, PackedClause)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (WCNF -> [WeightedClause]
CNF.wcnfClauses WCNF
wcnf) ((WeightedClause -> IO (Maybe (Weight, PackedClause)))
-> IO [Maybe (Weight, PackedClause)])
-> (WeightedClause -> IO (Maybe (Weight, PackedClause)))
-> IO [Maybe (Weight, PackedClause)]
forall a b. (a -> b) -> a -> b
$ \(Weight
w,PackedClause
pc) -> do
case Clause -> Maybe Clause
SAT.normalizeClause (PackedClause -> Clause
SAT.unpackClause PackedClause
pc) of
Maybe Clause
Nothing -> Maybe (Weight, PackedClause) -> IO (Maybe (Weight, PackedClause))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Weight, PackedClause)
forall a. Maybe a
Nothing
Just [] -> IORef Weight -> (Weight -> Weight) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Weight
objRef (Weight
wWeight -> Weight -> Weight
forall a. Num a => a -> a -> a
+) IO ()
-> IO (Maybe (Weight, PackedClause))
-> IO (Maybe (Weight, PackedClause))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (Weight, PackedClause) -> IO (Maybe (Weight, PackedClause))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Weight, PackedClause)
forall a. Maybe a
Nothing
Just Clause
c -> do
let c' :: PackedClause
c' = (ClauseId, ClauseId) -> Clause -> PackedClause
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (ClauseId
0, Clause -> ClauseId
forall (t :: * -> *) a. Foldable t => t a -> ClauseId
length Clause
c ClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
- ClauseId
1) Clause
c
PackedClause
-> IO (Maybe (Weight, PackedClause))
-> IO (Maybe (Weight, PackedClause))
seq PackedClause
c' (IO (Maybe (Weight, PackedClause))
-> IO (Maybe (Weight, PackedClause)))
-> IO (Maybe (Weight, PackedClause))
-> IO (Maybe (Weight, PackedClause))
forall a b. (a -> b) -> a -> b
$ Maybe (Weight, PackedClause) -> IO (Maybe (Weight, PackedClause))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Weight, PackedClause) -> Maybe (Weight, PackedClause)
forall a. a -> Maybe a
Just (Weight
w,PackedClause
c'))
let len :: ClauseId
len = [(Weight, PackedClause)] -> ClauseId
forall (t :: * -> *) a. Foldable t => t a -> ClauseId
length [(Weight, PackedClause)]
cs
clauses :: Array ClauseId PackedClause
clauses = (ClauseId, ClauseId)
-> [PackedClause] -> Array ClauseId PackedClause
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (ClauseId
0, ClauseId
len ClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
- ClauseId
1) (((Weight, PackedClause) -> PackedClause)
-> [(Weight, PackedClause)] -> [PackedClause]
forall a b. (a -> b) -> [a] -> [b]
map (Weight, PackedClause) -> PackedClause
forall a b. (a, b) -> b
snd [(Weight, PackedClause)]
cs)
weights :: Array ClauseId CNF.Weight
weights :: Array ClauseId Weight
weights = (ClauseId, ClauseId) -> [Weight] -> Array ClauseId Weight
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (ClauseId
0, ClauseId
len ClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
- ClauseId
1) (((Weight, PackedClause) -> Weight)
-> [(Weight, PackedClause)] -> [Weight]
forall a b. (a -> b) -> [a] -> [b]
map (Weight, PackedClause) -> Weight
forall a b. (a, b) -> a
fst [(Weight, PackedClause)]
cs)
weightsF :: UArray ClauseId Double
weightsF :: UArray ClauseId Double
weightsF = (ClauseId, ClauseId) -> [Double] -> UArray ClauseId Double
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (ClauseId
0, ClauseId
len ClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
- ClauseId
1) (((Weight, PackedClause) -> Double)
-> [(Weight, PackedClause)] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map (Weight -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Weight -> Double)
-> ((Weight, PackedClause) -> Weight)
-> (Weight, PackedClause)
-> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Weight, PackedClause) -> Weight
forall a b. (a, b) -> a
fst) [(Weight, PackedClause)]
cs)
(IOArray ClauseId (Seq (ClauseId, Bool))
varOccurs' :: IOArray SAT.Var (Seq.Seq (Int, Bool))) <- (ClauseId, ClauseId)
-> Seq (ClauseId, Bool)
-> IO (IOArray ClauseId (Seq (ClauseId, Bool)))
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (ClauseId
1, ClauseId
nv) Seq (ClauseId, Bool)
forall a. Seq a
Seq.empty
IOUArray ClauseId Int32
clauseNumTrueLits <- (ClauseId, ClauseId) -> Int32 -> IO (IOUArray ClauseId Int32)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (Array ClauseId PackedClause -> (ClauseId, ClauseId)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Array ClauseId PackedClause
clauses) Int32
0
IOUArray ClauseId ClauseId
clauseUnsatClauseIndex <- (ClauseId, ClauseId) -> ClauseId -> IO (IOUArray ClauseId ClauseId)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (Array ClauseId PackedClause -> (ClauseId, ClauseId)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Array ClauseId PackedClause
clauses) (-ClauseId
1)
UVec ClauseId
unsatClauses <- IO (UVec ClauseId)
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
Array ClauseId PackedClause
-> ((ClauseId, PackedClause) -> IO ()) -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a ClauseId e -> ((ClauseId, e) -> m ()) -> m ()
forAssocsM_ Array ClauseId PackedClause
clauses (((ClauseId, PackedClause) -> IO ()) -> IO ())
-> ((ClauseId, PackedClause) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(ClauseId
c,PackedClause
clause) -> do
let n :: Int32
n = [Int32] -> Int32
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int32
1 | ClauseId
lit <- PackedClause -> Clause
forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems PackedClause
clause, (ClauseId -> Bool) -> ClauseId -> Bool
forall m. IModel m => m -> ClauseId -> Bool
SAT.evalLit ClauseId -> Bool
m ClauseId
lit]
IOUArray ClauseId Int32 -> ClauseId -> Int32 -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray ClauseId Int32
clauseNumTrueLits ClauseId
c Int32
n
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int32
n Int32 -> Int32 -> Bool
forall a. Eq a => a -> a -> Bool
== Int32
0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
ClauseId
i <- UVec ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e. GenericVec a e -> IO ClauseId
Vec.getSize UVec ClauseId
unsatClauses
IOUArray ClauseId ClauseId -> ClauseId -> ClauseId -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray ClauseId ClauseId
clauseUnsatClauseIndex ClauseId
c ClauseId
i
UVec ClauseId -> ClauseId -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec ClauseId
unsatClauses ClauseId
c
IORef Weight -> (Weight -> Weight) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef Weight
objRef ((Array ClauseId Weight
weights Array ClauseId Weight -> ClauseId -> Weight
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! ClauseId
c) Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
+)
Clause -> (ClauseId -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (PackedClause -> Clause
forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems PackedClause
clause) ((ClauseId -> IO ()) -> IO ()) -> (ClauseId -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \ClauseId
lit -> do
let v :: ClauseId
v = ClauseId -> ClauseId
SAT.litVar ClauseId
lit
let b :: Bool
b = (ClauseId -> Bool) -> ClauseId -> Bool
forall m. IModel m => m -> ClauseId -> Bool
SAT.evalLit ClauseId -> Bool
m ClauseId
lit
Bool -> IO () -> IO ()
seq Bool
b (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ IOArray ClauseId (Seq (ClauseId, Bool))
-> ClauseId
-> (Seq (ClauseId, Bool) -> Seq (ClauseId, Bool))
-> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> (e -> e) -> m ()
modifyArray IOArray ClauseId (Seq (ClauseId, Bool))
varOccurs' ClauseId
v (Seq (ClauseId, Bool) -> (ClauseId, Bool) -> Seq (ClauseId, Bool)
forall a. Seq a -> a -> Seq a
|> (ClauseId
c,Bool
b))
Array ClauseId (UArray ClauseId ClauseId)
varOccurs <- do
(IOArray ClauseId (UArray ClauseId ClauseId)
arr::IOArray SAT.Var (UArray Int ClauseId)) <- (ClauseId, ClauseId)
-> IO (IOArray ClauseId (UArray ClauseId ClauseId))
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (ClauseId
1, ClauseId
nv)
Clause -> (ClauseId -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ClauseId
1 .. ClauseId
nv] ((ClauseId -> IO ()) -> IO ()) -> (ClauseId -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \ClauseId
v -> do
Seq (ClauseId, Bool)
s <- IOArray ClauseId (Seq (ClauseId, Bool))
-> ClauseId -> IO (Seq (ClauseId, Bool))
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray IOArray ClauseId (Seq (ClauseId, Bool))
varOccurs' ClauseId
v
IOArray ClauseId (UArray ClauseId ClauseId)
-> ClauseId -> UArray ClauseId ClauseId -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOArray ClauseId (UArray ClauseId ClauseId)
arr ClauseId
v (UArray ClauseId ClauseId -> IO ())
-> UArray ClauseId ClauseId -> IO ()
forall a b. (a -> b) -> a -> b
$ (ClauseId, ClauseId) -> Clause -> UArray ClauseId ClauseId
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (ClauseId
0, Seq (ClauseId, Bool) -> ClauseId
forall a. Seq a -> ClauseId
Seq.length Seq (ClauseId, Bool)
s ClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
- ClauseId
1) (((ClauseId, Bool) -> ClauseId) -> [(ClauseId, Bool)] -> Clause
forall a b. (a -> b) -> [a] -> [b]
map (ClauseId, Bool) -> ClauseId
forall a b. (a, b) -> a
fst (Seq (ClauseId, Bool) -> [(ClauseId, Bool)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (ClauseId, Bool)
s))
IOArray ClauseId (UArray ClauseId ClauseId)
-> IO (Array ClauseId (UArray ClauseId ClauseId))
forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
unsafeFreeze IOArray ClauseId (UArray ClauseId ClauseId)
arr
Array ClauseId (IOUArray ClauseId Bool)
varOccursState <- do
(IOArray ClauseId (IOUArray ClauseId Bool)
arr::IOArray SAT.Var (IOUArray Int Bool)) <- (ClauseId, ClauseId)
-> IO (IOArray ClauseId (IOUArray ClauseId Bool))
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (ClauseId
1, ClauseId
nv)
Clause -> (ClauseId -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ClauseId
1 .. ClauseId
nv] ((ClauseId -> IO ()) -> IO ()) -> (ClauseId -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \ClauseId
v -> do
Seq (ClauseId, Bool)
s <- IOArray ClauseId (Seq (ClauseId, Bool))
-> ClauseId -> IO (Seq (ClauseId, Bool))
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray IOArray ClauseId (Seq (ClauseId, Bool))
varOccurs' ClauseId
v
IOUArray ClauseId Bool
ss <- (ClauseId, ClauseId) -> IO (IOUArray ClauseId Bool)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (ClauseId
0, Seq (ClauseId, Bool) -> ClauseId
forall a. Seq a -> ClauseId
Seq.length Seq (ClauseId, Bool)
s ClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
- ClauseId
1)
[(ClauseId, (ClauseId, Bool))]
-> ((ClauseId, (ClauseId, Bool)) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Clause -> [(ClauseId, Bool)] -> [(ClauseId, (ClauseId, Bool))]
forall a b. [a] -> [b] -> [(a, b)]
zip [ClauseId
0..] (Seq (ClauseId, Bool) -> [(ClauseId, Bool)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (ClauseId, Bool)
s)) (((ClauseId, (ClauseId, Bool)) -> IO ()) -> IO ())
-> ((ClauseId, (ClauseId, Bool)) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(ClauseId
j,(ClauseId, Bool)
a) -> IOUArray ClauseId Bool -> ClauseId -> Bool -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray ClauseId Bool
ss ClauseId
j ((ClauseId, Bool) -> Bool
forall a b. (a, b) -> b
snd (ClauseId, Bool)
a)
IOArray ClauseId (IOUArray ClauseId Bool)
-> ClauseId -> IOUArray ClauseId Bool -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOArray ClauseId (IOUArray ClauseId Bool)
arr ClauseId
v IOUArray ClauseId Bool
ss
IOArray ClauseId (IOUArray ClauseId Bool)
-> IO (Array ClauseId (IOUArray ClauseId Bool))
forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
unsafeFreeze IOArray ClauseId (IOUArray ClauseId Bool)
arr
IOUArray ClauseId Bool
solution <- (ClauseId, ClauseId) -> [Bool] -> IO (IOUArray ClauseId Bool)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> [e] -> m (a i e)
newListArray (ClauseId
1, ClauseId
nv) ([Bool] -> IO (IOUArray ClauseId Bool))
-> [Bool] -> IO (IOUArray ClauseId Bool)
forall a b. (a -> b) -> a -> b
$ [(ClauseId -> Bool) -> ClauseId -> Bool
forall m. IModel m => m -> ClauseId -> Bool
SAT.evalVar ClauseId -> Bool
m ClauseId
v | ClauseId
v <- [ClauseId
1..ClauseId
nv]]
Weight
bestObj <- IORef Weight -> IO Weight
forall a. IORef a -> IO a
readIORef IORef Weight
objRef
Model
bestSol <- IOUArray ClauseId Bool -> IO Model
forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
freeze IOUArray ClauseId Bool
solution
IORef (Weight, Model)
bestSolution <- (Weight, Model) -> IO (IORef (Weight, Model))
forall a. a -> IO (IORef a)
newIORef (Weight
bestObj, Model
bestSol)
IORef (Gen RealWorld)
randGen <- Gen RealWorld -> IO (IORef (Gen RealWorld))
forall a. a -> IO (IORef a)
newIORef (Gen RealWorld -> IO (IORef (Gen RealWorld)))
-> IO (Gen RealWorld) -> IO (IORef (Gen RealWorld))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (Gen RealWorld)
forall (m :: * -> *). PrimMonad m => m (Gen (PrimState m))
Rand.create
IORef Statistics
stat <- Statistics -> IO (IORef Statistics)
forall a. a -> IO (IORef a)
newIORef Statistics
forall a. Default a => a
def
Solver -> IO Solver
forall (m :: * -> *) a. Monad m => a -> m a
return (Solver -> IO Solver) -> Solver -> IO Solver
forall a b. (a -> b) -> a -> b
$
Solver :: Array ClauseId PackedClause
-> Array ClauseId Weight
-> UArray ClauseId Double
-> IOUArray ClauseId Int32
-> IOUArray ClauseId ClauseId
-> UVec ClauseId
-> Array ClauseId (UArray ClauseId ClauseId)
-> Array ClauseId (IOUArray ClauseId Bool)
-> IOUArray ClauseId Bool
-> IORef Weight
-> IORef GenIO
-> IORef (Weight, Model)
-> IORef Statistics
-> Solver
Solver
{ svClauses :: Array ClauseId PackedClause
svClauses = Array ClauseId PackedClause
clauses
, svClauseWeights :: Array ClauseId Weight
svClauseWeights = Array ClauseId Weight
weights
, svClauseWeightsF :: UArray ClauseId Double
svClauseWeightsF = UArray ClauseId Double
weightsF
, svClauseNumTrueLits :: IOUArray ClauseId Int32
svClauseNumTrueLits = IOUArray ClauseId Int32
clauseNumTrueLits
, svClauseUnsatClauseIndex :: IOUArray ClauseId ClauseId
svClauseUnsatClauseIndex = IOUArray ClauseId ClauseId
clauseUnsatClauseIndex
, svUnsatClauses :: UVec ClauseId
svUnsatClauses = UVec ClauseId
unsatClauses
, svVarOccurs :: Array ClauseId (UArray ClauseId ClauseId)
svVarOccurs = Array ClauseId (UArray ClauseId ClauseId)
varOccurs
, svVarOccursState :: Array ClauseId (IOUArray ClauseId Bool)
svVarOccursState = Array ClauseId (IOUArray ClauseId Bool)
varOccursState
, svSolution :: IOUArray ClauseId Bool
svSolution = IOUArray ClauseId Bool
solution
, svObj :: IORef Weight
svObj = IORef Weight
objRef
, svRandomGen :: IORef GenIO
svRandomGen = IORef (Gen RealWorld)
IORef GenIO
randGen
, svBestSolution :: IORef (Weight, Model)
svBestSolution = IORef (Weight, Model)
bestSolution
, svStatistics :: IORef Statistics
svStatistics = IORef Statistics
stat
}
flipVar :: Solver -> SAT.Var -> IO ()
flipVar :: Solver -> ClauseId -> IO ()
flipVar Solver
solver ClauseId
v = IO () -> IO ()
forall a. IO a -> IO a
mask_ (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
let occurs :: UArray ClauseId ClauseId
occurs = Solver -> Array ClauseId (UArray ClauseId ClauseId)
svVarOccurs Solver
solver Array ClauseId (UArray ClauseId ClauseId)
-> ClauseId -> UArray ClauseId ClauseId
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! ClauseId
v
occursState :: IOUArray ClauseId Bool
occursState = Solver -> Array ClauseId (IOUArray ClauseId Bool)
svVarOccursState Solver
solver Array ClauseId (IOUArray ClauseId Bool)
-> ClauseId -> IOUArray ClauseId Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! ClauseId
v
UArray ClauseId ClauseId -> IO () -> IO ()
seq UArray ClauseId ClauseId
occurs (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ IOUArray ClauseId Bool -> IO () -> IO ()
seq IOUArray ClauseId Bool
occursState (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
IOUArray ClauseId Bool -> ClauseId -> (Bool -> Bool) -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> (e -> e) -> m ()
modifyArray (Solver -> IOUArray ClauseId Bool
svSolution Solver
solver) ClauseId
v Bool -> Bool
not
UArray ClauseId ClauseId
-> ((ClauseId, ClauseId) -> IO ()) -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a ClauseId e -> ((ClauseId, e) -> m ()) -> m ()
forAssocsM_ UArray ClauseId ClauseId
occurs (((ClauseId, ClauseId) -> IO ()) -> IO ())
-> ((ClauseId, ClauseId) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(ClauseId
j,!ClauseId
c) -> do
Bool
b <- IOUArray ClauseId Bool -> ClauseId -> IO Bool
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> ClauseId -> m e
unsafeRead IOUArray ClauseId Bool
occursState ClauseId
j
Int32
n <- IOUArray ClauseId Int32 -> ClauseId -> IO Int32
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> ClauseId -> m e
unsafeRead (Solver -> IOUArray ClauseId Int32
svClauseNumTrueLits Solver
solver) ClauseId
c
IOUArray ClauseId Bool -> ClauseId -> Bool -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> ClauseId -> e -> m ()
unsafeWrite IOUArray ClauseId Bool
occursState ClauseId
j (Bool -> Bool
not Bool
b)
if Bool
b then do
IOUArray ClauseId Int32 -> ClauseId -> Int32 -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> ClauseId -> e -> m ()
unsafeWrite (Solver -> IOUArray ClauseId Int32
svClauseNumTrueLits Solver
solver) ClauseId
c (Int32
nInt32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
-Int32
1)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int32
nInt32 -> Int32 -> Bool
forall a. Eq a => a -> a -> Bool
==Int32
1) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
ClauseId
i <- UVec ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e. GenericVec a e -> IO ClauseId
Vec.getSize (Solver -> UVec ClauseId
svUnsatClauses Solver
solver)
UVec ClauseId -> ClauseId -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec ClauseId
svUnsatClauses Solver
solver) ClauseId
c
IOUArray ClauseId ClauseId -> ClauseId -> ClauseId -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> ClauseId -> e -> m ()
unsafeWrite (Solver -> IOUArray ClauseId ClauseId
svClauseUnsatClauseIndex Solver
solver) ClauseId
c ClauseId
i
IORef Weight -> (Weight -> Weight) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef Weight
svObj Solver
solver) (Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
+ Array ClauseId Weight -> ClauseId -> Weight
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> ClauseId -> e
unsafeAt (Solver -> Array ClauseId Weight
svClauseWeights Solver
solver) ClauseId
c)
else do
IOUArray ClauseId Int32 -> ClauseId -> Int32 -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> ClauseId -> e -> m ()
unsafeWrite (Solver -> IOUArray ClauseId Int32
svClauseNumTrueLits Solver
solver) ClauseId
c (Int32
nInt32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
+Int32
1)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int32
nInt32 -> Int32 -> Bool
forall a. Eq a => a -> a -> Bool
==Int32
0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
ClauseId
s <- UVec ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e. GenericVec a e -> IO ClauseId
Vec.getSize (Solver -> UVec ClauseId
svUnsatClauses Solver
solver)
ClauseId
i <- IOUArray ClauseId ClauseId -> ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> ClauseId -> m e
unsafeRead (Solver -> IOUArray ClauseId ClauseId
svClauseUnsatClauseIndex Solver
solver) ClauseId
c
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ClauseId
i ClauseId -> ClauseId -> Bool
forall a. Eq a => a -> a -> Bool
== ClauseId
sClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
-ClauseId
1) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
let i2 :: ClauseId
i2 = ClauseId
sClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
-ClauseId
1
ClauseId
c2 <- UVec ClauseId -> ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> ClauseId -> IO e
Vec.unsafeRead (Solver -> UVec ClauseId
svUnsatClauses Solver
solver) ClauseId
i2
UVec ClauseId -> ClauseId -> ClauseId -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> ClauseId -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec ClauseId
svUnsatClauses Solver
solver) ClauseId
i2 ClauseId
c
UVec ClauseId -> ClauseId -> ClauseId -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> ClauseId -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec ClauseId
svUnsatClauses Solver
solver) ClauseId
i ClauseId
c2
IOUArray ClauseId ClauseId -> ClauseId -> ClauseId -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> ClauseId -> e -> m ()
unsafeWrite (Solver -> IOUArray ClauseId ClauseId
svClauseUnsatClauseIndex Solver
solver) ClauseId
c2 ClauseId
i
ClauseId
_ <- UVec ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.unsafePop (Solver -> UVec ClauseId
svUnsatClauses Solver
solver)
IORef Weight -> (Weight -> Weight) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef Weight
svObj Solver
solver) (Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
subtract (Array ClauseId Weight -> ClauseId -> Weight
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> ClauseId -> e
unsafeAt (Solver -> Array ClauseId Weight
svClauseWeights Solver
solver) ClauseId
c))
() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
setSolution :: SAT.IModel m => Solver -> m -> IO ()
setSolution :: Solver -> m -> IO ()
setSolution Solver
solver m
m = do
(ClauseId, ClauseId)
b <- IOUArray ClauseId Bool -> IO (ClauseId, ClauseId)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> m (i, i)
getBounds (Solver -> IOUArray ClauseId Bool
svSolution Solver
solver)
Clause -> (ClauseId -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((ClauseId, ClauseId) -> Clause
forall a. Ix a => (a, a) -> [a]
range (ClauseId, ClauseId)
b) ((ClauseId -> IO ()) -> IO ()) -> (ClauseId -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \ClauseId
v -> do
Bool
val <- IOUArray ClauseId Bool -> ClauseId -> IO Bool
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray (Solver -> IOUArray ClauseId Bool
svSolution Solver
solver) ClauseId
v
let val' :: Bool
val' = m -> ClauseId -> Bool
forall m. IModel m => m -> ClauseId -> Bool
SAT.evalVar m
m ClauseId
v
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
val Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
val') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
Solver -> ClauseId -> IO ()
flipVar Solver
solver ClauseId
v
getNumVars :: Solver -> IO Int
getNumVars :: Solver -> IO ClauseId
getNumVars Solver
solver = ClauseId -> IO ClauseId
forall (m :: * -> *) a. Monad m => a -> m a
return (ClauseId -> IO ClauseId) -> ClauseId -> IO ClauseId
forall a b. (a -> b) -> a -> b
$ (ClauseId, ClauseId) -> ClauseId
forall a. Ix a => (a, a) -> ClauseId
rangeSize ((ClauseId, ClauseId) -> ClauseId)
-> (ClauseId, ClauseId) -> ClauseId
forall a b. (a -> b) -> a -> b
$ Array ClauseId (UArray ClauseId ClauseId) -> (ClauseId, ClauseId)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds (Solver -> Array ClauseId (UArray ClauseId ClauseId)
svVarOccurs Solver
solver)
getRandomGen :: Solver -> IO Rand.GenIO
getRandomGen :: Solver -> IO GenIO
getRandomGen Solver
solver = IORef (Gen RealWorld) -> IO (Gen RealWorld)
forall a. IORef a -> IO a
readIORef (Solver -> IORef GenIO
svRandomGen Solver
solver)
setRandomGen :: Solver -> Rand.GenIO -> IO ()
setRandomGen :: Solver -> GenIO -> IO ()
setRandomGen Solver
solver GenIO
gen = IORef (Gen RealWorld) -> Gen RealWorld -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef GenIO
svRandomGen Solver
solver) Gen RealWorld
GenIO
gen
getBestSolution :: Solver -> IO (CNF.Weight, SAT.Model)
getBestSolution :: Solver -> IO (Weight, Model)
getBestSolution Solver
solver = IORef (Weight, Model) -> IO (Weight, Model)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Weight, Model)
svBestSolution Solver
solver)
getStatistics :: Solver -> IO Statistics
getStatistics :: Solver -> IO Statistics
getStatistics Solver
solver = IORef Statistics -> IO Statistics
forall a. IORef a -> IO a
readIORef (Solver -> IORef Statistics
svStatistics Solver
solver)
{-# INLINE getMakeValue #-}
getMakeValue :: Solver -> SAT.Var -> IO Double
getMakeValue :: Solver -> ClauseId -> IO Double
getMakeValue Solver
solver ClauseId
v = do
let occurs :: UArray ClauseId ClauseId
occurs = Solver -> Array ClauseId (UArray ClauseId ClauseId)
svVarOccurs Solver
solver Array ClauseId (UArray ClauseId ClauseId)
-> ClauseId -> UArray ClauseId ClauseId
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! ClauseId
v
(ClauseId
lb,ClauseId
ub) = UArray ClauseId ClauseId -> (ClauseId, ClauseId)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds UArray ClauseId ClauseId
occurs
UArray ClauseId ClauseId -> IO Double -> IO Double
seq UArray ClauseId ClauseId
occurs (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$ ClauseId -> IO Double -> IO Double
seq ClauseId
lb (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$ ClauseId -> IO Double -> IO Double
seq ClauseId
ub (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$
ClauseId
-> ClauseId
-> Double
-> (Double -> ClauseId -> IO Double)
-> IO Double
forall a (m :: * -> *) b.
(Num a, Eq a, Monad m) =>
a -> a -> b -> (b -> a -> m b) -> m b
numLoopState ClauseId
lb ClauseId
ub Double
0 ((Double -> ClauseId -> IO Double) -> IO Double)
-> (Double -> ClauseId -> IO Double) -> IO Double
forall a b. (a -> b) -> a -> b
$ \ !Double
r !ClauseId
i -> do
let c :: ClauseId
c = UArray ClauseId ClauseId -> ClauseId -> ClauseId
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> ClauseId -> e
unsafeAt UArray ClauseId ClauseId
occurs ClauseId
i
Int32
n <- IOUArray ClauseId Int32 -> ClauseId -> IO Int32
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> ClauseId -> m e
unsafeRead (Solver -> IOUArray ClauseId Int32
svClauseNumTrueLits Solver
solver) ClauseId
c
Double -> IO Double
forall (m :: * -> *) a. Monad m => a -> m a
return (Double -> IO Double) -> Double -> IO Double
forall a b. (a -> b) -> a -> b
$! if Int32
n Int32 -> Int32 -> Bool
forall a. Eq a => a -> a -> Bool
== Int32
0 then (Double
r Double -> Double -> Double
forall a. Num a => a -> a -> a
+ UArray ClauseId Double -> ClauseId -> Double
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> ClauseId -> e
unsafeAt (Solver -> UArray ClauseId Double
svClauseWeightsF Solver
solver) ClauseId
c) else Double
r
{-# INLINE getBreakValue #-}
getBreakValue :: Solver -> SAT.Var -> IO Double
getBreakValue :: Solver -> ClauseId -> IO Double
getBreakValue Solver
solver ClauseId
v = do
let occurs :: UArray ClauseId ClauseId
occurs = Solver -> Array ClauseId (UArray ClauseId ClauseId)
svVarOccurs Solver
solver Array ClauseId (UArray ClauseId ClauseId)
-> ClauseId -> UArray ClauseId ClauseId
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! ClauseId
v
occursState :: IOUArray ClauseId Bool
occursState = Solver -> Array ClauseId (IOUArray ClauseId Bool)
svVarOccursState Solver
solver Array ClauseId (IOUArray ClauseId Bool)
-> ClauseId -> IOUArray ClauseId Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! ClauseId
v
(ClauseId
lb,ClauseId
ub) = UArray ClauseId ClauseId -> (ClauseId, ClauseId)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds UArray ClauseId ClauseId
occurs
UArray ClauseId ClauseId -> IO Double -> IO Double
seq UArray ClauseId ClauseId
occurs (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$ IOUArray ClauseId Bool -> IO Double -> IO Double
seq IOUArray ClauseId Bool
occursState (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$ ClauseId -> IO Double -> IO Double
seq ClauseId
lb (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$ ClauseId -> IO Double -> IO Double
seq ClauseId
ub (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$
ClauseId
-> ClauseId
-> Double
-> (Double -> ClauseId -> IO Double)
-> IO Double
forall a (m :: * -> *) b.
(Num a, Eq a, Monad m) =>
a -> a -> b -> (b -> a -> m b) -> m b
numLoopState ClauseId
lb ClauseId
ub Double
0 ((Double -> ClauseId -> IO Double) -> IO Double)
-> (Double -> ClauseId -> IO Double) -> IO Double
forall a b. (a -> b) -> a -> b
$ \ !Double
r !ClauseId
i -> do
Bool
b <- IOUArray ClauseId Bool -> ClauseId -> IO Bool
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> ClauseId -> m e
unsafeRead IOUArray ClauseId Bool
occursState ClauseId
i
if Bool
b then do
let c :: ClauseId
c = UArray ClauseId ClauseId -> ClauseId -> ClauseId
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> ClauseId -> e
unsafeAt UArray ClauseId ClauseId
occurs ClauseId
i
Int32
n <- IOUArray ClauseId Int32 -> ClauseId -> IO Int32
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> ClauseId -> m e
unsafeRead (Solver -> IOUArray ClauseId Int32
svClauseNumTrueLits Solver
solver) ClauseId
c
Double -> IO Double
forall (m :: * -> *) a. Monad m => a -> m a
return (Double -> IO Double) -> Double -> IO Double
forall a b. (a -> b) -> a -> b
$! if Int32
nInt32 -> Int32 -> Bool
forall a. Eq a => a -> a -> Bool
==Int32
1 then (Double
r Double -> Double -> Double
forall a. Num a => a -> a -> a
+ UArray ClauseId Double -> ClauseId -> Double
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> ClauseId -> e
unsafeAt (Solver -> UArray ClauseId Double
svClauseWeightsF Solver
solver) ClauseId
c) else Double
r
else
Double -> IO Double
forall (m :: * -> *) a. Monad m => a -> m a
return Double
r
data Options
= Options
{ Options -> Weight
optTarget :: !CNF.Weight
, Options -> ClauseId
optMaxTries :: !Int
, Options -> ClauseId
optMaxFlips :: !Int
, Options -> Bool
optPickClauseWeighted :: Bool
}
deriving (Options -> Options -> Bool
(Options -> Options -> Bool)
-> (Options -> Options -> Bool) -> Eq Options
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Options -> Options -> Bool
$c/= :: Options -> Options -> Bool
== :: Options -> Options -> Bool
$c== :: Options -> Options -> Bool
Eq, ClauseId -> Options -> ShowS
[Options] -> ShowS
Options -> String
(ClauseId -> Options -> ShowS)
-> (Options -> String) -> ([Options] -> ShowS) -> Show Options
forall a.
(ClauseId -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Options] -> ShowS
$cshowList :: [Options] -> ShowS
show :: Options -> String
$cshow :: Options -> String
showsPrec :: ClauseId -> Options -> ShowS
$cshowsPrec :: ClauseId -> Options -> ShowS
Show)
instance Default Options where
def :: Options
def =
Options :: Weight -> ClauseId -> ClauseId -> Bool -> Options
Options
{ optTarget :: Weight
optTarget = Weight
0
, optMaxTries :: ClauseId
optMaxTries = ClauseId
1
, optMaxFlips :: ClauseId
optMaxFlips = ClauseId
100000
, optPickClauseWeighted :: Bool
optPickClauseWeighted = Bool
False
}
data Callbacks
= Callbacks
{ Callbacks -> Solver -> IO Model
cbGenerateInitialSolution :: Solver -> IO SAT.Model
, Callbacks -> Solver -> Weight -> Model -> IO ()
cbOnUpdateBestSolution :: Solver -> CNF.Weight -> SAT.Model -> IO ()
}
instance Default Callbacks where
def :: Callbacks
def =
Callbacks :: (Solver -> IO Model)
-> (Solver -> Weight -> Model -> IO ()) -> Callbacks
Callbacks
{ cbGenerateInitialSolution :: Solver -> IO Model
cbGenerateInitialSolution = Solver -> IO Model
generateUniformRandomSolution
, cbOnUpdateBestSolution :: Solver -> Weight -> Model -> IO ()
cbOnUpdateBestSolution = \Solver
_ Weight
_ Model
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
}
data Statistics
= Statistics
{ Statistics -> TimeSpec
statTotalCPUTime :: !TimeSpec
, Statistics -> ClauseId
statFlips :: !Int
, Statistics -> Double
statFlipsPerSecond :: !Double
}
deriving (Statistics -> Statistics -> Bool
(Statistics -> Statistics -> Bool)
-> (Statistics -> Statistics -> Bool) -> Eq Statistics
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Statistics -> Statistics -> Bool
$c/= :: Statistics -> Statistics -> Bool
== :: Statistics -> Statistics -> Bool
$c== :: Statistics -> Statistics -> Bool
Eq, ClauseId -> Statistics -> ShowS
[Statistics] -> ShowS
Statistics -> String
(ClauseId -> Statistics -> ShowS)
-> (Statistics -> String)
-> ([Statistics] -> ShowS)
-> Show Statistics
forall a.
(ClauseId -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Statistics] -> ShowS
$cshowList :: [Statistics] -> ShowS
show :: Statistics -> String
$cshow :: Statistics -> String
showsPrec :: ClauseId -> Statistics -> ShowS
$cshowsPrec :: ClauseId -> Statistics -> ShowS
Show)
instance Default Statistics where
def :: Statistics
def =
Statistics :: TimeSpec -> ClauseId -> Double -> Statistics
Statistics
{ statTotalCPUTime :: TimeSpec
statTotalCPUTime = TimeSpec
0
, statFlips :: ClauseId
statFlips = ClauseId
0
, statFlipsPerSecond :: Double
statFlipsPerSecond = Double
0
}
generateUniformRandomSolution :: Solver -> IO SAT.Model
generateUniformRandomSolution :: Solver -> IO Model
generateUniformRandomSolution Solver
solver = do
Gen RealWorld
gen <- Solver -> IO GenIO
getRandomGen Solver
solver
ClauseId
n <- Solver -> IO ClauseId
getNumVars Solver
solver
(IOUArray ClauseId Bool
a :: IOUArray Int Bool) <- (ClauseId, ClauseId) -> IO (IOUArray ClauseId Bool)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (ClauseId
1,ClauseId
n)
Clause -> (ClauseId -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ClauseId
1..ClauseId
n] ((ClauseId -> IO ()) -> IO ()) -> (ClauseId -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \ClauseId
v -> do
Bool
b <- GenIO -> IO Bool
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
Gen (PrimState m) -> m a
Rand.uniform Gen RealWorld
GenIO
gen
IOUArray ClauseId Bool -> ClauseId -> Bool -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray ClauseId Bool
a ClauseId
v Bool
b
IOUArray ClauseId Bool -> IO Model
forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
unsafeFreeze IOUArray ClauseId Bool
a
checkCurrentSolution :: Solver -> Callbacks -> IO ()
checkCurrentSolution :: Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb = do
(Weight, Model)
best <- IORef (Weight, Model) -> IO (Weight, Model)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Weight, Model)
svBestSolution Solver
solver)
Weight
obj <- IORef Weight -> IO Weight
forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Weight
obj Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
< (Weight, Model) -> Weight
forall a b. (a, b) -> a
fst (Weight, Model)
best) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
Model
sol <- IOUArray ClauseId Bool -> IO Model
forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
freeze (Solver -> IOUArray ClauseId Bool
svSolution Solver
solver)
IORef (Weight, Model) -> (Weight, Model) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Weight, Model)
svBestSolution Solver
solver) (Weight
obj, Model
sol)
Callbacks -> Solver -> Weight -> Model -> IO ()
cbOnUpdateBestSolution Callbacks
cb Solver
solver Weight
obj Model
sol
pickClause :: Solver -> Options -> IO PackedClause
pickClause :: Solver -> Options -> IO PackedClause
pickClause Solver
solver Options
opt = do
Gen RealWorld
gen <- Solver -> IO GenIO
getRandomGen Solver
solver
if Options -> Bool
optPickClauseWeighted Options
opt then do
Weight
obj <- IORef Weight -> IO Weight
forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
let f :: ClauseId -> Weight -> IO ClauseId
f !ClauseId
j !Weight
x = do
ClauseId
c <- UVec ClauseId -> ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> ClauseId -> IO e
Vec.read (Solver -> UVec ClauseId
svUnsatClauses Solver
solver) ClauseId
j
let w :: Weight
w = Solver -> Array ClauseId Weight
svClauseWeights Solver
solver Array ClauseId Weight -> ClauseId -> Weight
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! ClauseId
c
if Weight
x Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
< Weight
w then
ClauseId -> IO ClauseId
forall (m :: * -> *) a. Monad m => a -> m a
return ClauseId
c
else
ClauseId -> Weight -> IO ClauseId
f (ClauseId
j ClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
+ ClauseId
1) (Weight
x Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
- Weight
w)
Weight
x <- Weight -> GenIO -> IO Weight
forall (m :: * -> *).
PrimMonad m =>
Weight -> Gen (PrimState m) -> m Weight
rand Weight
obj Gen RealWorld
GenIO
gen
ClauseId
c <- ClauseId -> Weight -> IO ClauseId
f ClauseId
0 Weight
x
PackedClause -> IO PackedClause
forall (m :: * -> *) a. Monad m => a -> m a
return (PackedClause -> IO PackedClause)
-> PackedClause -> IO PackedClause
forall a b. (a -> b) -> a -> b
$ (Solver -> Array ClauseId PackedClause
svClauses Solver
solver Array ClauseId PackedClause -> ClauseId -> PackedClause
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! ClauseId
c)
else do
ClauseId
s <- UVec ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e. GenericVec a e -> IO ClauseId
Vec.getSize (Solver -> UVec ClauseId
svUnsatClauses Solver
solver)
ClauseId
j <- (ClauseId, ClauseId) -> GenIO -> IO ClauseId
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (ClauseId
0, ClauseId
s ClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
- ClauseId
1) Gen RealWorld
GenIO
gen
(ClauseId -> PackedClause) -> IO ClauseId -> IO PackedClause
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Solver -> Array ClauseId PackedClause
svClauses Solver
solver Array ClauseId PackedClause -> ClauseId -> PackedClause
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
!) (IO ClauseId -> IO PackedClause) -> IO ClauseId -> IO PackedClause
forall a b. (a -> b) -> a -> b
$ UVec ClauseId -> ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> ClauseId -> IO e
Vec.read (Solver -> UVec ClauseId
svUnsatClauses Solver
solver) ClauseId
j
rand :: PrimMonad m => Integer -> Rand.Gen (PrimState m) -> m Integer
rand :: Weight -> Gen (PrimState m) -> m Weight
rand Weight
n Gen (PrimState m)
gen
| Weight
n Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
<= Word32 -> Weight
forall a. Integral a => a -> Weight
toInteger (Word32
forall a. Bounded a => a
maxBound :: Word32) = (Word32 -> Weight) -> m Word32 -> m Weight
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Word32 -> Weight
forall a. Integral a => a -> Weight
toInteger (m Word32 -> m Weight) -> m Word32 -> m Weight
forall a b. (a -> b) -> a -> b
$ (Word32, Word32) -> Gen (PrimState m) -> m Word32
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Word32
0, Weight -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Weight
n Word32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
- Word32
1 :: Word32) Gen (PrimState m)
gen
| Bool
otherwise = do
Weight
a <- Weight -> Gen (PrimState m) -> m Weight
forall (m :: * -> *).
PrimMonad m =>
Weight -> Gen (PrimState m) -> m Weight
rand (Weight
n Weight -> ClauseId -> Weight
forall a. Bits a => a -> ClauseId -> a
`shiftR` ClauseId
32) Gen (PrimState m)
gen
(Word32
b::Word32) <- Gen (PrimState m) -> m Word32
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
Gen (PrimState m) -> m a
Rand.uniform Gen (PrimState m)
gen
Weight -> m Weight
forall (m :: * -> *) a. Monad m => a -> m a
return (Weight -> m Weight) -> Weight -> m Weight
forall a b. (a -> b) -> a -> b
$ (Weight
a Weight -> ClauseId -> Weight
forall a. Bits a => a -> ClauseId -> a
`shiftL` ClauseId
32) Weight -> Weight -> Weight
forall a. Bits a => a -> a -> a
.|. Word32 -> Weight
forall a. Integral a => a -> Weight
toInteger Word32
b
data Finished = Finished
deriving (ClauseId -> Finished -> ShowS
[Finished] -> ShowS
Finished -> String
(ClauseId -> Finished -> ShowS)
-> (Finished -> String) -> ([Finished] -> ShowS) -> Show Finished
forall a.
(ClauseId -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Finished] -> ShowS
$cshowList :: [Finished] -> ShowS
show :: Finished -> String
$cshow :: Finished -> String
showsPrec :: ClauseId -> Finished -> ShowS
$cshowsPrec :: ClauseId -> Finished -> ShowS
Show, Typeable)
instance Exception Finished
probsat :: Solver -> Options -> Callbacks -> (Double -> Double -> Double) -> IO ()
probsat :: Solver
-> Options -> Callbacks -> (Double -> Double -> Double) -> IO ()
probsat Solver
solver Options
opt Callbacks
cb Double -> Double -> Double
f = do
Gen RealWorld
gen <- Solver -> IO GenIO
getRandomGen Solver
solver
let maxClauseLen :: ClauseId
maxClauseLen =
if (ClauseId, ClauseId) -> ClauseId
forall a. Ix a => (a, a) -> ClauseId
rangeSize (Array ClauseId PackedClause -> (ClauseId, ClauseId)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds (Solver -> Array ClauseId PackedClause
svClauses Solver
solver)) ClauseId -> ClauseId -> Bool
forall a. Eq a => a -> a -> Bool
== ClauseId
0
then ClauseId
0
else Clause -> ClauseId
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Clause -> ClauseId) -> Clause -> ClauseId
forall a b. (a -> b) -> a -> b
$ (PackedClause -> ClauseId) -> [PackedClause] -> Clause
forall a b. (a -> b) -> [a] -> [b]
map ((ClauseId, ClauseId) -> ClauseId
forall a. Ix a => (a, a) -> ClauseId
rangeSize ((ClauseId, ClauseId) -> ClauseId)
-> (PackedClause -> (ClauseId, ClauseId))
-> PackedClause
-> ClauseId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedClause -> (ClauseId, ClauseId)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds) ([PackedClause] -> Clause) -> [PackedClause] -> Clause
forall a b. (a -> b) -> a -> b
$ Array ClauseId PackedClause -> [PackedClause]
forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems (Solver -> Array ClauseId PackedClause
svClauses Solver
solver)
(IOUArray ClauseId Double
wbuf :: IOUArray Int Double) <- (ClauseId, ClauseId) -> IO (IOUArray ClauseId Double)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (ClauseId
0, ClauseId
maxClauseLenClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
-ClauseId
1)
IOURef Double
wsumRef <- Double -> IO (IOURef Double)
forall a. MArray IOUArray a IO => a -> IO (IOURef a)
newIOURef (Double
0 :: Double)
let pickVar :: PackedClause -> IO SAT.Var
pickVar :: PackedClause -> IO ClauseId
pickVar PackedClause
c = do
IOURef Double -> Double -> IO ()
forall a. MArray IOUArray a IO => IOURef a -> a -> IO ()
writeIOURef IOURef Double
wsumRef Double
0
PackedClause -> ((ClauseId, ClauseId) -> IO ()) -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a ClauseId e -> ((ClauseId, e) -> m ()) -> m ()
forAssocsM_ PackedClause
c (((ClauseId, ClauseId) -> IO ()) -> IO ())
-> ((ClauseId, ClauseId) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(ClauseId
k,ClauseId
lit) -> do
let v :: ClauseId
v = ClauseId -> ClauseId
SAT.litVar ClauseId
lit
Double
m <- Solver -> ClauseId -> IO Double
getMakeValue Solver
solver ClauseId
v
Double
b <- Solver -> ClauseId -> IO Double
getBreakValue Solver
solver ClauseId
v
let w :: Double
w = Double -> Double -> Double
f Double
m Double
b
IOUArray ClauseId Double -> ClauseId -> Double -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray ClauseId Double
wbuf ClauseId
k Double
w
IOURef Double -> (Double -> Double) -> IO ()
forall a. MArray IOUArray a IO => IOURef a -> (a -> a) -> IO ()
modifyIOURef IOURef Double
wsumRef (Double -> Double -> Double
forall a. Num a => a -> a -> a
+Double
w)
Double
wsum <- IOURef Double -> IO Double
forall a. MArray IOUArray a IO => IOURef a -> IO a
readIOURef IOURef Double
wsumRef
let go :: Int -> Double -> IO Int
go :: ClauseId -> Double -> IO ClauseId
go !ClauseId
k !Double
a = do
if Bool -> Bool
not ((ClauseId, ClauseId) -> ClauseId -> Bool
forall a. Ix a => (a, a) -> a -> Bool
inRange (PackedClause -> (ClauseId, ClauseId)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c) ClauseId
k) then do
ClauseId -> IO ClauseId
forall (m :: * -> *) a. Monad m => a -> m a
return (ClauseId -> IO ClauseId) -> ClauseId -> IO ClauseId
forall a b. (a -> b) -> a -> b
$! (ClauseId, ClauseId) -> ClauseId
forall a b. (a, b) -> b
snd (PackedClause -> (ClauseId, ClauseId)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c)
else do
Double
w <- IOUArray ClauseId Double -> ClauseId -> IO Double
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray IOUArray ClauseId Double
wbuf ClauseId
k
if Double
a Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
w then
ClauseId -> IO ClauseId
forall (m :: * -> *) a. Monad m => a -> m a
return ClauseId
k
else
ClauseId -> Double -> IO ClauseId
go (ClauseId
k ClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
+ ClauseId
1) (Double
a Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
w)
ClauseId
k <- ClauseId -> Double -> IO ClauseId
go ClauseId
0 (Double -> IO ClauseId) -> IO Double -> IO ClauseId
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Double, Double) -> GenIO -> IO Double
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Double
0, Double
wsum) Gen RealWorld
GenIO
gen
ClauseId -> IO ClauseId
forall (m :: * -> *) a. Monad m => a -> m a
return (ClauseId -> IO ClauseId) -> ClauseId -> IO ClauseId
forall a b. (a -> b) -> a -> b
$! ClauseId -> ClauseId
SAT.litVar (PackedClause
c PackedClause -> ClauseId -> ClauseId
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! ClauseId
k)
TimeSpec
startCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
IOURef ClauseId
flipsRef <- ClauseId -> IO (IOURef ClauseId)
forall a. MArray IOUArray a IO => a -> IO (IOURef a)
newIOURef (ClauseId
0::Int)
let body :: IO ()
body = do
ClauseId -> IO () -> IO ()
forall (m :: * -> *) a. Applicative m => ClauseId -> m a -> m ()
replicateM_ (Options -> ClauseId
optMaxTries Options
opt) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
Model
sol <- Callbacks -> Solver -> IO Model
cbGenerateInitialSolution Callbacks
cb Solver
solver
Solver -> Model -> IO ()
forall m. IModel m => Solver -> m -> IO ()
setSolution Solver
solver Model
sol
Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
ClauseId -> IO () -> IO ()
forall (m :: * -> *) a. Applicative m => ClauseId -> m a -> m ()
replicateM_ (Options -> ClauseId
optMaxFlips Options
opt) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
ClauseId
s <- UVec ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e. GenericVec a e -> IO ClauseId
Vec.getSize (Solver -> UVec ClauseId
svUnsatClauses Solver
solver)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ClauseId
s ClauseId -> ClauseId -> Bool
forall a. Eq a => a -> a -> Bool
== ClauseId
0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Finished -> IO ()
forall a e. Exception e => e -> a
throw Finished
Finished
Weight
obj <- IORef Weight -> IO Weight
forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Weight
obj Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
<= Options -> Weight
optTarget Options
opt) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Finished -> IO ()
forall a e. Exception e => e -> a
throw Finished
Finished
PackedClause
c <- Solver -> Options -> IO PackedClause
pickClause Solver
solver Options
opt
ClauseId
v <- PackedClause -> IO ClauseId
pickVar PackedClause
c
Solver -> ClauseId -> IO ()
flipVar Solver
solver ClauseId
v
IOURef ClauseId -> (ClauseId -> ClauseId) -> IO ()
forall a. MArray IOUArray a IO => IOURef a -> (a -> a) -> IO ()
modifyIOURef IOURef ClauseId
flipsRef ClauseId -> ClauseId
forall a. Integral a => a -> a
inc
Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
IO ()
body IO () -> (Finished -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(Finished
_::Finished) -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
TimeSpec
endCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
ClauseId
flips <- IOURef ClauseId -> IO ClauseId
forall a. MArray IOUArray a IO => IOURef a -> IO a
readIOURef IOURef ClauseId
flipsRef
let totalCPUTime :: TimeSpec
totalCPUTime = TimeSpec
endCPUTime TimeSpec -> TimeSpec -> TimeSpec
`diffTimeSpec` TimeSpec
startCPUTime
totalCPUTimeSec :: Double
totalCPUTimeSec = Weight -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (TimeSpec -> Weight
toNanoSecs TimeSpec
totalCPUTime) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
10Double -> ClauseId -> Double
forall a b. (Num a, Integral b) => a -> b -> a
^(ClauseId
9::Int)
IORef Statistics -> Statistics -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Statistics
svStatistics Solver
solver) (Statistics -> IO ()) -> Statistics -> IO ()
forall a b. (a -> b) -> a -> b
$
Statistics :: TimeSpec -> ClauseId -> Double -> Statistics
Statistics
{ statTotalCPUTime :: TimeSpec
statTotalCPUTime = TimeSpec
totalCPUTime
, statFlips :: ClauseId
statFlips = ClauseId
flips
, statFlipsPerSecond :: Double
statFlipsPerSecond = ClauseId -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral ClauseId
flips Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
totalCPUTimeSec
}
() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
walksat :: Solver -> Options -> Callbacks -> Double -> IO ()
walksat :: Solver -> Options -> Callbacks -> Double -> IO ()
walksat Solver
solver Options
opt Callbacks
cb Double
p = do
Gen RealWorld
gen <- Solver -> IO GenIO
getRandomGen Solver
solver
(UVec ClauseId
buf :: Vec.UVec SAT.Var) <- IO (UVec ClauseId)
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
let pickVar :: PackedClause -> IO SAT.Var
pickVar :: PackedClause -> IO ClauseId
pickVar PackedClause
c = do
UVec ClauseId -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO ()
Vec.clear UVec ClauseId
buf
let (ClauseId
lb,ClauseId
ub) = PackedClause -> (ClauseId, ClauseId)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c
Either ClauseId ()
r <- ExceptT ClauseId IO () -> IO (Either ClauseId ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT ClauseId IO () -> IO (Either ClauseId ()))
-> ExceptT ClauseId IO () -> IO (Either ClauseId ())
forall a b. (a -> b) -> a -> b
$ do
Double
_ <- ClauseId
-> ClauseId
-> Double
-> (Double -> ClauseId -> ExceptT ClauseId IO Double)
-> ExceptT ClauseId IO Double
forall a (m :: * -> *) b.
(Num a, Eq a, Monad m) =>
a -> a -> b -> (b -> a -> m b) -> m b
numLoopState ClauseId
lb ClauseId
ub (Double
1.0Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/Double
0.0) ((Double -> ClauseId -> ExceptT ClauseId IO Double)
-> ExceptT ClauseId IO Double)
-> (Double -> ClauseId -> ExceptT ClauseId IO Double)
-> ExceptT ClauseId IO Double
forall a b. (a -> b) -> a -> b
$ \ !Double
b0 !ClauseId
i -> do
let v :: ClauseId
v = ClauseId -> ClauseId
SAT.litVar (PackedClause
c PackedClause -> ClauseId -> ClauseId
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! ClauseId
i)
Double
b <- IO Double -> ExceptT ClauseId IO Double
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Double -> ExceptT ClauseId IO Double)
-> IO Double -> ExceptT ClauseId IO Double
forall a b. (a -> b) -> a -> b
$ Solver -> ClauseId -> IO Double
getBreakValue Solver
solver ClauseId
v
if Double
b Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
0 then
ClauseId -> ExceptT ClauseId IO Double
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ClauseId
v
else if Double
b Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
b0 then do
IO () -> ExceptT ClauseId IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ExceptT ClauseId IO ())
-> IO () -> ExceptT ClauseId IO ()
forall a b. (a -> b) -> a -> b
$ UVec ClauseId -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO ()
Vec.clear UVec ClauseId
buf IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> UVec ClauseId -> ClauseId -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec ClauseId
buf ClauseId
v
Double -> ExceptT ClauseId IO Double
forall (m :: * -> *) a. Monad m => a -> m a
return Double
b
else if Double
b Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
b0 then do
IO () -> ExceptT ClauseId IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ExceptT ClauseId IO ())
-> IO () -> ExceptT ClauseId IO ()
forall a b. (a -> b) -> a -> b
$ UVec ClauseId -> ClauseId -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec ClauseId
buf ClauseId
v
Double -> ExceptT ClauseId IO Double
forall (m :: * -> *) a. Monad m => a -> m a
return Double
b0
else do
Double -> ExceptT ClauseId IO Double
forall (m :: * -> *) a. Monad m => a -> m a
return Double
b0
() -> ExceptT ClauseId IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
case Either ClauseId ()
r of
Left ClauseId
v -> ClauseId -> IO ClauseId
forall (m :: * -> *) a. Monad m => a -> m a
return ClauseId
v
Right ()
_ -> do
Bool
flag <- Double -> GenIO -> IO Bool
forall (m :: * -> *).
PrimMonad m =>
Double -> Gen (PrimState m) -> m Bool
Rand.bernoulli Double
p Gen RealWorld
GenIO
gen
if Bool
flag then do
ClauseId
i <- (ClauseId, ClauseId) -> GenIO -> IO ClauseId
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (ClauseId
lb,ClauseId
ub) Gen RealWorld
GenIO
gen
ClauseId -> IO ClauseId
forall (m :: * -> *) a. Monad m => a -> m a
return (ClauseId -> IO ClauseId) -> ClauseId -> IO ClauseId
forall a b. (a -> b) -> a -> b
$! ClauseId -> ClauseId
SAT.litVar (PackedClause
c PackedClause -> ClauseId -> ClauseId
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! ClauseId
i)
else do
ClauseId
s <- UVec ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e. GenericVec a e -> IO ClauseId
Vec.getSize UVec ClauseId
buf
if ClauseId
s ClauseId -> ClauseId -> Bool
forall a. Eq a => a -> a -> Bool
== ClauseId
1 then
UVec ClauseId -> ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> ClauseId -> IO e
Vec.unsafeRead UVec ClauseId
buf ClauseId
0
else do
ClauseId
i <- (ClauseId, ClauseId) -> GenIO -> IO ClauseId
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (ClauseId
0, ClauseId
s ClauseId -> ClauseId -> ClauseId
forall a. Num a => a -> a -> a
- ClauseId
1) Gen RealWorld
GenIO
gen
UVec ClauseId -> ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> ClauseId -> IO e
Vec.unsafeRead UVec ClauseId
buf ClauseId
i
TimeSpec
startCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
IOURef ClauseId
flipsRef <- ClauseId -> IO (IOURef ClauseId)
forall a. MArray IOUArray a IO => a -> IO (IOURef a)
newIOURef (ClauseId
0::Int)
let body :: IO ()
body = do
ClauseId -> IO () -> IO ()
forall (m :: * -> *) a. Applicative m => ClauseId -> m a -> m ()
replicateM_ (Options -> ClauseId
optMaxTries Options
opt) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
Model
sol <- Callbacks -> Solver -> IO Model
cbGenerateInitialSolution Callbacks
cb Solver
solver
Solver -> Model -> IO ()
forall m. IModel m => Solver -> m -> IO ()
setSolution Solver
solver Model
sol
Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
ClauseId -> IO () -> IO ()
forall (m :: * -> *) a. Applicative m => ClauseId -> m a -> m ()
replicateM_ (Options -> ClauseId
optMaxFlips Options
opt) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
ClauseId
s <- UVec ClauseId -> IO ClauseId
forall (a :: * -> * -> *) e. GenericVec a e -> IO ClauseId
Vec.getSize (Solver -> UVec ClauseId
svUnsatClauses Solver
solver)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ClauseId
s ClauseId -> ClauseId -> Bool
forall a. Eq a => a -> a -> Bool
== ClauseId
0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Finished -> IO ()
forall a e. Exception e => e -> a
throw Finished
Finished
Weight
obj <- IORef Weight -> IO Weight
forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Weight
obj Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
<= Options -> Weight
optTarget Options
opt) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Finished -> IO ()
forall a e. Exception e => e -> a
throw Finished
Finished
PackedClause
c <- Solver -> Options -> IO PackedClause
pickClause Solver
solver Options
opt
ClauseId
v <- PackedClause -> IO ClauseId
pickVar PackedClause
c
Solver -> ClauseId -> IO ()
flipVar Solver
solver ClauseId
v
IOURef ClauseId -> (ClauseId -> ClauseId) -> IO ()
forall a. MArray IOUArray a IO => IOURef a -> (a -> a) -> IO ()
modifyIOURef IOURef ClauseId
flipsRef ClauseId -> ClauseId
forall a. Integral a => a -> a
inc
Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
IO ()
body IO () -> (Finished -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(Finished
_::Finished) -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
TimeSpec
endCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
ClauseId
flips <- IOURef ClauseId -> IO ClauseId
forall a. MArray IOUArray a IO => IOURef a -> IO a
readIOURef IOURef ClauseId
flipsRef
let totalCPUTime :: TimeSpec
totalCPUTime = TimeSpec
endCPUTime TimeSpec -> TimeSpec -> TimeSpec
`diffTimeSpec` TimeSpec
startCPUTime
totalCPUTimeSec :: Double
totalCPUTimeSec = Weight -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (TimeSpec -> Weight
toNanoSecs TimeSpec
totalCPUTime) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
10Double -> ClauseId -> Double
forall a b. (Num a, Integral b) => a -> b -> a
^(ClauseId
9::Int)
IORef Statistics -> Statistics -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Statistics
svStatistics Solver
solver) (Statistics -> IO ()) -> Statistics -> IO ()
forall a b. (a -> b) -> a -> b
$
Statistics :: TimeSpec -> ClauseId -> Double -> Statistics
Statistics
{ statTotalCPUTime :: TimeSpec
statTotalCPUTime = TimeSpec
totalCPUTime
, statFlips :: ClauseId
statFlips = ClauseId
flips
, statFlipsPerSecond :: Double
statFlipsPerSecond = ClauseId -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral ClauseId
flips Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
totalCPUTimeSec
}
() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
{-# INLINE modifyArray #-}
modifyArray :: (MArray a e m, Ix i) => a i e -> i -> (e -> e) -> m ()
modifyArray :: a i e -> i -> (e -> e) -> m ()
modifyArray a i e
a i
i e -> e
f = do
e
e <- a i e -> i -> m e
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray a i e
a i
i
a i e -> i -> e -> m ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray a i e
a i
i (e -> e
f e
e)
{-# INLINE forAssocsM_ #-}
forAssocsM_ :: (IArray a e, Monad m) => a Int e -> ((Int,e) -> m ()) -> m ()
forAssocsM_ :: a ClauseId e -> ((ClauseId, e) -> m ()) -> m ()
forAssocsM_ a ClauseId e
a (ClauseId, e) -> m ()
f = do
let (ClauseId
lb,ClauseId
ub) = a ClauseId e -> (ClauseId, ClauseId)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds a ClauseId e
a
ClauseId -> ClauseId -> (ClauseId -> m ()) -> m ()
forall a (m :: * -> *).
(Num a, Ord a, Monad m) =>
a -> a -> (a -> m ()) -> m ()
numLoop ClauseId
lb ClauseId
ub ((ClauseId -> m ()) -> m ()) -> (ClauseId -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ClauseId
i ->
(ClauseId, e) -> m ()
f (ClauseId
i, a ClauseId e -> ClauseId -> e
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> ClauseId -> e
unsafeAt a ClauseId e
a ClauseId
i)
{-# INLINE inc #-}
inc :: Integral a => a -> a
inc :: a -> a
inc a
a = a
aa -> a -> a
forall a. Num a => a -> a -> a
+a
1