{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.PB
-- Copyright   :  (c) Masahiro Sakai 2013,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

  -- * 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
  , PB2SATInfo

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

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

import Control.Monad
import Control.Monad.Primitive
import Control.Monad.ST
import Data.Array.IArray
import Data.Bits
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
#if !MIN_VERSION_base(4,11,0)
import Data.Monoid
#endif
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 ToySolver.Data.BoolExpr
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import qualified ToySolver.SAT.Encoder.PB as PB
import qualified ToySolver.SAT.Encoder.PBNLC as PBNLC
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
  { pbConstraints :: [Constraint]
PBFile.pbConstraints =
      (Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> Constraint
normalizePBConstraint (Formula -> [Constraint]
PBFile.pbConstraints Formula
formula)
  }

normalizeWBO :: PBFile.SoftFormula -> PBFile.SoftFormula
normalizeWBO :: SoftFormula -> SoftFormula
normalizeWBO SoftFormula
formula =
  SoftFormula
formula
  { wboConstraints :: [SoftConstraint]
PBFile.wboConstraints =
      (SoftConstraint -> SoftConstraint)
-> [SoftConstraint] -> [SoftConstraint]
forall a b. (a -> b) -> [a] -> [b]
map (\(Maybe Integer
w,Constraint
constr) -> (Maybe Integer
w, Constraint -> Constraint
normalizePBConstraint Constraint
constr)) (SoftFormula -> [SoftConstraint]
PBFile.wboConstraints SoftFormula
formula)
  }

normalizePBConstraint :: PBFile.Constraint -> PBFile.Constraint
normalizePBConstraint :: Constraint -> Constraint
normalizePBConstraint (Sum
lhs,Op
op,Integer
rhs) =
  case (Integer -> (Integer, [Lit]) -> (Integer, (Integer, [Lit])))
-> Integer -> Sum -> (Integer, Sum)
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL Integer -> (Integer, [Lit]) -> (Integer, (Integer, [Lit]))
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)

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

type PBLinearizeInfo = TseitinInfo

linearizePB :: PBFile.Formula -> Bool -> (PBFile.Formula, PBLinearizeInfo)
linearizePB :: Formula -> Bool -> (Formula, PBLinearizeInfo)
linearizePB Formula
formula Bool
usePB = (forall s. ST s (Formula, PBLinearizeInfo))
-> (Formula, PBLinearizeInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Formula, PBLinearizeInfo))
 -> (Formula, PBLinearizeInfo))
