Add results conversion

smtcomp/convert_csv.py

@@ -11,6 +11,7 @@
 from rich.progress import track
 
 import smtcomp.defs as defs
+from smtcomp.list_benchmarks import get_smt2_file
 
 
 class CsvColumn(str, Enum):
@@ -175,3 +176,36 @@ def convert_csv(file: Path, dstdir: Path) -> None:
                 submission = convert_row(row, dstdir)
                 with open(Path.joinpath(dstdir, submission.name + ".json"), "w") as f:
                     f.write(submission.model_dump_json())
+
+
+def convert_csv_result(file: Path, track: defs.Track) -> defs.Results:
+    # Some csv benchmark name start with track_.../QF..
+    with open(file) as dcsv:
+        results = csv.DictReader(dcsv)
+        compatibility = next(results)["benchmark"].startswith("track_")
+
+    with open(file) as dcsv:
+        results = csv.DictReader(dcsv)
+        l: list[defs.Result] = []
+        for row in results:
+            if row["result"] == "starexec-unknown":
+                row["result"] = "unknown"
+            elif row["result"] == "--":
+                row["result"] = "unknown"
+            row["benchmark"] = row["benchmark"].replace("UFFPDTLIRA", "UFFPDTNIRA")
+
+            smt2file = get_smt2_file(src=None, file=Path(row["benchmark"]), incremental=track is defs.Track.Incremental)
+
+            l.append(
+                defs.Result(
+                    track=track,
+                    file=smt2file,
+                    solver=row["solver"],
+                    cpu_time=float(row["cpu time"]),
+                    wallclock_time=float(row["wallclock time"]),
+                    memory_usage=float(row["memory usage"]),
+                    result=defs.Status(row["result"]),
+                )
+            )
+
+    return defs.Results(results=l)

smtcomp/defs.py

@@ -2,14 +2,19 @@
 
 import hashlib
 import re
-from enum import Enum
+from enum import Enum as enum_Enum
 from pathlib import Path
-from typing import Any
+from typing import Any, Dict
 
 from pydantic import BaseModel, Field, RootModel, model_validator
 from pydantic.networks import HttpUrl, validate_email
 
 
