{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.PB
-- Copyright   :  (c) Masahiro Sakai 2011-2014,2016-2018
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.Converter.PB
  ( module ToySolver.Converter.Base
  , module ToySolver.Converter.Tseitin

  -- * Normalization of PB/WBO problems
  , normalizePB
  , normalizeWBO

  -- * Modify objective function
  , ObjType (..)
  , setObj

  -- * Linealization of PB/WBO problems
  , linearizePB
  , linearizeWBO
  , PBLinearizeInfo

  -- * Quadratization of PB problems
  , quadratizePB
  , quadratizePB'
  , PBQuadratizeInfo

  -- * Converting inequality constraints into equality constraints
  , inequalitiesToEqualitiesPB
  , PBInequalitiesToEqualitiesInfo (..)

  -- * Converting constraints into penalty terms in objective function
  , unconstrainPB
  , PBUnconstrainInfo (..)

  -- * PB↔WBO conversion
  , pb2wbo
  , PB2WBOInfo (..)
  , wbo2pb
  , WBO2PBInfo (..)
  , addWBO

  -- * SAT↔PB conversion
  , sat2pb
  , SAT2PBInfo
  , pb2sat
  , pb2satWith
  , PB2SATInfo

  -- * MaxSAT↔WBO conversion
  , maxsat2wbo
  , MaxSAT2WBOInfo
  , wbo2maxsat
  , wbo2maxsatWith
  , WBO2MaxSATInfo

  -- * PB→QUBO conversion
  , pb2qubo'
  , PB2QUBOInfo'

  -- * General data types
  , PBIdentityInfo (..)
  , PBTseitinInfo (..)

  -- * misc
  , pb2lsp
  , wbo2lsp
  , pb2smp
  ) where

import Control.Monad
import Control.Monad.Primitive
import Control.Monad.ST
import qualified Data.Aeson as J
import Data.Aeson ((.=), (.:))
import Data.Array.IArray
import Data.Bits hiding (And (..))
import Data.ByteString.Builder
import Data.Default.Class
import qualified Data.Foldable as F
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe
import Data.Primitive.MutVar
import qualified Data.Sequence as Seq
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.PseudoBoolean as PBFile

import ToySolver.Converter.Base
import qualified ToySolver.Converter.PB.Internal.Product as Product
import ToySolver.Converter.Tseitin
import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.Internal.JSON
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Formula (..))
import qualified ToySolver.SAT.Encoder.PB as PB
import qualified ToySolver.SAT.Encoder.PBNLC as PBNLC
import ToySolver.SAT.Internal.JSON
import ToySolver.SAT.Store.CNF
import ToySolver.SAT.Store.PB

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

-- XXX: we do not normalize objective function, because normalization might
-- introduce constant terms, but OPB file format does not allow constant terms.
--
-- Options:
-- (1) not normalize objective function (current implementation),
-- (2) normalize and simply delete constant terms (in pseudo-boolean package?),
-- (3) normalize and introduce dummy variable to make constant terms
--     into non-constant terms (in pseudo-boolean package?).
normalizePB :: PBFile.Formula -> PBFile.Formula
normalizePB :: Formula -> Formula
normalizePB Formula
formula =
  Formula
formula
  { PBFile.pbConstraints =
      map normalizePBConstraint (PBFile.pbConstraints formula)
  }

normalizeWBO :: PBFile.SoftFormula -> PBFile.SoftFormula
normalizeWBO :: SoftFormula -> SoftFormula
normalizeWBO SoftFormula
formula =
  SoftFormula
formula
  { PBFile.wboConstraints =
      map (\(Maybe Integer
w,Constraint
constr) -> (Maybe Integer
w, Constraint -> Constraint
normalizePBConstraint Constraint
constr)) (PBFile.wboConstraints formula)
  }

normalizePBConstraint :: PBFile.Constraint -> PBFile.Constraint
normalizePBConstraint :: Constraint -> Constraint
normalizePBConstraint (Sum
lhs,Op
op,Integer
rhs) =
  case (Integer -> (Integer, [Int]) -> (Integer, (Integer, [Int])))
-> Integer -> Sum -> (Integer, Sum)
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL Integer -> (Integer, [Int]) -> (Integer, (Integer, [Int]))
forall {a} {a}.
(Ord a, Num a, Num a) =>
a -> (a, [a]) -> (a, (a, [a]))
h Integer
0 Sum
lhs of
    (Integer
offset, Sum
lhs') -> (Sum
lhs', Op
op, Integer
rhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
offset)
  where
    h :: a -> (a, [a]) -> (a, (a, [a]))
h a
s (a
w,[a
x]) | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = (a
sa -> a -> a
forall a. Num a => a -> a -> a
+a
w, (-a
w,[-a
x]))
    h a
s (a, [a])
t = (a
s,(a, [a])
t)

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

data ObjType = ObjNone | ObjMaxOne | ObjMaxZero
  deriving (ObjType -> ObjType -> Bool
(ObjType -> ObjType -> Bool)
-> (ObjType -> ObjType -> Bool) -> Eq ObjType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ObjType -> ObjType -> Bool
== :: ObjType -> ObjType -> Bool
$c/= :: ObjType -> ObjType -> Bool
/= :: ObjType -> ObjType -> Bool
Eq, Eq ObjType
Eq ObjType =>
(ObjType -> ObjType -> Ordering)
-> (ObjType -> ObjType -> Bool)
-> (ObjType -> ObjType -> Bool)
-> (ObjType -> ObjType -> Bool)
-> (ObjType -> ObjType -> Bool)
-> (ObjType -> ObjType -> ObjType)
-> (ObjType -> ObjType -> ObjType)
-> Ord ObjType
ObjType -> ObjType -> Bool
ObjType -> ObjType -> Ordering
ObjType -> ObjType -> ObjType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ObjType -> ObjType -> Ordering
compare :: ObjType -> ObjType -> Ordering
$c< :: ObjType -> ObjType -> Bool
< :: ObjType -> ObjType -> Bool
$c<= :: ObjType -> ObjType -> Bool
<= :: ObjType -> ObjType -> Bool
$c> :: ObjType -> ObjType -> Bool
> :: ObjType -> ObjType -> Bool
$c>= :: ObjType -> ObjType -> Bool
>= :: ObjType -> ObjType -> Bool
$cmax :: ObjType -> ObjType -> ObjType
max :: ObjType -> ObjType -> ObjType
$cmin :: ObjType -> ObjType -> ObjType
min :: ObjType -> ObjType -> ObjType
Ord, Int -> ObjType
ObjType -> Int
ObjType -> [ObjType]
ObjType -> ObjType
ObjType -> ObjType -> [ObjType]
ObjType -> ObjType -> ObjType -> [ObjType]
(ObjType -> ObjType)
-> (ObjType -> ObjType)
-> (Int -> ObjType)
-> (ObjType -> Int)
-> (ObjType -> [ObjType])
-> (ObjType -> ObjType -> [ObjType])
-> (ObjType -> ObjType -> [ObjType])
-> (ObjType -> ObjType -> ObjType -> [ObjType])
-> Enum ObjType
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: ObjType -> ObjType
succ :: ObjType -> ObjType
$cpred :: ObjType -> ObjType
pred :: ObjType -> ObjType
$ctoEnum :: Int -> ObjType
toEnum :: Int -> ObjType
$cfromEnum :: ObjType -> Int
fromEnum :: ObjType -> Int
$cenumFrom :: ObjType -> [ObjType]
enumFrom :: ObjType -> [ObjType]
$cenumFromThen :: ObjType -> ObjType -> [ObjType]
enumFromThen :: ObjType -> ObjType -> [ObjType]
$cenumFromTo :: ObjType -> ObjType -> [ObjType]
enumFromTo :: ObjType -> ObjType -> [ObjType]
$cenumFromThenTo :: ObjType -> ObjType -> ObjType -> [ObjType]
enumFromThenTo :: ObjType -> ObjType -> ObjType -> [ObjType]
Enum, ObjType
ObjType -> ObjType -> Bounded ObjType
forall a. a -> a -> Bounded a
$cminBound :: ObjType
minBound :: ObjType
$cmaxBound :: ObjType
maxBound :: ObjType
Bounded, Int -> ObjType -> ShowS
[ObjType] -> ShowS
ObjType -> [Char]
(Int -> ObjType -> ShowS)
-> (ObjType -> [Char]) -> ([ObjType] -> ShowS) -> Show ObjType
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ObjType -> ShowS
showsPrec :: Int -> ObjType -> ShowS
$cshow :: ObjType -> [Char]
show :: ObjType -> [Char]
$cshowList :: [ObjType] -> ShowS
showList :: [ObjType] -> ShowS
Show)

setObj :: ObjType -> PBFile.Formula -> PBFile.Formula
setObj :: ObjType -> Formula -> Formula
setObj ObjType
objType Formula
formula = Formula
formula{ PBFile.pbObjectiveFunction = Just obj2 }
  where
    obj2 :: Sum
obj2 = ObjType -> Formula -> Sum
genObj ObjType
objType Formula
formula

genObj :: ObjType -> PBFile.Formula -> PBFile.Sum
genObj :: ObjType -> Formula -> Sum
genObj ObjType
objType Formula
formula =
  case ObjType
objType of
    ObjType
ObjNone    -> []
    ObjType
ObjMaxOne  -> [(Integer
1,[-Int
v]) | Int
v <- [Int
1 .. Formula -> Int
PBFile.pbNumVars Formula
formula]] -- minimize false literals
    ObjType
ObjMaxZero -> [(Integer
1,[ Int
v]) | Int
v <- [Int
1 .. Formula -> Int
PBFile.pbNumVars Formula
formula]] -- minimize true literals

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

data PBIdentityInfo = PBIdentityInfo
  deriving (Int -> PBIdentityInfo -> ShowS
[PBIdentityInfo] -> ShowS
PBIdentityInfo -> [Char]
(Int -> PBIdentityInfo -> ShowS)
-> (PBIdentityInfo -> [Char])
-> ([PBIdentityInfo] -> ShowS)
-> Show PBIdentityInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PBIdentityInfo -> ShowS
showsPrec :: Int -> PBIdentityInfo -> ShowS
$cshow :: PBIdentityInfo -> [Char]
show :: PBIdentityInfo -> [Char]
$cshowList :: [PBIdentityInfo] -> ShowS
showList :: [PBIdentityInfo] -> ShowS
Show, PBIdentityInfo -> PBIdentityInfo -> Bool
(PBIdentityInfo -> PBIdentityInfo -> Bool)
-> (PBIdentityInfo -> PBIdentityInfo -> Bool) -> Eq PBIdentityInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PBIdentityInfo -> PBIdentityInfo -> Bool
== :: PBIdentityInfo -> PBIdentityInfo -> Bool
$c/= :: PBIdentityInfo -> PBIdentityInfo -> Bool
/= :: PBIdentityInfo -> PBIdentityInfo -> Bool
Eq)

instance Transformer PBIdentityInfo where
  type Source PBIdentityInfo = SAT.Model
  type Target PBIdentityInfo = SAT.Model

instance ForwardTransformer PBIdentityInfo where
  transformForward :: PBIdentityInfo -> Source PBIdentityInfo -> Target PBIdentityInfo
transformForward PBIdentityInfo
_ = Model -> Model
Source PBIdentityInfo -> Target PBIdentityInfo
forall a. a -> a
id

instance BackwardTransformer PBIdentityInfo where
  transformBackward :: PBIdentityInfo -> Target PBIdentityInfo -> Source PBIdentityInfo
transformBackward PBIdentityInfo
_ = Model -> Model
Target PBIdentityInfo -> Source PBIdentityInfo
forall a. a -> a
id

instance ObjValueTransformer PBIdentityInfo where
  type SourceObjValue PBIdentityInfo = Integer
  type TargetObjValue PBIdentityInfo = Integer

instance ObjValueForwardTransformer PBIdentityInfo where
  transformObjValueForward :: PBIdentityInfo
-> SourceObjValue PBIdentityInfo -> TargetObjValue PBIdentityInfo
transformObjValueForward PBIdentityInfo
_ = Integer -> Integer
SourceObjValue PBIdentityInfo -> TargetObjValue PBIdentityInfo
forall a. a -> a
id

instance ObjValueBackwardTransformer PBIdentityInfo where
  transformObjValueBackward :: PBIdentityInfo
-> TargetObjValue PBIdentityInfo -> SourceObjValue PBIdentityInfo
transformObjValueBackward PBIdentityInfo
_ = Integer -> Integer
TargetObjValue PBIdentityInfo -> SourceObjValue PBIdentityInfo
forall a. a -> a
id

instance J.ToJSON PBIdentityInfo where
  toJSON :: PBIdentityInfo -> Value
toJSON PBIdentityInfo
PBIdentityInfo =
    [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
"PBIdentityInfo" :: J.Value)
    ]

instance J.FromJSON PBIdentityInfo where
  parseJSON :: Value -> Parser PBIdentityInfo
parseJSON = [Char]
-> (Object -> Parser PBIdentityInfo)
-> Value
-> Parser PBIdentityInfo
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withTypedObject [Char]
"PBIdentityInfo" ((Object -> Parser PBIdentityInfo)
 -> Value -> Parser PBIdentityInfo)
-> (Object -> Parser PBIdentityInfo)
-> Value
-> Parser PBIdentityInfo
forall a b. (a -> b) -> a -> b
$ \Object
_ -> PBIdentityInfo -> Parser PBIdentityInfo
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PBIdentityInfo
PBIdentityInfo


newtype PBTseitinInfo = PBTseitinInfo TseitinInfo
  deriving (PBTseitinInfo -> PBTseitinInfo -> Bool
(PBTseitinInfo -> PBTseitinInfo -> Bool)
-> (PBTseitinInfo -> PBTseitinInfo -> Bool) -> Eq PBTseitinInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PBTseitinInfo -> PBTseitinInfo -> Bool
== :: PBTseitinInfo -> PBTseitinInfo -> Bool
$c/= :: PBTseitinInfo -> PBTseitinInfo -> Bool
/= :: PBTseitinInfo -> PBTseitinInfo -> Bool
Eq, Int -> PBTseitinInfo -> ShowS
[PBTseitinInfo] -> ShowS
PBTseitinInfo -> [Char]
(Int -> PBTseitinInfo -> ShowS)
-> (PBTseitinInfo -> [Char])
-> ([PBTseitinInfo] -> ShowS)
-> Show PBTseitinInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PBTseitinInfo -> ShowS
showsPrec :: Int -> PBTseitinInfo -> ShowS
$cshow :: PBTseitinInfo -> [Char]
show :: PBTseitinInfo -> [Char]
$cshowList :: [PBTseitinInfo] -> ShowS
showList :: [PBTseitinInfo] -> ShowS
Show)

