|
| 1 | +#!/usr/bin/env python3 |
| 2 | +"""Run all TC/SG benchmarks on Logica and Nemo, collect times into CSV + ASCII table.""" |
| 3 | + |
| 4 | +import csv |
| 5 | +import os |
| 6 | +import re |
| 7 | +import resource |
| 8 | +import subprocess |
| 9 | +import sys |
| 10 | +import time |
| 11 | + |
| 12 | + |
| 13 | +BENCHMARKS = [ |
| 14 | + # (problem, dataset, csv_file) |
| 15 | + ("TC", "g1k", "g1k.csv"), |
| 16 | + ("TC", "g2k", "g2k.csv"), |
| 17 | + ("TC", "g3k", "g3k.csv"), |
| 18 | + ("TC", "g4k", "g4k.csv"), |
| 19 | + ("TC", "g5k", "g5k.csv"), |
| 20 | + ("SG", "tree7", "tree7.csv"), |
| 21 | + ("SG", "tree8", "tree8.csv"), |
| 22 | + ("SG", "tree9", "tree9.csv"), |
| 23 | + ("SG", "tree10", "tree10.csv"), |
| 24 | + ("SG", "tree11", "tree11.csv"), |
| 25 | + ("SG", "tree12", "tree12.csv"), |
| 26 | +] |
| 27 | + |
| 28 | + |
| 29 | +LOGICA_TEMPLATES = { |
| 30 | + "TC": '''@Ground(G); |
| 31 | +G(a, b) :- `("{csv}")`(a, b); |
| 32 | +
|
| 33 | +@Recursive(TC, ∞, stop: Stop); |
| 34 | +TC(a, b) distinct :- G(a, b); |
| 35 | +TC(a, c) distinct :- TC(a, b), G(b, c); |
| 36 | +
|
| 37 | +OldN() += 1 :- TC(); |
| 38 | +Stop() :- OldN() == Sum{{1 :- TC()}}; |
| 39 | +
|
| 40 | +N() += 1 :- TC(a, b); |
| 41 | +''', |
| 42 | + "SG": '''G(a, b) :- `("{csv}")`(a, b); |
| 43 | +
|
| 44 | +@Recursive(SG, -1, stop: Done); |
| 45 | +SG(x, y) distinct :- G(a, x), G(a, y); |
| 46 | +SG(x, y) distinct :- SG(a, b), G(a, x), G(b, y); |
| 47 | +PrevSG(x, y) :- SG(x, y); |
| 48 | +Done() :- Sum{{ 1 :- SG(x, y) }} == Sum{{ 1 :- PrevSG(x, y) }}; |
| 49 | +
|
| 50 | +N() += 1 :- SG(x, y); |
| 51 | +''', |
| 52 | +} |
| 53 | + |
| 54 | +NEMO_TEMPLATES = { |
| 55 | + "TC": '''@import edge :- csv{{resource="{csv}", ignore_headers=true}}. |
| 56 | +
|
| 57 | +TC(?A, ?B) :- edge(?A, ?B). |
| 58 | +TC(?A, ?C) :- TC(?A, ?B), edge(?B, ?C). |
| 59 | +
|
| 60 | +N(#count(?A, ?B)) :- TC(?A, ?B). |
| 61 | +
|
| 62 | +@export N :- csv{{resource="n.csv"}}. |
| 63 | +''', |
| 64 | + "SG": '''@import tree :- csv{{resource="{csv}", ignore_headers=true, format=(string,string)}}. |
| 65 | +
|
| 66 | +SG(?X, ?Y) :- tree(?A, ?X), tree(?A, ?Y). |
| 67 | +SG(?X, ?Y) :- SG(?A, ?B), tree(?A, ?X), tree(?B, ?Y). |
| 68 | +
|
| 69 | +N(#count(?X, ?Y)) :- SG(?X, ?Y). |
| 70 | +
|
| 71 | +@export N :- csv{{resource="n.csv"}}. |
| 72 | +''', |
| 73 | +} |
| 74 | + |
| 75 | + |
| 76 | +def generate_programs(problem, dataset, csv_file): |
| 77 | + """Write <problem>_<dataset>.l and .nemo files from templates.""" |
| 78 | + base = f"{problem.lower()}_{dataset}" |
| 79 | + l_file = f"{base}.l" |
| 80 | + nemo_file = f"{base}.nemo" |
| 81 | + with open(l_file, "w") as f: |
| 82 | + f.write(LOGICA_TEMPLATES[problem].format(csv=csv_file)) |
| 83 | + with open(nemo_file, "w") as f: |
| 84 | + f.write(NEMO_TEMPLATES[problem].format(csv=csv_file)) |
| 85 | + return l_file, nemo_file |
| 86 | + |
| 87 | + |
| 88 | +def run_timed(cmd): |
| 89 | + """Run a command, return (wall, user, sys, stdout, stderr).""" |
| 90 | + r0 = resource.getrusage(resource.RUSAGE_CHILDREN) |
| 91 | + t0 = time.time() |
| 92 | + proc = subprocess.run(cmd, capture_output=True, text=True) |
| 93 | + wall = time.time() - t0 |
| 94 | + r1 = resource.getrusage(resource.RUSAGE_CHILDREN) |
| 95 | + user = r1.ru_utime - r0.ru_utime |
| 96 | + sys_t = r1.ru_stime - r0.ru_stime |
| 97 | + return wall, user, sys_t, proc.stdout, proc.stderr |
| 98 | + |
| 99 | + |
| 100 | +def parse_logica_n(stdout): |
| 101 | + """Extract the N value from Logica's artistic_table output.""" |
| 102 | + # Look for a number inside a table row like "| 12345 |" |
| 103 | + for line in stdout.splitlines(): |
| 104 | + m = re.match(r"\|\s*(\d+)\s*\|", line) |
| 105 | + if m: |
| 106 | + return int(m.group(1)) |
| 107 | + return None |
| 108 | + |
| 109 | + |
| 110 | +def parse_nemo_n(results_path="results/n.csv"): |
| 111 | + """Nemo writes N to results/n.csv (one number per file).""" |
| 112 | + try: |
| 113 | + with open(results_path) as f: |
| 114 | + line = f.readline().strip().strip('"') |
| 115 | + return int(line) |
| 116 | + except (FileNotFoundError, ValueError): |
| 117 | + return None |
| 118 | + |
| 119 | + |
| 120 | +def run_logica(l_file): |
| 121 | + cmd = ["python3", "logica/logica.py", l_file, "run_in_terminal", "N"] |
| 122 | + wall, user, sys_t, out, err = run_timed(cmd) |
| 123 | + n = parse_logica_n(out) |
| 124 | + return wall, user + sys_t, n |
| 125 | + |
| 126 | + |
| 127 | +def run_nemo(nemo_file): |
| 128 | + cmd = ["nemo", nemo_file, "--overwrite-results"] |
| 129 | + wall, user, sys_t, out, err = run_timed(cmd) |
| 130 | + n = parse_nemo_n() |
| 131 | + return wall, user + sys_t, n |
| 132 | + |
| 133 | + |
| 134 | +def ascii_table(rows, header): |
| 135 | + """Render rows as +---+---+ style table.""" |
| 136 | + all_rows = [header] + [[str(c) for c in r] for r in rows] |
| 137 | + widths = [max(len(r[i]) for r in all_rows) for i in range(len(header))] |
| 138 | + sep = "+" + "+".join("-" * (w + 2) for w in widths) + "+" |
| 139 | + def fmt(r): |
| 140 | + return "| " + " | ".join(c.ljust(w) for c, w in zip(r, widths)) + " |" |
| 141 | + lines = [sep, fmt(header), sep] |
| 142 | + for r in all_rows[1:]: |
| 143 | + lines.append(fmt(r)) |
| 144 | + lines.append(sep) |
| 145 | + return "\n".join(lines) |
| 146 | + |
| 147 | + |
| 148 | +def main(): |
| 149 | + os.chdir(os.path.dirname(os.path.abspath(__file__))) |
| 150 | + os.makedirs("results", exist_ok=True) |
| 151 | + |
| 152 | + rows = [] |
| 153 | + for problem, dataset, csv_file in BENCHMARKS: |
| 154 | + print(f"=== {problem} {dataset} ===", flush=True) |
| 155 | + |
| 156 | + l_file, nemo_file = generate_programs(problem, dataset, csv_file) |
| 157 | + print(f" Generated: {l_file}, {nemo_file}", flush=True) |
| 158 | + |
| 159 | + print(f" Logica: {l_file}", flush=True) |
| 160 | + l_wall, l_cpu, l_n = run_logica(l_file) |
| 161 | + print(f" wall={l_wall:.2f}s cpu={l_cpu:.2f}s N={l_n}", flush=True) |
| 162 | + |
| 163 | + print(f" Nemo: {nemo_file}", flush=True) |
| 164 | + n_wall, n_cpu, n_n = run_nemo(nemo_file) |
| 165 | + print(f" wall={n_wall:.2f}s cpu={n_cpu:.2f}s N={n_n}", flush=True) |
| 166 | + |
| 167 | + rows.append([ |
| 168 | + problem, dataset, |
| 169 | + f"{l_wall:.2f}", f"{l_cpu:.2f}", |
| 170 | + f"{n_wall:.2f}", f"{n_cpu:.2f}", |
| 171 | + l_n if l_n is not None else "?", |
| 172 | + n_n if n_n is not None else "?", |
| 173 | + ]) |
| 174 | + |
| 175 | + header = ["Problem", "Dataset", |
| 176 | + "Logica wall", "Logica CPU", |
| 177 | + "Nemo wall", "Nemo CPU", |
| 178 | + "Logica N", "Nemo N"] |
| 179 | + |
| 180 | + with open("benchmark_results.csv", "w", newline="") as f: |
| 181 | + w = csv.writer(f) |
| 182 | + w.writerow(header) |
| 183 | + w.writerows(rows) |
| 184 | + |
| 185 | + table = ascii_table(rows, header) |
| 186 | + with open("benchmark_results.txt", "w") as f: |
| 187 | + f.write(table + "\n") |
| 188 | + |
| 189 | + print() |
| 190 | + print(table) |
| 191 | + print() |
| 192 | + print("Wrote benchmark_results.csv and benchmark_results.txt") |
| 193 | + |
| 194 | + |
| 195 | +if __name__ == "__main__": |
| 196 | + main() |
0 commit comments