{-# LANGUAGE CPP #-}
{-# 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    = Var -> Weight
forall a b. (Integral a, Num b) => a -> b
fromIntegral (CNF -> Var
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 :: Var -> Bool
m Var
_ = Bool
False
      nv :: Var
nv = WCNF -> Var
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 a. a -> IO a
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 a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (Weight, PackedClause) -> IO (Maybe (Weight, PackedClause))
forall a. a -> IO a
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' = (Var, Var) -> Clause -> PackedClause
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, Clause -> Var
forall a. [a] -> Var
forall (t :: * -> *) a. Foldable t => t a -> Var
length Clause
c Var -> Var -> Var
forall a. Num a => a -> a -> a
- Var
1) Clause
c
        PackedClause
-> IO (Maybe (Weight, PackedClause))
-> IO (Maybe (Weight, PackedClause))
forall a b. a -> b -> b
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 a. a -> IO a
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 :: Var
len = [(Weight, PackedClause)] -> Var
forall a. [a] -> Var
forall (t :: * -> *) a. Foldable t => t a -> Var
length [(Weight, PackedClause)]
cs
      clauses :: Array Var PackedClause
clauses  = (Var, Var) -> [PackedClause] -> Array Var PackedClause
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, Var
len Var -> Var -> Var
forall a. Num a => a -> a -> a
- Var
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 Var Weight
weights  = (Var, Var) -> [Weight] -> Array Var Weight
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, Var
len Var -> Var -> Var
forall a. Num a => a -> a -> a
- Var
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 Var Double
weightsF = (Var, Var) -> [Double] -> UArray Var Double
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, Var
len Var -> Var -> Var
forall a. Num a => a -> a -> a
- Var
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 Var (Seq (Var, Bool))
varOccurs' :: IOArray SAT.Var (Seq.Seq (Int, Bool))) <- (Var, Var) -> Seq (Var, Bool) -> IO (IOArray Var (Seq (Var, Bool)))
forall i.
Ix i =>
(i, i) -> Seq (Var, Bool) -> IO (IOArray i (Seq (Var, Bool)))
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (Var
1, Var
nv) Seq (Var, Bool)
forall a. Seq a
Seq.empty

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

  Array Var PackedClause -> ((Var, PackedClause) -> IO ()) -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a Var e -> ((Var, e) -> m ()) -> m ()
forAssocsM_ Array Var PackedClause
clauses (((Var, PackedClause) -> IO ()) -> IO ())
-> ((Var, PackedClause) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Var
c,PackedClause
clause) -> do
    let n :: Int32
n = [Int32] -> Int32
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int32
1 | Var
lit <- PackedClause -> Clause
forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems PackedClause
clause, (Var -> Bool) -> Var -> Bool
forall m. IModel m => m -> Var -> Bool
SAT.evalLit Var -> Bool
m Var
lit]
    IOUArray Var Int32 -> Var -> Int32 -> IO ()
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
    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
      Var
i <- UVec Var -> IO Var
forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize UVec Var
unsatClauses
      IOUArray Var Var -> Var -> Var -> IO ()
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
      UVec Var -> Var -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec Var
unsatClauses Var
c
      IORef Weight -> (Weight -> Weight) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef Weight
objRef ((Array Var Weight
weights Array Var Weight -> Var -> Weight
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
c) Weight -> Weight -> Weight
forall a. Num a => a -> a -> a
+)
    Clause -> (Var -> 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) ((Var -> IO ()) -> IO ()) -> (Var -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Var
lit -> do
      let v :: Var
v = Var -> Var
SAT.litVar Var
lit
      let b :: Bool
b = (Var -> Bool) -> Var -> Bool
forall m. IModel m => m -> Var -> Bool
SAT.evalLit Var -> Bool
m Var
lit
      Bool -> IO () -> IO ()
forall a b. a -> b -> b
seq Bool
b (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ IOArray Var (Seq (Var, Bool))
-> Var -> (Seq (Var, Bool) -> Seq (Var, Bool)) -> IO ()
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 (Seq (Var, Bool) -> (Var, Bool) -> Seq (Var, Bool)
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)) <- (Var, Var) -> IO (IOArray Var (UArray Var Var))
forall i. Ix i => (i, i) -> IO (IOArray i (UArray Var Var))
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
1, Var
nv)
    Clause -> (Var -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var
1 .. Var
nv] ((Var -> IO ()) -> IO ()) -> (Var -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Var
v -> do
      Seq (Var, Bool)
s <- IOArray Var (Seq (Var, Bool)) -> Var -> IO (Seq (Var, Bool))
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
      IOArray Var (UArray Var Var) -> Var -> UArray Var Var -> IO ()
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 (UArray Var Var -> IO ()) -> UArray Var Var -> IO ()
forall a b. (a -> b) -> a -> b
$ (Var, Var) -> Clause -> UArray Var Var
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, Seq (Var, Bool) -> Var
forall a. Seq a -> Var
Seq.length Seq (Var, Bool)
s Var -> Var -> Var
forall a. Num a => a -> a -> a
- Var
1) (((Var, Bool) -> Var) -> [(Var, Bool)] -> Clause
forall a b. (a -> b) -> [a] -> [b]
map (Var, Bool) -> Var
forall a b. (a, b) -> a
fst (Seq (Var, Bool) -> [(Var, Bool)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Var, Bool)
s))
    IOArray Var (UArray Var Var) -> IO (Array Var (UArray Var Var))
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)) <- (Var, Var) -> IO (IOArray Var (IOUArray Var Bool))
forall i. Ix i => (i, i) -> IO (IOArray i (IOUArray Var Bool))
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
1, Var
nv)
    Clause -> (Var -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var
1 .. Var
nv] ((Var -> IO ()) -> IO ()) -> (Var -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Var
v -> do
      Seq (Var, Bool)
s <- IOArray Var (Seq (Var, Bool)) -> Var -> IO (Seq (Var, Bool))
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 <- (Var, Var) -> IO (IOUArray Var Bool)
forall i. Ix i => (i, i) -> IO (IOUArray i Bool)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
0, Seq (Var, Bool) -> Var
forall a. Seq a -> Var
Seq.length Seq (Var, Bool)
s Var -> Var -> Var
forall a. Num a => a -> a -> a
- Var
1)
      [(Var, (Var, Bool))] -> ((Var, (Var, Bool)) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Clause -> [(Var, Bool)] -> [(Var, (Var, Bool))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var
0..] (Seq (Var, Bool) -> [(Var, Bool)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Var, Bool)
s)) (((Var, (Var, Bool)) -> IO ()) -> IO ())
-> ((Var, (Var, Bool)) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Var
j,(Var, Bool)
a) -> IOUArray Var Bool -> Var -> Bool -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray Var Bool
ss Var
j ((Var, Bool) -> Bool
forall a b. (a, b) -> b
snd (Var, Bool)
a)
      IOArray Var (IOUArray Var Bool)
