{-# LANGUAGE BangPatterns #-}
{-# 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 Var PackedClause
svClauses                :: !(Array ClauseId PackedClause)
  , Solver -> Array Var Weight
svClauseWeights          :: !(Array ClauseId CNF.Weight)
  , Solver -> UArray Var Double
svClauseWeightsF         :: !(UArray ClauseId Double)
  , Solver -> IOUArray Var Int32
svClauseNumTrueLits      :: !(IOUArray ClauseId Int32)
  , Solver -> IOUArray Var Var
svClauseUnsatClauseIndex :: !(IOUArray ClauseId Int)
  , Solver -> UVec Var
svUnsatClauses           :: !(Vec.UVec ClauseId)

  , Solver -> Array Var (UArray Var Var)
svVarOccurs         :: !(Array SAT.Var (UArray Int ClauseId))
  , Solver -> Array Var (IOUArray Var Bool)
svVarOccursState    :: !(Array SAT.Var (IOUArray Int Bool))
  , Solver -> IOUArray Var 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 =
        CNF.WCNF
        { wcnfNumVars :: Var
CNF.wcnfNumVars    = CNF -> Var
CNF.cnfNumVars CNF
cnf
        , wcnfNumClauses :: Var
CNF.wcnfNumClauses = CNF -> Var
CNF.cnfNumClauses CNF
cnf
        , wcnfTopCost :: Weight
CNF.wcnfTopCost    = forall a b. (Integral a, Num b) => a -> b
fromIntegral (CNF -> Var
CNF.cnfNumClauses CNF
cnf) 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 :: Var -> Bool
m Var
_ = Bool
False
      nv :: Var
nv = WCNF -> Var
CNF.wcnfNumVars WCNF
wcnf

  IORef Weight
objRef <- forall a. a -> IO (IORef a)
newIORef (Weight
0::Integer)

  [(Weight, PackedClause)]
cs <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (WCNF -> [WeightedClause]
CNF.wcnfClauses WCNF
wcnf) 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      Just [] -> forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Weight
objRef (Weight
wforall a. Num a => a -> a -> a
+) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      Just Clause
c  -> do
        let c' :: PackedClause
c' = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, forall (t :: * -> *) a. Foldable t => t a -> Var
length Clause
c forall a. Num a => a -> a -> a
- Var
1) Clause
c
        seq :: forall a b. a -> b -> b
seq PackedClause
c' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (Weight
w,PackedClause
c'))
  let len :: Var
len = forall (t :: * -> *) a. Foldable t => t a -> Var
length [(Weight, PackedClause)]
cs
      clauses :: Array Var PackedClause
clauses  = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, Var
len forall a. Num a => a -> a -> a
- Var
1) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Weight, PackedClause)]
cs)
      weights  :: Array ClauseId CNF.Weight
      weights :: Array Var Weight
weights  = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, Var
len forall a. Num a => a -> a -> a
- Var
1) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Weight, PackedClause)]
cs)
      weightsF :: UArray ClauseId Double
      weightsF :: UArray Var Double
weightsF = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, Var
len forall a. Num a => a -> a -> a
- Var
1) (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Weight, PackedClause)]
cs)

  (IOArray Var (Seq (Var, Bool))
varOccurs' :: IOArray SAT.Var (Seq.Seq (Int, Bool))) <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (Var
1, Var
nv) forall a. Seq a
Seq.empty

  IOUArray Var Int32
clauseNumTrueLits <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Array Var PackedClause
clauses) Int32
0
  IOUArray Var Var
clauseUnsatClauseIndex <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Array Var PackedClause
clauses) (-Var
1)
  UVec Var
unsatClauses <- forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new

  forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a Var e -> ((Var, e) -> m ()) -> m ()
forAssocsM_ Array Var PackedClause
clauses forall a b. (a -> b) -> a -> b
$ \(Var
c,PackedClause
clause) -> do
    let n :: Int32
n = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int32
1 | Var
lit <- forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems PackedClause
clause, forall m. IModel m => m -> Var -> Bool
SAT.evalLit Var -> Bool
m Var
lit]
    forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray Var Int32
clauseNumTrueLits Var
c Int32
n
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int32
n forall a. Eq a => a -> a -> Bool
== Int32
0) forall a b. (a -> b) -> a -> b
$ do
      Var
i <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize UVec Var
unsatClauses
      forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray Var Var
clauseUnsatClauseIndex Var
c Var
i
      forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec Var
unsatClauses Var
c
      forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef Weight