instance Transformer PBTseitinInfo where
  type Source PBTseitinInfo = SAT.Model
  type Target PBTseitinInfo = SAT.Model

instance ForwardTransformer PBTseitinInfo where
  transformForward :: PBTseitinInfo -> Source PBTseitinInfo -> Target PBTseitinInfo
transformForward (PBTseitinInfo TseitinInfo
info) = TseitinInfo -> Source TseitinInfo -> Target TseitinInfo
forall a. ForwardTransformer a => a -> Source a -> Target a
transformForward TseitinInfo
info

instance BackwardTransformer PBTseitinInfo where
  transformBackward :: PBTseitinInfo -> Target PBTseitinInfo -> Source PBTseitinInfo
transformBackward (PBTseitinInfo TseitinInfo
info) = TseitinInfo -> Target TseitinInfo -> Source TseitinInfo
forall a. BackwardTransformer a => a -> Target a -> Source a
transformBackward TseitinInfo
info

instance ObjValueTransformer PBTseitinInfo where
  type SourceObjValue PBTseitinInfo = Integer
  type TargetObjValue PBTseitinInfo = Integer

instance ObjValueForwardTransformer PBTseitinInfo where
  transformObjValueForward :: PBTseitinInfo
-> SourceObjValue PBTseitinInfo -> TargetObjValue PBTseitinInfo
transformObjValueForward PBTseitinInfo
_ = Integer -> Integer
SourceObjValue PBTseitinInfo -> TargetObjValue PBTseitinInfo
forall a. a -> a
id

instance ObjValueBackwardTransformer PBTseitinInfo where
  transformObjValueBackward :: PBTseitinInfo
-> TargetObjValue PBTseitinInfo -> SourceObjValue PBTseitinInfo
transformObjValueBackward PBTseitinInfo
_ = Integer -> Integer
TargetObjValue PBTseitinInfo -> SourceObjValue PBTseitinInfo
forall a. a -> a
id

instance J.ToJSON PBTseitinInfo where
  toJSON :: PBTseitinInfo -> Value
toJSON (PBTseitinInfo TseitinInfo
info) =
    [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
"PBTseitinInfo" :: J.Value)
    , Key
"base" Key -> TseitinInfo -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= TseitinInfo
info
    ]

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

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

type PBLinearizeInfo = PBTseitinInfo

linearizePB :: PBFile.Formula -> Bool -> (PBFile.Formula, PBLinearizeInfo)
linearizePB :: Formula -> Bool -> (Formula, PBTseitinInfo)
linearizePB Formula
formula Bool
usePB = (forall s. ST s (Formula, PBTseitinInfo))
-> (Formula, PBTseitinInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Formula, PBTseitinInfo))
 -> (Formula, PBTseitinInfo))
-> (forall s. ST s (Formula, PBTseitinInfo))
-> (Formula, PBTseitinInfo)
forall a b. (a -> b) -> a -> b
$ do
  PBStore (ST s)
db <- ST s (PBStore (ST s))
forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
  PBStore (ST s) -> Int -> ST s ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ PBStore (ST s)
db (Formula -> Int
PBFile.pbNumVars Formula
formula)
  Encoder (ST s)
tseitin <-  PBStore (ST s) -> ST s (Encoder (ST s))
forall (m :: * -> *) a.
(PrimMonad m, AddPBLin m a) =>
a -> m (Encoder m)
Tseitin.newEncoderWithPBLin PBStore (ST s)
db
  Encoder (ST s) -> Bool -> ST s ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Bool -> m ()
Tseitin.setUsePB Encoder (ST s)
tseitin Bool
usePB
  Encoder (ST s)
pbnlc <- PBStore (ST s) -> Encoder (ST s) -> ST s (Encoder (ST s))
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Encoder m -> m (Encoder m)
PBNLC.newEncoder PBStore (ST s)
db Encoder (ST s)
tseitin
  [Constraint]
cs' <- [Constraint]
-> (Constraint -> ST s Constraint) -> ST s [Constraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Formula -> [Constraint]
PBFile.pbConstraints Formula
formula) ((Constraint -> ST s Constraint) -> ST s [Constraint])
-> (Constraint -> ST s Constraint) -> ST s [Constraint]
forall a b. (a -> b) -> a -> b
$ \(Sum
lhs,Op
op,Integer
rhs) -> do
    let p :: Polarity
p = case Op
op of
              Op
PBFile.Ge -> Polarity
Tseitin.polarityPos
              Op
PBFile.Eq -> Polarity
Tseitin.polarityBoth
    PBLinSum
lhs' <- Encoder (ST s) -> Polarity -> Sum -> ST s PBLinSum
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Sum -> m PBLinSum
PBNLC.linearizePBSumWithPolarity Encoder (ST s)
pbnlc Polarity
p Sum
lhs
    Constraint -> ST s Constraint
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Integer
c,[Int
l]) | (Integer
c,Int
l) <- PBLinSum
lhs'],Op
op,Integer
rhs)
  Maybe Sum
obj' <-
    case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
      Maybe Sum
Nothing -> Maybe Sum -> ST s (Maybe Sum)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Sum
forall a. Maybe a
Nothing
      Just Sum
obj -> do
        PBLinSum
obj' <- Encoder (ST s) -> Polarity -> Sum -> ST s PBLinSum
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Sum -> m PBLinSum
PBNLC.linearizePBSumWithPolarity Encoder (ST s)
pbnlc Polarity
Tseitin.polarityNeg Sum
obj
        Maybe Sum -> ST s (Maybe Sum)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Sum -> ST s (Maybe Sum)) -> Maybe Sum -> ST s (Maybe Sum)
forall a b. (a -> b) -> a -> b
$ Sum -> Maybe Sum
forall a. a -> Maybe a
Just [(Integer
c, [Int
l]) | (Integer
c,Int
l) <- PBLinSum
obj']
  Formula
formula' <- PBStore (ST s) -> ST s Formula
forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
  VarMap Formula
defs <- Encoder (ST s) -> ST s (VarMap Formula)
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m (VarMap Formula)
Tseitin.getDefinitions Encoder (ST s)
tseitin
  (Formula, PBTseitinInfo) -> ST s (Formula, PBTseitinInfo)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Formula, PBTseitinInfo) -> ST s (Formula, PBTseitinInfo))
-> (Formula, PBTseitinInfo) -> ST s (Formula, PBTseitinInfo)
forall a b. (a -> b) -> a -> b
$
    ( Formula
formula'
      { PBFile.pbObjectiveFunction = obj'
      , PBFile.pbConstraints = cs' ++ PBFile.pbConstraints formula'
      , PBFile.pbNumConstraints = PBFile.pbNumConstraints formula + PBFile.pbNumConstraints formula'
      }
    , TseitinInfo -> PBTseitinInfo
PBTseitinInfo (TseitinInfo -> PBTseitinInfo) -> TseitinInfo -> PBTseitinInfo
forall a b. (a -> b) -> a -> b
$ Int -> Int -> VarMap Formula -> TseitinInfo
TseitinInfo (Formula -> Int
PBFile.pbNumVars Formula
formula) (Formula -> Int
PBFile.pbNumVars Formula
formula') VarMap Formula
defs
    )

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

linearizeWBO :: PBFile.SoftFormula -> Bool -> (PBFile.SoftFormula, PBLinearizeInfo)
linearizeWBO :: SoftFormula -> Bool -> (SoftFormula, PBTseitinInfo)
linearizeWBO SoftFormula
formula Bool
usePB = (forall s. ST s (SoftFormula, PBTseitinInfo))
-> (SoftFormula, PBTseitinInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (SoftFormula, PBTseitinInfo))
 -> (SoftFormula, PBTseitinInfo))
-> (forall s. ST s (SoftFormula, PBTseitinInfo))
-> (SoftFormula, PBTseitinInfo)
forall a b. (a -> b) -> a -> b
$ do
  PBStore (ST s)
db <- ST s (PBStore (ST s))
forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
  PBStore (ST s) -> Int -> ST s ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ PBStore (ST s)
db (SoftFormula -> Int
PBFile.wboNumVars SoftFormula
formula)
  Encoder (ST s)
tseitin <-  PBStore (ST s) -> ST s (Encoder (ST s))
forall (m :: * -> *) a.
(PrimMonad m, AddPBLin m a) =>
a -> m (Encoder m)
Tseitin.newEncoderWithPBLin PBStore (ST s)
db
  Encoder (ST s) -> Bool -> ST s ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Bool -> m ()
Tseitin.setUsePB Encoder (ST s)
tseitin Bool
usePB
  Encoder (ST s)
pbnlc <- PBStore (ST s) -> Encoder (ST s) -> ST s (Encoder (ST s))
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Encoder m -> m (Encoder m)
PBNLC.newEncoder PBStore (ST s)
db Encoder (ST s)
tseitin
  [(Maybe Integer, Constraint)]
cs' <- [(Maybe Integer, Constraint)]
-> ((Maybe Integer, Constraint)
    -> ST s (Maybe Integer, Constraint))
-> ST s [(Maybe Integer, Constraint)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (SoftFormula -> [(Maybe Integer, Constraint)]
PBFile.wboConstraints SoftFormula
formula) (((Maybe Integer, Constraint) -> ST s (Maybe Integer, Constraint))
 -> ST s [(Maybe Integer, Constraint)])
-> ((Maybe Integer, Constraint)
    -> ST s (Maybe Integer, Constraint))
-> ST s [(Maybe Integer, Constraint)]
forall a b. (a -> b) -> a -> b
$ \(Maybe Integer
cost,(Sum
lhs,Op
op,Integer
rhs)) -> do
    let p :: Polarity
p = case Op
op of
              Op
PBFile.Ge -> Polarity
Tseitin.polarityPos
              Op
PBFile.Eq -> Polarity
Tseitin.polarityBoth
    PBLinSum
lhs' <- Encoder (ST s) -> Polarity -> Sum -> ST s PBLinSum
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Sum -> m PBLinSum
PBNLC.linearizePBSumWithPolarity Encoder (ST s)
pbnlc Polarity
p Sum
lhs
    (Maybe Integer, Constraint) -> ST s (Maybe Integer, Constraint)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer
cost,([(Integer
c,[Int
l]) | (Integer
c,Int
l) <- PBLinSum
lhs'],Op
op,Integer
rhs))
  Formula
formula' <- PBStore (ST s) -> ST s Formula
forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
  VarMap Formula
defs <- Encoder (ST s) -> ST s (VarMap Formula)
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m (VarMap Formula)
Tseitin.getDefinitions Encoder (ST s)
tseitin
  (SoftFormula, PBTseitinInfo) -> ST s (SoftFormula, PBTseitinInfo)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ((SoftFormula, PBTseitinInfo) -> ST s (SoftFormula, PBTseitinInfo))
-> (SoftFormula, PBTseitinInfo)
-> ST s (SoftFormula, PBTseitinInfo)
forall a b. (a -> b) -> a -> b
$
    ( PBFile.SoftFormula
      { wboTopCost :: Maybe Integer
PBFile.wboTopCost = SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
formula
      , wboConstraints :: [(Maybe Integer, Constraint)]
PBFile.wboConstraints = [(Maybe Integer, Constraint)]
cs' [(Maybe Integer, Constraint)]
-> [(Maybe Integer, Constraint)] -> [(Maybe Integer, Constraint)]
forall a. [a] -> [a] -> [a]
++ [(Maybe Integer
forall a. Maybe a
Nothing, Constraint
constr) | Constraint
constr <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula']
      , wboNumVars :: Int
PBFile.wboNumVars = Formula -> Int
PBFile.pbNumVars Formula
formula'
      , wboNumConstraints :: Int
PBFile.wboNumConstraints = SoftFormula -> Int
PBFile.wboNumConstraints SoftFormula
formula Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Formula -> Int
PBFile.pbNumConstraints Formula
formula'
      }
    , TseitinInfo -> PBTseitinInfo
PBTseitinInfo (TseitinInfo -> PBTseitinInfo) -> TseitinInfo -> PBTseitinInfo
forall a b. (a -> b) -> a -> b
$ Int -> Int -> VarMap Formula -> TseitinInfo
TseitinInfo (SoftFormula -> Int
PBFile.wboNumVars SoftFormula
formula) (Formula -> Int
PBFile.pbNumVars Formula
formula') VarMap Formula
defs
    )

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

type PBQuadratizeInfo = PBTseitinInfo

-- | Quandratize PBO/PBS problem without introducing additional constraints.
quadratizePB :: PBFile.Formula -> ((PBFile.Formula, Integer), PBQuadratizeInfo)
quadratizePB :: Formula -> ((Formula, Integer), PBTseitinInfo)
quadratizePB Formula
formula = (Formula, Integer) -> ((Formula, Integer), PBTseitinInfo)
quadratizePB' (Formula
formula, Sum -> Integer
SAT.pbUpperBound Sum
obj)
  where
    obj :: Sum
obj = Sum -> Maybe Sum -> Sum
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe Sum -> Sum) -> Maybe Sum -> Sum
forall a b. (a -> b) -> a -> b
$ Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula

-- | Quandratize PBO/PBS problem without introducing additional constraints.
quadratizePB' :: (PBFile.Formula, Integer) -> ((PBFile.Formula, Integer), PBQuadratizeInfo)
quadratizePB' :: (Formula, Integer) -> ((Formula, Integer), PBTseitinInfo)
quadratizePB' (Formula
formula, Integer
maxObj) =
  ( ( PBFile.Formula
      { pbObjectiveFunction :: Maybe Sum
PBFile.pbObjectiveFunction = Sum -> Maybe Sum
forall a. a -> Maybe a
Just (Sum -> Maybe Sum) -> Sum -> Maybe Sum
forall a b. (a -> b) -> a -> b
$ Sum -> Sum
conv Sum
obj Sum -> Sum -> Sum
forall a. [a] -> [a] -> [a]
++ Sum
penalty
      , pbConstraints :: [Constraint]
PBFile.pbConstraints = [(Sum -> Sum
conv Sum
lhs, Op
op, Integer
rhs) | (Sum
lhs,Op
op,Integer
rhs) <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula]
      , pbNumVars :: Int
PBFile.pbNumVars = Int
nv2
      , pbNumConstraints :: Int
PBFile.pbNumConstraints = Formula -> Int
PBFile.pbNumConstraints Formula
formula
      }
    , Integer
maxObj
    )
  , TseitinInfo -> PBTseitinInfo
PBTseitinInfo (TseitinInfo -> PBTseitinInfo) -> TseitinInfo -> PBTseitinInfo
forall a b. (a -> b) -> a -> b
$ Int -> Int -> VarMap Formula -> TseitinInfo
TseitinInfo Int
nv1 Int
nv2 ([(Int, Formula)] -> VarMap Formula
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int
v, [Formula] -> Formula
And [Int -> Formula
atom Int
l1, Int -> Formula
atom Int
l2]) | (Int
v, (Int
l1,Int
l2)) <- [(Int, (Int, Int))]
prodDefs])
  )
  where
    nv1 :: Int