+class Enum(enum_Enum):
+    def __str__(self) -> str:
+        return str(self.value)
+
+
 class NameEmail(BaseModel):
     """
     Name and valide email "name <email>"
@@ -84,9 +89,6 @@ class SolverType(str, Enum):
     standalone = "Standalone"
 
 
-# class RegexpTracks:
-
-
 class Status(str, Enum):
     Unsat = "unsat"
     Sat = "sat"
@@ -129,9 +131,6 @@ class Division(str, Enum):
 
 
 class Logic(str, Enum):
-    def __str__(self) -> str:
-        return str(self.value)
-
     ABV = "ABV"
     ABVFP = "ABVFP"
     ABVFPLRA = "ABVFPLRA"
@@ -174,6 +173,7 @@ def __str__(self) -> str:
     QF_BV = "QF_BV"
     QF_BVFP = "QF_BVFP"
     QF_BVFPLRA = "QF_BVFPLRA"
+    QF_BVLRA = "QF_BVLRA"
     QF_DT = "QF_DT"
     QF_FP = "QF_FP"
     QF_FPLRA = "QF_FPLRA"
@@ -1103,12 +1103,10 @@ def uniq_id(self) -> str:
 
 
 class Smt2File(BaseModel):
+    incremental: bool
     logic: Logic
-    family: list[str]
+    family: tuple[str, ...]
     name: str
-    status: Status
-    asserts: int
-    check_sats: int
 
     @model_validator(mode="after")
     def check_archive(self) -> Smt2File:
@@ -1120,13 +1118,41 @@ def check_archive(self) -> Smt2File:
         return self
 
     def path(self) -> Path:
-        return Path(self.logic).joinpath(Path(*self.family)).joinpath(self.name)
+        if self.incremental:
+            i = "incremental"
+        else:
+            i = "non-incremental"
+        return Path(i, self.logic).joinpath(Path(*self.family)).joinpath(self.name)
+
+
+class InfoIncremental(BaseModel):
+    file: Smt2File
+    check_sats: int
+
+
+class InfoNonIncremental(BaseModel):
+    file: Smt2File
+    status: Status
+    asserts: int
 
 
 class Benchmarks(BaseModel):
-    files: list[Smt2File]
+    incremental: list[InfoIncremental] = []
+    non_incremental: list[InfoNonIncremental] = []
+
+
+class Result(BaseModel):
+    track: Track
+    solver: str
+    file: Smt2File
+    result: Status
+    cpu_time: float
+    wallclock_time: float
+    memory_usage: float
+
 
+class Results(BaseModel):
+    results: list[Result]
 
-Benchmarks.model_validate_json
 
 default = {"timelimit_s": 60, "memlimit_M": 1024 * 20, "cpuCores": 4}

smtcomp/list_benchmarks.py

@@ -1,4 +1,4 @@
-from typing import Set, Dict, Optional
+from typing import Set, Dict, Optional, cast, List
 from pathlib import Path, PurePath
 from smtcomp import defs
 import subprocess
@@ -52,27 +52,52 @@ def get_nb_check_sats(src: Path) -> int:
     return int(grep.stdout)
 
 
-def get_info_smt2_file(src: Path, file: Path, scrambler: Optional[Path]) -> defs.Smt2File:
-    parts = PurePath(file.relative_to(src)).parts
+def get_smt2_file(src: Path | None, file: Path, incremental: bool) -> defs.Smt2File:
+    if src is None:
+        p = list(PurePath(file).parts)
+        parts: tuple[str, ...] = tuple()
+        for i in range(0, len(p) - 1):
+            if p[i] in defs.Logic.__members__:
+                parts = tuple(p[i:])
+                break
+    else:
+        parts = PurePath(file.relative_to(src)).parts
+
     return defs.Smt2File(
+        incremental=incremental,
         logic=defs.Logic(parts[0]),
-        family=list(parts[1:-1]),
+        family=parts[1:-1],
         name=parts[-1],
-        status=get_status(file),
-        asserts=get_nb_asserts(file, scrambler),
-        check_sats=get_nb_check_sats(file),
     )
 
 
-def list_benchmarks(src: Path, dst: Path, scrambler: Optional[Path], max_workers: int) -> defs.Benchmarks:
+def get_info_smt2_file(
+    src: Path, file: Path, scrambler: Optional[Path], incremental: bool
+) -> defs.InfoIncremental | defs.InfoNonIncremental:
+    if incremental:
+        return defs.InfoIncremental(
+            file=get_smt2_file(src, file, True),
+            check_sats=get_nb_check_sats(file),
+        )
+    else:
+        return defs.InfoNonIncremental(
+            file=get_smt2_file(src, file, False),
+            status=get_status(file),
+            asserts=get_nb_asserts(file, scrambler),
+        )
+
+
+def list_benchmarks(
+    src: Path, scrambler: Optional[Path], max_workers: int, incremental: bool
+) -> List[defs.InfoIncremental | defs.InfoNonIncremental]:
     l = list(track(src.rglob("*.smt2"), description="Scanning directories..."))
     with concurrent.futures.ThreadPoolExecutor(max_workers=max_workers) as executor:
         files = list(
             track(
-                executor.map(lambda file: get_info_smt2_file(src, file, scrambler), l),
+                executor.map(lambda file: get_info_smt2_file(src, file, scrambler, incremental), l),
                 total=len(l),
                 description="Scanning files...",
             )
         )
-    files.sort(key=(lambda k: k.path()))
-    return defs.Benchmarks(files=files)
+    files.sort(key=(lambda k: k.file.path()))
+    return files

smtcomp/main.py

@@ -1,20 +1,25 @@
 import json
 from pathlib import Path
-from typing import List, Optional
+from typing import List, Optional, cast
 import rich
 from rich.progress import track
+from rich.tree import Tree
+from rich import print
 import typer
 from pydantic import ValidationError
+from collections import defaultdict
 
 import smtcomp.archive as archive
 import smtcomp.benchexec as benchexec
 import smtcomp.defs as defs
 import smtcomp.submission as submission
 import smtcomp.execution as execution
 from smtcomp.benchmarks import clone_group
-from smtcomp.convert_csv import convert_csv as convert_csv_file
+import smtcomp.convert_csv
 import smtcomp.generate_benchmarks
 import smtcomp.list_benchmarks
+import smtcomp.selection
+from smtcomp.unpack import write_cin, read_cin
 
 app = typer.Typer()
 
@@ -55,7 +60,7 @@ def convert_csv(file: str, dstdir: Path) -> None:
     Convert a csv (old submission format) to json files (new format)
     """
     dstdir.mkdir(parents=True, exist_ok=True)
-    convert_csv_file(Path(file), Path(dstdir))
+    smtcomp.convert_csv.convert_csv(Path(file), Path(dstdir))
 
 
 @app.command()
