#!/bin/bash
set -Eeuo pipefail
shopt -s extglob
full=true
POSITIONAL_ARGS=()
while [[ $# -gt 0 ]]; do
  case $1 in
    -s|--small)
      full=false
      shift
      ;;
    -*|--*)
      echo "Unknown option $1"
      exit 1
      ;;
    *)
      POSITIONAL_ARGS+=("$1")
      shift
      ;;
  esac
done
set -- "${POSITIONAL_ARGS[@]}"
benchmark_dir=$1
mkdir -p $benchmark_dir
output_file=$2
if $full
then
  for param in $(seq 1 6)
  do
    instance_path="$benchmark_dir/php-$param.orig.cnf"
    cnfgen php $(($param+1)) $param > $instance_path
    instance_path="$benchmark_dir/parity-$param.orig.cnf"
    cnfgen parity $((2*$param+1)) > $instance_path
    instance_path="$benchmark_dir/op-$param.orig.cnf"
    cnfgen op $(($param+1)) > $instance_path
  done
  echo "Generated parametric instances"
fi
n_seeds_3cnf=1
if $full
then
  n_seeds_3cnf=10
fi
for vars in $(seq 5 15)
do
  for clauses in $(seq $((3*vars)) $((6*vars)))
  do
    for seed in $(seq 1 $n_seeds_3cnf)
    do
      instance_path="$benchmark_dir/3cnf-$vars-$clauses-$seed.orig.cnf"
      cnfgen randkcnf 3 $vars $clauses > $instance_path
    done
  done
  echo "Generated $vars-variable 3-CNF instances"
done
echo "Generated $(ls $benchmark_dir -1 | grep -ce 3cnf) 3-CNF instances"
n_seeds_card=10
if $full
then
  n_seeds_card=100
fi
for vars in $(seq 5 10)
do
  for seed in $(seq 1 $n_seeds_card)
  do
    instance_path="$benchmark_dir/subsetcard-$vars-$seed.orig.cnf"
    cnfgen subsetcard $vars > $instance_path
  done
  echo "Generated $vars-subset cardinality instances"
done
echo "Generated $(ls $benchmark_dir -1 | grep -ce subsetcard) subset cardinality instances"
n_seeds_gc=3
if $full
then
  n_seeds_gc=10
fi
for colors in $(seq 3 6)
do
  deg=$((2*$colors-2))
  nodes_min=$(($deg+2))
  nodes_max=$((2*$nodes_min))
  for nodes in $(seq $nodes_min 2 $nodes_max)
  do
    for seed in $(seq 1 $n_seeds_gc)
    do
      instance_path="$benchmark_dir/coloring-$nodes-$deg-$colors-$seed.orig.cnf"
      cnfgen kcolor $colors gnd $nodes $deg > $instance_path
      instance_path="$benchmark_dir/coloring-$nodes-$deg-$colors-$seed-clique.orig.cnf"
      cnfgen kcolor $colors gnd $nodes $deg plantclique $(($colors+1)) > $instance_path
    done
  done
done
echo "Generated $(ls $benchmark_dir -1 | grep -ce coloring) graph coloring instances"
for instance in $benchmark_dir/*.cnf
do
  solver_status=0
  cadical -q --unsat $instance  > /dev/null || solver_status=$?
  if [ $solver_status -ne 20 ]
  then
    rm $instance
  fi
done;
echo "Retained $(ls $benchmark_dir -1 | wc -l) samples in $benchmark_dir after removing SAT formulas:"
echo "- $(ls $benchmark_dir -1 | grep -ce 3cnf) 3-CNF instances"
echo "- $(ls $benchmark_dir -1 | grep -ce subsetcard) subset cardinality instances"
echo "- $(ls $benchmark_dir -1 | grep -ce coloring) graph coloring instances"
for instance_path in $benchmark_dir/*.orig.cnf
do
  mus_instance_path="$benchmark_dir/$(basename $instance_path .orig.cnf).mus"
  muser2 -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
  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"
