Merge remote-tracking branch 'origin/2025_final_execution' into presentation-derived-solver

Author: wintered

README.md

@@ -257,7 +257,7 @@ The step from Single Query can be followed with the model validation results whe
 Tasks for unsat core validation can be generated by:
 
 ```
-smtcomp generate-unsatcore-validation-files ../tmp/execution SCRAMBLER_EXECUTABLE UNSAT_CORE_RESULT_DIR/*/*
+smtcomp generate-unsatcore-validation-files ../tmp/execution SCRAMBLER_EXECUTABLE UNSAT_CORE_RESULT_DIR
 ```
 
 ---

data/latex-certificates/gen_certificates_ornament.tex

@@ -136,7 +136,7 @@
       \node [circular drop shadow={shadow scale=1.05},
              decorate, decoration=zigzag,
              fill=blue!20,draw,thick,circle,text width=3.5cm,align=center,xshift=2cm]
-              {\large\textbf{SMT-COMP\\ 2024}};
+              {\large\textbf{SMT-COMP\\ 2025}};
     \end{tikzpicture}
     \end{minipage}
 

data/latex-certificates/solvers_pretty_name.csv

@@ -10,6 +10,7 @@
 import smtcomp.defs as defs
 import smtcomp.results as results
 import smtcomp.generate_website_page as page
+import smtcomp.submission as submission
 
 show_experimental = False
 
@@ -70,11 +71,13 @@ def withtrack(l: list[str], name: str, category: category) -> None:
 class overall:
 
     def __init__(self) -> None:
+        self.best = category()
         self.biggest = category()
         self.largest = category()
 
     def latex(self) -> str:
         l: list[str] = []
+        withtrack(l, "Best Overall", self.best)
         withtrack(l, "Biggest Lead", self.biggest)
         withtrack(l, "Largest Contribution", self.largest)
         return ", ".join(l)
@@ -83,7 +86,7 @@ def __str__(self) -> str:
         return self.latex()
 
     def isNotEmpty(self) -> bool:
-        return self.biggest.isNotEmpty() and self.largest.isNotEmpty()
+        return self.best.isNotEmpty() or self.biggest.isNotEmpty() or self.largest.isNotEmpty()
 
 
 class info:
@@ -132,7 +135,7 @@ def __repr__(self) -> str:
 def update(
     solvers: defaultdict[str, info],
     select: Callable[[info, str], None],
-    podium: page.PodiumDivision | page.PodiumBiggestLead | page.PodiumLargestContribution,
+    podium: page.PodiumDivision | page.PodiumBestOverall | page.PodiumBiggestLead | page.PodiumLargestContribution,
 ) -> None:
     if podium.track == defs.Track.SingleQuery:
         select(solvers[podium.winner_seq], "sq_seq")
