module Data.PseudoBoolean.Builder
(
opbBuilder
, wboBuilder
, 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
opbBuilder :: (Monoid a, IsString a) => Formula -> a
opbBuilder opb = (size <> part1 <> part2)
where
nv = pbNumVars opb
nc = pbNumConstraints opb
p = pbProducts opb
np = Set.size p
sp = Prelude.sum [IntSet.size tm | tm <- Set.toList p]
size = fromString (printf "* #variable= %d #constraint= %d" nv nc)
<> (if np >= 1 then fromString (printf " #product= %d sizeproduct= %d" np sp) else mempty)
<> fromString "\n"
part1 =
case pbObjectiveFunction opb of
Nothing -> mempty
Just o -> fromString "min: " <> showSum o <> fromString ";\n"
part2 = mconcat $ map showConstraint (pbConstraints opb)
wboBuilder :: (Monoid a, IsString a) => SoftFormula -> a
wboBuilder wbo = size <> part1 <> part2
where
nv = wboNumVars wbo
nc = wboNumConstraints wbo
p = wboProducts wbo
np = Set.size p
sp = Prelude.sum [IntSet.size tm | tm <- Set.toList p]
size = fromString (printf "* #variable= %d #constraint= %d" nv nc)
<> (if np >= 1 then fromString (printf " #product= %d sizeproduct= %d" np sp) else mempty)
<> fromString (printf " #soft= %d" (wboNumSoft wbo))
<> fromString "\n"
part1 =
case wboTopCost wbo of
Nothing -> fromString "soft: ;\n"
Just t -> fromString "soft: " <> fromString (show t) <> fromString ";\n"
part2 = mconcat $ map showSoftConstraint (wboConstraints wbo)
showSum :: (Monoid a, IsString a) => Sum -> a
showSum = mconcat . map showWeightedTerm
showWeightedTerm :: (Monoid a, IsString a) => WeightedTerm -> a
showWeightedTerm (c, lits) = foldr (\f g -> f <> fromString " " <> g) mempty (x:xs)
where
x = if c >= 0 then fromString "+" <> fromString (show c) else fromString (show c)
xs = map showLit $ sortBy (comparing abs) lits
showLit :: (Monoid a, IsString a) => Lit -> a
showLit lit = if lit > 0 then v else fromString "~" <> v
where
v = fromString "x" <> fromString (show (abs lit))
showConstraint :: (Monoid a, IsString a) => Constraint -> a
showConstraint (lhs, op, rhs) =
showSum lhs <> f op <> fromString " " <> fromString (show rhs) <> fromString ";\n"
where
f Eq = fromString "="
f Ge = fromString ">="
showSoftConstraint :: (Monoid a, IsString a) => SoftConstraint -> a
showSoftConstraint (cost, constr) =
case cost of
Nothing -> showConstraint constr
Just c -> fromString "[" <> fromString (show c) <> fromString "] " <> showConstraint constr
toOPBString :: Formula -> String
toOPBString opb = DList.apply (opbBuilder opb) ""
toWBOString :: SoftFormula -> String
toWBOString wbo = DList.apply (wboBuilder wbo) ""