{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.MIP2PB
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.Converter.MIP2PB
  ( mip2pb
  , MIP2PBInfo (..)
  , addMIP
  ) where

import Control.Monad
import Control.Monad.ST
import Control.Monad.Trans
import Control.Monad.Trans.Except
import Data.List (intercalate, foldl', sortBy)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Ord
import Data.Ratio
import qualified Data.Set as Set
import Data.VectorSpace

import qualified Data.PseudoBoolean as PBFile
import qualified Numeric.Optimization.MIP as MIP

import ToySolver.Converter.Base
import ToySolver.Data.OrdRel
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Integer as Integer
import ToySolver.SAT.Store.PB
import ToySolver.Internal.Util (revForM)

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

mip2pb :: MIP.Problem Rational -> Either String (PBFile.Formula, MIP2PBInfo)
mip2pb :: Problem Rational -> Either String (Formula, MIP2PBInfo)
mip2pb Problem Rational
mip = forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall s. ExceptT String (ST s) (Formula, MIP2PBInfo)
m
  where
    m :: ExceptT String (ST s) (PBFile.Formula, MIP2PBInfo)
    m :: forall s. ExceptT String (ST s) (Formula, MIP2PBInfo)
m = do
      PBStore (ST s)
db <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
      (Integer.Expr PBSum
obj, MIP2PBInfo
info) <- forall (m :: * -> *) enc.
AddPBNL m enc =>
enc -> Problem Rational -> ExceptT String m (Expr, MIP2PBInfo)
addMIP' PBStore (ST s)
db Problem Rational
mip
      Formula
formula <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Formula
formula{ pbObjectiveFunction :: Maybe PBSum
PBFile.pbObjectiveFunction = forall a. a -> Maybe a
Just PBSum
obj }, MIP2PBInfo
info)

data MIP2PBInfo = MIP2PBInfo (Map MIP.Var Integer.Expr) !Integer
  deriving (MIP2PBInfo -> MIP2PBInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MIP2PBInfo -> MIP2PBInfo -> Bool
$c/= :: MIP2PBInfo -> MIP2PBInfo -> Bool
== :: MIP2PBInfo -> MIP2PBInfo -> Bool
$c== :: MIP2PBInfo -> MIP2PBInfo -> Bool
Eq, Int -> MIP2PBInfo -> ShowS
[MIP2PBInfo] -> ShowS
MIP2PBInfo -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MIP2PBInfo] -> ShowS
$cshowList :: [MIP2PBInfo] -> ShowS
show :: MIP2PBInfo -> String
$cshow :: MIP2PBInfo -> String
showsPrec :: Int -> MIP2PBInfo -> ShowS
$cshowsPrec :: Int -> MIP2PBInfo -> ShowS
Show)

instance Transformer MIP2PBInfo where
  type Source MIP2PBInfo = Map MIP.Var Integer
  type Target MIP2PBInfo = SAT.Model

instance BackwardTransformer MIP2PBInfo where
  transformBackward :: MIP2PBInfo -> Target MIP2PBInfo -> Source MIP2PBInfo
transformBackward (MIP2PBInfo Map Var Expr
vmap Integer
_d) Target MIP2PBInfo
m = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall m. IModel m => m -> Expr -> Integer
Integer.eval Target MIP2PBInfo
m) Map Var Expr
vmap

instance ObjValueTransformer MIP2PBInfo where
  type SourceObjValue MIP2PBInfo = Rational
  type TargetObjValue MIP2PBInfo = Integer

instance ObjValueForwardTransformer MIP2PBInfo where
  transformObjValueForward :: MIP2PBInfo
-> SourceObjValue MIP2PBInfo -> TargetObjValue MIP2PBInfo
transformObjValueForward (MIP2PBInfo Map Var Expr
_vmap Integer
d) SourceObjValue MIP2PBInfo
val = Rational -> Integer
asInteger (SourceObjValue MIP2PBInfo
val forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d)

instance ObjValueBackwardTransformer MIP2PBInfo where
  transformObjValueBackward :: MIP2PBInfo
-> TargetObjValue MIP2PBInfo -> SourceObjValue MIP2PBInfo
transformObjValueBackward (MIP2PBInfo Map Var Expr
_vmap Integer
d) TargetObjValue MIP2PBInfo
val = forall a b. (Integral a, Num b) => a -> b
fromIntegral TargetObjValue MIP2PBInfo
val forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d

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

addMIP :: SAT.AddPBNL m enc => enc -> MIP.Problem Rational -> m (Either String (Integer.Expr, MIP2PBInfo))
addMIP :: forall (m :: * -> *) enc.
AddPBNL m enc =>
enc -> Problem Rational -> m (Either String (Expr, MIP2PBInfo))
addMIP enc
enc Problem Rational
mip = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) enc.
AddPBNL m enc =>
enc -> Problem Rational -> ExceptT String m (Expr, MIP2PBInfo)
addMIP' enc
enc Problem Rational
mip

