{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.MIP
-- Copyright   :  (c) Masahiro Sakai 2011-2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.Converter.MIP
  (
  -- * PB/WBO to IP
    pb2ip
  , PB2IPInfo
  , wbo2ip
  , WBO2IPInfo

  -- * SAT/Max-SAT to IP
  , sat2ip
  , SAT2IPInfo
  , maxsat2ip
  , MaxSAT2IPInfo

  -- * IP to PB
  , ip2pb
  , IP2PBInfo (..)
  , addMIP
  ) where

import Control.Monad
import Control.Monad.Primitive
import Control.Monad.ST
import Control.Monad.Trans
import Control.Monad.Trans.Except
import qualified Data.Aeson as J
import qualified Data.Aeson.Types as J
#if MIN_VERSION_aeson(2,0,0)
import qualified Data.Aeson.Key as Key
#endif
import Data.Aeson ((.=), (.:))
import Data.Array.IArray
import Data.Default.Class
import qualified Data.IntSet as IntSet
import Data.List (intercalate, foldl', sortBy)
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Ord
import Data.Primitive.MutVar
import Data.Ratio
import qualified Data.Set as Set
import Data.String
import qualified Data.Text as T
import Data.VectorSpace

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

import ToySolver.Converter.Base
import ToySolver.Converter.PB
import ToySolver.Data.OrdRel
import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.Internal.JSON
import ToySolver.SAT.Internal.JSON
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)

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

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
$c== :: PB2IPInfo -> PB2IPInfo -> Bool
== :: PB2IPInfo -> PB2IPInfo -> Bool
$c/= :: PB2IPInfo -> PB2IPInfo -> Bool
/= :: PB2IPInfo -> PB2IPInfo -> Bool
Eq, Var -> PB2IPInfo -> ShowS
[PB2IPInfo] -> ShowS
PB2IPInfo -> [Char]
(Var -> PB2IPInfo -> ShowS)
-> (PB2IPInfo -> [Char])
-> ([PB2IPInfo] -> ShowS)
-> Show PB2IPInfo
forall a.
(Var -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Var -> PB2IPInfo -> ShowS
showsPrec :: Var -> PB2IPInfo -> ShowS
$cshow :: PB2IPInfo -> [Char]
show :: PB2IPInfo -> [Char]
$cshowList :: [PB2IPInfo] -> ShowS
showList :: [PB2IPInfo] -> ShowS
Show, ReadPrec [PB2IPInfo]
ReadPrec PB2IPInfo
Var -> ReadS PB2IPInfo
ReadS [PB2IPInfo]
(Var -> ReadS PB2IPInfo)
-> ReadS [PB2IPInfo]
-> ReadPrec PB2IPInfo
-> ReadPrec [PB2IPInfo]
-> Read PB2IPInfo
forall a.
(Var -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Var -> ReadS PB2IPInfo
readsPrec :: Var -> ReadS PB2IPInfo
$creadList :: ReadS [PB2IPInfo]
readList :: ReadS [PB2IPInfo]
$creadPrec :: ReadPrec PB2IPInfo
readPrec :: ReadPrec PB2IPInfo
$creadListPrec :: ReadPrec [PB2IPInfo]
readListPrec :: ReadPrec [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 [(Var -> Var
convVar Var
v, if Bool
val then Rational
1 else Rational
0) | (Var
v,Bool
val) <- UArray Var Bool -> [(Var, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Var Bool
Source PB2IPInfo
m]

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

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

instance ObjValueForwardTransformer PB2IPInfo where
  transformObjValueForward :: PB2IPInfo -> SourceObjValue PB2IPInfo -> TargetObjValue PB2IPInfo
transformObjValueForward PB2IPInfo
_ = Integer -> Rational
SourceObjValue PB2IPInfo -> TargetObjValue PB2IPInfo
forall a b. (Integral a, Num b) => a -> b
fromIntegral

instance ObjValueBackwardTransformer PB2IPInfo where
  transformObjValueBackward :: PB2IPInfo -> TargetObjValue PB2IPInfo -> SourceObjValue PB2IPInfo
transformObjValueBackward PB2IPInfo
_ = Rational -> Integer
TargetObjValue PB2IPInfo -> SourceObjValue PB2IPInfo
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
round

instance J.ToJSON PB2IPInfo where
  toJSON :: PB2IPInfo -> Value
toJSON (PB2IPInfo Var
nv) =
    [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"PB2IPInfo" :: J.Value)
    , Key
"num_original_variables" Key -> Var -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Var
nv
    ]

instance J.FromJSON PB2IPInfo where
  parseJSON :: Value -> Parser PB2IPInfo
parseJSON =
    [Char] -> (Object -> Parser PB2IPInfo) -> Value -> Parser PB2IPInfo
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withTypedObject [Char]
"PB2IPInfo" ((Object -> Parser PB2IPInfo) -> Value -> Parser PB2IPInfo)
-> (Object -> Parser PB2IPInfo) -> Value -> Parser PB2IPInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
      Var -> PB2IPInfo
PB2IPInfo (Var -> PB2IPInfo) -> Parser Var -> Parser PB2IPInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Var
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_original_variables"

pb2ip :: PBFile.Formula -> (MIP.Problem Integer, PB2IPInfo)
pb2ip :: Formula -> (Problem Integer, PB2IPInfo)
pb2ip Formula
formula = (Problem Integer
mip, Var -> PB2IPInfo
PB2IPInfo (Formula -> Var
PBFile.pbNumVars Formula
formula))
  where
    mip :: Problem Integer
mip = Problem Integer
forall a. Default a => a
def
      { MIP.objectiveFunction = obj2
      , MIP.constraints = cs2
      , MIP.varDomains = Map.fromList [(v, (MIP.IntegerVariable, (0,1))) | v <- vs]
      }

    vs :: [Var]
vs = [Var -> Var
convVar Var
v | Var
v <- [Var
1..Formula -> Var
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{ MIP.objDir = MIP.OptMin, MIP.objExpr = convExpr obj' }
        Maybe Sum
Nothing   -> ObjectiveFunction Any
forall a. Default a => a
def{ MIP.objDir = MIP.OptMin, MIP.objExpr = 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 a. a -> [a]
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{ MIP.constrExpr = lhs2, MIP.constrLB = MIP.Finite rhs2 }
        Op
PBFile.Eq -> Constraint Integer
forall a. Default a => a
def{ MIP.constrExpr = lhs2, MIP.constrLB = MIP.Finite rhs2, MIP.constrUB = MIP.Finite rhs2 }


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

convVar :: PBFile.Var -> MIP.Var
convVar :: Var -> Var
convVar Var
x = [Char] -> Var
forall a. IsString a => [Char] -> a
fromString ([Char]
"x" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Show a => a -> [Char]
show Var
x)

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

data WBO2IPInfo = WBO2IPInfo !Int [(MIP.Var, PBFile.Constraint)]
  deriving (WBO2IPInfo -> WBO2IPInfo -> Bool
(WBO2IPInfo -> WBO2IPInfo -> Bool)
-> (WBO2IPInfo -> WBO2IPInfo -> Bool) -> Eq WBO2IPInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WBO2IPInfo -> WBO2IPInfo -> Bool
== :: WBO2IPInfo -> WBO2IPInfo -> Bool
$c/= :: WBO2IPInfo -> WBO2IPInfo -> Bool
/= :: WBO2IPInfo -> WBO2IPInfo -> Bool
Eq, Var -> WBO2IPInfo -> ShowS
[WBO2IPInfo] -> ShowS
WBO2IPInfo -> [Char]
(Var -> WBO2IPInfo -> ShowS)
-> (WBO2IPInfo -> [Char])
-> ([WBO2IPInfo] -> ShowS)
-> Show WBO2IPInfo
forall a.
(Var -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Var -> WBO2IPInfo -> ShowS
showsPrec :: Var -> WBO2IPInfo -> ShowS
$cshow :: WBO2IPInfo -> [Char]
show :: WBO2IPInfo -> [Char]
$cshowList :: [WBO2IPInfo] -> ShowS
showList :: [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 Var
_nv [(Var, (Sum, Op, Integer))]
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
$ [(Var -> Var
convVar Var
v, if Bool
val then Rational
1 else Rational
0) | (Var
v,Bool
val) <- UArray Var Bool -> [(Var, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Var 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 Var Bool -> (Sum, Op, Integer) -> Bool
forall m. IModel m => m -> (Sum, Op, Integer) -> Bool
SAT.evalPBConstraint UArray Var Bool
Source WBO2IPInfo
m (Sum, Op, Integer)
c then Rational
0 else Rational
1) | (Var
v, (Sum, Op, Integer)
c) <- [(Var, (Sum, Op, Integer))]
relaxVariables]

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

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

instance ObjValueForwardTransformer WBO2IPInfo where
  transformObjValueForward :: WBO2IPInfo
-> SourceObjValue WBO2IPInfo -> TargetObjValue WBO2IPInfo
transformObjValueForward WBO2IPInfo
_ = Integer -> Rational
SourceObjValue WBO2IPInfo -> TargetObjValue WBO2IPInfo
forall a b. (Integral a, Num b) => a -> b
fromIntegral

instance ObjValueBackwardTransformer WBO2IPInfo where
  transformObjValueBackward :: WBO2IPInfo
-> TargetObjValue WBO2IPInfo -> SourceObjValue WBO2IPInfo
transformObjValueBackward WBO2IPInfo
_ = Rational -> Integer
TargetObjValue WBO2IPInfo -> SourceObjValue WBO2IPInfo
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
round

instance J.ToJSON WBO2IPInfo where
  toJSON :: WBO2IPInfo -> Value
toJSON (WBO2IPInfo Var
nv [(Var, (Sum, Op, Integer))]
relaxVariables) =
    [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"WBO2IPInfo" :: J.Value)
    , Key
"num_original_variables" Key -> Var -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Var
nv
    , Key
"relax_variables" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Pair] -> Value
J.object
        [ Text -> Key
toKey (Var -> Text
MIP.varName Var
v) Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Sum, Op, Integer) -> Value
jPBConstraint (Sum, Op, Integer)
constr
        | (Var
v, (Sum, Op, Integer)
constr) <- [(Var, (Sum, Op, Integer))]
relaxVariables
        ]
    ]
    where
#if MIN_VERSION_aeson(2,0,0)
      toKey :: Text -> Key
toKey = Text -> Key
Key.fromText
#else
      toKey = id
#endif

instance J.FromJSON WBO2IPInfo where
  parseJSON :: Value -> Parser WBO2IPInfo
parseJSON =
    [Char]
-> (Object -> Parser WBO2IPInfo) -> Value -> Parser WBO2IPInfo
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withTypedObject [Char]
"WBO2IPInfo" ((Object -> Parser WBO2IPInfo) -> Value -> Parser WBO2IPInfo)
-> (Object -> Parser WBO2IPInfo) -> Value -> Parser WBO2IPInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
      Map Text Value
xs <- Object
obj Object -> Key -> Parser (Map Text Value)
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"relax_variables"
      Var -> [(Var, (Sum, Op, Integer))] -> WBO2IPInfo
WBO2IPInfo
        (Var -> [(Var, (Sum, Op, Integer))] -> WBO2IPInfo)
-> Parser Var -> Parser ([(Var, (Sum, Op, Integer))] -> WBO2IPInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Var
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_original_variables"
        Parser ([(Var, (Sum, Op, Integer))] -> WBO2IPInfo)
-> Parser [(Var, (Sum, Op, Integer))] -> Parser WBO2IPInfo
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Text, Value) -> Parser (Var, (Sum, Op, Integer)))
-> [(Text, Value)] -> Parser [(Var, (Sum, Op, Integer))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Text, Value) -> Parser (Var, (Sum, Op, Integer))
f (Map Text Value -> [(Text, Value)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Text Value
xs)
    where
      f :: (T.Text, J.Value) -> J.Parser (MIP.Var, PBFile.Constraint)
      f :: (Text, Value) -> Parser (Var, (Sum, Op, Integer))
f (Text
name, Value
val) = do
        (Sum, Op, Integer)
constr <- Value -> Parser (Sum, Op, Integer)
parsePBConstraint Value
val
        (Var, (Sum, Op, Integer)) -> Parser (Var, (Sum, Op, Integer))
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Var
MIP.Var Text
name, (Sum, Op, Integer)
constr)

wbo2ip :: Bool -> PBFile.SoftFormula -> (MIP.Problem Integer, WBO2IPInfo)
wbo2ip :: Bool -> SoftFormula -> (Problem Integer, WBO2IPInfo)
wbo2ip Bool
useIndicator SoftFormula
formula = (Problem Integer
mip, Var -> [(Var, (Sum, Op, Integer))] -> WBO2IPInfo
WBO2IPInfo (SoftFormula -> Var
PBFile.wboNumVars SoftFormula
formula) [(Var
r, (Sum, Op, Integer)
c) | (Var
r, (Just Integer
_, (Sum, Op, Integer)
c)) <- [(Var, SoftConstraint)]
relaxVariables])
  where
    mip :: Problem Integer
mip = Problem Integer
forall a. Default a => a
def
      { MIP.objectiveFunction = obj2
      , MIP.constraints = topConstr ++ map snd cs2
      , MIP.varDomains = Map.fromList [(v, (MIP.IntegerVariable, (0,1))) | v <- vs]
      }

    vs :: [Var]
vs = [Var -> Var
convVar Var
v | Var
v <- [Var
1..SoftFormula -> Var
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
      { MIP.objDir = MIP.OptMin
      , MIP.objExpr = MIP.Expr [MIP.Term w [v] | (ts, _) <- cs2, (w, v) <- 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{ MIP.constrExpr = MIP.objExpr obj2, MIP.constrUB = MIP.Finite (fromInteger t - 1) } ]

    relaxVariables :: [(MIP.Var, PBFile.SoftConstraint)]
    relaxVariables :: [(Var, SoftConstraint)]
relaxVariables = [([Char] -> Var
forall a. IsString a => [Char] -> a
fromString ([Char]
"r" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Show a => a -> [Char]
show Var
n), SoftConstraint
c) | (Var
n, SoftConstraint
c) <- [Var] -> [SoftConstraint] -> [(Var, SoftConstraint)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Var
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
MIP..>=. Integer -> Expr Integer
forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr Integer
rhs2) { MIP.constrIndicator = ind }
                 Op
PBFile.Eq -> (Expr Integer
lhs2 Expr Integer -> Expr Integer -> Constraint Integer
forall c. Num c => Expr c -> Expr c -> Constraint c
MIP..==. Integer -> Expr Integer
forall c. (Eq c, Num c) => c -> Expr c
MIP.constExpr Integer
rhs2) { MIP.constrIndicator = ind }
         ([(Integer, Var)], Constraint Integer)
-> [([(Integer, Var)], Constraint Integer)]
forall a. a -> [a]
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
MIP..>=. 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 a. a -> [a]
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
MIP..<=. 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 a. Num a => [a] -> a
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 a. Num a => [a] -> a
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 a. Num a => [a] -> a
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 :: Var -> Map Var Rational -> UArray Var Bool
mtrans Var
nvar Map Var Rational
m =
  (Var, Var) -> [(Var, Bool)] -> UArray Var Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Var
1, Var
nvar)
    [ (Var
i, Bool
val)
    | Var
i <- [Var
1 .. Var
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 (Var -> Var
convVar Var
i) Map Var Rational
m of
              Rational
0  -> Bool
False
              Rational
1  -> Bool
True
              Rational
v0 -> [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error (Rational -> [Char]
forall a. Show a => a -> [Char]
show Rational
v0 [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" 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, MaxSAT2WBOInfo -> WBO2IPInfo -> MaxSAT2IPInfo
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer MaxSAT2WBOInfo
info1 WBO2IPInfo
info2)
  where
    (SoftFormula
wbo, MaxSAT2WBOInfo
info1) = WCNF -> (SoftFormula, MaxSAT2WBOInfo)
maxsat2wbo WCNF
wcnf
    (Problem Integer
ip, WBO2IPInfo
info2) = Bool -> SoftFormula -> (Problem Integer, WBO2IPInfo)
wbo2ip Bool
useIndicator SoftFormula
wbo

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

ip2pb :: MIP.Problem Rational -> Either String (PBFile.Formula, IP2PBInfo)
ip2pb :: Problem Rational -> Either [Char] (Formula, IP2PBInfo)
ip2pb Problem Rational
mip = (forall s. ST s (Either [Char] (Formula, IP2PBInfo)))
-> Either [Char] (Formula, IP2PBInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Either [Char] (Formula, IP2PBInfo)))
 -> Either [Char] (Formula, IP2PBInfo))
-> (forall s. ST s (Either [Char] (Formula, IP2PBInfo)))
-> Either [Char] (Formula, IP2PBInfo)
forall a b. (a -> b) -> a -> b
$ ExceptT [Char] (ST s) (Formula, IP2PBInfo)
-> ST s (Either [Char] (Formula, IP2PBInfo))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT [Char] (ST s) (Formula, IP2PBInfo)
 -> ST s (Either [Char] (Formula, IP2PBInfo)))
-> ExceptT [Char] (ST s) (Formula, IP2PBInfo)
-> ST s (Either [Char] (Formula, IP2PBInfo))
forall a b. (a -> b) -> a -> b
$ ExceptT [Char] (ST s) (Formula, IP2PBInfo)
forall s. ExceptT [Char] (ST s) (Formula, IP2PBInfo)
m
  where
    m :: ExceptT String (ST s) (PBFile.Formula, IP2PBInfo)
    m :: forall s. ExceptT [Char] (ST s) (Formula, IP2PBInfo)
m = do
      PBStore (ST s)
db <- ST s (PBStore (ST s)) -> ExceptT [Char] (ST s) (PBStore (ST s))
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ST s (PBStore (ST s)) -> ExceptT [Char] (ST s) (PBStore (ST s)))
-> ST s (PBStore (ST s)) -> ExceptT [Char] (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 Sum
obj, IP2PBInfo
info) <- PBStore (ST s)
-> Problem Rational -> ExceptT [Char] (ST s) (Expr, IP2PBInfo)
forall (m :: * -> *) enc.
(AddPBNL m enc, PrimMonad m) =>
enc -> Problem Rational -> ExceptT [Char] m (Expr, IP2PBInfo)
addMIP' PBStore (ST s)
db Problem Rational
mip
      Formula
formula <- ST s Formula -> ExceptT [Char] (ST s) Formula
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ST s Formula -> ExceptT [Char] (ST s) Formula)
-> ST s Formula -> ExceptT [Char] (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, IP2PBInfo) -> ExceptT [Char] (ST s) (Formula, IP2PBInfo)
forall a. a -> ExceptT [Char] (ST s) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Formula, IP2PBInfo)
 -> ExceptT [Char] (ST s) (Formula, IP2PBInfo))
-> (Formula, IP2PBInfo)
-> ExceptT [Char] (ST s) (Formula, IP2PBInfo)
forall a b. (a -> b) -> a -> b
$ (Formula
formula{ PBFile.pbObjectiveFunction = Just obj }, IP2PBInfo
info)

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

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

instance ForwardTransformer IP2PBInfo where
  transformForward :: IP2PBInfo -> Source IP2PBInfo -> Target IP2PBInfo
transformForward (IP2PBInfo Map Var Expr
vmap Map Var Var
nonZeroTable Integer
_d) Source IP2PBInfo
sol
    | Map Var Expr -> Set Var
forall k a. Map k a -> Set k
Map.keysSet Map Var Expr
vmap Set Var -> Set Var -> Bool
forall a. Eq a => a -> a -> Bool
/= Map Var Rational -> Set Var
forall k a. Map k a -> Set k
Map.keysSet Map Var Rational
Source IP2PBInfo
sol = [Char] -> UArray Var Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"variables mismatch"
    | Bool
otherwise = (Var, Var) -> [(Var, Bool)] -> UArray Var Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Var
1, Var
x_max) ([(Var, Bool)] -> UArray Var Bool)
-> [(Var, Bool)] -> UArray Var Bool
forall a b. (a -> b) -> a -> b
$
        [(Var
x, Bool
val) | (Var
var, Integer.Expr Sum
s) <- Map Var Expr -> [(Var, Expr)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Var Expr
vmap, (Var
x, Bool
val) <- Sum -> Rational -> [(Var, Bool)]
f Sum
s (Map Var Rational
Source IP2PBInfo
sol Map Var Rational -> Var -> Rational
forall k a. Ord k => Map k a -> k -> a
Map.! Var
var)] [(Var, Bool)] -> [(Var, Bool)] -> [(Var, Bool)]
forall a. [a] -> [a] -> [a]
++
        [(Var
y, (Map Var Rational
Source IP2PBInfo
sol Map Var Rational -> Var -> Rational
forall k a. Ord k => Map k a -> k -> a
Map.! Var
var) Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
/= Rational
0) | (Var
var, Var
y) <- Map Var Var -> [(Var, Var)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Var Var
nonZeroTable]
    where
      x_max :: SAT.Var
      x_max :: Var
x_max = IntSet -> Var
IntSet.findMax IntSet
xs
        where
          xs :: IntSet
xs = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions ([IntSet] -> IntSet) -> [IntSet] -> IntSet
forall a b. (a -> b) -> a -> b
$
               [[Var] -> IntSet
IntSet.fromList ((Var -> Var) -> [Var] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Var
SAT.litVar [Var]
lits) | Integer.Expr Sum
s <- Map Var Expr -> [Expr]
forall k a. Map k a -> [a]
Map.elems Map Var Expr
vmap, (Integer
_, [Var]
lits) <- Sum
s] [IntSet] -> [IntSet] -> [IntSet]
forall a. [a] -> [a] -> [a]
++
               [[Var] -> IntSet
IntSet.fromList ((Var -> Var) -> [Var] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Var
SAT.litVar (Map Var Var -> [Var]
forall k a. Map k a -> [a]
Map.elems Map Var Var
nonZeroTable))] [IntSet] -> [IntSet] -> [IntSet]
forall a. [a] -> [a] -> [a]
++
               [Var -> IntSet
IntSet.singleton Var
0]

      f :: SAT.PBSum -> Rational -> [(SAT.Var, Bool)]
      f :: Sum -> Rational -> [(Var, Bool)]
f Sum
s Rational
val
        | Rational -> Integer
forall a. Ratio a -> a
denominator Rational
val Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
1 = [Char] -> [(Var, Bool)]
forall a. HasCallStack => [Char] -> a
error [Char]
"value should be integer"
        | Bool
otherwise = Integer -> [(Integer, Var)] -> [(Var, Bool)]
g (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
val Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer
c | (Integer
c, []) <- Sum
s]) (Map Integer Var -> [(Integer, Var)]
forall k a. Map k a -> [(k, a)]
Map.toDescList Map Integer Var
tmp)
        where
          tmp :: Map Integer SAT.Var
          tmp :: Map Integer Var
tmp =
            [(Integer, Var)] -> Map Integer Var
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
            [ if Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then
                [Char] -> (Integer, Var)
forall a. HasCallStack => [Char] -> a
error [Char]
"coefficient should be non-negative"
              else if [Var] -> Var
forall a. [a] -> Var
forall (t :: * -> *) a. Foldable t => t a -> Var
length [Var]
ls Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
> Var
1 then
                [Char] -> (Integer, Var)
forall a. HasCallStack => [Char] -> a
error [Char]
"variable definition should be linear"
              else
                (Integer
c, [Var] -> Var
forall a. HasCallStack => [a] -> a
head [Var]
ls)
            | (Integer
c, [Var]
ls) <- Sum
s, Bool -> Bool
not ([Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
ls), Integer
c Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0
            ]

          g :: Integer -> [(Integer, SAT.Var)] -> [(SAT.Var, Bool)]
          g :: Integer -> [(Integer, Var)] -> [(Var, Bool)]
g Integer
0 [] = []
          g Integer
_ [] = [Char] -> [(Var, Bool)]
forall a. HasCallStack => [Char] -> a
error [Char]
"no more variables"
          g Integer
v ((Integer
c,Var
l) : [(Integer, Var)]
ys)
            | Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
c    = (Var
l, Bool
True)  (Var, Bool) -> [(Var, Bool)] -> [(Var, Bool)]
forall a. a -> [a] -> [a]
: Integer -> [(Integer, Var)] -> [(Var, Bool)]
g (Integer
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
c) [(Integer, Var)]
ys
            | Bool
otherwise = (Var
l, Bool
False) (Var, Bool) -> [(Var, Bool)] -> [(Var, Bool)]
forall a. a -> [a] -> [a]
: Integer -> [(Integer, Var)] -> [(Var, Bool)]
g Integer
v [(Integer, Var)]
ys

instance BackwardTransformer IP2PBInfo where
  transformBackward :: IP2PBInfo -> Target IP2PBInfo -> Source IP2PBInfo
transformBackward (IP2PBInfo Map Var Expr
vmap Map Var Var
_nonZeroTable Integer
_d) Target IP2PBInfo
m = (Expr -> Rational) -> Map Var Expr -> Map Var Rational
forall a b. (a -> b) -> Map Var a -> Map Var b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Rational
forall a. Real a => a -> Rational
toRational (Integer -> Rational) -> (Expr -> Integer) -> Expr -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UArray Var Bool -> Expr -> Integer
forall m. IModel m => m -> Expr -> Integer
Integer.eval UArray Var Bool
Target IP2PBInfo
m) Map Var Expr
vmap

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

instance ObjValueForwardTransformer IP2PBInfo where
  transformObjValueForward :: IP2PBInfo -> SourceObjValue IP2PBInfo -> TargetObjValue IP2PBInfo
transformObjValueForward (IP2PBInfo Map Var Expr
_vmap Map Var Var
_nonZeroTable Integer
d) SourceObjValue IP2PBInfo
val = Rational -> Integer
asInteger (Rational
SourceObjValue IP2PBInfo
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 IP2PBInfo where
  transformObjValueBackward :: IP2PBInfo -> TargetObjValue IP2PBInfo -> SourceObjValue IP2PBInfo
transformObjValueBackward (IP2PBInfo Map Var Expr
_vmap Map Var Var
_nonZeroTable Integer
d) TargetObjValue IP2PBInfo
val = Integer -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
TargetObjValue IP2PBInfo
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

instance J.ToJSON IP2PBInfo where
  toJSON :: IP2PBInfo -> Value
toJSON (IP2PBInfo Map Var Expr
vmap Map Var Var
nonZeroTable Integer
d) =
    [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"IP2PBInfo" :: J.Value)
    , Key
"substitutions" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Pair] -> Value
J.object
        [ Text -> Key
toKey (Var -> Text
MIP.varName Var
v) Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Sum -> Value
jPBSum Sum
s
        | (Var
v, Integer.Expr Sum
s) <- Map Var Expr -> [(Var, Expr)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Var Expr
vmap
        ]
    , Key
"nonzero_indicators" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Pair] -> Value
J.object
        [ Text -> Key
toKey (Var -> Text
MIP.varName Var
v) Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Var -> Value
forall a. IsString a => Var -> a
jLitName Var
lit :: J.Value)
        | (Var
v, Var
lit) <- Map Var Var -> [(Var, Var)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Var Var
nonZeroTable
        ]
    , Key
"objective_function_scale_factor" Key -> Integer -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Integer
d
    ]
    where
#if MIN_VERSION_aeson(2,0,0)
      toKey :: Text -> Key
toKey = Text -> Key
Key.fromText
#else
      toKey = id
#endif

instance J.FromJSON IP2PBInfo where
  parseJSON :: Value -> Parser IP2PBInfo
parseJSON = [Char] -> (Object -> Parser IP2PBInfo) -> Value -> Parser IP2PBInfo
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withTypedObject [Char]
"IP2PBInfo" ((Object -> Parser IP2PBInfo) -> Value -> Parser IP2PBInfo)
-> (Object -> Parser IP2PBInfo) -> Value -> Parser IP2PBInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    Map Text Value
tmp1 <- Object
obj Object -> Key -> Parser (Map Text Value)
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"substitutions"
    Map Var Expr
subst <- ([(Var, Expr)] -> Map Var Expr)
-> Parser [(Var, Expr)] -> Parser (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 (Parser [(Var, Expr)] -> Parser (Map Var Expr))
-> Parser [(Var, Expr)] -> Parser (Map Var Expr)
forall a b. (a -> b) -> a -> b
$ [(Text, Value)]
-> ((Text, Value) -> Parser (Var, Expr)) -> Parser [(Var, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map Text Value -> [(Text, Value)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Text Value
tmp1) (((Text, Value) -> Parser (Var, Expr)) -> Parser [(Var, Expr)])
-> ((Text, Value) -> Parser (Var, Expr)) -> Parser [(Var, Expr)]
forall a b. (a -> b) -> a -> b
$ \(Text
name, Value
expr) -> do
      Sum
s <- Value -> Parser Sum
parsePBSum Value
expr
      (Var, Expr) -> Parser (Var, Expr)
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> Var
MIP.Var Text
name, Sum -> Expr
Integer.Expr Sum
s)
    Map Text Value
tmp2 <- Object
obj Object -> Key -> Parser (Map Text Value)
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"nonzero_indicators"
    Map Var Var
nonZeroTable <- ([(Var, Var)] -> Map Var Var)
-> Parser [(Var, Var)] -> Parser (Map Var Var)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Var, Var)] -> Map Var Var
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (Parser [(Var, Var)] -> Parser (Map Var Var))
-> Parser [(Var, Var)] -> Parser (Map Var Var)
forall a b. (a -> b) -> a -> b
$ [(Text, Value)]
-> ((Text, Value) -> Parser (Var, Var)) -> Parser [(Var, Var)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map Text Value -> [(Text, Value)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Text Value
tmp2) (((Text, Value) -> Parser (Var, Var)) -> Parser [(Var, Var)])
-> ((Text, Value) -> Parser (Var, Var)) -> Parser [(Var, Var)]
forall a b. (a -> b) -> a -> b
$ \(Text
name, Value
s) -> do
      Var
lit <- Value -> Parser Var
parseLitName Value
s
      (Var, Var) -> Parser (Var, Var)
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> Var
MIP.Var Text
name, Var
lit)
    Integer
d <- Object
obj Object -> Key -> Parser Integer
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"objective_function_scale_factor"
    IP2PBInfo -> Parser IP2PBInfo
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IP2PBInfo -> Parser IP2PBInfo) -> IP2PBInfo -> Parser IP2PBInfo
forall a b. (a -> b) -> a -> b
$ Map Var Expr -> Map Var Var -> Integer -> IP2PBInfo
IP2PBInfo Map Var Expr
subst Map Var Var
nonZeroTable Integer
d

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

addMIP' :: forall m enc. (SAT.AddPBNL m enc, PrimMonad m) => enc -> MIP.Problem Rational -> ExceptT String m (Integer.Expr, IP2PBInfo)
addMIP' :: forall (m :: * -> *) enc.
(AddPBNL m enc, PrimMonad m) =>
enc -> Problem Rational -> ExceptT [Char] m (Expr, IP2PBInfo)
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
    [Char] -> ExceptT [Char] m (Expr, IP2PBInfo)
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ([Char] -> ExceptT [Char] m (Expr, IP2PBInfo))
-> [Char] -> ExceptT [Char] m (Expr, IP2PBInfo)
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot handle non-integer variables: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " ((Var -> [Char]) -> [Var] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> [Char]
T.unpack (Text -> [Char]) -> (Var -> Text) -> Var -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Text
MIP.varName) (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 [Char] m [(Var, Expr)]
-> ExceptT [Char] 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 [Char] m [(Var, Expr)] -> ExceptT [Char] m (Map Var Expr))
-> ExceptT [Char] m [(Var, Expr)]
-> ExceptT [Char] m (Map Var Expr)
forall a b. (a -> b) -> a -> b
$ [Var]
-> (Var -> ExceptT [Char] m (Var, Expr))
-> ExceptT [Char] 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 [Char] m (Var, Expr))
 -> ExceptT [Char] m [(Var, Expr)])
-> (Var -> ExceptT [Char] m (Var, Expr))
-> ExceptT [Char] 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 [Char] m Expr
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Expr -> ExceptT [Char] m Expr)
-> m Expr -> ExceptT [Char] 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 b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
lb) (Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
ub)
          (Var, Expr) -> ExceptT [Char] m (Var, Expr)
forall a. a -> ExceptT [Char] m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
v,Expr
v2)
        Bounds Rational
_ -> do
          [Char] -> ExceptT [Char] m (Var, Expr)
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ([Char] -> ExceptT [Char] m (Var, Expr))
-> [Char] -> ExceptT [Char] m (Var, Expr)
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot handle unbounded variable: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
T.unpack (Var -> Text
MIP.varName Var
v)
    [Constraint Rational]
-> (Constraint Rational -> ExceptT [Char] m ())
-> ExceptT [Char] 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 [Char] m ())
 -> ExceptT [Char] m ())
