{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.PB2IP
-- Copyright   :  (c) Masahiro Sakai 2011-2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.Converter.PB2IP
  ( pb2ip
  , PB2IPInfo
  , wbo2ip
  , WBO2IPInfo

  , sat2ip
  , SAT2IPInfo
  , maxsat2ip
  , MaxSAT2IPInfo
  ) where

import Data.Array.IArray
import Data.Default.Class
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map

import qualified Data.PseudoBoolean as PBFile
import qualified Numeric.Optimization.MIP as MIP
import Numeric.Optimization.MIP ((.==.), (.<=.), (.>=.))

import ToySolver.Converter.Base
import ToySolver.Converter.PB
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT

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

newtype PB2IPInfo = PB2IPInfo Int
  deriving (PB2IPInfo -> PB2IPInfo -> Bool
(PB2IPInfo -> PB2IPInfo -> Bool)
-> (PB2IPInfo -> PB2IPInfo -> Bool) -> Eq PB2IPInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PB2IPInfo -> PB2IPInfo -> Bool
$c/= :: PB2IPInfo -> PB2IPInfo -> Bool
== :: PB2IPInfo -> PB2IPInfo -> Bool
$c== :: PB2IPInfo -> PB2IPInfo -> Bool
Eq, Int -> PB2IPInfo -> ShowS
[PB2IPInfo] -> ShowS
PB2IPInfo -> String
(Int -> PB2IPInfo -> ShowS)
-> (PB2IPInfo -> String)
-> ([PB2IPInfo] -> ShowS)
-> Show PB2IPInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PB2IPInfo] -> ShowS
$cshowList :: [PB2IPInfo] -> ShowS
show :: PB2IPInfo -> String
$cshow :: PB2IPInfo -> String
showsPrec :: Int -> PB2IPInfo -> ShowS
$cshowsPrec :: Int -> PB2IPInfo -> ShowS
Show, ReadPrec [PB2IPInfo]
ReadPrec PB2IPInfo
Int -> ReadS PB2IPInfo
ReadS [PB2IPInfo]
(Int -> ReadS PB2IPInfo)
-> ReadS [PB2IPInfo]
-> ReadPrec PB2IPInfo
-> ReadPrec [PB2IPInfo]
-> Read PB2IPInfo
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [PB2IPInfo]
$creadListPrec :: ReadPrec [PB2IPInfo]
readPrec :: ReadPrec PB2IPInfo
$creadPrec :: ReadPrec PB2IPInfo
readList :: ReadS [PB2IPInfo]
$creadList :: ReadS [PB2IPInfo]
readsPrec :: Int -> ReadS PB2IPInfo
$creadsPrec :: Int -> ReadS PB2IPInfo
Read)

instance Transformer PB2IPInfo where
  type Source PB2IPInfo = SAT.Model
  type Target PB2IPInfo = Map MIP.Var Rational

instance ForwardTransformer PB2IPInfo where
  transformForward :: PB2IPInfo -> Source PB2IPInfo -> Target PB2IPInfo
transformForward PB2IPInfo
_ Source PB2IPInfo
m =
    [(Var, Rational)] -> Map Var Rational
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int -> Var
convVar Int
v, if Bool
val then Rational
1 else Rational
0) | (Int
v,Bool
val) <- UArray Int Bool -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Int Bool
Source PB2IPInfo
m]

instance BackwardTransformer PB2IPInfo where
  transformBackward :: PB2IPInfo -> Target PB2IPInfo -> Source PB2IPInfo
transformBackward (PB2IPInfo Int
nv) = Int -> Map Var Rational -> UArray Int Bool
mtrans Int
nv

pb2ip :: PBFile.Formula -> (MIP.Problem Integer, PB2IPInfo)
pb2ip :: Formula -> (Problem Integer, PB2IPInfo)
pb2ip Formula
formula = (Problem Integer
mip, Int -> PB2IPInfo
PB2IPInfo (Formula -> Int
PBFile.pbNumVars Formula
formula))
  where
    mip :: Problem Integer
