{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
----------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Solver.SLS.ProbSAT
-- Copyright   :  (c) Masahiro Sakai 2017
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
----------------------------------------------------------------------
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))
  , Solver -> Array ClauseId (IOUArray ClauseId Bool)
svVarOccursState    :: !(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 -- For integral types inclusive range is used
    (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)

  -- It's faster to use Control.Exception than using Control.Monad.Except
  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 -- freebie move
            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
              -- random walk move
              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
              -- greedy move
              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)

  -- It's faster to use Control.Exception than using Control.Monad.Except
  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

-- -------------------------------------------------------------------