-> (forall s. ST s (Formula, PBLinearizeInfo))
-> (Formula, PBLinearizeInfo)
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) -> Lit -> ST s ()
forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ PBStore (ST s)
db (Formula -> Lit
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 (m :: * -> *) a. Monad m => a -> m a
return ([(Integer
c,[Lit
l]) | (Integer
c,Lit
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 (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 (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, [Lit
l]) | (Integer
c,Lit
l) <- PBLinSum
obj']
  Formula
formula' <- PBStore (ST s) -> ST s Formula
forall (m :: * -> *). PrimMonad m => PBStore m -> m Formula
getPBFormula PBStore (ST s)
db
  [(Lit, Formula)]
defs <- Encoder (ST s) -> ST s [(Lit, Formula)]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m [(Lit, Formula)]
Tseitin.getDefinitions Encoder (ST s)
tseitin
  (Formula, PBLinearizeInfo) -> ST s (Formula, PBLinearizeInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Formula, PBLinearizeInfo) -> ST s (Formula, PBLinearizeInfo))
-> (Formula, PBLinearizeInfo) -> ST s (Formula, PBLinearizeInfo)
forall a b. (a -> b) -> a -> b
$
    ( Formula
formula'
      { pbObjectiveFunction :: Maybe Sum
PBFile.pbObjectiveFunction = Maybe Sum
obj'
      , pbConstraints :: [Constraint]
PBFile.pbConstraints = [Constraint]
cs' [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ Formula -> [Constraint]
PBFile.pbConstraints Formula
formula'
      , pbNumConstraints :: Lit
PBFile.pbNumConstraints = Formula -> Lit
PBFile.pbNumConstraints Formula
formula Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+ Formula -> Lit
PBFile.pbNumConstraints Formula
formula'
      }
    , Lit -> Lit -> [(Lit, Formula)] -> PBLinearizeInfo
TseitinInfo (Formula -> Lit
PBFile.pbNumVars Formula
formula) (Formula -> Lit
PBFile.pbNumVars Formula
formula') [(Lit, Formula)]
defs
    )

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

linearizeWBO :: PBFile.SoftFormula -> Bool -> (PBFile.SoftFormula, PBLinearizeInfo)
linearizeWBO :: SoftFormula -> Bool -> (SoftFormula, PBLinearizeInfo)
linearizeWBO SoftFormula
formula Bool
usePB = (forall s. ST s (SoftFormula, PBLinearizeInfo))
-> (SoftFormula, PBLinearizeInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (SoftFormula, PBLinearizeInfo))
 -> (SoftFormula, PBLinearizeInfo))
-> (forall s. ST s (SoftFormula, PBLinearizeInfo))
-> (SoftFormula, PBLinearizeInfo)
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) -> Lit -> ST s ()
forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ PBStore (ST s)
db (SoftFormula -> Lit
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
  [SoftConstraint]
cs' <- [SoftConstraint]
-> (SoftConstraint -> ST s SoftConstraint) -> ST s [SoftConstraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (SoftFormula -> [SoftConstraint]
PBFile.wboConstraints SoftFormula
formula) ((SoftConstraint -> ST s SoftConstraint) -> ST s [SoftConstraint])
-> (SoftConstraint -> ST s SoftConstraint) -> ST s [SoftConstraint]
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
    SoftConstraint -> ST s SoftConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer
cost,([(Integer
c,[Lit
l]) | (Integer
c,Lit
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
  [(Lit, Formula)]
defs <- Encoder (ST s) -> ST s [(Lit, Formula)]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m [(Lit, Formula)]
Tseitin.getDefinitions Encoder (ST s)
tseitin
  (SoftFormula, PBLinearizeInfo)
-> ST s (SoftFormula, PBLinearizeInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return ((SoftFormula, PBLinearizeInfo)
 -> ST s (SoftFormula, PBLinearizeInfo))
-> (SoftFormula, PBLinearizeInfo)
-> ST s (SoftFormula, PBLinearizeInfo)
forall a b. (a -> b) -> a -> b
$
    ( SoftFormula :: Maybe Integer -> [SoftConstraint] -> Lit -> Lit -> SoftFormula
PBFile.SoftFormula
      { wboTopCost :: Maybe Integer
PBFile.wboTopCost = SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
formula
      , wboConstraints :: [SoftConstraint]
PBFile.wboConstraints = [SoftConstraint]
cs' [SoftConstraint] -> [SoftConstraint] -> [SoftConstraint]
forall a. [a] -> [a] -> [a]
++ [(Maybe Integer
forall a. Maybe a
Nothing, Constraint
constr) | Constraint
constr <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula']
      , wboNumVars :: Lit
PBFile.wboNumVars = Formula -> Lit
PBFile.pbNumVars Formula
formula'
      , wboNumConstraints :: Lit
PBFile.wboNumConstraints = SoftFormula -> Lit
PBFile.wboNumConstraints SoftFormula
formula Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+ Formula -> Lit
PBFile.pbNumConstraints Formula
formula'
      }
    , Lit -> Lit -> [(Lit, Formula)] -> PBLinearizeInfo
TseitinInfo (SoftFormula -> Lit
PBFile.wboNumVars SoftFormula
formula) (Formula -> Lit
PBFile.pbNumVars Formula
formula') [(Lit, Formula)]
defs
    )

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

-- | Quandratize PBO/PBS problem without introducing additional constraints.
quadratizePB :: PBFile.Formula -> ((PBFile.Formula, Integer), PBQuadratizeInfo)
quadratizePB :: Formula -> ((Formula, Integer), PBQuadratizeInfo)
quadratizePB Formula
formula = (Formula, Integer) -> ((Formula, Integer), PBQuadratizeInfo)
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), PBQuadratizeInfo)
quadratizePB' (Formula
formula, Integer
maxObj) =
  ( ( Formula :: Maybe Sum -> [Constraint] -> Lit -> Lit -> Formula
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 :: Lit
PBFile.pbNumVars = Lit
nv2
      , pbNumConstraints :: Lit
PBFile.pbNumConstraints = Formula -> Lit
PBFile.pbNumConstraints Formula
formula
      }
    , Integer
maxObj
    )
  , PBLinearizeInfo -> PBQuadratizeInfo
PBQuadratizeInfo (PBLinearizeInfo -> PBQuadratizeInfo)
-> PBLinearizeInfo -> PBQuadratizeInfo
forall a b. (a -> b) -> a -> b
$ Lit -> Lit -> [(Lit, Formula)] -> PBLinearizeInfo
TseitinInfo Lit
nv1 Lit
nv2 [(Lit
v, [Formula] -> Formula
forall a. [BoolExpr a] -> BoolExpr a
And [Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
l1, Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
l2]) | (Lit
v, (Lit
l1,Lit
l2)) <- [(Lit, (Lit, Lit))]
prodDefs]
  )
  where
    nv1 :: Lit
nv1 = Formula -> Lit
PBFile.pbNumVars Formula
formula
    nv2 :: Lit
nv2 = Formula -> Lit
PBFile.pbNumVars Formula
formula Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+ Set IntSet -> Lit
forall a. Set a -> Lit
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 -> Lit
IntSet.size IntSet
t Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
< Lit
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 Lit
toV) = ([(Lit, IntSet)] -> IntMap IntSet
forall a. [(Lit, a)] -> IntMap a
IntMap.fromList [(Lit, IntSet)]
l, [(IntSet, Lit)] -> Map IntSet Lit
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(IntSet
s,Lit
v) | (Lit
v,IntSet
s) <- [(Lit, IntSet)]
l])
      where
        l :: [(Lit, IntSet)]
l = [Lit] -> [IntSet] -> [(Lit, IntSet)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Formula -> Lit
PBFile.pbNumVars Formula
formula Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+ Lit
1 ..] (Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
termsToReplace)

    prodDefs :: [(SAT.Var, (SAT.Var, SAT.Var))]
    prodDefs :: [(Lit, (Lit, Lit))]
prodDefs = [(Lit
v, (IntSet -> Lit
f IntSet
t1, IntSet -> Lit
f IntSet
t2)) | (Lit
v,IntSet
t) <- IntMap IntSet -> [(Lit, IntSet)]
forall a. IntMap a -> [(Lit, 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 -> Lit
f IntSet
t
          | IntSet -> Lit
IntSet.size IntSet
t Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
1 = [Lit] -> Lit
forall a. [a] -> a
head (IntSet -> [Lit]
IntSet.toList IntSet
t)
          | Bool
otherwise =
               case IntSet -> Map IntSet Lit -> Maybe Lit
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IntSet
t Map IntSet Lit
toV of
                 Maybe Lit
Nothing -> [Char] -> Lit
forall a. HasCallStack => [Char] -> a
error [Char]
"quadratizePB.prodDefs: should not happen"
                 Just Lit
v -> Lit
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, [Lit]
ts) | (Integer
w,[Lit]
ts) <- [Sum] -> Sum
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Lit -> Lit -> Lit -> Sum
forall a a. Num a => a -> a -> a -> [(a, [a])]
p Lit
x Lit
y Lit
z | (Lit
z,(Lit
x,Lit
y)) <- [(Lit, (Lit, Lit))]
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, [Lit] -> [Lit]
f [Lit]
t) | (Integer
w,[Lit]
t) <- Sum
s]
      where
        f :: [Lit] -> [Lit]
f [Lit]
t =
          case IntSet -> Map IntSet Lit -> Maybe Lit
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IntSet
t' Map IntSet Lit
toV of
            Just Lit
v  -> [Lit
v]
            Maybe Lit
Nothing
              | IntSet -> Lit
IntSet.size IntSet
t' Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
>= Lit
3 -> (IntSet -> Lit) -> [IntSet] -> [Lit]
forall a b. (a -> b) -> [a] -> [b]
map IntSet -> Lit
g [IntSet
t1, IntSet
t2]
              | Bool
otherwise -> [Lit]
t
          where
            t' :: IntSet
t' = [Lit] -> IntSet
IntSet.fromList [Lit]
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 -> Lit
g IntSet
t
          | IntSet -> Lit
IntSet.size IntSet
t Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
1 = [Lit] -> Lit
forall a. [a] -> a
head ([Lit] -> Lit) -> [Lit] -> Lit
forall a b. (a -> b) -> a -> b
$ IntSet -> [Lit]
IntSet.toList IntSet
t
          | Bool
otherwise = Map IntSet Lit
toV Map IntSet Lit -> IntSet -> Lit
forall k a. Ord k => Map k a -> k -> a
Map.! IntSet
t


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' | [Lit]
t <- [[Lit]]
terms, let t' :: IntSet
t' = [Lit] -> IntSet
IntSet.fromList [Lit]
t, IntSet -> Lit
IntSet.size IntSet
t' Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
>= Lit
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 :: [[Lit]]
terms = [[Lit]
t | Sum
s <- [Sum]
sums, (Integer
_,[Lit]
t) <- Sum
s]

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

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

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

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

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

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

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

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

-- | 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) -> Lit -> ST s ()
forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ PBStore (ST s)
db (Formula -> Lit
PBFile.pbNumVars Formula
formula)

  [(Sum, Integer, [Lit])]
defs <- ([Maybe (Sum, Integer, [Lit])] -> [(Sum, Integer, [Lit])])
-> ST s [Maybe (Sum, Integer, [Lit])]
-> ST s [(Sum, Integer, [Lit])]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Maybe (Sum, Integer, [Lit])] -> [(Sum, Integer, [Lit])]
forall a. [Maybe a] -> [a]
catMaybes (ST s [Maybe (Sum, Integer, [Lit])]
 -> ST s [(Sum, Integer, [Lit])])
-> ST s [Maybe (Sum, Integer, [Lit])]
-> ST s [(Sum, Integer, [Lit])]
forall a b. (a -> b) -> a -> b
$ [Constraint]
-> (Constraint -> ST s (Maybe (Sum, Integer, [Lit])))
-> ST s [Maybe (Sum, Integer, [Lit])]
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, [Lit])))
 -> ST s [Maybe (Sum, Integer, [Lit])])
