Simulate previous year criteria

smtcomp/main.py

@@ -1,7 +1,7 @@
 import json
 import itertools
 from pathlib import Path
-from typing import List, Optional, cast, Dict, Any
+from typing import List, Optional, cast, Dict, Any, Annotated
 import rich
 from rich.progress import track
 import rich.style
@@ -240,12 +240,17 @@ def merge_benchmarks(files: list[Path], dst: Path) -> None:
     write_cin(dst, defs.Benchmarks(incremental=incremental, non_incremental=non_incremental).model_dump_json(indent=1))
 
 
+OLD_CRITERIA = Annotated[bool, typer.Option(help="Simulate previous year criteria (needs only to be trivial one year)")]
+
+
 @app.command()
-def show_benchmarks_trivial_stats(data: Path) -> None:
+def show_benchmarks_trivial_stats(data: Path, old_criteria: OLD_CRITERIA = False) -> None:
     datafiles = defs.DataFiles(data)
     benchmarks = pl.read_ipc(datafiles.cached_non_incremental_benchmarks)
     results = pl.read_ipc(datafiles.cached_previous_results)
-    benchmarks_with_trivial_info = smtcomp.selection.add_trivial_run_info(benchmarks, results)
+    benchmarks_with_trivial_info = smtcomp.selection.add_trivial_run_info(
+        benchmarks.lazy(), results.lazy(), old_criteria
+    )
     b3 = (
         benchmarks_with_trivial_info.group_by(["logic"])
         .agg(
@@ -287,7 +292,7 @@ def show_benchmarks_trivial_stats(data: Path) -> None:
 
 
 @app.command()
-def show_sq_selection_stats(data: Path, seed: int) -> None:
+def show_sq_selection_stats(data: Path, seed: int, old_criteria: OLD_CRITERIA = False) -> None:
     """
     Show statistics on the benchmarks selected for single query track
 
@@ -296,7 +301,7 @@ def show_sq_selection_stats(data: Path, seed: int) -> None:
     datafiles = defs.DataFiles(data)
     benchmarks = pl.read_ipc(datafiles.cached_non_incremental_benchmarks)
     results = pl.read_ipc(datafiles.cached_previous_results)
-    benchmarks_with_info = smtcomp.selection.add_trivial_run_info(benchmarks, results)
+    benchmarks_with_info = smtcomp.selection.add_trivial_run_info(benchmarks.lazy(), results.lazy(), old_criteria)
     benchmarks_with_info = smtcomp.selection.sq_selection(benchmarks_with_info, seed)
     b3 = (
         benchmarks_with_info.group_by(["logic"])

smtcomp/selection.py

@@ -22,30 +22,40 @@
 c_file = pl.col("file")
 
 
-def find_trivial(results: pl.LazyFrame) -> pl.LazyFrame:
+def find_trivial(results: pl.LazyFrame, old_criteria: bool) -> pl.LazyFrame:
+    incoherence_scope = ["file", "year"] if old_criteria else ["file"]
     tally = (
         results
+        # Remove incoherent results
+        .filter(
+            (c_result != int(defs.Status.Sat)).all().over(*incoherence_scope)
+            | (c_result != int(defs.Status.Unsat)).all().over(*incoherence_scope)
+        )
         # Remove the results of non-competitive year (the only result for this file for this year)
         .filter(c_file.len().over("file", "year") > 1)
         # Aggregate information for each file
-        .group_by("file").agg(
+        .group_by("file", "year")
+        .agg(
             trivial=
             # All the results are sat or unsat and the time is below 1s
             ((c_result != int(defs.Status.Unknown)) & (c_cpu_time <= 1.0)).all()
-            # No contradictory results
-            & ((c_result == int(defs.Status.Sat)).any() & (c_result == int(defs.Status.Unsat)).any()).not_(),
+        )
+        .group_by("file")
+        .agg(
+            trivial=c_trivial.any() if old_criteria else c_trivial.all(),
             run=True,
         )
     )
     return tally
 
 
-def add_trivial_run_info(benchmarks: pl.DataFrame, previous_results: pl.DataFrame) -> pl.LazyFrame:
+def add_trivial_run_info(
+    benchmarks: pl.LazyFrame, previous_results: pl.LazyFrame, old_criteria: bool = False
+) -> pl.LazyFrame:
 
-    is_trivial = find_trivial(previous_results.lazy())
+    is_trivial = find_trivial(previous_results, old_criteria)
     return (
-        benchmarks.lazy()
-        .join(is_trivial, on="file", how="outer_coalesce")
+        benchmarks.join(is_trivial, on="file", how="outer_coalesce")
         .fill_null(False)
         .with_columns(new=pl.col("family").str.starts_with(str(defs.Config.current_year)))
     )