#!/bin/bash
set -Eeuo pipefail
shopt -s extglob
instance_file=$2
>&2 echo "$1 $2"
if [[ "$1" == "--raw" ]]; then
  echo -n "none;"
  lrat_file=$(mktemp /tmp/proof.XXXXXXXXXX.lrat)
  cadical --no-binary -q --unsat --lrat $instance_file $lrat_file > /dev/null || true
  RUST_LOG=off $PROOFMIN_BUILD_DIR/lrat-score -d $instance_file $lrat_file
elif [[ "$1" == "--drat-trim" ]]; then
  echo -n "drat-trim;"
  drat_file=$(mktemp /tmp/proof.XXXXXXXXXX.drat)
  lrat_file=$(mktemp /tmp/proof.XXXXXXXXXX.lrat)
  cadical --no-binary -q --unsat $instance_file $drat_file > /dev/null || true
  drat-trim $instance_file $drat_file -U -L $lrat_file > /dev/null
  RUST_LOG=off $PROOFMIN_BUILD_DIR/lrat-score -d $instance_file $lrat_file
else
  echo -n "adhoc;"
  lrat_file=$(mktemp /tmp/proof.XXXXXXXXXX.lrat)
  cadical --no-binary -q --unsat --lrat $instance_file $lrat_file > /dev/null || true
  RUST_LOG=off $PROOFMIN_BUILD_DIR/lrat-score -d -t $instance_file $lrat_file
fi