objRef ((Array Var Weight
weights forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
c) forall a. Num a => a -> a -> a
+)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems PackedClause
clause) forall a b. (a -> b) -> a -> b
$ \Var
lit -> do
      let v :: Var
v = Var -> Var
SAT.litVar Var
lit
      let b :: Bool
b = forall m. IModel m => m -> Var -> Bool
SAT.evalLit Var -> Bool
m Var
lit
      seq :: forall a b. a -> b -> b
seq Bool
b forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> (e -> e) -> m ()
modifyArray IOArray Var (Seq (Var, Bool))
varOccurs' Var
v (forall a. Seq a -> a -> Seq a
|> (Var
c,Bool
b))

  Array Var (UArray Var Var)
varOccurs <- do
    (IOArray Var (UArray Var Var)
arr::IOArray SAT.Var (UArray Int ClauseId)) <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
1, Var
nv)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var
1 .. Var
nv] forall a b. (a -> b) -> a -> b
$ \Var
v -> do
      Seq (Var, Bool)
s <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray IOArray Var (Seq (Var, Bool))
varOccurs' Var
v
      forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOArray Var (UArray Var Var)
arr Var
v forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, forall a. Seq a -> Var
Seq.length Seq (Var, Bool)
s forall a. Num a => a -> a -> a
- Var
1) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Var, Bool)
s))
    forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
unsafeFreeze IOArray Var (UArray Var Var)
arr

  Array Var (IOUArray Var Bool)
varOccursState <- do
    (IOArray Var (IOUArray Var Bool)
arr::IOArray SAT.Var (IOUArray Int Bool)) <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
1, Var
nv)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var
1 .. Var
nv] forall a b. (a -> b) -> a -> b
$ \Var
v -> do
      Seq (Var, Bool)
s <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray IOArray Var (Seq (Var, Bool))
varOccurs' Var
v
      IOUArray Var Bool
ss <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
0, forall a. Seq a -> Var
Seq.length Seq (Var, Bool)
s forall a. Num a => a -> a -> a
- Var
1)
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [Var
0..] (forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Var, Bool)
s)) forall a b. (a -> b) -> a -> b
$ \(Var
j,(Var, Bool)
a) -> forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray Var Bool
ss Var
j (forall a b. (a, b) -> b
snd (Var, Bool)
a)
      forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOArray Var (IOUArray Var Bool)
arr Var
v IOUArray Var Bool
ss
    forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
unsafeFreeze IOArray Var (IOUArray Var Bool)
arr

  IOUArray Var Bool
solution <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> [e] -> m (a i e)
newListArray (Var
1, Var
nv) forall a b. (a -> b) -> a -> b
$ [forall m. IModel m => m -> Var -> Bool
SAT.evalVar Var -> Bool
m Var
v | Var
v <- [Var
1..Var
nv]]

  Weight
bestObj <- forall a. IORef a -> IO a
readIORef IORef Weight
objRef
  Model
bestSol <- forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
freeze IOUArray Var Bool
solution
  IORef (Weight, Model)
bestSolution <- forall a. a -> IO (IORef a)
newIORef (Weight
bestObj, Model
bestSol)

  IORef (Gen RealWorld)
randGen <- forall a. a -> IO (IORef a)
newIORef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). PrimMonad m => m (Gen (PrimState m))
Rand.create

  IORef Statistics
stat <- forall a. a -> IO (IORef a)
newIORef forall a. Default a => a
def

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    Solver
    { svClauses :: Array Var PackedClause
svClauses = Array Var PackedClause
clauses
    , svClauseWeights :: Array Var Weight
svClauseWeights          = Array Var Weight
weights
    , svClauseWeightsF :: UArray Var Double
svClauseWeightsF         = UArray Var Double
weightsF
    , svClauseNumTrueLits :: IOUArray Var Int32
svClauseNumTrueLits      = IOUArray Var Int32
clauseNumTrueLits
    , svClauseUnsatClauseIndex :: IOUArray Var Var
svClauseUnsatClauseIndex = IOUArray Var Var
clauseUnsatClauseIndex
    , svUnsatClauses :: UVec Var
svUnsatClauses           = UVec Var
unsatClauses

    , svVarOccurs :: Array Var (UArray Var Var)
svVarOccurs         = Array Var (UArray Var Var)
varOccurs
    , svVarOccursState :: Array Var (IOUArray Var Bool)
svVarOccursState    = Array Var (IOUArray Var Bool)
varOccursState
    , svSolution :: IOUArray Var Bool
svSolution          = IOUArray Var Bool
solution

    , svObj :: IORef Weight
svObj = IORef Weight
objRef

    , svRandomGen :: IORef GenIO
svRandomGen         = IORef (Gen RealWorld)
randGen
    , svBestSolution :: IORef (Weight, Model)
svBestSolution      = IORef (Weight, Model)
bestSolution
    , svStatistics :: IORef Statistics
svStatistics        = IORef Statistics
stat
    }


