{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module ToySolver.SAT.PBO.Context
( Context (..)
, getBestValue
, getBestModel
, isOptimum
, isFinished
, getSearchUpperBound
, setFinished
, SimpleContext
, newSimpleContext
, newSimpleContext2
, setOnUpdateBestSolution
, setOnUpdateLowerBound
, setLogger
, Normalized
, normalize
) where
import Control.Monad
import Control.Concurrent.STM
import Data.IORef
import Data.Maybe
import qualified ToySolver.SAT.Types as SAT
class Context a where
getObjectiveFunction :: a -> SAT.PBLinSum
evalObjectiveFunction :: a -> SAT.Model -> Integer
isUnsat :: a -> STM Bool
getBestSolution :: a -> STM (Maybe (SAT.Model, Integer))
getLowerBound :: a -> STM Integer
setUnsat :: a -> IO ()
addSolution :: a -> SAT.Model -> IO ()
addLowerBound :: a -> Integer -> IO ()
logMessage :: a -> String -> IO ()
evalObjectiveFunction a
c Model
m = forall m. IModel m => m -> PBLinSum -> Integer
SAT.evalPBLinSum Model
m (forall a. Context a => a -> PBLinSum
getObjectiveFunction a
c)
getBestValue :: Context a => a -> STM (Maybe Integer)
getBestValue :: forall a. Context a => a -> STM (Maybe Integer)
getBestValue a
cxt = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> STM (Maybe (Model, Integer))
getBestSolution a
cxt
getBestModel :: Context a => a -> STM (Maybe SAT.Model)
getBestModel :: forall a. Context a => a -> STM (Maybe Model)
getBestModel a
cxt = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> STM (Maybe (Model, Integer))
getBestSolution a
cxt
isOptimum :: Context a => a -> STM Bool
isOptimum :: forall a. Context a => a -> STM Bool
isOptimum a
cxt = do
Maybe Integer
ub <- forall a. Context a => a -> STM (Maybe Integer)
getBestValue a
cxt
Integer
lb <- forall a. Context a => a -> STM Integer
getLowerBound a
cxt
case Maybe Integer
ub of
Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just Integer
val -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Integer
val forall a. Ord a => a -> a -> Bool
<= Integer
lb
isFinished :: Context a => a -> STM Bool
isFinished :: forall a. Context a => a -> STM Bool
isFinished a
cxt = do
Bool
b1 <- forall a. Context a => a -> STM Bool
isUnsat a
cxt
Bool
b2 <- forall a. Context a => a -> STM Bool
isOptimum a
cxt
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool
b1 Bool -> Bool -> Bool
|| Bool
b2
getSearchUpperBound :: Context a => a -> STM Integer
getSearchUpperBound :: forall a. Context a => a -> STM Integer
getSearchUpperBound a
ctx = do
Maybe Integer
ret <- forall a. Context a => a -> STM (Maybe Integer)
getBestValue a
ctx
case Maybe Integer
ret of
Just Integer
val -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Integer
val forall a. Num a => a -> a -> a
- Integer
1
Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PBLinSum -> Integer
SAT.pbLinUpperBound forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> PBLinSum
getObjectiveFunction a
ctx
setFinished :: Context a => a -> IO ()
setFinished :: forall a. Context a => a -> IO ()
setFinished a
cxt = do
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ do
Maybe Integer
ret <- forall a. Context a => a -> STM (Maybe Integer)
getBestValue a
cxt
case Maybe Integer
ret of
Just Integer
val -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> Integer -> IO ()
addLowerBound a
cxt Integer
val
Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Context a => a -> IO ()
setUnsat a
cxt
data SimpleContext
= SimpleContext
{ SimpleContext -> PBLinSum
scGetObjectiveFunction :: SAT.PBLinSum
, SimpleContext -> Model -> Integer
scEvalObjectiveFunction :: SAT.Model -> Integer
, SimpleContext -> TVar Bool
scUnsatRef :: TVar Bool
, SimpleContext -> TVar (Maybe (Model, Integer))
scBestSolutionRef :: TVar (Maybe (SAT.Model, Integer))
, SimpleContext -> TVar Integer
scLowerBoundRef :: TVar Integer
, SimpleContext -> IORef (Model -> Integer -> IO ())
scOnUpdateBestSolutionRef :: IORef (SAT.Model -> Integer -> IO ())
, SimpleContext -> IORef (Integer -> IO ())
scOnUpdateLowerBoundRef :: IORef (Integer -> IO ())
, SimpleContext -> IORef (String -> IO ())
scLoggerRef :: IORef (String -> IO ())
}
instance Context SimpleContext where
getObjectiveFunction :: SimpleContext -> PBLinSum
getObjectiveFunction = SimpleContext -> PBLinSum
scGetObjectiveFunction
evalObjectiveFunction :: SimpleContext -> Model -> Integer
evalObjectiveFunction = SimpleContext -> Model -> Integer
scEvalObjectiveFunction
isUnsat :: SimpleContext -> STM Bool
isUnsat SimpleContext
sc = forall a. TVar a -> STM a
readTVar (SimpleContext -> TVar Bool
scUnsatRef SimpleContext
sc)
getBestSolution :: SimpleContext -> STM (Maybe (Model, Integer))
getBestSolution SimpleContext
sc = forall a. TVar a -> STM a
readTVar (SimpleContext -> TVar (Maybe (Model, Integer))
scBestSolutionRef SimpleContext
sc)
getLowerBound :: SimpleContext -> STM Integer
getLowerBound SimpleContext
sc = forall a. TVar a -> STM a
readTVar (SimpleContext -> TVar Integer
scLowerBoundRef SimpleContext
sc)
setUnsat :: SimpleContext -> IO ()
setUnsat SimpleContext
sc = do
forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ do
Maybe (Model, Integer)
sol <- forall a. Context a => a -> STM (Maybe (Model, Integer))
getBestSolution SimpleContext
sc
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Maybe a -> Bool
isNothing Maybe (Model, Integer)
sol) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error String
"setUnsat: already has a solution"
forall a. TVar a -> a -> STM ()
writeTVar (SimpleContext -> TVar Bool
scUnsatRef SimpleContext
sc) Bool
True
addSolution :: SimpleContext -> Model -> IO ()
addSolution SimpleContext
sc Model
m = do
let !val :: Integer
val = forall a. Context a => a -> Model -> Integer
evalObjectiveFunction SimpleContext
sc Model
m
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ do
Bool
unsat <- forall a. Context a => a -> STM Bool
isUnsat SimpleContext
sc
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
unsat forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error String
"addSolution: already marked as unsatisfiable"
Maybe Integer
sol0 <- forall a. Context a => a -> STM (Maybe Integer)
getBestValue SimpleContext
sc
case Maybe Integer
sol0 of
Just Integer
val0 | Integer
val0 forall a. Ord a => a -> a -> Bool
<= Integer
val -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe Integer
_ -> do
forall a. TVar a -> a -> STM ()
writeTVar (SimpleContext -> TVar (Maybe (Model, Integer))
scBestSolutionRef SimpleContext
sc) (forall a. a -> Maybe a
Just (Model
m, Integer
val))
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
Model -> Integer -> IO ()
h <- forall a. IORef a -> IO a
readIORef (SimpleContext -> IORef (Model -> Integer -> IO ())
scOnUpdateBestSolutionRef SimpleContext
sc)
Model -> Integer -> IO ()
h Model
m Integer
val
addLowerBound :: SimpleContext -> Integer -> IO ()
addLowerBound SimpleContext
sc Integer
lb = do
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ do
Integer
lb0 <- forall a. Context a => a -> STM Integer
getLowerBound SimpleContext
sc
if Integer
lb forall a. Ord a => a -> a -> Bool
<= Integer
lb0 then
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
else do
forall a. TVar a -> a -> STM ()
writeTVar (SimpleContext -> TVar Integer
scLowerBoundRef SimpleContext
sc) Integer
lb
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
Integer -> IO ()
h <- forall a. IORef a -> IO a
readIORef (SimpleContext -> IORef (Integer -> IO ())
scOnUpdateLowerBoundRef SimpleContext
sc)
Integer -> IO ()
h Integer
lb
logMessage :: SimpleContext -> String -> IO ()
logMessage SimpleContext
sc String
msg = do
String -> IO ()
h <- forall a. IORef a -> IO a
readIORef (SimpleContext -> IORef (String -> IO ())
scLoggerRef SimpleContext
sc)
String -> IO ()
h String
msg
newSimpleContext :: SAT.PBLinSum -> IO SimpleContext
newSimpleContext :: PBLinSum -> IO SimpleContext
newSimpleContext PBLinSum
obj = PBLinSum -> (Model -> Integer) -> IO SimpleContext
newSimpleContext2 PBLinSum
obj (\Model
m -> forall m. IModel m => m -> PBLinSum -> Integer
SAT.evalPBLinSum Model
m PBLinSum
obj)
newSimpleContext2 :: SAT.PBLinSum -> (SAT.Model -> Integer) -> IO SimpleContext
newSimpleContext2 :: PBLinSum -> (Model -> Integer) -> IO SimpleContext
newSimpleContext2 PBLinSum
obj Model -> Integer
obj2 = do
TVar Bool
unsatRef <- forall a. a -> IO (TVar a)
newTVarIO Bool
False
TVar (Maybe (Model, Integer))
bestsolRef <- forall a. a -> IO (TVar a)
newTVarIO forall a. Maybe a
Nothing
TVar Integer
lbRef <- forall a. a -> IO (TVar a)
newTVarIO forall a b. (a -> b) -> a -> b
$! PBLinSum -> Integer
SAT.pbLinLowerBound PBLinSum
obj
IORef (Model -> Integer -> IO ())
onUpdateBestSolRef <- forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ \Model
_ Integer
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
IORef (Integer -> IO ())
onUpdateLBRef <- forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ \Integer
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
IORef (String -> IO ())
loggerRef <- forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ \String
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
SimpleContext
{ scGetObjectiveFunction :: PBLinSum
scGetObjectiveFunction = PBLinSum
obj
, scEvalObjectiveFunction :: Model -> Integer
scEvalObjectiveFunction = Model -> Integer
obj2
, scUnsatRef :: TVar Bool
scUnsatRef = TVar Bool
unsatRef
, scBestSolutionRef :: TVar (Maybe (Model, Integer))
scBestSolutionRef = TVar (Maybe (Model, Integer))
bestsolRef
, scLowerBoundRef :: TVar Integer
scLowerBoundRef = TVar Integer
lbRef
, scOnUpdateBestSolutionRef :: IORef (Model -> Integer -> IO ())
scOnUpdateBestSolutionRef = IORef (Model -> Integer -> IO ())
onUpdateBestSolRef
, scOnUpdateLowerBoundRef :: IORef (Integer -> IO ())
scOnUpdateLowerBoundRef = IORef (Integer -> IO ())
onUpdateLBRef
, scLoggerRef :: IORef (String -> IO ())
scLoggerRef = IORef (String -> IO ())
loggerRef
}
setOnUpdateBestSolution :: SimpleContext -> (SAT.Model -> Integer -> IO ()) -> IO ()
setOnUpdateBestSolution :: SimpleContext -> (Model -> Integer -> IO ()) -> IO ()
setOnUpdateBestSolution SimpleContext
sc Model -> Integer -> IO ()
h = forall a. IORef a -> a -> IO ()
writeIORef (SimpleContext -> IORef (Model -> Integer -> IO ())
scOnUpdateBestSolutionRef SimpleContext
sc) Model -> Integer -> IO ()
h
setOnUpdateLowerBound :: SimpleContext -> (Integer -> IO ()) -> IO ()
setOnUpdateLowerBound :: SimpleContext -> (Integer -> IO ()) -> IO ()
setOnUpdateLowerBound SimpleContext
sc Integer -> IO ()
h = forall a. IORef a -> a -> IO ()
writeIORef (SimpleContext -> IORef (Integer -> IO ())
scOnUpdateLowerBoundRef SimpleContext
sc) Integer -> IO ()
h
setLogger :: SimpleContext -> (String -> IO ()) -> IO ()
setLogger :: SimpleContext -> (String -> IO ()) -> IO ()
setLogger SimpleContext
sc String -> IO ()
h = forall a. IORef a -> a -> IO ()
writeIORef (SimpleContext -> IORef (String -> IO ())
scLoggerRef SimpleContext
sc) String -> IO ()
h
data Normalized a
= Normalized
{ forall a. Normalized a -> a
nBase :: a
, forall a. Normalized a -> PBLinSum
nObjectiveFunction :: SAT.PBLinSum
, forall a. Normalized a -> Integer
nOffset :: Integer
}
instance Context a => Context (Normalized a) where
getObjectiveFunction :: Normalized a -> PBLinSum
getObjectiveFunction = forall a. Normalized a -> PBLinSum
nObjectiveFunction
evalObjectiveFunction :: Normalized a -> Model -> Integer
evalObjectiveFunction Normalized a
cxt Model
m = forall a. Context a => a -> Model -> Integer
evalObjectiveFunction (forall a. Normalized a -> a
nBase Normalized a
cxt) Model
m forall a. Num a => a -> a -> a
- forall a. Normalized a -> Integer
nOffset Normalized a
cxt
isUnsat :: Normalized a -> STM Bool
isUnsat Normalized a
cxt = forall a. Context a => a -> STM Bool
isUnsat (forall a. Normalized a -> a
nBase Normalized a
cxt)
getBestSolution :: Normalized a -> STM (Maybe (Model, Integer))
getBestSolution Normalized a
cxt = do
Maybe (Model, Integer)
sol <- forall a. Context a => a -> STM (Maybe (Model, Integer))
getBestSolution (forall a. Normalized a -> a
nBase Normalized a
cxt)
case Maybe (Model, Integer)
sol of
Maybe (Model, Integer)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Just (Model
m, Integer
val) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Model
m, Integer
val forall a. Num a => a -> a -> a
- forall a. Normalized a -> Integer
nOffset Normalized a
cxt)
getLowerBound :: Normalized a -> STM Integer
getLowerBound Normalized a
cxt = do
Integer
lb <- forall a. Context a => a -> STM Integer
getLowerBound (forall a. Normalized a -> a
nBase Normalized a
cxt)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Integer
lb forall a. Num a => a -> a -> a
- forall a. Normalized a -> Integer
nOffset Normalized a
cxt
setUnsat :: Normalized a -> IO ()
setUnsat Normalized a
cxt = forall a. Context a => a -> IO ()
setUnsat forall a b. (a -> b) -> a -> b
$ forall a. Normalized a -> a
nBase Normalized a
cxt
addSolution :: Normalized a -> Model -> IO ()
addSolution Normalized a
cxt Model
m = do
forall a. Context a => a -> Model -> IO ()
addSolution (forall a. Normalized a -> a
nBase Normalized a
cxt) Model
m
addLowerBound :: Normalized a -> Integer -> IO ()
addLowerBound Normalized a
cxt Integer
lb = do
forall a. Context a => a -> Integer -> IO ()
addLowerBound (forall a. Normalized a -> a
nBase Normalized a
cxt) (Integer
lb forall a. Num a => a -> a -> a
+ forall a. Normalized a -> Integer
nOffset Normalized a
cxt)
logMessage :: Normalized a -> String -> IO ()
logMessage Normalized a
cxt String
msg = forall a. Context a => a -> String -> IO ()
logMessage (forall a. Normalized a -> a
nBase Normalized a
cxt) String
msg
normalize :: Context a => a -> Normalized a
normalize :: forall a. Context a => a -> Normalized a
normalize a
cxt = forall a. a -> PBLinSum -> Integer -> Normalized a
Normalized a
cxt PBLinSum
obj' Integer
offset
where
obj :: PBLinSum
obj = forall a. Context a => a -> PBLinSum
getObjectiveFunction a
cxt
(PBLinSum
obj',Integer
offset) = (PBLinSum, Integer) -> (PBLinSum, Integer)
SAT.normalizePBLinSum (PBLinSum
obj, Integer
0)