addMIP' :: SAT.AddPBNL m enc => enc -> MIP.Problem Rational -> ExceptT String m (Integer.Expr, MIP2PBInfo)
addMIP' :: forall (m :: * -> *) enc.
AddPBNL m enc =>
enc -> Problem Rational -> ExceptT String m (Expr, MIP2PBInfo)
addMIP' enc
enc Problem Rational
mip = do
  if Bool -> Bool
not (forall a. Set a -> Bool
Set.null Set Var
nivs) then do
    forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE forall a b. (a -> b) -> a -> b
$ String
"cannot handle non-integer variables: " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map Var -> String
MIP.fromVar (forall a. Set a -> [a]
Set.toList Set Var
nivs))
  else do
    Map Var Expr
vmap <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Monad m => [a] -> (a -> m b) -> m [b]
revForM (forall a. Set a -> [a]
Set.toList Set Var
ivs) forall a b. (a -> b) -> a -> b
$ \Var
v -> do
      case forall c. Num c => Problem c -> Var -> Bounds c
MIP.getBounds Problem Rational
mip Var
v of
        (MIP.Finite Rational
lb, MIP.Finite Rational
ub) -> do
          Expr
v2 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) enc.
AddPBNL m enc =>
enc -> Integer -> Integer -> m Expr
Integer.newVar enc
enc (forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
lb) (forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
ub)
          forall (m :: * -> *) a. Monad m => a -> m a
return (Var
v,Expr
v2)
        (BoundExpr Rational, BoundExpr Rational)
_ -> do
          forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE forall a b. (a -> b) -> a -> b
$ String
"cannot handle unbounded variable: " forall a. [a] -> [a] -> [a]
++ Var -> String
MIP.fromVar Var
v
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall c. Problem c -> [Constraint c]
MIP.constraints Problem Rational
mip) forall a b. (a -> b) -> a -> b
$ \Constraint Rational
c -> do
      let lhs :: Expr Rational
lhs = forall c. Constraint c -> Expr c
MIP.constrExpr Constraint Rational
c
      let f :: RelOp -> Rational -> ExceptT String m ()
f RelOp
op Rational
rhs = do
            let d :: Integer
d = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Integral a => a -> a -> a
lcm Integer
1 (forall a b. (a -> b) -> [a] -> [b]
map forall a. Ratio a -> a
denominator  (Rational
rhsforall a. a -> [a] -> [a]
:[Rational
r | MIP.Term Rational
r [Var]
_ <- forall c. Expr c -> [Term c]
MIP.terms Expr Rational
lhs]))
                lhs' :: Expr
lhs' = forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [Rational -> Integer
asInteger (Rational
r forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d) forall v. VectorSpace v => Scalar v -> v -> v
*^ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [Map Var Expr
vmap forall k a. Ord k => Map k a -> k -> a
Map.! Var
v | Var
v <- [Var]
vs] | MIP.Term Rational
r [Var]
vs <- forall c. Expr c -> [Term c]
MIP.terms Expr Rational
lhs]
                rhs' :: Integer
rhs' = Rational -> Integer
asInteger (Rational
rhs forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d)
                c2 :: OrdRel Expr
c2 = case RelOp
op of
                       RelOp
MIP.Le  -> Expr
lhs' forall e r. IsOrdRel e r => e -> e -> r
.<=. forall a. Num a => Integer -> a
fromInteger Integer
rhs'
                       RelOp
MIP.Ge  -> Expr
lhs' forall e r. IsOrdRel e r => e -> e -> r
.>=. forall a. Num a => Integer -> a
fromInteger Integer
rhs'
                       RelOp
MIP.Eql -> Expr
lhs' forall e r. IsEqRel e r => e -> e -> r
.==. forall a. Num a => Integer -> a
fromInteger Integer
rhs'
            case forall c. Constraint c -> Maybe (Var, c)
MIP.constrIndicator Constraint Rational
c of
              Maybe (Var, Rational)
Nothing -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) enc.
AddPBNL m enc =>
enc -> OrdRel Expr -> m ()
Integer.addConstraint enc
enc OrdRel Expr
c2
              Just (Var
var, Rational
val) -> do
                let var' :: Int
var' = Expr -> Int
asBin (Map Var Expr
vmap forall k a. Ord k => Map k a -> k -> a
Map.! Var
var)
                case Rational
val of
                  Rational
1 -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) enc.
AddPBNL m enc =>
enc -> Int -> OrdRel Expr -> m ()
Integer.addConstraintSoft enc
enc Int
var' OrdRel Expr
c2
                  Rational
