#!/usr/bin/env bash
# VNN-COMP 2023 acasxu benchmark (186 instances, 45 networks, properties 1-10) with NeuralSAT's main.py, as
# vnncomp_scripts/run_instance.sh calls it: per-instance timeout from instances.csv, default settings, one GPU.
ROW=/var/tmp/kv-repro/041-dynaroars-neuralsat
B=$ROW/data/acasxu
export HOME=$ROW/data/home
OUT=$ROW/data/results-$(date +%s)
mkdir -p $OUT
(cd $B && sha256sum instances.csv onnx/*.onnx vnnlib/*.vnnlib)
echo "KVERITAS_PHASE name=verify_acasxu"
i=0
while IFS=, read -r net spec tmo; do
  i=$((i+1))
  res=$OUT/$i.txt
  start=$(date +%s.%N)
  (cd src && python main.py --net $B/$net --spec $B/$spec --timeout $tmo --verbosity 0 --result_file $res --export_cex > $OUT/$i.log 2>&1)
  wall=$(echo "$(date +%s.%N) - $start" | bc)
  verdict=$(head -1 $res 2>/dev/null | cut -d, -f1)
  echo "$i $net $spec ${verdict:-error} wall=$wall"
  echo "$i,$net,$spec,${verdict:-error},$wall" >> $OUT/summary.csv
  echo "KVERITAS_METRIC name=instance_wall_s value=$wall step=$i"
done < <(tr -d '\r' < $B/instances.csv)
python - $OUT/summary.csv <<'PY'
import collections, sys
rows = [l.strip().split(",") for l in open(sys.argv[1])]
c = collections.Counter(r[3] for r in rows)
solved = c["unsat"] + c["sat"]
for k in ("unsat", "sat", "timeout", "unknown", "error"):
    print(f"KVERITAS_CLAIM metric=acasxu_{k} value={c[k]}")
print(f"KVERITAS_CLAIM metric=acasxu_solved value={solved}")
print(f"KVERITAS_CLAIM metric=acasxu_instances value={len(rows)}")
print(f"KVERITAS_CLAIM metric=acasxu_solved_mean_wall_s value={sum(float(r[4]) for r in rows if r[3] in ('sat','unsat')) / max(solved,1):.2f}")
print("verdicts:", dict(c))
PY
