{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
module ToySolver.Converter.PB2SMP
( pb2smp
) 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
pb2smp :: Bool -> PBFile.Formula -> Builder
pb2smp :: Bool -> Formula -> Builder
pb2smp Bool
isUnix Formula
formula =
Builder
header Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Builder
decls Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Char -> Builder
char7 Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Builder
obj2 Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Char -> Builder
char7 Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Builder
constrs Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Char -> Builder
char7 Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
Builder
actions Builder -> Builder -> Builder
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 Builder
forall a. Monoid a => a
mempty
footer :: Builder
footer =
if Bool
isUnix
then Builder
"\n}\n"
else Builder
forall a. Monoid a => a
mempty
actions :: Builder
actions = ByteString -> Builder
byteString (ByteString -> Builder) -> ByteString -> Builder
forall a b. (a -> b) -> a -> b
$
ByteString
"solve();\n" ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<>
ByteString
"x[i].val.print();\n" ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<>
ByteString
"cost.val.print();\n"
decls :: Builder
decls =
ByteString -> Builder
byteString ByteString
"Element i(set=\"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
"\");\nIntegerVariable x(type=binary, index=i);\n"
constrs :: Builder
constrs = [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
[ 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 Builder -> Builder -> Builder
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 = [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, [Int]) -> Builder) -> Sum -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, [Int]) -> Builder
showTerm Sum
xs
showTerm :: (Integer, [Int]) -> Builder
showTerm (Integer
n,[Int]
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 (Char -> Builder
char7 Char
'*') ([Builder] -> [Builder]) -> [Builder] -> [Builder]
forall a b. (a -> b) -> a -> b
$ Integer -> [Builder]
showCoeff Integer
n [Builder] -> [Builder] -> [Builder]
forall a. [a] -> [a] -> [a]
++ [Int -> Builder
showLit Int
l | Int
l<-[Int]
ls]
showCoeff :: Integer -> [Builder]
showCoeff Integer
n
| Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 = []
| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = [Char -> Builder
char7 Char
'(' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec Integer
n Builder -> Builder -> Builder
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
then Builder
"(1-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
"]"
obj2 :: Builder
obj2 =
case Formula -> Maybe Sum
PBFile.pbObjectiveFunction Formula
formula of
Just Sum
obj' ->
ByteString -> Builder
byteString ByteString
"Objective cost(type=minimize);\ncost = " 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