{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE OverloadedStrings #-}
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