-> (Constraint -> ST s (Maybe (Sum, Integer, [Lit])))
-> ST s [Maybe (Sum, Integer, [Lit])]
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, [Lit]) -> ST s (Maybe (Sum, Integer, [Lit]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Sum, Integer, [Lit])
forall a. Maybe a
Nothing
      (Sum
lhs, Op
PBFile.Ge, Integer
rhs) -> do
        case (Sum, Integer) -> Maybe [Lit]
asClause (Sum
lhs,Integer
rhs) of
          Just [Lit]
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, [- Lit
l | Lit
l <- [Lit]
clause])] Integer
0
            Maybe (Sum, Integer, [Lit]) -> ST s (Maybe (Sum, Integer, [Lit]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Sum, Integer, [Lit])
forall a. Maybe a
Nothing
          Maybe [Lit]
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 :: Lit
maxSurpassNBits = [Lit] -> Lit
forall a. [a] -> a
head [Lit
i | Lit
i <- [Lit
0..], Integer
maxSurpass Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Lit -> Integer
forall a. Bits a => Lit -> a
bit Lit
i]
            [Lit]
vs <- PBStore (ST s) -> Lit -> ST s [Lit]
forall (m :: * -> *) a. NewVar m a => a -> Lit -> m [Lit]
SAT.newVars PBStore (ST s)
db Lit
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,[Lit
x]) | (Integer
c,Lit
x) <- [Integer] -> [Lit] -> 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) [Lit]
vs]) Integer
rhs
            if Lit
maxSurpassNBits Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
> Lit
0 then do
              Maybe (Sum, Integer, [Lit]) -> ST s (Maybe (Sum, Integer, [Lit]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Sum, Integer, [Lit]) -> ST s (Maybe (Sum, Integer, [Lit])))
