Merge branch 'b2-aspic-completeness'

Author: ctoth

bench/asp_vs_sat.py

@@ -30,7 +30,15 @@ def main() -> None:
     with out_path.open("w", newline="", encoding="utf-8") as handle:
         writer = csv.DictWriter(
             handle,
-            fieldnames=["family", "size", "semantics", "backend", "status", "extensions", "seconds"],
+            fieldnames=[
+                "family",
+                "size",
+                "semantics",
+                "backend",
+                "status",
+                "extensions",
+                "seconds",
+            ],
         )
         writer.writeheader()
         writer.writerows(rows)
@@ -48,7 +56,17 @@ def _run_aba(size: int, timeout: float) -> list[dict[str, str]]:
                 semantics=semantics,
                 timeout_seconds=timeout,
             )
-            rows.append(_row("aba", size, semantics, backend, result.status, len(result.extensions), start))
+            rows.append(
+                _row(
+                    "aba",
+                    size,
+                    semantics,
+                    backend,
+                    result.status,
+                    len(result.extensions),
+                    start,
+                )
+            )
     return rows
 
 
@@ -66,7 +84,17 @@ def _run_aspic(size: int, timeout: float) -> list[dict[str, str]]:
                 semantics=semantics,
                 timeout_seconds=timeout,
             )
-            rows.append(_row("aspic", size, semantics, backend, result.status, len(result.extensions), start))
+            rows.append(
+                _row(
+                    "aspic",
+                    size,
+                    semantics,
+                    backend,
+                    result.status,
+                    len(result.extensions),
+                    start,
+                )
+            )
     return rows
 
 

bench/instance_gen.py

@@ -19,7 +19,9 @@ def aba_chain(size: int, *, body_size: int = 1) -> ABAFramework:
     contraries = tuple(Literal(GroundAtom(f"c{index}")) for index in range(size))
     rules: set[Rule] = set()
     for index, contrary in enumerate(contraries):
-        body = tuple(assumptions[(index + offset + 1) % size] for offset in range(body_size))
+        body = tuple(
+            assumptions[(index + offset + 1) % size] for offset in range(body_size)
+        )
         rules.add(Rule(body, contrary, "strict", f"r_{index}"))
     return ABAFramework(
         language=frozenset((*assumptions, *contraries)),
@@ -37,7 +39,11 @@ def aspic_chain(size: int, *, defeasible_ratio: float = 1.0):
     defeasible_cutoff = int(max(0, min(1, defeasible_ratio)) * max(0, size - 1))
     for index in range(size - 1):
         if index < defeasible_cutoff:
-            defeasible_rules.add(Rule((literals[index],), literals[index + 1], "defeasible", f"d_{index}"))
+            defeasible_rules.add(
+                Rule(
+                    (literals[index],), literals[index + 1], "defeasible", f"d_{index}"
+                )
+            )
         else:
             strict_rules.add(Rule((literals[index],), literals[index + 1], "strict"))
     system = ArgumentationSystem(

experiments/iccma-census/aggregate_census.py

@@ -57,21 +57,31 @@ def main() -> int:
         print(f"MISSING run outputs for: {missing}")
     print(f"\n{'family':12} {'subtrack':8} {'solved':>6} {'timeout':>7} {'other':>6}")
     tot = defaultdict(int)
-    for (fam, st) in sorted(cells):
+    for fam, st in sorted(cells):
         c = cells[(fam, st)]
         solved = c.get("solved", 0)
         timeout = c.get("timeout", 0)
         other = sum(v for k, v in c.items() if k not in ("solved", "timeout"))
-        othertxt = "" if not other else " ".join(f"{k}={v}" for k, v in c.items() if k not in ("solved", "timeout"))
+        othertxt = (
+            ""
+            if not other
+            else " ".join(
+                f"{k}={v}" for k, v in c.items() if k not in ("solved", "timeout")
+            )
+        )
         print(f"{fam:12} {st:8} {solved:>6} {timeout:>7} {other:>6}  {othertxt}")
         tot["solved"] += solved
         tot["timeout"] += timeout
         tot["other"] += other
     total_rows = tot["solved"] + tot["timeout"] + tot["other"]
-    print(f"\nTOTAL rows={total_rows} solved={tot['solved']} timeout={tot['timeout']} other={tot['other']}")
+    print(
+        f"\nTOTAL rows={total_rows} solved={tot['solved']} timeout={tot['timeout']} other={tot['other']}"
+    )
     if total_rows:
         frac = tot["solved"] / total_rows
-        print(f"budget-artifact fraction (solved@600 / sampled timeouts) = {tot['solved']}/{total_rows} = {frac:.3f}")
+        print(
+            f"budget-artifact fraction (solved@600 / sampled timeouts) = {tot['solved']}/{total_rows} = {frac:.3f}"
+        )
     return 0
 
 

experiments/iccma-census/select_sample.py

@@ -107,7 +107,9 @@ def select(csv_path: Path) -> dict:
             }
         )
         for instance in picked:
-            entries.append({"family": family, "subtrack": subtrack, "instance": instance})
+            entries.append(
+                {"family": family, "subtrack": subtrack, "instance": instance}
+            )
 
     return {
         "source_csv": csv_path.name,
@@ -127,7 +129,9 @@ def main() -> int:
     args = parser.parse_args()
     manifest = select(args.csv)
     args.out.parent.mkdir(parents=True, exist_ok=True)
-    args.out.write_text(json.dumps(manifest, indent=2, sort_keys=True) + "\n", encoding="utf-8")
+    args.out.write_text(
+        json.dumps(manifest, indent=2, sort_keys=True) + "\n", encoding="utf-8"
+    )
     print(f"wrote {args.out} ({manifest['total_selected']} rows)")
     for stratum in manifest["strata"]:
         if stratum["selected"] < stratum["requested"]: