Merge branch 'master' into patch-3

smtcomp/archive.py

@@ -105,3 +105,17 @@ def unpack(archive: defs.Archive, dst: Path) -> None:
     if not (is_unpack_present(archive, dst)):
         print("[red]Empty archive", archive_file)
         exit(1)
+
+
+def download_unpack(s: defs.Submission, dst: Path) -> None:
+    """
+    Download and unpack
+    """
+    dst.mkdir(parents=True, exist_ok=True)
+    if s.archive:
+        download(s.archive, dst)
+        unpack(s.archive, dst)
+    for p in s.participations.root:
+        if p.archive:
+            download(p.archive, dst)
+            unpack(p.archive, dst)

smtcomp/benchexec.py

@@ -102,9 +102,7 @@ def generate_tool_modules(s: defs.Submission, cachedir: Path) -> None:
     generate_tool_module(s, cachedir, False)
 
 
-def generate_xml(
-    timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: List[CmdTask], file: Path, tool_module_name: str
-) -> None:
+def generate_xml(config: defs.Config, cmdtasks: List[CmdTask], file: Path, tool_module_name: str) -> None:
     doc, tag, text = Doc().tagtext()
 
     doc.asis('<?xml version="1.0"?>')
@@ -115,10 +113,10 @@ def generate_xml(
     with tag(
         "benchmark",
         tool=f"tools.{tool_module_name}",
-        timelimit=f"{timelimit_s}s",
-        hardlimit=f"{timelimit_s+30}s",
-        memlimit=f"{memlimit_M} MB",
-        cpuCores=f"{cpuCores}",
+        timelimit=f"{config.timelimit_s}s",
+        hardlimit=f"{config.timelimit_s+30}s",
+        memlimit=f"{config.memlimit_M} MB",
+        cpuCores=f"{config.cpuCores}",
     ):
         with tag("require", cpuModel="Intel Xeon E3-1230 v5 @ 3.40 GHz"):
             text()
@@ -180,3 +178,24 @@ def cmdtask_for_submission(s: defs.Submission, cachedir: Path, target_track: def
                 )
                 res.append(cmdtask)
     return res
+
+
+def generate(s: defs.Submission, cachedir: Path, config: defs.Config) -> None:
+    generate_tool_modules(s, cachedir)
+
+    for target_track in [
+        defs.Track.SingleQuery,
+        defs.Track.Incremental,
+        defs.Track.ModelValidation,
+        defs.Track.UnsatCore,
+    ]:
+        res = cmdtask_for_submission(s, cachedir, target_track)
+        if res:
+            basename = get_xml_name(s, target_track)
+            file = cachedir / basename
+            generate_xml(
+                config=config,
+                cmdtasks=res,
+                file=file,
+                tool_module_name=tool_module_name(s, target_track == defs.Track.Incremental),
+            )

smtcomp/defs.py

@@ -1156,6 +1156,8 @@ class Participation(BaseModel, extra="forbid"):
     @model_validator(mode="after")
     def check_archive(self) -> Participation:
         aws_track = {Track.Cloud, Track.Parallel}
+        if self.aws_repository is None and not set(self.tracks).isdisjoint(aws_track):
+            raise ValueError("aws_repository is required by Cloud and Parallel track")
         if self.aws_repository is not None and not set(self.tracks).issubset(aws_track):
             raise ValueError("aws_repository can be used only with Cloud and Parallel track")
         if (self.archive is not None or self.command is not None) and not set(self.tracks).isdisjoint(aws_track):
@@ -1252,7 +1254,7 @@ def uniq_id(self) -> str:
 
     def complete_participations(self) -> list[ParticipationCompleted]:
         """Push defaults from the submission into participations"""
-        return [p.complete(self.archive, self.command) for p in self.participations.root]
+        return [p.complete(self.archive, self.command) for p in self.participations.root if p.aws_repository is None]
 
 
 class Smt2File(BaseModel):
@@ -1374,21 +1376,39 @@ class Config:
     Number of selected benchmarks
     """
 
-    def __init__(self, data: Path) -> None:
-        if data.name != "data":
+    def __init__(self, data: Path | None) -> None:
+        if data is not None and data.name != "data":
             raise ValueError("Consistency check, data directory must be named 'data'")
-        self.previous_results = [
-            (year, data.joinpath(f"results-sq-{year}.json.gz"))
+        self._data = data
+
+    @functools.cached_property
+    def data(self) -> Path:
+        if self._data is None:
+            raise ValueError("Configuration without data")
+        return self._data
+
+    @functools.cached_property
+    def previous_results(self) -> list[tuple[int, Path]]:
+        return [
+            (year, self.data.joinpath(f"results-sq-{year}.json.gz"))
             for year in range(Config.oldest_previous_results, Config.current_year)
         ]
-        self.benchmarks = data.joinpath(f"benchmarks-{Config.current_year}.json.gz")
-        self.cached_non_incremental_benchmarks = data.joinpath(
-            f"benchmarks-non-incremental-{Config.current_year}.feather"
-        )
-        self.cached_incremental_benchmarks = data.joinpath(f"benchmarks-incremental-{Config.current_year}.feather")
-        self.cached_previous_results = data.joinpath(f"previous-sq-results-{Config.current_year}.feather")
-        self.data = data
-        self.__seed: int | None = None
+
+    @functools.cached_property
+    def benchmarks(self) -> Path:
+        return self.data.joinpath(f"benchmarks-{Config.current_year}.json.gz")
+
+    @functools.cached_property
+    def cached_non_incremental_benchmarks(self) -> Path:
+        return self.data.joinpath(f"benchmarks-non-incremental-{Config.current_year}.feather")
+
+    @functools.cached_property
+    def cached_incremental_benchmarks(self) -> Path:
+        return self.data.joinpath(f"benchmarks-incremental-{Config.current_year}.feather")
+
+    @functools.cached_property
+    def cached_previous_results(self) -> Path:
+        return self.data.joinpath(f"previous-sq-results-{Config.current_year}.feather")
 
     @functools.cached_property
     def submissions(self) -> list[Submission]:

smtcomp/generate_benchmarks.py

@@ -1,7 +1,7 @@
 from typing import Set, Dict
 from pathlib import Path
 from smtcomp import defs
-from smtcomp.benchexec import generate_benchmark_yml
+from smtcomp.benchexec import generate_benchmark_yml, get_suffix
 
 
 def path_trivial_benchmark(dst: Path, track: defs.Track, logic: defs.Logic, status: defs.Status) -> Path:
@@ -11,13 +11,13 @@ def path_trivial_benchmark(dst: Path, track: defs.Track, logic: defs.Logic, stat
     match track:
         case defs.Track.Incremental:
             assert status == defs.Status.Incremental
-            suffix = "_inc"
+            suffix = get_suffix(track)
         case defs.Track.ModelValidation:
             assert status != defs.Status.Incremental
-            suffix = "_model"
+            suffix = get_suffix(track)
         case defs.Track.SingleQuery:
             assert status != defs.Status.Incremental
-            suffix = ""
+            suffix = get_suffix(track)
         case defs.Track.UnsatCore | defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel:
             raise (ValueError("No trivial benchmarks yet for f{track}"))
     logic_dir = dst.joinpath(f"files{suffix}", str(logic))
@@ -41,12 +41,8 @@ def generate_trivial_benchmarks(dst: Path) -> None:
     dst.joinpath("files_inc").mkdir(parents=True, exist_ok=True)
     for track, divisions in defs.tracks.items():
         match track:
-            case defs.Track.Incremental:
-                suffix = "_inc"
-            case defs.Track.ModelValidation:
-                suffix = "_model"
-            case defs.Track.SingleQuery:
-                suffix = ""
+            case defs.Track.Incremental | defs.Track.ModelValidation | defs.Track.SingleQuery:
+                suffix = get_suffix(track)
             case defs.Track.UnsatCore | defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel:
                 continue
         for _, logics in divisions.items():
@@ -87,7 +83,11 @@ def generate_trivial_benchmarks(dst: Path) -> None:
                     generate_benchmark_yml(file_unsat, False, None)
 
 
-def generate_benchmarks(dst: Path, seed: int) -> None:
+def generate_benchmarks(cachedir: Path) -> None:
+    """
+    Generate files included by benchexec
+    """
+    dst = cachedir / "benchmarks"
     prop_dir = dst.joinpath("properties")
     prop_dir.mkdir(parents=True, exist_ok=True)
     (prop_dir / "SMT.prp").touch()
@@ -96,12 +96,8 @@ def generate_benchmarks(dst: Path, seed: int) -> None:
     dst.joinpath("files_inc").mkdir(parents=True, exist_ok=True)
     for track, divisions in defs.tracks.items():
         match track:
-            case defs.Track.Incremental:
-                suffix = "_inc"
-            case defs.Track.ModelValidation:
-                suffix = "_model"
-            case defs.Track.SingleQuery:
-                suffix = ""
+            case defs.Track.Incremental | defs.Track.ModelValidation | defs.Track.SingleQuery:
+                suffix = get_suffix(track)
             case defs.Track.UnsatCore | defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel:
                 continue
         for _, theories in divisions.items():