@@ -148,11 +153,101 @@ def create_benchmarks_list(src: Path, dst: Path, scrambler: Optional[Path] = Non
         https://zenodo.org/communities/smt-lib/
 
     The tar.zst must be uncompressed.
-    The given directory must contain "non-incremental" and "incremental"
+    The given directory must contain "non-incremental" and "incremental", or be one of them itself.
 
     The path to the binary of the scrambler must be given in order to count
     """
-    benchmarks = smtcomp.list_benchmarks.list_benchmarks(src, dst, scrambler, j)
-    src.read_text
-    with open(dst, "w") as f:
-        f.write(benchmarks.model_dump_json(indent=2))
+    if src.name == "incremental":
+        files_incremental = smtcomp.list_benchmarks.list_benchmarks(src, scrambler, j, True)
+        files_non_incremental = []
+    elif src.name == "non-incremental":
+        files_incremental = []
+        files_non_incremental = smtcomp.list_benchmarks.list_benchmarks(src, scrambler, j, False)
+    else:
+        incremental = src.joinpath("incremental")
+        non_incremental = src.joinpath("non-incremental")
+        if incremental.exists():
+            files_incremental = smtcomp.list_benchmarks.list_benchmarks(src, scrambler, j, True)
+        else:
+            files_incremental = []
+        if non_incremental.exists():
+            files_non_incremental = smtcomp.list_benchmarks.list_benchmarks(src, scrambler, j, False)
+        else:
+            files_non_incremental = []
+
+        if incremental is [] and non_incremental is []:
+            raise (ValueError("The directory must contain non-incremental or incremental"))
+
+    benchmarks = defs.Benchmarks(
+        incremental=cast(List[defs.InfoIncremental], files_incremental),
+        non_incremental=cast(List[defs.InfoNonIncremental], files_non_incremental),
+    )
+    write_cin(dst, benchmarks.model_dump_json(indent=1))
+
+
+@app.command()
+def benchmarks_stats(src: Path) -> None:
+    tree = Tree(src.name)
+    benchmarks = defs.Benchmarks.model_validate_json(src.read_text())
+    d: defaultdict[str, defaultdict[tuple[str, ...], int]] = defaultdict(lambda: defaultdict(int))
+
+    def tree_info(tree: Tree, l: List[defs.InfoIncremental] | List[defs.InfoNonIncremental]) -> None:
+        for s in l:
+            d[s.file.logic][s.file.family] = d[s.file.logic][s.file.family] + 1
+        for k, v in d.items():
+            t1 = tree.add(k)
+            for f, v2 in v.items():
+                fn = "/".join(f)
+                t2 = t1.add(f"{v2:4d}: [bold magenta]{fn}[/bold magenta]")
+
+    tree_info(tree.add("non-incremental"), benchmarks.non_incremental)
+    tree_info(tree.add("incremental"), benchmarks.incremental)
+    print(tree)
+
+
+@app.command()
+def convert_csv_result(src: Path, dst: Path, track: defs.Track) -> None:
+    results = smtcomp.convert_csv.convert_csv_result(src, track)
+    write_cin(dst, results.model_dump_json(indent=1))
+
+
+def merge_results_aux(files: list[Path]) -> defs.Results:
+    results: list[defs.Result] = []
+    for file in track(files):
+        r = defs.Results.model_validate_json(read_cin(file))
+        results.extend(r.results)
+    return defs.Results(results=results)
+
+
+@app.command()
+def merge_results(files: list[Path], dst: Path) -> None:
+    write_cin(dst, merge_results_aux(files).model_dump_json(indent=1))
+
+
+@app.command()
+def merge_benchmarks(files: list[Path], dst: Path) -> None:
+    incremental: list[defs.InfoIncremental] = []
+    non_incremental: list[defs.InfoNonIncremental] = []
+    for file in track(files):
+        r = defs.Benchmarks.model_validate_json(read_cin(file))
+        incremental.extend(r.incremental)
+        non_incremental.extend(r.non_incremental)
+    write_cin(dst, defs.Benchmarks(incremental=incremental, non_incremental=non_incremental).model_dump_json(indent=1))
+
+
+@app.command()
+def select_benchmarks(benchmark: Path, previous_results: list[Path], dst: Path, track: defs.Track, seed: int) -> None:
+    bench = defs.Benchmarks.model_validate_json(read_cin(benchmark))
+    results = merge_results_aux(previous_results)
+    selection = smtcomp.selection.select(bench, results, track, seed)
+    write_cin(dst, selection.model_dump_json(indent=1))
+
+
+# def conv(x:defs.Smt2FileOld) -> defs.Info:
+#     return defs.Info( file = defs.Smt2File(logic=x.logic,family=x.family,name=x.name), status= x.status, asserts = x.asserts, check_sats = x.check_sats)
+
+# @app.command()
+# def convert(src:Path,dst:Path) -> None:
+#     benchmarks = defs.BenchmarksOld.model_validate_json(read_cin(src))
+#     benchmarks2 = defs.Benchmarks(files=list(map(conv,benchmarks.files)))
+#     write_cin(dst,benchmarks2.model_dump_json(indent=1))

smtcomp/unpack.py

@@ -5,6 +5,8 @@
 from zipfile import ZipFile
 import tarfile
 from stat import S_IXUSR
+import gzip
+from typing import AnyStr
 
 ZIP_UNIX_SYSTEM = 3
 
@@ -30,3 +32,19 @@ def extract_all_with_executable_permission(file: Path, target_dir: Path) -> None
         zip_extract_all_with_executable_permission(file, target_dir)
     else:
         tar_extract_all_with_executable_permission(file, target_dir)
+
+
+def write_cin(file: Path, content: str) -> None:
+    if file.name.endswith(".gz"):
+        with gzip.open(file, "wt") as f:
+            f.write(content)
+    else:
+        file.write_text(content)
+
+
+def read_cin(file: Path) -> str:
+    if file.name.endswith(".gz"):
+        with gzip.open(file, "rt") as f:
+            return f.read()
+    else:
+        return file.read_text()