flipVar :: Solver -> SAT.Var -> IO ()
flipVar :: Solver -> Var -> IO ()
flipVar Solver
solver Var
v = forall a. IO a -> IO a
mask_ forall a b. (a -> b) -> a -> b
$ do
  let occurs :: UArray Var Var
occurs = Solver -> Array Var (UArray Var Var)
svVarOccurs Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
      occursState :: IOUArray Var Bool
occursState = Solver -> Array Var (IOUArray Var Bool)
svVarOccursState Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
  seq :: forall a b. a -> b -> b
seq UArray Var Var
occurs forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq IOUArray Var Bool
occursState forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
  forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> (e -> e) -> m ()
modifyArray (Solver -> IOUArray Var Bool
svSolution Solver
solver) Var
v Bool -> Bool
not
  forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a Var e -> ((Var, e) -> m ()) -> m ()
forAssocsM_ UArray Var Var
occurs forall a b. (a -> b) -> a -> b
$ \(Var
j,!Var
c) -> do
    Bool
b <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead IOUArray Var Bool
occursState Var
j
    Int32
n <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead (Solver -> IOUArray Var Int32
svClauseNumTrueLits Solver
solver) Var
c
    forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> e -> m ()
unsafeWrite IOUArray Var Bool
occursState Var
j (Bool -> Bool
not Bool
b)
    if Bool
b then do
      forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> e -> m ()
unsafeWrite (Solver -> IOUArray Var Int32
svClauseNumTrueLits Solver
solver) Var
c (Int32
nforall a. Num a => a -> a -> a
-Int32
1)
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int32
nforall a. Eq a => a -> a -> Bool
==Int32
1) forall a b. (a -> b) -> a -> b
$ do
        Var
i <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
        forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
c
        forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> e -> m ()
unsafeWrite (Solver -> IOUArray Var Var
svClauseUnsatClauseIndex Solver
solver) Var
c Var
i
        forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef Weight
svObj Solver
solver) (forall a. Num a => a -> a -> a
+ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt (Solver -> Array Var Weight
svClauseWeights Solver
solver) Var
c)
    else do
      forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> e -> m ()
unsafeWrite (Solver -> IOUArray Var Int32
svClauseNumTrueLits Solver
solver) Var
c (Int32
nforall a. Num a => a -> a -> a
+Int32
1)
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int32
nforall a. Eq a => a -> a -> Bool
==Int32
0) forall a b. (a -> b) -> a -> b
$ do
        Var
s <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
        Var
i <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead (Solver -> IOUArray Var Var
svClauseUnsatClauseIndex Solver
solver) Var
c
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Var
i forall a. Eq a => a -> a -> Bool
== Var
sforall a. Num a => a -> a -> a
-Var
1) forall a b. (a -> b) -> a -> b
$ do
          let i2 :: Var
i2 = Var
sforall a. Num a => a -> a -> a
-Var
1
          Var
c2 <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.unsafeRead (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
i2
          forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
i2 Var
c
          forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
i Var
c2
          forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> e -> m ()
unsafeWrite (Solver -> IOUArray Var Var
svClauseUnsatClauseIndex Solver
solver) Var
c2 Var
i
        Var
_ <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.unsafePop (Solver -> UVec Var
svUnsatClauses Solver
solver)
        forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef Weight
svObj Solver
solver) (forall a. Num a => a -> a -> a
subtract (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt (Solver -> Array Var Weight
svClauseWeights Solver
solver) Var
c))
        forall (m :: * -> *) a. Monad m => a -> m a
return ()

setSolution :: SAT.IModel m => Solver -> m -> IO ()
setSolution :: forall m. IModel m => Solver -> m -> IO ()
setSolution Solver
solver m
m = do
  (Var, Var)
b <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> m (i, i)
getBounds (Solver -> IOUArray Var Bool
svSolution Solver
solver)
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Ix a => (a, a) -> [a]
range (Var, Var)
b) forall a b. (a -> b) -> a -> b
$ \Var
v -> do
    Bool
