Fix naming in submissions for parallel track

Makefile

@@ -31,6 +31,12 @@ build: clean-build ## Build wheel file using poetry
 clean-build: ## clean build artifacts
 	@rm -rf dist
 
+.PHONY: clean-web-results
+clean-web-results: ## clean web results
+	@rm -rf web/content/results
+	@rm -rf web/public/results
+
+
 .PHONY: help
 help:
 	@grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-20s\033[0m %s\n", $$1, $$2}'

pyproject.toml

@@ -17,9 +17,6 @@ dependencies = [
 "gitpython",
 "yattag",
 "wget",
-"option",
-"requests",
-"bs4",
 "benchexec",
 "polars",
 "PyGithub"

smtcomp/benchexec.py

@@ -28,6 +28,8 @@ def get_suffix(track: defs.Track) -> str:
             return "_parallel"
         case defs.Track.Cloud:
             return "_cloud"
+        case defs.Track.ProofExhibition:
+            return "_proof"
 
 
 def get_xml_name(s: defs.Submission, track: defs.Track, division: defs.Division) -> str:
@@ -47,7 +49,7 @@ class CmdTask(BaseModel):
 
 
 def generate_benchmark_yml(
-    ymlfile: Path, benchmark: Path, expected_result: Optional[bool], orig_file: Optional[Path]
+    ymlfile: Path, benchmark: Path, expected_result: Optional[bool], orig_file: Optional[Path] = None
 ) -> None:
     with ymlfile.open("w") as f:
         f.write("format_version: '2.0'\n\n")

smtcomp/defs.py

@@ -135,7 +135,7 @@ def name_is_default_field(cls, data: Any) -> Any:
 
 class SolverType(EnumAutoInt):
     wrapped = "wrapped"
-    derived = "derived"
+    derived = "derived"  # TODO: put a datatype information on base solver
     standalone = "Standalone"
     portfolio = "Portfolio"
 
@@ -1317,6 +1317,7 @@ class Submission(BaseModel, extra="forbid"):
     website: HttpUrl
     system_description: HttpUrl
     solver_type: SolverType
+    # TODO add field base_solver?
     participations: Participations
     seed: int | None = None
     competitive: bool = True
@@ -1325,6 +1326,7 @@ class Submission(BaseModel, extra="forbid"):
         description="Must be set for the final version of the submission. An archive on zenodo is needed in this case.",
     )
 
+    # TODO: model validator to check the sanity of the new base_solver field
     @model_validator(mode="after")
     def check_archive(self) -> Submission:
         if self.archive is None and not all(p.archive for p in self.participations.root):
@@ -1510,11 +1512,26 @@ class Config:
     Benchmarks to remove before selection
     """
 
-    removed_results = []
+    removed_results: list[Any] = []
+
     """
     Benchmarks to remove after running the solvers. Can be used when the selection has already been done.
     """
 
+    """
+    Solver -> Base solver map for 2025
+    TODO: refactor this into Submission
+    """
+    baseSolverMap2025 = {
+        "Bitwuzla-MachBV": "Bitwuzla-MachBV-base",
+        "Z3-Inc-Z3++": "Z3-Inc-Z3++-base",
+        "Z3-Noodler-Mocha": "Z3-Noodler-Mocha-base",
+        "Z3-Owl": "Z3-Owl-base",
+        "Z3-Noodler": "Z3-Noodler",
+        "z3siri": "z3siri-base",
+        "Z3-alpha": "Z3-alpha-base",
+    }
+
     def __init__(self, data: Path | None) -> None:
         self.id = self.__class__.__next_id__
         self.__class__.__next_id__ += 1
@@ -1578,6 +1595,10 @@ def submissions(self) -> list[Submission]:
             Submission.model_validate_json(Path(file).read_text()) for file in self.data.glob("../submissions/*.json")
         ]
 
+    @functools.cached_property
+    def competitive_solvers(self) -> list[str]:
+        return [s.name for s in self.submissions if s.competitive]
+
     @functools.cached_property
     def web_results(self) -> Path:
         return self.data / ".." / "web" / "content" / "results"

smtcomp/generate_benchmarks.py

@@ -81,5 +81,5 @@ def generate_trivial_benchmarks(dst: Path) -> None:
                     file_sat.write_text(f"(set-logic {logic.value})(check-sat)")
                     file_unsat.write_text(f"(set-logic {logic.value})(assert false)(check-sat)")
 
-                    generate_benchmark_yml(file_sat, True, None)
-                    generate_benchmark_yml(file_unsat, False, None)
+                    generate_benchmark_yml(file_sat.with_suffix(".yml"), file_sat, True, None)
+                    generate_benchmark_yml(file_unsat.with_suffix(".yml"), file_unsat, False, None)