nv1 = Formula -> Int
PBFile.pbNumVars Formula
formula
    nv2 :: Int
nv2 = Formula -> Int
PBFile.pbNumVars Formula
formula Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
termsToReplace

    degGe3Terms :: Set IntSet
    degGe3Terms :: Set IntSet
degGe3Terms = Formula -> Set IntSet
collectDegGe3Terms Formula
formula

    m :: Map IntSet (IntSet,IntSet)
    m :: Map IntSet (IntSet, IntSet)
m = Set IntSet -> Map IntSet (IntSet, IntSet)
Product.decomposeToBinaryProducts Set IntSet
degGe3Terms

    termsToReplace :: Set IntSet
    termsToReplace :: Set IntSet
termsToReplace = [IntSet] -> Set IntSet -> Set IntSet
go [IntSet]
ts0 Set IntSet
forall a. Set a
Set.empty
      where
        ts0 :: [IntSet]
ts0 = [[IntSet]] -> [IntSet]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[IntSet
t1,IntSet
t2] | IntSet
t <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
degGe3Terms, let (IntSet
t1,IntSet
t2) = Map IntSet (IntSet, IntSet)
m Map IntSet (IntSet, IntSet) -> IntSet -> (IntSet, IntSet)
forall k a. Ord k => Map k a -> k -> a
Map.! IntSet
t]
        go :: [IntSet] -> Set IntSet -> Set IntSet
go [] !Set IntSet
ret = Set IntSet
ret
        go (IntSet
t : [IntSet]
ts) !Set IntSet
ret
          | IntSet -> Int
IntSet.size IntSet
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2  = [IntSet] -> Set IntSet -> Set IntSet
go [IntSet]
ts Set IntSet
ret
          | IntSet
t IntSet -> Set IntSet -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set IntSet
ret = [IntSet] -> Set IntSet -> Set IntSet
go [IntSet]
ts Set IntSet
ret
          | Bool
otherwise =
              case IntSet -> Map IntSet (IntSet, IntSet) -> Maybe (IntSet, IntSet)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IntSet
t Map IntSet (IntSet, IntSet)
m of
                Maybe (IntSet, IntSet)
Nothing -> [Char] -> Set IntSet
forall a. HasCallStack => [Char] -> a
error [Char]
"quadratizePB.termsToReplace: should not happen"
                Just (IntSet
t1,IntSet
t2) -> [IntSet] -> Set IntSet -> Set IntSet
go (IntSet
t1 IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
: IntSet
t2 IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
: [IntSet]
ts) (IntSet -> Set IntSet -> Set IntSet
forall a. Ord a => a -> Set a -> Set a
Set.insert IntSet
t Set IntSet
ret)

    fromV :: IntMap IntSet
    toV :: Map IntSet Int
    (IntMap IntSet
fromV, Map IntSet Int
toV) = ([(Int, IntSet)] -> IntMap IntSet
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int, IntSet)]
l, [(IntSet, Int)] -> Map IntSet Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(IntSet
s,Int
v) | (Int
v,IntSet
s) <- [(Int, IntSet)]
l])
      where
        l :: [(Int, IntSet)]
l = [Int] -> [IntSet] -> [(Int, IntSet)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Formula -> Int
PBFile.pbNumVars Formula
formula Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 ..] (Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
termsToReplace)

    prodDefs :: [(SAT.Var, (SAT.Var, SAT.Var))]
    prodDefs :: [(Int, (Int, Int))]
prodDefs = [(Int
v, (IntSet -> Int
f IntSet
t1, IntSet -> Int
f IntSet
t2)) | (Int
v,IntSet
t) <- IntMap IntSet -> [(Int, IntSet)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap IntSet
fromV, let (IntSet
t1,IntSet
t2) = Map IntSet (IntSet, IntSet)
m Map IntSet (IntSet, IntSet) -> IntSet -> (IntSet, IntSet)
forall k a. Ord k => Map k a -> k -> a
Map.! IntSet
t]
      where
        f :: IntSet -> Int
f IntSet
t
          | IntSet -> Int
IntSet.size IntSet
t Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = [Int] -> Int
forall a. HasCallStack => [a] -> a
head (IntSet -> [Int]
IntSet.toList IntSet
t)
          | Bool
otherwise =
               case IntSet -> Map IntSet Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IntSet
t Map IntSet Int
toV of
                 Maybe Int
Nothing -> [Char] -> Int
forall a. HasCallStack => [Char] -> a
error [Char]
"quadratizePB.prodDefs: should not happen"
                 Just Int
v -> Int
v

    obj :: PBFile.Sum
    obj :: Sum
obj = Sum -> Maybe Sum -> Sum
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe Sum -> Sum) -> Maybe Sum -> Sum
forall a b. (a -> b) -> a -> b
$ Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula

    minObj :: Integer
    minObj :: Integer
minObj = Sum -> Integer
SAT.pbLowerBound Sum
obj

    penalty :: PBFile.Sum
    penalty :: Sum
penalty = [(Integer
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
w2, [Int]
ts) | (Integer
w,[Int]
ts) <- [Sum] -> Sum
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Int -> Int -> Int -> Sum
forall {a} {a}. Num a => a -> a -> a -> [(a, [a])]
p Int
x Int
y Int
z | (Int
z,(Int
x,Int
y)) <- [(Int, (Int, Int))]
prodDefs]]
      where
        -- The penalty function P(x,y,z) = xy − 2xz − 2yz + 3z is such that
        -- P(x,y,z)=0 when z⇔xy and P(x,y,z)>0 when z⇎xy.
        p :: a -> a -> a -> [(a, [a])]
p a
x a
y a
z = [(a
1,[a
x,a
y]), (-a
2,[a
x,a
z]), (-a
2,[a
y,a
z]), (a
3,[a
z])]
        w2 :: Integer
w2 = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (Integer
maxObj Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
minObj) Integer
0 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1

    conv :: PBFile.Sum -> PBFile.Sum
    conv :: Sum -> Sum
conv Sum
s = [(Integer
w, [Int] -> [Int]
f [Int]
t) | (Integer
w,[Int]
t) <- Sum
s]
      where
        f :: [Int] -> [Int]
f [Int]
t =
          case IntSet -> Map IntSet Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IntSet
t' Map IntSet Int
toV of
            Just Int
v  -> [Int
v]
            Maybe Int
Nothing
              | IntSet -> Int
IntSet.size IntSet
t' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3 -> (IntSet -> Int) -> [IntSet] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map IntSet -> Int
g [IntSet
t1, IntSet
t2]
              | Bool
otherwise -> [Int]
t
          where
            t' :: IntSet
t' = [Int] -> IntSet
IntSet.fromList [Int]
t
            (IntSet
t1, IntSet
t2) = Map IntSet (IntSet, IntSet)
m Map IntSet (IntSet, IntSet) -> IntSet -> (IntSet, IntSet)
forall k a. Ord k => Map k a -> k -> a
Map.! IntSet
t'
        g :: IntSet -> Int
g IntSet
t
          | IntSet -> Int
IntSet.size IntSet
t Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = [Int] -> Int
forall a. HasCallStack => [a] -> a
head ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IntSet.toList IntSet
t
          | Bool
otherwise = Map IntSet Int
toV Map IntSet Int -> IntSet -> Int
forall k a. Ord k => Map k a -> k -> a
Map.! IntSet
t

    atom :: SAT.Lit -> Formula
    atom :: Int -> Formula
atom Int
l
      | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = Formula -> Formula
Not (Int -> Formula
Atom (- Int
l))
      | Bool
otherwise = Int -> Formula
Atom Int
l


collectDegGe3Terms :: PBFile.Formula -> Set IntSet
collectDegGe3Terms :: Formula -> Set IntSet
collectDegGe3Terms Formula
formula = [IntSet] -> Set IntSet
forall a. Ord a => [a] -> Set a
Set.fromList [IntSet
t' | [Int]
t <- [[Int]]
terms, let t' :: IntSet
t' = [Int] -> IntSet
IntSet.fromList [Int]
t, IntSet -> Int
IntSet.size IntSet
t' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3]
  where
    sums :: [Sum]
sums = Maybe Sum -> [Sum]
forall a. Maybe a -> [a]
maybeToList (Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula) [Sum] -> [Sum] -> [Sum]
forall a. [a] -> [a] -> [a]
++
           [Sum
lhs | (Sum
lhs,Op
_,Integer
_) <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula]
    terms :: [[Int]]
terms = [[Int]
t | Sum
s <- [Sum]
sums, (Integer
_,[Int]
t) <- Sum
s]

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

-- | Convert inequality constraints into equality constraints by introducing surpass variables.
inequalitiesToEqualitiesPB :: PBFile.Formula -> (PBFile.Formula, PBInequalitiesToEqualitiesInfo)
inequalitiesToEqualitiesPB :: Formula -> (Formula, PBInequalitiesToEqualitiesInfo)
inequalitiesToEqualitiesPB Formula
formula = (forall s. ST s (Formula, PBInequalitiesToEqualitiesInfo))
-> (Formula, PBInequalitiesToEqualitiesInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Formula, PBInequalitiesToEqualitiesInfo))
 -> (Formula, PBInequalitiesToEqualitiesInfo))
-> (forall s. ST s (Formula, PBInequalitiesToEqualitiesInfo))
-> (Formula, PBInequalitiesToEqualitiesInfo)
forall a b. (a -> b) -> a -> b
$ do
  PBStore (ST s)
db <- ST s (PBStore (ST s))
forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
  PBStore (ST s) -> Int -> ST s ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ PBStore (ST s)
db (Formula -> Int
PBFile.pbNumVars Formula
formula)

  [(Sum, Integer, [Int])]
defs <- ([Maybe (Sum, Integer, [Int])] -> [(Sum, Integer, [Int])])
-> ST s [Maybe (Sum, Integer, [Int])]
-> ST s [(Sum, Integer, [Int])]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Maybe (Sum, Integer, [Int])] -> [(Sum, Integer, [Int])]
forall a. [Maybe a] -> [a]
catMaybes (ST s [Maybe (Sum, Integer, [Int])]
 -> ST s [(Sum, Integer, [Int])])
-> ST s [Maybe (Sum, Integer, [Int])]
-> ST s [(Sum, Integer, [Int])]
forall a b. (a -> b) -> a -> b
$ [Constraint]
-> (Constraint -> ST s (Maybe (Sum, Integer, [Int])))
-> ST s [Maybe (Sum, Integer, [Int])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Formula -> [Constraint]
PBFile.pbConstraints Formula
formula) ((Constraint -> ST s (Maybe (Sum, Integer, [Int])))
 -> ST s [Maybe (Sum, Integer, [Int])])
-> (Constraint -> ST s (Maybe (Sum, Integer, [Int])))
-> ST s [Maybe (Sum, Integer, [Int])]
forall a b. (a -> b) -> a -> b
$ \Constraint
constr -> do
    case Constraint
constr of
      (Sum
lhs, Op
PBFile.Eq, Integer
rhs) -> do
        PBStore (ST s) -> Sum -> Integer -> ST s ()
forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly PBStore (ST s)
db Sum
lhs Integer
rhs
        Maybe (Sum, Integer, [Int]) -> ST s (Maybe (Sum, Integer, [Int]))
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Sum, Integer, [Int])
forall a. Maybe a
Nothing
      (Sum
lhs, Op
PBFile.Ge, Integer
rhs) -> do
        case (Sum, Integer) -> Maybe [Int]
asClause (Sum
lhs,Integer
rhs) of
          Just [Int]
clause -> do
            PBStore (ST s) -> Sum -> Integer -> ST s ()
forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly PBStore (ST s)
db [(Integer
1, [- Int
l | Int
l <- [Int]
clause])] Integer
0
            Maybe (Sum, Integer, [Int]) -> ST s (Maybe (Sum, Integer, [Int]))
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Sum, Integer, [Int])
forall a. Maybe a
Nothing
          Maybe [Int]
Nothing -> do
            let maxSurpass :: Integer
maxSurpass = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (Sum -> Integer
SAT.pbUpperBound Sum
lhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
rhs) Integer
0
                maxSurpassNBits :: Int
maxSurpassNBits = [Int] -> Int
forall a. HasCallStack => [a] -> a
head [Int
i | Int
i <- [Int
0..], Integer
maxSurpass Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Bits a => Int -> a
bit Int
i]
            [Int]
vs <- PBStore (ST s) -> Int -> ST s [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars PBStore (ST s)
db Int
maxSurpassNBits
            PBStore (ST s) -> Sum -> Integer -> ST s ()
forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly PBStore (ST s)
db (Sum
lhs Sum -> Sum -> Sum
forall a. [a] -> [a] -> [a]
++ [(-Integer
c,[Int
x]) | (Integer
c,Int
x) <- [Integer] -> [Int] -> PBLinSum
forall a b. [a] -> [b] -> [(a, b)]
zip ((Integer -> Integer) -> Integer -> [Integer]
forall a. (a -> a) -> a -> [a]
iterate (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
2) Integer
1) [Int]
vs]) Integer
rhs
            if Int
maxSurpassNBits Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then do
              Maybe (Sum, Integer, [Int]) -> ST s (Maybe (Sum, Integer, [Int]))
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Sum, Integer, [Int]) -> ST s (Maybe (Sum, Integer, [Int])))
-> Maybe (Sum, Integer, [Int])
-> ST s (Maybe (Sum, Integer, [Int]))
forall a b. (a -> b) -> a -> b
$ (Sum, Integer, [Int]) -> Maybe (Sum, Integer, [Int])
forall a. a -> Maybe a
Just (Sum
lhs, Integer
rhs, [Int]
vs)
            else
              Maybe (Sum, Integer, [Int]) -> ST s (Maybe (Sum, Integer, [Int]))
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Sum, Integer, [Int])
forall a. Maybe a
Nothing

  Formula
formula' <- PBStore (ST s) -> ST s Formula
forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
  (Formula, PBInequalitiesToEqualitiesInfo)
