#!/bin/sh
solver=lingeling
unsat=/tmp/checkmus$$-unsat.cnf
sat=/tmp/checkmus$$-sat.cnf
cleanup () {
  rm -f $sat $unsat
}
trap "cleanup" 2 15
cat $* > $unsat
die () {
  echo "*** checkmus: $*" 1>&2
  cleanup
  exit 1
}
nvars=`awk '/^p cnf/{print $3}' $unsat`
nclauses=`awk '/^p cnf/{print $4}' $unsat`
msg () {
  echo "[checkmus] $*"
}
msg "p cnf $nvars $nclauses"
$solver -n $unsat >/dev/null 2>/dev/null
[ $? = 20 ] || die "input file not unsatisfiable"
msg "'$solver' says input file is unsatisfiable"
i=0
while [ $i -lt $nclauses ]
do
  next=`expr $i + 1`
  echo -n '\r[checkmus] dropping '"$next/$nclauses"
  rm -f $sat
  awk '/^c/{print; next}
  /^p cnf/{print $1, $2, $3, $4 - 1; next}
  {if(nclauses++!='$i')print}' $unsat > $sat
  $solver -n $sat >/dev/null 2>/dev/null
  if [ ! $? = 10 ]
  then
    echo
    die "dropping clause $next generates unsatisfiable instance"
  fi
  i=$next
done
echo
msg "done"
cleanup