-> Var -> IOUArray Var Bool -> IO ()
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
    IOArray Var (IOUArray Var Bool)
-> IO (Array Var (IOUArray Var 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 Var (IOUArray Var Bool)
arr

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

  Weight
bestObj <- IORef Weight -> IO Weight
forall a. IORef a -> IO a
readIORef IORef Weight
objRef
  Model
bestSol <- IOUArray Var 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 Var 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)
IO GenIO
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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Solver -> IO Solver) -> Solver -> IO Solver
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)
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 -> Var -> IO ()
flipVar Solver
solver Var
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 Var Var
occurs = Solver -> Array Var (UArray Var Var)
svVarOccurs Solver
solver Array Var (UArray Var Var) -> Var -> UArray Var Var
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 Array Var (IOUArray Var Bool) -> Var -> IOUArray Var Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
  UArray Var Var -> IO () -> IO ()
forall a b. a -> b -> b
seq UArray Var Var
occurs (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ IOUArray Var Bool -> IO () -> IO ()
forall a b. a -> b -> b
seq IOUArray Var Bool
occursState (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  IOUArray Var Bool -> Var -> (Bool -> Bool) -> IO ()
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
  UArray Var Var -> ((Var, Var) -> IO ()) -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a Var e -> ((Var, e) -> m ()) -> m ()
forAssocsM_ UArray Var Var
occurs (((Var, Var) -> IO ()) -> IO ()) -> ((Var, Var) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Var
j,!Var
c) -> do
    Bool
b <- IOUArray Var Bool -> Var -> IO Bool
forall i. Ix i => IOUArray i Bool -> Var -> IO Bool
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 <- IOUArray Var Int32 -> Var -> IO Int32
forall i. Ix i => IOUArray i Int32 -> Var -> IO Int32
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
    IOUArray Var Bool -> Var -> Bool -> IO ()
forall i. Ix i => IOUArray i Bool -> Var -> Bool -> IO ()
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
      IOUArray Var Int32 -> Var -> Int32 -> IO ()
forall i. Ix i => IOUArray i Int32 -> Var -> Int32 -> IO ()
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
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
        Var
i <- UVec Var -> IO Var
forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
        UVec Var -> Var -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
c
        IOUArray Var Var -> Var -> Var -> IO ()
forall i. Ix i => IOUArray i Var -> Var -> Var -> IO ()
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
        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 Var Weight -> Var -> Weight
forall i. Ix i => Array i Weight -> Var -> Weight
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
      IOUArray Var Int32 -> Var -> Int32 -> IO ()
forall i. Ix i => IOUArray i Int32 -> Var -> Int32 -> IO ()
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
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
        Var
s <- UVec Var -> IO Var
forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
        Var
i <- IOUArray Var Var -> Var -> IO Var
forall i. Ix i => IOUArray i Var -> Var -> IO Var
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
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Var
i Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
sVar -> Var -> Var
forall a. Num a => a -> a -> a
-Var
1) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          let i2 :: Var
i2 = Var
sVar -> Var -> Var
forall a. Num a => a -> a -> a
-Var
1
          Var
c2 <- UVec Var -> Var -> IO Var
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.unsafeRead (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
i2
          UVec Var -> Var -> Var -> IO ()
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
          UVec Var -> Var -> Var -> IO ()
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
          IOUArray Var Var -> Var -> Var -> IO ()
forall i. Ix i => IOUArray i Var -> Var -> Var -> IO ()
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
_ <- UVec Var -> IO Var
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.unsafePop (Solver -> UVec Var
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 Var Weight -> Var -> Weight
forall i. Ix i => Array i Weight -> Var -> Weight
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt (Solver -> Array Var Weight
svClauseWeights Solver
solver) Var
c))
        () -> IO ()
forall a. a -> IO a
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 <- IOUArray Var Bool -> IO (Var, Var)
forall i. Ix i => IOUArray i Bool -> IO (i, i)
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)
  Clause -> (Var -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ((Var, Var) -> Clause
forall a. Ix a => (a, a) -> [a]
range (Var, Var)
b) ((Var -> IO ()) -> IO ()) -> (Var -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Var
v -> do
    Bool
val <- IOUArray Var Bool -> Var -> IO Bool
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' = m -> Var -> Bool
forall m. IModel m => m -> Var -> Bool
SAT.evalVar m
m Var
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 -> Var -> IO ()
flipVar Solver
solver Var
v

getNumVars :: Solver -> IO Int
getNumVars :: Solver -> IO Var
getNumVars Solver
solver = Var -> IO Var
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> IO Var) -> Var -> IO Var
forall a b. (a -> b) -> a -> b
$ (Var, Var) -> Var
forall a. Ix a => (a, a) -> Var
rangeSize ((Var, Var) -> Var) -> (Var, Var) -> Var
forall a b. (a -> b) -> a -> b
$ Array Var (UArray Var Var) -> (Var, Var)
forall i. Ix i => Array i (UArray Var Var) -> (i, i)
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 = 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 -> Var -> IO Double
getMakeValue Solver
solver Var
v = do
  let occurs :: UArray Var Var
occurs = Solver -> Array Var (UArray Var Var)
svVarOccurs Solver
solver Array Var (UArray Var Var) -> Var -> UArray Var Var
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
      (Var
lb,Var
ub) = UArray Var Var -> (Var, Var)
forall i. Ix i => UArray i Var -> (i, i)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds UArray Var Var
occurs
  UArray Var Var -> IO Double -> IO Double
forall a b. a -> b -> b
seq UArray Var Var
occurs (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$ Var -> IO Double -> IO Double
forall a b. a -> b -> b
seq Var
lb (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$ Var -> IO Double -> IO Double
forall a b. a -> b -> b
seq Var
ub (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$
    Var -> Var -> Double -> (Double -> Var -> IO Double) -> IO 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
0 ((Double -> Var -> IO Double) -> IO Double)
-> (Double -> Var -> IO Double) -> IO Double
forall a b. (a -> b) -> a -> b
$ \ !Double
r !Var
i -> do
      let c :: Var
c = UArray Var Var -> Var -> Var
forall i. Ix i => UArray i Var -> Var -> Var
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt UArray Var Var
occurs Var
i
      Int32
n <- IOUArray Var Int32 -> Var -> IO Int32
forall i. Ix i => IOUArray i Int32 -> Var -> IO Int32
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
      Double -> IO Double
forall a. a -> IO a
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 Var Double -> Var -> Double
forall i. Ix i => UArray i Double -> Var -> Double
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 Array Var (UArray Var Var) -> Var -> UArray Var Var
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 Array Var (IOUArray Var Bool) -> Var -> IOUArray Var Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
      (Var
lb,Var
ub) = UArray Var Var -> (Var, Var)
forall i. Ix i => UArray i Var -> (i, i)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds UArray Var Var
occurs
  UArray Var Var -> IO Double -> IO Double
forall a b. a -> b -> b
seq UArray Var Var
occurs (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$ IOUArray Var Bool -> IO Double -> IO Double
forall a b. a -> b -> b
seq IOUArray Var Bool
occursState (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$ Var -> IO Double -> IO Double
forall a b. a -> b -> b
seq Var
lb (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$ Var -> IO Double -> IO Double
forall a b. a -> b -> b
seq Var
ub (IO Double -> IO Double) -> IO Double -> IO Double
forall a b. (a -> b) -> a -> b
$
    Var -> Var -> Double -> (Double -> Var -> IO Double) -> IO 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
0 ((Double -> Var -> IO Double) -> IO Double)
-> (Double -> Var -> IO Double) -> IO Double
forall a b. (a -> b) -> a -> b
$ \ !Double
r !Var
i -> do
      Bool
b <- IOUArray Var Bool -> Var -> IO Bool
forall i. Ix i => IOUArray i Bool -> Var -> IO Bool
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 = UArray Var Var -> Var -> Var
forall i. Ix i => UArray i Var -> Var -> Var
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt UArray Var Var
occurs Var
i
        Int32
n <- IOUArray Var Int32 -> Var -> IO Int32
forall i. Ix i => IOUArray i Int32 -> Var -> IO Int32
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
        Double -> IO Double
forall a. a -> IO a
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 Var Double -> Var -> Double
forall i. Ix i => UArray i Double -> Var -> Double
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
        Double -> IO Double
forall a. a -> IO a
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
(Options -> Options -> Bool)
-> (Options -> Options -> Bool) -> Eq Options
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Options -> Options -> Bool
== :: Options -> Options -> Bool
$c/= :: Options -> Options -> Bool
/= :: Options -> Options -> Bool
Eq, Var -> Options -> ShowS
[Options] -> ShowS
Options -> String
(Var -> Options -> ShowS)
-> (Options -> String) -> ([Options] -> ShowS) -> Show Options
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Var -> Options -> ShowS
showsPrec :: Var -> Options -> ShowS
$cshow :: Options -> String
show :: Options -> String
$cshowList :: [Options] -> ShowS
showList :: [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
_ -> () -> IO ()
forall a. a -> IO a
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
(Statistics -> Statistics -> Bool)
-> (Statistics -> Statistics -> Bool) -> Eq Statistics
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Statistics -> Statistics -> Bool
== :: Statistics -> Statistics -> Bool
$c/= :: Statistics -> Statistics -> Bool
/= :: Statistics -> Statistics -> Bool
Eq, Var -> Statistics -> ShowS
[Statistics] -> ShowS
Statistics -> String
(Var -> Statistics -> ShowS)
-> (Statistics -> String)
-> ([Statistics] -> ShowS)
-> Show Statistics
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Var -> Statistics -> ShowS
showsPrec :: Var -> Statistics -> ShowS
$cshow :: Statistics -> String
show :: Statistics -> String
$cshowList :: [Statistics] -> ShowS
showList :: [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) <- (Var, Var) -> IO (IOUArray Var Bool)
forall i. Ix i => (i, i) -> IO (IOUArray i Bool)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
1,Var
n)
  Clause -> (Var -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var
1..Var
n] ((Var -> IO ()) -> IO ()) -> (Var -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Var
v -> do
    Bool
b <- GenIO -> IO Bool
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
Gen (PrimState m) -> m a
forall (m :: * -> *). PrimMonad m => Gen (PrimState m) -> m Bool
Rand.uniform Gen RealWorld
GenIO
gen
    IOUArray Var Bool -> Var -> Bool -> IO ()
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
  IOUArray Var 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 Var 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 Var 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 Var 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 :: Var -> Weight -> IO Var
f !Var
j !Weight
x = do
          Var
c <- UVec Var -> Var -> IO Var
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 Array Var Weight -> Var -> Weight
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
c
          if Weight
x Weight -> Weight -> Bool
forall a. Ord a => a -> a -> Bool
< Weight
w then
            Var -> IO Var
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
c
          else
            Var -> Weight -> IO Var
f (Var
j Var -> Var -> Var
forall a. Num a => a -> a -> a
+ Var
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
    Var
c <- Var -> Weight -> IO Var
f Var
0 Weight
x
    PackedClause -> IO PackedClause
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PackedClause -> IO PackedClause)
-> PackedClause -> IO PackedClause
forall a b. (a -> b) -> a -> b
$ (Solver -> Array Var PackedClause
svClauses Solver
solver Array Var PackedClause -> Var -> PackedClause
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
c)
  else do
    Var
s <- UVec Var -> IO Var
forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
    Var
j <- (Var, Var) -> GenIO -> IO Var
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
forall (m :: * -> *).
PrimMonad m =>
(Var, Var) -> Gen (PrimState m) -> m Var
Rand.uniformR (Var
0, Var
s Var -> Var -> Var
forall a. Num a => a -> a -> a
- Var
1) Gen RealWorld
GenIO
gen -- For integral types inclusive range is used
    (Var -> PackedClause) -> IO Var -> IO PackedClause
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Solver -> Array Var PackedClause
svClauses Solver
solver Array Var PackedClause -> Var -> PackedClause
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
!) (IO Var -> IO PackedClause) -> IO Var -> IO PackedClause
forall a b. (a -> b) -> a -> b
$ UVec Var -> Var -> IO Var
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 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
forall (m :: * -> *).
PrimMonad m =>
(Word32, Word32) -> Gen (PrimState m) -> m Word32
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 -> Var -> Weight
forall a. Bits a => a -> Var -> a
`shiftR` Var
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
forall (m :: * -> *). PrimMonad m => Gen (PrimState m) -> m Word32
Rand.uniform Gen (PrimState m)
gen
      Weight -> m Weight
forall a. a -> m a
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 -> Var -> Weight
forall a. Bits a => a -> Var -> a
`shiftL` Var
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 (Var -> Finished -> ShowS
[Finished] -> ShowS
Finished -> String
(Var -> Finished -> ShowS)
-> (Finished -> String) -> ([Finished] -> ShowS) -> Show Finished
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Var -> Finished -> ShowS
showsPrec :: Var -> Finished -> ShowS
$cshow :: Finished -> String
show :: Finished -> String
$cshowList :: [Finished] -> ShowS
showList :: [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 (Var, Var) -> Var
forall a. Ix a => (a, a) -> Var
rangeSize (Array Var PackedClause -> (Var, Var)
forall i. Ix i => Array i PackedClause -> (i, i)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds (Solver -> Array Var PackedClause
svClauses Solver
solver)) Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
0
        then Var
0
        else Clause -> Var
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Clause -> Var) -> Clause -> Var
forall a b. (a -> b) -> a -> b
$ (PackedClause -> Var) -> [PackedClause] -> Clause
forall a b. (a -> b) -> [a] -> [b]
map ((Var, Var) -> Var
forall a. Ix a => (a, a) -> Var
rangeSize ((Var, Var) -> Var)
-> (PackedClause -> (Var, Var)) -> PackedClause -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PackedClause -> (Var, Var)
forall i. Ix i => Array i Var -> (i, i)
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 Var PackedClause -> [PackedClause]
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) <- (Var, Var) -> IO (IOUArray Var Double)
forall i. Ix i => (i, i) -> IO (IOUArray i Double)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
0, Var
maxClauseLenVar -> Var -> Var
forall a. Num a => a -> a -> a
-Var
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 Var
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 -> ((Var, Var) -> IO ()) -> IO ()
forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a Var e -> ((Var, e) -> m ()) -> m ()
forAssocsM_ PackedClause
c (((Var, Var) -> IO ()) -> IO ()) -> ((Var, Var) -> IO ()) -> IO ()
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
          IOUArray Var Double -> Var -> Double -> IO ()
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
          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 :: Var -> Double -> IO Var
go !Var
k !Double
a = do
              if Bool -> Bool
not ((Var, Var) -> Var -> Bool
forall a. Ix a => (a, a) -> a -> Bool
inRange (PackedClause -> (Var, Var)
forall i. Ix i => Array i Var -> (i, i)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c) Var
k) then do
                Var -> IO Var
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> IO Var) -> Var -> IO Var
forall a b. (a -> b) -> a -> b
$! (Var, Var) -> Var
forall a b. (a, b) -> b
snd (PackedClause -> (Var, Var)
forall i. Ix i => Array i Var -> (i, i)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c)
              else do
                Double
w <- IOUArray Var Double -> Var -> IO Double
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
w then
                  Var -> IO Var
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
k
                else
                  Var -> Double -> IO Var
go (Var
k Var -> Var -> Var
forall a. Num a => a -> a -> a
+ Var
1) (Double
a Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
w)
        Var
k <- Var -> Double -> IO Var
go Var
0 (Double -> IO Var) -> IO Double -> IO Var
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
forall (m :: * -> *).
PrimMonad m =>
(Double, Double) -> Gen (PrimState m) -> m Double
Rand.uniformR (Double
0, Double
wsum) Gen RealWorld
GenIO
gen
        Var -> IO Var
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> IO Var) -> Var -> IO Var
forall a b. (a -> b) -> a -> b
$! Var -> Var
SAT.litVar (PackedClause
c PackedClause -> Var -> Var
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 <- Var -> IO (IOURef Var)
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
        Var -> IO () -> IO ()
forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
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
          Var -> IO () -> IO ()
forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
optMaxFlips Options
opt) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
            Var
s <- UVec Var -> IO Var
forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
            Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Var
s Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
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
            Var
v <- PackedClause -> IO Var
pickVar PackedClause
c
            Solver -> Var -> IO ()
flipVar Solver
solver Var
v
            IOURef Var -> (Var -> Var) -> IO ()
forall a. MArray IOUArray a IO => IOURef a -> (a -> a) -> IO ()
modifyIOURef IOURef Var
flipsRef Var -> Var
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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

  TimeSpec
endCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
  Var
flips <- IOURef Var -> IO Var
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 = 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 -> Var -> Double
forall a b. (Num a, Integral b) => a -> b -> a
^(Var
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
    { statTotalCPUTime :: TimeSpec
statTotalCPUTime = TimeSpec
totalCPUTime
    , statFlips :: Var
statFlips = Var
flips
    , statFlipsPerSecond :: Double
statFlipsPerSecond = Var -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Var
flips Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
totalCPUTimeSec
    }

  () -> IO ()
forall a. a -> IO a
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) <- IO (UVec 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
        UVec Var -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO ()
Vec.clear UVec Var
buf
        let (Var
lb,Var
ub) = PackedClause -> (Var, Var)
forall i. Ix i => Array i Var -> (i, i)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c
        Either Var ()
r <- ExceptT Var IO () -> IO (Either Var ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT Var IO () -> IO (Either Var ()))
-> ExceptT Var IO () -> IO (Either Var ())
forall a b. (a -> b) -> a -> b
$ do
          Double
_ <- Var
-> Var
-> Double
-> (Double -> Var -> ExceptT Var IO Double)
-> ExceptT Var IO 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.0Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/Double
0.0) ((Double -> Var -> ExceptT Var IO Double) -> ExceptT Var IO Double)
-> (Double -> Var -> ExceptT Var IO Double)
-> ExceptT Var IO Double
forall a b. (a -> b) -> a -> b
$ \ !Double
b0 !Var
i -> do
            let v :: Var
v = Var -> Var
SAT.litVar (PackedClause
c PackedClause -> Var -> Var
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
i)
            Double
b <- IO Double -> ExceptT Var IO Double
forall (m :: * -> *) a. Monad m => m a -> ExceptT Var m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Double -> ExceptT Var IO Double)
-> IO Double -> ExceptT Var IO Double
forall a b. (a -> b) -> a -> b
$ Solver -> Var -> IO Double
getBreakValue Solver
solver Var
v
            if Double
b Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
0 then
              Var -> ExceptT Var IO Double
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE Var
v -- freebie move
            else if Double
b Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
b0 then do
              IO () -> ExceptT Var IO ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT Var m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ExceptT Var IO ()) -> IO () -> ExceptT Var IO ()
forall a b. (a -> b) -> a -> b
$ UVec Var -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO ()
Vec.clear UVec Var
buf IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> UVec Var -> Var -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec Var
buf Var
v
              Double -> ExceptT Var IO Double
forall a. a -> ExceptT Var IO a
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 Var IO ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT Var m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ExceptT Var IO ()) -> IO () -> ExceptT Var IO ()
forall a b. (a -> b) -> a -> b
$ UVec Var -> Var -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec Var
buf Var
v
              Double -> ExceptT Var IO Double
forall a. a -> ExceptT Var IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Double
b0
            else do
              Double -> ExceptT Var IO Double
forall a. a -> ExceptT Var IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Double
b0
          () -> ExceptT Var IO ()
forall a. a -> ExceptT Var IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        case Either Var ()
r of
          Left Var
v -> Var -> IO Var
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
          Right ()
_ -> do
            Bool
flag <- Double -> Gen RealWorld -> IO Bool
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 <- (Var, Var) -> GenIO -> IO Var
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
forall (m :: * -> *).
PrimMonad m =>
(Var, Var) -> Gen (PrimState m) -> m Var
Rand.uniformR (Var
lb,Var
ub) Gen RealWorld
GenIO
gen
              Var -> IO Var
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> IO Var) -> Var -> IO Var
forall a b. (a -> b) -> a -> b
$! Var -> Var
SAT.litVar (PackedClause
c PackedClause -> Var -> Var
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
i)
            else do
              -- greedy move
              Var
s <- UVec Var -> IO Var
forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize UVec Var
buf
              if Var
s Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
1 then
                UVec Var -> Var -> IO Var
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.unsafeRead UVec Var
buf Var
0
              else do
                Var
i <- (Var, Var) -> GenIO -> IO Var
forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
forall (m :: * -> *).
PrimMonad m =>
(Var, Var) -> Gen (PrimState m) -> m Var
Rand.uniformR (Var
0, Var
s Var -> Var -> Var
forall a. Num a => a -> a -> a
- Var
1) Gen RealWorld
GenIO
gen
                UVec Var -> Var -> IO Var
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 <- Var -> IO (IOURef Var)
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
        Var -> IO () -> IO ()
forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
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
          Var -> IO () -> IO ()
forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
optMaxFlips Options
opt) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
            Var
s <- UVec Var -> IO Var
forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
            Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Var
s Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
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
            Var
v <- PackedClause -> IO Var
pickVar PackedClause
c
            Solver -> Var -> IO ()
flipVar Solver
solver Var
v
            IOURef Var -> (Var -> Var) -> IO ()
forall a. MArray IOUArray a IO => IOURef a -> (a -> a) -> IO ()
modifyIOURef IOURef Var
flipsRef Var -> Var
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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

  TimeSpec
endCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
  Var
flips <- IOURef Var -> IO Var
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 = 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 -> Var -> Double
forall a b. (Num a, Integral b) => a -> b -> a
^(Var
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
    { statTotalCPUTime :: TimeSpec
statTotalCPUTime = TimeSpec
totalCPUTime
    , statFlips :: Var
statFlips = Var
flips
    , statFlipsPerSecond :: Double
statFlipsPerSecond = Var -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Var
flips Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
totalCPUTimeSec
    }

  () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

#if !MIN_VERSION_array(0,5,6)

{-# 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 <- 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)

#endif

{-# 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) = a Var e -> (Var, Var)
forall i. Ix i => a i e -> (i, i)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds a Var e
a
  Var -> Var -> (Var -> m ()) -> m ()
forall a (m :: * -> *).
(Num a, Ord a, Monad m) =>
a -> a -> (a -> m ()) -> m ()
numLoop Var
lb Var
ub ((Var -> m ()) -> m ()) -> (Var -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Var
i ->
    (Var, e) -> m ()
f (Var
i, a Var e -> Var -> e
forall i. Ix i => a i e -> Var -> e
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
aa -> a -> a
forall a. Num a => a -> a -> a
+a
1

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