mip = Problem Integer
forall a. Default a => a
def
      { objectiveFunction :: ObjectiveFunction Integer
MIP.objectiveFunction = ObjectiveFunction Integer
obj2
      , constraints :: [Constraint Integer]
MIP.constraints = [Constraint Integer]
cs2
      , varType :: Map Var VarType
MIP.varType = [(Var, VarType)] -> Map Var VarType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var
v, VarType
MIP.IntegerVariable) | Var
v <- [Var]
vs]
      , varBounds :: Map Var (Bounds Integer)
MIP.varBounds = [(Var, Bounds Integer)] -> Map Var (Bounds Integer)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var
v, (BoundExpr Integer
0,BoundExpr Integer
1)) | Var
v <- [Var]
vs]
      }

    vs :: [Var]
vs = [Int -> Var
convVar Int
v | Int
v <- [Int
1..Formula -> Int
PBFile.pbNumVars Formula
formula]]

    obj2 :: ObjectiveFunction Integer
obj2 =
      case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
        Just Sum
obj' -> ObjectiveFunction Any
forall a. Default a => a
def{ objDir :: OptDir
MIP.objDir = OptDir
MIP.OptMin, objExpr :: Expr Integer
MIP.objExpr = Sum -> Expr Integer
convExpr Sum
obj' }
        Maybe Sum
Nothing   -> ObjectiveFunction Any
forall a. Default a => a
def{ objDir :: OptDir
MIP.objDir = OptDir
MIP.OptMin, objExpr :: Expr Integer
MIP.objExpr = Expr Integer
0 }

    cs2 :: [Constraint Integer]
cs2 = do
      (Sum
lhs,Op
op,Integer
rhs) <- Formula -> [(Sum, Op, Integer)]
PBFile.pbConstraints Formula
formula
      let (Expr Integer
lhs2,Integer
c) = Expr Integer -> (Expr Integer, Integer)
splitConst (Expr Integer -> (Expr Integer, Integer))
-> Expr Integer -> (Expr Integer, Integer)
forall a b. (a -> b) -> a -> b
$ Sum -> Expr Integer
convExpr Sum
lhs
          rhs2 :: Integer
rhs2 = Integer
rhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
c
      Constraint Integer -> [Constraint Integer]
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint Integer -> [Constraint Integer])
-> Constraint Integer -> [Constraint Integer]
forall a b. (a -> b) -> a -> b
$ case Op
op of
        Op
PBFile.Ge -> Constraint Integer
forall a. Default a => a
def{ constrExpr :: Expr Integer
MIP.constrExpr = Expr Integer
lhs2, constrLB :: BoundExpr Integer
MIP.constrLB = Integer -> BoundExpr Integer
forall r. r -> Extended r
MIP.Finite Integer
rhs2 }
        Op
PBFile.Eq -> Constraint Integer
forall a. Default a => a
def{ constrExpr :: Expr Integer
MIP.constrExpr = Expr Integer
lhs2, constrLB :: BoundExpr Integer
MIP.constrLB = Integer -> BoundExpr Integer
forall r. r -> Extended r
MIP.Finite Integer
rhs2, constrUB :: BoundExpr Integer
MIP.constrUB = Integer -> BoundExpr Integer
forall r. r -> Extended r
MIP.Finite Integer
rhs2 }


convExpr :: PBFile.Sum -> MIP.Expr Integer
convExpr :: Sum -> Expr Integer
convExpr Sum
s = [Expr Integer] -> Expr Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [[Expr Integer] -> Expr Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product (Integer -> Expr Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
w Expr Integer -> [Expr Integer] -> [Expr Integer]
forall a. a -> [a] -> [a]
: (Int -> Expr Integer) -> [Int] -> [Expr Integer]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Expr Integer
f [Int]
tm) | (Integer
w,[Int]
tm) <- Sum
s]
  where
    f :: PBFile.Lit -> MIP.Expr Integer
    f :: Int -> Expr Integer
f Int
x
      | Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0     = Var -> Expr Integer
