{-# LANGUAGE BangPatterns #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.PBO.Context
-- Copyright   :  (c) Masahiro Sakai 2014
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
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

{--------------------------------------------------------------------
  Context class
--------------------------------------------------------------------}

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 = Model -> PBLinSum -> Integer
forall m. IModel m => m -> PBLinSum -> Integer
SAT.evalPBLinSum Model
m (a -> PBLinSum
forall a. Context a => a -> PBLinSum
getObjectiveFunction a
c)

getBestValue :: Context a => a -> STM (Maybe Integer)
getBestValue :: a -> STM (Maybe Integer)
getBestValue a
cxt = (Maybe (Model, Integer) -> Maybe Integer)
-> STM (Maybe (Model, Integer)) -> STM (Maybe Integer)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (((Model, Integer) -> Integer)
-> Maybe (Model, Integer) -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Model, Integer) -> Integer
forall a b. (a, b) -> b
snd) (STM (Maybe (Model, Integer)) -> STM (Maybe Integer))
-> STM (Maybe (Model, Integer)) -> STM (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ a -> STM (Maybe (Model, Integer))
forall a. Context a => a -> STM (Maybe (Model, Integer))
getBestSolution a
cxt

getBestModel :: Context a => a -> STM (Maybe SAT.Model)
getBestModel :: a -> STM (Maybe Model)
getBestModel a
cxt = (Maybe (Model, Integer) -> Maybe Model)
-> STM (Maybe (Model, Integer)) -> STM (Maybe Model)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (((Model, Integer) -> Model)
-> Maybe (Model, Integer) -> Maybe Model
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Model, Integer) -> Model
forall a b. (a, b) -> a
fst) (STM (Maybe (Model, Integer)) -> STM (Maybe Model))
-> STM (Maybe (Model, Integer)) -> STM (Maybe Model)
forall a b. (a -> b) -> a -> b
$ a -> STM (Maybe (Model, Integer))
forall a. Context a => a -> STM (Maybe (Model, Integer))
getBestSolution a
cxt

isOptimum :: Context a => a -> STM Bool
isOptimum :: a -> STM Bool
isOptimum a
cxt = do
  Maybe Integer
ub <- a -> STM (Maybe Integer)
forall a. Context a => a -> STM (Maybe Integer)
getBestValue a
cxt
  Integer
lb <- a -> STM Integer
forall a. Context a => a -> STM Integer
getLowerBound a
cxt
  case Maybe Integer
ub of
    Maybe Integer
Nothing -> Bool -> STM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Just Integer
val -> Bool -> STM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> STM Bool) -> Bool -> STM Bool
forall a b. (a -> b) -> a -> b
$ Integer
val Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
lb
    -- Note that solving with the assumption 'obj < val' can yield
    -- a lower bound that is higher than val!

isFinished :: Context a => a -> STM Bool
isFinished :: a -> STM Bool
isFinished a
cxt = do
  Bool
b1 <- a -> STM Bool
forall a. Context a => a -> STM Bool
isUnsat a
cxt
  Bool
b2 <- a -> STM Bool
forall a. Context a => a -> STM Bool
isOptimum a
cxt
  Bool -> STM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> STM Bool) -> Bool -> STM Bool
forall a b. (a -> b) -> a -> b
$ Bool
b1 Bool -> Bool -> Bool
|| Bool
b2

getSearchUpperBound :: Context a => a -> STM Integer
getSearchUpperBound :: a -> STM Integer
getSearchUpperBound a
ctx = do
  Maybe Integer
ret <- a -> STM (Maybe Integer)
forall a. Context a => a -> STM (Maybe Integer)
getBestValue a
ctx
  case Maybe Integer
ret of
    Just Integer
val -> Integer -> STM Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> STM Integer) -> Integer -> STM Integer
forall a b. (a -> b) -> a -> b
$ Integer
val Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
    Maybe Integer
Nothing -> Integer -> STM Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> STM Integer) -> Integer -> STM Integer
forall a b. (a -> b) -> a -> b
$ PBLinSum -> Integer
SAT.pbLinUpperBound (PBLinSum -> Integer) -> PBLinSum -> Integer
forall a b. (a -> b) -> a -> b
$ a -> PBLinSum
forall a. Context a => a -> PBLinSum
getObjectiveFunction a
ctx

