{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.PseudoBoolean.ByteStringBuilder
-- Copyright   :  (c) Masahiro Sakai 2011-2015
-- License     :  BSD-style
-- 
-- Maintainer  :  masahiro.sakai@gmail.com
-- Portability :  portable
--
-----------------------------------------------------------------------------

module Data.PseudoBoolean.ByteStringBuilder
  (
  -- * Builder for (Lazy) ByteString generation
    opbBuilder
  , wboBuilder

  -- * Lazy ByteString generation
  , toOPBByteString
  , toWBOByteString

  -- * File I/O
  , writeOPBFile
  , writeWBOFile
  , hPutOPB
  , hPutWBO
  ) where

import qualified Prelude
import Prelude hiding (sum)
import qualified Data.IntSet as IntSet
import qualified Data.Set as Set
import Data.List (sortBy)
import Data.Monoid hiding (Sum (..))
import qualified Data.ByteString.Lazy as BS
import Data.ByteString.Builder (Builder, intDec, integerDec, char7, string7, hPutBuilder, toLazyByteString)
import Data.Ord
import System.IO
import Data.PseudoBoolean.Types

-- | A ByteString Builder which renders a OPB format byte-string containing pseudo boolean problem.
opbBuilder :: Formula -> Builder
opbBuilder :: Formula -> Builder
opbBuilder Formula
opb = (Builder
size Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
part1 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
part2)
  where
    nv :: Lit
nv = Formula -> Lit
pbNumVars Formula
opb
    nc :: Lit
nc = Formula -> Lit
pbNumConstraints Formula
opb
    p :: Set IntSet
p = Formula -> Set IntSet
pbProducts Formula
opb
    np :: Lit
np = Set IntSet -> Lit
forall a. Set a -> Lit
Set.size Set IntSet
p
    sp :: Lit
sp = [Lit] -> Lit
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
Prelude.sum [IntSet -> Lit
IntSet.size IntSet
tm | IntSet
tm <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
p]
    size :: Builder
size = String -> Builder
string7 String
"* #variable= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec Lit
nv Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
string7 String
" #constraint= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec Lit
nc
         Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (if Lit
np Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
>= Lit
1 then String -> Builder
string7 String
" #product= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec Lit
np Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
string7 String
" sizeproduct= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec Lit
sp else Builder
forall a. Monoid a => a
mempty)
         Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
'\n'
    part1 :: Builder
part1 = 
      case Formula -> Maybe Sum
pbObjectiveFunction Formula
opb of
        Maybe Sum
Nothing -> Builder
forall a. Monoid a => a
mempty
        Just Sum
o -> String -> Builder
string7 String
"min: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Sum -> Builder
showSum Sum
o Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
string7 String
";\n"
    part2 :: Builder
part2 = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ([Builder] -> Builder) -> [Builder] -> Builder
forall a b. (a -> b) -> a -> b
$ (Constraint -> Builder) -> [Constraint] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> Builder
showConstraint (Formula -> [Constraint]
pbConstraints Formula
opb)

-- | A ByteString Builder which renders a WBO format byte-string containing weighted boolean optimization problem.
wboBuilder :: SoftFormula -> Builder
wboBuilder :: SoftFormula -> Builder
wboBuilder SoftFormula
wbo = Builder
size Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
part1 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
part2
  where
    nv :: Lit
nv = SoftFormula -> Lit
wboNumVars SoftFormula
wbo
    nc :: Lit
nc = SoftFormula -> Lit
wboNumConstraints SoftFormula
wbo
    p :: Set IntSet
p = SoftFormula -> Set IntSet
wboProducts SoftFormula
wbo
    np :: Lit
np = Set IntSet -> Lit
forall a. Set a -> Lit
Set.size Set IntSet
p
    sp :: Lit
sp = [Lit] -> Lit
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
Prelude.sum [IntSet -> Lit
IntSet.size IntSet
tm | IntSet
tm <- Set IntSet -> [IntSet]
forall a. Set a -> [a]
Set.toList Set IntSet
p]
    mincost :: Integer
mincost =
      case [Integer
c | (Just Integer
c, Constraint
_) <- SoftFormula -> [(Maybe Integer, Constraint)]
wboConstraints SoftFormula
wbo] of
        [] -> Integer
1 -- this should not happen
        [Integer]
cs -> [Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
cs
    maxcost :: Integer
maxcost = [Integer] -> Integer
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
0 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer
c | (Just Integer
c, Constraint
_) <- SoftFormula -> [(Maybe Integer, Constraint)]
wboConstraints SoftFormula
wbo]
    sumcost :: Integer
sumcost = [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
Prelude.sum [Integer
c | (Just Integer
c, Constraint
_) <- SoftFormula -> [(Maybe Integer, Constraint)]
wboConstraints SoftFormula
wbo]
    size :: Builder
size = String -> Builder
string7 String
"* #variable= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec Lit
nv Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
string7 String
" #constraint= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec Lit
nc
         Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (if Lit
np Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
>= Lit
1 then String -> Builder
string7 String
" #product= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec Lit
np Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
string7 String
" sizeproduct= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec Lit
sp else Builder
forall a. Monoid a => a
mempty)
         Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
string7 String
" #soft= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec (SoftFormula -> Lit
wboNumSoft SoftFormula
wbo)
         Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
string7 String
" #mincost= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
mincost
         Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
string7 String
" #maxcost= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
maxcost
         Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
string7 String
" #sumcost= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
sumcost
         Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
'\n'
    part1 :: Builder
part1 = 
      case SoftFormula -> Maybe Integer
wboTopCost SoftFormula
wbo of
        Maybe Integer
Nothing -> String -> Builder
string7 String
"soft: ;\n"
        Just Integer
t -> String -> Builder
string7 String
"soft: " 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
<> String -> Builder
string7 String
";\n"
    part2 :: Builder
part2 = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ([Builder] -> Builder) -> [Builder] -> Builder
forall a b. (a -> b) -> a -> b
$ ((Maybe Integer, Constraint) -> Builder)
-> [(Maybe Integer, Constraint)] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Integer, Constraint) -> Builder
showSoftConstraint (SoftFormula -> [(Maybe Integer, Constraint)]
wboConstraints SoftFormula
wbo)