-> (Constraint Rational -> ExceptT [Char] m ())
-> ExceptT [Char] 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 [Char] m ()
f RelOp
op Rational
rhs = do
            let d :: Integer
d = (Integer -> Integer -> Integer) -> Integer -> [Integer] -> Integer
forall b a. (b -> a -> b) -> b -> [a] -> b
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 a. Num a => [a] -> a
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 [Char] m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT [Char] m ()) -> m () -> ExceptT [Char] 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' :: Var
var' = Expr -> Var
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 [Char] m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT [Char] m ()) -> m () -> ExceptT [Char] m ()
forall a b. (a -> b) -> a -> b
$ enc -> Var -> OrdRel Expr -> m ()
forall (m :: * -> *) enc.
AddPBNL m enc =>
enc -> Var -> OrdRel Expr -> m ()
Integer.addConstraintSoft enc
enc Var
var' OrdRel Expr
c2
                  Rational
0 -> m () -> ExceptT [Char] m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT [Char] m ()) -> m () -> ExceptT [Char] m ()
forall a b. (a -> b) -> a -> b
$ enc -> Var -> OrdRel Expr -> m ()
forall (m :: * -> *) enc.
AddPBNL m enc =>
enc -> Var -> OrdRel Expr -> m ()
Integer.addConstraintSoft enc
enc (Var -> Var
SAT.litNot Var
var') OrdRel Expr
c2
                  Rational
_ -> () -> ExceptT [Char] m ()
forall a. a -> ExceptT [Char] m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          g :: ExceptT [Char] m ()
g = do
            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 [Char] m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT [Char] m ()) -> m () -> ExceptT [Char] m ()