val <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray (Solver -> IOUArray Var Bool
svSolution Solver
solver) Var
v
    let val' :: Bool
val' = forall m. IModel m => m -> Var -> Bool
SAT.evalVar m
m Var
v
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
val forall a. Eq a => a -> a -> Bool
== Bool
val') forall a b. (a -> b) -> a -> b
$ do
      Solver -> Var -> IO ()
flipVar Solver
solver Var
v

getNumVars :: Solver -> IO Int
getNumVars :: Solver -> IO Var
getNumVars Solver
solver = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Ix a => (a, a) -> Var
rangeSize forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds (Solver -> Array Var (UArray Var Var)
svVarOccurs Solver
solver)

getRandomGen :: Solver -> IO Rand.GenIO
getRandomGen :: Solver -> IO GenIO
getRandomGen Solver
solver = 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 = forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef GenIO
svRandomGen Solver
solver) GenIO
gen

getBestSolution :: Solver -> IO (CNF.Weight, SAT.Model)
getBestSolution :: Solver -> IO (Weight, Model)
getBestSolution Solver
solver = 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 = forall a. IORef a -> IO a
readIORef (Solver -> IORef Statistics
svStatistics Solver
solver)

{-# INLINE getMakeValue #-}
getMakeValue :: Solver -> SAT.Var -> IO Double
getMakeValue :: Solver -> Var -> IO Double
getMakeValue Solver
solver Var
v = do
  let occurs :: UArray Var Var
occurs = Solver -> Array Var (UArray Var Var)
svVarOccurs Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
      (Var
lb,Var
ub) = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds UArray Var Var
occurs
  seq :: forall a b. a -> b -> b
seq UArray Var Var
occurs forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq Var
lb forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq Var
ub forall a b. (a -> b) -> a -> b
$
    forall a (m :: * -> *) b.
(Num a, Eq a, Monad m) =>
a -> a -> b -> (b -> a -> m b) -> m b
numLoopState Var
lb Var
ub Double
0 forall a b. (a -> b) -> a -> b
$ \ !Double
r !Var
i -> do
      let c :: Var
c = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt UArray Var Var
occurs Var
i
      Int32
n <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead (Solver -> IOUArray Var Int32
svClauseNumTrueLits Solver
solver) Var
c
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! if Int32
n forall a. Eq a => a -> a -> Bool
== Int32
0 then (Double
r forall a. Num a => a -> a -> a
+ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt (Solver -> UArray Var Double
svClauseWeightsF Solver
solver) Var
c) else Double
r

{-# INLINE getBreakValue #-}
getBreakValue :: Solver -> SAT.Var -> IO Double
getBreakValue :: Solver -> Var -> IO Double
getBreakValue Solver
solver Var
v = do
  let occurs :: UArray Var Var
occurs = Solver -> Array Var (UArray Var Var)
svVarOccurs Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
      occursState :: IOUArray Var Bool
occursState = Solver -> Array Var (IOUArray Var Bool)
svVarOccursState Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
      (Var
lb,Var
ub) = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds UArray Var Var
occurs
  seq :: forall a b. a -> b -> b
seq UArray Var Var
occurs forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq IOUArray Var Bool
occursState forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq Var
lb forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq Var
ub forall a b. (a -> b) -> a -> b
$
    forall a (m :: * -> *) b.
(Num a, Eq a, Monad m) =>
a -> a -> b -> (b -> a -> m b) -> m b
numLoopState Var
lb Var
ub Double
0 forall a b. (a -> b) -> a -> b
$ \ !Double
r !Var
i -> do
      Bool
b <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead IOUArray Var Bool
occursState Var
i
      if Bool
b then do
        let c :: Var
c = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt UArray Var Var
occurs Var
i
        Int32
n <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead (Solver -> IOUArray Var Int32
svClauseNumTrueLits Solver
solver) Var
c
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! if Int32
nforall a. Eq a => a -> a -> Bool
==Int32
1 then (Double
r forall a. Num a => a -> a -> a
+ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt (Solver -> UArray Var Double
svClauseWeightsF Solver
solver) Var
c) else Double
r
      else
        forall (m :: * -> *) a. Monad m => a -> m a
return Double
r

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

data Options
  = Options
  { Options -> Weight
optTarget   :: !CNF.Weight
  , Options -> Var
optMaxTries :: !Int
  , Options -> Var
optMaxFlips :: !Int
  , Options -> Bool
optPickClauseWeighted :: Bool
  }
  deriving (Options -> Options -> Bool
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, Var -> Options -> ShowS
[Options] -> ShowS
Options -> String
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Options] -> ShowS
$cshowList :: [Options] -> ShowS
show :: Options -> String
$cshow :: Options -> String
showsPrec :: Var -> Options -> ShowS
$cshowsPrec :: Var -> Options -> ShowS
Show)

instance Default Options where
  def :: Options
def =
    Options
    { optTarget :: Weight
optTarget   = Weight
0
    , optMaxTries :: Var
optMaxTries = Var
1
    , optMaxFlips :: Var
optMaxFlips = Var
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
    { cbGenerateInitialSolution :: Solver -> IO Model
cbGenerateInitialSolution = Solver -> IO Model
generateUniformRandomSolution
    , cbOnUpdateBestSolution :: Solver -> Weight -> Model -> IO ()
cbOnUpdateBestSolution = \Solver
_ Weight
_ Model
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    }

data Statistics
  = Statistics
  { Statistics -> TimeSpec
statTotalCPUTime   :: !TimeSpec
  , Statistics -> Var
statFlips          :: !Int
  , Statistics -> Double
statFlipsPerSecond :: !Double
  }
  deriving (Statistics -> Statistics -> Bool
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, Var -> Statistics -> ShowS
[Statistics] -> ShowS
Statistics -> String
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Statistics] -> ShowS
$cshowList :: [Statistics] -> ShowS
show :: Statistics -> String
$cshow :: Statistics -> String
showsPrec :: Var -> Statistics -> ShowS
$cshowsPrec :: Var -> Statistics -> ShowS
Show)

instance Default Statistics where
  def :: Statistics
def =
    Statistics
    { statTotalCPUTime :: TimeSpec
statTotalCPUTime = TimeSpec
0
    , statFlips :: Var
statFlips = Var
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
  Var
n <- Solver -> IO Var
getNumVars Solver
solver
  (IOUArray Var Bool
a :: IOUArray Int Bool) <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
1,Var
n)
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var
1..Var
n] forall a b. (a -> b) -> a -> b
$ \Var
v -> do
    Bool
