library(ggplot2)
library(patchwork)
library(dplyr)
library(tidyverse)
library(scales)
library(stringr)
library(jsonlite)

ref_df <- read_delim('./ref.csv', quote = "'") %>% mutate(
  total_dups = map(duplicates, function(dups) { sum(fromJSON(dups)$cls) }),
  ref_proof_len = ref_proof_axioms + ref_proof_derived
) %>% unnest
stats_df <- read_delim('./formula-stats.csv') %>% select(c(instance, formula_size, variable_count))

full_df <- stats_df |> full_join(ref_df) %>% mutate(
  mus_instance = str_detect(instance, 'mus'),
  instance_class = sub('-.*', '', instance),
  clique = str_detect(instance, 'clique'),
  full_instance_class = ifelse(
    instance_class == 'coloring',
    ifelse(clique, 'coloring-clique', 'coloring'),
    instance_class
  ))
full_df %>% filter(is.na(ref_proof_derived)) %>% count
full_df %>% filter(return_code != 0) %>% count
full_df %>% filter(rat_steps > 0) %>% count

full_df %>% mutate(no_dups = total_dups == 0) %>%
  group_by(full_instance_class) %>%
  select(no_dups) %>% summarize(
    no_dups_ratio = mean(no_dups),
    no_dups_count = sum(no_dups)
  )

p <- ggplot(full_df %>% filter(total_dups > 0 & !(instance_class %in% c('parity', 'php', 'op'))),
       aes(x = total_dups / (ref_proof_len + total_dups),
           fill = full_instance_class)) +
  geom_histogram(color = 'white') +
  scale_x_continuous(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())
p
ggsave('relative-dups.svg', plot = p, width = 4, height = 4)

full_df %>% select(instance, formula_size, variable_count, ref_proof_len) %>%
  write_csv(file = "reference-values.csv")

# ---

ref_df <- read_delim('./ref.competition.csv', quote = "'") %>% mutate(
  total_dups = map(duplicates, function(dups) { sum(fromJSON(dups)$cls) }),
  ref_proof_len = ref_proof_axioms + ref_proof_derived
) %>% unnest
stats_df <- read_delim('./formula-stats.comp.csv') %>% select(c(instance, formula_size, variable_count))

full_df <- stats_df |> left_join(ref_df) %>% mutate(
  mus_instance = str_detect(instance, 'mus'))
full_df %>% filter(is.na(ref_proof_derived)) %>% count
full_df %>% filter(return_code != 0) %>% count
full_df %>% filter(rat_steps > 0) %>% count

full_df %>% mutate(no_dups = total_dups == 0) %>%
  select(no_dups) %>% summarize(
    no_dups_ratio = mean(no_dups),
    no_dups_count = sum(no_dups)
  )

p <- ggplot(full_df %>% filter(total_dups > 0),
            aes(x = total_dups / (ref_proof_len + total_dups), fill = mus_instance)) +
  geom_histogram(color = 'white', binwidth = 5e-3) +
  scale_x_continuous(labels = scales::percent) +
  labs(x = 'Relative number of duplicates',
       y = 'Number of samples',
       fill = 'MUS instance?') +
  theme(legend.position = c(.8, .7), legend.background=element_blank())
p
ggsave('relative-dups-comp.svg', plot = p, width = 4, height = 4)

full_df %>% select(instance, formula_size, variable_count, ref_proof_len) %>%
  write_csv(file = "reference-values.comp.csv")