forall a b. (a -> b) -> a -> b
$ enc -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause enc
enc []
              Just (Var
var, Rational
val) -> do
                let var' :: Var
var' = Expr -> Var
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 [Char] m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT [Char] m ()) -> m () -> ExceptT [Char] m ()
forall a b. (a -> b) -> a -> b
$ enc -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause enc
enc [- Var
var']
                  Rational
0 -> m () -> ExceptT [Char] m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT [Char] m ()) -> m () -> ExceptT [Char] m ()
forall a b. (a -> b) -> a -> b
$ enc -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause enc
enc [Var
var']
                  Rational
_ -> () -> ExceptT [Char] m ()
forall a. a -> ExceptT [Char] m a
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 [Char] m ()
f RelOp
MIP.Eql Rational
x2
        (Extended Rational
lb, Extended Rational
ub) -> do
          case Extended Rational
lb of
            Extended Rational
MIP.NegInf -> () -> ExceptT [Char] m ()
forall a. a -> ExceptT [Char] m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            MIP.Finite Rational
x -> RelOp -> Rational -> ExceptT [Char] m ()
f RelOp
MIP.Ge Rational
x
            Extended Rational
MIP.PosInf -> ExceptT [Char] m ()
g
          case Extended Rational
ub of
            Extended Rational
MIP.NegInf -> ExceptT [Char] m ()
g
            MIP.Finite Rational
x -> RelOp -> Rational -> ExceptT [Char] m ()
f RelOp
MIP.Le Rational
x
            Extended Rational
MIP.PosInf -> () -> ExceptT [Char] m ()
forall a. a -> ExceptT [Char] m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    MutVar (PrimState m) (Map Var Var)
nonZeroTableRef <- m (MutVar (PrimState m) (Map Var Var))
-> ExceptT [Char] m (MutVar (PrimState m) (Map Var Var))
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (MutVar (PrimState m) (Map Var Var))
 -> ExceptT [Char] m (MutVar (PrimState m) (Map Var Var)))
