#!/bin/sh
# Rebuilds the tractable experiments of the study and re-checks the certificates.
#
#   sh code/reproduce.sh              default : bounded reproduction, about 25 min on 16 cores (our run: steps 0-7 in 26 min
#                                               before trimming; now bounded well inside the platform's 60 min limit)
#   QUICK=1 sh code/reproduce.sh      checks only, about 10 min
#   FULL=1  sh code/reproduce.sh      everything (adds roughly 5-6 h; see step 11)
#
# Where it writes. Nothing in the shipped archive is modified: the script makes a working copy
# of code/ and of the small result files under results/reproduction/work/ (symlinking the
# shipped certificate directory and .pydeps), runs every step there, writes regenerated
# certificates to results/reproduction/work/certificates/, and finally compares the working
# copy with the shipped files (code/tools/compare_reproduction.py) into
# results/reproduction/summary.json. Its execution log is results/reproduction/experiment-log.jsonl.
# INPLACE=1 runs in the archive itself instead (appends to the shipped record files; not
# recommended), REPRO_WORK=DIR chooses another working directory.
#
# What each mode does (manuscript Appendix C):
#   QUICK   : steps 0-3, 9, 10. Builds the tools, re-runs the graph-invariant, order-independence and
#             lemma checks, replays every stored witness, and re-verifies with drat-trim the shipped
#             fort-cover proofs for n = 11..21 and a fixed sample of the boundary proofs
#             (n = 24, 26..40, 60) if they are present on disk; rebuilds tables and metrics
#             in the working copy; re-runs the Stage 5 robustness checks that need no enumeration.
#             Proofs not present on disk are reported as "skipped", never as verified.
#   default : adds steps 4-8: exhaustive oracle n = 11..22 (rows 11..22 of Table 2), the boundary
#             table for p = 16..20, the certified window for 26 <= n <= 40 regenerated with fresh
#             DRAT proofs (checked, and their CNF digests compared with the shipped records), the
#             fort-cover certificates n = 11..21 (column F of Table 1 for n <= 21; the round-based
#             encoding only for n <= 17 with a 60 s limit), then a re-check of the regenerated
#             certificates.
#   FULL=1  : adds step 11: exhaustive oracle n = 23..27 (rows 23..27 of Table 2, about 70 min),
#             the complete boundary table p = 12..24, the complete certified window 26 <= n <= 154
#             (about 35 min on 12 cores), the fort-cover certificate n = 22 (about 11 min), a re-check of
#             every shipped proof present on disk including the 4.0 GB (n = 23) fort-cover proof (about
#             2 h), a drat-trim check of the stored 7.7 GB n = 25 proof file (status unknown; 1-2 h),
#             proof-logging re-solves of the stored fort-cover CNFs for n = 23 and 25 (about 2-3 h
#             including drat-trim), the round encoding n = 18..22 with the original 600 s limit,
#             the second enumerator E' through n = 40 (about 1 h) and the exhaustive boundary-encoding
#             checks of Section 8(c).
# Any interrupted step leaves the result rows of that step unchanged; a timed-out or killed solver is
# never recorded as UNSAT.
set -e
ROOT=$(cd "$(dirname "$0")/.." && pwd)
cd "$ROOT"
MODE=default; [ -n "$QUICK" ] && MODE=quick; [ "${FULL:-0}" = "1" ] && MODE=full
T0=$(date -u +%FT%TZ)

if [ "${INPLACE:-0}" = "1" ]; then
  WORK="$ROOT"
  export AUTOSCHOLAR_CERTS_DIR="$ROOT/results/reproduction/certificates"
