{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE CPP #-}
{-# 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
#if !MIN_VERSION_base(4,11,0)
import Data.Monoid
#endif
import qualified Data.PseudoBoolean as PBFile

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

    decls :: Builder
decls = ByteString -> Builder
byteString ByteString
"  for [i in 1.." 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
<> ByteString -> Builder
byteString ByteString
"] x[i] <- bool();\n"

    constrs :: Builder
constrs = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
      [ ByteString -> Builder
byteString ByteString
"  constraint " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Constraint -> Builder
showConstr Constraint
c Builder -> Builder -> Builder
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 " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Sum -> Builder
showSum Sum
obj' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
";\n"
        Maybe Sum
Nothing -> Builder
forall a. Monoid a => a
mempty

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

    decls :: Builder
decls = ByteString -> Builder
byteString ByteString
"  for [i in 1.." 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
<> ByteString -> Builder
byteString ByteString
"] x[i] <- bool();\n"

    constrs :: Builder
constrs = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
      [ ByteString -> Builder
byteString ByteString
"  constraint " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
        Constraint -> Builder
showConstr Constraint
c Builder -> Builder -> Builder
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" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
s Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
");\n"
      where
        s :: Builder
s = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ([Builder] -> Builder)
-> ([Builder] -> [Builder]) -> [Builder] -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
intersperse (Builder
",\n") ([Builder] -> Builder) -> [Builder] -> Builder
forall a b. (a -> b) -> a -> b
$ [Builder]
xs
        xs :: [Builder]
xs = [Builder
"    " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
w Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"*!(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Constraint -> Builder
showConstr Constraint
c Builder -> Builder -> Builder
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 -> Builder
forall a. Monoid a => a
mempty
        Just Integer
t -> ByteString -> Builder
byteString ByteString
"  constraint cost <= " 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
<> Builder
";\n"

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

showSum :: PBFile.Sum -> Builder
showSum :: Sum -> Builder
showSum = [Builder] -> Builder
sum' ([Builder] -> Builder) -> (Sum -> [Builder]) -> Sum -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Integer, Term) -> Builder) -> Sum -> [Builder]
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) = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat ([Builder] -> Builder) -> [Builder] -> Builder
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
intersperse Builder
"*" ([Builder] -> [Builder]) -> [Builder] -> [Builder]
forall a b. (a -> b) -> a -> b
$ [Integer -> Builder
integerDec Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
1] [Builder] -> [Builder] -> [Builder]
forall a. [a] -> [a] -> [a]
++ [Int -> Builder
showLit Int
l | Int
l<-Term
ls]

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