b <- forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
Gen (PrimState m) -> m a
Rand.uniform Gen RealWorld
gen
    forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray Var Bool
a Var
v Bool
b
  forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
unsafeFreeze IOUArray Var Bool
a

checkCurrentSolution :: Solver -> Callbacks -> IO ()
checkCurrentSolution :: Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb = do
  (Weight, Model)
best <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Weight, Model)
svBestSolution Solver
solver)
  Weight
obj <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Weight
obj forall a. Ord a => a -> a -> Bool
< forall a b. (a, b) -> a
fst (Weight, Model)
best) forall a b. (a -> b) -> a -> b
$ do
    Model
sol <- 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 Var Bool
svSolution Solver
solver)
    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 <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
    let f :: Var -> Weight -> IO Var
f !Var
j !Weight
x = do
          Var
c <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.read (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
j
          let w :: Weight
w = Solver -> Array Var Weight
svClauseWeights Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
c
          if Weight
x forall a. Ord a => a -> a -> Bool
< Weight
w then
            forall (m :: * -> *) a. Monad m => a -> m a
return Var
c
          else
            Var -> Weight -> IO Var
f (Var
j forall a. Num a => a -> a -> a
+ Var
1) (Weight
x forall a. Num a => a -> a -> a
- Weight
w)
    Weight
x <- forall (m :: * -> *).
PrimMonad m =>
Weight -> Gen (PrimState m) -> m Weight
rand Weight
obj Gen RealWorld
gen
    Var
c <- Var -> Weight -> IO Var
f Var
0 Weight
x
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Solver -> Array Var PackedClause
svClauses Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
c)
  else do
    Var
s <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
    Var
j <- forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Var
0, Var
s forall a. Num a => a -> a -> a
- Var
1) Gen RealWorld
gen -- For integral types inclusive range is used
    forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Solver -> Array Var PackedClause
svClauses Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
!) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.read (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
j

rand :: PrimMonad m => Integer -> Rand.Gen (PrimState m) -> m Integer
rand :: forall (m :: * -> *).
PrimMonad m =>
Weight -> Gen (PrimState m) -> m Weight
rand Weight
n Gen (PrimState m)
gen
  | Weight
n forall a. Ord a => a -> a -> Bool
<= forall a. Integral a => a -> Weight
toInteger (forall a. Bounded a => a
maxBound :: Word32) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Integral a => a -> Weight
toInteger forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Word32
0, forall a b. (Integral a, Num b) => a -> b
fromIntegral Weight
n forall a. Num a => a -> a -> a
- Word32
1 :: Word32) Gen (PrimState m)
gen
  | Bool
