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

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

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

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

    (Expr, MIP2PBInfo) -> ExceptT String m (Expr, MIP2PBInfo)
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 = Problem Rational -> Set Var
forall c. Problem c -> Set Var
MIP.integerVariables Problem Rational
mip
    nivs :: Set Var
nivs = Problem Rational -> Set Var
forall c. Problem c -> Set Var
MIP.variables Problem Rational
mip Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set Var
ivs

    nonAdjacentPairs :: [a] -> [(a,a)]
    nonAdjacentPairs :: [a] -> [(a, a)]
nonAdjacentPairs (a
x1:a
x2:[a]
xs) = [(a
x1,a
x3) | a
x3 <- [a]
xs] [(a, a)] -> [(a, a)] -> [(a, a)]
forall a. [a] -> [a] -> [a]
++ [a] -> [(a, a)]
forall a. [a] -> [(a, a)]
nonAdjacentPairs (a
x2a -> [a] -> [a]
forall 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
_ = String -> Int
forall a. HasCallStack => String -> a
error String
"asBin: failure"

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

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

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