-> ST s (Formula, PBInequalitiesToEqualitiesInfo)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return
    ( Formula
formula'{ PBFile.pbObjectiveFunction = PBFile.pbObjectiveFunction formula }
    , Int
-> Int -> [(Sum, Integer, [Int])] -> PBInequalitiesToEqualitiesInfo
PBInequalitiesToEqualitiesInfo (Formula -> Int
PBFile.pbNumVars Formula
formula) (Formula -> Int
PBFile.pbNumVars Formula
formula') [(Sum, Integer, [Int])]
defs
    )
  where
    asLinSum :: SAT.PBSum -> Maybe (SAT.PBLinSum, Integer)
    asLinSum :: Sum -> Maybe (PBLinSum, Integer)
asLinSum Sum
s = do
      [(Maybe (Integer, Int), Integer)]
ret <- Sum
-> ((Integer, [Int]) -> Maybe (Maybe (Integer, Int), Integer))
-> Maybe [(Maybe (Integer, Int), Integer)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Sum
s (((Integer, [Int]) -> Maybe (Maybe (Integer, Int), Integer))
 -> Maybe [(Maybe (Integer, Int), Integer)])
-> ((Integer, [Int]) -> Maybe (Maybe (Integer, Int), Integer))
-> Maybe [(Maybe (Integer, Int), Integer)]
forall a b. (a -> b) -> a -> b
$ \(Integer
c, [Int]
ls) -> do
        case [Int]
ls of
          [] -> (Maybe (Integer, Int), Integer)
-> Maybe (Maybe (Integer, Int), Integer)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Integer, Int)
forall a. Maybe a
Nothing, Integer
c)
          [Int
l] -> (Maybe (Integer, Int), Integer)
-> Maybe (Maybe (Integer, Int), Integer)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Integer, Int) -> Maybe (Integer, Int)
forall a. a -> Maybe a
Just (Integer
c,Int
l), Integer
0)
          [Int]
_ -> Maybe (Maybe (Integer, Int), Integer)
forall a. Maybe a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      (PBLinSum, Integer) -> Maybe (PBLinSum, Integer)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe (Integer, Int)] -> PBLinSum
forall a. [Maybe a] -> [a]
catMaybes (((Maybe (Integer, Int), Integer) -> Maybe (Integer, Int))
-> [(Maybe (Integer, Int), Integer)] -> [Maybe (Integer, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (Integer, Int), Integer) -> Maybe (Integer, Int)
forall a b. (a, b) -> a
fst [(Maybe (Integer, Int), Integer)]
ret), [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (((Maybe (Integer, Int), Integer) -> Integer)
-> [(Maybe (Integer, Int), Integer)] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (Integer, Int), Integer) -> Integer
forall a b. (a, b) -> b
snd [(Maybe (Integer, Int), Integer)]
ret))

    asClause :: (SAT.PBSum, Integer) -> Maybe SAT.Clause
    asClause :: (Sum, Integer) -> Maybe [Int]
asClause (Sum
lhs, Integer
rhs) = do
      (PBLinSum
lhs', Integer
off) <- Sum -> Maybe (PBLinSum, Integer)
asLinSum Sum
lhs
      let rhs' :: Integer
rhs' = Integer
rhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
off
      case (PBLinSum, Integer) -> (PBLinSum, Integer)
SAT.normalizePBLinAtLeast (PBLinSum
lhs', Integer
rhs') of
        (PBLinSum
lhs'', Integer
1) | ((Integer, Int) -> Bool) -> PBLinSum -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Integer
c,Int
_) -> Integer
c Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1) PBLinSum
lhs'' -> [Int] -> Maybe [Int]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Integer, Int) -> Int) -> PBLinSum -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, Int) -> Int
forall a b. (a, b) -> b
snd PBLinSum
lhs'')
        (PBLinSum, Integer)
_ -> Maybe [Int]
forall a. Maybe a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

data PBInequalitiesToEqualitiesInfo
  = PBInequalitiesToEqualitiesInfo !Int !Int [(PBFile.Sum, Integer, [SAT.Var])]
  deriving (PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
(PBInequalitiesToEqualitiesInfo
 -> PBInequalitiesToEqualitiesInfo -> Bool)
-> (PBInequalitiesToEqualitiesInfo
    -> PBInequalitiesToEqualitiesInfo -> Bool)
-> Eq PBInequalitiesToEqualitiesInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
== :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
$c/= :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
/= :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
Eq, Int -> PBInequalitiesToEqualitiesInfo -> ShowS
[PBInequalitiesToEqualitiesInfo] -> ShowS
PBInequalitiesToEqualitiesInfo -> [Char]
(Int -> PBInequalitiesToEqualitiesInfo -> ShowS)
-> (PBInequalitiesToEqualitiesInfo -> [Char])
-> ([PBInequalitiesToEqualitiesInfo] -> ShowS)
-> Show PBInequalitiesToEqualitiesInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PBInequalitiesToEqualitiesInfo -> ShowS
showsPrec :: Int -> PBInequalitiesToEqualitiesInfo -> ShowS
$cshow :: PBInequalitiesToEqualitiesInfo -> [Char]
show :: PBInequalitiesToEqualitiesInfo -> [Char]
$cshowList :: [PBInequalitiesToEqualitiesInfo] -> ShowS
showList :: [PBInequalitiesToEqualitiesInfo] -> ShowS
Show)

instance Transformer PBInequalitiesToEqualitiesInfo where
  type Source PBInequalitiesToEqualitiesInfo = SAT.Model
  type Target PBInequalitiesToEqualitiesInfo = SAT.Model

instance ForwardTransformer PBInequalitiesToEqualitiesInfo where
  transformForward :: PBInequalitiesToEqualitiesInfo
-> Source PBInequalitiesToEqualitiesInfo
-> Target PBInequalitiesToEqualitiesInfo
transformForward (PBInequalitiesToEqualitiesInfo Int
_nv1 Int
nv2 [(Sum, Integer, [Int])]
defs) Source PBInequalitiesToEqualitiesInfo
m =
    (Int, Int) -> [(Int, Bool)] -> Model
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1, Int
nv2) ([(Int, Bool)] -> Model) -> [(Int, Bool)] -> Model
forall a b. (a -> b) -> a -> b
$ Model -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
Source PBInequalitiesToEqualitiesInfo
m [(Int, Bool)] -> [(Int, Bool)] -> [(Int, Bool)]
forall a. [a] -> [a] -> [a]
++ [(Int
v, Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
n Int
i) | (Sum
lhs, Integer
rhs, [Int]
vs) <- [(Sum, Integer, [Int])]
defs, let n :: Integer
n = Model -> Sum -> Integer
forall m. IModel m => m -> Sum -> Integer
SAT.evalPBSum Model
Source PBInequalitiesToEqualitiesInfo
m Sum
lhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
rhs, (Int
i,Int
v) <- [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Int]
vs]

instance BackwardTransformer PBInequalitiesToEqualitiesInfo where
  transformBackward :: PBInequalitiesToEqualitiesInfo
-> Target PBInequalitiesToEqualitiesInfo
-> Source PBInequalitiesToEqualitiesInfo
transformBackward (PBInequalitiesToEqualitiesInfo Int
nv1 Int
_nv2 [(Sum, Integer, [Int])]
_defs) = Int -> Model -> Model
SAT.restrictModel Int
nv1

instance ObjValueTransformer PBInequalitiesToEqualitiesInfo where
  type SourceObjValue PBInequalitiesToEqualitiesInfo = Integer
  type TargetObjValue PBInequalitiesToEqualitiesInfo = Integer

instance ObjValueForwardTransformer PBInequalitiesToEqualitiesInfo where
  transformObjValueForward :: PBInequalitiesToEqualitiesInfo
-> SourceObjValue PBInequalitiesToEqualitiesInfo
-> TargetObjValue PBInequalitiesToEqualitiesInfo
transformObjValueForward PBInequalitiesToEqualitiesInfo
_ = Integer -> Integer
SourceObjValue PBInequalitiesToEqualitiesInfo
-> TargetObjValue PBInequalitiesToEqualitiesInfo
forall a. a -> a
id

instance ObjValueBackwardTransformer PBInequalitiesToEqualitiesInfo where
  transformObjValueBackward :: PBInequalitiesToEqualitiesInfo
-> TargetObjValue PBInequalitiesToEqualitiesInfo
-> SourceObjValue PBInequalitiesToEqualitiesInfo
transformObjValueBackward PBInequalitiesToEqualitiesInfo
_ = Integer -> Integer
TargetObjValue PBInequalitiesToEqualitiesInfo
-> SourceObjValue PBInequalitiesToEqualitiesInfo
forall a. a -> a
id

instance J.ToJSON PBInequalitiesToEqualitiesInfo where
  toJSON :: PBInequalitiesToEqualitiesInfo -> Value
toJSON (PBInequalitiesToEqualitiesInfo Int
nv1 Int
nv2 [(Sum, Integer, [Int])]
defs) =
    [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
"PBInequalitiesToEqualitiesInfo" :: J.Value)
    , Key
"num_original_variables" Key -> Int -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Int
nv1
    , Key
"num_transformed_variables" Key -> Int -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Int
nv2
    , Key
"slack" 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
          [ Key
"lhs" 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
lhs
          , Key
"rhs" Key -> Integer -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Integer
rhs
          , Key
"slack" Key -> [Value] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Int -> Value
forall a. IsString a => Int -> a
jVarName Int
v :: J.Value | Int
v <- [Int]
vs]
          ]
        | (Sum
lhs, Integer
rhs, [Int]
vs) <- [(Sum, Integer, [Int])]
defs
        ]
    ]

instance J.FromJSON PBInequalitiesToEqualitiesInfo where
  parseJSON :: Value -> Parser PBInequalitiesToEqualitiesInfo
parseJSON = [Char]
-> (Object -> Parser PBInequalitiesToEqualitiesInfo)
-> Value
-> Parser PBInequalitiesToEqualitiesInfo
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withTypedObject [Char]
"PBInequalitiesToEqualitiesInfo" ((Object -> Parser PBInequalitiesToEqualitiesInfo)
 -> Value -> Parser PBInequalitiesToEqualitiesInfo)
-> (Object -> Parser PBInequalitiesToEqualitiesInfo)
-> Value
-> Parser PBInequalitiesToEqualitiesInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    Int
-> Int -> [(Sum, Integer, [Int])] -> PBInequalitiesToEqualitiesInfo
PBInequalitiesToEqualitiesInfo
      (Int
 -> Int
 -> [(Sum, Integer, [Int])]
 -> PBInequalitiesToEqualitiesInfo)
-> Parser Int
-> Parser
     (Int -> [(Sum, Integer, [Int])] -> PBInequalitiesToEqualitiesInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Int
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_original_variables"
      Parser
  (Int -> [(Sum, Integer, [Int])] -> PBInequalitiesToEqualitiesInfo)
-> Parser Int
-> Parser
     ([(Sum, Integer, [Int])] -> PBInequalitiesToEqualitiesInfo)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser Int
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_transformed_variables"
      Parser ([(Sum, Integer, [Int])] -> PBInequalitiesToEqualitiesInfo)
-> Parser [(Sum, Integer, [Int])]
-> Parser PBInequalitiesToEqualitiesInfo
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Value -> Parser (Sum, Integer, [Int]))
-> [Value] -> Parser [(Sum, Integer, [Int])]
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 Value -> Parser (Sum, Integer, [Int])
f ([Value] -> Parser [(Sum, Integer, [Int])])
-> Parser [Value] -> Parser [(Sum, Integer, [Int])]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Object
obj Object -> Key -> Parser [Value]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"slack")
    where
      f :: Value -> Parser (Sum, Integer, [Int])
f = [Char]
-> (Object -> Parser (Sum, Integer, [Int]))
-> Value
-> Parser (Sum, Integer, [Int])
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
J.withObject [Char]
"slack" ((Object -> Parser (Sum, Integer, [Int]))
 -> Value -> Parser (Sum, Integer, [Int]))
-> (Object -> Parser (Sum, Integer, [Int]))
-> Value
-> Parser (Sum, Integer, [Int])
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
        Sum
lhs <- Value -> Parser Sum
parsePBSum (Value -> Parser Sum) -> Parser Value -> Parser Sum
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Object
obj Object -> Key -> Parser Value
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"lhs"
        Integer
rhs <- Object
obj Object -> Key -> Parser Integer
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"rhs"
        [Int]
vs <- ([Char] -> Parser Int) -> [[Char]] -> Parser [Int]
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 [Char] -> Parser Int
forall {f :: * -> *} {a}. (Read a, MonadFail f) => [Char] -> f a
g ([[Char]] -> Parser [Int]) -> Parser [[Char]] -> Parser [Int]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Object
obj Object -> Key -> Parser [[Char]]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"slack"
        (Sum, Integer, [Int]) -> Parser (Sum, Integer, [Int])
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sum
lhs, Integer
rhs, [Int]
vs)
      g :: [Char] -> f a
g (Char
'x' : [Char]
rest) = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> f a) -> a -> f a
forall a b. (a -> b) -> a -> b
$! [Char] -> a
forall a. Read a => [Char] -> a
read [Char]
rest
      g [Char]
s = [Char] -> f a
forall a. [Char] -> f a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char]
"fail to parse variable: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> [Char]
show [Char]
s)

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

unconstrainPB :: PBFile.Formula -> ((PBFile.Formula, Integer), PBUnconstrainInfo)
unconstrainPB :: Formula -> ((Formula, Integer), PBUnconstrainInfo)
unconstrainPB Formula
formula = (Formula -> (Formula, Integer)
unconstrainPB' Formula
formula', PBInequalitiesToEqualitiesInfo -> PBUnconstrainInfo
PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
info)
  where
    (Formula
formula', PBInequalitiesToEqualitiesInfo
info) = Formula -> (Formula, PBInequalitiesToEqualitiesInfo)
inequalitiesToEqualitiesPB Formula
formula

newtype PBUnconstrainInfo = PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
  deriving (PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
(PBUnconstrainInfo -> PBUnconstrainInfo -> Bool)
-> (PBUnconstrainInfo -> PBUnconstrainInfo -> Bool)
-> Eq PBUnconstrainInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
== :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
$c/= :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
/= :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
Eq, Int -> PBUnconstrainInfo -> ShowS
[PBUnconstrainInfo] -> ShowS
PBUnconstrainInfo -> [Char]
(Int -> PBUnconstrainInfo -> ShowS)
-> (PBUnconstrainInfo -> [Char])
-> ([PBUnconstrainInfo] -> ShowS)
-> Show PBUnconstrainInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PBUnconstrainInfo -> ShowS
showsPrec :: Int -> PBUnconstrainInfo -> ShowS
$cshow :: PBUnconstrainInfo -> [Char]
show :: PBUnconstrainInfo -> [Char]
$cshowList :: [PBUnconstrainInfo] -> ShowS
showList :: [PBUnconstrainInfo] -> ShowS
Show)

