Merge branch 'master' into patch-1

README.md

@@ -17,6 +17,19 @@ Tools used for the organization of the SMT competition
 git clone [email protected]:smtcomp/smtcomp.github.io.git
 ```
 
+On Debian/Ubuntu installation a virtual env (here in .venv) is needed:
+
+```
+python3 -m venv .venv
+source .venv/bin/activate
+```
+
+Poetry is used for handling dependencies:
+
+```
+pip install poetry
+```
+
 Finally, install the environment with
 
 ```bash
@@ -56,10 +69,10 @@ $DIR/zenodo
 Then you can run (very io intensive):
 
 ```
-smtcomp $DIR/zenodo ./data/
+smtcomp create-benchmarks-list $DIR/zenodo ./data/
 ```
 
-The directory `./data/` is the one present in this repository
+The directory `./data/` is the one present in this repository.
 
 ## Using the smtcomp tool for selecting the benchmarks
 

smtcomp/main.py

@@ -11,6 +11,7 @@
 import typer
 from pydantic import ValidationError
 from collections import defaultdict
+import json
 
 import polars as pl
 
@@ -69,6 +70,21 @@ def show(
             md.write("</details>\n")
 
 
+@app.command(rich_help_panel=submissions_panel)
+def show_json(files: list[Path] = typer.Argument(None), prefix: Optional[Path] = None) -> None:
+    """
+    Show information about solver submissions in JSON format
+    """
+
+    if prefix is not None:
+        files = list(map(prefix.joinpath, files))
+
+    l = list(map(submission.read_submission_or_exit, files))
+
+    data = [submission.raw_summary(s) for s in l]
+    print(json.dumps(data, indent=4))
+
+
 @app.command(rich_help_panel=submissions_panel)
 def get_contacts(files: list[Path] = typer.Argument(None)) -> None:
     """

smtcomp/submission.py

@@ -50,6 +50,25 @@ def rich_tree_summary(s: Submission) -> Tree:
     return tree
 
 
+def raw_summary(s: Submission) -> dict[str, Any]:
+    data = dict[str, Any]()
+    data["name"] = s.name
+    data["authors"] = [c.name for c in s.contributors]
+    data["website"] = str(s.website)
+    data["archive_url"] = str(s.archive.url if s.archive is not None else "")
+    data["system_description"] = str(s.system_description)
+    data["tracks"] = dict[str, dict[str, list[str]]]()
+
+    tracks = s.participations.get()
+    for track, divs in sorted(tracks.items()):
+        divisions = {}
+        for div, logics in sorted(divs.items()):
+            divisions[str(div)] = [str(l) for l in logics]
+        data["tracks"][str(track)] = divisions
+
+    return data
+
+
 def md_item(md: TextIO, s: str, level: int) -> None:
     md.write("  " * level)
     md.write("* ")
@@ -111,4 +130,4 @@ def merge_all_submissions(local_repo_path: str) -> None:
             shas = [p.head.sha for p in fpulls]
             message = "merge submissions\n\n" + "\n".join(f"#{p.number}: {p.title}" for p in fpulls)
             print(shas)
-            subprocess.run(["git", "-C", local_repo_path, "merge", "-m", message] + shas)
+            subprocess.run(["git", "-C", local_repo_path, "merge", "-m", message, "-s", "ours"] + shas)

web/content/model/index.md

@@ -2,6 +2,7 @@
 title = 'Model Validation Track'
 date = 2023-12-11T21:09:02+01:00
 draft = false
+aliases = ['/model.html']
 +++
 
 ## Experimental model validation track

web/content/parallel_cloud/index.md

@@ -2,6 +2,7 @@
 title = 'Parallel and Cloud Tracks'
 date = 2024-05-07T10:09:02+01:00
 draft = false
+aliases = ['/parallel-and-cloud-tracks.html']
 +++
 
 ## Parallel and Cloud Tracks

web/content/participants/_index.md

@@ -0,0 +1,8 @@
++++
+layout = 'single'
+title = 'Participants'
++++
+
+The following solvers have been submitted to SMT-COMP 2024 or were entered as non-competing solvers by the organizers for comparison.
+
+{{< participants >}}