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

module Data.PseudoBoolean.Builder
  (
  -- * Builder for String-like Monoid
    opbBuilder
  , wboBuilder

  -- * String generation
  , toOPBString
  , toWBOString
  ) where

import qualified Prelude
import Prelude hiding (sum)
import qualified Data.DList as DList
import qualified Data.IntSet as IntSet
import qualified Data.Set as Set
import Data.List (sortBy)
import Data.Monoid hiding (Sum (..))
import Data.Ord
import Data.String
import Text.Printf
import Data.PseudoBoolean.Types

-- | A builder which renders a OPB format in any String-like 'Monoid'.
opbBuilder :: (Monoid a, IsString a) => Formula -> a
opbBuilder :: forall a. (Monoid a, IsString a) => Formula -> a
opbBuilder Formula
opb = (a
size a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
part1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
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 a. Num a => [a] -> a
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 :: a
size = String -> a
forall a. IsString a => String -> a
fromString (String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"* #variable= %d #constraint= %d" Int
nv Int
nc)
         a -> a -> a
forall a. Semigroup a => a -> a -> a
<> (if Int
np Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1 then String -> a
forall a. IsString a => String -> a
fromString (String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
" #product= %d sizeproduct= %d" Int
np Int
sp) else a
forall a. Monoid a => a
mempty)
         a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString String
"\n"
    part1 :: a
part1 = 
      case Formula -> Maybe Sum
pbObjectiveFunction Formula
opb of
        Maybe Sum
Nothing -> a
forall a. Monoid a => a
mempty
        Just Sum
o -> String -> a
forall a. IsString a => String -> a
fromString String
"min: " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Sum -> a
forall a. (Monoid a, IsString a) => Sum -> a
showSum Sum
o a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString String
";\n"
    part2 :: a
part2 = [a] -> a
forall a. Monoid a => [a] -> a
mconcat ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ (Constraint -> a) -> [Constraint] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> a
forall a. (Monoid a, IsString a) => Constraint -> a
showConstraint (Formula -> [Constraint]
pbConstraints Formula
opb)

-- | A builder which renders a WBO format in any String-like 'Monoid'.
wboBuilder :: (Monoid a, IsString a) => SoftFormula -> a
wboBuilder :: forall a. (Monoid a, IsString a) => SoftFormula -> a
wboBuilder SoftFormula
wbo = a
size a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
part1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
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 a. Num a => [a] -> a
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 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 :: a
size = String -> a
forall a. IsString a => String -> a
fromString (String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"* #variable= %d #constraint= %d" Int
nv Int
nc)
         a -> a -> a
forall a. Semigroup a => a -> a -> a
<> (if Int
np Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1 then String -> a
forall a. IsString a => String -> a
fromString (String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
" #product= %d sizeproduct= %d" Int
np Int
sp) else a
forall a. Monoid a => a
mempty)
         a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
" #soft= %d" (SoftFormula -> Int
wboNumSoft SoftFormula
wbo))
         a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString (String -> Integer -> Integer -> Integer -> String
forall r. PrintfType r => String -> r
printf String
" #mincost= %d #maxcost= %d #sumcost= %d" Integer
mincost Integer
maxcost Integer
sumcost)
         a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString String
"\n"
    part1 :: a
part1 = 
      case SoftFormula -> Maybe Integer
wboTopCost SoftFormula
wbo of
        Maybe Integer
Nothing -> String -> a
forall a. IsString a => String -> a
fromString String
"soft: ;\n"
        Just Integer
t -> String -> a
forall a. IsString a => String -> a
fromString String
"soft: " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString (Integer -> String
forall a. Show a => a -> String
show Integer
t) a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString String
";\n"
    part2 :: a
part2 = [a] -> a
forall a. Monoid a => [a] -> a
mconcat ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ ((Maybe Integer, Constraint) -> a)
-> [(Maybe Integer, Constraint)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Integer, Constraint) -> a
forall a.
(Monoid a, IsString a) =>
(Maybe Integer, Constraint) -> a
showSoftConstraint (SoftFormula -> [(Maybe Integer, Constraint)]
wboConstraints SoftFormula
wbo)

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