instance Transformer PBUnconstrainInfo where
  -- type Source PBUnconstrainInfo = Source PBInequalitiesToEqualitiesInfo
  type Source PBUnconstrainInfo = SAT.Model
  -- type Target PBUnconstrainInfo = Target PBInequalitiesToEqualitiesInfo
  type Target PBUnconstrainInfo = SAT.Model

instance ForwardTransformer PBUnconstrainInfo where
  transformForward :: PBUnconstrainInfo
-> Source PBUnconstrainInfo -> Target PBUnconstrainInfo
transformForward (PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
info) = PBInequalitiesToEqualitiesInfo
-> Source PBInequalitiesToEqualitiesInfo
-> Target PBInequalitiesToEqualitiesInfo
forall a. ForwardTransformer a => a -> Source a -> Target a
transformForward PBInequalitiesToEqualitiesInfo
info

instance BackwardTransformer PBUnconstrainInfo where
  transformBackward :: PBUnconstrainInfo
-> Target PBUnconstrainInfo -> Source PBUnconstrainInfo
transformBackward (PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
info) = PBInequalitiesToEqualitiesInfo
-> Target PBInequalitiesToEqualitiesInfo
-> Source PBInequalitiesToEqualitiesInfo
forall a. BackwardTransformer a => a -> Target a -> Source a
transformBackward PBInequalitiesToEqualitiesInfo
info

instance ObjValueTransformer PBUnconstrainInfo where
  -- type SourceObjValue PBUnconstrainInfo = SourceObjValue PBInequalitiesToEqualitiesInfo
  type SourceObjValue PBUnconstrainInfo = Integer
  -- type TargetObjValue PBUnconstrainInfo = TargetObjValue PBInequalitiesToEqualitiesInfo
  type TargetObjValue PBUnconstrainInfo = Integer

instance ObjValueForwardTransformer PBUnconstrainInfo where
  transformObjValueForward :: PBUnconstrainInfo
-> SourceObjValue PBUnconstrainInfo
-> TargetObjValue PBUnconstrainInfo
transformObjValueForward (PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
info) = PBInequalitiesToEqualitiesInfo
-> SourceObjValue PBInequalitiesToEqualitiesInfo
-> TargetObjValue PBInequalitiesToEqualitiesInfo
forall a.
ObjValueForwardTransformer a =>
a -> SourceObjValue a -> TargetObjValue a
transformObjValueForward PBInequalitiesToEqualitiesInfo
info

instance ObjValueBackwardTransformer PBUnconstrainInfo where
  transformObjValueBackward :: PBUnconstrainInfo
-> TargetObjValue PBUnconstrainInfo
-> SourceObjValue PBUnconstrainInfo
transformObjValueBackward (PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
info) = PBInequalitiesToEqualitiesInfo
-> TargetObjValue PBInequalitiesToEqualitiesInfo
-> SourceObjValue PBInequalitiesToEqualitiesInfo
forall a.
ObjValueBackwardTransformer a =>
a -> TargetObjValue a -> SourceObjValue a
transformObjValueBackward PBInequalitiesToEqualitiesInfo
info

instance J.ToJSON PBUnconstrainInfo where
  toJSON :: PBUnconstrainInfo -> Value
toJSON (PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
info) =
    [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
"PBUnconstrainInfo" :: J.Value)
    , Key
"base" Key -> PBInequalitiesToEqualitiesInfo -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= PBInequalitiesToEqualitiesInfo
info
    ]

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

unconstrainPB' :: PBFile.Formula -> (PBFile.Formula, Integer)
unconstrainPB' :: Formula -> (Formula, Integer)
unconstrainPB' Formula
formula =
  ( Formula
formula
    { PBFile.pbObjectiveFunction = Just $ obj1 ++ obj2
    , PBFile.pbConstraints = []
    , PBFile.pbNumConstraints = 0
    }
  , Integer
obj1ub
  )
  where
    obj1 :: Sum
obj1 = Sum -> Maybe Sum -> Sum
forall a. a -> Maybe a -> a
fromMaybe [] (Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula)
    obj1ub :: Integer
obj1ub = Sum -> Integer
SAT.pbUpperBound Sum
obj1
    obj1lb :: Integer
obj1lb = Sum -> Integer
SAT.pbLowerBound Sum
obj1
    p :: Integer
p = Integer
obj1ub Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
obj1lb Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
    obj2 :: Sum
obj2 = [(Integer
pInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
c, IntSet -> [Int]
IntSet.toList IntSet
ls) | (IntSet
ls, Integer
c) <- Map IntSet Integer -> [(IntSet, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList Map IntSet Integer
obj2', Integer
c Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0]
    obj2' :: Map IntSet Integer
obj2' = (Integer -> Integer -> Integer)
-> [Map IntSet Integer] -> Map IntSet Integer
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) [Sum -> Map IntSet Integer
forall {a}. Num a => [(a, [Int])] -> Map IntSet a
sq ((-Integer
rhs, []) (Integer, [Int]) -> Sum -> Sum
forall a. a -> [a] -> [a]
: Sum
lhs) | (Sum
lhs, Op
PBFile.Eq, Integer
rhs) <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula]
    sq :: [(a, [Int])] -> Map IntSet a
sq [(a, [Int])]
ts = (a -> a -> a) -> [(IntSet, a)] -> Map IntSet a
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith a -> a -> a
forall a. Num a => a -> a -> a
(+) ([(IntSet, a)] -> Map IntSet a) -> [(IntSet, a)] -> Map IntSet a
forall a b. (a -> b) -> a -> b
$ do
              (a
c1,[Int]
ls1) <- [(a, [Int])]
ts
              (a
c2,[Int]
ls2) <- [(a, [Int])]
ts
              let ls3 :: IntSet
ls3 = [Int] -> IntSet
IntSet.fromList [Int]
ls1 IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList [Int]
ls2
              Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ IntSet -> Bool
isFalse IntSet
ls3
              (IntSet, a) -> [(IntSet, a)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet
ls3, a
c1a -> a -> a
forall a. Num a => a -> a -> a
*a
c2)
    isFalse :: IntSet -> Bool
isFalse IntSet
ls = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ IntSet -> Bool
IntSet.null (IntSet -> Bool) -> IntSet -> Bool
forall a b. (a -> b) -> a -> b
$ IntSet
ls IntSet -> IntSet -> IntSet
`IntSet.intersection` (Int -> Int) -> IntSet -> IntSet
IntSet.map Int -> Int
forall a. Num a => a -> a
negate IntSet
ls

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

pb2qubo' :: PBFile.Formula -> ((PBFile.Formula, Integer), PB2QUBOInfo')
pb2qubo' :: Formula -> ((Formula, Integer), PB2QUBOInfo')
pb2qubo' Formula
formula = ((Formula
formula2, Integer
th2), PBUnconstrainInfo -> PBTseitinInfo -> PB2QUBOInfo'
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer PBUnconstrainInfo
info1 PBTseitinInfo
info2)
  where
    ((Formula
formula1, Integer
th1), PBUnconstrainInfo
info1) = Formula -> ((Formula, Integer), PBUnconstrainInfo)
unconstrainPB Formula
formula
    ((Formula
formula2, Integer
th2), PBTseitinInfo
info2) = (Formula, Integer) -> ((Formula, Integer), PBTseitinInfo)
quadratizePB' (Formula
formula1, Integer
th1)

type PB2QUBOInfo' = ComposedTransformer PBUnconstrainInfo PBQuadratizeInfo

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

pb2wbo :: PBFile.Formula -> (PBFile.SoftFormula, PB2WBOInfo)
pb2wbo :: Formula -> (SoftFormula, PB2WBOInfo)
pb2wbo Formula
formula
  = ( PBFile.SoftFormula
      { wboTopCost :: Maybe Integer
PBFile.wboTopCost = Maybe Integer
forall a. Maybe a
Nothing
      , wboConstraints :: [(Maybe Integer, Constraint)]
PBFile.wboConstraints = [(Maybe Integer, Constraint)]
cs1 [(Maybe Integer, Constraint)]
-> [(Maybe Integer, Constraint)] -> [(Maybe Integer, Constraint)]
forall a. [a] -> [a] -> [a]
++ [(Maybe Integer, Constraint)]
cs2
      , wboNumVars :: Int
PBFile.wboNumVars = Formula -> Int
PBFile.pbNumVars Formula
formula
      , wboNumConstraints :: Int
PBFile.wboNumConstraints = Formula -> Int
PBFile.pbNumConstraints Formula
formula Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(Maybe Integer, Constraint)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Maybe Integer, Constraint)]
cs2
      }
    , Integer -> PB2WBOInfo
PB2WBOInfo Integer
offset
    )
  where
    cs1 :: [(Maybe Integer, Constraint)]
cs1 = [(Maybe Integer
forall a. Maybe a
Nothing, Constraint
c) | Constraint
c <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula]
    ([(Maybe Integer, Constraint)]
cs2, Integer
offset) =
      case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
        Maybe Sum
Nothing -> ([], Integer
0)
        Just Sum
e  ->
          ( [ if Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
              then (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
w,       ([(-Integer
1,[Int]
ls)], Op
PBFile.Ge, Integer
0))
              else (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Integer
forall a. Num a => a -> a
abs Integer
w), ([(Integer
1,[Int]
ls)],  Op
PBFile.Ge, Integer
1))
            | (Integer
w,[Int]
ls) <- Sum
e
            ]
          , [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [if Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Integer
0 else - Integer
w | (Integer
w, [Int]
_) <- Sum
e]
          )

newtype PB2WBOInfo = PB2WBOInfo Integer
  deriving (PB2WBOInfo -> PB2WBOInfo -> Bool
(PB2WBOInfo -> PB2WBOInfo -> Bool)
-> (PB2WBOInfo -> PB2WBOInfo -> Bool) -> Eq PB2WBOInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PB2WBOInfo -> PB2WBOInfo -> Bool
== :: PB2WBOInfo -> PB2WBOInfo -> Bool
$c/= :: PB2WBOInfo -> PB2WBOInfo -> Bool
/= :: PB2WBOInfo -> PB2WBOInfo -> Bool
Eq, Int -> PB2WBOInfo -> ShowS
[PB2WBOInfo] -> ShowS
PB2WBOInfo -> [Char]
(Int -> PB2WBOInfo -> ShowS)
-> (PB2WBOInfo -> [Char])
-> ([PB2WBOInfo] -> ShowS)
-> Show PB2WBOInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PB2WBOInfo -> ShowS
showsPrec :: Int -> PB2WBOInfo -> ShowS
$cshow :: PB2WBOInfo -> [Char]
show :: PB2WBOInfo -> [Char]
$cshowList :: [PB2WBOInfo] -> ShowS
showList :: [PB2WBOInfo] -> ShowS
Show)

instance Transformer PB2WBOInfo where
  type Source PB2WBOInfo = SAT.Model
  type Target PB2WBOInfo = SAT.Model

instance ForwardTransformer PB2WBOInfo where
  transformForward :: PB2WBOInfo -> Source PB2WBOInfo -> Target PB2WBOInfo
transformForward PB2WBOInfo
_ = Model -> Model
Source PB2WBOInfo -> Target PB2WBOInfo
forall a. a -> a
id

instance BackwardTransformer PB2WBOInfo where
  transformBackward :: PB2WBOInfo -> Target PB2WBOInfo -> Source PB2WBOInfo
transformBackward PB2WBOInfo
_ = Model -> Model
Target PB2WBOInfo -> Source PB2WBOInfo
forall a. a -> a
id

instance ObjValueTransformer PB2WBOInfo where
  type SourceObjValue PB2WBOInfo = Integer
  type TargetObjValue PB2WBOInfo = Integer

instance ObjValueForwardTransformer PB2WBOInfo where
  transformObjValueForward :: PB2WBOInfo
-> SourceObjValue PB2WBOInfo -> TargetObjValue PB2WBOInfo
transformObjValueForward (PB2WBOInfo Integer
offset) SourceObjValue PB2WBOInfo
obj = Integer
SourceObjValue PB2WBOInfo
obj Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
offset

instance ObjValueBackwardTransformer PB2WBOInfo where
  transformObjValueBackward :: PB2WBOInfo
-> TargetObjValue PB2WBOInfo -> SourceObjValue PB2WBOInfo
transformObjValueBackward (PB2WBOInfo Integer
offset) TargetObjValue PB2WBOInfo
obj = Integer
TargetObjValue PB2WBOInfo
obj Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
offset

instance J.ToJSON PB2WBOInfo where
  toJSON :: PB2WBOInfo -> Value
toJSON (PB2WBOInfo Integer
offset) =
    [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
.= Text -> Value
J.String Text
"PB2WBOInfo"
    , Key
"objective_function_offset" Key -> Integer -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Integer
offset
    ]

instance J.FromJSON PB2WBOInfo where
  parseJSON :: Value -> Parser PB2WBOInfo
parseJSON =
    [Char]
-> (Object -> Parser PB2WBOInfo) -> Value -> Parser PB2WBOInfo
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withTypedObject [Char]
"PB2WBOInfo" ((Object -> Parser PB2WBOInfo) -> Value -> Parser PB2WBOInfo)
-> (Object -> Parser PB2WBOInfo) -> Value -> Parser PB2WBOInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
      Integer
offset <- Object
obj Object -> Key -> Parser Integer
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"objective_function_offset"
      PB2WBOInfo -> Parser PB2WBOInfo
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> PB2WBOInfo
PB2WBOInfo Integer
offset)

wbo2pb :: PBFile.SoftFormula -> (PBFile.Formula, WBO2PBInfo)
wbo2pb :: SoftFormula -> (Formula, WBO2PBInfo)
wbo2pb SoftFormula
wbo = (forall s. ST s (Formula, WBO2PBInfo)) -> (Formula, WBO2PBInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Formula, WBO2PBInfo)) -> (Formula, WBO2PBInfo))
-> (forall s. ST s (Formula, WBO2PBInfo)) -> (Formula, WBO2PBInfo)
forall a b. (a -> b) -> a -> b
$ do
  let nv :: Int
nv = SoftFormula -> Int
PBFile.wboNumVars SoftFormula
wbo
  PBStore (ST s)
db <- ST s (PBStore (ST s))
forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
  (Sum
obj, VarMap Constraint
defs) <- PBStore (ST s) -> SoftFormula -> ST s (Sum, VarMap Constraint)
forall (m :: * -> *) enc.
(PrimMonad m, AddPBNL m enc) =>
enc -> SoftFormula -> m (Sum, VarMap Constraint)
addWBO PBStore (ST s)
db SoftFormula
wbo
  Formula