otherwise = do
      Weight
a <- forall (m :: * -> *).
PrimMonad m =>
Weight -> Gen (PrimState m) -> m Weight
rand (Weight
n forall a. Bits a => a -> Var -> a
`shiftR` Var
32) Gen (PrimState m)
gen
      (Word32
b::Word32) <- forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
Gen (PrimState m) -> m a
Rand.uniform Gen (PrimState m)
gen
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Weight
a forall a. Bits a => a -> Var -> a
`shiftL` Var
32) forall a. Bits a => a -> a -> a
.|. forall a. Integral a => a -> Weight
toInteger Word32
b

data Finished = Finished
  deriving (Var -> Finished -> ShowS
[Finished] -> ShowS
Finished -> String
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Finished] -> ShowS
$cshowList :: [Finished] -> ShowS
show :: Finished -> String
$cshow :: Finished -> String
showsPrec :: Var -> Finished -> ShowS
$cshowsPrec :: Var -> 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 :: Var
maxClauseLen =
        if forall a. Ix a => (a, a) -> Var
rangeSize (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds (Solver -> Array Var PackedClause
svClauses Solver
solver)) forall a. Eq a => a -> a -> Bool
== Var
0
        then Var
0
        else forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Ix a => (a, a) -> Var
rangeSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems (Solver -> Array Var PackedClause
svClauses Solver
solver)
  (IOUArray Var Double
wbuf :: IOUArray Int Double) <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
0, Var
maxClauseLenforall a. Num a => a -> a -> a
-Var
1)
  IOURef Double
wsumRef <- forall a. MArray IOUArray a IO => a -> IO (IOURef a)
newIOURef (Double
0 :: Double)

  let pickVar :: PackedClause -> IO SAT.Var
      pickVar :: PackedClause -> IO Var
pickVar PackedClause
c = do
        forall a. MArray IOUArray a IO => IOURef a -> a -> IO ()
writeIOURef IOURef Double
wsumRef Double
0
        forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a Var e -> ((Var, e) -> m ()) -> m ()
forAssocsM_ PackedClause
c forall a b. (a -> b) -> a -> b
$ \(Var
k,Var
lit) -> do
          let v :: Var
v = Var -> Var
SAT.litVar Var
lit
          Double
m <- Solver -> Var -> IO Double
getMakeValue Solver
solver Var
v
          Double
b <- Solver -> Var -> IO Double
getBreakValue Solver
solver Var
v
          let w :: Double
w = Double -> Double -> Double
f Double
m Double
b
          forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray Var Double
wbuf Var
k Double
w
          forall a. MArray IOUArray a IO => IOURef a -> (a -> a) -> IO ()
modifyIOURef IOURef Double
wsumRef (forall a. Num a => a -> a -> a
+Double
w)
        Double
wsum <- forall a. MArray IOUArray a IO => IOURef a -> IO a
readIOURef IOURef Double
wsumRef

        let go :: Int -> Double -> IO Int
            go :: Var -> Double -> IO Var
go !Var
k !Double
a = do
              if Bool -> Bool
not (forall a. Ix a => (a, a) -> a -> Bool
inRange (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c) Var
k) then do
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall a b. (a, b) -> b
snd (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c)
              else do
                Double
w <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray IOUArray Var Double
wbuf Var
k
                if Double
a forall a. Ord a => a -> a -> Bool
<= Double
w then
                  forall (m :: * -> *) a. Monad m => a -> m a
return Var
k
                else
                  Var -> Double -> IO Var
go (Var
k forall a. Num a => a -> a -> a
+ Var
1) (Double
a forall a. Num a => a -> a -> a
- Double
w)
        Var
k <- Var -> Double -> IO Var
go Var
0 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Double
0, Double
wsum) Gen RealWorld
gen
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! Var -> Var
SAT.litVar (PackedClause
c forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
k)

  TimeSpec
startCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
  IOURef Var
flipsRef <- forall a. MArray IOUArray a IO => a -> IO (IOURef a)
newIOURef (Var
0::Int)

  -- It's faster to use Control.Exception than using Control.Monad.Except
  let body :: IO ()
body = do
        forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
optMaxTries Options
opt) forall a b. (a -> b) -> a -> b
$ do
          Model
