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

formula_stats <- read_delim('./reference-values.comp.csv') %>%
  mutate(mus_instance = str_detect(instance, 'mus'), instance = sub('\\.mus', '', sub('\\.orig', '', sub('\\.cnf', '', instance))))

df <- read_delim('./results.comp.csv') %>%
  mutate(solver = sub('_.*', '', run_name),
         instance = sub('\\.orig', '', sub('.*_', '', run_name)))

df_full <- formula_stats %>% left_join(df, by = c('instance'))

ggplot(df_full, aes(x = proof_length, y = ref_proof_len, color = mus_instance)) +
  geom_point() +
  geom_abline(color = 'red', linetype = 'dashed') +
  scale_x_log10(
    breaks = trans_breaks("log10", function(x) 10^x),
    labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(
    breaks = trans_breaks("log10", function(x) 10^x),
    labels = trans_format("log10", math_format(10^.x)))

ggplot(df_full, aes(x = proof_length / ref_proof_len, fill = mus_instance)) +
  geom_histogram(color = 'white') +
  scale_x_log10(
    breaks = trans_breaks("log10", function(x) 10^x),
    labels = trans_format("log10", math_format(10^.x)))

ggplot(df_full, aes(y = is.na(proof_length), x = ref_proof_len, color = mus_instance)) +
  geom_boxplot() +
  scale_x_log10(
    breaks = trans_breaks("log10", function(x) 10^x),
    labels = trans_format("log10", math_format(10^.x)))