formula <- PBStore (ST s) -> ST s Formula
forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
  (Formula, WBO2PBInfo) -> ST s (Formula, WBO2PBInfo)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return
    ( Formula
formula{ PBFile.pbObjectiveFunction = Just obj }
    , Int -> Int -> VarMap Constraint -> WBO2PBInfo
WBO2PBInfo Int
nv (Formula -> Int
PBFile.pbNumVars Formula
formula) VarMap Constraint
defs
    )

data WBO2PBInfo = WBO2PBInfo !Int !Int (SAT.VarMap PBFile.Constraint)
  deriving (Int -> WBO2PBInfo -> ShowS
[WBO2PBInfo] -> ShowS
WBO2PBInfo -> [Char]
(Int -> WBO2PBInfo -> ShowS)
-> (WBO2PBInfo -> [Char])
-> ([WBO2PBInfo] -> ShowS)
-> Show WBO2PBInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WBO2PBInfo -> ShowS
showsPrec :: Int -> WBO2PBInfo -> ShowS
$cshow :: WBO2PBInfo -> [Char]
show :: WBO2PBInfo -> [Char]
$cshowList :: [WBO2PBInfo] -> ShowS
showList :: [WBO2PBInfo] -> ShowS
Show, WBO2PBInfo -> WBO2PBInfo -> Bool
(WBO2PBInfo -> WBO2PBInfo -> Bool)
-> (WBO2PBInfo -> WBO2PBInfo -> Bool) -> Eq WBO2PBInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WBO2PBInfo -> WBO2PBInfo -> Bool
== :: WBO2PBInfo -> WBO2PBInfo -> Bool
$c/= :: WBO2PBInfo -> WBO2PBInfo -> Bool
/= :: WBO2PBInfo -> WBO2PBInfo -> Bool
Eq)

instance Transformer WBO2PBInfo where
  type Source WBO2PBInfo = SAT.Model
  type Target WBO2PBInfo = SAT.Model

instance ForwardTransformer WBO2PBInfo where
  transformForward :: WBO2PBInfo -> Source WBO2PBInfo -> Target WBO2PBInfo
transformForward (WBO2PBInfo Int
_nv1 Int
nv2 VarMap Constraint
defs) Source WBO2PBInfo
m =
    (Int, Int) -> [(Int, Bool)] -> Model
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1, Int
nv2) ([(Int, Bool)] -> Model) -> [(Int, Bool)] -> Model
forall a b. (a -> b) -> a -> b
$ Model -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
Source WBO2PBInfo
m [(Int, Bool)] -> [(Int, Bool)] -> [(Int, Bool)]
forall a. [a] -> [a] -> [a]
++ [(Int
v, Model -> Constraint -> Bool
forall m. IModel m => m -> Constraint -> Bool
SAT.evalPBConstraint Model
Source WBO2PBInfo
m Constraint
constr) | (Int
v, Constraint
constr) <- VarMap Constraint -> [(Int, Constraint)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList VarMap Constraint
defs]

instance BackwardTransformer WBO2PBInfo where
  transformBackward :: WBO2PBInfo -> Target WBO2PBInfo -> Source WBO2PBInfo
transformBackward (WBO2PBInfo Int
nv1 Int
_nv2 VarMap Constraint
_defs) = Int -> Model -> Model
SAT.restrictModel Int
nv1

instance ObjValueTransformer WBO2PBInfo where
  type SourceObjValue WBO2PBInfo = Integer
  type TargetObjValue WBO2PBInfo = Integer

instance ObjValueForwardTransformer WBO2PBInfo where
  transformObjValueForward :: WBO2PBInfo
-> SourceObjValue WBO2PBInfo -> TargetObjValue WBO2PBInfo
transformObjValueForward WBO2PBInfo
_ = Integer -> Integer
SourceObjValue WBO2PBInfo -> TargetObjValue WBO2PBInfo
forall a. a -> a
id

instance ObjValueBackwardTransformer WBO2PBInfo where
  transformObjValueBackward :: WBO2PBInfo
-> TargetObjValue WBO2PBInfo -> SourceObjValue WBO2PBInfo
transformObjValueBackward WBO2PBInfo
_ = Integer -> Integer
TargetObjValue WBO2PBInfo -> SourceObjValue WBO2PBInfo
forall a. a -> a
id

instance J.ToJSON WBO2PBInfo where
  toJSON :: WBO2PBInfo -> Value
toJSON (WBO2PBInfo Int
nv1 Int
nv2 VarMap Constraint
defs) =
    [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
.= Text -> Value
J.String Text
"WBO2PBInfo"
    , Key
"num_original_variables" Key -> Int -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Int
nv1
    , Key
"num_transformed_variables" Key -> Int -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Int
nv2
    , Key
"definitions" 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
        [ Int -> Key
forall a. IsString a => Int -> a
jVarName Int
v Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Constraint -> Value
jPBConstraint Constraint
constr
        | (Int
v, Constraint
constr) <- VarMap Constraint -> [(Int, Constraint)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList VarMap Constraint
defs
        ]
    ]

instance J.FromJSON WBO2PBInfo where
  parseJSON :: Value -> Parser WBO2PBInfo
parseJSON = [Char]
-> (Object -> Parser WBO2PBInfo) -> Value -> Parser WBO2PBInfo
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withTypedObject [Char]
"WBO2PBInfo" ((Object -> Parser WBO2PBInfo) -> Value -> Parser WBO2PBInfo)
-> (Object -> Parser WBO2PBInfo) -> Value -> Parser WBO2PBInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    Map Text Value
defs <- Object
obj Object -> Key -> Parser (Map Text Value)
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"definitions"
    Int -> Int -> VarMap Constraint -> WBO2PBInfo
WBO2PBInfo
      (Int -> Int -> VarMap Constraint -> WBO2PBInfo)
-> Parser Int -> Parser (Int -> VarMap Constraint -> WBO2PBInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Int
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_original_variables"
      Parser (Int -> VarMap Constraint -> WBO2PBInfo)
-> Parser Int -> Parser (VarMap Constraint -> WBO2PBInfo)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser Int
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_transformed_variables"
      Parser (VarMap Constraint -> WBO2PBInfo)
-> Parser (VarMap Constraint) -> Parser WBO2PBInfo
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([(Int, Constraint)] -> VarMap Constraint
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Constraint)] -> VarMap Constraint)
-> Parser [(Int, Constraint)] -> Parser (VarMap Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Text, Value) -> Parser (Int, Constraint))
-> [(Text, Value)] -> Parser [(Int, Constraint)]
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 (Int, Constraint)
f (Map Text Value -> [(Text, Value)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Text Value
defs))
    where
      f :: (Text, Value) -> Parser (Int, Constraint)
f (Text
name, Value
constr) = do
        Int
v <- Text -> Parser Int
parseVarNameText Text
name
        Constraint
constr' <- Value -> Parser Constraint
parsePBConstraint Value
constr
        (Int, Constraint) -> Parser (Int, Constraint)
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
v, Constraint
constr')

addWBO :: (PrimMonad m, SAT.AddPBNL m enc) => enc -> PBFile.SoftFormula -> m (SAT.PBSum, (SAT.VarMap PBFile.Constraint))
addWBO :: forall (m :: * -> *) enc.
(PrimMonad m, AddPBNL m enc) =>
enc -> SoftFormula -> m (Sum, VarMap Constraint)
addWBO enc
db SoftFormula
wbo = do
  enc -> Int -> m ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ enc
db (Int -> m ()) -> Int -> m ()
forall a b. (a -> b) -> a -> b
$ SoftFormula -> Int
PBFile.wboNumVars SoftFormula
wbo

  MutVar (PrimState m) Sum
objRef <- Sum -> m (MutVar (PrimState m) Sum)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar []
  MutVar (PrimState m) Integer
objOffsetRef <- Integer -> m (MutVar (PrimState m) Integer)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Integer
0
  MutVar (PrimState m) [(Int, Constraint)]
defsRef <- [(Int, Constraint)] -> m (MutVar (PrimState m) [(Int, Constraint)])
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar []
  MutVar (PrimState m) Int
trueLitRef <- Int -> m (MutVar (PrimState m) Int)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Int
SAT.litUndef

  [(Maybe Integer, Constraint)]
-> ((Maybe Integer, Constraint) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (SoftFormula -> [(Maybe Integer, Constraint)]
PBFile.wboConstraints SoftFormula
wbo) (((Maybe Integer, Constraint) -> m ()) -> m ())
-> ((Maybe Integer, Constraint) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \(Maybe Integer
cost, constr :: Constraint
constr@(Sum
lhs,Op
op,Integer
rhs)) -> do
    case Maybe Integer
cost of
      Maybe Integer
Nothing -> do
        case Op
op of
          Op
PBFile.Ge -> enc -> Sum -> Integer -> m ()
forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLAtLeast enc
db Sum
lhs Integer
rhs
          Op
PBFile.Eq -> enc -> Sum -> Integer -> m ()
forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly enc
db Sum
lhs Integer
rhs
        Int
trueLit <- MutVar (PrimState m) Int -> m Int
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Int
trueLitRef
        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
trueLit Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
SAT.litUndef) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
          case Constraint -> Maybe Int
detectTrueLit Constraint
constr of
            Maybe Int
Nothing -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just Int
l -> MutVar (PrimState m) Int -> Int -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar MutVar (PrimState m) Int
trueLitRef Int
l
      Just Integer
w -> do
        case Op
op of
          Op
PBFile.Ge -> do
            case Sum
lhs of
              [(Integer
c,[Int]
ls)] | Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
&& (Integer
rhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
c Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 -> do
                -- c ∧L ≥ rhs ⇔ ∧L ≥ ⌈rhs / c⌉
                -- ∧L ≥ 1 ⇔ ∧L
                -- obj += w * (1 - ∧L)
                Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
ls) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
                  MutVar (PrimState m) Sum -> (Sum -> Sum) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef (\Sum
obj -> (-Integer
w,[Int]
ls) (Integer, [Int]) -> Sum -> Sum
forall a. a -> [a] -> [a]
: Sum
obj)
                  MutVar (PrimState m) Integer -> (Integer -> Integer) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Integer
objOffsetRef (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
w)
              [(Integer
c,[Int]
ls)] | Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
&& (Integer
rhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer -> Integer
forall a. Num a => a -> a
abs Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer -> Integer
forall a. Num a => a -> a
abs Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 -> do
                -- c*∧L ≥ rhs ⇔ -1*∧L ≥ ⌈rhs / abs c⌉ ⇔ (1 - ∧L) ≥ ⌈rhs / abs c⌉ + 1 ⇔ ¬∧L ≥ ⌈rhs / abs c⌉ + 1
                -- ￢∧L ≥ 1 ⇔ ￢∧L
                -- obj += w * ∧L
                if [Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
ls then do
                  MutVar (PrimState m) Integer -> (Integer -> Integer) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Integer
objOffsetRef (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
w)
                else do
                  MutVar (PrimState m) Sum -> (Sum -> Sum) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef ((Integer
w,[Int]
ls) (Integer, [Int]) -> Sum -> Sum
forall a. a -> [a] -> [a]
:)
              Sum
_ | Integer
rhs Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
rhs Bool -> Bool -> Bool
&& [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
ls Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 | (Integer
c,[Int]
ls) <- Sum
lhs] -> do
                -- ∑L ≥ 1 ⇔ ∨L ⇔ ￢∧￢L
                -- obj += w * ∧￢L
                if Sum -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Sum
lhs then do
                  MutVar (PrimState m) Integer -> (Integer -> Integer) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Integer
objOffsetRef (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
w)
                else do
                  MutVar (PrimState m) Sum -> (Sum -> Sum) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef ((Integer
w, [-Int
l | (Integer
_,[Int
l]) <- Sum
lhs]) (Integer, [Int]) -> Sum -> Sum
forall a. a -> [a] -> [a]
:)
              Sum
_ -> do
                Int
sel <- enc -> m Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar enc
db
                enc -> Int -> Sum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> Int -> Sum -> Integer -> m ()
SAT.addPBNLAtLeastSoft enc
db Int
sel Sum
lhs Integer
rhs
                MutVar (PrimState m) Sum -> (Sum -> Sum) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef ((Integer
w,[-Int
sel]) (Integer, [Int]) -> Sum -> Sum
forall a. a -> [a] -> [a]
:)
                MutVar (PrimState m) [(Int, Constraint)]
-> ([(Int, Constraint)] -> [(Int, Constraint)]) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) [(Int, Constraint)]
defsRef ((Int
sel,Constraint
constr) (Int, Constraint) -> [(Int, Constraint)] -> [(Int, Constraint)]
forall a. a -> [a] -> [a]
:)
          Op
PBFile.Eq -> do
            Int
sel <- enc -> m Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar enc
db
            enc -> Int -> Sum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> Int -> Sum -> Integer -> m ()
SAT.addPBNLExactlySoft enc
db Int
sel Sum
lhs Integer
rhs
            MutVar (PrimState m) Sum -> (Sum -> Sum) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef ((Integer
w,[-Int
sel]) (Integer, [Int]) -> Sum -> Sum
forall a. a -> [a] -> [a]
:)
            MutVar (PrimState m) [(Int, Constraint)]
-> ([(Int, Constraint)] -> [(Int, Constraint)]) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) [(Int, Constraint)]
defsRef ((Int
sel,Constraint
constr) (Int, Constraint) -> [(Int, Constraint)] -> [(Int, Constraint)]
forall a. a -> [a] -> [a]
:)

  Integer
offset <- MutVar (PrimState m) Integer -> m Integer
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Integer
objOffsetRef
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
offset Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    Int
l <- MutVar (PrimState m) Int -> m Int
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Int
trueLitRef
    Int
trueLit <-
      if Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
SAT.litUndef then
        Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
l
      else do
        Int
v <- enc -> m Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar enc
db
        enc -> [Int] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause enc
db [Int
v]
        MutVar (PrimState m) [(Int, Constraint)]
-> ([(Int, Constraint)] -> [(Int, Constraint)]) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) [(Int, Constraint)]
defsRef ((Int
v, ([], Op
PBFile.Ge, Integer
0)) (Int, Constraint) -> [(Int, Constraint)] -> [(Int, Constraint)]
forall a. a -> [a] -> [a]
:)
        Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
v
    MutVar (PrimState m) Sum -> (Sum -> Sum) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) Sum
objRef ((Integer
offset,[Int
trueLit]) (Integer, [Int]) -> Sum -> Sum
forall a. a -> [a] -> [a]
:)

  Sum