forall c. Num c => Var -> Expr c
MIP.varExpr (Int -> Var
convVar Int
x)
      | Bool
otherwise = Expr Integer
1 Expr Integer -> Expr Integer -> Expr Integer
forall a. Num a => a -> a -> a
- Var -> Expr Integer
forall c. Num c => Var -> Expr c
MIP.varExpr (Int -> Var
convVar (Int -> Int
forall a. Num a => a -> a
abs Int
x))

convVar :: PBFile.Var -> MIP.Var
convVar :: Int -> Var
convVar Int
x = String -> Var
MIP.toVar (String
"x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x)

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

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

instance Transformer WBO2IPInfo where
  type Source WBO2IPInfo = SAT.Model
  type Target WBO2IPInfo = Map MIP.Var Rational

instance ForwardTransformer WBO2IPInfo where
  transformForward :: WBO2IPInfo -> Source WBO2IPInfo -> Target WBO2IPInfo
transformForward (WBO2IPInfo Int
_nv [(Var, SoftConstraint)]
relaxVariables) Source WBO2IPInfo
m = Map Var Rational -> Map Var Rational -> Map Var Rational
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Var Rational
m1 Map Var Rational
m2
      where
        m1 :: Map Var Rational
m1 = [(Var, Rational)] -> Map Var Rational
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Var, Rational)] -> Map Var Rational)
-> [(Var, Rational)] -> Map Var Rational
forall a b. (a -> b) -> a -> b
$ [(Int -> Var
convVar Int
v, if Bool
val then Rational
1 else Rational
0) | (Int
v,Bool
val) <- UArray Int Bool -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Int Bool
Source WBO2IPInfo
m]
        m2 :: Map Var Rational
m2 = [(Var, Rational)] -> Map Var Rational
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Var, Rational)] -> Map Var Rational)
-> [(Var, Rational)] -> Map Var Rational
forall a b. (a -> b) -> a -> b
$ [(Var
v, if UArray Int Bool -> (Sum, Op, Integer) -> Bool
forall m. IModel m => m -> (Sum, Op, Integer) -> Bool
SAT.evalPBConstraint UArray Int Bool
Source WBO2IPInfo
m (Sum, Op, Integer)
c then Rational
0 else Rational
1) | (Var
v, (Just Integer
_, (Sum, Op, Integer)
c)) <- [(Var, SoftConstraint)]
relaxVariables]

instance BackwardTransformer WBO2IPInfo where
  transformBackward :: WBO2IPInfo -> Target WBO2IPInfo -> Source WBO2IPInfo
transformBackward (WBO2IPInfo Int
nv [(Var, SoftConstraint)]
_relaxVariables) = Int -> Map Var Rational -> UArray Int Bool
mtrans Int
nv

wbo2ip :: Bool -> PBFile.SoftFormula -> (MIP.Problem Integer, WBO2IPInfo)
wbo2ip :: Bool -> SoftFormula -> (Problem Integer, WBO2IPInfo)
wbo2ip Bool
useIndicator SoftFormula
formula = (Problem Integer
mip, Int -> [(Var, SoftConstraint)] -> WBO2IPInfo
WBO2IPInfo (SoftFormula -> Int
PBFile.wboNumVars SoftFormula
formula) [(Var, SoftConstraint)]
relaxVariables)
  where
    mip :: Problem Integer
mip = Problem Integer
forall a. Default a => a
def
      { objectiveFunction :: ObjectiveFunction Integer
MIP.objectiveFunction = ObjectiveFunction Integer
obj2
      , constraints :: [Constraint Integer]
MIP.constraints = [Constraint Integer]
topConstr [Constraint Integer]
-> [Constraint Integer] -> [Constraint Integer]
forall a. [a] -> [a] -> [a]
++ (([(Integer, Var)], Constraint Integer) -> Constraint Integer)
-> [([(Integer, Var)], Constraint Integer)] -> [Constraint Integer]
forall a b. (a -> b) -> [a] -> [b]
map ([(Integer, Var)], Constraint Integer) -> Constraint Integer
forall a b. (a, b) -> b
snd [([(Integer, Var)], Constraint Integer)]
cs2
      , varType :: Map Var VarType
MIP.varType = [(Var, VarType)] -> Map Var VarType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var
v, VarType
MIP.IntegerVariable) | Var
v <- [Var]
vs]
      , varBounds :: Map Var (Bounds Integer)