showWeightedTerm :: (Monoid a, IsString a) => WeightedTerm -> a
showWeightedTerm :: forall a. (Monoid a, IsString a) => WeightedTerm -> a
showWeightedTerm (Integer
c, [Int]
lits) = (a -> a -> a) -> a -> [a] -> a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
f a
g -> a
f a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString String
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
g) a
forall a. Monoid a => a
mempty (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs)
  where
    x :: a
x = if Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then String -> a
forall a. IsString a => String -> a
fromString String
"+" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString (Integer -> String
forall a. Show a => a -> String
show Integer
c) else String -> a
forall a. IsString a => String -> a
fromString (Integer -> String
forall a. Show a => a -> String
show Integer
c)
    xs :: [a]
xs = (Int -> a) -> [Int] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Int -> a
forall a. (Monoid a, IsString a) => Int -> a
showLit ([Int] -> [a]) -> [Int] -> [a]
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 :: (Monoid a, IsString a) => Lit -> a
showLit :: forall a. (Monoid a, IsString a) => Int -> a
showLit Int
lit = if Int
lit Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then a
v else String -> a
forall a. IsString a => String -> a
fromString String
"~" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
v
  where
    v :: a
v = String -> a
forall a. IsString a => String -> a
fromString String
"x" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString (Int -> String
forall a. Show a => a -> String
show (Int -> Int
forall a. Num a => a -> a
abs Int
lit))

showConstraint :: (Monoid a, IsString a) => Constraint -> a
showConstraint :: forall a. (Monoid a, IsString a) => Constraint -> a
showConstraint (Sum
lhs, Op
op, Integer
rhs) =
  Sum -> a
forall a. (Monoid a, IsString a) => Sum -> a
showSum Sum
lhs a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Op -> a
forall {a}. IsString a => Op -> a
f Op
op a -> a -> a
forall a. Semigroup a => a -> a -> a
<>  String -> a
forall a. IsString a => String -> a
fromString String
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString (Integer -> String
forall a. Show a => a -> String
show Integer
rhs) a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString String
";\n"
  where
    f :: Op -> a
f Op
Eq = String -> a
forall a. IsString a => String -> a
fromString String
"="
    f Op
Ge = String -> a
forall a. IsString a => String -> a
fromString String
">="

showSoftConstraint :: (Monoid a, IsString a) => SoftConstraint -> a
showSoftConstraint :: forall a.
(Monoid a, IsString a) =>
(Maybe Integer, Constraint) -> a
showSoftConstraint (Maybe Integer
cost, Constraint
constr) =
  case Maybe Integer
cost of
    Maybe Integer
Nothing -> Constraint -> a
forall a. (Monoid a, IsString a) => Constraint -> a
showConstraint Constraint
constr
    Just Integer
c -> String -> a
forall a. IsString a => String -> a
fromString String
"[" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString (Integer -> String
forall a. Show a => a -> String
show Integer
c) a -> a -> a
forall a. Semigroup a => a -> a -> a
<> String -> a
forall a. IsString a => String -> a
fromString String
"] " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Constraint -> a
forall a. (Monoid a, IsString a) => Constraint -> a
showConstraint Constraint
constr


-- | Generate a OPB format string containing pseudo boolean problem.
toOPBString :: Formula -> String
toOPBString :: Formula -> String
toOPBString Formula
opb = DList Char -> String -> String
forall a. DList a -> [a] -> [a]
DList.apply (Formula -> DList Char
forall a. (Monoid a, IsString a) => Formula -> a
opbBuilder Formula
opb) String
""

-- | Generate a WBO format string containing weighted boolean optimization problem.
toWBOString :: SoftFormula -> String
toWBOString :: SoftFormula -> String
toWBOString SoftFormula
wbo = DList Char -> String -> String
forall a. DList a -> [a] -> [a]
DList.apply (SoftFormula -> DList Char
forall a. (Monoid a, IsString a) => SoftFormula -> a
wboBuilder SoftFormula
wbo) String
""