library(tidyverse)
library(stringr)
library(scales)
library(svglite)
library(ggplot2)
library(lvplot)
library(jsonlite)
library(xtable)

data_baseline <- (
  read_csv('./data/competition.baseline.csv', quote = "'")
) %>%
  mutate(
    total_dups = sapply(
      map(duplicates, function(dups) { sum(fromJSON(dups)$cls) }),
     "[[",
     1
    ),
    len = n_axioms + n_derived,
  )

stopifnot(data_baseline %>% tally(is.na(len)) == 0)
stopifnot(data_baseline %>% tally(n_rat > 0) == 0)

dir.create('./svg', showWarnings = FALSE)

p <- ggplot(
  data_baseline %>%
  filter(trim & total_dups > 0),
  aes(x = total_dups / (len + total_dups))
) +
  geom_histogram(color = 'white', binwidth = 5e-3) +
  scale_x_continuous(limits = c(0, 0.15), labels = scales::percent) +
  labs(x = 'Relative number of duplicates',
       y = 'Number of samples',
       fill = 'Instance class') +
  theme(legend.position = c(.8, .7), legend.background=element_blank())
ggsave('svg/relative-dups-competition.svg', plot = p, width = 4, height = 4)

data_baseline_clean <- data_baseline %>% filter(trim) %>%
  select(-trim, -n_rat, -duplicates, -total_dups) |>
  left_join(
    data_baseline %>% filter(!trim) %>% mutate(solver_len = len) %>%
      select(formula, solver_len),
  ) %>%
  mutate(formula = paste(formula, "xz", sep = "."))

families <- read_delim('./data/competition-families.csv', delim = ' ') |>
  inner_join(read_delim('./data/sc02to25-gbd-hashes-filenames.txt', delim = ' ')) %>%
  mutate(formula = filename) %>%
  select(-hash)

data <- read_csv('./data/competition.csv') |>
  left_join(data_baseline_clean) |>
  left_join(families) %>%
  mutate(gain.trim = solver_len / len,
         gain.bnb = len / best_proof,
         family_compact = case_match(
           family,
           c('xor-chain', 'tseitin-formulas', 'ordering-principle', 'sgen', 'pigeon-hole', 'mutilated-chessboard') ~ 'hard-synthetic',
           c('theorem-proving', 'design-debugging', 'hardware-verification', 'hardware-bmc', 'miter', 'fpga-routing') ~ 'hardware',
           c('bitvector', 'bounded-model-checking', 'software-verification', 'software-bmc') ~ 'software',
           c('planning') ~ 'planning',
           .default = NA))

dir.create('./reports', showWarnings = FALSE)

data %>%
  arrange(desc(gain.bnb)) %>%
  select(-family_compact) %>%
  write_csv("./reports/gains.csv")

data %>%
  filter(gain.bnb >= 10) %>%
  arrange(family, desc(gain.bnb)) %>%
  select(formula, family, len, best_proof) %>%
  mutate(formula = str_replace(formula, ".cnf.xz", "")) %>%
  mutate(across(
    .cols = matches('solver_len|len|best_proof'),
    .fns = ~ as.integer(.x))) %>%
  xtable(type = 'latex', label = "table:10x-gains") %>%
  print(file = 'tex/gains.tex', include.rownames = FALSE)


p <- ggplot(data, aes(y = family_compact, x = len / best_proof, fill = family_compact)) +
  geom_boxplot() +
  geom_vline(xintercept = 1, color = 'red') +
  scale_x_log10("Ratio of the trimmed CaDiCaL proof length\n to the best discovered proof length") +
                # breaks = trans_breaks("log10", function(x) 10^x),
                # labels = trans_format("log10", math_format(10^.x))) +
  labs(y = "Formula family") +
  theme(legend.position = "none",
	axis.text.y = element_text(angle = 45, vjust = 0.5, hjust = 1))
ggsave('svg/competition-gains-by-family.svg', plot = p, width = 4, height = 2)

p <- ggplot(data, aes(x = len / best_proof)) +
  geom_histogram(color = 'white') +
  scale_x_log10("Ratio of the trimmed CaDiCaL proof length\nto the best discovered proof length",
                labels = scales::percent) +
  geom_vline(xintercept = 1, color = 'red', linetype = 'dashed') +
  labs(y = "Number of samples")
ggsave('svg/competition-length.svg', plot = p, width = 4, height = 2)

data %>% mutate(gain = best_proof / len) %>%
  summarise(gain = quantile(gain, c(0.25, 0.5, 0.75), na.rm = TRUE), q = c(0.25, 0.5, 0.75))

data %>% mutate(gain = best_proof / len) %>%
  group_by(family_compact) %>%
  summarise(gain = quantile(gain, c(0.25, 0.5, 0.75), na.rm = TRUE), q = c(0.25, 0.5, 0.75))

p <- ggplot(data %>% mutate(is_hard = !is.na(family_compact) & family_compact == 'hard-synthetic'),
       aes(x = gain.trim, y = gain.bnb, color = is_hard)) +
  geom_point(shape = 4) +
  scale_x_log10("Ratio of CaDiCaL proof length\nto trimmed proof length") +
                # breaks = trans_breaks("log10", function(x) 10^x),
                # labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10("Ratio of trimmed proof length\nto the best discovered proof length") +
                # breaks = trans_breaks("log10", function(x) 10^x),
                # labels = trans_format("log10", math_format(10^.x))) +
  scale_color_manual("Known intractable instance?",
                     values = c("TRUE" = "red", "FALSE" = "#777")) +
  geom_vline(xintercept = 1, color = 'black') +
  geom_hline(yintercept = 1, color = 'black') +
  geom_vline(xintercept = 5, color = 'black', linetype = 'dashed') +
  geom_hline(yintercept = 5, color = 'black', linetype = 'dashed') +
  coord_equal()
ggsave("svg/trim-vs-bnb-reds.svg", p, width = 6, height = 3)

data %>%
  filter(gain.bnb >= 5 & gain.trim >= 5) %>%
  mutate(proof.bnb = best_proof, proof.trim = len, proof.orig = solver_len) %>%
  select(formula, proof.bnb, proof.trim, proof.orig)
