Incorporated suggestions by Francois.

README.md

@@ -257,3 +257,17 @@ The step from Single Query can be followed with the model validation results whe
 ---
 
 Repository initiated with [fpgmaas/cookiecutter-poetry](https://github.com/fpgmaas/cookiecutter-poetry).
+
+## Using the `smtcomp` tool for handling results for Cloud and Parallel tracks provided in `csv` format by AWS
+
+Works the same for both Parallel and Cloud track. If only one csv file is provided, the file needs to be split into one just containing the results for the relevant track. Furthermore, the file must be called results.csv, stored in its own local directory (here tmp/cloud_results), and contain at least the columns: solver, scramble_id, logic, solver_time, file, track, and solver_result.
+
+We will suppose that results.csv is locally available in directory `tmp/cloud_results`:
+
+In order to allow looking at the results incrementally, the first step is to translate the `.csv` file into a faster `.feather` file.
+
+```
+smtcomp convert-aws-results tmp/cloud_results
+```
+
+Everything else works the same as for any feather file that was converted by `smtcomp convert-benchexec-results`.

smtcomp/results.py

@@ -470,7 +470,9 @@ def helper_get_results(
 
     selection = smtcomp.selection.helper(config, track).filter(selected=True).with_columns(track=int(track))
 
-    selection = selection.unique()
+    selection = (
+        selection.unique()
+    )  # Needed because smtcomp.selection.helper(...) returns the selected benchmarks for both Cloud and Parallel track at once if track equals either of them. This can lead to dublipcates! Should be improved later.
 
     selection = (
         add_columns(selection, smtcomp.selection.tracks(), on=["track", "logic"], defaults={"division": -1})
@@ -500,10 +502,8 @@ def parse_aws_csv(dir: Path) -> pl.LazyFrame:
     """
     output columns: solver, participation, track, cputime_s, memory_B, status, walltime_s, scramble_id, file, answer
 
-    The track stored in the results is *not* used for some decisions:
-    - if a file mapping.json is present it used and the original_id.csv is not needed
-    - if original_id is present it is used (all the other track)
-    - if it ends with "unsatcore" and the directory "../unsat_core_valisation_results" is present and converted (feather file) it is used to validate the unsat cores
+    Assumes that there is a file results.csv in the directory dir. The file
+    must contain columns: solver, scramble_id, logic, solver_time, file, track, solver_result
     """
 
     def aws_logic(logic: str) -> int:
@@ -535,10 +535,10 @@ def aws_result(res: str) -> int:
     )
 
     results = lf.with_columns(
-        participation = pl.lit(0,dtype=pl.Int64),
-        memory_B = pl.lit(0,dtype=pl.Int64),
-        nb_answers = pl.lit(0,dtype=pl.Int64),
-        cputime_s = pl.lit(0,dtype=pl.Int64),
+        participation=pl.lit(0, dtype=pl.Int64),
+        memory_B=pl.lit(0, dtype=pl.Int64),
+        nb_answers=pl.lit(0, dtype=pl.Int64),
+        cputime_s=pl.lit(0, dtype=pl.Int64),
     )
 
     return results