MIP.varBounds = [(Var, Bounds Integer)] -> Map Var (Bounds Integer)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var
v, (BoundExpr Integer
0,BoundExpr Integer
1)) | Var
v <- [Var]
vs]
      }

    vs :: [Var]
vs = [Int -> Var
convVar Int
v | Int
v <- [Int
1..SoftFormula -> Int
PBFile.wboNumVars SoftFormula
formula]] [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var
v | ([(Integer, Var)]
ts, Constraint Integer
_) <- [([(Integer, Var)], Constraint Integer)]
cs2, (Integer
_, Var
v) <- [(Integer, Var)]
ts]

    obj2 :: ObjectiveFunction Integer
obj2 = ObjectiveFunction Any
forall a. Default a => a
def
      { objDir :: OptDir
MIP.objDir = OptDir
MIP.OptMin
      , objExpr :: Expr Integer
MIP.objExpr = [Term Integer] -> Expr Integer
forall c. [Term c] -> Expr c
MIP.Expr [Integer -> [Var] -> Term Integer
forall c. c -> [Var] -> Term c
MIP.Term Integer
w [Var
v] | ([(Integer, Var)]
ts, Constraint Integer
_) <- [([(Integer, Var)], Constraint Integer)]
cs2, (Integer
w, Var
v) <- [(Integer, Var)]
ts]
      }

    topConstr :: [MIP.Constraint Integer]
    topConstr :: [Constraint Integer]
topConstr =
     case SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
formula of
       Maybe Integer
Nothing -> []
       Just Integer
t ->
          [ Constraint Integer
forall a. Default a => a
def{ constrExpr :: Expr Integer
MIP.constrExpr = ObjectiveFunction Integer -> Expr Integer
forall c. ObjectiveFunction c -> Expr c
MIP.objExpr ObjectiveFunction Integer
obj2, constrUB :: BoundExpr Integer
MIP.constrUB = Integer -> BoundExpr Integer
forall r. r -> Extended r
MIP.Finite (Integer -> Integer
forall a. Num a => Integer -> a
fromInteger Integer
t Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) } ]

    relaxVariables :: [(MIP.Var, PBFile.SoftConstraint)]
    relaxVariables :: [(Var, SoftConstraint)]
relaxVariables = [(String -> Var
MIP.toVar (String
"r" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n), SoftConstraint
c) | (Int
n, SoftConstraint
c) <- [Int] -> [SoftConstraint] -> [(Int, SoftConstraint)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
0::Int)..] (SoftFormula -> [SoftConstraint]
PBFile.wboConstraints SoftFormula
formula)]

    cs2 :: [([(Integer, MIP.Var)], MIP.Constraint Integer)]
    cs2 :: [([(Integer, Var)], Constraint Integer)]
cs2 = do
      (Var
v, (Maybe Integer
w, (Sum
lhs,Op
op,Integer
rhs))) <- [(Var, SoftConstraint)]
relaxVariables
      let (Expr Integer
lhs2,Integer
c) = Expr Integer -> (Expr Integer, Integer)
splitConst (Expr Integer -> (Expr Integer, Integer))
-> Expr Integer -> (Expr Integer, Integer)
forall a b. (a -> b) -> a -> b
$ Sum -> Expr Integer
convExpr Sum
lhs
          rhs2 :: Integer
rhs2 = Integer
rhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
c
          ([(Integer, Var)]
ts,Maybe (Var, Integer)
ind) =
            case Maybe Integer
w of
              Maybe Integer
Nothing -> ([], Maybe (Var, Integer)
forall a. Maybe a
Nothing)
              Just Integer