obj <- (Sum -> Sum) -> m Sum -> m Sum
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Sum -> Sum
forall a. [a] -> [a]
reverse (m Sum -> m Sum) -> m Sum -> m Sum
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) Sum -> m Sum
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Sum
objRef
  VarMap Constraint
defs <- ([(Int, Constraint)] -> VarMap Constraint)
-> m [(Int, Constraint)] -> m (VarMap Constraint)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Int, Constraint)] -> VarMap Constraint
forall a. [(Int, a)] -> IntMap a
IntMap.fromList (m [(Int, Constraint)] -> m (VarMap Constraint))
-> m [(Int, Constraint)] -> m (VarMap Constraint)
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) [(Int, Constraint)] -> m [(Int, Constraint)]
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) [(Int, Constraint)]
defsRef

  case SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
wbo of
    Maybe Integer
Nothing -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Integer
t -> enc -> Sum -> Integer -> m ()
forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLAtMost enc
db Sum
obj (Integer
t Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)

  (Sum, VarMap Constraint) -> m (Sum, VarMap Constraint)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sum
obj, VarMap Constraint
defs)


detectTrueLit :: PBFile.Constraint -> Maybe SAT.Lit
detectTrueLit :: Constraint -> Maybe Int
detectTrueLit (Sum
lhs, Op
op, Integer
rhs) =
  case Op
op of
    Op
PBFile.Ge -> Sum -> Integer -> Maybe Int
forall {a} {a}. (Integral a, Num a) => [(a, [a])] -> a -> Maybe a
f Sum
lhs Integer
rhs
    Op
PBFile.Eq -> Sum -> Integer -> Maybe Int
forall {a} {a}. (Integral a, Num a) => [(a, [a])] -> a -> Maybe a
f Sum
lhs Integer
rhs Maybe Int -> Maybe Int -> Maybe Int
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Sum -> Integer -> Maybe Int
forall {a} {a}. (Integral a, Num a) => [(a, [a])] -> a -> Maybe a
f [(- Integer
c, [Int]
ls) | (Integer
c,[Int]
ls) <- Sum
lhs] (- Integer
rhs)
  where
    f :: [(a, [a])] -> a -> Maybe a
f [(a
c, [a
l])] a
rhs
      | a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 Bool -> Bool -> Bool
&& (a
rhs a -> a -> a
forall a. Num a => a -> a -> a
+ a
c a -> a -> a
forall a. Num a => a -> a -> a
- a
1) a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
1 =
          -- c l ≥ rhs ↔ l ≥ ⌈rhs / c⌉
          a -> Maybe a
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return a
l
      | a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 Bool -> Bool -> Bool
&& a
rhs a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 =
          -- c l ≥ rhs ↔ l ≤ ⌊rhs / c⌋
          a -> Maybe a
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (- a
l)
    f [(a, [a])]
_ a
_ = Maybe a
forall a. Maybe a
Nothing

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

type SAT2PBInfo = IdentityTransformer SAT.Model

sat2pb :: CNF.CNF -> (PBFile.Formula, SAT2PBInfo)
sat2pb :: CNF -> (Formula, SAT2PBInfo)
sat2pb CNF
cnf
  = ( PBFile.Formula
      { pbObjectiveFunction :: Maybe Sum
PBFile.pbObjectiveFunction = Maybe Sum
forall a. Maybe a
Nothing
      , pbConstraints :: [Constraint]
PBFile.pbConstraints = (PackedClause -> Constraint) -> [PackedClause] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map PackedClause -> Constraint
forall {a} {c}.
(Num a, Num c) =>
PackedClause -> ([(a, [Int])], Op, c)
f (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf)
      , pbNumVars :: Int
PBFile.pbNumVars = CNF -> Int
CNF.cnfNumVars CNF
cnf
      , pbNumConstraints :: Int
PBFile.pbNumConstraints = CNF -> Int
CNF.cnfNumClauses CNF
cnf
      }
    , SAT2PBInfo
forall a. IdentityTransformer a
IdentityTransformer
    )
  where
    f :: PackedClause -> ([(a, [Int])], Op, c)
f PackedClause
clause = ([(a
1,[Int
l]) | Int
l <- PackedClause -> [Int]
SAT.unpackClause PackedClause
clause], Op
PBFile.Ge, c
1)

type PB2SATInfo = TseitinInfo

-- | Convert a pseudo boolean formula φ to a equisatisfiable CNF formula ψ
-- together with two functions f and g such that:
--
-- * if M ⊨ φ then f(M) ⊨ ψ
--
-- * if M ⊨ ψ then g(M) ⊨ φ
--
pb2sat :: PBFile.Formula -> (CNF.CNF, PB2SATInfo)
pb2sat :: Formula -> (CNF, TseitinInfo)
pb2sat = Strategy -> Formula -> (CNF, TseitinInfo)
pb2satWith Strategy
forall a. Default a => a
def

pb2satWith :: PB.Strategy -> PBFile.Formula -> (CNF.CNF, PB2SATInfo)
pb2satWith :: Strategy -> Formula -> (CNF, TseitinInfo)
pb2satWith Strategy
strategy Formula
formula = (forall s. ST s (CNF, TseitinInfo)) -> (CNF, TseitinInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (CNF, TseitinInfo)) -> (CNF, TseitinInfo))
-> (forall s. ST s (CNF, TseitinInfo)) -> (CNF, TseitinInfo)
forall a b. (a -> b) -> a -> b
$ do
  CNFStore (ST s)
db <- ST s (CNFStore (ST s))
forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore
  let nv1 :: Int
nv1 = Formula -> Int
PBFile.pbNumVars Formula
formula
  CNFStore (ST s) -> Int -> ST s ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ CNFStore (ST s)
db Int
nv1
  Encoder (ST s)
tseitin <-  CNFStore (ST s) -> ST s (Encoder (ST s))
forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder CNFStore (ST s)
db
  Encoder (ST s)
pb <- Encoder (ST s) -> Strategy -> ST s (Encoder (ST s))
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Strategy -> m (Encoder m)
PB.newEncoderWithStrategy Encoder (ST s)
tseitin Strategy
strategy
  Encoder (ST s)
pbnlc <- Encoder (ST s) -> Encoder (ST s) -> ST s (Encoder (ST s))
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Encoder m -> m (Encoder m)
PBNLC.newEncoder Encoder (ST s)
pb Encoder (ST s)
tseitin
  [Constraint] -> (Constraint -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Formula -> [Constraint]
PBFile.pbConstraints Formula
formula) ((Constraint -> ST s ()) -> ST s ())
-> (Constraint -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \(Sum
lhs,Op
op,Integer
rhs) -> do
    case Op
op of
      Op
PBFile.Ge -> Encoder (ST s) -> Sum -> Integer -> ST s ()
forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLAtLeast Encoder (ST s)
pbnlc Sum
lhs Integer
rhs
      Op
PBFile.Eq -> Encoder (ST s) -> Sum -> Integer -> ST s ()
forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly Encoder (ST s)
pbnlc Sum
lhs Integer
rhs
  CNF
cnf <- CNFStore (ST s) -> ST s CNF
forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula CNFStore (ST s)
db
  VarMap Formula
defs <- Encoder (ST s) -> ST s (VarMap Formula)
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m (VarMap Formula)
Tseitin.getDefinitions Encoder (ST s)
tseitin
  (CNF, TseitinInfo) -> ST s (CNF, TseitinInfo)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (CNF
cnf, Int -> Int -> VarMap Formula -> TseitinInfo
TseitinInfo Int
nv1 (CNF -> Int
CNF.cnfNumVars CNF
cnf) VarMap Formula
defs)

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

type MaxSAT2WBOInfo = PBIdentityInfo

maxsat2wbo :: CNF.WCNF -> (PBFile.SoftFormula, MaxSAT2WBOInfo)
maxsat2wbo :: WCNF -> (SoftFormula, PBIdentityInfo)
maxsat2wbo
  CNF.WCNF
  { wcnfTopCost :: WCNF -> Integer
CNF.wcnfTopCost = Integer
top
  , wcnfClauses :: WCNF -> [WeightedClause]
CNF.wcnfClauses = [WeightedClause]
cs
  , wcnfNumVars :: WCNF -> Int
CNF.wcnfNumVars = Int
nv
  , wcnfNumClauses :: WCNF -> Int
CNF.wcnfNumClauses = Int
nc
  } =
  ( PBFile.SoftFormula
    { wboTopCost :: Maybe Integer
PBFile.wboTopCost = Maybe Integer
forall a. Maybe a
Nothing
    , wboConstraints :: [(Maybe Integer, Constraint)]
PBFile.wboConstraints = (WeightedClause -> (Maybe Integer, Constraint))
-> [WeightedClause] -> [(Maybe Integer, Constraint)]
forall a b. (a -> b) -> [a] -> [b]
map WeightedClause -> (Maybe Integer, Constraint)
f [WeightedClause]
cs
    , wboNumVars :: Int
PBFile.wboNumVars = Int
nv
    , wboNumConstraints :: Int
PBFile.wboNumConstraints = Int
nc
    }
  , PBIdentityInfo
PBIdentityInfo
  )
  where
    f :: WeightedClause -> (Maybe Integer, Constraint)
f (Integer
w,PackedClause
c)
     | Integer
wInteger -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>=Integer
top    = (Maybe Integer
forall a. Maybe a
Nothing, Constraint
p) -- hard constraint
     | Bool
otherwise = (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
w, Constraint
p)  -- soft constraint
     where
       p :: Constraint
p = ([(Integer
1,[Int
l]) | Int
l <- PackedClause -> [Int]
SAT.unpackClause PackedClause
c], Op
PBFile.Ge, Integer
1)

type WBO2MaxSATInfo = PBTseitinInfo

wbo2maxsat :: PBFile.SoftFormula -> (CNF.WCNF, WBO2MaxSATInfo)
wbo2maxsat :: SoftFormula -> (WCNF, PBTseitinInfo)
wbo2maxsat = Strategy -> SoftFormula -> (WCNF, PBTseitinInfo)
wbo2maxsatWith Strategy
forall a. Default a => a
def

wbo2maxsatWith :: PB.Strategy -> PBFile.SoftFormula -> (CNF.WCNF, WBO2MaxSATInfo)
wbo2maxsatWith :: Strategy -> SoftFormula -> (WCNF, PBTseitinInfo)
wbo2maxsatWith Strategy
strategy SoftFormula
formula = (forall s. ST s (WCNF, PBTseitinInfo)) -> (WCNF, PBTseitinInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (WCNF, PBTseitinInfo)) -> (WCNF, PBTseitinInfo))
-> (forall s. ST s (WCNF, PBTseitinInfo)) -> (WCNF, PBTseitinInfo)
forall a b. (a -> b) -> a -> b
$ do
  CNFStore (ST s)
db <- ST s (CNFStore (ST s))
forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore
  CNFStore (ST s) -> Int -> ST s ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ CNFStore (ST s)
db (SoftFormula -> Int
PBFile.wboNumVars SoftFormula
formula)
  Encoder (ST s)
tseitin <-  CNFStore (ST s) -> ST s (Encoder (ST s))
forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder CNFStore (ST s)
db
  Encoder (ST s)
pb <- Encoder (ST s) -> Strategy -> ST s (Encoder (ST s))
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Strategy -> m (Encoder m)
PB.newEncoderWithStrategy Encoder (ST s)
tseitin Strategy
strategy
  Encoder (ST s)
pbnlc <- Encoder (ST s) -> Encoder (ST s) -> ST s (Encoder (ST s))
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Encoder m -> m (Encoder m)
PBNLC.newEncoder Encoder (ST s)
pb Encoder (ST s)
tseitin

  Seq WeightedClause
softClauses <- ([Seq WeightedClause] -> Seq WeightedClause)
-> ST s [Seq WeightedClause] -> ST s (Seq WeightedClause)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Seq WeightedClause] -> Seq WeightedClause
forall a. Monoid a => [a] -> a
mconcat (ST s [Seq WeightedClause] -> ST s (Seq WeightedClause))
-> ST s [Seq WeightedClause] -> ST s (Seq WeightedClause)
forall a b. (a -> b) -> a -> b
$ [(Maybe Integer, Constraint)]
-> ((Maybe Integer, Constraint) -> ST s (Seq WeightedClause))
-> ST s [Seq WeightedClause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (SoftFormula -> [(Maybe Integer, Constraint)]
PBFile.wboConstraints SoftFormula
formula) (((Maybe Integer, Constraint) -> ST s (Seq WeightedClause))
 -> ST s [Seq WeightedClause])
-> ((Maybe Integer, Constraint) -> ST s (Seq WeightedClause))
-> ST s [Seq WeightedClause]
forall a b. (a -> b) -> a -> b
$ \(Maybe Integer
cost, (Sum
lhs,Op
op,Integer
rhs)) -> do
    case Maybe Integer
cost of
      Maybe Integer
Nothing ->
        case Op
op of
          Op
PBFile.Ge -> Encoder (ST s) -> Sum -> Integer -> ST s ()
forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLAtLeast Encoder (ST s)
pbnlc Sum
lhs Integer
rhs ST s () -> ST s (Seq WeightedClause) -> ST s (Seq WeightedClause)
forall a b. ST s a -> ST s b -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Seq WeightedClause -> ST s (Seq WeightedClause)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Seq WeightedClause
forall a. Monoid a => a
mempty
          Op
PBFile.Eq -> Encoder (ST s) -> Sum -> Integer -> ST s ()
forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLExactly Encoder (ST s)
pbnlc Sum
lhs Integer
rhs ST s () -> ST s (Seq WeightedClause) -> ST s (Seq WeightedClause)
forall a b. ST s a -> ST s b -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Seq WeightedClause -> ST s (Seq WeightedClause)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Seq WeightedClause
forall a. Monoid a => a
mempty
      Just Integer
c -> do
        case Op
op of
          Op
PBFile.Ge -> do
            PBLinSum
lhs2 <- Encoder (ST s) -> Polarity -> Sum -> ST s PBLinSum
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Sum -> m PBLinSum
PBNLC.linearizePBSumWithPolarity Encoder (ST s)
pbnlc Polarity
Tseitin.polarityPos Sum
lhs
            let (PBLinSum
lhs3,Integer
rhs3) = (PBLinSum, Integer) -> (PBLinSum, Integer)
SAT.normalizePBLinAtLeast (PBLinSum
lhs2,Integer
rhs)
            if Integer
rhs3Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
1 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
cInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
1 | (Integer
c,Int
_) <- PBLinSum
lhs3] then
              Seq WeightedClause -> ST s (Seq WeightedClause)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Seq WeightedClause -> ST s (Seq WeightedClause))