@@ -173,12 +176,10 @@ def add_logic(logics: dict[Tuple[str, defs.Track], bool], list: dict[str, int],
         logics[v, track] = True
 
 
-def parse_pretty_names(solvers: defaultdict[str, info], pretty_names: Path) -> None:
-    with open(pretty_names, newline="") as input:
-        input = csv.DictReader(input)  # type: ignore
-
-        for row in input:
-            solvers[row["Solver Name"]].members = int(row["Members"])  # type: ignore
+def process_submissions(solvers: defaultdict[str, info], submissions: list[defs.Submission]) -> None:
+    for s in submissions:
+        if s.competitive:
+            solvers[s.name].members = len(s.contributors)
 
 
 def parse_experimental_division(solvers: Any, experimental_division: Path) -> dict[str, bool]:
@@ -192,11 +193,14 @@ def parse_experimental_division(solvers: Any, experimental_division: Path) -> di
 
 
 def generate_certificates(
-    website_results: Path, input_for_certificates: Path, pretty_names: Path, experimental_division: Path
+    website_results: Path, input_for_certificates: Path, submission_dir: Path, experimental_division: Path
 ) -> None:
     solvers: defaultdict[str, info] = defaultdict(info)
 
-    parse_pretty_names(solvers, pretty_names)
+    submissions = [submission.read_submission_or_exit(f)
+                   for f in submission_dir.glob("*.json")]
+
+    process_submissions(solvers, submissions)
     solvers["-"].members = 0
 
     # Remove experimental division
@@ -223,6 +227,8 @@ def generate_certificates(
                 continue
             case page.PodiumCrossDivision():
                 match result.root:
+                    case page.PodiumBestOverall():
+                        update(solvers, (lambda x, k: x.overall.best.update(k, True)), result.root)
                     case page.PodiumBiggestLead():
                         update(solvers, (lambda x, k: x.overall.biggest.update(k, True)), result.root)
                     case page.PodiumLargestContribution():

data/results-uc-2025.json.gz

@@ -1471,8 +1471,8 @@ class Config:
     cpuCores_test = 2
     cpuCores_parallel = 128
     cpuCores_parallel_test = 8
-    unsatcore_validation_timelimit_s = 60 * 5
-    unsatcore_validation_memlimit_M = 1024 * 30
+    unsatcore_validation_timelimit_s = 60 * 20
+    unsatcore_validation_memlimit_M = 1024 * 15
     unsatcore_validation_cpuCores = 4
     min_used_benchmarks = 300
     ratio_of_used_benchmarks = 0.5

smtcomp/certificates.py

@@ -232,7 +232,7 @@ class PodiumLargestContribution(BaseModel):
 
 
 class PodiumCrossDivision(RootModel):
-    root: PodiumLargestContribution | PodiumBiggestLead = Field(..., discriminator="recognition")
+    root: PodiumBestOverall | PodiumLargestContribution | PodiumBiggestLead = Field(..., discriminator="recognition")
 
 
 class Podium(RootModel):

smtcomp/defs.py

@@ -239,9 +239,8 @@ def store_results(
                 on=["file"],
                 defaults={"logic": -1, "family": "", "name": ""},
             )
-            .join(removed_results, on=["logic", "family", "name"], how="anti")
-            .sort("file", "solver")
-            .collect()
+            # .join(removed_results, on=["logic", "family", "name"], how="anti")
+            .sort("file", "solver").collect()
         )
         if len(df) > 0:
             results_track = defs.Results(
@@ -1060,10 +1059,9 @@ def keyfunc(
 
 
 @app.command()
-def generate_unsatcore_validation_files(
-    cachedir: Path, scrambler: Path, resultdirs: list[Path], max_workers: int = 8
-) -> None:
-    unsat_core_validation.generate_validation_files(cachedir, resultdirs, scrambler)
+def generate_unsatcore_validation_files(cachedir: Path, scrambler: Path, resultdir: Path) -> None:
+
+    unsat_core_validation.generate_validation_files(cachedir, resultdir, scrambler)
 
 
 @app.command()
@@ -1134,12 +1132,12 @@ def build_dolmen(data: Path) -> None:
 def generate_certificates(
     website_results: Path = Path("web/content/results"),
     input_for_certificates: Path = Path("data/latex-certificates/input_for_certificates.tex"),
-    pretty_names: Path = Path("data/latex-certificates/solvers_pretty_name.csv"),
+    submission_dir: Path = Path("submissions"),
     experimental_division: Path = Path("data/latex-certificates/experimental.csv"),
 ) -> None:
     """
     generates the input data for the tex certificate generator.
     """
     smtcomp.certificates.generate_certificates(
-        website_results, input_for_certificates, pretty_names, experimental_division
+        website_results, input_for_certificates, submission_dir, experimental_division
     )

smtcomp/generate_website_page.py

@@ -124,7 +124,7 @@ def convert_run(r: ET.Element) -> Run | None:
     parts = r.attrib["name"].split("/")
     logic = defs.Logic(parts[-2])
     benchmark_yml = parts[-1]
-    benchmark_file = int(benchmark_yml.split("_", 1)[0])
+    benchmark_file = smtcomp.scramble_benchmarks.unscramble_yml_basename(benchmark_yml)
     cputime_s: Optional[float] = None
     memory_B: Optional[int] = None
     answer: Optional[defs.Answer] = None
@@ -367,17 +367,17 @@ def parse_mapping(p: Path) -> pl.LazyFrame:
     return pl.LazyFrame(
         (
             (
-                smtcomp.scramble_benchmarks.unscramble_yml_basename(Path(k).name),
+                int(file),
                 sorted(v["core"]),
                 smtcomp.scramble_benchmarks.unscramble_yml_basename(Path(v["file"]).name),
             )
-            for k, l in d.items()
-            for v in l
+            for file, cores in d.items()
+            for v in cores
         ),
         {
-            "scramble_id_orig": pl.Int64,
+            "orig_file": pl.Int64,
             "unsat_core": pl.List(pl.Int64),
-            "scramble_id": pl.Int64,
+            "file": pl.Int64,
         },
     )
 
@@ -402,35 +402,44 @@ def parse_dir(dir: Path, no_cache: bool) -> pl.LazyFrame:
     l_parsed = list(track((parse_to_pl(f, no_cache) for f in l), total=len(l)))
     results = pl.concat(l_parsed)
 
-    ucvr = dir / "../unsat_core_validation_results" / "parsed.feather"
-    if (dir.name).endswith("unsatcore"):
-        json = dir / json_mapping_name
-        if not json.exists():
-            raise (ValueError(f"No file {json!s} in the directory"))
+    uc_validation_results = dir / "../unsat_core_validation_results" / "parsed.feather"
+
+    json = dir / json_mapping_name
+    if json.exists():
+        # add information about the original benchmark to each UC validation run
         lf = parse_mapping(json)
-        defaults = {"unsat_core": [], "scramble_id_orig": -1}
+        results = add_columns(results.drop("unsat_core"), lf, on=["file"], defaults={"unsat_core": [], "orig_file": -1})
 
-        if ucvr.is_file():
-            vr = pl.read_ipc(ucvr).lazy()
+    if (dir.name).endswith("unsatcore"):
+        if uc_validation_results.is_file():
+            # compute stats of validated and refuted cores
+            vr = pl.read_ipc(uc_validation_results).lazy()
             vr = (
-                vr.select("answer", "unsat_core", scramble_id="scramble_id_orig")
-                .group_by("scramble_id", "unsat_core")
+                vr.select("answer", "unsat_core", file="orig_file")
+                .group_by("file", "unsat_core")
                 .agg(
-                    sat=(pl.col("answer") == int(defs.Answer.Sat)).count(),
-                    unsat=(pl.col("answer") == int(defs.Answer.Unsat)).count(),
+                    sat=(pl.col("answer") == int(defs.Answer.Sat)).sum(),
+                    unsat=(pl.col("answer") == int(defs.Answer.Unsat)).sum(),
                     validation_attempted=True,
                 )
             )
+
             results = add_columns(
                 results,
                 vr,
-                on=["scramble_id", "unsat_core"],
+                on=["file", "unsat_core"],
                 defaults={"sat": 0, "unsat": 0, "validation_attempted": False},
             )
+
+            # change answer according to the validity of the core
             results = results.with_columns(
-                answer=pl.when((pl.col("answer") == int(defs.Answer.Unsat)) & (pl.col("sat") > pl.col("unsat")))
-                .then(int(defs.Answer.UnsatCoreInvalidated))
-                .otherwise("answer")
+                answer=pl.when((pl.col("answer") == int(defs.Answer.Unsat)) & (pl.col("sat") >= pl.col("unsat")))
+                .then(
+                    pl.when(pl.col("sat") == 0)
+                    .then(int(defs.Answer.Unknown))  # sat == unsat == 0
+                    .otherwise(int(defs.Answer.UnsatCoreInvalidated))
+                )
+                .otherwise("answer")  # sat < unsat
             ).drop("sat", "unsat", "unsat_core")
         else:
             results = results.with_columns(validation_attempted=False)

smtcomp/main.py

@@ -21,19 +21,18 @@ def scramble_basename(id: int, suffix: str = "smt2") -> str:
 
 
 def unscramble_yml_basename(basename: str) -> int:
-    # We are unscrabling scrambled%i.yml
-    assert basename[0:9] == "scrambled"
-    # assert basename[-4:] == ".yml"
+    # We are unscrabling {i}.yml or scrambled{i}_{core}.smt2
     if basename[-4:] == ".yml":
-        return int(basename[9:-4])
+        parts = basename.split("_")
+        file_id = parts[0]
+        return int(file_id)
     else:
+        assert basename[0:9] == "scrambled"
         assert basename[-5:] == ".smt2"
         s = basename[9:-5]
-        l = list(map(int, s.split("_")))
-        i = l[0]
-        if len(l) > 1:
-            i += l[1] * 10_000_000  # Hack for unsat_core_verification
-        return i
+        file_id, core = list(map(int, s.split("_")))
+        file_id += core * 10_000_000  # Hack for unsat_core_verification
+        return file_id
 
 
 def benchmark_files_dir(cachedir: Path, track: defs.Track) -> Path: