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