sol <- Callbacks -> Solver -> IO Model
cbGenerateInitialSolution Callbacks
cb Solver
solver
          forall m. IModel m => Solver -> m -> IO ()
setSolution Solver
solver Model
sol
          Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
          forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
optMaxFlips Options
opt) forall a b. (a -> b) -> a -> b
$ do
            Var
s <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Var
s forall a. Eq a => a -> a -> Bool
== Var
0) forall a b. (a -> b) -> a -> b
$ forall a e. Exception e => e -> a
throw Finished
Finished
            Weight
obj <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Weight
obj forall a. Ord a => a -> a -> Bool
<= Options -> Weight
optTarget Options
opt) forall a b. (a -> b) -> a -> b
$ forall a e. Exception e => e -> a
throw Finished
Finished
            PackedClause
c <- Solver -> Options -> IO PackedClause
pickClause Solver
solver Options
opt
            Var
v <- PackedClause -> IO Var
pickVar PackedClause
c
            Solver -> Var -> IO ()
flipVar Solver
solver Var
v
            forall a. MArray IOUArray a IO => IOURef a -> (a -> a) -> IO ()
modifyIOURef IOURef Var
flipsRef forall a. Integral a => a -> a
inc
            Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
  IO ()
body forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(Finished
_::Finished) -> forall (m :: * -> *) a. Monad m => a -> m a
return ())

  TimeSpec
endCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
  Var
flips <- forall a. MArray IOUArray a IO => IOURef a -> IO a
readIOURef IOURef Var
flipsRef
  let totalCPUTime :: TimeSpec
totalCPUTime = TimeSpec
endCPUTime TimeSpec -> TimeSpec -> TimeSpec
`diffTimeSpec` TimeSpec
startCPUTime
      totalCPUTimeSec :: Double
totalCPUTimeSec = forall a b. (Integral a, Num b) => a -> b
fromIntegral (TimeSpec -> Weight
toNanoSecs TimeSpec
totalCPUTime) forall a. Fractional a => a -> a -> a
/ Double
10forall a b. (Num a, Integral b) => a -> b -> a
^(Var
9::Int)
  forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Statistics
svStatistics Solver
solver) forall a b. (a -> b) -> a -> b
$
    Statistics
    { statTotalCPUTime :: TimeSpec
statTotalCPUTime = TimeSpec
totalCPUTime
    , statFlips :: Var
statFlips = Var
flips
    , statFlipsPerSecond :: Double
statFlipsPerSecond = forall a b. (Integral a, Num b) => a -> b
fromIntegral Var
flips forall a. Fractional a => a -> a -> a
/ Double
totalCPUTimeSec
    }

  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 Var
buf :: Vec.UVec SAT.Var) <- forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new

  let pickVar :: PackedClause -> IO SAT.Var
      pickVar :: PackedClause -> IO Var
pickVar PackedClause
c = do
        forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO ()
Vec.clear UVec Var
buf
        let (Var
lb,Var
ub) = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c
        Either Var ()
r <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ do
          Double
_ <- forall a (m :: * -> *) b.
(Num a, Eq a, Monad m) =>
a -> a -> b -> (b -> a -> m b) -> m b
numLoopState Var
lb Var
ub (Double
1.0forall a. Fractional a => a -> a -> a
/Double
0.0) forall a b. (a -> b) -> a -> b
$ \ !Double
b0 !Var
i -> do
            let v :: Var
v = Var -> Var
SAT.litVar (PackedClause
c forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
i)
            Double
b <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Solver -> Var -> IO Double
getBreakValue Solver
solver Var
v
            if Double
b forall a. Ord a => a -> a -> Bool
<= Double
0 then
              forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE Var
v -- freebie move
            else if Double
b forall a. Ord a => a -> a -> Bool
< Double
b0 then do
              forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO ()
Vec.clear UVec Var
buf forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec Var
buf Var
v
              forall (m :: * -> *) a. Monad m => a -> m a
return Double
b
            else if Double
b forall a. Eq a => a -> a -> Bool
== Double
b0 then do
              forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec Var
buf Var
v
              forall (m :: * -> *) a. Monad m => a -> m a
return Double
b0
            else do
              forall (m :: * -> *) a. Monad m => a -> m a
return Double
b0
          forall (m :: * -> *) a. Monad m => a -> m a
return ()
        case Either Var ()
r of
          Left Var
v -> forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
          Right ()
_ -> do
            Bool
flag <- forall g (m :: * -> *). StatefulGen g m => Double -> g -> m Bool
Rand.bernoulli Double
p Gen RealWorld
gen
            if Bool
