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