w2 -> ([(Integer
w2,Var
v)], (Var, Integer) -> Maybe (Var, Integer)
forall a. a -> Maybe a
Just (Var
v,Integer
0))
      if Maybe Integer -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Integer
w Bool -> Bool -> Bool
|| Bool
useIndicator then do
         let c :: Constraint Integer
c =
               case Op
op of
                 Op
PBFile.Ge -> (Expr Integer
lhs2 Expr Integer -> Expr Integer -> Constraint Integer
forall c. Num c => Expr c -> Expr c -> Constraint c
.>=. Integer -> Expr Integer
forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr Integer
rhs2) { constrIndicator :: Maybe (Var, Integer)
MIP.constrIndicator = Maybe (Var, Integer)
ind }
                 Op
PBFile.Eq -> (Expr Integer
lhs2 Expr Integer -> Expr Integer -> Constraint Integer
forall c. Num c => Expr c -> Expr c -> Constraint c
.==. Integer -> Expr Integer
forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr Integer
rhs2) { constrIndicator :: Maybe (Var, Integer)
MIP.constrIndicator = Maybe (Var, Integer)
ind }
         ([(Integer, Var)], Constraint Integer)
-> [([(Integer, Var)], Constraint Integer)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Integer, Var)]
ts, Constraint Integer
c)
      else do
         let (Expr Integer
lhsGE,Integer
rhsGE) = Var -> (Expr Integer, Integer) -> (Expr Integer, Integer)
relaxGE Var
v (Expr Integer
lhs2,Integer
rhs2)
             c1 :: Constraint Integer
c1 = Expr Integer
lhsGE Expr Integer -> Expr Integer -> Constraint Integer
forall c. Num c => Expr c -> Expr c -> Constraint c
.>=. Integer -> Expr Integer
forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr Integer
rhsGE
         case Op
op of
           Op
PBFile.Ge -> do
             ([(Integer, Var)], Constraint Integer)
-> [([(Integer, Var)], Constraint Integer)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Integer, Var)]
ts, Constraint Integer
c1)
           Op
PBFile.Eq -> do
             let (Expr Integer
lhsLE,Integer
rhsLE) = Var -> (Expr Integer, Integer) -> (Expr Integer, Integer)
relaxLE Var
v (Expr Integer
lhs2,Integer
rhs2)
                 c2 :: Constraint Integer
c2 = Expr Integer
lhsLE Expr Integer -> Expr Integer -> Constraint Integer
forall c. Num c => Expr c -> Expr c -> Constraint c
.<=. Integer -> Expr Integer
forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr Integer
rhsLE
             [ ([(Integer, Var)]
ts, Constraint Integer
c1), ([], Constraint Integer
c2) ]

splitConst :: MIP.Expr Integer -> (MIP.Expr Integer, Integer)
splitConst :: Expr Integer -> (Expr Integer, Integer)
splitConst Expr Integer
e = (Expr Integer
e2, Integer
c)
  where
    e2 :: Expr Integer
e2 = [Term Integer] -> Expr Integer
forall c. [Term c] -> Expr c
MIP.Expr [Term Integer
t | t :: Term Integer
t@(MIP.Term Integer
_ (Var
_:[Var]
_)) <- Expr Integer -> [Term Integer]
forall c. Expr c -> [Term c]
MIP.terms Expr Integer
e]
    c :: Integer
c = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
c | MIP.Term Integer
c [] <- Expr Integer -> [Term Integer]
forall c. Expr c -> [Term c]
MIP.terms Expr Integer
e]

relaxGE :: MIP.Var -> (MIP.Expr Integer, Integer) -> (MIP.Expr Integer, Integer)
relaxGE :: Var -> (Expr Integer, Integer) -> (Expr Integer, Integer)
relaxGE Var
v (Expr Integer
lhs, Integer
rhs) = (Integer -> Expr Integer
forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr (Integer
rhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lhs_lb) Expr Integer -> Expr Integer -> Expr Integer
forall a. Num a => a -> a -> a
* Var -> Expr Integer
forall c. Num c => Var -> Expr c
MIP.varExpr Var
v Expr Integer -> Expr Integer -> Expr Integer
forall a. Num a => a -> a -> a
+ Expr Integer
lhs, Integer
rhs)
  where
    lhs_lb :: Integer