setFinished :: Context a => a -> IO ()
setFinished :: a -> IO ()
setFinished a
cxt = do
  IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (IO ()) -> IO ()) -> IO (IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ STM (IO ()) -> IO (IO ())
forall a. STM a -> IO a
atomically (STM (IO ()) -> IO (IO ())) -> STM (IO ()) -> IO (IO ())
forall a b. (a -> b) -> a -> b
$ do
    Maybe Integer
ret <- a -> STM (Maybe Integer)
forall a. Context a => a -> STM (Maybe Integer)
getBestValue a
cxt
    case Maybe Integer
ret of
      Just Integer
val -> IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ a -> Integer -> IO ()
forall a. Context a => a -> Integer -> IO ()
addLowerBound a
cxt Integer
val
      Maybe Integer
Nothing -> IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ a -> IO ()
forall a. Context a => a -> IO ()
setUnsat a
cxt

{--------------------------------------------------------------------
  Simple Context
--------------------------------------------------------------------}

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 = TVar Bool -> STM Bool
forall a. TVar a -> STM a
readTVar (SimpleContext -> TVar Bool
scUnsatRef SimpleContext
sc)
  getBestSolution :: SimpleContext -> STM (Maybe (Model, Integer))
getBestSolution SimpleContext
sc = TVar (Maybe (Model, Integer)) -> STM (Maybe (Model, Integer))
forall a. TVar a -> STM a
readTVar (SimpleContext -> TVar (Maybe (Model, Integer))
scBestSolutionRef SimpleContext
sc)
  getLowerBound :: SimpleContext -> STM Integer
getLowerBound SimpleContext
sc = TVar Integer -> STM Integer
forall a. TVar a -> STM a
readTVar (SimpleContext -> TVar Integer
scLowerBoundRef SimpleContext
sc)

  setUnsat :: SimpleContext -> IO ()
setUnsat SimpleContext
sc = do
    STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      Maybe (Model, Integer)
sol <- SimpleContext -> STM (Maybe (Model, Integer))
forall a. Context a => a -> STM (Maybe (Model, Integer))
getBestSolution SimpleContext
sc
      Bool -> STM () -> STM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Maybe (Model, Integer) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (Model, Integer)
sol) (STM () -> STM ()) -> STM () -> STM ()
forall a b. (a -> b) -> a -> b
$ String -> STM ()
forall a. HasCallStack => String -> a
error String
"setUnsat: already has a solution" -- FIXME: use throwSTM?
      TVar Bool -> Bool -> STM ()
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 = SimpleContext -> Model -> Integer
forall a. Context a => a -> Model -> Integer
evalObjectiveFunction SimpleContext
sc Model
m
    IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (IO ()) -> IO ()) -> IO (IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ STM (IO ()) -> IO (IO ())
forall a. STM a -> IO a
atomically (STM (IO ()) -> IO (IO ())) -> STM (IO ()) -> IO (IO ())
forall a b. (a -> b) -> a -> b
$ do
      Bool
unsat <- SimpleContext -> STM Bool
forall a. Context a => a -> STM Bool
isUnsat SimpleContext
sc
      Bool -> STM () -> STM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
unsat (STM () -> STM ()) -> STM () -> STM ()
forall a b. (a -> b) -> a -> b
$ String -> STM ()
forall a. HasCallStack => String -> a
error String
"addSolution: already marked as unsatisfiable" -- FIXME: use throwSTM?

      Maybe Integer
sol0 <- SimpleContext -> STM (Maybe Integer)
forall a. Context a => a -> STM (Maybe Integer)
getBestValue SimpleContext
sc
      case Maybe Integer
sol0 of
        Just Integer
val0 | Integer
val0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
val -> IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Maybe Integer
_ -> do
          TVar (Maybe (Model, Integer)) -> Maybe (Model, Integer) -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar (SimpleContext -> TVar (Maybe (Model, Integer))
scBestSolutionRef SimpleContext
sc) ((Model, Integer) -> Maybe (Model, Integer)
forall a. a -> Maybe a
Just (Model
m, Integer
val))
          IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ do
            Model -> Integer -> IO ()
h <- IORef (Model -> Integer -> IO ()) -> IO (Model -> Integer -> IO ())
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
    IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (IO ()) -> IO ()) -> IO (IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ STM (IO ()) -> IO (IO ())
forall a. STM a -> IO a
atomically (STM (IO ()) -> IO (IO ())) -> STM (IO ()) -> IO (IO ())
forall a b. (a -> b) -> a -> b
$ do
      Integer
lb0 <- SimpleContext -> STM Integer
forall a. Context a => a -> STM Integer
getLowerBound SimpleContext
sc
      if Integer
lb Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
lb0 then
        IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      else do
        TVar Integer -> Integer -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar (SimpleContext -> TVar Integer
scLowerBoundRef SimpleContext
sc) Integer
lb
        IO () -> STM (IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ do
          Integer -> IO ()
h <- IORef (Integer -> IO ()) -> IO (Integer -> IO ())
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 <- IORef (String -> IO ()) -> IO (String -> IO ())
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 -> Model -> PBLinSum -> Integer
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 <- Bool -> IO (TVar Bool)
forall a. a -> IO (TVar a)
newTVarIO Bool
False
  TVar (Maybe (Model, Integer))
bestsolRef <- Maybe (Model, Integer) -> IO (TVar (Maybe (Model, Integer)))
forall a. a -> IO (TVar a)
newTVarIO Maybe (Model, Integer)
forall a. Maybe a
Nothing
  TVar Integer
lbRef <- Integer -> IO (TVar Integer)
forall a. a -> IO (TVar a)
newTVarIO (Integer -> IO (TVar Integer)) -> Integer -> IO (TVar Integer)
forall a b. (a -> b) -> a -> b
$! PBLinSum -> Integer
SAT.pbLinLowerBound PBLinSum
obj

  IORef (Model -> Integer -> IO ())
onUpdateBestSolRef <- (Model -> Integer -> IO ())
-> IO (IORef (Model -> Integer -> IO ()))
forall a. a -> IO (IORef a)
newIORef ((Model -> Integer -> IO ())
 -> IO (IORef (Model -> Integer -> IO ())))
-> (Model -> Integer -> IO ())
-> IO (IORef (Model -> Integer -> IO ()))
forall a b. (a -> b) -> a -> b
$ \Model
_ Integer
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  IORef (Integer -> IO ())
onUpdateLBRef <- (Integer -> IO ()) -> IO (IORef (Integer -> IO ()))
forall a. a -> IO (IORef a)
newIORef ((Integer -> IO ()) -> IO (IORef (Integer -> IO ())))
-> (Integer -> IO ()) -> IO (IORef (Integer -> IO ()))
forall a b. (a -> b) -> a -> b
$ \Integer
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  IORef (String -> IO ())
loggerRef <- (String -> IO ()) -> IO (IORef (String -> IO ()))
forall a. a -> IO (IORef a)
newIORef ((String -> IO ()) -> IO (IORef (String -> IO ())))
-> (String -> IO ()) -> IO (IORef (String -> IO ()))
forall a b. (a -> b) -> a -> b
$ \String
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  SimpleContext -> IO SimpleContext
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpleContext -> IO SimpleContext)
-> SimpleContext -> IO SimpleContext
forall a b. (a -> b) -> a -> b
$
    SimpleContext :: PBLinSum
-> (Model -> Integer)
-> TVar Bool
-> TVar (Maybe (Model, Integer))
-> TVar Integer
-> IORef (Model -> Integer -> IO ())
-> IORef (Integer -> IO ())
-> IORef (String -> IO ())
-> SimpleContext
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 = IORef (Model -> Integer -> IO ())
-> (Model -> Integer -> IO ()) -> IO ()
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 = IORef (Integer -> IO ()) -> (Integer -> IO ()) -> IO ()
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 = IORef (String -> IO ()) -> (String -> IO ()) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (SimpleContext -> IORef (String -> IO ())
scLoggerRef SimpleContext
sc) String -> IO ()
h

{--------------------------------------------------------------------
  Normalization
--------------------------------------------------------------------}

data Normalized a
  = Normalized
  { Normalized a -> a
nBase :: a
  , Normalized a -> PBLinSum
nObjectiveFunction :: SAT.PBLinSum
  , Normalized a -> Integer
nOffset :: Integer
  }

instance Context a => Context (Normalized a) where
  getObjectiveFunction :: Normalized a -> PBLinSum
getObjectiveFunction = Normalized a -> PBLinSum
forall a. Normalized a -> PBLinSum
nObjectiveFunction

  evalObjectiveFunction :: Normalized a -> Model -> Integer
evalObjectiveFunction Normalized a
cxt Model
m = a -> Model -> Integer
forall a. Context a => a -> Model -> Integer
evalObjectiveFunction (Normalized a -> a
forall a. Normalized a -> a
nBase Normalized a
cxt) Model
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Normalized a -> Integer
forall a. Normalized a -> Integer
nOffset Normalized a
cxt

  isUnsat :: Normalized a -> STM Bool
isUnsat Normalized a
cxt = a -> STM Bool
forall a. Context a => a -> STM Bool
isUnsat (Normalized a -> a
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 <- a -> STM (Maybe (Model, Integer))
forall a. Context a => a -> STM (Maybe (Model, Integer))
getBestSolution (Normalized a -> a
forall a. Normalized a -> a
nBase Normalized a
cxt)
    case Maybe (Model, Integer)
sol of
      Maybe (Model, Integer)
Nothing -> Maybe (Model, Integer) -> STM (Maybe (Model, Integer))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Model, Integer)
forall a. Maybe a
Nothing
      Just (Model
m, Integer
val) -> Maybe (Model, Integer) -> STM (Maybe (Model, Integer))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Model, Integer) -> STM (Maybe (Model, Integer)))
-> Maybe (Model, Integer) -> STM (Maybe (Model, Integer))
forall a b. (a -> b) -> a -> b
$ (Model, Integer) -> Maybe (Model, Integer)
forall a. a -> Maybe a
Just (Model
m, Integer
val Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Normalized a -> Integer
forall a. Normalized a -> Integer
nOffset Normalized a
cxt)

  getLowerBound :: Normalized a -> STM Integer