-> Maybe (Sum, Integer, [Lit])
-> ST s (Maybe (Sum, Integer, [Lit]))
forall a b. (a -> b) -> a -> b
$ (Sum, Integer, [Lit]) -> Maybe (Sum, Integer, [Lit])
forall a. a -> Maybe a
Just (Sum
lhs, Integer
rhs, [Lit]
vs)
            else
              Maybe (Sum, Integer, [Lit]) -> ST s (Maybe (Sum, Integer, [Lit]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Sum, Integer, [Lit])
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 (m :: * -> *) a. Monad m => a -> m a
return
    ( Formula
formula'{ pbObjectiveFunction :: Maybe Sum
PBFile.pbObjectiveFunction = Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula }
    , Lit
-> Lit -> [(Sum, Integer, [Lit])] -> PBInequalitiesToEqualitiesInfo
PBInequalitiesToEqualitiesInfo (Formula -> Lit
PBFile.pbNumVars Formula
formula) (Formula -> Lit
PBFile.pbNumVars Formula
formula') [(Sum, Integer, [Lit])]
defs
    )
  where
    asLinSum :: SAT.PBSum -> Maybe (SAT.PBLinSum, Integer)
    asLinSum :: Sum -> Maybe (PBLinSum, Integer)
asLinSum Sum
s = do
      [(Maybe (Integer, Lit), Integer)]
ret <- Sum
-> ((Integer, [Lit]) -> Maybe (Maybe (Integer, Lit), Integer))
-> Maybe [(Maybe (Integer, Lit), Integer)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Sum
s (((Integer, [Lit]) -> Maybe (Maybe (Integer, Lit), Integer))
 -> Maybe [(Maybe (Integer, Lit), Integer)])
-> ((Integer, [Lit]) -> Maybe (Maybe (Integer, Lit), Integer))
-> Maybe [(Maybe (Integer, Lit), Integer)]
forall a b. (a -> b) -> a -> b
$ \(Integer
c, [Lit]
ls) -> do
        case [Lit]
ls of
          [] -> (Maybe (Integer, Lit), Integer)
-> Maybe (Maybe (Integer, Lit), Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Integer, Lit)
forall a. Maybe a
Nothing, Integer
c)
          [Lit
l] -> (Maybe (Integer, Lit), Integer)
-> Maybe (Maybe (Integer, Lit), Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Integer, Lit) -> Maybe (Integer, Lit)
forall a. a -> Maybe a
Just (Integer
c,Lit
l), Integer
0)
          [Lit]
_ -> Maybe (Maybe (Integer, Lit), Integer)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      (PBLinSum, Integer) -> Maybe (PBLinSum, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe (Integer, Lit)] -> PBLinSum
forall a. [Maybe a] -> [a]
catMaybes (((Maybe (Integer, Lit), Integer) -> Maybe (Integer, Lit))
-> [(Maybe (Integer, Lit), Integer)] -> [Maybe (Integer, Lit)]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (Integer, Lit), Integer) -> Maybe (Integer, Lit)
forall a b. (a, b) -> a
fst [(Maybe (Integer, Lit), Integer)]
ret), [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (((Maybe (Integer, Lit), Integer) -> Integer)
-> [(Maybe (Integer, Lit), Integer)] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (Integer, Lit), Integer) -> Integer
forall a b. (a, b) -> b
snd [(Maybe (Integer, Lit), Integer)]
ret))

    asClause :: (SAT.PBSum, Integer) -> Maybe SAT.Clause
    asClause :: (Sum, Integer) -> Maybe [Lit]
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, Lit) -> Bool) -> PBLinSum -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Integer
c,Lit
_) -> Integer
c Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1) PBLinSum
lhs'' -> [Lit] -> Maybe [Lit]
forall (m :: * -> *) a. Monad m => a -> m a
return (((Integer, Lit) -> Lit) -> PBLinSum -> [Lit]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, Lit) -> Lit
forall a b. (a, b) -> b
snd PBLinSum
lhs'')
        (PBLinSum, Integer)
_ -> Maybe [Lit]
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
/= :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
$c/= :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
== :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
$c== :: PBInequalitiesToEqualitiesInfo
-> PBInequalitiesToEqualitiesInfo -> Bool
Eq, Lit -> PBInequalitiesToEqualitiesInfo -> ShowS
[PBInequalitiesToEqualitiesInfo] -> ShowS
PBInequalitiesToEqualitiesInfo -> [Char]
(Lit -> PBInequalitiesToEqualitiesInfo -> ShowS)
-> (PBInequalitiesToEqualitiesInfo -> [Char])
-> ([PBInequalitiesToEqualitiesInfo] -> ShowS)
-> Show PBInequalitiesToEqualitiesInfo
forall a.
(Lit -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [PBInequalitiesToEqualitiesInfo] -> ShowS
$cshowList :: [PBInequalitiesToEqualitiesInfo] -> ShowS
show :: PBInequalitiesToEqualitiesInfo -> [Char]
$cshow :: PBInequalitiesToEqualitiesInfo -> [Char]
showsPrec :: Lit -> PBInequalitiesToEqualitiesInfo -> ShowS
$cshowsPrec :: Lit -> 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 Lit
_nv1 Lit
nv2 [(Sum, Integer, [Lit])]
defs) Source PBInequalitiesToEqualitiesInfo
m =
    (Lit, Lit) -> [(Lit, Bool)] -> UArray Lit Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1, Lit
