#!/bin/bash
set -Eeuo pipefail
shopt -s extglob
benchmark_dir=$1
mkdir -p $benchmark_dir
output_file=$2
wget -qO- https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/New/Competition-02/sat-2002-beta.tgz | tar xz -C $benchmark_dir
echo "Extracted SAT Competition 2002 benchmark into $benchmark_dir"
find $benchmark_dir/sat-2002-beta/submitted -mindepth 1 -type f -name "*.cnf" -exec mv -t $benchmark_dir -f '{}' +
rm -r $benchmark_dir/sat-2002-beta
echo "Unpacked $(ls $benchmark_dir -1 | wc -l) samples in $benchmark_dir"
counter=0
total=$(ls $benchmark_dir -1 | wc -l)
for instance in $benchmark_dir/*.cnf
do
  solver_status=0
  cadical -q --unsat -t 15 $instance  > /dev/null || solver_status=$?
  counter=$((counter+1))
  if [ $solver_status -ne 20 ]
  then
    rm $instance
  else
   mv $instance "$benchmark_dir/$(basename $instance .cnf).orig.cnf"
  fi
  echo "$counter / $total processed instances"
done;
echo "Retained $(ls $benchmark_dir -1 | wc -l) samples in $benchmark_dir after removing SAT formulas"
for instance_path in $benchmark_dir/*.orig.cnf
do
  mus_instance_path="$benchmark_dir/$(basename $instance_path .orig.cnf).mus"
  muser2 -T 60 -wf $mus_instance_path $instance_path > /dev/null || true 
  orig_formula_size=$(grep -E '\s*p\s+cnf' $instance_path | awk '{ print $4 }')
  mus_formula_size=$(grep -E '\s*p\s+cnf' "$mus_instance_path.cnf" | awk '{ print $4 }')
  if [ $orig_formula_size -eq $mus_formula_size ]
  then
    rm $instance_path
    echo "Instance $instance_path is already a MUS"
  else
    echo "Extracted a MUS of size $mus_formula_size from the formula $instance_path of size $orig_formula_size"
  fi
done
echo "Added MUS versions of the formulas in $benchmark_dir"
echo "Total collection size is $(ls $benchmark_dir -1 | wc -l):"
echo "- $(ls $benchmark_dir -1 | grep -ce orig) non-MUS instances"
echo "- $(ls $benchmark_dir -1 | grep -ce mus) MUS instances"
echo "instance,formula_size,variable_count" > $output_file
for instance in $benchmark_dir/*.cnf
do
  formula_size=$(grep -E '\s*p\s+cnf' $instance | awk '{ print $4 }')
  variable_count=$(grep -E '\s*p\s+cnf' $instance | awk '{ print $3 }')
  echo "$(basename $instance),$formula_size,$variable_count" >> $output_file;
done
echo "Stored statistics for $(($(ls $benchmark_dir -1 | wc -l) - 1)) instances in $output_file"
