merge submissions

#84: Create cvc5-cloud
#74: Draft STP submission
#70: draft yicesQS submission
#68: Create STP-CNFLS
#66: Yices2 SMTCOMP 2024 Submission
#65: Z3-alpha draft PR
#64: Solver submission: cvc5
#63: submission iProver
#61: OSTRICH 1.4
#60: SMT-RAT submission
#57: Amaya's submission for SMT-COMP 2024
#55: plat-smt submission
#54: Add 2024 Bitwuzla submission.
#53: 2024 solver participant submission: OpenSMT
#52: Z3-Noodler submission
#51: Submission Colibri
#45: Submission for smtinterpol
#42: Adding Algaroba to SMTCOMP 2024

README.md

@@ -1,4 +1,4 @@
-# smtcomp
+# SMT Competition
 
 [![Release](https://img.shields.io/github/v/release/smtcomp/smtcomp.github.io)](https://img.shields.io/github/v/release/smtcomp/smtcomp.github.io)
 [![Build status](https://img.shields.io/github/actions/workflow/status/smtcomp/smtcomp.github.io/main.yml?branch=main)](https://github.com/smtcomp/smtcomp.github.io/actions/workflows/main.yml?query=branch%3Amain)
@@ -38,7 +38,7 @@ make install
 
 ## For starting a new SMT-COMP year
 
-Edit the file `smtcomp/defs.py`, in particular `Config.current_year`, `Logic` for adding new logics and `tracks` for new divisions.
+Edit the file `smtcomp/defs.py`, in particular `Config.current_year`, `Logic` for adding new logics and `tracks` for new divisions. Reset `Config.NYSE_seed` to `None`, and set the date the New York Stock Exchange Index will be used in `Config.NYSE_date`.
 
 Download the new benchmarks from zenodo, unpack them, unpack the .tar.zst, you should get something like:
 
@@ -74,10 +74,9 @@ smtcomp create-benchmarks-list $DIR/zenodo ./data/
 
 The directory `./data/` is the one present in this repository.
 
-## Using the smtcomp tool for selecting the benchmarks
+## Using the `smtcomp` tool for selecting the benchmarks
 
-The list of benchmarks and the previous results are in json which are human
-readable, but slow to parse (1min). So locally the tool use the feather format. The
+The list of benchmarks and the previous results are in `json` which are human-readable, but slow to parse (1min). So locally the tool use the feather format. The
 feather files are generated with:
 
 ```
@@ -87,7 +86,7 @@ smtcomp create-cache ./data/
 Working with the feather files with [polars](https://docs.pola.rs/) is very fast,
 so no more intermediate files are needed.
 
-However statistics can be shown, for example for the selection of single track:
+However, statistics can be shown, for example for the selection of single track:
 
 ```
 smtcomp show-sq-selection-stats ./data/ 0
@@ -110,7 +109,7 @@ Which outputs:
 ...
 ```
 
-## Using the smtcomp tool for generating benchexec
+## Using the `smtcomp` tool for generating `benchexec` configuration
 
 #### Generate submissions [Optional]
 

smtcomp/defs.py

@@ -5,50 +5,14 @@
 import re
 from enum import Enum
 from pathlib import Path, PurePath
-from typing import Any, Dict, cast, Optional
+from typing import Any, Dict, cast, Optional, Iterable, TypeVar
 
 from pydantic import BaseModel, Field, RootModel, model_validator, ConfigDict
 from pydantic.networks import HttpUrl, validate_email
+from datetime import date
+from rich import print
 
-
-## Parameters that can change each year
-class Config:
-    current_year = 2024
-    oldest_previous_results = 2018
-    timelimit_s = 60
-    memlimit_M = 1024 * 20
-    cpuCores = 4
-    min_used_benchmarks = 300
-    ratio_of_used_benchmarks = 0.5
-    old_criteria = False
-    """"Do we try to emulate <= 2023 criteria that does not really follow the rules"""
-    invert_triviality = False
-    """Prioritize triviality as much as possible for testing purpose.
-        Look for simple problems instead of hard one"""
-
-    def __init__(self: Config, seed: int | None) -> None:
-        self.__seed = seed
-
-    def seed(self) -> int:
-        if self.__seed is None:
-            raise ValueError("The seed as not been set")
-        s = self.__seed
-        self.__seed = +1
-        return s
-
-
-class DataFiles:
-    def __init__(self, data: Path) -> None:
-        self.previous_results = [
-            (year, 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")
+U = TypeVar("U")
 
 
 class EnumAutoInt(Enum):
@@ -167,6 +131,7 @@ class SolverType(EnumAutoInt):
     wrapped = "wrapped"
     derived = "derived"
     standalone = "Standalone"
+    portfolio = "Portfolio"
 
 
 class Status(EnumAutoInt):
@@ -1225,20 +1190,27 @@ def complete(self, archive: Archive | None, command: Command | None) -> Particip
 import itertools
 
 
+def union(s: Iterable[set[U]]) -> set[U]:
+    return functools.reduce(lambda x, y: x | y, s, set())
+
+
 class Participations(RootModel):
     root: list[Participation]
 
     def get_divisions(self, l: list[Track] = list(Track)) -> set[Division]:
         """ " Return the divisions in which the solver participates"""
         tracks = self.get()
-        divs = [set(tracks[track].keys()) for track in l]
-        return functools.reduce(lambda x, y: x | y, divs)
+        return union(set(tracks[track].keys()) for track in l if track in tracks)
 
     def get_logics(self, l: list[Track] = list(Track)) -> set[Logic]:
         """ " Return the logics in which the solver participates"""
         tracks = self.get()
-        logics = itertools.chain.from_iterable([iter(tracks[track].values()) for track in l])
-        return functools.reduce(lambda x, y: x | y, logics)
+        return union(itertools.chain.from_iterable([tracks[track].values() for track in l if track in tracks]))
+
+    def get_logics_by_track(self) -> dict[Track, set[Logic]]:
+        """Return the logics in which the solver participates"""
+        tracks = self.get()
+        return dict((track, union(tracks[track].values())) for track in tracks)
 
     def get(self, d: None | dict[Track, dict[Division, set[Logic]]] = None) -> dict[Track, dict[Division, set[Logic]]]:
         if d is None:
@@ -1261,6 +1233,7 @@ class Submission(BaseModel, extra="forbid"):
     solver_type: SolverType
     participations: Participations
     seed: int | None = None
+    competitive: bool = True
 
     @model_validator(mode="after")
     def check_archive(self) -> Submission:
@@ -1367,3 +1340,72 @@ class Result(BaseModel):
 
 class Results(BaseModel):
     results: list[Result]
+
+
+## Parameters that can change each year
+class Config:
+    current_year = 2024
+    oldest_previous_results = 2018
+    timelimit_s = 60
+    memlimit_M = 1024 * 20
+    cpuCores = 4
+    min_used_benchmarks = 300
+    ratio_of_used_benchmarks = 0.5
+    old_criteria = False
+    """"Do we try to emulate <= 2023 criteria that does not really follow the rules"""
+    invert_triviality = False
+    """Prioritize triviality as much as possible for testing purpose.
+        Look for simple problems instead of hard one"""
+
+    nyse_seed = None
+    """The integer part of one hundred times the opening value of the New York Stock Exchange Composite Index on the first day the exchange is open on or after the date specified in nyse_date"""
+    nyse_date = date(year=2024, month=6, day=10)
+
+    aws_timelimit_hard = 600
+    """
+    Time in seconds upon which benchmarks are considered hards
+    """
+    aws_num_selected = 400
+    """
+    Number of selected benchmarks
+    """
+
+    def __init__(self, data: Path) -> None:
+        if 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"))
+            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 submissions(self) -> list[Submission]:
+        return [
+            Submission.model_validate_json(Path(file).read_text()) for file in self.data.glob("../submissions/*.json")
+        ]
+
+    @functools.cached_property
+    def seed(self) -> int:
+        unknown_seed = 0
+        seed = 0
+        for s in self.submissions:
+            if s.seed is None:
+                unknown_seed += 1
+            else:
+                seed += s.seed
+        seed = seed % (2**30)
+        if self.nyse_seed is None:
+            print(f"[red]Warning[/red] NYSE seed not set, and {unknown_seed} submissions are missing a seed")
+        else:
+            if unknown_seed > 0:
+                raise ValueError(f"{unknown_seed} submissions are missing a seed")
+            seed += self.nyse_seed
+        return seed

smtcomp/main.py

@@ -80,6 +80,12 @@ def get_contacts(files: list[Path] = typer.Argument(None)) -> None:
     print("\n".join(contacts))
 
 
+@app.command(rich_help_panel=submissions_panel)
+def get_seed(data: Path) -> None:
+    conf = defs.Config(data)
+    print(conf.seed)
+
+
 @app.command(rich_help_panel=submissions_panel)
 def merge_pull_requests_locally(C: str = ".") -> None:
     submission.merge_all_submissions(C)
@@ -189,11 +195,12 @@ def generate_trivial_benchmarks(dst: Path) -> None:
 
 
 @app.command()
-def generate_benchmarks(dst: Path, seed: int = 0) -> None:
+def generate_benchmarks(dst: Path, data: Path) -> None:
     """
     Generate benchmarks for smtcomp
     """
-    smtcomp.generate_benchmarks.generate_benchmarks(dst, seed)
+    config = defs.Config(data)
+    smtcomp.generate_benchmarks.generate_benchmarks(dst, config.seed)
 
 
 @app.command(rich_help_panel=benchmarks_panel)
@@ -232,9 +239,9 @@ def create_benchmarks_list(src: Path, data: Path, scrambler: Optional[Path] = No
         incremental=cast(List[defs.InfoIncremental], files_incremental),
         non_incremental=cast(List[defs.InfoNonIncremental], files_non_incremental),
     )
-    datafiles = defs.DataFiles(data)
+    config = defs.Config(data)
     print("Writing benchmarks file")
-    write_cin(datafiles.benchmarks, benchmarks.model_dump_json(indent=1))
+    write_cin(config.benchmarks, benchmarks.model_dump_json(indent=1))
 
 
 @app.command(rich_help_panel=benchmarks_panel)
@@ -297,11 +304,10 @@ def show_benchmarks_trivial_stats(data: Path, old_criteria: OLD_CRITERIA = False
 
     Never compet.: old benchmarks never run competitively (more than one prover)
     """
-    config = defs.Config(seed=None)
+    config = defs.Config(data)
     config.old_criteria = old_criteria
-    datafiles = defs.DataFiles(data)
-    benchmarks = pl.read_ipc(datafiles.cached_non_incremental_benchmarks)
-    results = pl.read_ipc(datafiles.cached_previous_results)
+    benchmarks = pl.read_ipc(config.cached_non_incremental_benchmarks)
+    results = pl.read_ipc(config.cached_previous_results)
     benchmarks_with_trivial_info = smtcomp.selection.add_trivial_run_info(benchmarks.lazy(), results.lazy(), config)
     b3 = (
         benchmarks_with_trivial_info.group_by(["logic"])
@@ -346,7 +352,6 @@ def show_benchmarks_trivial_stats(data: Path, old_criteria: OLD_CRITERIA = False
 @app.command(rich_help_panel=selection_panel)
 def show_sq_selection_stats(
     data: Path,
-    seed: int,
     old_criteria: OLD_CRITERIA = False,
     min_use_benchmarks: int = defs.Config.min_used_benchmarks,
     ratio_of_used_benchmarks: float = defs.Config.ratio_of_used_benchmarks,
@@ -359,12 +364,12 @@ def show_sq_selection_stats(
 
     Never compet.: old benchmarks never run competitively (more than one prover)
     """
-    config = defs.Config(seed=seed)
+    config = defs.Config(data)
     config.min_used_benchmarks = min_use_benchmarks
     config.ratio_of_used_benchmarks = ratio_of_used_benchmarks
     config.invert_triviality = invert_triviality
     config.old_criteria = old_criteria
-    benchmarks_with_info = smtcomp.selection.helper_compute_sq(data, config)
+    benchmarks_with_info = smtcomp.selection.helper_compute_sq(config)
     b3 = (
         benchmarks_with_info.group_by(["logic"])
         .agg(
@@ -431,9 +436,9 @@ def print_iterable(i: int, tree: Tree, a: Any) -> None:
 
 @app.command(rich_help_panel=data_panel)
 def create_cache(data: Path) -> None:
-    datafiles = defs.DataFiles(data)
+    config = defs.Config(data)
     print("Loading benchmarks")
-    bench = defs.Benchmarks.model_validate_json(read_cin(datafiles.benchmarks))
+    bench = defs.Benchmarks.model_validate_json(read_cin(config.benchmarks))
     bd: Dict[defs.Smt2File, int] = {}
     for i, smtfile in enumerate(
         itertools.chain(map(lambda x: x.file, bench.non_incremental), map(lambda x: x.file, bench.incremental))
@@ -456,7 +461,7 @@ def create_cache(data: Path) -> None:
     df = pl.DataFrame(bench_simplified)
     # df["family"] = df["family"].astype("string")
     # df["name"] = df["name"].astype("string")
-    df.write_ipc(datafiles.cached_non_incremental_benchmarks)
+    df.write_ipc(config.cached_non_incremental_benchmarks)
 
     print("Creating incremental benchmarks cache as feather file")
     bench_simplified = map(
@@ -472,7 +477,7 @@ def create_cache(data: Path) -> None:
     df = pl.DataFrame(bench_simplified)
     # df["family"] = df["family"].astype("string")
     # df["name"] = df["name"].astype("string")
-    df.write_ipc(datafiles.cached_incremental_benchmarks)
+    df.write_ipc(config.cached_incremental_benchmarks)
 
     def convert(x: defs.Result, year: int) -> dict[str, int | str | float] | None:
         if x.file not in bd:
@@ -489,14 +494,14 @@ def convert(x: defs.Result, year: int) -> dict[str, int | str | float] | None:
         }
 
     results_filtered: list[Any] = []
-    for year, file in track(datafiles.previous_results, description="Loading json results"):
+    for year, file in track(config.previous_results, description="Loading json results"):
         results = defs.Results.model_validate_json(read_cin(file))
         results_filtered.extend(filter(lambda x: x is not None, map(lambda r: convert(r, year), results.results)))
 
     print("Creating old results cache as feather file")
     df = pl.DataFrame(results_filtered)
     # df["solver"] = df["solver"].astype("string")
-    df.write_ipc(datafiles.cached_previous_results)
+    df.write_ipc(config.cached_previous_results)
 
 
 # def conv(x:defs.Smt2FileOld) -> defs.Info:
@@ -516,7 +521,6 @@ def select_and_scramble(
     srcdir: Path,
     dstdir: Path,
     scrambler: Path,
-    seed: int,
     max_workers: int = 8,
 ) -> None:
     """
@@ -526,10 +530,8 @@ def select_and_scramble(
     outlined in the data.
     """
 
-    config = defs.Config(seed=seed)
-    smtcomp.scramble_benchmarks.select_and_scramble(
-        competition_track, data, config, srcdir, dstdir, scrambler, max_workers
-    )
+    config = defs.Config(data)
+    smtcomp.scramble_benchmarks.select_and_scramble(competition_track, config, srcdir, dstdir, scrambler, max_workers)
 
 
 @app.command()