showSum :: Sum -> Builder
showSum :: Sum -> Builder
showSum = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ([Builder] -> Builder) -> (Sum -> [Builder]) -> Sum -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WeightedTerm -> Builder) -> Sum -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map WeightedTerm -> Builder
showWeightedTerm

showWeightedTerm :: WeightedTerm -> Builder
showWeightedTerm :: WeightedTerm -> Builder
showWeightedTerm (Integer
c, [Lit]
lits) = (Builder -> Builder -> Builder) -> Builder -> [Builder] -> Builder
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Builder
f Builder
g -> Builder
f Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
' ' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
g) Builder
forall a. Monoid a => a
mempty (Builder
xBuilder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
:[Builder]
xs)
  where
    x :: Builder
x = if Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Char -> Builder
char7 Char
'+' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
c else Integer -> Builder
integerDec Integer
c
    xs :: [Builder]
xs = (Lit -> Builder) -> [Lit] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map Lit -> Builder
showLit ([Lit] -> [Builder]) -> [Lit] -> [Builder]
forall a b. (a -> b) -> a -> b
$ (Lit -> Lit -> Ordering) -> [Lit] -> [Lit]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Lit -> Lit) -> Lit -> Lit -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Lit -> Lit
forall a. Num a => a -> a
abs) [Lit]
lits

showLit :: Lit -> Builder
showLit :: Lit -> Builder
showLit Lit
lit = if Lit
lit Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
> Lit
0 then Builder
v else Char -> Builder
char7 Char
'~' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
v
  where
    v :: Builder
v = Char -> Builder
char7 Char
'x' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec (Lit -> Lit
forall a. Num a => a -> a
abs Lit
lit)

showConstraint :: Constraint -> Builder
showConstraint :: Constraint -> Builder
showConstraint (Sum
lhs, Op
op, Integer
rhs) =
  Sum -> Builder
showSum Sum
lhs Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Op -> Builder
f Op
op Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>  Char -> Builder
char7 Char
' ' 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
<> String -> Builder
string7 String
";\n"
  where
    f :: Op -> Builder
