{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE OverloadedStrings #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.PB2LSP
-- Copyright   :  (c) Masahiro Sakai 2013-2014,2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.Converter.PB2LSP
  ( pb2lsp
  , wbo2lsp
  ) where

import Data.ByteString.Builder
import Data.List
import qualified Data.PseudoBoolean as PBFile

pb2lsp :: PBFile.Formula -> Builder
pb2lsp :: Formula -> Builder
pb2lsp Formula
formula =
  ByteString -> Builder
byteString ByteString
"function model() {\n" forall a. Semigroup a => a -> a -> a
<>
  Builder
decls forall a. Semigroup a => a -> a -> a
<>
  Builder
constrs forall a. Semigroup a => a -> a -> a
<>
  Builder
obj2 forall a. Semigroup a => a -> a -> a
<>
  Builder
"}\n"
  where
    nv :: Lit
nv = Formula -> Lit
PBFile.pbNumVars Formula
formula

    decls :: Builder
decls = ByteString -> Builder
byteString ByteString
"  for [i in 1.." forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec Lit
nv forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
"] x[i] <- bool();\n"

    constrs :: Builder
constrs = forall a. Monoid a => [a] -> a
mconcat
      [ ByteString -> Builder
byteString ByteString
"  constraint " forall a. Semigroup a => a -> a -> a
<>
        Constraint -> Builder
showConstr Constraint
c forall a. Semigroup a => a -> a -> a
<>
        Builder
";\n"
      | Constraint
c <- Formula -> [Constraint]
PBFile.pbConstraints Formula
formula
      ]

    obj2 :: Builder
obj2 =
      case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
        Just Sum
obj' -> ByteString -> Builder
byteString ByteString
"  minimize " forall a. Semigroup a => a -> a -> a
<> Sum -> Builder
showSum Sum
obj' forall a. Semigroup a => a -> a -> a
<> Builder
";\n"
        Maybe Sum
Nothing -> forall a. Monoid a => a
mempty

wbo2lsp :: PBFile.SoftFormula -> Builder
wbo2lsp :: SoftFormula -> Builder
wbo2lsp SoftFormula
softFormula =
  ByteString -> Builder
byteString ByteString
"function model() {\n" forall a. Semigroup a => a -> a -> a
<>
  Builder
decls forall a. Semigroup a => a -> a -> a
<>
  Builder
constrs forall a. Semigroup a => a -> a -> a
<>
  Builder
costDef forall a. Semigroup a => a -> a -> a
<>
  Builder
topConstr forall a. Semigroup a => a -> a -> a
<>
  ByteString -> Builder
byteString ByteString
"  minimize cost;\n}\n"
  where
    nv :: Lit
nv = SoftFormula -> Lit
PBFile.wboNumVars SoftFormula
softFormula

    decls :: Builder
decls = ByteString -> Builder
byteString ByteString
"  for [i in 1.." forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec Lit
nv forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
byteString ByteString
"] x[i] <- bool();\n"

    constrs :: Builder
constrs = forall a. Monoid a => [a] -> a
mconcat
      [ ByteString -> Builder
byteString ByteString
"  constraint " forall a. Semigroup a => a -> a -> a
<>
        Constraint -> Builder
showConstr Constraint
c forall a. Semigroup a => a -> a -> a
<>
        Builder
";\n"
      | (Maybe Integer
Nothing, Constraint
c) <- SoftFormula -> [(Maybe Integer, Constraint)]
PBFile.wboConstraints SoftFormula
softFormula
      ]

    costDef :: Builder
costDef = ByteString -> Builder
byteString ByteString
"  cost <- sum(\n" forall a. Semigroup a => a -> a -> a
<> Builder
s forall a. Semigroup a => a -> a -> a
<> Builder
");\n"
      where
        s :: Builder
s = forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> [a]
intersperse (Builder
",\n") forall a b. (a -> b) -> a -> b
$ [Builder]
xs
        xs :: [Builder]
xs = [Builder
"    " forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
w forall a. Semigroup a => a -> a -> a
<> Builder
"*!(" forall a. Semigroup a => a -> a -> a
<> Constraint -> Builder
showConstr Constraint
c forall a. Semigroup a => a -> a -> a
<> Builder
")"
             | (Just Integer
w, Constraint
c) <- SoftFormula -> [(Maybe Integer, Constraint)]
PBFile.wboConstraints SoftFormula
softFormula]

    topConstr :: Builder
topConstr =
      case SoftFormula -> Maybe Integer
PBFile.wboTopCost SoftFormula
softFormula of
        Maybe Integer
Nothing -> forall a. Monoid a => a
mempty
        Just Integer
t -> ByteString -> Builder
byteString ByteString
"  constraint cost <= " forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
t forall a. Semigroup a => a -> a -> a
<> Builder
";\n"

showConstr :: PBFile.Constraint -> Builder
showConstr :: Constraint -> Builder
showConstr (Sum
lhs, Op
PBFile.Ge, Integer
1) | forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Integer
cforall a. Eq a => a -> a -> Bool
==Integer
1 | (Integer
c,Term
_) <- Sum
lhs] =
  Builder
"or(" forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a. a -> [a] -> [a]
intersperse Builder
"," (forall a b. (a -> b) -> [a] -> [b]
map (Term -> Builder
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Sum
lhs)) forall a. Semigroup a => a -> a -> a
<> Builder
")"
  where
    f :: Term -> Builder
f [Lit
l] = Lit -> Builder
showLit Lit
l
    f Term
ls  = Builder
"and(" forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a. a -> [a] -> [a]
intersperse Builder
"," (forall a b. (a -> b) -> [a] -> [b]
map Lit -> Builder
showLit Term
ls)) forall a. Semigroup a => a -> a -> a
<> Builder
")"
showConstr (Sum
lhs, Op
op, Integer
rhs) = Sum -> Builder
showSum Sum
lhs  forall a. Semigroup a => a -> a -> a
<> Builder
op2 forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
rhs
  where
    op2 :: Builder
op2 = case Op
op of
            Op
PBFile.Ge -> Builder
" >= "
            Op
PBFile.Eq -> Builder
" == "

sum' :: [Builder] -> Builder
sum' :: [Builder] -> Builder
sum' [Builder]
xs = Builder
"sum(" forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a. a -> [a] -> [a]
intersperse Builder
", " [Builder]
xs) forall a. Semigroup a => a -> a -> a
<> Builder
")"

showSum :: PBFile.Sum -> Builder
showSum :: Sum -> Builder
showSum = [Builder] -> Builder
sum' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Integer, Term) -> Builder
showTerm

showTerm :: PBFile.WeightedTerm -> Builder
showTerm :: (Integer, Term) -> Builder
showTerm (Integer
n,Term
ls) = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
intersperse Builder
"*" forall a b. (a -> b) -> a -> b
$ [Integer -> Builder
integerDec Integer
n | Integer
n forall a. Eq a => a -> a -> Bool
/= Integer
1] forall a. [a] -> [a] -> [a]
++ [Lit -> Builder
showLit Lit
l | Lit
l<-Term
ls]

showLit :: PBFile.Lit -> Builder
showLit :: Lit -> Builder
showLit Lit
l =
  if Lit
l forall a. Ord a => a -> a -> Bool
< Lit
0
  then Builder
"!x[" forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec (forall a. Num a => a -> a
abs Lit
l) forall a. Semigroup a => a -> a -> a
<> Builder
"]"
  else Builder
"x[" forall a. Semigroup a => a -> a -> a
<> Lit -> Builder
intDec Lit
l forall a. Semigroup a => a -> a -> a
<> Builder
"]"