getLowerBound Normalized a
cxt = do
    Integer
lb <- a -> STM Integer
forall a. Context a => a -> STM Integer
getLowerBound (Normalized a -> a
forall a. Normalized a -> a
nBase Normalized a
cxt)
    Integer -> STM Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> STM Integer) -> Integer -> STM Integer
forall a b. (a -> b) -> a -> b
$ Integer
lb Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Normalized a -> Integer
forall a. Normalized a -> Integer
nOffset Normalized a
cxt

  setUnsat :: Normalized a -> IO ()
setUnsat Normalized a
cxt = a -> IO ()
forall a. Context a => a -> IO ()
setUnsat (a -> IO ()) -> a -> IO ()
forall a b. (a -> b) -> a -> b
$ Normalized a -> a
forall a. Normalized a -> a
nBase Normalized a
cxt

  addSolution :: Normalized a -> Model -> IO ()
addSolution Normalized a
cxt Model
m = do
    a -> Model -> IO ()
forall a. Context a => a -> Model -> IO ()
addSolution (Normalized a -> a
forall a. Normalized a -> a
nBase Normalized a
cxt) Model
m

  addLowerBound :: Normalized a -> Integer -> IO ()
addLowerBound Normalized a
cxt Integer
lb = do
    a -> Integer -> IO ()
forall a. Context a => a -> Integer -> IO ()
addLowerBound (Normalized a -> a
forall a. Normalized a -> a
nBase Normalized a
cxt) (Integer
lb Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Normalized a -> Integer
forall a. Normalized a -> Integer
nOffset Normalized a
cxt)

  logMessage :: Normalized a -> String -> IO ()
logMessage Normalized a
cxt String
msg = a -> String -> IO ()
forall a. Context a => a -> String -> IO ()
logMessage (Normalized a -> a
forall a. Normalized a -> a
nBase Normalized a
cxt) String
msg

normalize :: Context a => a -> Normalized a
normalize :: a -> Normalized a
normalize a
cxt = a -> PBLinSum -> Integer -> Normalized a
forall a. a -> PBLinSum -> Integer -> Normalized a
Normalized a
cxt PBLinSum
obj' Integer
offset
  where
    obj :: PBLinSum
obj = a -> PBLinSum
forall a. Context a => a -> PBLinSum
getObjectiveFunction a
cxt
    (PBLinSum
obj',Integer
offset) = (PBLinSum, Integer) -> (PBLinSum, Integer)
SAT.normalizePBLinSum (PBLinSum
obj, Integer
0)