-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
2 changed files
with
120 additions
and
33 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,11 +1,13 @@ | ||
#!/usr/bin/env Rscript | ||
# generate a cactus plot (png and pdf) from CVS files | ||
# USAGE: mkCactus runs [subtitle] [nproblems] | ||
# where runs is a filename that contains a list of CSV filenames which are generated by sat-benchmark | ||
# USAGE: mkCactus runs [nproblems] [subtitle] | ||
# where runs is a filename that contains a list of CSV filenames which are generated by satbenchmark2csv | ||
library("ggplot2") | ||
version = "0.11.0" | ||
version = "0.11.1 for SC2018" | ||
|
||
getData = function (t, p, c) { | ||
solved = 0 | ||
|
||
getData = function (t, p, cut) { | ||
df1 <- read.csv(as.character(t[[1]]), header=T, sep=",", comment="#") | ||
if (nrow(df1) == 0) { return(NULL) } | ||
df2 <- data.frame(solver=df1[["solver"]], | ||
|
@@ -17,63 +19,64 @@ getData = function (t, p, c) { | |
} else { | ||
df2[["valid"]] <- numeric(nrow(df2)) | ||
} | ||
if (0 < c) { | ||
df2 <- df2[1:c,] | ||
if (0 < cut) { | ||
df2 <- df2[1:min(nrow(df2),cut),] | ||
} | ||
df2 <- df2[order(df2[["time"]]),] # sort by time | ||
if (p && t[[2]] != "") { df2[["solver"]] = sub("^ +", "", as.character(t[[2]])) } | ||
df2[["num"]] <- 1:nrow(df2) # reassign rownumbers | ||
thr <- max(df2[["time"]]) | ||
solved <<- max(solved, nrow(subset(df2, time < 0.8 * thr))) | ||
df2 | ||
} | ||
|
||
graph = function (d, subt) { | ||
graph = function (d, subt, cut) { | ||
g <- ggplot(d, aes(num, time, color=solver, size=solver, alpha=solver)) | ||
g <- g + geom_point(size=0.5) | ||
g <- g + geom_line(data=d) | ||
g <- g + geom_point(data=subset(d, valid==3),size=2,shape=4) | ||
g <- g + scale_size_manual(values=rep(0.6, times=nrow(d))) | ||
g <- g + scale_alpha_manual(values=rep(1.0, times=nrow(d))) | ||
g <- g + geom_point(data=subset(d, valid==3),size=2,shape=4) | ||
# g <- g + scale_size_manual(values=c(0.7,0.7,0.7,0.7,0.3,0.3,0.3)) -- by aes(size=solver) | ||
# g <- g + scale_alpha_manual(values=c(1.0,1.0,1.0,1.0,0.5,0.5,0.5)) -- by aes(alpha=solver) | ||
g <- g + theme(legend.position = c(0.85,0.2), legend.justification = c(1,0)) | ||
g <- g + scale_x_continuous(limits=c(0,350), breaks=seq(0,350,10), expand=c(0,4)) | ||
g <- g + scale_y_continuous(limits=c(0, max(d$time)), breaks=seq(0,max(d$time),100), expand=c(0,4)) | ||
# g <- g + scale_y_continuous(limits=c(0,410) ,breaks=seq(0,410,100)) | ||
g <- g + labs(title="Cactus plot on SAT-Race 2017 Main track (with a short timeout)", subtitle=subt, | ||
x="#solved", y="execution time [sec]") | ||
g <- g + annotate("text", x=0.75*max(d$num), y=10, | ||
label=paste(format(as.POSIXlt(Sys.time()), "%Y-%m-%dT%H:%M:%S"), " ", "drawn with mkCactus.R (ver. ", version, ")", sep=""), | ||
color="darkgray", size=2.6) | ||
maxx = 400 | ||
g <- g + theme(legend.position = c(0.95,0.05), legend.justification = c(1,0)) | ||
g <- g + scale_y_continuous(limits=c(0,max(d$time)), breaks=seq(0,max(d$time),100), expand=c(0.01,4)) | ||
g <- g + scale_x_continuous(limits=c(0,maxx), breaks=seq(00,maxx,10), expand=c(0,2)) | ||
#g <- g + annotate("text", x=100, y=50, | ||
# label=paste(format(as.POSIXlt(Sys.time()), "%Y-%m-%dT%H:%M:%S"), " ", "drawn with mkCactusL.R (ver. ", version, ")", sep=""), | ||
# color="darkgray", size=2.6) | ||
g <- g + labs(title="Cactus plot on SAT Competition 2018 Benchmark Main track", subtitle=subt, | ||
x=if (0 < cut) paste("#solved out of ", cut, sep="") else "#solved", y="CPU time [sec]") | ||
print(g) | ||
} | ||
|
||
(function() { | ||
merged <- list() | ||
args <- commandArgs(trailingOnly=TRUE) | ||
ts <-format(as.POSIXlt(Sys.time()), "%Y-%m-%dT%H:%M:%S") | ||
subt <- paste(" - ", ts, " drawn with mkCactus.R (ver. ", version, ")", sep="") | ||
if (0 < length(args)){ | ||
|
||
if (1 <= length(args)){ | ||
exps <- args[1] | ||
name <- gsub("\\.[^.]+$", "", exps) | ||
targetPDF <- paste("cactus-", name, ".pdf", sep="") | ||
targetPNG <- paste("cactus-", name, ".png", sep="") | ||
if (1 < length(args) && args[2] != "") { subt <- args[2] } | ||
targetPDF <- paste("Cactus-", name, ".pdf", sep="") | ||
targetPNG <- paste("Cactus-", name, ".png", sep="") | ||
} else { | ||
exps <- "runs" | ||
name <- "runs" | ||
targetPDF <- "cactus-SC17main.pdf" | ||
targetPNG <- "cactus-SC17main.png" | ||
targetPDF <- "Cactus-SC18main.pdf" | ||
targetPNG <- "Cactus-SC18main.png" | ||
} | ||
cut <- -1 | ||
if (2 < length(args)) { | ||
cut <- as.integer(args[3]) | ||
} | ||
runs <- read.csv(exps, comment="#", sep=",", header=F) | ||
withTag <- 1 < ncol(runs) | ||
for (i in seq(nrow(runs))) { merged = rbind(merged, getData(runs[i,], withTag, cut)); } | ||
|
||
if (2 <= length(args)) { cut <- as.integer(args[2] ) } | ||
subt <- paste(exps, " -- ", ts, " drawn with mkCactus.R (ver. ", version, ")", sep="") | ||
spec <- " - CPU: Intel Core [email protected], Mem: 32GB, SSD, NixOS on Darwin" | ||
#runs <- read.csv(exps, comment="#", sep=",", header=F) | ||
#withTag <- 1 < ncol(runs) | ||
#for (i in seq(nrow(runs))) { merged = rbind(merged, getData(runs[i,], withTag, cut)); } | ||
merged = rbind(merged, getData(exps, FALSE, 5000)); | ||
cairo_pdf(filename=targetPDF, width=10, height=6, antialias="subpixel", onefile=TRUE) | ||
graph(merged, subt) | ||
graph(merged, paste(subt, spec, sep="\n"), cut) | ||
ggsave(filename=targetPDF, width=10, height=6, scale=1.0, dpi=400) | ||
ggsave(filename=targetPNG, width=10, height=6, scale=1.0, dpi=200) | ||
# ggsave(filename=targetPNG, width=10, height=6, scale=1.0, dpi=400) | ||
})() |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,84 @@ | ||
#!/usr/bin/env Rscript | ||
# generate a cactus plot (png and pdf) from CVS files | ||
# USAGE: mkCactusL runs [nproblems] [subtitle] | ||
# where runs is a filename that contains a list of CSV filenames which are generated by satbenchmark2csv | ||
library("ggplot2") | ||
version = "0.13 for SR2019" | ||
|
||
solved = 0 | ||
|
||
getData = function (t, p, cut) { | ||
df1 <- read.csv(as.character(t[[1]]), header=T, sep=",", comment="#") | ||
if (nrow(df1) == 0) { return(NULL) } | ||
df2 <- data.frame(solver=df1[["solver"]], | ||
num=df1[["num"]], | ||
target=df1[["target"]], | ||
time=df1[["time"]]) | ||
if (ncol(df1) == 5) { | ||
df2[["valid"]] <- df1[["valid"]] | ||
} else { | ||
df2[["valid"]] <- numeric(nrow(df2)) | ||
} | ||
if (0 < cut) { | ||
df2 <- df2[1:min(nrow(df2),cut),] | ||
} | ||
df2 <- df2[order(df2[["time"]]),] # sort by time | ||
if (p && t[[2]] != "") { df2[["solver"]] = sub("^ +", "", as.character(t[[2]])) } | ||
df2[["num"]] <- 1:nrow(df2) # reassign rownumbers | ||
thr <- max(df2[["time"]]) | ||
solved <<- max(solved, nrow(subset(df2, time < 0.8 * thr))) | ||
df2 | ||
} | ||
|
||
graph = function (d, subt, cut) { | ||
g <- ggplot(d, aes(num, time, color=solver, size=solver, alpha=solver)) | ||
g <- g + geom_point(size=0.5) | ||
g <- g + geom_line(data=d) | ||
g <- g + geom_point(data=subset(d, valid==3),size=2,shape=4) | ||
g <- g + scale_size_manual(values=rep(0.6, times=nrow(d))) | ||
g <- g + scale_alpha_manual(values=rep(1.0, times=nrow(d))) | ||
# g <- g + scale_size_manual(values=c(0.7,0.7,0.7,0.7,0.3,0.3,0.3)) -- by aes(size=solver) | ||
# g <- g + scale_alpha_manual(values=c(1.0,1.0,1.0,1.0,0.5,0.5,0.5)) -- by aes(alpha=solver) | ||
maxx = 400 | ||
g <- g + theme(legend.position = c(0.95,0.05), legend.justification = c(1,0)) | ||
g <- g + scale_y_continuous(limits=c(0,max(d$time)), breaks=seq(0,max(d$time),100), expand=c(0.01,4)) | ||
g <- g + scale_x_continuous(limits=c(0,maxx), breaks=seq(00,maxx,10), expand=c(0,2)) | ||
#g <- g + annotate("text", x=100, y=50, | ||
# label=paste(format(as.POSIXlt(Sys.time()), "%Y-%m-%dT%H:%M:%S"), " ", "drawn with mkCactusL.R (ver. ", version, ")", sep=""), | ||
# color="darkgray", size=2.6) | ||
g <- g + labs(title="Cactus plot on SAT RACE 2019 Benchmark Main track", subtitle=subt, | ||
x=if (0 < cut) paste("#solved out of ", cut, sep="") else "#solved", y="CPU time [sec]") | ||
print(g) | ||
} | ||
|
||
(function() { | ||
merged <- list() | ||
args <- commandArgs(trailingOnly=TRUE) | ||
ts <-format(as.POSIXlt(Sys.time()), "%Y-%m-%dT%H:%M:%S") | ||
|
||
if (1 <= length(args)){ | ||
exps <- args[1] | ||
name <- gsub("\\.[^.]+$", "", exps) | ||
targetPDF <- paste("CactusL-", name, ".pdf", sep="") | ||
targetPNG <- paste("CactusL-", name, ".png", sep="") | ||
} else { | ||
exps <- "runs" | ||
name <- "runs" | ||
targetPDF <- "CactusL-SC18main.pdf" | ||
targetPNG <- "CactusL-SC18main.png" | ||
} | ||
cut <- -1 | ||
if (2 <= length(args)) { cut <- as.integer(args[2] ) } | ||
subt <- paste(exps, " -- ", ts, " drawn with mkCactusL.R (ver. ", version, ")", sep="") | ||
spec <- " - CPU: Intel Core [email protected], Mem: 32GB, SDD, NixOS on Darwin" | ||
# if (3 <= length(args) && args[3] != "") { subt <- args[3] } | ||
runs <- read.csv(exps, comment="#", sep=",", header=F) | ||
withTag <- 1 < ncol(runs) | ||
for (i in seq(nrow(runs))) { merged = rbind(merged, getData(runs[i,], withTag, cut)); } | ||
|
||
# png(filename=targetPNG, width=1600, height=1000) | ||
# cairo_pdf(filename=targetPDF, width=10, height=6, antialias="subpixel", onefile=TRUE) | ||
graph(merged, paste(subt, spec, sep="\n"), cut) | ||
ggsave(filename=targetPDF, width=10, height=6, scale=1.0, dpi=400) | ||
# ggsave(filename=targetPNG, width=10, height=6, scale=1.0, dpi=400) | ||
})() |