55 lines
1.6 KiB
Python
55 lines
1.6 KiB
Python
#!/usr/bin/env python3
|
|
# bench-lean4-0001.py
|
|
# lean4-0001: guardCycle List.contains vs HashSet
|
|
#
|
|
# Models the Lean4 Environment.guardCycle defect where ancestor cycle
|
|
# detection uses List.contains (O(N) per call) inside an O(N) traversal,
|
|
# giving O(N^2) total. Fixed version uses a HashSet/set for O(1) contains.
|
|
|
|
import sys
|
|
import time
|
|
|
|
def bench_defective(n):
|
|
"""Model guardCycle with list.contains, O(N^2) total."""
|
|
t0 = time.perf_counter()
|
|
parents = []
|
|
for i in range(n):
|
|
_ = i in parents # O(len(parents)) linear scan
|
|
parents.insert(0, i) # prepend like withCallStack
|
|
return time.perf_counter() - t0
|
|
|
|
def bench_fixed(n):
|
|
"""Model guardCycle with set.contains, O(N) total."""
|
|
t0 = time.perf_counter()
|
|
parents_set = set()
|
|
parents_list = []
|
|
for i in range(n):
|
|
_ = i in parents_set # O(1)
|
|
parents_set.add(i)
|
|
parents_list.insert(0, i)
|
|
return time.perf_counter() - t0
|
|
|
|
TRIALS = 3
|
|
SIZES = [100, 500, 1000, 2000]
|
|
|
|
def run():
|
|
lines = []
|
|
header = "=== lean4-0001: guardCycle List vs HashSet ==="
|
|
print(header)
|
|
lines.append(header)
|
|
|
|
for n in SIZES:
|
|
def_times = [bench_defective(n) for _ in range(TRIALS)]
|
|
fix_times = [bench_fixed(n) for _ in range(TRIALS)]
|
|
d_ms = min(def_times) * 1000
|
|
f_ms = min(fix_times) * 1000
|
|
speedup = d_ms / f_ms if f_ms > 0 else float('inf')
|
|
line = f"N={n:<5}: defective={d_ms:.3f}ms fixed={f_ms:.3f}ms speedup={speedup:.1f}x"
|
|
print(line)
|
|
lines.append(line)
|
|
sys.stdout.flush()
|
|
|
|
return lines
|
|
|
|
if __name__ == "__main__":
|
|
run()
|