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

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

pb2smp :: Bool -> PBFile.Formula -> Builder
pb2smp :: Bool -> Formula -> Builder
pb2smp Bool
isUnix Formula
formula =
  Builder
header forall a. Semigroup a => a -> a -> a
<>
  Builder
decls forall a. Semigroup a => a -> a -> a
<>
  Char -> Builder
char7 Char
'\n' forall a. Semigroup a => a -> a -> a
<>
  Builder
obj2 forall a. Semigroup a => a -> a -> a
<>
  Char -> Builder
char7 Char
'\n' forall a. Semigroup a => a -> a -> a
<>
  Builder
constrs forall a. Semigroup a => a -> a -> a
<>
  Char -> Builder
char7 Char
'\n' forall a. Semigroup a => a -> a -> a
<>
  Builder
actions forall a. Semigroup a => a -> a -> a
<>
  Builder
footer
  where
    nv :: Int
nv = Formula -> Int
PBFile.pbNumVars Formula
formula

    header :: Builder
header =
      if Bool
isUnix
      then ByteString -> Builder
byteString ByteString
"#include \"simple.h\"\nvoid ufun()\n{\n\n"
      else forall a. Monoid a => a
mempty

    footer :: Builder
footer =
      if Bool
isUnix
      then Builder
"\n}\n"
      else forall a. Monoid a => a
mempty

    actions :: Builder
actions = ByteString -> Builder
byteString forall a b. (a -> b) -> a -> b
$
      ByteString
"solve();\n" forall a. Semigroup a => a -> a -> a
<>
      ByteString
"x[i].val.print();\n" forall a. Semigroup a => a -> a -> a
<>
      ByteString
"cost.val.print();\n"

    decls :: Builder
decls =
      ByteString -> Builder
byteString ByteString
"Element i(set=\"1 .. " forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec Int
nv forall a. Semigroup a => a -> a -> a
<>
      ByteString -> Builder
byteString ByteString
"\");\nIntegerVariable x(type=binary, index=i);\n"

    constrs :: Builder
constrs = forall a. Monoid a => [a] -> a
mconcat
      [ 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 forall a. Semigroup a => a -> a -> a
<>
        Builder
";\n"
      | (Sum
lhs, Op
op, Integer
rhs) <- Formula -> [(Sum, Op, Integer)]
PBFile.pbConstraints Formula
formula
      , let op2 :: Builder
op2 = case Op
op of
                    Op
PBFile.Ge -> Builder
" >= "
                    Op
PBFile.Eq -> Builder
" == "
      ]

    showSum :: PBFile.Sum -> Builder
    showSum :: Sum -> Builder
showSum [] = Char -> Builder
char7 Char
'0'
    showSum Sum
xs = 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
$ forall a b. (a -> b) -> [a] -> [b]
map (Integer, [Int]) -> Builder
showTerm Sum
xs

    showTerm :: (Integer, [Int]) -> Builder
showTerm (Integer
n,[Int]
ls) = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
intersperse (Char -> Builder
char7 Char
'*') forall a b. (a -> b) -> a -> b
$ Integer -> [Builder]
showCoeff Integer
n forall a. [a] -> [a] -> [a]
++ [Int -> Builder
showLit Int
l | Int
l<-[Int]
ls]

    showCoeff :: Integer -> [Builder]
showCoeff Integer
n
      | Integer
n forall a. Eq a => a -> a -> Bool
== Integer
1    = []
      | Integer
n forall a. Ord a => a -> a -> Bool
< Integer
0     = [Char -> Builder
char7 Char
'(' forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
n forall a. Semigroup a => a -> a -> a
<> Char -> Builder
char7 Char
')']
      | Bool
otherwise = [Integer -> Builder
integerDec Integer
n]

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

    obj2 :: Builder
obj2 =
      case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
        Just Sum
obj' ->
          ByteString -> Builder
byteString ByteString
"Objective cost(type=minimize);\ncost = " 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