else
  WORK=${REPRO_WORK:-$ROOT/results/reproduction/work}
  rm -rf "$WORK"; mkdir -p "$WORK/code/proofs" "$WORK/results"
  rsync -a --exclude proofs/certificates --exclude brute_force --exclude robustness/ff_brute --exclude robustness/beta_brute \
        --exclude tools/drat-trim/drat-trim "$ROOT/code/" "$WORK/code/"
  ln -s "$ROOT/code/proofs/certificates" "$WORK/code/proofs/certificates"
  [ -d "$ROOT/.pydeps" ] && ln -s "$ROOT/.pydeps" "$WORK/.pydeps"
  cp "$ROOT"/results/*.json "$ROOT"/results/*.jsonl "$ROOT"/results/*.csv "$ROOT"/results/*.md "$WORK/results/" 2>/dev/null || true
  for d in tables robustness; do [ -d "$ROOT/results/$d" ] && cp -R "$ROOT/results/$d" "$WORK/results/$d"; done
  export AUTOSCHOLAR_CERTS_DIR="$WORK/certificates"
fi
mkdir -p "$ROOT/results/reproduction" "$WORK/results/logs" "$AUTOSCHOLAR_CERTS_DIR"
export AUTOSCHOLAR_EXPLOG="$WORK/results/experiment-log.jsonl"
[ "$WORK" = "$ROOT" ] || : > "$AUTOSCHOLAR_EXPLOG"
cd "$WORK"
export PYTHONPATH=.pydeps:code
run() { name=$1; shift; echo "== $name: $*"; python3 code/tools/logrun.py "$name" --log "results/logs/$name.log" -- "$@"; }

echo "[0] dependencies and tools (mode: $MODE, work: $WORK)"
[ -d .pydeps/pysat ] || python3 -m pip install --no-index --target "$ROOT/.pydeps" "$ROOT"/code/wheels/*.whl
run build_drat_trim gcc -O2 -o code/tools/drat-trim/drat-trim code/tools/drat-trim/drat-trim.c
run build_brute_force gcc -O2 -o code/brute_force code/brute_force.c
run build_ff_brute gcc -O2 -o code/robustness/ff_brute code/robustness/ff_brute.c -lpthread
run build_beta_brute gcc -O2 -o code/robustness/beta_brute code/robustness/beta_brute.c -lpthread

echo "[1] graph invariants (T1) and order independence (T2)"
run T1_graph_invariants python3 code/graph_constructor.py 5 48
run T2_order_independence python3 code/closure_oracle.py

echo "[2] lemma checks (CS6, T8, sympy)"
run lemma_checks python3 code/verify_lemmas.py

echo "[3] independent certificate checks: witness replay; drat-trim on shipped proofs present on disk"
run verify_upper_bounds python3 code/verify_upper_bounds.py 60
if [ "$MODE" = "full" ]; then
  run verify_lower_bounds_all_shipped python3 code/verify_lower_bounds.py 8
else
  VERIFY_BOUNDARY_N="24,26-40,60" VERIFY_FORTCOVER_N="11-21" VERIFY_MAX_PROOF_BYTES=1500000000 \
    run verify_lower_bounds_sample python3 code/verify_lower_bounds.py 8
fi

if [ "$MODE" != "quick" ]; then
  echo "[4] exhaustive oracle n = 11..22 (C program, 16 threads, ~2 min)"
  BF_TIME_LIMIT=3600 run brute_force_11_22 python3 code/brute_force.py 11 12 13 14 15 16 17 18 19 20 21 22
  echo "[5] boundary table p = 16..20, n = 13..30 (~2 min)"
  run boundary_table_p16_20 python3 code/run_boundary_table.py 16 20 13 30 12
  echo "[6] certified boundary window p = 18, n = 26..40, fresh DRAT proofs (~2 min)"
  run boundary_window_26_40 python3 code/run_boundary_window.py 18 26 40 12
  echo "[7] fort-cover certificates n = 11..21 (round encoding only n <= 17, 60 s limit; ~8 min; n = 22 is in FULL mode)"
  FORT_LIMIT=300 ROUND_LIMIT=60 run exact_fortcover_11_17 python3 code/run_exact.py 11 12 13 14 15 16 17
  FORT_LIMIT=600 SKIP_ROUND=1 run exact_fortcover_18_21 python3 code/run_exact.py 18 19 20 21
  echo "[8] re-check of the regenerated certificates with the independent checker"
  run verify_upper_bounds_again python3 code/verify_upper_bounds.py 60
  VERIFY_BOUNDARY_N="26-40" VERIFY_FORTCOVER_N="11-21" VERIFY_MAX_PROOF_BYTES=1500000000 \
    VERIFY_OUT=results/lower_bound_verification_regenerated.json run verify_lower_bounds_regenerated python3 code/verify_lower_bounds.py 8
fi

echo "[9] tables and metrics (working copy)"
run build_tables python3 code/build_tables.py

echo "[10] Stage 5 robustness checks that need no enumeration (see code/robustness/README.md)"
run robustness_check_counts python3 code/robustness/check_counts.py
run robustness_witness_replay python3 code/robustness/check_witness_replay.py
run robustness_deletion_lemma python3 code/robustness/check_deletion_lemma.py
run robustness_drat_negative_controls python3 code/robustness/check_drat_negative_controls.py
run robustness_margin python3 code/robustness/check_margin.py
run robustness_local_search python3 code/robustness/attack_local_search.py

if [ "$MODE" = "full" ]; then
  echo "[11] FULL: exhaustive oracle n = 23..27, complete boundary table and window, big proof re-solves, E' enumerations"
  BF_TIME_LIMIT=3600 run brute_force_23_27 python3 code/brute_force.py 23 24 25 26 27
  run boundary_table_full python3 code/run_boundary_table.py 12 24 13 30 12
  run boundary_window_41_154 python3 code/run_boundary_window.py 18 41 154 12
  FORT_LIMIT=600 SKIP_ROUND=1 run exact_fortcover_22 python3 code/run_exact.py 22
  FORT_LIMIT=600 ROUND_LIMIT=600 run exact_round_18_22 python3 code/run_exact.py 18 19 20 21 22
  run regen_fortcover_proof_23 python3 code/regen_fortcover_proof.py 23 11
  run regen_fortcover_proof_25 python3 code/regen_fortcover_proof.py 25 11
  # drat-trim on the stored n = 25 proof file (exit 1 and no record if it does not verify)
  run check_fortcover_proof_25 python3 code/check_fortcover_proof.py 25 11 18000 || true
  VERIFY_OUT=results/lower_bound_verification_regenerated.json run verify_lower_bounds_regenerated_full python3 code/verify_lower_bounds.py 8
  run build_tables_full python3 code/build_tables.py
  run robustness_beta_brute sh code/robustness/run_beta_brute.sh
  run robustness_boundary_encoding python3 code/robustness/check_boundary_encoding.py
  run robustness_ff_brute sh code/robustness/run_ff_brute.sh
  for n in 31 32 33 34 35 36 37 38 39 40; do code/robustness/ff_brute $n 5 11 16; done >> results/robustness/ff_brute_stdout_31_40.txt
fi
run robustness_collect python3 code/robustness/collect_robustness_metrics.py

echo "[12] comparison with the shipped artifacts"
cd "$ROOT"
set +e
python3 code/tools/compare_reproduction.py "$WORK" "$ROOT" "$MODE" "$ROOT/results/reproduction/summary.json"
CMP=$?
set -e
[ "$WORK" = "$ROOT" ] || cp "$AUTOSCHOLAR_EXPLOG" "$ROOT/results/reproduction/experiment-log.jsonl"
# remove compiled binaries (rebuilt by step 0) and regenerated DRAT proofs (their digests are in the records)
rm -f "$WORK/code/brute_force" "$WORK/code/robustness/ff_brute" "$WORK/code/robustness/beta_brute" "$WORK/code/tools/drat-trim/drat-trim"
find "$AUTOSCHOLAR_CERTS_DIR" -name '*.drat' -delete 2>/dev/null || true
echo "reproduce.sh finished: mode=$MODE started=$T0 ended=$(date -u +%FT%TZ) comparison_exit=$CMP (results/reproduction/summary.json)"
exit $CMP