diff --git a/examples/dimacs/bf/bf0432-007.cnf b/data/dimacs/bf/bf0432-007.cnf similarity index 100% rename from examples/dimacs/bf/bf0432-007.cnf rename to data/dimacs/bf/bf0432-007.cnf diff --git a/examples/dimacs/bf/bf1355-075.cnf b/data/dimacs/bf/bf1355-075.cnf similarity index 100% rename from examples/dimacs/bf/bf1355-075.cnf rename to data/dimacs/bf/bf1355-075.cnf diff --git a/examples/dimacs/bf/bf1355-638.cnf b/data/dimacs/bf/bf1355-638.cnf similarity index 100% rename from examples/dimacs/bf/bf1355-638.cnf rename to data/dimacs/bf/bf1355-638.cnf diff --git a/examples/dimacs/bf/bf2670-001.cnf b/data/dimacs/bf/bf2670-001.cnf similarity index 100% rename from examples/dimacs/bf/bf2670-001.cnf rename to data/dimacs/bf/bf2670-001.cnf diff --git a/examples/dimacs/bf/descr.html b/data/dimacs/bf/descr.html similarity index 100% rename from examples/dimacs/bf/descr.html rename to data/dimacs/bf/descr.html diff --git a/examples/dimacs/bf/ssa0432-003.cnf b/data/dimacs/bf/ssa0432-003.cnf similarity index 100% rename from examples/dimacs/bf/ssa0432-003.cnf rename to data/dimacs/bf/ssa0432-003.cnf diff --git a/examples/dimacs/bf/ssa2670-130.cnf b/data/dimacs/bf/ssa2670-130.cnf similarity index 100% rename from examples/dimacs/bf/ssa2670-130.cnf rename to data/dimacs/bf/ssa2670-130.cnf diff --git a/examples/dimacs/bf/ssa2670-141.cnf b/data/dimacs/bf/ssa2670-141.cnf similarity index 100% rename from examples/dimacs/bf/ssa2670-141.cnf rename to data/dimacs/bf/ssa2670-141.cnf diff --git a/examples/dimacs/bf/ssa6288-047.cnf b/data/dimacs/bf/ssa6288-047.cnf similarity index 100% rename from examples/dimacs/bf/ssa6288-047.cnf rename to data/dimacs/bf/ssa6288-047.cnf diff --git a/examples/dimacs/bf/ssa7552-038.cnf b/data/dimacs/bf/ssa7552-038.cnf similarity index 100% rename from examples/dimacs/bf/ssa7552-038.cnf rename to data/dimacs/bf/ssa7552-038.cnf diff --git a/examples/dimacs/bf/ssa7552-158.cnf b/data/dimacs/bf/ssa7552-158.cnf similarity index 100% rename from examples/dimacs/bf/ssa7552-158.cnf rename to data/dimacs/bf/ssa7552-158.cnf diff --git a/examples/dimacs/bf/ssa7552-159.cnf b/data/dimacs/bf/ssa7552-159.cnf similarity index 100% rename from examples/dimacs/bf/ssa7552-159.cnf rename to data/dimacs/bf/ssa7552-159.cnf diff --git a/examples/dimacs/bf/ssa7552-160.cnf b/data/dimacs/bf/ssa7552-160.cnf similarity index 100% rename from examples/dimacs/bf/ssa7552-160.cnf rename to data/dimacs/bf/ssa7552-160.cnf diff --git a/examples/dimacs/blocksworld/anomaly.cnf b/data/dimacs/blocksworld/anomaly.cnf similarity index 100% rename from examples/dimacs/blocksworld/anomaly.cnf rename to data/dimacs/blocksworld/anomaly.cnf diff --git a/examples/dimacs/blocksworld/bw_large.a.cnf b/data/dimacs/blocksworld/bw_large.a.cnf similarity index 100% rename from examples/dimacs/blocksworld/bw_large.a.cnf rename to data/dimacs/blocksworld/bw_large.a.cnf diff --git a/examples/dimacs/blocksworld/bw_large.b.cnf b/data/dimacs/blocksworld/bw_large.b.cnf similarity index 100% rename from examples/dimacs/blocksworld/bw_large.b.cnf rename to data/dimacs/blocksworld/bw_large.b.cnf diff --git a/examples/dimacs/blocksworld/bw_large.c.cnf b/data/dimacs/blocksworld/bw_large.c.cnf similarity index 100% rename from examples/dimacs/blocksworld/bw_large.c.cnf rename to data/dimacs/blocksworld/bw_large.c.cnf diff --git a/examples/dimacs/blocksworld/descr.html b/data/dimacs/blocksworld/descr.html similarity index 100% rename from examples/dimacs/blocksworld/descr.html rename to data/dimacs/blocksworld/descr.html diff --git a/examples/dimacs/blocksworld/huge.cnf b/data/dimacs/blocksworld/huge.cnf similarity index 100% rename from examples/dimacs/blocksworld/huge.cnf rename to data/dimacs/blocksworld/huge.cnf diff --git a/examples/dimacs/blocksworld/medium.cnf b/data/dimacs/blocksworld/medium.cnf similarity index 100% rename from examples/dimacs/blocksworld/medium.cnf rename to data/dimacs/blocksworld/medium.cnf diff --git a/examples/dimacs/bmc/bmc-ibm-1.cnf b/data/dimacs/bmc/bmc-ibm-1.cnf similarity index 100% rename from examples/dimacs/bmc/bmc-ibm-1.cnf rename to data/dimacs/bmc/bmc-ibm-1.cnf diff --git a/examples/dimacs/bmc/bmc-ibm-2.cnf b/data/dimacs/bmc/bmc-ibm-2.cnf similarity index 100% rename from examples/dimacs/bmc/bmc-ibm-2.cnf rename to data/dimacs/bmc/bmc-ibm-2.cnf diff --git a/examples/dimacs/bmc/bmc-ibm-3.cnf b/data/dimacs/bmc/bmc-ibm-3.cnf similarity index 100% rename from examples/dimacs/bmc/bmc-ibm-3.cnf rename to data/dimacs/bmc/bmc-ibm-3.cnf diff --git a/examples/dimacs/bmc/bmc-ibm-4.cnf b/data/dimacs/bmc/bmc-ibm-4.cnf similarity index 100% rename from examples/dimacs/bmc/bmc-ibm-4.cnf rename to data/dimacs/bmc/bmc-ibm-4.cnf diff --git a/examples/dimacs/bmc/bmc-ibm-5.cnf b/data/dimacs/bmc/bmc-ibm-5.cnf similarity index 100% rename from examples/dimacs/bmc/bmc-ibm-5.cnf rename to data/dimacs/bmc/bmc-ibm-5.cnf diff --git a/examples/dimacs/bmc/bmc-ibm-7.cnf b/data/dimacs/bmc/bmc-ibm-7.cnf similarity index 100% rename from examples/dimacs/bmc/bmc-ibm-7.cnf rename to data/dimacs/bmc/bmc-ibm-7.cnf diff --git a/examples/dimacs/logistics/descr.html b/data/dimacs/logistics/descr.html similarity index 100% rename from examples/dimacs/logistics/descr.html rename to data/dimacs/logistics/descr.html diff --git a/examples/dimacs/logistics/logistics.a.cnf b/data/dimacs/logistics/logistics.a.cnf similarity index 100% rename from examples/dimacs/logistics/logistics.a.cnf rename to data/dimacs/logistics/logistics.a.cnf diff --git a/examples/dimacs/logistics/logistics.b.cnf b/data/dimacs/logistics/logistics.b.cnf similarity index 100% rename from examples/dimacs/logistics/logistics.b.cnf rename to data/dimacs/logistics/logistics.b.cnf diff --git a/examples/dimacs/logistics/logistics.c.cnf b/data/dimacs/logistics/logistics.c.cnf similarity index 100% rename from examples/dimacs/logistics/logistics.c.cnf rename to data/dimacs/logistics/logistics.c.cnf diff --git a/examples/dimacs/logistics/logistics.d.cnf b/data/dimacs/logistics/logistics.d.cnf similarity index 100% rename from examples/dimacs/logistics/logistics.d.cnf rename to data/dimacs/logistics/logistics.d.cnf diff --git a/examples/dimacs/parity/descr b/data/dimacs/parity/descr similarity index 100% rename from examples/dimacs/parity/descr rename to data/dimacs/parity/descr diff --git a/examples/dimacs/parity/par16-1-c.cnf b/data/dimacs/parity/par16-1-c.cnf similarity index 100% rename from examples/dimacs/parity/par16-1-c.cnf rename to data/dimacs/parity/par16-1-c.cnf diff --git a/examples/dimacs/parity/par16-1.cnf b/data/dimacs/parity/par16-1.cnf similarity index 100% rename from examples/dimacs/parity/par16-1.cnf rename to data/dimacs/parity/par16-1.cnf diff --git a/examples/dimacs/parity/par16-2-c.cnf b/data/dimacs/parity/par16-2-c.cnf similarity index 100% rename from examples/dimacs/parity/par16-2-c.cnf rename to data/dimacs/parity/par16-2-c.cnf diff --git a/examples/dimacs/parity/par16-2.cnf b/data/dimacs/parity/par16-2.cnf similarity index 100% rename from examples/dimacs/parity/par16-2.cnf rename to data/dimacs/parity/par16-2.cnf diff --git a/examples/dimacs/parity/par16-3-c.cnf b/data/dimacs/parity/par16-3-c.cnf similarity index 100% rename from examples/dimacs/parity/par16-3-c.cnf rename to data/dimacs/parity/par16-3-c.cnf diff --git a/examples/dimacs/parity/par16-3.cnf b/data/dimacs/parity/par16-3.cnf similarity index 100% rename from examples/dimacs/parity/par16-3.cnf rename to data/dimacs/parity/par16-3.cnf diff --git a/examples/dimacs/parity/par16-4-c.cnf b/data/dimacs/parity/par16-4-c.cnf similarity index 100% rename from examples/dimacs/parity/par16-4-c.cnf rename to data/dimacs/parity/par16-4-c.cnf diff --git a/examples/dimacs/parity/par16-4.cnf b/data/dimacs/parity/par16-4.cnf similarity index 100% rename from examples/dimacs/parity/par16-4.cnf rename to data/dimacs/parity/par16-4.cnf diff --git a/examples/dimacs/parity/par16-5-c.cnf b/data/dimacs/parity/par16-5-c.cnf similarity index 100% rename from examples/dimacs/parity/par16-5-c.cnf rename to data/dimacs/parity/par16-5-c.cnf diff --git a/examples/dimacs/parity/par16-5.cnf b/data/dimacs/parity/par16-5.cnf similarity index 100% rename from examples/dimacs/parity/par16-5.cnf rename to data/dimacs/parity/par16-5.cnf diff --git a/examples/dimacs/parity/par8-1-c.cnf b/data/dimacs/parity/par8-1-c.cnf similarity index 100% rename from examples/dimacs/parity/par8-1-c.cnf rename to data/dimacs/parity/par8-1-c.cnf diff --git a/examples/dimacs/parity/par8-1.cnf b/data/dimacs/parity/par8-1.cnf similarity index 100% rename from examples/dimacs/parity/par8-1.cnf rename to data/dimacs/parity/par8-1.cnf diff --git a/examples/dimacs/parity/par8-2-c.cnf b/data/dimacs/parity/par8-2-c.cnf similarity index 100% rename from examples/dimacs/parity/par8-2-c.cnf rename to data/dimacs/parity/par8-2-c.cnf diff --git a/examples/dimacs/parity/par8-2.cnf b/data/dimacs/parity/par8-2.cnf similarity index 100% rename from examples/dimacs/parity/par8-2.cnf rename to data/dimacs/parity/par8-2.cnf diff --git a/examples/dimacs/parity/par8-3-c.cnf b/data/dimacs/parity/par8-3-c.cnf similarity index 100% rename from examples/dimacs/parity/par8-3-c.cnf rename to data/dimacs/parity/par8-3-c.cnf diff --git a/examples/dimacs/parity/par8-3.cnf b/data/dimacs/parity/par8-3.cnf similarity index 100% rename from examples/dimacs/parity/par8-3.cnf rename to data/dimacs/parity/par8-3.cnf diff --git a/examples/dimacs/parity/par8-4-c.cnf b/data/dimacs/parity/par8-4-c.cnf similarity index 100% rename from examples/dimacs/parity/par8-4-c.cnf rename to data/dimacs/parity/par8-4-c.cnf diff --git a/examples/dimacs/parity/par8-4.cnf b/data/dimacs/parity/par8-4.cnf similarity index 100% rename from examples/dimacs/parity/par8-4.cnf rename to data/dimacs/parity/par8-4.cnf diff --git a/examples/dimacs/parity/par8-5-c.cnf b/data/dimacs/parity/par8-5-c.cnf similarity index 100% rename from examples/dimacs/parity/par8-5-c.cnf rename to data/dimacs/parity/par8-5-c.cnf diff --git a/examples/dimacs/parity/par8-5.cnf b/data/dimacs/parity/par8-5.cnf similarity index 100% rename from examples/dimacs/parity/par8-5.cnf rename to data/dimacs/parity/par8-5.cnf diff --git a/examples/dimacs/phole/descr.html b/data/dimacs/phole/descr.html similarity index 100% rename from examples/dimacs/phole/descr.html rename to data/dimacs/phole/descr.html diff --git a/examples/dimacs/phole/hole6.cnf b/data/dimacs/phole/hole6.cnf similarity index 100% rename from examples/dimacs/phole/hole6.cnf rename to data/dimacs/phole/hole6.cnf diff --git a/examples/dimacs/phole/hole7.cnf b/data/dimacs/phole/hole7.cnf similarity index 100% rename from examples/dimacs/phole/hole7.cnf rename to data/dimacs/phole/hole7.cnf diff --git a/examples/dimacs/phole/hole8.cnf b/data/dimacs/phole/hole8.cnf similarity index 100% rename from examples/dimacs/phole/hole8.cnf rename to data/dimacs/phole/hole8.cnf diff --git a/ersatz.cabal b/ersatz.cabal index 2d65c8c..6e8dc88 100644 --- a/ersatz.cabal +++ b/ersatz.cabal @@ -29,6 +29,21 @@ extra-source-files: README.md CHANGELOG.md +data-files: + data/dimacs/bf/descr.html + data/dimacs/bf/*.cnf + data/dimacs/blocksworld/descr.html + data/dimacs/blocksworld/*.cnf + data/dimacs/bmc/*.cnf + data/dimacs/logistics/descr.html + data/dimacs/logistics/logistics.a.cnf + data/dimacs/logistics/logistics.b.cnf + data/dimacs/logistics/logistics.c.cnf + data/dimacs/logistics/logistics.d.cnf + data/dimacs/parity/descr + data/dimacs/parity/*.cnf + data/dimacs/phole/descr.html + data/dimacs/phole/*.cnf source-repository head type: git diff --git a/examples/dimacs/GraphResult.hs b/examples/dimacs/GraphResult.hs deleted file mode 100644 index ad42212..0000000 --- a/examples/dimacs/GraphResult.hs +++ /dev/null @@ -1,206 +0,0 @@ -{-# OPTIONS_GHC -fglasgow-exts #-} - --- | This file cooperates with @benchmark.sh@. This script grovels over the --- result files produced by @benchmark.sh@ given on the command-line and outputs --- a PNG graph comparison of the runtime data. --- --- Example usage: --- --- runghc GraphResult.hs /path/to/benchmark/date-1 ... /path/to/benchmark/date-n -module Main where - -import Control.Monad -import Data.List( foldl', intercalate, transpose, genericLength ) -import Graphics.Rendering.Chart -import System.Console.GetOpt -import System.Environment( getArgs ) -import System.Exit( exitWith, ExitCode(..) ) -import System.FilePath.Posix( pathSeparator ) -import Text.Regex - -type RegexGroup = ([String], String) - --- | Assume the input contains @n>0@ records delimited at the start by --- whatever matches regexp. Each element @(xs, s)@ of @groups rx f s@ is such --- that (1) @xs@ is a list of submatches of @rx@ and (2) @s@ is the string --- from (and not including) the last match, up to and not including the next --- match (if any). --- --- If the regex fails to match at all (i.e. @n=0@), the empty list is --- returned. -groups :: Regex -> String -> [RegexGroup] -groups markerRx s = snd $ groups' markerRx s - where - -- Returns the text before the match, if any match, in its first position. - groups' markerRx s = - case matchRegexAll markerRx s of - Nothing -> (s, []) - Just (beforeMatch, _matched, afterMatch, submatches) -> - let (beforeNext, retList) = groups' markerRx afterMatch - in ( beforeMatch, (submatches, beforeNext) : retList ) - ------------------------------------------------------------------------------- --- Plots - -plotColumnPoints col s = defaultPlotPoints - { plot_points_style = s - , plot_points_values = zipWith Point [1..] col } - -plotLines col s = defaultPlotLines - { plot_lines_style = s - , plot_lines_values = [zipWith Point [1..] col] } - -verticalLines numTests s = defaultPlotLines - { plot_lines_style = s - , plot_lines_values = map (\p -> [Point (p_x p) 1, p]) $ - zipWith Point [1..numTests] (repeat 210) } - -manyTickAxis = defaultAxis - --- input matrix a list of rows of data; first row has test label -myLayout header yLabel names matrix = defaultLayout1 - { layout1_title = header ++ intercalate " vs. " names - , layout1_plots = - -- Vertical lines. - ("", HA_Bottom, VA_Right, - toPlot (verticalLines (genericLength matrix) (gridLineStyle dimGray))): - -- Show each column of data, not including the label column. - concat - [ [ ("", HA_Bottom, VA_Right, toPlot (plotLines col (lineStyle color))) - , (yLabel ++ ": " ++ name ++ " (" ++ show i ++ ")", HA_Bottom, VA_Left, - toPlot (plotColumnPoints col (pointStyle color))) ] - | i <- [1..length names] - | name <- names - | col <- pointsRows - | color <- map toColor colors ] } - where - pointStyle color = exes 7 2 color - gridLineStyle color = dashedLine 0.3 [4.0] (toColor color) - lineStyle color = solidLine 0.4 color --dashedLine 0.4 [7.0] color - - black = Color 0 0 0 - red = Color 1 0 0 - green = Color 0 1 0 - blue = Color 0 0 1 - dimGray = IntColor 105 105 105 - colors = [blue, red, green] - - -- remove label, convert to doubles, and turn into list of columns - pointsRows = transpose . map (map read) . map tail $ matrix :: [[Double]] - -data IntColor = IntColor Int Int Int -class ToColor a where - toColor :: a -> Color -instance ToColor Color where - toColor = id -instance ToColor IntColor where - toColor (IntColor ri gi bi) = Color (r/255) (g/255) (b/255) - where r = fromIntegral ri - g = fromIntegral gi - b = fromIntegral bi -instance Show Color where - show (Color r g b) = "Color " ++ intercalate " " [show r, show g, show b] - -savePNG filename header yLabel names matrix = - renderableToPNGFile (toRenderable (myLayout header yLabel names matrix)) - 1024 768 filename - ------------------------------------------------------------------------------- --- Statistics - --- | @deltas xs ys@ produces a list @zs@ such that @zs!!i == (xs!!i - ys!!i)@ --- for all @i@ for which indexing @xs@ and @ys@ is correct. --- --- @deltas xs (repeat 0) == xs@ -deltas :: (Num a) => [a] -> [a] -> [a] -{-# INLINE deltas #-} -deltas = zipWith (-) - -deltasF :: (Floating r) => [r] -> [r] -> [r] -{-# INLINE deltasF #-} -deltasF = zipWith (-) - ------------------------------------------------------------------------------- --- Main - --- group is filename at start of each run -satrunRx = mkRegex $ - "Solving ([-_./a-zA-Z0-9]+[.]cnf)"-- ./bench/bf/bf0432-007.cnf - --- group is user time -userTimeRx = mkRegex "([[:digit:]]+[.][[:digit:]]+) user" - -findUserTime s = - head `fmap` matchRegex userTimeRx s - - - - -main = do - (opts, dirs) <- getArgs >>= parseOptions - when (null dirs) $ do putStrLn "Nothing to do." - putStrLn (usageInfo usageHeader validOptions) - exitWith ExitSuccess - groupList <- forM dirs (\dir -> groups satrunRx `liftM` - readFile (dir ++ [pathSeparator] ++ "result.1")) - :: IO [[RegexGroup]] - titles <- forM dirs (\dir -> readFile (dir ++ [pathSeparator] ++ "info")) - let benchFiles = map (head . fst) $ head groupList - showTime maybeTime = case maybeTime of - Nothing -> optionMax opts - Just time -> time - labelRow = replicate (length dirs + 1) "IGNOREDLABEL" - dataMatrix = - (labelRow :) - . zipWith (:) benchFiles - . transpose - . reverse $ - foldl' (\matrix grouping -> - (map showTime . map findUserTime . map snd $ grouping) - : matrix) - [] groupList - :: [[String]] - putStrLn $ "Saving '" ++ optionOutput opts ++ "'..." - savePNG (optionOutput opts) (optionHeader opts) (optionYLabel opts) titles - (tail dataMatrix) --- forM_ dataMatrix $ putStrLn . intercalate " " - - - -validOptions :: [OptDescr (RunOptions -> RunOptions)] -validOptions = - [ Option [] ["header"] (ReqArg (\t opts -> opts{ optionHeader = t }) "STRING") - "Header for the graph." - , Option ['o'] ["output"] - (ReqArg (\t opts -> opts{ optionOutput = t }) "FILENAME") - "Output filename, a PNG." - , Option [] ["ylabel"] (ReqArg (\t opts -> opts{ optionYLabel = t }) "STRING") - "Label of the graphed value." - , Option [] ["max"] - (ReqArg (\t opts -> opts{ optionMax = t }) "NUMBER") - "Height of y axis on graph." ] - -data RunOptions = RunOptions - { optionHeader :: String - , optionOutput :: String - , optionMax :: String - , optionYLabel :: String } -defaultRunOptions = RunOptions - { optionHeader = "funsat comparison: " - , optionOutput = "result.png" - , optionMax = "300.0" - , optionYLabel = "y" } - --- Parse options, possibly exiting if there is nothing to do, or an error. -parseOptions :: [String] -> IO (RunOptions, [FilePath]) -parseOptions args = do - let (runOptTranss, filepaths, errors) = getOpt RequireOrder validOptions args - when (not (null errors)) $ do { mapM_ putStr errors ; - putStrLn (usageInfo usageHeader validOptions) ; - exitWith (ExitFailure 1) } - return (foldr id defaultRunOptions runOptTranss, filepaths) - -usageHeader = - "Usage: GraphResult [options] ... \nOptions:\n" - -