nv2) ([(Lit, Bool)] -> UArray Lit Bool)
-> [(Lit, Bool)] -> UArray Lit Bool
forall a b. (a -> b) -> a -> b
$ UArray Lit Bool -> [(Lit, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Lit Bool
Source PBInequalitiesToEqualitiesInfo
m [(Lit, Bool)] -> [(Lit, Bool)] -> [(Lit, Bool)]
forall a. [a] -> [a] -> [a]
++ [(Lit
v, Integer -> Lit -> Bool
forall a. Bits a => a -> Lit -> Bool
testBit Integer
n Lit
i) | (Sum
lhs, Integer
rhs, [Lit]
vs) <- [(Sum, Integer, [Lit])]
defs, let n :: Integer
n = UArray Lit Bool -> Sum -> Integer
forall m. IModel m => m -> Sum -> Integer
SAT.evalPBSum UArray Lit Bool
Source PBInequalitiesToEqualitiesInfo
m Sum
lhs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
rhs, (Lit
i,Lit
v) <- [Lit] -> [Lit] -> [(Lit, Lit)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Lit
0..] [Lit]
vs]

instance BackwardTransformer PBInequalitiesToEqualitiesInfo where
  transformBackward :: PBInequalitiesToEqualitiesInfo
-> Target PBInequalitiesToEqualitiesInfo
-> Source PBInequalitiesToEqualitiesInfo
transformBackward (PBInequalitiesToEqualitiesInfo Lit
nv1 Lit
_nv2 [(Sum, Integer, [Lit])]
_defs) = Lit -> UArray Lit Bool -> UArray Lit Bool
SAT.restrictModel Lit
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
_ = SourceObjValue PBInequalitiesToEqualitiesInfo
-> TargetObjValue PBInequalitiesToEqualitiesInfo
forall a. a -> a
id

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

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

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
/= :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
$c/= :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
== :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
$c== :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool
Eq, Lit -> PBUnconstrainInfo -> ShowS
[PBUnconstrainInfo] -> ShowS
PBUnconstrainInfo -> [Char]
(Lit -> PBUnconstrainInfo -> ShowS)
-> (PBUnconstrainInfo -> [Char])
-> ([PBUnconstrainInfo] -> ShowS)
-> Show PBUnconstrainInfo
forall a.
(Lit -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [PBUnconstrainInfo] -> ShowS
$cshowList :: [PBUnconstrainInfo] -> ShowS
show :: PBUnconstrainInfo -> [Char]
$cshow :: PBUnconstrainInfo -> [Char]
showsPrec :: Lit -> PBUnconstrainInfo -> ShowS
$cshowsPrec :: Lit -> 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

unconstrainPB' :: PBFile.Formula -> (PBFile.Formula, Integer)
unconstrainPB' :: Formula -> (Formula, Integer)
unconstrainPB' Formula
formula =
  ( Formula
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
obj1 Sum -> Sum -> Sum
forall a. [a] -> [a] -> [a]
++ Sum
obj2
    , pbConstraints :: [Constraint]
PBFile.pbConstraints = []
    , pbNumConstraints :: Lit
PBFile.pbNumConstraints = Lit
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 -> [Lit]
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, [Lit])] -> Map IntSet a
sq ((-Integer
rhs, []) (Integer, [Lit]) -> Sum -> Sum
forall a. a -> [a] -> [a]
: Sum
lhs) | (Sum
lhs, Op
PBFile.Eq, Integer
rhs) <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula]
    sq :: [(a, [Lit])] -> Map IntSet a
sq [(a, [Lit])]
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,[Lit]
ls1) <- [(a, [Lit])]
ts
              (a
c2,[Lit]
ls2) <- [(a, [Lit])]
ts
              let ls3 :: IntSet
ls3 = [Lit] -> IntSet
IntSet.fromList [Lit]
ls1 IntSet -> IntSet -> IntSet
`IntSet.union` [Lit] -> IntSet
IntSet.fromList [Lit]
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 (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` (Lit -> Lit) -> IntSet -> IntSet
IntSet.map Lit -> Lit
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 -> PBQuadratizeInfo -> PB2QUBOInfo'
forall a b. a -> b -> ComposedTransformer a b
ComposedTransformer PBUnconstrainInfo
info1 PBQuadratizeInfo
info2)
  where
    ((Formula
formula1, Integer
th1), PBUnconstrainInfo
info1) = Formula -> ((Formula, Integer), PBUnconstrainInfo)
unconstrainPB Formula
formula
    ((Formula
formula2, Integer
th2), PBQuadratizeInfo
info2) = (Formula, Integer) -> ((Formula, Integer), PBQuadratizeInfo)
quadratizePB' (Formula
formula1, Integer
th1)

type PB2QUBOInfo' = ComposedTransformer PBUnconstrainInfo PBQuadratizeInfo

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

type PB2WBOInfo = IdentityTransformer SAT.Model

pb2wbo :: PBFile.Formula -> (PBFile.SoftFormula, PB2WBOInfo)
pb2wbo :: Formula -> (SoftFormula, PB2WBOInfo)
pb2wbo Formula
formula
  = ( SoftFormula :: Maybe Integer -> [SoftConstraint] -> Lit -> Lit -> SoftFormula
PBFile.SoftFormula
      { wboTopCost :: Maybe Integer
PBFile.wboTopCost = Maybe Integer
forall a. Maybe a
Nothing
      , wboConstraints :: [SoftConstraint]
PBFile.wboConstraints = [SoftConstraint]
cs1 [SoftConstraint] -> [SoftConstraint] -> [SoftConstraint]
forall a. [a] -> [a] -> [a]
++ [SoftConstraint]
cs2
      , wboNumVars :: Lit
PBFile.wboNumVars = Formula -> Lit
PBFile.pbNumVars Formula
formula
      , wboNumConstraints :: Lit
PBFile.wboNumConstraints = Formula -> Lit
PBFile.pbNumConstraints Formula
formula Lit -> Lit -> Lit
forall a. Num a => a -> a -> a
+ [SoftConstraint] -> Lit
forall (t :: * -> *) a. Foldable t => t a -> Lit
length [SoftConstraint]
cs2
      }
    , PB2WBOInfo
forall a. IdentityTransformer a
IdentityTransformer
    )
  where
    cs1 :: [SoftConstraint]
cs1 = [(Maybe Integer
forall a. Maybe a
Nothing, Constraint
c) | Constraint
c <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula]
    cs2 :: [SoftConstraint]
cs2 = case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
            Maybe Sum
Nothing -> []
            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,[Lit]
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,[Lit]
ls)],  Op
PBFile.Ge, Integer
1))
              | (Integer
w,[Lit]
ls) <- Sum
e
              ]

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 :: Lit
nv = SoftFormula -> Lit
PBFile.wboNumVars SoftFormula
wbo
  PBStore (ST s)
db <- ST s (PBStore (ST s))
forall (m :: * -> *). PrimMonad m => m (PBStore m)
newPBStore
  (Sum
obj, [(Lit, Constraint)]
defs) <- PBStore (ST s) -> SoftFormula -> ST s (Sum, [(Lit, Constraint)])
forall (m :: * -> *) enc.
(PrimMonad m, AddPBNL m enc) =>
enc -> SoftFormula -> m (Sum, [(Lit, 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 (m :: * -> *) a. Monad m => a -> m a
return
    ( Formula
formula{ pbObjectiveFunction :: Maybe Sum
PBFile.pbObjectiveFunction = Sum -> Maybe Sum
forall a. a -> Maybe a
Just Sum
obj }
    , Lit -> Lit -> [(Lit, Constraint)] -> WBO2PBInfo
WBO2PBInfo Lit
nv (Formula -> Lit
PBFile.pbNumVars Formula
formula) [(Lit, Constraint)]
defs
    )

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

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 Lit
_nv1 Lit
nv2 [(Lit, Constraint)]
defs) Source WBO2PBInfo
m =
    (Lit, Lit) -> [(Lit, Bool)] -> UArray Lit Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1, Lit
nv2) ([(Lit, Bool)] -> UArray Lit Bool)
-> [(Lit, Bool)] -> UArray Lit Bool
forall a b. (a -> b) -> a -> b
$ UArray Lit Bool -> [(Lit, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Lit Bool
Source WBO2PBInfo
m [(Lit, Bool)] -> [(Lit, Bool)] -> [(Lit, Bool)]
forall a. [a] -> [a] -> [a]
++ [(Lit
v, UArray Lit Bool -> Constraint -> Bool
forall m. IModel m => m -> Constraint -> Bool
SAT.evalPBConstraint UArray Lit Bool
Source WBO2PBInfo
m Constraint
constr) | (Lit
v, Constraint
constr) <- [(Lit, Constraint)]
defs]

instance BackwardTransformer WBO2PBInfo where
  transformBackward :: WBO2PBInfo -> Target WBO2PBInfo -> Source WBO2PBInfo
transformBackward (WBO2PBInfo Lit
nv1 Lit
_nv2 [(Lit, Constraint)]
_defs) = Lit -> UArray Lit Bool -> UArray Lit Bool
SAT.restrictModel Lit
nv1

addWBO :: (PrimMonad m, SAT.AddPBNL m enc) => enc -> PBFile.SoftFormula -> m (SAT.PBSum, [(SAT.Var, PBFile.Constraint)])
addWBO :: enc -> SoftFormula -> m (Sum, [(Lit, Constraint)])
addWBO enc
db SoftFormula
wbo = do
  enc -> Lit -> m ()
forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ enc
db (Lit -> m ()) -> Lit -> m ()
forall a b. (a -> b) -> a -> b
$ SoftFormula -> Lit
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) [(Lit, Constraint)]
defsRef <- [(Lit, Constraint)] -> m (MutVar (PrimState m) [(Lit, Constraint)])
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar []
  MutVar (PrimState m) Lit
trueLitRef <- Lit -> m (MutVar (PrimState m) Lit)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Lit
SAT.litUndef

  [SoftConstraint] -> (SoftConstraint -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (SoftFormula -> [SoftConstraint]
PBFile.wboConstraints SoftFormula
wbo) ((SoftConstraint -> m ()) -> m ())
-> (SoftConstraint -> 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
        Lit
trueLit <- MutVar (PrimState m) Lit -> m Lit
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Lit
trueLitRef
        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Lit
trueLit Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
SAT.litUndef) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
          case Constraint -> Maybe Lit
detectTrueLit Constraint
constr of
            Maybe Lit
Nothing -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just Lit
l -> MutVar (PrimState m) Lit -> Lit -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar MutVar (PrimState m) Lit
trueLitRef Lit
l
      Just Integer
w -> do
        case Op
op of
          Op
PBFile.Ge -> do
            case Sum
lhs of
              [(Integer
c,[Lit]
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 ([Lit] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Lit]
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,[Lit]
ls) (Integer, [Lit]) -> 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,[Lit]
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 [Lit] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Lit]
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,[Lit]
ls) (Integer, [Lit]) -> 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
&& [Lit] -> Lit
forall (t :: * -> *) a. Foldable t => t a -> Lit
length [Lit]
ls Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
1 | (Integer
c,[Lit]
ls) <- Sum
lhs] -> do
                -- ∑L ≥ 1 ⇔ ∨L ⇔ ￢∧￢L
                -- obj += w * ∧￢L
                if Sum -> 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, [-Lit
l | (Integer
_,[Lit
l]) <- Sum
lhs]) (Integer, [Lit]) -> Sum -> Sum
forall a. a -> [a] -> [a]
:)
              Sum
_ -> do
                Lit
sel <- enc -> m Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar enc
db
                enc -> Lit -> Sum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> Lit -> Sum -> Integer -> m ()
SAT.addPBNLAtLeastSoft enc
db Lit
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,[-Lit
sel]) (Integer, [Lit]) -> Sum -> Sum
forall a. a -> [a] -> [a]
:)
                MutVar (PrimState m) [(Lit, Constraint)]
-> ([(Lit, Constraint)] -> [(Lit, Constraint)]) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) [(Lit, Constraint)]
defsRef ((Lit
sel,Constraint
constr) (Lit, Constraint) -> [(Lit, Constraint)] -> [(Lit, Constraint)]
forall a. a -> [a] -> [a]
:)
          Op
PBFile.Eq -> do
            Lit
sel <- enc -> m Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar enc
db
            enc -> Lit -> Sum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBNL m a =>
a -> Lit -> Sum -> Integer -> m ()
SAT.addPBNLExactlySoft enc
db Lit
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,[-Lit
sel]) (Integer, [Lit]) -> Sum -> Sum
forall a. a -> [a] -> [a]
:)
            MutVar (PrimState m) [(Lit, Constraint)]
-> ([(Lit, Constraint)] -> [(Lit, Constraint)]) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) [(Lit, Constraint)]
defsRef ((Lit
sel,Constraint
constr) (Lit, Constraint) -> [(Lit, Constraint)] -> [(Lit, 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
    Lit
l <- MutVar (PrimState m) Lit -> m Lit
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) Lit
trueLitRef
    Lit
trueLit <-
      if Lit
l Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
SAT.litUndef then
        Lit -> m Lit
forall (m :: * -> *) a. Monad m => a -> m a
return Lit
l
      else do
        Lit
v <- enc -> m Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar enc
db
        enc -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause enc
db [Lit
v]
        MutVar (PrimState m) [(Lit, Constraint)]
-> ([(Lit, Constraint)] -> [(Lit, Constraint)]) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar MutVar (PrimState m) [(Lit, Constraint)]
defsRef ((Lit
v, ([], Op
PBFile.Ge, Integer
0)) (Lit, Constraint) -> [(Lit, Constraint)] -> [(Lit, Constraint)]
forall a. a -> [a] -> [a]
:)
        Lit -> m Lit
forall (m :: * -> *) a. Monad m => a -> m a
return Lit
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,[Lit
trueLit]) (Integer, [Lit]) -> 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
  [(Lit, Constraint)]
defs <- ([(Lit, Constraint)] -> [(Lit, Constraint)])
-> m [(Lit, Constraint)] -> m [(Lit, Constraint)]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Lit, Constraint)] -> [(Lit, Constraint)]
forall a. [a] -> [a]
reverse (m [(Lit, Constraint)] -> m [(Lit, Constraint)])
-> m [(Lit, Constraint)] -> m [(Lit, Constraint)]
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) [(Lit, Constraint)] -> m [(Lit, Constraint)]
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) [(Lit, Constraint)]
defsRef

  case SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
wbo of
    Maybe Integer
Nothing -> () -> m ()
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, [(Lit, Constraint)]) -> m (Sum, [(Lit, Constraint)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sum
obj, [(Lit, Constraint)]
defs)


detectTrueLit :: PBFile.Constraint -> Maybe SAT.Lit
detectTrueLit :: Constraint -> Maybe Lit
detectTrueLit (Sum
lhs, Op
op, Integer
rhs) =
  case Op
op of
    Op
PBFile.Ge -> Sum -> Integer -> Maybe Lit
forall a a. (Integral a, Num a) => [(a, [a])] -> a -> Maybe a
f Sum
lhs Integer
rhs
    Op
PBFile.Eq -> Sum -> Integer -> Maybe Lit
forall a a. (Integral a, Num a) => [(a, [a])] -> a -> Maybe a
f Sum
lhs Integer
rhs Maybe Lit -> Maybe Lit -> Maybe Lit
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Sum -> Integer -> Maybe Lit
forall a a. (Integral a, Num a) => [(a, [a])] -> a -> Maybe a
f [(- Integer
c, [Lit]
ls) | (Integer
c,[Lit]
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 (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 (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, PB2WBOInfo)
sat2pb CNF
cnf
  = ( Formula :: Maybe Sum -> [Constraint] -> Lit -> Lit -> Formula
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, [Lit])], Op, c)
f (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf)
      , pbNumVars :: Lit
PBFile.pbNumVars = CNF -> Lit
CNF.cnfNumVars CNF
cnf
      , pbNumConstraints :: Lit
PBFile.pbNumConstraints = CNF -> Lit
CNF.cnfNumClauses CNF
cnf
      }
    , PB2WBOInfo
forall a. IdentityTransformer a
IdentityTransformer
    )
  where
    f :: PackedClause -> ([(a, [Lit])], Op, c)
f PackedClause
clause = ([(a
1,[Lit
l]) | Lit
l <- PackedClause -> [Lit]
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, PBLinearizeInfo)
pb2sat Formula
formula = (forall s. ST s (CNF, PBLinearizeInfo)) -> (CNF, PBLinearizeInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (CNF, PBLinearizeInfo)) -> (CNF, PBLinearizeInfo))
-> (forall s. ST s (CNF, PBLinearizeInfo))
-> (CNF, PBLinearizeInfo)
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 :: Lit
nv1 = Formula -> Lit
PBFile.pbNumVars Formula
formula
  CNFStore (ST s) -> Lit -> ST s ()
forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ CNFStore (ST s)
db Lit
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) -> ST s (Encoder (ST s))
forall (m :: * -> *). Monad m => Encoder m -> m (Encoder m)
PB.newEncoder Encoder (ST s)
tseitin
  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
  [(Lit, Formula)]
defs <- Encoder (ST s) -> ST s [(Lit, Formula)]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m [(Lit, Formula)]
Tseitin.getDefinitions Encoder (ST s)
tseitin
  (CNF, PBLinearizeInfo) -> ST s (CNF, PBLinearizeInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return (CNF
cnf, Lit -> Lit -> [(Lit, Formula)] -> PBLinearizeInfo
TseitinInfo Lit
nv1 (CNF -> Lit
CNF.cnfNumVars CNF
cnf) [(Lit, Formula)]
defs)

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

type MaxSAT2WBOInfo = IdentityTransformer SAT.Model

maxsat2wbo :: CNF.WCNF -> (PBFile.SoftFormula, MaxSAT2WBOInfo)
maxsat2wbo :: WCNF -> (SoftFormula, PB2WBOInfo)
maxsat2wbo
  CNF.WCNF
  { wcnfTopCost :: WCNF -> Integer
CNF.wcnfTopCost = Integer
top
  , wcnfClauses :: WCNF -> [WeightedClause]
CNF.wcnfClauses = [WeightedClause]
cs
  , wcnfNumVars :: WCNF -> Lit
CNF.wcnfNumVars = Lit
nv
  , wcnfNumClauses :: WCNF -> Lit
CNF.wcnfNumClauses = Lit
nc
  } =
  ( SoftFormula :: Maybe Integer -> [SoftConstraint] -> Lit -> Lit -> SoftFormula
PBFile.SoftFormula
    { wboTopCost :: Maybe Integer
PBFile.wboTopCost = Maybe Integer
forall a. Maybe a
Nothing
    , wboConstraints :: [SoftConstraint]
PBFile.wboConstraints = (WeightedClause -> SoftConstraint)
-> [WeightedClause] -> [SoftConstraint]
forall a b. (a -> b) -> [a] -> [b]
map WeightedClause -> SoftConstraint
f [WeightedClause]
cs
    , wboNumVars :: Lit
PBFile.wboNumVars = Lit
nv
    , wboNumConstraints :: Lit
PBFile.wboNumConstraints = Lit
nc
    }
  , PB2WBOInfo
forall a. IdentityTransformer a
IdentityTransformer
  )
  where
    f :: WeightedClause -> SoftConstraint
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,[Lit
l]) | Lit
l <- PackedClause -> [Lit]
SAT.unpackClause PackedClause
c], Op
PBFile.Ge, Integer
1)

type WBO2MaxSATInfo = TseitinInfo

wbo2maxsat :: PBFile.SoftFormula -> (CNF.WCNF, WBO2MaxSATInfo)
wbo2maxsat :: SoftFormula -> (WCNF, PBLinearizeInfo)
wbo2maxsat SoftFormula
formula = (forall s. ST s (WCNF, PBLinearizeInfo)) -> (WCNF, PBLinearizeInfo)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (WCNF, PBLinearizeInfo))
 -> (WCNF, PBLinearizeInfo))
-> (forall s. ST s (WCNF, PBLinearizeInfo))
-> (WCNF, PBLinearizeInfo)
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) -> Lit -> ST s ()
forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ CNFStore (ST s)
db (SoftFormula -> Lit
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) -> ST s (Encoder (ST s))
forall (m :: * -> *). Monad m => Encoder m -> m (Encoder m)
PB.newEncoder Encoder (ST s)
tseitin
  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
$ [SoftConstraint]
-> (SoftConstraint -> 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 -> [SoftConstraint]
PBFile.wboConstraints SoftFormula
formula) ((SoftConstraint -> ST s (Seq WeightedClause))
 -> ST s [Seq WeightedClause])
-> (SoftConstraint -> 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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Seq WeightedClause -> ST s (Seq WeightedClause)
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Seq WeightedClause -> ST s (Seq WeightedClause)
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,Lit
_) <- PBLinSum
lhs3] then
              Seq WeightedClause -> ST s (Seq WeightedClause)
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, [Lit] -> PackedClause
SAT.packClause [Lit
l | (Integer
_,Lit
l) <- PBLinSum
lhs3])
            else do
              Lit
lit <- Encoder (ST s) -> (PBLinSum, Integer) -> ST s Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Lit
PB.encodePBLinAtLeast Encoder (ST s)
pb (PBLinSum
lhs3,Integer
rhs3)
              Seq WeightedClause -> ST s (Seq WeightedClause)
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, [Lit] -> PackedClause
SAT.packClause [Lit
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
            Lit
lit1 <- Encoder (ST s) -> (PBLinSum, Integer) -> ST s Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Lit
PB.encodePBLinAtLeast Encoder (ST s)
pb (PBLinSum
lhs2, Integer
rhs)
            Lit
lit2 <- Encoder (ST s) -> (PBLinSum, Integer) -> ST s Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> (PBLinSum, Integer) -> m Lit
PB.encodePBLinAtLeast Encoder (ST s)
pb ([(-Integer
c, Lit
l) | (Integer
c,Lit
l) <- PBLinSum
lhs2], Integer -> Integer
forall a. Num a => a -> a
negate Integer
rhs)
            Lit
lit <- Encoder (ST s) -> Polarity -> [Lit] -> ST s Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Lit] -> m Lit
Tseitin.encodeConjWithPolarity Encoder (ST s)
tseitin Polarity
Tseitin.polarityPos [Lit
lit1,Lit
lit2]
            Seq WeightedClause -> ST s (Seq WeightedClause)
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, [Lit] -> PackedClause
SAT.packClause [Lit
lit])

  case SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
formula of
    Maybe Integer
Nothing -> () -> ST s ()
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, [-Lit
l | Lit
l <- PackedClause -> [Lit]
SAT.unpackClause PackedClause
clause]) | (Integer
c,PackedClause
clause) <- Seq WeightedClause -> [WeightedClause]
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 (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 = WCNF :: Lit -> Lit -> Integer -> [WeightedClause] -> WCNF
CNF.WCNF
             { wcnfNumVars :: Lit
CNF.wcnfNumVars = CNF -> Lit
CNF.cnfNumVars CNF
cnf
             , wcnfNumClauses :: Lit
CNF.wcnfNumClauses = Seq WeightedClause -> Lit
forall a. Seq a -> Lit
Seq.length Seq WeightedClause
cs
             , wcnfTopCost :: Integer
CNF.wcnfTopCost = Integer
top
             , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = Seq WeightedClause -> [WeightedClause]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq WeightedClause
cs
             }
  [(Lit, Formula)]
defs <- Encoder (ST s) -> ST s [(Lit, Formula)]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m [(Lit, Formula)]
Tseitin.getDefinitions Encoder (ST s)
tseitin
  (WCNF, PBLinearizeInfo) -> ST s (WCNF, PBLinearizeInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return (WCNF
wcnf, Lit -> Lit -> [(Lit, Formula)] -> PBLinearizeInfo
TseitinInfo (SoftFormula -> Lit
PBFile.wboNumVars SoftFormula
formula) (CNF -> Lit
CNF.cnfNumVars CNF
cnf) [(Lit, Formula)]
defs)

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