f Op
Eq = Char -> Builder
char7 Char
'='
    f Op
Ge = String -> Builder
string7 String
">="

showSoftConstraint :: SoftConstraint -> Builder
showSoftConstraint :: (Maybe Integer, Constraint) -> Builder
showSoftConstraint (Maybe Integer
cost, Constraint
constr) =
  case Maybe Integer
cost of
    Maybe Integer
Nothing -> Constraint -> Builder
showConstraint Constraint
constr
    Just Integer
c -> Char -> Builder
char7 Char
'[' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
c Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
string7 String
"] " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Constraint -> Builder
showConstraint Constraint
constr



-- | Generate a OPB format byte-string containing pseudo boolean problem.
toOPBByteString :: Formula -> BS.ByteString
toOPBByteString :: Formula -> ByteString
toOPBByteString Formula
opb = Builder -> ByteString
toLazyByteString (Formula -> Builder
opbBuilder Formula
opb)

-- | Generate a WBO format byte-string containing weighted boolean optimization problem.
toWBOByteString :: SoftFormula -> BS.ByteString
toWBOByteString :: SoftFormula -> ByteString
toWBOByteString SoftFormula
wbo = Builder -> ByteString
toLazyByteString (SoftFormula -> Builder
wboBuilder SoftFormula
wbo)

-- | Output a OPB file containing pseudo boolean problem.
writeOPBFile :: FilePath -> Formula -> IO ()
writeOPBFile :: String -> Formula -> IO ()
writeOPBFile String
filepath Formula
opb = String -> IOMode -> (Handle -> IO ()) -> IO ()
forall r. String -> IOMode -> (Handle -> IO r) -> IO r
withBinaryFile String
filepath IOMode
WriteMode ((Handle -> IO ()) -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle
h -> do
  Handle -> BufferMode -> IO ()
hSetBuffering Handle
h (Maybe Lit -> BufferMode
BlockBuffering Maybe Lit
forall a. Maybe a
Nothing)
  Handle -> Formula -> IO ()
hPutOPB Handle
h Formula
opb

-- | Output a WBO file containing weighted boolean optimization problem.
writeWBOFile :: FilePath -> SoftFormula -> IO ()
writeWBOFile :: String -> SoftFormula -> IO ()
writeWBOFile String
filepath SoftFormula
wbo = String -> IOMode -> (Handle -> IO ()) -> IO ()
forall r. String -> IOMode -> (Handle -> IO r) -> IO r
withBinaryFile String
filepath IOMode
WriteMode ((Handle -> IO ()) -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle
h -> do
  Handle -> BufferMode -> IO ()
hSetBuffering Handle
h (Maybe Lit -> BufferMode
BlockBuffering Maybe Lit
forall a. Maybe a
Nothing)
  Handle -> SoftFormula -> IO ()
hPutWBO Handle
h SoftFormula
wbo

-- | Output a OPB file to a 'Handle' using 'hPutBuilder'.
--
-- It is recommended that the 'Handle' is set to binary and
-- 'BlockBuffering' mode. See 'hSetBinaryMode' and 'hSetBuffering'.
--
-- This function is more efficient than 'hPut' . 'toOPBByteString'
-- because in many cases no buffer allocation has to be done.
hPutOPB :: Handle -> Formula -> IO ()
hPutOPB :: Handle -> Formula -> IO ()
hPutOPB Handle
h Formula
opb = Handle -> Builder -> IO ()
hPutBuilder Handle
h (Formula -> Builder
opbBuilder Formula
opb)


-- | Output a WBO file to a 'Handle' using 'hPutBuilder'.
--
-- It is recommended that the 'Handle' is set to binary and
-- 'BlockBuffering' mode. See 'hSetBinaryMode' and 'hSetBuffering'.
--
-- This function is more efficient than 'hPut' . 'toWBOByteString'
-- because in many cases no buffer allocation has to be done.
hPutWBO :: Handle -> SoftFormula -> IO ()
hPutWBO :: Handle -> SoftFormula -> IO ()
hPutWBO Handle
h SoftFormula
wbo = Handle -> Builder -> IO ()
hPutBuilder Handle
h (SoftFormula -> Builder
wboBuilder SoftFormula
wbo)