-> m (MutVar (PrimState m) (Map Var Var))
-> ExceptT [Char] m (MutVar (PrimState m) (Map Var Var))
forall a b. (a -> b) -> a -> b
$ Map Var Var -> m (MutVar (PrimState m) (Map Var Var))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map Var Var
forall k a. Map k a
Map.empty
    let isNonZero :: MIP.Var -> ExceptT String m SAT.Lit
        isNonZero :: Var -> ExceptT [Char] m Var
isNonZero Var
v = do
          Map Var Var
tbl <- m (Map Var Var) -> ExceptT [Char] m (Map Var Var)
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Map Var Var) -> ExceptT [Char] m (Map Var Var))
-> m (Map Var Var) -> ExceptT [Char] m (Map Var Var)
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) (Map Var Var) -> m (Map Var Var)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) (Map Var Var)
nonZeroTableRef
          case Var -> Map Var Var -> Maybe Var
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Var
v Map Var Var
tbl of
            Just Var
lit -> Var -> ExceptT [Char] m Var
forall a. a -> ExceptT [Char] m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Var
lit
            Maybe Var
Nothing -> do
              let (MIP.Finite Rational
lb, MIP.Finite Rational
ub) = Problem Rational -> Var -> Bounds Rational
forall c. Num c => Problem c -> Var -> Bounds c
MIP.getBounds Problem Rational
mip Var
v
                  e :: Expr