lhs_lb = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
c Integer
0 | MIP.Term Integer
c [Var]
_ <- Expr Integer -> [Term Integer]
forall c. Expr c -> [Term c]
MIP.terms Expr Integer
lhs]

relaxLE :: MIP.Var -> (MIP.Expr Integer, Integer) -> (MIP.Expr Integer, Integer)
relaxLE :: Var -> (Expr Integer, Integer) -> (Expr Integer, Integer)
relaxLE Var
v (Expr Integer
lhs, Integer
rhs) = (Integer -> Expr Integer
forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr (Integer
rhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lhs_ub) Expr Integer -> Expr Integer -> Expr Integer
forall a. Num a => a -> a -> a
* Var -> Expr Integer
forall c. Num c => Var -> Expr c
MIP.varExpr Var
v Expr Integer -> Expr Integer -> Expr Integer
forall a. Num a => a -> a -> a
+ Expr Integer
lhs, Integer
rhs)
  where
    lhs_ub :: Integer
lhs_ub = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
c Integer
0 | MIP.Term Integer
c [Var]
_ <- Expr Integer -> [Term Integer]
forall c. Expr c -> [Term c]
MIP.terms Expr Integer
lhs]

mtrans :: Int -> Map MIP.Var Rational -> SAT.Model
mtrans :: Int -> Map Var Rational -> UArray Int Bool
mtrans Int
nvar Map Var Rational
m =
  (Int, Int) -> [(Int, Bool)] -> UArray Int Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1, Int
nvar)
    [ (Int
i, Bool
val)
    | Int
i <- [Int
1 .. Int
nvar]
    , let val :: Bool
val =
            case Rational -> Var -> Map Var Rational -> Rational
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Rational
0 (Int -> Var
convVar Int
i) Map Var Rational
m of
              Rational
0  -> Bool
False
              Rational
1  -> Bool
True
              Rational
v0 -> String -> Bool
forall a. HasCallStack => String -> a
error (Rational -> String
forall a. Show a => a -> String
show Rational
v0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is neither 0 nor 1")
    ]

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

type SAT2IPInfo = ComposedTransformer SAT2PBInfo PB2IPInfo

sat2ip :: CNF.CNF -> (MIP.Problem Integer, SAT2IPInfo)
sat2ip :: CNF -> (Problem Integer, SAT2IPInfo)
sat2ip CNF
cnf = (Problem Integer
ip, SAT2PBInfo -> PB2IPInfo -> SAT2IPInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SAT2PBInfo
info1 PB2IPInfo
info2)
  where
    (Formula
pb,SAT2PBInfo
info1) = CNF -> (Formula, SAT2PBInfo)
sat2pb CNF
cnf
    (Problem Integer
ip,PB2IPInfo
info2) = Formula -> (Problem Integer, PB2IPInfo)
pb2ip Formula
pb

type MaxSAT2IPInfo = ComposedTransformer MaxSAT2WBOInfo WBO2IPInfo

maxsat2ip :: Bool -> CNF.WCNF -> (MIP.Problem Integer, MaxSAT2IPInfo)
maxsat2ip :: Bool -> WCNF -> (Problem Integer, MaxSAT2IPInfo)
maxsat2ip Bool
useIndicator WCNF
wcnf = (Problem Integer
ip, SAT2PBInfo -> WBO2IPInfo -> MaxSAT2IPInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer SAT2PBInfo
info1 WBO2IPInfo
info2)
  where
    (SoftFormula
wbo, SAT2PBInfo
info1) = WCNF -> (SoftFormula, SAT2PBInfo)
maxsat2wbo WCNF
wcnf
    (Problem Integer
ip, WBO2IPInfo
info2) = Bool -> SoftFormula -> (Problem Integer, WBO2IPInfo)
wbo2ip Bool
useIndicator SoftFormula
wbo

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