{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module ToySolver.Arith.MIP
(
Solver
, newSolver
, optimize
, getBestSolution
, getBestValue
, getBestModel
, setNThread
, setLogger
, setOnUpdateBestSolution
, setShowRational
) where
import Prelude hiding (log)
import Control.Monad
import Control.Exception
import Control.Concurrent
import Control.Concurrent.STM
import Data.Default.Class
import Data.List
import Data.OptDir
import Data.Ord
import Data.IORef
import Data.Maybe
import qualified Data.IntSet as IS
import qualified Data.IntMap as IM
import qualified Data.Map as Map
import qualified Data.Sequence as Seq
import qualified Data.Foldable as F
import Data.VectorSpace
import System.Clock
import System.Timeout
import Text.Printf
import qualified ToySolver.Data.LA as LA
import ToySolver.Data.OrdRel ((.<=.), (.>=.))
import qualified ToySolver.Arith.Simplex as Simplex
import ToySolver.Arith.Simplex (OptResult (..), Var, Model)
import ToySolver.Internal.Util (isInteger, fracPart)
data Solver
= MIP
{ Solver -> Solver
mipRootLP :: Simplex.Solver
, Solver -> IntSet
mipIVs :: IS.IntSet
, Solver -> TVar (Maybe Node)
mipBest :: TVar (Maybe Node)
, Solver -> IORef Int
mipNThread :: IORef Int
, Solver -> IORef (Maybe (String -> IO ()))
mipLogger :: IORef (Maybe (String -> IO ()))
, Solver -> IORef (Model -> Rational -> IO ())
mipOnUpdateBestSolution :: IORef (Model -> Rational -> IO ())
, Solver -> IORef Bool
mipShowRational :: IORef Bool
}
data Node =
Node
{ Node -> Solver
ndLP :: Simplex.Solver
, Node -> Int
ndDepth :: {-# UNPACK #-} !Int
, Node -> Rational
ndValue :: Rational
}
newSolver :: Simplex.Solver -> IS.IntSet -> IO Solver
newSolver :: Solver -> IntSet -> IO Solver
newSolver Solver
lp IntSet
ivs = do
Solver
lp2 <- Solver -> IO Solver
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m (GenericSolverM m v)
Simplex.cloneSolver Solver
lp
[Int] -> (Int -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [Int]
IS.toList IntSet
ivs) ((Int -> IO ()) -> IO ()) -> (Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Int
v -> do
Bound Rational
lb <- Solver -> Int -> IO (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
Simplex.getLB Solver
lp2 Int
v
case Bound Rational
lb of
Just (Rational
l,IntSet
_) | Bool -> Bool
not (Rational -> Bool
forall a. RealFrac a => a -> Bool
isInteger Rational
l) ->
Solver -> Int -> Rational -> IO ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> m ()
Simplex.assertLower Solver
lp2 Int
v (Integer -> Rational
forall a. Num a => Integer -> a
fromInteger (Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
l))
Bound Rational
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Bound Rational
ub <- Solver -> Int -> IO (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
Simplex.getUB Solver
lp2 Int
v
case Bound Rational
ub of
Just (Rational
u,IntSet
_) | Bool -> Bool
not (Rational -> Bool
forall a. RealFrac a => a -> Bool
isInteger Rational
u) ->
Solver -> Int -> Rational -> IO ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> m ()
Simplex.assertLower Solver
lp2 Int
v (Integer -> Rational
forall a. Num a => Integer -> a
fromInteger (Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
u))
Bound Rational
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
TVar (Maybe Node)
bestRef <- Maybe Node -> IO (TVar (Maybe Node))
forall a. a -> IO (TVar a)
newTVarIO Maybe Node
forall a. Maybe a
Nothing
IORef Int
nthreadRef <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
IORef (Maybe (String -> IO ()))
logRef <- Maybe (String -> IO ()) -> IO (IORef (Maybe (String -> IO ())))
forall a. a -> IO (IORef a)
newIORef Maybe (String -> IO ())
forall a. Maybe a
Nothing
IORef Bool
showRef <- Bool -> IO (IORef Bool)
forall a. a -> IO (IORef a)
newIORef Bool
False
IORef (Model -> Rational -> IO ())
updateRef <- (Model -> Rational -> IO ())
-> IO (IORef (Model -> Rational -> IO ()))
forall a. a -> IO (IORef a)
newIORef (\Model
_ Rational
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
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
$
MIP
{ mipRootLP :: Solver
mipRootLP = Solver
lp2
, mipIVs :: IntSet
mipIVs = IntSet
ivs
, mipBest :: TVar (Maybe Node)
mipBest = TVar (Maybe Node)
bestRef
, mipNThread :: IORef Int
mipNThread = IORef Int
nthreadRef
, mipLogger :: IORef (Maybe (String -> IO ()))
mipLogger = IORef (Maybe (String -> IO ()))
logRef
, mipOnUpdateBestSolution :: IORef (Model -> Rational -> IO ())
mipOnUpdateBestSolution = IORef (Model -> Rational -> IO ())
updateRef
, mipShowRational :: IORef Bool
mipShowRational = IORef Bool
showRef
}
optimize :: Solver -> IO OptResult
optimize :: Solver -> IO OptResult
optimize Solver
solver = do
let lp :: Solver
lp = Solver -> Solver
mipRootLP Solver
solver
Model -> Rational -> IO ()
update <- IORef (Model -> Rational -> IO ())
-> IO (Model -> Rational -> IO ())
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Model -> Rational -> IO ())
mipOnUpdateBestSolution Solver
solver)
Solver -> String -> IO ()
log Solver
solver String
"MIP: Solving LP relaxation..."
Bool
ret <- Solver -> IO Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
Simplex.check Solver
lp
if Bool -> Bool
not Bool
ret
then OptResult -> IO OptResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unsat
else do
String
s0 <- Solver -> Rational -> IO String
showValue Solver
solver (Rational -> IO String) -> IO Rational -> IO String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Rational
forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m v
Simplex.getObjValue Solver
lp
Solver -> String -> IO ()
log Solver
solver (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"MIP: LP relaxation is satisfiable with obj = %s" String
s0)
Solver -> String -> IO ()
log Solver
solver String
"MIP: Optimizing LP relaxation"
OptResult
ret2 <- Solver -> Options -> IO OptResult
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Options -> m OptResult
Simplex.optimize Solver
lp Options
forall a. Default a => a
def
case OptResult
ret2 of
OptResult
Unsat -> String -> IO OptResult
forall a. (?callStack::CallStack) => String -> a
error String
"should not happen"
OptResult
ObjLimit -> String -> IO OptResult
forall a. (?callStack::CallStack) => String -> a
error String
"should not happen"
OptResult
Unbounded -> do
Solver -> String -> IO ()
log Solver
solver String
"MIP: LP relaxation is unbounded"
let ivs :: IntSet
ivs = Solver -> IntSet
mipIVs Solver
solver
if IntSet -> Bool
IS.null IntSet
ivs
then OptResult -> IO OptResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unbounded
else do
Expr Rational
origObj <- Solver -> IO (Expr Rational)
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m (Expr Rational)
Simplex.getObj Solver
lp
Solver
lp2 <- Solver -> IO Solver
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m (GenericSolverM m v)
Simplex.cloneSolver Solver
lp
Solver -> IO ()
forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m ()
Simplex.clearLogger Solver
lp2
Solver -> Expr Rational -> IO ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Expr Rational -> m ()
Simplex.setObj Solver
lp2 (Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
0)
Solver -> Solver -> (Model -> Rational -> IO ()) -> IO ()
branchAndBound Solver
solver Solver
lp2 ((Model -> Rational -> IO ()) -> IO ())
-> (Model -> Rational -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Model
m Rational
_ -> do
Model -> Rational -> IO ()
update Model
m (Model -> Expr Rational -> Rational
forall m e v. Eval m e v => m -> e -> v
LA.eval Model
m Expr Rational
origObj)
Maybe Node
best <- TVar (Maybe Node) -> IO (Maybe Node)
forall a. TVar a -> IO a
readTVarIO (Solver -> TVar (Maybe Node)
mipBest Solver
solver)
case Maybe Node
best of
Just Node
nd -> do
Model
m <- Solver -> IO Model
forall v (m :: * -> *).
(SolverValue v, PrimMonad m) =>
GenericSolverM m v -> m Model
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> m Model
Simplex.getModel (Node -> Solver
ndLP Node
nd)
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TVar (Maybe Node) -> Maybe Node -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar (Solver -> TVar (Maybe Node)
mipBest Solver
solver) (Maybe Node -> STM ()) -> Maybe Node -> STM ()
forall a b. (a -> b) -> a -> b
$ Node -> Maybe Node
forall a. a -> Maybe a
Just Node
nd{ ndValue = LA.eval m origObj }
OptResult -> IO OptResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unbounded
Maybe Node
Nothing -> OptResult -> IO OptResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unsat
OptResult
Optimum -> do
String
s1 <- Solver -> Rational -> IO String
showValue Solver
solver (Rational -> IO String) -> IO Rational -> IO String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Rational
forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m v
Simplex.getObjValue Solver
lp
Solver -> String -> IO ()
log Solver
solver (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"MIP: LP relaxation optimum is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s1
Solver -> String -> IO ()
log Solver
solver String
"MIP: Integer optimization begins..."
Solver -> IO ()
forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m ()
Simplex.clearLogger Solver
lp
Solver -> Solver -> (Model -> Rational -> IO ()) -> IO ()
branchAndBound Solver
solver Solver
lp Model -> Rational -> IO ()
update
Maybe Node
m <- TVar (Maybe Node) -> IO (Maybe Node)
forall a. TVar a -> IO a
readTVarIO (Solver -> TVar (Maybe Node)
mipBest Solver
solver)
case Maybe Node
m of
Maybe Node
Nothing -> OptResult -> IO OptResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unsat
Just Node
_ -> OptResult -> IO OptResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Optimum
branchAndBound :: Solver -> Simplex.Solver -> (Model -> Rational -> IO ()) -> IO ()
branchAndBound :: Solver -> Solver -> (Model -> Rational -> IO ()) -> IO ()
branchAndBound Solver
solver Solver
rootLP Model -> Rational -> IO ()
update = do
OptDir
dir <- Solver -> IO OptDir
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m OptDir
Simplex.getOptDir Solver
rootLP
Rational
rootVal <- Solver -> IO Rational
forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m v
Simplex.getObjValue Solver
rootLP
let root :: Node
root = Node{ ndLP :: Solver
ndLP = Solver
rootLP, ndDepth :: Int
ndDepth = Int
0, ndValue :: Rational
ndValue = Rational
rootVal }
TVar (Seq Node)
pool <- Seq Node -> IO (TVar (Seq Node))
forall a. a -> IO (TVar a)
newTVarIO (Node -> Seq Node
forall a. a -> Seq a
Seq.singleton Node
root)
TVar (Map ThreadId Node)
activeThreads <- Map ThreadId Node -> IO (TVar (Map ThreadId Node))
forall a. a -> IO (TVar a)
newTVarIO (Map ThreadId Node
forall k a. Map k a
Map.empty)
TVar Int
visitedNodes <- Int -> IO (TVar Int)
forall a. a -> IO (TVar a)
newTVarIO Int
0
TChan Node
solchan <- IO (TChan Node)
forall a. IO (TChan a)
newTChanIO
let addNode :: Node -> STM ()
addNode :: Node -> STM ()
addNode Node
nd = do
TVar (Seq Node) -> (Seq Node -> Seq Node) -> STM ()
forall a. TVar a -> (a -> a) -> STM ()
modifyTVar TVar (Seq Node)
pool (Seq Node -> Node -> Seq Node
forall a. Seq a -> a -> Seq a
Seq.|> Node
nd)
pickNode :: IO (Maybe Node)
pickNode :: IO (Maybe Node)
pickNode = do
ThreadId
self <- IO ThreadId
myThreadId
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TVar (Map ThreadId Node)
-> (Map ThreadId Node -> Map ThreadId Node) -> STM ()
forall a. TVar a -> (a -> a) -> STM ()
modifyTVar TVar (Map ThreadId Node)
activeThreads (ThreadId -> Map ThreadId Node -> Map ThreadId Node
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete ThreadId
self)
STM (Maybe Node) -> IO (Maybe Node)
forall a. STM a -> IO a
atomically (STM (Maybe Node) -> IO (Maybe Node))
-> STM (Maybe Node) -> IO (Maybe Node)
forall a b. (a -> b) -> a -> b
$ do
Seq Node
s <- TVar (Seq Node) -> STM (Seq Node)
forall a. TVar a -> STM a
readTVar TVar (Seq Node)
pool
case Seq Node -> ViewL Node
forall a. Seq a -> ViewL a
Seq.viewl Seq Node
s of
Node
nd Seq.:< Seq Node
s2 -> do
TVar (Seq Node) -> Seq Node -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar TVar (Seq Node)
pool Seq Node
s2
TVar (Map ThreadId Node)
-> (Map ThreadId Node -> Map ThreadId Node) -> STM ()
forall a. TVar a -> (a -> a) -> STM ()
modifyTVar TVar (Map ThreadId Node)
activeThreads (ThreadId -> Node -> Map ThreadId Node -> Map ThreadId Node
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ThreadId
self Node
nd)
Maybe Node -> STM (Maybe Node)
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Node -> Maybe Node
forall a. a -> Maybe a
Just Node
nd)
ViewL Node
Seq.EmptyL -> do
Map ThreadId Node
ths <- TVar (Map ThreadId Node) -> STM (Map ThreadId Node)
forall a. TVar a -> STM a
readTVar TVar (Map ThreadId Node)
activeThreads
if Map ThreadId Node -> Bool
forall k a. Map k a -> Bool
Map.null Map ThreadId Node
ths
then Maybe Node -> STM (Maybe Node)
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Node
forall a. Maybe a
Nothing
else STM (Maybe Node)
forall a. STM a
retry
processNode :: Node -> IO ()
processNode :: Node -> IO ()
processNode Node
node = do
let lp :: Solver
lp = Node -> Solver
ndLP Node
node
Maybe Rational
lim <- (Maybe Node -> Maybe Rational)
-> IO (Maybe Node) -> IO (Maybe Rational)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((Node -> Rational) -> Maybe Node -> Maybe Rational
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Node -> Rational
ndValue) (IO (Maybe Node) -> IO (Maybe Rational))
-> IO (Maybe Node) -> IO (Maybe Rational)
forall a b. (a -> b) -> a -> b
$ TVar (Maybe Node) -> IO (Maybe Node)
forall a. TVar a -> IO a
readTVarIO (Solver -> TVar (Maybe Node)
mipBest Solver
solver)
OptResult
ret <- Solver -> Options -> IO OptResult
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Options -> m OptResult
Simplex.dualSimplex Solver
lp Options
forall a. Default a => a
def{ Simplex.objLimit = lim }
case OptResult
ret of
OptResult
Unbounded -> String -> IO ()
forall a. (?callStack::CallStack) => String -> a
error String
"should not happen"
OptResult
Unsat -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
OptResult
ObjLimit -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
OptResult
Optimum -> do
Rational
val <- Solver -> IO Rational
forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m v
Simplex.getObjValue Solver
lp
Bool
p <- Solver -> Rational -> IO Bool
prune Solver
solver Rational
val
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
p (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
[(Int, Rational)]
xs <- Node -> IntSet -> IO [(Int, Rational)]
violated Node
node (Solver -> IntSet
mipIVs Solver
solver)
case [(Int, Rational)]
xs of
[] -> STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TChan Node -> Node -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan Node
solchan (Node -> STM ()) -> Node -> STM ()
forall a b. (a -> b) -> a -> b
$ Node
node { ndValue = val }
[(Int, Rational)]
_ -> do
Maybe Int
r <- if Node -> Int
ndDepth Node
node Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
100 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0
then Maybe Int -> IO (Maybe Int)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing
else ([Int] -> Maybe Int) -> IO [Int] -> IO (Maybe Int)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Int] -> Maybe Int
forall a. [a] -> Maybe a
listToMaybe (IO [Int] -> IO (Maybe Int)) -> IO [Int] -> IO (Maybe Int)
forall a b. (a -> b) -> a -> b
$ (Int -> IO Bool) -> [Int] -> IO [Int]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Solver -> Int -> IO Bool
canDeriveGomoryCut Solver
lp) ([Int] -> IO [Int]) -> [Int] -> IO [Int]
forall a b. (a -> b) -> a -> b
$ ((Int, Rational) -> Int) -> [(Int, Rational)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Rational) -> Int
forall a b. (a, b) -> a
fst [(Int, Rational)]
xs
case Maybe Int
r of
Maybe Int
Nothing -> do
let (Int
v0,Rational
val0) = ((Int, Rational), Rational) -> (Int, Rational)
forall a b. (a, b) -> a
fst (((Int, Rational), Rational) -> (Int, Rational))
-> ((Int, Rational), Rational) -> (Int, Rational)
forall a b. (a -> b) -> a -> b
$ (((Int, Rational), Rational)
-> ((Int, Rational), Rational) -> Ordering)
-> [((Int, Rational), Rational)] -> ((Int, Rational), Rational)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy ((((Int, Rational), Rational) -> Rational)
-> ((Int, Rational), Rational)
-> ((Int, Rational), Rational)
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ((Int, Rational), Rational) -> Rational
forall a b. (a, b) -> b
snd)
[((Int
v,Rational
vval), Rational -> Rational
forall a. Num a => a -> a
abs (Integer -> Rational
forall a. Num a => Integer -> a
fromInteger (Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
round Rational
vval) Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
vval)) | (Int
v,Rational
vval) <- [(Int, Rational)]
xs]
let lp1 :: Solver
lp1 = Solver
lp
Solver
lp2 <- Solver -> IO Solver
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m (GenericSolverM m v)
Simplex.cloneSolver Solver
lp
Solver -> Atom Rational -> IO ()
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Atom Rational -> m ()
Simplex.assertAtom Solver
lp1 (Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
v0 Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsOrdRel e r => e -> e -> r
.<=. Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant (Integer -> Rational
forall a. Num a => Integer -> a
fromInteger (Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
val0)))
Solver -> Atom Rational -> IO ()
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Atom Rational -> m ()
Simplex.assertAtom Solver
lp2 (Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
v0 Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsOrdRel e r => e -> e -> r
.>=. Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant (Integer -> Rational
forall a. Num a => Integer -> a
fromInteger (Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
val0)))
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
Node -> STM ()
addNode (Node -> STM ()) -> Node -> STM ()
forall a b. (a -> b) -> a -> b
$ Solver -> Int -> Rational -> Node
Node Solver
lp1 (Node -> Int
ndDepth Node
node Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Rational
val
Node -> STM ()
addNode (Node -> STM ()) -> Node -> STM ()
forall a b. (a -> b) -> a -> b
$ Solver -> Int -> Rational -> Node
Node Solver
lp2 (Node -> Int
ndDepth Node
node Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Rational
val
TVar Int -> (Int -> Int) -> STM ()
forall a. TVar a -> (a -> a) -> STM ()
modifyTVar TVar Int
visitedNodes (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
Just Int
v -> do
Atom Rational
atom <- Solver -> IntSet -> Int -> IO (Atom Rational)
deriveGomoryCut Solver
lp (Solver -> IntSet
mipIVs Solver
solver) Int
v
Solver -> Atom Rational -> IO ()
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Atom Rational -> m ()
Simplex.assertAtom Solver
lp Atom Rational
atom
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
Node -> STM ()
addNode (Node -> STM ()) -> Node -> STM ()
forall a b. (a -> b) -> a -> b
$ Solver -> Int -> Rational -> Node
Node Solver
lp (Node -> Int
ndDepth Node
node Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Rational
val
let isCompleted :: STM Bool
isCompleted = do
Seq Node
nodes <- TVar (Seq Node) -> STM (Seq Node)
forall a. TVar a -> STM a
readTVar TVar (Seq Node)
pool
Map ThreadId Node
threads <- TVar (Map ThreadId Node) -> STM (Map ThreadId Node)
forall a. TVar a -> STM a
readTVar TVar (Map ThreadId Node)
activeThreads
Bool -> STM Bool
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> STM Bool) -> Bool -> STM Bool
forall a b. (a -> b) -> a -> b
$ Seq Node -> Bool
forall a. Seq a -> Bool
Seq.null Seq Node
nodes Bool -> Bool -> Bool
&& Map ThreadId Node -> Bool
forall k a. Map k a -> Bool
Map.null Map ThreadId Node
threads
Int
nthreads <- (Int -> Int) -> IO Int -> IO Int
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
1) (IO Int -> IO Int) -> IO Int -> IO Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef (Solver -> IORef Int
mipNThread Solver
solver)
Solver -> String -> IO ()
log Solver
solver (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"MIP: forking %d worker threads..." Int
nthreads
TimeSpec
startCPU <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
TimeSpec
startWC <- Clock -> IO TimeSpec
getTime Clock
Monotonic
TMVar SomeException
ex <- IO (TMVar SomeException)
forall a. IO (TMVar a)
newEmptyTMVarIO
let printStatus :: Seq.Seq Node -> Int -> IO ()
printStatus :: Seq Node -> Int -> IO ()
printStatus Seq Node
nodes Int
visited
| Seq Node -> Bool
forall a. Seq a -> Bool
Seq.null Seq Node
nodes = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = do
TimeSpec
nowCPU <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
TimeSpec
nowWC <- Clock -> IO TimeSpec
getTime Clock
Monotonic
let spentCPU :: Int64
spentCPU = TimeSpec -> Int64
sec (TimeSpec
nowCPU TimeSpec -> TimeSpec -> TimeSpec
`diffTimeSpec` TimeSpec
startCPU)
let spentWC :: Int64
spentWC = TimeSpec -> Int64
sec (TimeSpec
nowWC TimeSpec -> TimeSpec -> TimeSpec
`diffTimeSpec` TimeSpec
startWC )
let vs :: [Rational]
vs = (Node -> Rational) -> [Node] -> [Rational]
forall a b. (a -> b) -> [a] -> [b]
map Node -> Rational
ndValue (Seq Node -> [Node]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq Node
nodes)
dualBound :: Rational
dualBound =
case OptDir
dir of
OptDir
OptMin -> [Rational] -> Rational
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Rational]
vs
OptDir
OptMax -> [Rational] -> Rational
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Rational]
vs
Maybe Rational
primalBound <- do
Maybe Node
x <- TVar (Maybe Node) -> IO (Maybe Node)
forall a. TVar a -> IO a
readTVarIO (Solver -> TVar (Maybe Node)
mipBest Solver
solver)
Maybe Rational -> IO (Maybe Rational)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Rational -> IO (Maybe Rational))
-> Maybe Rational -> IO (Maybe Rational)
forall a b. (a -> b) -> a -> b
$ case Maybe Node
x of
Maybe Node
Nothing -> Maybe Rational
forall a. Maybe a
Nothing
Just Node
node -> Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Node -> Rational
ndValue Node
node)
(String
p,String
g) <- case Maybe Rational
primalBound of
Maybe Rational
Nothing -> (String, String) -> IO (String, String)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
"not yet found", String
"--")
Just Rational
val -> do
String
p <- Solver -> Rational -> IO String
showValue Solver
solver Rational
val
let g :: String
g = if Rational
val Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
0
then String
"inf"
else String -> Double -> String
forall r. PrintfType r => String -> r
printf String
"%.2f%%" (Rational -> Double
forall a. Fractional a => Rational -> a
fromRational (Rational -> Rational
forall a. Num a => a -> a
abs (Rational
dualBound Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
val) Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
100 Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational -> Rational
forall a. Num a => a -> a
abs Rational
val) :: Double)
(String, String) -> IO (String, String)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
p, String
g)
String
d <- Solver -> Rational -> IO String
showValue Solver
solver Rational
dualBound
let range :: String
range =
case OptDir
dir of
OptDir
OptMin -> String
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" >= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
d
OptDir
OptMax -> String
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
d
Solver -> String -> IO ()
log Solver
solver (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
-> Int64 -> Int64 -> Int -> Int -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"cpu time = %d sec; wc time = %d sec; active nodes = %d; visited nodes = %d; %s; gap = %s"
Int64
spentCPU Int64
spentWC (Seq Node -> Int
forall a. Seq a -> Int
Seq.length Seq Node
nodes) Int
visited String
range String
g
((forall a. IO a -> IO a) -> IO ()) -> IO ()
forall b. ((forall a. IO a -> IO a) -> IO b) -> IO b
mask (((forall a. IO a -> IO a) -> IO ()) -> IO ())
-> ((forall a. IO a -> IO a) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(forall a. IO a -> IO a
restore :: forall a. IO a -> IO a) -> do
[ThreadId]
threads <- Int -> IO ThreadId -> IO [ThreadId]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
nthreads (IO ThreadId -> IO [ThreadId]) -> IO ThreadId -> IO [ThreadId]
forall a b. (a -> b) -> a -> b
$ do
IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ do
let loop :: IO ()
loop = do
Maybe Node
m <- IO (Maybe Node)
pickNode
case Maybe Node
m of
Maybe Node
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just Node
node -> Node -> IO ()
processNode Node
node IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO ()
loop
Either SomeException ()
ret <- IO () -> IO (Either SomeException ())
forall e a. Exception e => IO a -> IO (Either e a)
try (IO () -> IO (Either SomeException ()))
-> IO () -> IO (Either SomeException ())
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
forall a. IO a -> IO a
restore IO ()
loop
case Either SomeException ()
ret of
Left SomeException
e -> STM () -> IO ()
forall a. STM a -> IO a
atomically (TMVar SomeException -> SomeException -> STM ()
forall a. TMVar a -> a -> STM ()
putTMVar TMVar SomeException
ex SomeException
e)
Right ()
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
let propagateException :: SomeException -> IO ()
propagateException :: SomeException -> IO ()
propagateException SomeException
e = do
(ThreadId -> IO ()) -> [ThreadId] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ThreadId
t -> ThreadId -> SomeException -> IO ()
forall e. Exception e => ThreadId -> e -> IO ()
throwTo ThreadId
t SomeException
e) [ThreadId]
threads
SomeException -> IO ()
forall e a. Exception e => e -> IO a
throwIO SomeException
e
let loop :: IO ()
loop = do
Either SomeException (Maybe (IO ()))
ret <- IO (Maybe (IO ())) -> IO (Either SomeException (Maybe (IO ())))
forall e a. Exception e => IO a -> IO (Either e a)
try (IO (Maybe (IO ())) -> IO (Either SomeException (Maybe (IO ()))))
-> IO (Maybe (IO ())) -> IO (Either SomeException (Maybe (IO ())))
forall a b. (a -> b) -> a -> b
$ Int -> IO (IO ()) -> IO (Maybe (IO ()))
forall a. Int -> IO a -> IO (Maybe a)
timeout (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
1000Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
1000) (IO (IO ()) -> IO (Maybe (IO ())))
-> IO (IO ()) -> IO (Maybe (IO ()))
forall a b. (a -> b) -> a -> b
$ IO (IO ()) -> IO (IO ())
forall a. IO a -> IO a
restore (IO (IO ()) -> 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
$ [STM (IO ())] -> STM (IO ())
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[ do Node
node <- TChan Node -> STM Node
forall a. TChan a -> STM a
readTChan TChan Node
solchan
Bool
ret <- do
Maybe Node
old <- TVar (Maybe Node) -> STM (Maybe Node)
forall a. TVar a -> STM a
readTVar (Solver -> TVar (Maybe Node)
mipBest Solver
solver)
case Maybe Node
old of
Maybe Node
Nothing -> do
TVar (Maybe Node) -> Maybe Node -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar (Solver -> TVar (Maybe Node)
mipBest Solver
solver) (Node -> Maybe Node
forall a. a -> Maybe a
Just Node
node)
Bool -> STM Bool
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Just Node
best -> do
let isBetter :: Bool
isBetter = if OptDir
dirOptDir -> OptDir -> Bool
forall a. Eq a => a -> a -> Bool
==OptDir
OptMin then Node -> Rational
ndValue Node
node Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Node -> Rational
ndValue Node
best else Node -> Rational
ndValue Node
node Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Node -> Rational
ndValue Node
best
Bool -> STM () -> STM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isBetter (STM () -> STM ()) -> STM () -> STM ()
forall a b. (a -> b) -> a -> b
$ TVar (Maybe Node) -> Maybe Node -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar (Solver -> TVar (Maybe Node)
mipBest Solver
solver) (Node -> Maybe Node
forall a. a -> Maybe a
Just Node
node)
Bool -> STM Bool
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
isBetter
IO () -> STM (IO ())
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ret (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
let lp :: Solver
lp = Node -> Solver
ndLP Node
node
Model
m <- Solver -> IO Model
forall v (m :: * -> *).
(SolverValue v, PrimMonad m) =>
GenericSolverM m v -> m Model
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> m Model
Simplex.getModel Solver
lp
Model -> Rational -> IO ()
update Model
m (Node -> Rational
ndValue Node
node)
IO ()
loop
, do Bool
b <- STM Bool
isCompleted
Bool -> STM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
b
IO () -> STM (IO ())
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, do SomeException
e <- TMVar SomeException -> STM SomeException
forall a. TMVar a -> STM a
readTMVar TMVar SomeException
ex
IO () -> STM (IO ())
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return (IO () -> STM (IO ())) -> IO () -> STM (IO ())
forall a b. (a -> b) -> a -> b
$ SomeException -> IO ()
propagateException SomeException
e
]
case Either SomeException (Maybe (IO ()))
ret of
Left (SomeException
e::SomeException) -> SomeException -> IO ()
propagateException SomeException
e
Right (Just IO ()
m) -> IO ()
m
Right Maybe (IO ())
Nothing -> do
(Seq Node
nodes, Int
visited) <- STM (Seq Node, Int) -> IO (Seq Node, Int)
forall a. STM a -> IO a
atomically (STM (Seq Node, Int) -> IO (Seq Node, Int))
-> STM (Seq Node, Int) -> IO (Seq Node, Int)
forall a b. (a -> b) -> a -> b
$ do
Seq Node
nodes <- TVar (Seq Node) -> STM (Seq Node)
forall a. TVar a -> STM a
readTVar TVar (Seq Node)
pool
Map ThreadId Node
athreads <- TVar (Map ThreadId Node) -> STM (Map ThreadId Node)
forall a. TVar a -> STM a
readTVar TVar (Map ThreadId Node)
activeThreads
Int
visited <- TVar Int -> STM Int
forall a. TVar a -> STM a
readTVar TVar Int
visitedNodes
(Seq Node, Int) -> STM (Seq Node, Int)
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Node] -> Seq Node
forall a. [a] -> Seq a
Seq.fromList (Map ThreadId Node -> [Node]
forall k a. Map k a -> [a]
Map.elems Map ThreadId Node
athreads) Seq Node -> Seq Node -> Seq Node
forall a. Seq a -> Seq a -> Seq a
Seq.>< Seq Node
nodes, Int
visited)
Seq Node -> Int -> IO ()
printStatus Seq Node
nodes Int
visited
IO ()
loop
IO ()
loop
getBestSolution :: Solver -> IO (Maybe (Model, Rational))
getBestSolution :: Solver -> IO (Maybe (Model, Rational))
getBestSolution Solver
solver = do
Maybe Node
ret <- TVar (Maybe Node) -> IO (Maybe Node)
forall a. TVar a -> IO a
readTVarIO (Solver -> TVar (Maybe Node)
mipBest Solver
solver)
case Maybe Node
ret of
Maybe Node
Nothing -> Maybe (Model, Rational) -> IO (Maybe (Model, Rational))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Model, Rational)
forall a. Maybe a
Nothing
Just Node
node -> do
Model
m <- Solver -> IO Model
forall v (m :: * -> *).
(SolverValue v, PrimMonad m) =>
GenericSolverM m v -> m Model
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> m Model
Simplex.getModel (Node -> Solver
ndLP Node
node)
Maybe (Model, Rational) -> IO (Maybe (Model, Rational))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Model, Rational) -> IO (Maybe (Model, Rational)))
-> Maybe (Model, Rational) -> IO (Maybe (Model, Rational))
forall a b. (a -> b) -> a -> b
$ (Model, Rational) -> Maybe (Model, Rational)
forall a. a -> Maybe a
Just (Model
m, Node -> Rational
ndValue Node
node)
getBestModel :: Solver -> IO (Maybe Model)
getBestModel :: Solver -> IO (Maybe Model)
getBestModel Solver
solver = (Maybe (Model, Rational) -> Maybe Model)
-> IO (Maybe (Model, Rational)) -> IO (Maybe Model)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (((Model, Rational) -> Model)
-> Maybe (Model, Rational) -> Maybe Model
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Model, Rational) -> Model
forall a b. (a, b) -> a
fst) (IO (Maybe (Model, Rational)) -> IO (Maybe Model))
-> IO (Maybe (Model, Rational)) -> IO (Maybe Model)
forall a b. (a -> b) -> a -> b
$ Solver -> IO (Maybe (Model, Rational))
getBestSolution Solver
solver
getBestValue :: Solver -> IO (Maybe Rational)
getBestValue :: Solver -> IO (Maybe Rational)
getBestValue Solver
solver = (Maybe (Model, Rational) -> Maybe Rational)
-> IO (Maybe (Model, Rational)) -> IO (Maybe Rational)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (((Model, Rational) -> Rational)
-> Maybe (Model, Rational) -> Maybe Rational
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Model, Rational) -> Rational
forall a b. (a, b) -> b
snd) (IO (Maybe (Model, Rational)) -> IO (Maybe Rational))
-> IO (Maybe (Model, Rational)) -> IO (Maybe Rational)
forall a b. (a -> b) -> a -> b
$ Solver -> IO (Maybe (Model, Rational))
getBestSolution Solver
solver
violated :: Node -> IS.IntSet -> IO [(Var, Rational)]
violated :: Node -> IntSet -> IO [(Int, Rational)]
violated Node
node IntSet
ivs = do
Model
m <- Solver -> IO Model
forall v (m :: * -> *).
(SolverValue v, PrimMonad m) =>
GenericSolverM m v -> m Model
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> m Model
Simplex.getModel (Node -> Solver
ndLP Node
node)
let p :: (Int, a) -> Bool
p (Int
v,a
val) = Int
v Int -> IntSet -> Bool
`IS.member` IntSet
ivs Bool -> Bool -> Bool
&& Bool -> Bool
not (a -> Bool
forall a. RealFrac a => a -> Bool
isInteger a
val)
[(Int, Rational)] -> IO [(Int, Rational)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, Rational)] -> IO [(Int, Rational)])
-> [(Int, Rational)] -> IO [(Int, Rational)]
forall a b. (a -> b) -> a -> b
$ ((Int, Rational) -> Bool) -> [(Int, Rational)] -> [(Int, Rational)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int, Rational) -> Bool
forall {a}. RealFrac a => (Int, a) -> Bool
p (Model -> [(Int, Rational)]
forall a. IntMap a -> [(Int, a)]
IM.toList Model
m)
prune :: Solver -> Rational -> IO Bool
prune :: Solver -> Rational -> IO Bool
prune Solver
solver Rational
lb = do
Maybe Node
b <- TVar (Maybe Node) -> IO (Maybe Node)
forall a. TVar a -> IO a
readTVarIO (Solver -> TVar (Maybe Node)
mipBest Solver
solver)
case Maybe Node
b of
Maybe Node
Nothing -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just Node
node -> do
OptDir
dir <- Solver -> IO OptDir
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m OptDir
Simplex.getOptDir (Solver -> Solver
mipRootLP Solver
solver)
Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ if OptDir
dirOptDir -> OptDir -> Bool
forall a. Eq a => a -> a -> Bool
==OptDir
OptMin then Node -> Rational
ndValue Node
node Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
lb else Node -> Rational
ndValue Node
node Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
>= Rational
lb
showValue :: Solver -> Rational -> IO String
showValue :: Solver -> Rational -> IO String
showValue Solver
solver Rational
v = do
Bool
printRat <- IORef Bool -> IO Bool
forall a. IORef a -> IO a
readIORef (Solver -> IORef Bool
mipShowRational Solver
solver)
String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Bool -> Rational -> String
forall v. SolverValue v => Bool -> v -> String
Simplex.showValue Bool
printRat Rational
v
setShowRational :: Solver -> Bool -> IO ()
setShowRational :: Solver -> Bool -> IO ()
setShowRational Solver
solver = IORef Bool -> Bool -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Bool
mipShowRational Solver
solver)
setNThread :: Solver -> Int -> IO ()
setNThread :: Solver -> Int -> IO ()
setNThread Solver
solver = IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Int
mipNThread Solver
solver)
setLogger :: Solver -> (String -> IO ()) -> IO ()
setLogger :: Solver -> (String -> IO ()) -> IO ()
setLogger Solver
solver String -> IO ()
logger = do
IORef (Maybe (String -> IO ())) -> Maybe (String -> IO ()) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Maybe (String -> IO ()))
mipLogger Solver
solver) ((String -> IO ()) -> Maybe (String -> IO ())
forall a. a -> Maybe a
Just String -> IO ()
logger)
setOnUpdateBestSolution :: Solver -> (Model -> Rational -> IO ()) -> IO ()
setOnUpdateBestSolution :: Solver -> (Model -> Rational -> IO ()) -> IO ()
setOnUpdateBestSolution Solver
solver Model -> Rational -> IO ()
cb = do
IORef (Model -> Rational -> IO ())
-> (Model -> Rational -> IO ()) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Model -> Rational -> IO ())
mipOnUpdateBestSolution Solver
solver) Model -> Rational -> IO ()
cb
log :: Solver -> String -> IO ()
log :: Solver -> String -> IO ()
log Solver
solver String
msg = Solver -> IO String -> IO ()
logIO Solver
solver (String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return String
msg)
logIO :: Solver -> IO String -> IO ()
logIO :: Solver -> IO String -> IO ()
logIO Solver
solver IO String
action = do
Maybe (String -> IO ())
m <- IORef (Maybe (String -> IO ())) -> IO (Maybe (String -> IO ()))
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Maybe (String -> IO ()))
mipLogger Solver
solver)
case Maybe (String -> IO ())
m of
Maybe (String -> IO ())
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just String -> IO ()
logger -> IO String
action IO String -> (String -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> IO ()
logger
deriveGomoryCut :: Simplex.Solver -> IS.IntSet -> Var -> IO (LA.Atom Rational)
deriveGomoryCut :: Solver -> IntSet -> Int -> IO (Atom Rational)
deriveGomoryCut Solver
lp IntSet
ivs Int
xi = do
Rational
v0 <- Solver -> Int -> IO Rational
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
Simplex.getValue Solver
lp Int
xi
let f0 :: Rational
f0 = Rational -> Rational
forall a. RealFrac a => a -> a
fracPart Rational
v0
Bool -> IO () -> IO ()
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Rational
0 Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
f0 Bool -> Bool -> Bool
&& Rational
f0 Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
1) (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 ()
Expr Rational
row <- Solver -> Int -> IO (Expr Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
Simplex.getRow Solver
lp Int
xi
let p :: (a, Int) -> IO Bool
p (a
_,Int
xj) = do
Bound Rational
lb <- Solver -> Int -> IO (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
Simplex.getLB Solver
lp Int
xj
Bound Rational
ub <- Solver -> Int -> IO (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
Simplex.getUB Solver
lp Int
xj
case (Bound Rational
lb,Bound Rational
ub) of
(Just (Rational, IntSet)
l, Just (Rational, IntSet)
u) -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Rational, IntSet)
l (Rational, IntSet) -> (Rational, IntSet) -> Bool
forall a. Ord a => a -> a -> Bool
< (Rational, IntSet)
u)
(Bound Rational, Bound Rational)
_ -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
[(Rational, Int)]
ns <- ((Rational, Int) -> IO Bool)
-> [(Rational, Int)] -> IO [(Rational, Int)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Rational, Int) -> IO Bool
forall {a}. (a, Int) -> IO Bool
p ([(Rational, Int)] -> IO [(Rational, Int)])
-> [(Rational, Int)] -> IO [(Rational, Int)]
forall a b. (a -> b) -> a -> b
$ Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
row
[(Rational, Int)]
js <- (((Rational, Int) -> IO Bool)
-> [(Rational, Int)] -> IO [(Rational, Int)])
-> [(Rational, Int)]
-> ((Rational, Int) -> IO Bool)
-> IO [(Rational, Int)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Rational, Int) -> IO Bool)
-> [(Rational, Int)] -> IO [(Rational, Int)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM [(Rational, Int)]
ns (((Rational, Int) -> IO Bool) -> IO [(Rational, Int)])
-> ((Rational, Int) -> IO Bool) -> IO [(Rational, Int)]
forall a b. (a -> b) -> a -> b
$ \(Rational
_, Int
xj) -> do
Rational
vj <- Solver -> Int -> IO Rational
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
Simplex.getValue Solver
lp Int
xj
Bound Rational
lb <- Solver -> Int -> IO (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
Simplex.getLB Solver
lp Int
xj
Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Rational -> Maybe Rational
forall a. a -> Maybe a
Just Rational
vj Maybe Rational -> Maybe Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Bound Rational -> Maybe Rational
forall v. SolverValue v => Bound v -> Maybe v
Simplex.boundValue Bound Rational
lb
[(Rational, Int)]
ks <- (((Rational, Int) -> IO Bool)
-> [(Rational, Int)] -> IO [(Rational, Int)])
-> [(Rational, Int)]
-> ((Rational, Int) -> IO Bool)
-> IO [(Rational, Int)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Rational, Int) -> IO Bool)
-> [(Rational, Int)] -> IO [(Rational, Int)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM [(Rational, Int)]
ns (((Rational, Int) -> IO Bool) -> IO [(Rational, Int)])
-> ((Rational, Int) -> IO Bool) -> IO [(Rational, Int)]
forall a b. (a -> b) -> a -> b
$ \(Rational
_, Int
xj) -> do
Rational
vj <- Solver -> Int -> IO Rational
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
Simplex.getValue Solver
lp Int
xj
Bound Rational
ub <- Solver -> Int -> IO (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
Simplex.getUB Solver
lp Int
xj
Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Rational -> Maybe Rational
forall a. a -> Maybe a
Just Rational
vj Maybe Rational -> Maybe Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Bound Rational -> Maybe Rational
forall v. SolverValue v => Bound v -> Maybe v
Simplex.boundValue Bound Rational
ub
[Expr Rational]
xs1 <- [(Rational, Int)]
-> ((Rational, Int) -> IO (Expr Rational)) -> IO [Expr Rational]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Rational, Int)]
js (((Rational, Int) -> IO (Expr Rational)) -> IO [Expr Rational])
-> ((Rational, Int) -> IO (Expr Rational)) -> IO [Expr Rational]
forall a b. (a -> b) -> a -> b
$ \(Rational
aij, Int
xj) -> do
let fj :: Rational
fj = Rational -> Rational
forall a. RealFrac a => a -> a
fracPart Rational
aij
Just (Rational
lj,IntSet
_) <- Solver -> Int -> IO (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
Simplex.getLB Solver
lp Int
xj
let c :: Rational
c = if Int
xj Int -> IntSet -> Bool
`IS.member` IntSet
ivs
then (if Rational
fj Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
f0 then Rational
fj Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ (Rational
1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
f0) else ((Rational
1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
fj) Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
f0))
else (if Rational
aij Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0 then Rational
aij Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ (Rational
1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
f0) else (-Rational
aij Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
f0))
Expr Rational -> IO (Expr Rational)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Rational -> IO (Expr Rational))
-> Expr Rational -> IO (Expr Rational)
forall a b. (a -> b) -> a -> b
$ Rational
Scalar (Expr Rational)
c Scalar (Expr Rational) -> Expr Rational -> Expr Rational
forall v. VectorSpace v => Scalar v -> v -> v
*^ (Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
xj Expr Rational -> Expr Rational -> Expr Rational
forall v. AdditiveGroup v => v -> v -> v
^-^ Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
lj)
[Expr Rational]
xs2 <- [(Rational, Int)]
-> ((Rational, Int) -> IO (Expr Rational)) -> IO [Expr Rational]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Rational, Int)]
ks (((Rational, Int) -> IO (Expr Rational)) -> IO [Expr Rational])
-> ((Rational, Int) -> IO (Expr Rational)) -> IO [Expr Rational]
forall a b. (a -> b) -> a -> b
$ \(Rational
aij, Int
xj) -> do
let fj :: Rational
fj = Rational -> Rational
forall a. RealFrac a => a -> a
fracPart Rational
aij
Just (Rational
uj, IntSet
_) <- Solver -> Int -> IO (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
Simplex.getUB Solver
lp Int
xj
let c :: Rational
c = if Int
xj Int -> IntSet -> Bool
`IS.member` IntSet
ivs
then (if Rational
fj Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
f0 then Rational
fj Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
f0 else ((Rational
1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
fj) Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ (Rational
1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
f0)))
else (if Rational
aij Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0 then Rational
aij Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
f0 else (-Rational
aij Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ (Rational
1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
f0)))
Expr Rational -> IO (Expr Rational)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Rational -> IO (Expr Rational))
-> Expr Rational -> IO (Expr Rational)
forall a b. (a -> b) -> a -> b
$ Rational
Scalar (Expr Rational)
c Scalar (Expr Rational) -> Expr Rational -> Expr Rational
forall v. VectorSpace v => Scalar v -> v -> v
*^ (Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
uj Expr Rational -> Expr Rational -> Expr Rational
forall v. AdditiveGroup v => v -> v -> v
^-^ Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
xj)
Atom Rational -> IO (Atom Rational)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom Rational -> IO (Atom Rational))
-> Atom Rational -> IO (Atom Rational)
forall a b. (a -> b) -> a -> b
$ [Expr Rational] -> Expr Rational
forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [Expr Rational]
xs1 Expr Rational -> Expr Rational -> Expr Rational
forall v. AdditiveGroup v => v -> v -> v
^+^ [Expr Rational] -> Expr Rational
forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [Expr Rational]
xs2 Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsOrdRel e r => e -> e -> r
.>=. Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
1
canDeriveGomoryCut :: Simplex.Solver -> Var -> IO Bool
canDeriveGomoryCut :: Solver -> Int -> IO Bool
canDeriveGomoryCut Solver
lp Int
xi = do
Bool
b <- Solver -> Int -> IO Bool
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m Bool
Simplex.isBasicVariable Solver
lp Int
xi
if Bool -> Bool
not Bool
b
then Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
else do
Rational
val <- Solver -> Int -> IO Rational
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
Simplex.getValue Solver
lp Int
xi
if Rational -> Bool
forall a. RealFrac a => a -> Bool
isInteger Rational
val
then Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
else do
Expr Rational
row <- Solver -> Int -> IO (Expr Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
Simplex.getRow Solver
lp Int
xi
[Bool]
ys <- [(Rational, Int)] -> ((Rational, Int) -> IO Bool) -> IO [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
row) (((Rational, Int) -> IO Bool) -> IO [Bool])
-> ((Rational, Int) -> IO Bool) -> IO [Bool]
forall a b. (a -> b) -> a -> b
$ \(Rational
_,Int
xj) -> do
Rational
vj <- Solver -> Int -> IO Rational
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
Simplex.getValue Solver
lp Int
xj
Bound Rational
lb <- Solver -> Int -> IO (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
Simplex.getLB Solver
lp Int
xj
Bound Rational
ub <- Solver -> Int -> IO (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
Simplex.getUB Solver
lp Int
xj
Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Rational -> Maybe Rational
forall a. a -> Maybe a
Just Rational
vj Maybe Rational -> Maybe Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Bound Rational -> Maybe Rational
forall v. SolverValue v => Bound v -> Maybe v
Simplex.boundValue Bound Rational
lb Bool -> Bool -> Bool
|| Rational -> Maybe Rational
forall a. a -> Maybe a
Just Rational
vj Maybe Rational -> Maybe Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Bound Rational -> Maybe Rational
forall v. SolverValue v => Bound v -> Maybe v
Simplex.boundValue Bound Rational
ub
Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
ys)