e@(Integer.Expr Sum
s) = Map Var Expr
vmap Map Var Expr -> Var -> Expr
forall k a. Ord k => Map k a -> k -> a
Map.! Var
v
              Var
lit <-
                if Rational
lb Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
0 Bool -> Bool -> Bool
&& Rational
ub Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
1 then do
                  Var -> ExceptT [Char] m Var
forall a. a -> ExceptT [Char] m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Var
asBin Expr
e)
                else do
                  Var
v <- m Var -> ExceptT [Char] m Var
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Var -> ExceptT [Char] m Var) -> m Var -> ExceptT [Char] m Var
forall a b. (a -> b) -> a -> b
$ enc -> m Var
forall (m :: * -> *) a. NewVar m a => a -> m Var
SAT.newVar enc
enc
                  -- F(v) → F(s ≠ 0)
                  -- ⇐ s≠0 → v
                  -- ⇔ ¬v → s=0
                  m () -> ExceptT [Char] m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT [Char] m ()) -> m () -> ExceptT [Char] m ()
forall a b. (a -> b) -> a -> b
$ enc -> Var -> Sum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> Var -> Sum -> Integer -> m ()
SAT.addPBNLExactlySoft enc
enc (- Var
v) Sum
s Integer
0
                  Var -> ExceptT [Char] m Var