-> Seq WeightedClause -> ST s (Seq WeightedClause)
forall a b. (a -> b) -> a -> b
$ WeightedClause -> Seq WeightedClause
forall a. a -> Seq a
Seq.singleton (Integer
c, [Int] -> PackedClause
SAT.packClause [Int
l | (Integer
_,Int
l) <- PBLinSum
lhs3])
            else do
              Int
lit <- Encoder (ST s) -> (PBLinSum, Integer) -> ST s Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Int
PB.encodePBLinAtLeast Encoder (ST s)
pb (PBLinSum
lhs3,Integer
rhs3)
              Seq WeightedClause -> ST s (Seq WeightedClause)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Seq WeightedClause -> ST s (Seq WeightedClause))
-> Seq WeightedClause -> ST s (Seq WeightedClause)
forall a b. (a -> b) -> a -> b
$ WeightedClause -> Seq WeightedClause
forall a. a -> Seq a
Seq.singleton (Integer
c, [Int] -> PackedClause
SAT.packClause [Int
lit])
          Op
PBFile.Eq -> do
            PBLinSum
lhs2 <- Encoder (ST s) -> Polarity -> Sum -> ST s PBLinSum
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Sum -> m PBLinSum
PBNLC.linearizePBSumWithPolarity Encoder (ST s)
pbnlc Polarity
Tseitin.polarityBoth Sum
lhs
            Int
lit1 <- Encoder (ST s) -> (PBLinSum, Integer) -> ST s Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Int
PB.encodePBLinAtLeast Encoder (ST s)
pb (PBLinSum
lhs2, Integer
rhs)
            Int
lit2 <- Encoder (ST s) -> (PBLinSum, Integer) -> ST s Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Int
PB.encodePBLinAtLeast Encoder (ST s)
pb ([(-Integer
c, Int
l) | (Integer
c,Int
l) <- PBLinSum
lhs2], Integer -> Integer
forall a. Num a => a -> a
negate Integer
rhs)
            Int
lit <- Encoder (ST s) -> Polarity -> [Int] -> ST s Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Int] -> m Int
Tseitin.encodeConjWithPolarity Encoder (ST s)
tseitin Polarity
Tseitin.polarityPos [Int
lit1,Int
lit2]
            Seq WeightedClause -> ST s (Seq WeightedClause)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Seq WeightedClause -> ST s (Seq WeightedClause))
-> Seq WeightedClause -> ST s (Seq WeightedClause)
forall a b. (a -> b) -> a -> b
$ WeightedClause -> Seq WeightedClause
forall a. a -> Seq a
Seq.singleton (Integer
c, [Int] -> PackedClause
SAT.packClause [Int
lit])

  case SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
formula of
    Maybe Integer
Nothing -> () -> ST s ()
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Integer
top -> Encoder (ST s) -> Sum -> Integer -> ST s ()
forall (m :: * -> *) a. AddPBNL m a => a -> Sum -> Integer -> m ()
SAT.addPBNLAtMost Encoder (ST s)
pbnlc [(Integer
c, [-Int
l | Int
l <- PackedClause -> [Int]
SAT.unpackClause PackedClause
clause]) | (Integer
c,PackedClause
clause) <- Seq WeightedClause -> [WeightedClause]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq WeightedClause
softClauses] (Integer
top Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)

  let top :: Integer
top = Seq Integer -> Integer
forall a. Num a => Seq a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
F.sum (WeightedClause -> Integer
forall a b. (a, b) -> a
fst (WeightedClause -> Integer) -> Seq WeightedClause -> Seq Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq WeightedClause
softClauses) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
  CNF
cnf <- CNFStore (ST s) -> ST s CNF
forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula CNFStore (ST s)
db
  let cs :: Seq WeightedClause
cs = Seq WeightedClause
softClauses Seq WeightedClause -> Seq WeightedClause -> Seq WeightedClause
forall a. Semigroup a => a -> a -> a
<> [WeightedClause] -> Seq WeightedClause
forall a. [a] -> Seq a
Seq.fromList [(Integer
top, PackedClause
clause) | PackedClause
clause <- CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf]
  let wcnf :: WCNF
wcnf = CNF.WCNF
             { wcnfNumVars :: Int
CNF.wcnfNumVars = CNF -> Int
CNF.cnfNumVars CNF
cnf
             , wcnfNumClauses :: Int
CNF.wcnfNumClauses = Seq WeightedClause -> Int
forall a. Seq a -> Int
Seq.length Seq WeightedClause
cs
             , wcnfTopCost :: Integer
CNF.wcnfTopCost = Integer
top
             , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = Seq WeightedClause -> [WeightedClause]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq WeightedClause
cs
             }
  VarMap Formula
defs <- Encoder (ST s) -> ST s (VarMap Formula)
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m (VarMap Formula)
Tseitin.getDefinitions Encoder (ST s)
tseitin
  (WCNF, PBTseitinInfo) -> ST s (WCNF, PBTseitinInfo)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (WCNF
wcnf, TseitinInfo -> PBTseitinInfo
PBTseitinInfo (Int -> Int -> VarMap Formula -> TseitinInfo
TseitinInfo (SoftFormula -> Int
PBFile.wboNumVars SoftFormula
formula) (CNF -> Int
CNF.cnfNumVars CNF
cnf) VarMap Formula
defs))

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

pb2lsp :: PBFile.Formula -> Builder
pb2lsp :: Formula -> Builder
pb2lsp Formula
formula =
  ByteString -> Builder
byteString ByteString
"function model() {\n" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
decls Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
constrs Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
obj2 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
"}\n"
  where
    nv :: Int
nv = Formula -> Int
PBFile.pbNumVars Formula
formula

    decls :: Builder
decls = ByteString -> Builder
byteString ByteString
"  for [i in 1.." Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
nv Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
"] x[i] <- bool();\n"

    constrs :: Builder
constrs = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
      [ ByteString -> Builder
byteString ByteString
"  constraint " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Constraint -> Builder
showConstrLSP Constraint
c Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Builder
";\n"
      | Constraint
c <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula
      ]

    obj2 :: Builder
obj2 =
      case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
        Just Sum
obj' -> ByteString -> Builder
byteString ByteString
"  minimize " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Sum -> Builder
showSumLSP Sum
obj' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
";\n"
        Maybe Sum
Nothing -> Builder
forall a. Monoid a => a
mempty

wbo2lsp :: PBFile.SoftFormula -> Builder
wbo2lsp :: SoftFormula -> Builder
wbo2lsp SoftFormula
softFormula =
  ByteString -> Builder
byteString ByteString
"function model() {\n" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
decls Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
constrs Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
costDef Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
topConstr Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  ByteString -> Builder
byteString ByteString
"  minimize cost;\n}\n"
  where
    nv :: Int
nv = SoftFormula -> Int
PBFile.wboNumVars SoftFormula
softFormula

    decls :: Builder
decls = ByteString -> Builder
byteString ByteString
"  for [i in 1.." Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
nv Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
"] x[i] <- bool();\n"

    constrs :: Builder
constrs = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
      [ ByteString -> Builder
byteString ByteString
"  constraint " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Constraint -> Builder
showConstrLSP Constraint
c Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Builder
";\n"
      | (Maybe Integer
Nothing, Constraint
c) <- SoftFormula -> [(Maybe Integer, Constraint)]
PBFile.wboConstraints SoftFormula
softFormula
      ]

    costDef :: Builder
costDef = ByteString -> Builder
byteString ByteString
"  cost <- sum(\n" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
s Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
");\n"
      where
        s :: Builder
s = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ([Builder] -> Builder)
-> ([Builder] -> [Builder]) -> [Builder] -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
intersperse (Builder
",\n") ([Builder] -> Builder) -> [Builder] -> Builder
forall a b. (a -> b) -> a -> b
$ [Builder]
xs
        xs :: [Builder]
xs = [Builder
"    " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
w Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"*!(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Constraint -> Builder
showConstrLSP Constraint
c Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
             | (Just Integer
w, Constraint
c) <- SoftFormula -> [(Maybe Integer, Constraint)]
PBFile.wboConstraints SoftFormula
softFormula]

    topConstr :: Builder
topConstr =
      case SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
softFormula of
        Maybe Integer
Nothing -> Builder
forall a. Monoid a => a
mempty
        Just Integer
t -> ByteString -> Builder
byteString ByteString
"  constraint cost <= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
t Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
";\n"

showConstrLSP :: PBFile.Constraint -> Builder
showConstrLSP :: Constraint -> Builder
showConstrLSP (Sum
lhs, Op
PBFile.Ge, Integer
1) | [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
cInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
1 | (Integer
c,[Int]
_) <- Sum
lhs] =
  Builder
"or(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat (Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
intersperse Builder
"," (((Integer, [Int]) -> Builder) -> Sum -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map ([Int] -> Builder
f ([Int] -> Builder)
-> ((Integer, [Int]) -> [Int]) -> (Integer, [Int]) -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, [Int]) -> [Int]
forall a b. (a, b) -> b
snd) Sum
lhs)) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  where
    f :: [Int] -> Builder
f [Int
l] = Int -> Builder
showLitLSP Int
l
    f [Int]
ls  = Builder
"and(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat (Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
intersperse Builder
"," ((Int -> Builder) -> [Int] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Builder
showLitLSP [Int]
ls)) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
showConstrLSP (Sum
lhs, Op
op, Integer
rhs) = Sum -> Builder
showSumLSP Sum
lhs  Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
op2 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
rhs
  where
    op2 :: Builder
op2 = case Op
op of
            Op
PBFile.Ge -> Builder
" >= "
            Op
PBFile.Eq -> Builder
" == "

sum' :: [Builder] -> Builder
sum' :: [Builder] -> Builder
sum' [Builder]
xs = Builder
"sum(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat (Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
intersperse Builder
", " [Builder]
xs) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

showSumLSP :: PBFile.Sum -> Builder
showSumLSP :: Sum -> Builder
showSumLSP = [Builder] -> Builder
sum' ([Builder] -> Builder) -> (Sum -> [Builder]) -> Sum -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Integer, [Int]) -> Builder) -> Sum -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, [Int]) -> Builder
showTermLSP

showTermLSP :: PBFile.WeightedTerm -> Builder
showTermLSP :: (Integer, [Int]) -> Builder
showTermLSP (Integer
n,[Int]
ls) = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ([Builder] -> Builder) -> [Builder] -> Builder
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
intersperse Builder
"*" ([Builder] -> [Builder]) -> [Builder] -> [Builder]
forall a b. (a -> b) -> a -> b
$ [Integer -> Builder
integerDec Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
1] [Builder] -> [Builder] -> [Builder]
forall a. [a] -> [a] -> [a]
++ [Int -> Builder
showLitLSP Int
l | Int
l<-[Int]
ls]

showLitLSP :: PBFile.Lit -> Builder
showLitLSP :: Int -> Builder
showLitLSP Int
l =
  if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
  then Builder
"!x[" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec (Int -> Int
forall a. Num a => a -> a
abs Int
l) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"]"
  else Builder
"x[" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
l Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"]"

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

pb2smp :: Bool -> PBFile.Formula -> Builder
pb2smp :: Bool -> Formula -> Builder
pb2smp Bool
isUnix Formula
formula =
  Builder
header Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
decls Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Char -> Builder
char7 Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
obj2 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Char -> Builder
char7 Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
constrs Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Char -> Builder
char7 Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
actions Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
  Builder
footer
  where
    nv :: Int
nv = Formula -> Int
PBFile.pbNumVars Formula
formula

    header :: Builder
header =
      if Bool
isUnix
      then ByteString -> Builder
byteString ByteString
"#include \"simple.h\"\nvoid ufun()\n{\n\n"
      else Builder
forall a. Monoid a => a
mempty

    footer :: Builder
footer =
      if Bool
isUnix
      then Builder
"\n}\n"
      else Builder
forall a. Monoid a => a
mempty

    actions :: Builder
actions = ByteString -> Builder
byteString (ByteString -> Builder) -> ByteString -> Builder
forall a b. (a -> b) -> a -> b
$
      ByteString
"solve();\n" ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<>
      ByteString
"x[i].val.print();\n" ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<>
      ByteString
"cost.val.print();\n"

    decls :: Builder
decls =
      ByteString -> Builder
byteString ByteString
"Element i(set=\"1 .. " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
nv Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
      ByteString -> Builder
byteString ByteString
"\");\nIntegerVariable x(type=binary, index=i);\n"

    constrs :: Builder
constrs = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
      [ Sum -> Builder
showSum Sum
lhs Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Builder
op2 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Integer -> Builder
integerDec Integer
rhs Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Builder
";\n"
      | (Sum
lhs, Op
op, Integer
rhs) <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula
      , let op2 :: Builder
op2 = case Op
op of
                    Op
PBFile.Ge -> Builder
" >= "
                    Op
PBFile.Eq -> Builder
" == "
      ]

    showSum :: PBFile.Sum -> Builder
    showSum :: Sum -> Builder
showSum [] = Char -> Builder
char7 Char
'0'
    showSum Sum
xs = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ([Builder] -> Builder) -> [Builder] -> Builder
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
intersperse Builder
" + " ([Builder] -> [Builder]) -> [Builder] -> [Builder]
forall a b. (a -> b) -> a -> b
$ ((Integer, [Int]) -> Builder) -> Sum -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, [Int]) -> Builder
showTerm Sum
xs

    showTerm :: (Integer, [Int]) -> Builder
showTerm (Integer
n,[Int]
ls) = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ([Builder] -> Builder) -> [Builder] -> Builder
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
intersperse (Char -> Builder
char7 Char
'*') ([Builder] -> [Builder]) -> [Builder] -> [Builder]
forall a b. (a -> b) -> a -> b
$ Integer -> [Builder]
showCoeff Integer
n [Builder] -> [Builder] -> [Builder]
forall a. [a] -> [a] -> [a]
++ [Int -> Builder
showLit Int
l | Int
l<-[Int]
ls]

    showCoeff :: Integer -> [Builder]
showCoeff Integer
n
      | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1    = []
      | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = [Char -> Builder
char7 Char
'(' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
')']
      | Bool
otherwise = [Integer -> Builder
integerDec Integer
n]

    showLit :: Int -> Builder
showLit Int
l =
      if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
      then Builder
"(1-x[" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec (Int -> Int
forall a. Num a => a -> a
abs Int
l) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"])"
      else Builder
"x[" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
l Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"]"

    obj2 :: Builder
obj2 =
      case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
        Just Sum
obj' ->
          ByteString -> Builder
byteString ByteString
"Objective cost(type=minimize);\ncost = " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Sum -> Builder
showSum Sum
obj' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
";\n"
        Maybe Sum
Nothing -> Builder
forall a. Monoid a => a
mempty

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