0 -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) enc.
AddPBNL m enc =>
enc -> Int -> OrdRel Expr -> m ()
Integer.addConstraintSoft enc
enc (Int -> Int
SAT.litNot Int
var') OrdRel Expr
c2
                  Rational
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      case (forall c. Constraint c -> BoundExpr c
MIP.constrLB Constraint Rational
c, forall c. Constraint c -> BoundExpr c
MIP.constrUB Constraint Rational
c) of
        (MIP.Finite Rational
x1, MIP.Finite Rational
x2) | Rational
x1forall a. Eq a => a -> a -> Bool
==Rational
x2 -> RelOp -> Rational -> ExceptT String m ()
f RelOp
MIP.Eql Rational
x2
        (BoundExpr Rational
lb, BoundExpr Rational
ub) -> do
          case BoundExpr Rational
lb of
            BoundExpr Rational
MIP.NegInf -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
            MIP.Finite Rational
x -> RelOp -> Rational -> ExceptT String m ()
f RelOp
MIP.Ge Rational
x
            BoundExpr Rational
MIP.PosInf -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause enc
enc []
          case BoundExpr Rational
ub of
            BoundExpr Rational
MIP.NegInf -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause enc
enc []
            MIP.Finite Rational
x -> RelOp -> Rational -> ExceptT String m ()
f RelOp
MIP.Le Rational
x
            BoundExpr Rational
MIP.PosInf -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall c. Problem c -> [SOSConstraint c]
MIP.sosConstraints Problem Rational
mip) forall a b. (a -> b) -> a -> b
$ \MIP.SOSConstraint{ sosType :: forall c. SOSConstraint c -> SOSType
MIP.sosType = SOSType
typ, sosBody :: forall c. SOSConstraint c -> [(Var, c)]
MIP.sosBody = [(Var, Rational)]
xs } -> do
      case SOSType
typ of
        SOSType
MIP.S1 -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
AddCardinality m a =>
a -> Clause -> Int -> m ()
SAT.addAtMost enc
enc (forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Int
asBin forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Var Expr
vmap forall k a. Ord k => Map k a -> k -> a
Map.!) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Var, Rational)]
xs) Int
1
        SOSType
MIP.S2 -> do
          let ps :: [(Var, Var)]
ps = forall a. [a] -> [(a, a)]
nonAdjacentPairs forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ [(Var, Rational)]
xs
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Var, Var)]
ps forall a b. (a -> b) -> a -> b
$ \(Var
x1,Var
x2) -> do
            forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. AddClause m a => a -> Clause -> m ()
SAT.addClause enc
enc [Int -> Int
SAT.litNot forall a b. (a -> b) -> a -> b
$ Expr -> Int
asBin forall a b. (a -> b) -> a -> b
$ Map Var Expr
vmap forall k a. Ord k => Map k a -> k -> a
Map.! Var
v | Var
v <- [Var
x1,Var
x2]]

    let obj :: ObjectiveFunction Rational
obj = forall c. Problem c -> ObjectiveFunction c
MIP.objectiveFunction Problem Rational
mip
        d :: Integer
d = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Integral a => a -> a -> a
lcm Integer
1 [forall a. Ratio a -> a
denominator Rational
r | MIP.Term Rational
r [Var]
_ <- forall c. Expr c -> [Term c]
MIP.terms (forall c. ObjectiveFunction c -> Expr c
MIP.objExpr ObjectiveFunction Rational
obj)] forall a. Num a => a -> a -> a
*
            (if forall c. ObjectiveFunction c -> OptDir
MIP.objDir ObjectiveFunction Rational
obj forall a. Eq a => a -> a -> Bool
== OptDir
MIP.OptMin then Integer
1 else -Integer
1)
        obj2 :: Expr
obj2 = forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [Rational -> Integer
asInteger (Rational
r forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d) forall v. VectorSpace v => Scalar v -> v -> v
*^ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [Map Var Expr
vmap forall k a. Ord k => Map k a -> k -> a
Map.! Var
v | Var
v <- [Var]
vs] | MIP.Term Rational
r [Var]
vs <- forall c. Expr c -> [Term c]
MIP.terms (forall c. ObjectiveFunction c -> Expr c
MIP.objExpr ObjectiveFunction Rational
obj)]

    forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
obj2, Map Var Expr -> Integer -> MIP2PBInfo
MIP2PBInfo Map Var Expr
vmap Integer
d)

  where
    ivs :: Set Var
ivs = forall c. Problem c -> Set Var
MIP.integerVariables Problem Rational
mip
    nivs :: Set Var
nivs = forall c. Problem c -> Set Var
MIP.variables Problem Rational
mip forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set Var
ivs

    nonAdjacentPairs :: [a] -> [(a,a)]
    nonAdjacentPairs :: forall a. [a] -> [(a, a)]
nonAdjacentPairs (a
x1:a
x2:[a]
xs) = [(a
x1,a
x3) | a
x3 <- [a]
xs] forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [(a, a)]
nonAdjacentPairs (a
x2forall a. a -> [a] -> [a]
:[a]
xs)
    nonAdjacentPairs [a]
_ = []

    asBin :: Integer.Expr -> SAT.Lit
    asBin :: Expr -> Int
asBin (Integer.Expr [(Integer
1,[Int
lit])]) = Int
lit
    asBin Expr
_ = forall a. HasCallStack => String -> a
error String
"asBin: failure"

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

asInteger :: Rational -> Integer
asInteger :: Rational -> Integer
asInteger Rational
r
  | forall a. Ratio a -> a
denominator Rational
r forall a. Eq a => a -> a -> Bool
/= Integer
1 = forall a. HasCallStack => String -> a
error (forall a. Show a => a -> String
show Rational
r forall a. [a] -> [a] -> [a]
++ String
" is not integer")
  | Bool
otherwise = forall a. Ratio a -> a
numerator Rational
r

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