#!/bin/bash
set -Eeuo pipefail
shopt -s extglob
instance_file=$1
lrat_file=$(mktemp /tmp/proof.XXXXXXXXXX.lrat)
# 1. Score the original LRAT proof, without any trimming
cadical --no-binary -q --unsat --lrat --seed=0 $instance_file $lrat_file > /dev/null || true
RUST_LOG=off $PROOFMIN_BUILD_DIR/lrat-score -d $instance_file $lrat_file
# 3. Run LRAT-trim on the original proof
trim_file="/tmp/$(basename "$lrat_file" .lrat).trim.lrat"
if /home/ksidorov/lrat-trim/lrat-trim -a $lrat_file $trim_file > /dev/null 2> /dev/null; then
  # 4. Score the trimmed proof
  RUST_LOG=off $PROOFMIN_BUILD_DIR/lrat-score -d $instance_file $trim_file || echo "scoring,$instance_file" > /dev/stderr
else
  echo "lrat-trim,$instance_file" > /dev/stderr
fi