forall a. a -> ExceptT [Char] m a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
              m () -> ExceptT [Char] m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT [Char] m ()) -> m () -> ExceptT [Char] m ()
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) (Map Var Var) -> Map Var Var -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar MutVar (PrimState m) (Map Var Var)
nonZeroTableRef (Var -> Var -> Map Var Var -> Map Var Var
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v Var
lit Map Var Var
tbl)
              Var -> ExceptT [Char] m Var
forall a. a -> ExceptT [Char] m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Var
lit

    [SOSConstraint Rational]
-> (SOSConstraint Rational -> ExceptT [Char] m ())
-> ExceptT [Char] 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 [Char] m ())
 -> ExceptT [Char] m ())
-> (SOSConstraint Rational -> ExceptT [Char] m ())
-> ExceptT [Char] 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 -> do
          [Var]
ys <- ((Var, Rational) -> ExceptT [Char] m Var)
-> [(Var, Rational)] -> ExceptT [Char] m [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Var -> ExceptT [Char] m Var
isNonZero (Var -> ExceptT [Char] m Var)
-> ((Var, Rational) -> Var)
-> (Var, Rational)
-> ExceptT [Char] m Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Rational) -> Var
forall a b. (a, b) -> a
fst) [(Var, Rational)]
xs
          m () -> ExceptT [Char] m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT [Char] m ()) -> m () -> ExceptT [Char] m ()
