{-# 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.Maybe (maybeToList)
import Data.Monoid hiding (Sum (..))
import Data.Ord
import Data.String
import Math.NumberTheory.Logarithms (integerLog2)
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
    neq :: Int
neq = [()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [() | (Sum
_lhs, Op
Eq, Integer
_rhs) <- Formula -> [(Sum, Op, Integer)]
pbConstraints Formula
opb]
    intsize :: Int
intsize = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:
      [ if Integer
tmp Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Int
0 else Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Integer -> Int
integerLog2 Integer
tmp
      | (Sum
ts, Integer
d) <- [(Sum
ts, Integer
0) | Sum
ts <- Maybe Sum -> [Sum]
forall a. Maybe a -> [a]
maybeToList (Formula -> Maybe Sum
pbObjectiveFunction Formula
opb)] [(Sum, Integer)] -> [(Sum, Integer)] -> [(Sum, Integer)]
forall a. [a] -> [a] -> [a]
++ [(Sum
lhs,Integer
rhs) | (Sum
lhs,Op
_op,Integer
rhs) <- Formula -> [(Sum, Op, Integer)]
pbConstraints Formula
opb]
      , let tmp :: Integer
tmp = Integer -> Integer
forall a. Num a => a -> a
abs Integer
d Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
Prelude.sum [Integer -> Integer
forall a. Num a => a -> a
abs Integer
c | (Integer
c,[Int]
_) <- Sum
ts]
      ]
    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 -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"* #variable= %d #constraint= %d #equal= %d intsize= %d" Int
nv Int
nc Int
neq Int
intsize)
         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
$ ((Sum, Op, Integer) -> a) -> [(Sum, Op, Integer)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Sum, Op, Integer) -> a
forall a. (Monoid a, IsString a) => (Sum, Op, Integer) -> a
showConstraint (Formula -> [(Sum, Op, Integer)]
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
    neq :: Int
neq = [()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [() | (Maybe Integer
_, (Sum
_lhs, Op
Eq, Integer
_rhs)) <- SoftFormula -> [(Maybe Integer, (Sum, Op, Integer))]
wboConstraints 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, (Sum, Op, Integer)
_) <- SoftFormula -> [(Maybe Integer, (Sum, Op, Integer))]
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, (Sum, Op, Integer)
_) <- SoftFormula -> [(Maybe Integer, (Sum, Op, Integer))]
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, (Sum, Op, Integer)
_) <- SoftFormula -> [(Maybe Integer, (Sum, Op, Integer))]
wboConstraints SoftFormula
wbo]
    intsize :: Int
intsize = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:
      [ if Integer
tmp Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Int
0 else Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Integer -> Int
integerLog2 Integer
tmp
      | ([Integer]
cs, Integer
d) <- ([Integer
sumcost], Integer
0) ([Integer], Integer)
-> [([Integer], Integer)] -> [([Integer], Integer)]
forall a. a -> [a] -> [a]
: [(((Integer, [Int]) -> Integer) -> Sum -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, [Int]) -> Integer
forall a b. (a, b) -> a
fst Sum
lhs, Integer
rhs) | (Maybe Integer
_,(Sum
lhs,Op
_op,Integer
rhs)) <- SoftFormula -> [(Maybe Integer, (Sum, Op, Integer))]
wboConstraints SoftFormula
wbo]
      , let tmp :: Integer
tmp = Integer -> Integer
forall a. Num a => a -> a
abs Integer
d Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
Prelude.sum [Integer -> Integer
forall a. Num a => a -> a
abs Integer
c | Integer
c <- [Integer]
cs]
      ]
    size :: a
size = String -> a
forall a. IsString a => String -> a
fromString (String -> Int -> Int -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"* #variable= %d #constraint= %d #equal= %d intsize= %d" Int
nv Int
nc Int
neq Int
intsize)
         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, (Sum, Op, Integer)) -> a)
-> [(Maybe Integer, (Sum, Op, Integer))] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Integer, (Sum, Op, Integer)) -> a
forall a.
(Monoid a, IsString a) =>
(Maybe Integer, (Sum, Op, Integer)) -> a
showSoftConstraint (SoftFormula -> [(Maybe Integer, (Sum, Op, Integer))]
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
. ((Integer, [Int]) -> a) -> Sum -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, [Int]) -> a
forall a. (Monoid a, IsString a) => (Integer, [Int]) -> a
showWeightedTerm

showWeightedTerm :: (Monoid a, IsString a) => WeightedTerm -> a
showWeightedTerm :: forall a. (Monoid a, IsString a) => (Integer, [Int]) -> 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) => (Sum, Op, Integer) -> 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, (Sum, Op, Integer)) -> a
showSoftConstraint (Maybe Integer
cost, (Sum, Op, Integer)
constr) =
  case Maybe Integer
cost of
    Maybe Integer
Nothing -> (Sum, Op, Integer) -> a
forall a. (Monoid a, IsString a) => (Sum, Op, Integer) -> a
showConstraint (Sum, Op, Integer)
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
<> (Sum, Op, Integer) -> a
forall a. (Monoid a, IsString a) => (Sum, Op, Integer) -> a
showConstraint (Sum, Op, Integer)
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
""