{-# 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 :: Int
nv = Formula -> Int
pbNumVars Formula
opb
    nc :: Int
nc = Formula -> Int
pbNumConstraints Formula
opb
    p :: Set IntSet
p = Formula -> Set IntSet
pbProducts Formula
opb
    np :: Int
np = Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
p
    sp :: Int
sp = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
Prelude.sum [IntSet -> Int
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
<> Int -> Builder
intDec Int
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
<> Int -> Builder
intDec Int
nc
         Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (if Int
np Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1 then String -> Builder
string7 String
" #product= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
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
<> Int -> Builder
intDec Int
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 :: Int
nv = SoftFormula -> Int
wboNumVars SoftFormula
wbo
    nc :: Int
nc = SoftFormula -> Int
wboNumConstraints SoftFormula
wbo
    p :: Set IntSet
p = SoftFormula -> Set IntSet
wboProducts SoftFormula
wbo
    np :: Int
np = Set IntSet -> Int
forall a. Set a -> Int
Set.size Set IntSet
p
    sp :: Int
sp = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
Prelude.sum [IntSet -> Int
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 (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
cs
    maxcost :: Integer
maxcost = [Integer] -> Integer
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 (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
<> Int -> Builder
intDec Int
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
<> Int -> Builder
intDec Int
nc
         Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (if Int
np Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1 then String -> Builder
string7 String
" #product= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
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
<> Int -> Builder
intDec Int
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
<> Int -> Builder
intDec (SoftFormula -> Int
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, [Int]
lits) = (Builder -> Builder -> Builder) -> Builder -> [Builder] -> Builder
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 = (Int -> Builder) -> [Int] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Builder
showLit ([Int] -> [Builder]) -> [Int] -> [Builder]
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Int -> Int) -> Int -> Int -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Int -> Int
forall a. Num a => a -> a
abs) [Int]
lits

showLit :: Lit -> Builder
showLit :: Int -> Builder
showLit Int
lit = if Int
lit Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
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
<> Int -> Builder
intDec (Int -> Int
forall a. Num a => a -> a
abs Int
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 Int -> BufferMode
BlockBuffering Maybe Int
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 Int -> BufferMode
BlockBuffering Maybe Int
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)