#!/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
# 2. Convert LRAT to DRAT by removing the first token and truncating on `0`
drat_file="/tmp/$(basename "$lrat_file" .lrat).drat"
awk '$2 == "d" { next } {
  out=""
  for (i = 2; i <= NF; i++) {
    out = out $i (i < NF ? OFS : "")
    if ($i == 0) break
  }
  print out
}' "$lrat_file" > "$drat_file"
# 3. Run DRAT-trim on the DRAT version
trim_file="/tmp/$(basename "$drat_file" .drat).trim.lrat"
if drat-trim $instance_file $drat_file -OU -L $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 "drat-trim,$instance_file" > /dev/stderr
fi