flag then do
              -- random walk move
              Var
i <- forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Var
lb,Var
ub) Gen RealWorld
gen
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! Var -> Var
SAT.litVar (PackedClause
c forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
i)
            else do
              -- greedy move
              Var
s <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize UVec Var
buf
              if Var
s forall a. Eq a => a -> a -> Bool
== Var
1 then
                forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.unsafeRead UVec Var
buf Var
0
              else do
                Var
i <- forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Var
0, Var
s forall a. Num a => a -> a -> a
- Var
1) Gen RealWorld
gen
                forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.unsafeRead UVec Var
buf Var
i

  TimeSpec
startCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
  IOURef Var
flipsRef <- forall a. MArray IOUArray a IO => a -> IO (IOURef a)
newIOURef (Var
0::Int)

  -- It's faster to use Control.Exception than using Control.Monad.Except
  let body :: IO ()
body = do
        forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
optMaxTries Options
opt) forall a b. (a -> b) -> a -> b
$ do
          Model
sol <- Callbacks -> Solver -> IO Model
cbGenerateInitialSolution Callbacks
cb Solver
solver
          forall m. IModel m => Solver -> m -> IO ()
setSolution Solver
solver Model
sol
          Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
          forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
optMaxFlips Options
opt) forall a b. (a -> b) -> a -> b
$ do
            Var
s <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Var
s forall a. Eq a => a -> a -> Bool
== Var
0) forall a b. (a -> b) -> a -> b
$ forall a e. Exception e => e -> a
throw Finished
Finished
            Weight
obj <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Weight
obj forall a. Ord a => a -> a -> Bool
<= Options -> Weight
optTarget Options
opt) forall a b. (a -> b) -> a -> b
$ forall a e. Exception e => e -> a
throw Finished
Finished
            PackedClause
c <- Solver -> Options -> IO PackedClause
pickClause Solver
solver Options
opt
            Var
v <- PackedClause -> IO Var
pickVar PackedClause
c
            Solver -> Var -> IO ()
flipVar Solver
solver Var
v
            forall a. MArray IOUArray a IO => IOURef a -> (a -> a) -> IO ()
modifyIOURef IOURef Var
flipsRef forall a. Integral a => a -> a
inc
            Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
  IO ()
body forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(Finished
_::Finished) -> forall (m :: * -> *) a. Monad m => a -> m a
return ())

  TimeSpec
endCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
  Var
flips <- forall a. MArray IOUArray a IO => IOURef a -> IO a
readIOURef IOURef Var
flipsRef
  let totalCPUTime :: TimeSpec
totalCPUTime = TimeSpec
endCPUTime TimeSpec -> TimeSpec -> TimeSpec
`diffTimeSpec` TimeSpec
startCPUTime
      totalCPUTimeSec :: Double
totalCPUTimeSec = forall a b. (Integral a, Num b) => a -> b
fromIntegral (TimeSpec -> Weight
toNanoSecs TimeSpec
totalCPUTime) forall a. Fractional a => a -> a -> a
/ Double
10forall a b. (Num a, Integral b) => a -> b -> a
^(Var
9::Int)
  forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Statistics
svStatistics Solver
solver) forall a b. (a -> b) -> a -> b
$
    Statistics
    { statTotalCPUTime :: TimeSpec
statTotalCPUTime = TimeSpec
totalCPUTime
    , statFlips :: Var
statFlips = Var
flips
    , statFlipsPerSecond :: Double
statFlipsPerSecond = forall a b. (Integral a, Num b) => a -> b
fromIntegral Var
flips forall a. Fractional a => a -> a -> a
/ Double
totalCPUTimeSec
    }

  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 :: forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> (e -> e) -> m ()
modifyArray a i e
a i
i e -> e
f = do
  e
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
  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_ :: forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a Var e -> ((Var, e) -> m ()) -> m ()
forAssocsM_ a Var e
a (Var, e) -> m ()
f = do
  let (Var
lb,Var
ub) = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds a Var e
a
  forall a (m :: * -> *).
(Num a, Ord a, Monad m) =>
a -> a -> (a -> m ()) -> m ()
numLoop Var
lb Var
ub forall a b. (a -> b) -> a -> b
$ \Var
i ->
    (Var, e) -> m ()
f (Var
i, forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt a Var e
a Var
i)

{-# INLINE inc #-}
inc :: Integral a => a -> a
inc :: forall a. Integral a => a -> a
inc a
a = a
aforall a. Num a => a -> a -> a
+a
1

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