forall a b. (a -> b) -> a -> b
$ enc -> [Var] -> Var -> m ()
forall (m :: * -> *) a.
AddCardinality m a =>
a -> [Var] -> Var -> m ()
SAT.addAtMost enc
enc [Var]
ys Var
1
        SOSType
MIP.S2 -> do
          [Var]
ys <- ((Var, Rational) -> ExceptT [Char] m Var)
-> [(Var, Rational)] -> ExceptT [Char] m [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Var -> ExceptT [Char] m Var
isNonZero (Var -> ExceptT [Char] m Var)
-> ((Var, Rational) -> Var)
-> (Var, Rational)
-> ExceptT [Char] m Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Rational) -> Var
forall a b. (a, b) -> a
fst) ([(Var, Rational)] -> ExceptT [Char] m [Var])
-> [(Var, Rational)] -> ExceptT [Char] m [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)]
xs
          m () -> ExceptT [Char] m ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT [Char] m ()) -> m () -> ExceptT [Char] m ()
forall a b. (a -> b) -> a -> b
$ enc -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addSOS2 enc
enc [Var]
ys

    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 b a. (b -> a -> b) -> b -> [a] -> b
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 a. Num a => [a] -> a
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)]

    Map Var Var
nonZeroTable <- MutVar (PrimState (ExceptT [Char] m)) (Map Var Var)
-> ExceptT [Char] m (Map Var Var)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) (Map Var Var)
MutVar (PrimState (ExceptT [Char] m)) (Map Var Var)
nonZeroTableRef

    (Expr, IP2PBInfo) -> ExceptT [Char] m (Expr, IP2PBInfo)
forall a. a -> ExceptT [Char] m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
obj2, Map Var Expr -> Map Var Var -> Integer -> IP2PBInfo
IP2PBInfo Map Var Expr
vmap Map Var Var
nonZeroTable 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

    asBin :: Integer.Expr -> SAT.Lit
    asBin :: Expr -> Var
asBin (Integer.Expr [(Integer
1,[Var
lit])]) = Var
lit
    asBin Expr
_ = [Char] -> Var
forall a. HasCallStack => [Char] -> a
error [Char]
"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 = [Char] -> Integer
forall a. HasCallStack => [Char] -> a
error (Rational -> [Char]
forall a. Show a => a -> [Char]
show Rational
r [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" is not integer")
  | Bool
otherwise = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r

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