msakai / pseudo-boolean / 127

Committed 05 Apr 2025 12:13AM UTC coverage: 92.679% (-0.6%) from 93.287%

Build # 127

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #23 from msakai/feature/PB24-format

Generate #equal= hint and intsize= hint specified for PB24 competition

Run Details

19 of 24 new or added lines in 2 files covered. (79.17%)

2 existing lines in 2 files now uncovered.

557 of 601 relevant lines covered (92.68%)

0.93 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

93.67

/src/Data/PseudoBoolean/ByteStringBuilder.hs

{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.PseudoBoolean.ByteStringBuilder
-- Copyright   :  (c) Masahiro Sakai 2011-2015
-- License     :  BSD-style
-- 
-- Maintainer  :  masahiro.sakai@gmail.com
-- Portability :  portable
--
-----------------------------------------------------------------------------

module Data.PseudoBoolean.ByteStringBuilder
  (
  -- * Builder for (Lazy) ByteString generation
    opbBuilder
  , wboBuilder

  -- * Lazy ByteString generation
  , toOPBByteString
  , toWBOByteString

  -- * File I/O
  , writeOPBFile
  , writeWBOFile
  , hPutOPB
  , hPutWBO
  ) where

import qualified Prelude
import Prelude hiding (sum)
import qualified Data.IntSet as IntSet
import qualified Data.Set as Set
import Data.List (sortBy)
import Data.Maybe (maybeToList)
import qualified Data.ByteString.Lazy as BS
import Data.ByteString.Builder (Builder, intDec, integerDec, char7, string7, hPutBuilder, toLazyByteString)
import Data.Ord
import Math.NumberTheory.Logarithms (integerLog2)
import System.IO
import Data.PseudoBoolean.Types

-- | A ByteString Builder which renders a OPB format byte-string containing pseudo boolean problem.
opbBuilder :: Formula -> Builder
opbBuilder opb = (size <> part1 <> part2)
  where
    nv = pbNumVars opb
    nc = pbNumConstraints opb
    neq = length [() | (_lhs, Eq, _rhs) <- pbConstraints opb]
    intsize = maximum $ 0 :
      [ if tmp == 0 then 0 else 1 + integerLog2 tmp
      | (ts, d) <- [(ts, 0) | (_, ts) <- maybeToList (pbObjectiveFunction opb)] ++ [(lhs,rhs) | (lhs,_op,rhs) <- pbConstraints opb]
      , let tmp = abs d + Prelude.sum [abs c | (c,_) <- ts]
      ]
    p = pbProducts opb
    np = Set.size p
    sp = Prelude.sum [IntSet.size tm | tm <- Set.toList p]
    size = string7 "* #variable= " <> intDec nv <> string7 " #constraint= " <> intDec nc <> string7 " #equal= " <> intDec neq <> string7 " intsize= " <> intDec intsize
         <> (if np >= 1 then string7 " #product= " <> intDec np <> string7 " sizeproduct= " <> intDec sp else mempty)
         <> char7 '\n'
    part1 = 
      case pbObjectiveFunction opb of
        Nothing -> mempty
        Just (dir, o) ->
          (case dir of
            OptMin -> string7 "min"
            OptMax -> string7 "max")
          <> string7 ": " <> showSum o <> string7 ";\n"
    part2 = mconcat $ map showConstraint (pbConstraints opb)

-- | A ByteString Builder which renders a WBO format byte-string containing weighted boolean optimization problem.
wboBuilder :: SoftFormula -> Builder
wboBuilder wbo = size <> part1 <> part2
  where
    nv = wboNumVars wbo
    nc = wboNumConstraints wbo
    neq = length [() | (_, (_lhs, Eq, _rhs)) <- wboConstraints wbo]
    p = wboProducts wbo
    np = Set.size p
    sp = Prelude.sum [IntSet.size tm | tm <- Set.toList p]
    mincost =
      case [c | (Just c, _) <- wboConstraints wbo] of
        [] -> 1 -- this should not happen
        cs -> minimum cs
    maxcost = maximum $ 0 : [c | (Just c, _) <- wboConstraints wbo]
    sumcost = Prelude.sum [c | (Just c, _) <- wboConstraints wbo]
    intsize = maximum $ 0 :
      [ if tmp == 0 then 0 else 1 + integerLog2 tmp
      | (cs, d) <- ([sumcost], 0) : [(map fst lhs, rhs) | (_,(lhs,_op,rhs)) <- wboConstraints wbo]
      , let tmp = abs d + Prelude.sum [abs c | c <- cs]
      ]
    size = string7 "* #variable= " <> intDec nv <> string7 " #constraint= " <> intDec nc <> string7 " #equal= " <> intDec neq <> string7 " intsize= " <> intDec intsize
         <> (if np >= 1 then string7 " #product= " <> intDec np <> string7 " sizeproduct= " <> intDec sp else mempty)
         <> string7 " #soft= " <> intDec (wboNumSoft wbo)
         <> string7 " mincost= " <> integerDec mincost
         <> string7 " maxcost= " <> integerDec maxcost
         <> string7 " sumcost= " <> integerDec sumcost
         <> char7 '\n'
    part1 = 
      case wboTopCost wbo of
        Nothing -> string7 "soft: ;\n"
        Just t -> string7 "soft: " <> integerDec t <> string7 ";\n"
    part2 = mconcat $ map showSoftConstraint (wboConstraints wbo)

showSum :: Sum -> Builder
showSum = mconcat . map showWeightedTerm

showWeightedTerm :: WeightedTerm -> Builder
showWeightedTerm (c, lits) = foldr (\f g -> f <> char7 ' ' <> g) mempty (x:xs)
  where
    x = if c >= 0 then char7 '+' <> integerDec c else integerDec c
    xs = map showLit $ sortBy (comparing abs) lits

showLit :: Lit -> Builder
showLit lit = if lit > 0 then v else char7 '~' <> v
  where
    v = char7 'x' <> intDec (abs lit)

showConstraint :: Constraint -> Builder
showConstraint (lhs, op, rhs) =
  showSum lhs <> f op <>  char7 ' ' <> integerDec rhs <> string7 ";\n"
  where
    f Eq = char7 '='
    f NEq = string7 "!="
    f Gt = string7 ">"
    f Ge = string7 ">="
    f Lt = string7 "<"
    f Le = string7 "<="

showSoftConstraint :: SoftConstraint -> Builder
showSoftConstraint (cost, constr) =
  case cost of
    Nothing -> showConstraint constr
    Just c -> char7 '[' <> integerDec c <> string7 "] " <> showConstraint constr



-- | Generate a OPB format byte-string containing pseudo boolean problem.
toOPBByteString :: Formula -> BS.ByteString
toOPBByteString opb = toLazyByteString (opbBuilder opb)

-- | Generate a WBO format byte-string containing weighted boolean optimization problem.
toWBOByteString :: SoftFormula -> BS.ByteString
toWBOByteString wbo = toLazyByteString (wboBuilder wbo)

-- | Output a OPB file containing pseudo boolean problem.
writeOPBFile :: FilePath -> Formula -> IO ()
writeOPBFile filepath opb = withBinaryFile filepath WriteMode $ \h -> do
  hSetBuffering h (BlockBuffering Nothing)
  hPutOPB h opb

-- | Output a WBO file containing weighted boolean optimization problem.
writeWBOFile :: FilePath -> SoftFormula -> IO ()
writeWBOFile filepath wbo = withBinaryFile filepath WriteMode $ \h -> do
  hSetBuffering h (BlockBuffering Nothing)
  hPutWBO h wbo

-- | Output a OPB file to a 'Handle' using 'hPutBuilder'.
--
-- It is recommended that the 'Handle' is set to binary and
-- 'BlockBuffering' mode. See 'hSetBinaryMode' and 'hSetBuffering'.
--
-- This function is more efficient than 'hPut' . 'toOPBByteString'
-- because in many cases no buffer allocation has to be done.
hPutOPB :: Handle -> Formula -> IO ()
hPutOPB h opb = hPutBuilder h (opbBuilder opb)


-- | Output a WBO file to a 'Handle' using 'hPutBuilder'.
--
-- It is recommended that the 'Handle' is set to binary and
-- 'BlockBuffering' mode. See 'hSetBinaryMode' and 'hSetBuffering'.
--
-- This function is more efficient than 'hPut' . 'toWBOByteString'
-- because in many cases no buffer allocation has to be done.
hPutWBO :: Handle -> SoftFormula -> IO ()
hPutWBO h wbo = hPutBuilder h (wboBuilder wbo)

1	{-# OPTIONS_GHC -Wall #-}
2	-----------------------------------------------------------------------------
3	-- \|
4	-- Module : Data.PseudoBoolean.ByteStringBuilder
5	-- Copyright : (c) Masahiro Sakai 2011-2015
6	-- License : BSD-style
7	--
8	-- Maintainer : masahiro.sakai@gmail.com
9	-- Portability : portable
10	--
11	-----------------------------------------------------------------------------
12
13	module Data.PseudoBoolean.ByteStringBuilder
14	(
15	-- * Builder for (Lazy) ByteString generation
16	opbBuilder
17	, wboBuilder
18
19	-- * Lazy ByteString generation
20	, toOPBByteString
21	, toWBOByteString
22
23	-- * File I/O
24	, writeOPBFile
25	, writeWBOFile
26	, hPutOPB
27	, hPutWBO
28	) where
29
30	import qualified Prelude
31	import Prelude hiding (sum)
32	import qualified Data.IntSet as IntSet
33	import qualified Data.Set as Set
34	import Data.List (sortBy)
35	import Data.Maybe (maybeToList)
36	import qualified Data.ByteString.Lazy as BS
37	import Data.ByteString.Builder (Builder, intDec, integerDec, char7, string7, hPutBuilder, toLazyByteString)
38	import Data.Ord
39	import Math.NumberTheory.Logarithms (integerLog2)
40	import System.IO
41	import Data.PseudoBoolean.Types
42
43	-- \| A ByteString Builder which renders a OPB format byte-string containing pseudo boolean problem.
44	opbBuilder :: Formula -> Builder
45	opbBuilder opb = (size <> part1 <> part2)	1✔
46	where
47	nv = pbNumVars opb	1✔
48	nc = pbNumConstraints opb	1✔
NEW 49	neq = length [() \| (_lhs, Eq, _rhs) <- pbConstraints opb]	×
50	intsize = maximum $ 0 :	1✔
51	[ if tmp == 0 then 0 else 1 + integerLog2 tmp	1✔
52	\| (ts, d) <- [(ts, 0) \| (_, ts) <- maybeToList (pbObjectiveFunction opb)] ++ [(lhs,rhs) \| (lhs,_op,rhs) <- pbConstraints opb]	1✔
53	, let tmp = abs d + Prelude.sum [abs c \| (c,_) <- ts]	1✔
54	]
55	p = pbProducts opb	1✔
56	np = Set.size p	1✔
57	sp = Prelude.sum [IntSet.size tm \| tm <- Set.toList p]	1✔
58	size = string7 "* #variable= " <> intDec nv <> string7 " #constraint= " <> intDec nc <> string7 " #equal= " <> intDec neq <> string7 " intsize= " <> intDec intsize	1✔
59	<> (if np >= 1 then string7 " #product= " <> intDec np <> string7 " sizeproduct= " <> intDec sp else mempty)	1✔
60	<> char7 '\n'	1✔
61	part1 =	1✔
62	case pbObjectiveFunction opb of	1✔
63	Nothing -> mempty	1✔
64	Just (dir, o) ->
65	(case dir of	1✔
66	OptMin -> string7 "min"	1✔
67	OptMax -> string7 "max")	1✔
68	<> string7 ": " <> showSum o <> string7 ";\n"	1✔
69	part2 = mconcat $ map showConstraint (pbConstraints opb)	1✔
70
71	-- \| A ByteString Builder which renders a WBO format byte-string containing weighted boolean optimization problem.
72	wboBuilder :: SoftFormula -> Builder
73	wboBuilder wbo = size <> part1 <> part2	1✔
74	where
75	nv = wboNumVars wbo	1✔
76	nc = wboNumConstraints wbo	1✔
NEW 77	neq = length [() \| (_, (_lhs, Eq, _rhs)) <- wboConstraints wbo]	×
78	p = wboProducts wbo	1✔
79	np = Set.size p	1✔
80	sp = Prelude.sum [IntSet.size tm \| tm <- Set.toList p]	×
81	mincost =	1✔
82	case [c \| (Just c, _) <- wboConstraints wbo] of	1✔
83	[] -> 1 -- this should not happen	×
84	cs -> minimum cs	1✔
85	maxcost = maximum $ 0 : [c \| (Just c, _) <- wboConstraints wbo]	1✔
86	sumcost = Prelude.sum [c \| (Just c, _) <- wboConstraints wbo]	1✔
87	intsize = maximum $ 0 :	1✔
88	[ if tmp == 0 then 0 else 1 + integerLog2 tmp	1✔
89	\| (cs, d) <- ([sumcost], 0) : [(map fst lhs, rhs) \| (_,(lhs,_op,rhs)) <- wboConstraints wbo]	1✔
90	, let tmp = abs d + Prelude.sum [abs c \| c <- cs]	1✔
91	]
92	size = string7 "* #variable= " <> intDec nv <> string7 " #constraint= " <> intDec nc <> string7 " #equal= " <> intDec neq <> string7 " intsize= " <> intDec intsize	1✔
UNCOV 93	<> (if np >= 1 then string7 " #product= " <> intDec np <> string7 " sizeproduct= " <> intDec sp else mempty)	×
94	<> string7 " #soft= " <> intDec (wboNumSoft wbo)	1✔
95	<> string7 " mincost= " <> integerDec mincost	1✔
96	<> string7 " maxcost= " <> integerDec maxcost	1✔
97	<> string7 " sumcost= " <> integerDec sumcost	1✔
98	<> char7 '\n'	1✔
99	part1 =	1✔
100	case wboTopCost wbo of	1✔
101	Nothing -> string7 "soft: ;\n"	1✔
102	Just t -> string7 "soft: " <> integerDec t <> string7 ";\n"	1✔
103	part2 = mconcat $ map showSoftConstraint (wboConstraints wbo)	1✔
104
105	showSum :: Sum -> Builder
106	showSum = mconcat . map showWeightedTerm	1✔
107
108	showWeightedTerm :: WeightedTerm -> Builder
109	showWeightedTerm (c, lits) = foldr (\f g -> f <> char7 ' ' <> g) mempty (x:xs)	1✔
110	where
111	x = if c >= 0 then char7 '+' <> integerDec c else integerDec c	1✔
112	xs = map showLit $ sortBy (comparing abs) lits	1✔
113
114	showLit :: Lit -> Builder
115	showLit lit = if lit > 0 then v else char7 '~' <> v	1✔
116	where
117	v = char7 'x' <> intDec (abs lit)	1✔
118
119	showConstraint :: Constraint -> Builder
120	showConstraint (lhs, op, rhs) =	1✔
121	showSum lhs <> f op <> char7 ' ' <> integerDec rhs <> string7 ";\n"	1✔
122	where
123	f Eq = char7 '='	1✔
124	f NEq = string7 "!="	1✔
125	f Gt = string7 ">"	1✔
126	f Ge = string7 ">="	1✔
127	f Lt = string7 "<"	1✔
128	f Le = string7 "<="	1✔
129
130	showSoftConstraint :: SoftConstraint -> Builder
131	showSoftConstraint (cost, constr) =	1✔
132	case cost of	1✔
133	Nothing -> showConstraint constr	1✔
134	Just c -> char7 '[' <> integerDec c <> string7 "] " <> showConstraint constr	1✔
135
136
137
138	-- \| Generate a OPB format byte-string containing pseudo boolean problem.
139	toOPBByteString :: Formula -> BS.ByteString
140	toOPBByteString opb = toLazyByteString (opbBuilder opb)	1✔
141
142	-- \| Generate a WBO format byte-string containing weighted boolean optimization problem.
143	toWBOByteString :: SoftFormula -> BS.ByteString
144	toWBOByteString wbo = toLazyByteString (wboBuilder wbo)	1✔
145
146	-- \| Output a OPB file containing pseudo boolean problem.
147	writeOPBFile :: FilePath -> Formula -> IO ()
148	writeOPBFile filepath opb = withBinaryFile filepath WriteMode $ \h -> do	1✔
149	hSetBuffering h (BlockBuffering Nothing)	1✔
150	hPutOPB h opb	1✔
151
152	-- \| Output a WBO file containing weighted boolean optimization problem.
153	writeWBOFile :: FilePath -> SoftFormula -> IO ()
154	writeWBOFile filepath wbo = withBinaryFile filepath WriteMode $ \h -> do	1✔
155	hSetBuffering h (BlockBuffering Nothing)	1✔
156	hPutWBO h wbo	1✔
157
158	-- \| Output a OPB file to a 'Handle' using 'hPutBuilder'.
159	--
160	-- It is recommended that the 'Handle' is set to binary and
161	-- 'BlockBuffering' mode. See 'hSetBinaryMode' and 'hSetBuffering'.
162	--
163	-- This function is more efficient than 'hPut' . 'toOPBByteString'
164	-- because in many cases no buffer allocation has to be done.
165	hPutOPB :: Handle -> Formula -> IO ()
166	hPutOPB h opb = hPutBuilder h (opbBuilder opb)	1✔
167
168
169	-- \| Output a WBO file to a 'Handle' using 'hPutBuilder'.
170	--
171	-- It is recommended that the 'Handle' is set to binary and
172	-- 'BlockBuffering' mode. See 'hSetBinaryMode' and 'hSetBuffering'.
173	--
174	-- This function is more efficient than 'hPut' . 'toWBOByteString'
175	-- because in many cases no buffer allocation has to be done.
176	hPutWBO :: Handle -> SoftFormula -> IO ()
177	hPutWBO h wbo = hPutBuilder h (wboBuilder wbo)	1✔

msakai / pseudo-boolean / 127

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous