From c0de3304829c973a5aa31cb10ef879ba9a15c40c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Thu, 13 Jun 2024 09:48:38 +0200 Subject: [PATCH 01/25] Cleanup useful function --- smtcomp/main.py | 62 ------------------------------------------------- 1 file changed, 62 deletions(-) diff --git a/smtcomp/main.py b/smtcomp/main.py index b0e8a0c0..d84c05cd 100644 --- a/smtcomp/main.py +++ b/smtcomp/main.py @@ -323,58 +323,6 @@ def merge_benchmarks(files: list[Path], dst: Path) -> None: OLD_CRITERIA = Annotated[bool, typer.Option(help="Simulate previous year criteria (needs only to be trivial one year)")] -@app.command(rich_help_panel=selection_panel) -def show_benchmarks_trivial_stats(data: Path, old_criteria: OLD_CRITERIA = False) -> None: - """ - Show statistics on the trivial benchmarks - - Never compet.: old benchmarks never run competitively (more than one prover) - """ - config = defs.Config(data) - config.old_criteria = old_criteria - 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"]) - .agg( - trivial=pl.col("file").filter(trivial=True).len(), - not_trivial=pl.col("file").filter(trivial=False, run=True).len(), - old_never_ran=pl.col("file").filter(run=False, new=False).len(), - new=pl.col("file").filter(new=True).len(), - ) - .sort(by="logic") - .collect() - ) - table = Table(title="Statistics on the benchmark pruning") - - table.add_column("Logic", justify="left", style="cyan", no_wrap=True) - table.add_column("trivial", justify="right", style="green") - table.add_column("not trivial", justify="right", style="orange_red1") - table.add_column("never compet.", justify="right", style="magenta") - table.add_column("new", justify="right", style="magenta1") - - for d in b3.to_dicts(): - table.add_row( - str(defs.Logic.of_int(d["logic"])), - str(d["trivial"]), - str(d["not_trivial"]), - str(d["old_never_ran"]), - str(d["new"]), - ) - - table.add_section() - table.add_row( - "Total", - str(b3["trivial"].sum()), - str(b3["not_trivial"].sum()), - str(b3["old_never_ran"].sum()), - str(b3["new"].sum()), - ) - - print(table) - - @app.command(rich_help_panel=selection_panel) def show_sq_selection_stats( data: Path, @@ -540,16 +488,6 @@ def convert(x: defs.Result, year: int) -> dict[str, int | str | float] | None: df.write_ipc(config.cached_previous_results) -# 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)) - - @app.command(rich_help_panel=benchexec_panel) def select_and_scramble( competition_track: defs.Track, From 3490e173823d3a3e02cc4fec94ef09cdad5014c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Thu, 13 Jun 2024 09:49:08 +0200 Subject: [PATCH 02/25] Fix generate-benchmark for unsat-core --- smtcomp/generate_benchmarks.py | 27 +++++++++++---------------- 1 file changed, 11 insertions(+), 16 deletions(-) diff --git a/smtcomp/generate_benchmarks.py b/smtcomp/generate_benchmarks.py index c9cddaaf..cc7e3db3 100644 --- a/smtcomp/generate_benchmarks.py +++ b/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(): @@ -88,6 +84,9 @@ def generate_trivial_benchmarks(dst: Path) -> None: def generate_benchmarks(dst: Path, seed: int) -> None: + """ + Generate files included by benchexec + """ prop_dir = dst.joinpath("properties") prop_dir.mkdir(parents=True, exist_ok=True) (prop_dir / "SMT.prp").touch() @@ -96,12 +95,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(): From c2aabb79269d3279e212fbe7a2dab2d31f7bcf78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Thu, 13 Jun 2024 10:30:39 +0200 Subject: [PATCH 03/25] Cleanup main.py by moving code to respective file --- smtcomp/archive.py | 14 +++++++++++++ smtcomp/benchexec.py | 35 +++++++++++++++++++++++++------- smtcomp/defs.py | 42 +++++++++++++++++++++++++++----------- smtcomp/main.py | 48 +++++++++----------------------------------- 4 files changed, 81 insertions(+), 58 deletions(-) diff --git a/smtcomp/archive.py b/smtcomp/archive.py index 8e6e35fb..426c34b9 100644 --- a/smtcomp/archive.py +++ b/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) diff --git a/smtcomp/benchexec.py b/smtcomp/benchexec.py index 2b55e375..c70b9bc9 100644 --- a/smtcomp/benchexec.py +++ b/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('') @@ -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,26 @@ 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, + ]: + tool_module_name = tool_module_name(s, target_track == defs.Track.Incremental) + + 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, + ) diff --git a/smtcomp/defs.py b/smtcomp/defs.py index 1474ae7b..a37de822 100644 --- a/smtcomp/defs.py +++ b/smtcomp/defs.py @@ -1374,21 +1374,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]: diff --git a/smtcomp/main.py b/smtcomp/main.py index d84c05cd..4f55dd58 100644 --- a/smtcomp/main.py +++ b/smtcomp/main.py @@ -17,6 +17,7 @@ import smtcomp.archive as archive import smtcomp.benchexec as benchexec +import smtcomp.benchexec import smtcomp.defs as defs import smtcomp.submission as submission import smtcomp.execution as execution @@ -160,46 +161,15 @@ def generate_benchexec( (The cachedir directory need to contain unpacked archive only with compa_starexec command) """ + config = defs.Config(data=None) + config.timelimit_s = timelimit_s + config.memlimit_M = memlimit_M + config.cpuCores = cpuCores + (cachedir / "tools").mkdir(parents=True, exist_ok=True) for file in track(files): s = submission.read(str(file)) - benchexec.generate_tool_modules(s, cachedir) - - for target_track in [ - defs.Track.SingleQuery, - defs.Track.Incremental, - defs.Track.ModelValidation, - defs.Track.UnsatCore, - ]: - tool_module_name = benchexec.tool_module_name(s, target_track == defs.Track.Incremental) - - res = benchexec.cmdtask_for_submission(s, cachedir, target_track) - if res: - basename = benchexec.get_xml_name(s, target_track) - file = cachedir / basename - benchexec.generate_xml( - timelimit_s=timelimit_s, - memlimit_M=memlimit_M, - cpuCores=cpuCores, - cmdtasks=res, - file=file, - tool_module_name=tool_module_name, - ) - - -# Should be moved somewhere else -def download_archive_aux(s: defs.Submission, dst: Path) -> None: - """ - Download and unpack - """ - dst.mkdir(parents=True, exist_ok=True) - if s.archive: - archive.download(s.archive, dst) - archive.unpack(s.archive, dst) - for p in s.participations.root: - if p.archive: - archive.download(p.archive, dst) - archive.unpack(p.archive, dst) + smtcomp.benchexec.generate(s, cachedir, config) @app.command(rich_help_panel=benchexec_panel) @@ -209,7 +179,7 @@ def download_archive(files: List[Path], dst: Path) -> None: """ for file in track(files): s = submission.read(str(file)) - download_archive_aux(s, dst) + archive.download_unpack(s, dst) @app.command() @@ -541,7 +511,7 @@ def read_submission(file: Path) -> defs.Submission: out.write("""print("Testing provers")\n""") for sub in l: out.write(f"print({sub.name!r})\n") - download_archive_aux(sub, outdir) + archive.download_unpack(sub, outdir) for part in sub.complete_participations(): for track, divisions in part.tracks.items(): match track: From fee7c10b9f09ccd4d87570a1d0878e426c0876c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Thu, 13 Jun 2024 10:49:31 +0200 Subject: [PATCH 04/25] Make command take the same cachedir as argument - generate-benchmarks do not need "benchmark" added - select-and-scramble do not need "benchmark/files$suffix" added --- smtcomp/benchexec.py | 4 +--- smtcomp/generate_benchmarks.py | 3 ++- smtcomp/main.py | 9 ++++----- smtcomp/scramble_benchmarks.py | 6 ++++-- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/smtcomp/benchexec.py b/smtcomp/benchexec.py index c70b9bc9..30a333ef 100644 --- a/smtcomp/benchexec.py +++ b/smtcomp/benchexec.py @@ -189,8 +189,6 @@ def generate(s: defs.Submission, cachedir: Path, config: defs.Config) -> None: defs.Track.ModelValidation, defs.Track.UnsatCore, ]: - tool_module_name = tool_module_name(s, target_track == defs.Track.Incremental) - res = cmdtask_for_submission(s, cachedir, target_track) if res: basename = get_xml_name(s, target_track) @@ -199,5 +197,5 @@ def generate(s: defs.Submission, cachedir: Path, config: defs.Config) -> None: config=config, cmdtasks=res, file=file, - tool_module_name=tool_module_name, + tool_module_name=tool_module_name(s, target_track == defs.Track.Incremental), ) diff --git a/smtcomp/generate_benchmarks.py b/smtcomp/generate_benchmarks.py index cc7e3db3..68d6eb83 100644 --- a/smtcomp/generate_benchmarks.py +++ b/smtcomp/generate_benchmarks.py @@ -83,10 +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() diff --git a/smtcomp/main.py b/smtcomp/main.py index 4f55dd58..0de23773 100644 --- a/smtcomp/main.py +++ b/smtcomp/main.py @@ -191,12 +191,11 @@ def generate_trivial_benchmarks(dst: Path) -> None: @app.command() -def generate_benchmarks(dst: Path, data: Path) -> None: +def generate_benchmarks(cachedir: Path) -> None: """ Generate benchmarks for smtcomp """ - config = defs.Config(data) - smtcomp.generate_benchmarks.generate_benchmarks(dst, config.seed) + smtcomp.generate_benchmarks.generate_benchmarks(cachedir) @app.command(rich_help_panel=benchmarks_panel) @@ -463,7 +462,7 @@ def select_and_scramble( competition_track: defs.Track, data: Path, srcdir: Path, - dstdir: Path, + cachedir: Path, scrambler: Path, max_workers: int = 8, test: bool = False, @@ -483,7 +482,7 @@ def select_and_scramble( config.invert_triviality = True config.seed = 1 - smtcomp.scramble_benchmarks.select_and_scramble(competition_track, config, srcdir, dstdir, scrambler, max_workers) + smtcomp.scramble_benchmarks.select_and_scramble(competition_track, config, srcdir, cachedir, scrambler, max_workers) @app.command() diff --git a/smtcomp/scramble_benchmarks.py b/smtcomp/scramble_benchmarks.py index d579cdd8..369b2767 100644 --- a/smtcomp/scramble_benchmarks.py +++ b/smtcomp/scramble_benchmarks.py @@ -4,7 +4,7 @@ import subprocess import concurrent.futures import smtcomp.defs as defs -from smtcomp.benchexec import generate_benchmark_yml +from smtcomp.benchexec import generate_benchmark_yml, get_suffix import polars as pl import smtcomp.selection from typing import Optional @@ -143,10 +143,12 @@ def select_and_scramble( competition_track: defs.Track, config: defs.Config, srcdir: Path, - dstdir: Path, + cachedir: Path, scrambler: Path, max_workers: int, ) -> None: + suffix = get_suffix(competition_track) + dstdir = cachedir / "benchmarks" / f"files{suffix}" match competition_track: case defs.Track.SingleQuery: selected = smtcomp.selection.helper_compute_sq(config) From 75d5844290869b6be750e84cdc5efc7c90600715 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Thu, 13 Jun 2024 11:41:06 +0200 Subject: [PATCH 05/25] Remove test function the duplication of code seems dangerous --- smtcomp/scramble_benchmarks.py | 39 ---------------------------------- 1 file changed, 39 deletions(-) diff --git a/smtcomp/scramble_benchmarks.py b/smtcomp/scramble_benchmarks.py index 369b2767..7ea8166b 100644 --- a/smtcomp/scramble_benchmarks.py +++ b/smtcomp/scramble_benchmarks.py @@ -100,45 +100,6 @@ def scramble_lazyframe( ) -def test_select_and_scramble( - competition_track: defs.Track, - config: defs.Config, - srcdir: Path, - dstdir: Path, - scrambler: Path, - max_workers: int, -) -> None: - match competition_track: - case defs.Track.SingleQuery: - selected = smtcomp.selection.helper_compute_sq(config) - case defs.Track.Incremental: - selected = pl.read_ipc(config.cached_incremental_benchmarks).lazy() - # rich.print( - # f"[red]The scramble_benchmarks command does not yet work for the competition track: {competition_track}[/red]" - # ) - # exit(1) - case defs.Track.ModelValidation: - selected = smtcomp.selection.helper_compute_sq(config) - rich.print( - f"[red]The scramble_benchmarks command does not yet work for the competition track: {competition_track}[/red]" - ) - exit(1) - case defs.Track.UnsatCore: - selected = smtcomp.selection.helper_compute_sq(config) - rich.print( - f"[red]The scramble_benchmarks command does not yet work for the competition track: {competition_track}[/red]" - ) - exit(1) - case defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel: - selected = smtcomp.selection.helper_compute_sq(config) - rich.print( - f"[red]The scramble_benchmarks command does not yet work for the competition track: {competition_track}[/red]" - ) - exit(1) - selected = create_scramble_id(selected, config).filter(pl.col("logic") == int(defs.Logic.BVFP)) - scramble_lazyframe(selected, competition_track, config, srcdir, dstdir, scrambler, max_workers) - - def select_and_scramble( competition_track: defs.Track, config: defs.Config, From d44734e24c5c8315ee900c1f1bdc658cdc19df53 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Thu, 13 Jun 2024 11:41:46 +0200 Subject: [PATCH 06/25] Create directory for scramble destination --- smtcomp/scramble_benchmarks.py | 1 + 1 file changed, 1 insertion(+) diff --git a/smtcomp/scramble_benchmarks.py b/smtcomp/scramble_benchmarks.py index 7ea8166b..ebd24c1d 100644 --- a/smtcomp/scramble_benchmarks.py +++ b/smtcomp/scramble_benchmarks.py @@ -110,6 +110,7 @@ def select_and_scramble( ) -> None: suffix = get_suffix(competition_track) dstdir = cachedir / "benchmarks" / f"files{suffix}" + dstdir.mkdir(parents=True, exist_ok=True) match competition_track: case defs.Track.SingleQuery: selected = smtcomp.selection.helper_compute_sq(config) From 479af4f9e6d57d88b2c81cf303c0c48640a63de9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Thu, 13 Jun 2024 11:42:33 +0200 Subject: [PATCH 07/25] Create original_id.csv file during scrambling --- smtcomp/scramble_benchmarks.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/smtcomp/scramble_benchmarks.py b/smtcomp/scramble_benchmarks.py index ebd24c1d..31d83e68 100644 --- a/smtcomp/scramble_benchmarks.py +++ b/smtcomp/scramble_benchmarks.py @@ -70,7 +70,9 @@ def scramble_lazyframe( max_workers: int, ) -> None: args = [] - files = benchmarks.select("scramble_id", "logic", "family", "name").collect().to_dicts() + df = benchmarks.select("scramble_id", "logic", "family", "name", "file").collect() + df.select("scramble_id", "file").write_csv(dstdir / "original_id.csv") + files = df.to_dicts() incremental = False seed = config.seed From 15b7725fc2277f67179f5e447f22670ff3b0f3ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Thu, 13 Jun 2024 17:03:18 +0200 Subject: [PATCH 08/25] Allow to check model locally. --- smtcomp/main.py | 18 ++++++- smtcomp/model_validation.py | 92 ++++++++++++++++++++++++++++++++++ smtcomp/results.py | 4 ++ smtcomp/scramble_benchmarks.py | 9 +++- 4 files changed, 120 insertions(+), 3 deletions(-) create mode 100644 smtcomp/model_validation.py diff --git a/smtcomp/main.py b/smtcomp/main.py index 0de23773..8e38b0a5 100644 --- a/smtcomp/main.py +++ b/smtcomp/main.py @@ -3,7 +3,7 @@ from pathlib import Path from typing import List, Optional, cast, Dict, Any, Annotated, TextIO import rich -from rich.progress import track +from rich.progress import track, Progress import rich.style from rich.tree import Tree from rich.table import Table @@ -21,6 +21,8 @@ import smtcomp.defs as defs import smtcomp.submission as submission import smtcomp.execution as execution +import smtcomp.model_validation as model_validation +import smtcomp.results as results from smtcomp.benchmarks import clone_group import smtcomp.convert_csv import smtcomp.generate_benchmarks @@ -30,6 +32,7 @@ import smtcomp.scramble_benchmarks from rich.console import Console import smtcomp.test_solver as test_solver +from concurrent.futures import ThreadPoolExecutor app = typer.Typer() @@ -545,3 +548,16 @@ def read_submission(file: Path) -> defs.Submission: f"test({str(cmd)!r},{part.command.arguments!r},{str(file_sat)!r},{expected!r})\n" ) out.write("end()\n") + + +@app.command() +def check_model_locally(cachedir: Path, resultdirs: list[Path], max_workers: int = 8) -> None: + l: list[tuple[results.RunId, results.Run, model_validation.ValidationResult]] = [] + with Progress() as progress: + with ThreadPoolExecutor(max_workers) as executor: + for resultdir in resultdirs: + l2 = model_validation.check_results_locally(cachedir, resultdir, executor, progress) + for rid, r, result in l2: + if result.status != defs.Status.Sat: + l.append((rid, r, result)) + print(l) diff --git a/smtcomp/model_validation.py b/smtcomp/model_validation.py new file mode 100644 index 00000000..f553a51a --- /dev/null +++ b/smtcomp/model_validation.py @@ -0,0 +1,92 @@ +from dataclasses import dataclass +from pathlib import Path +import smtcomp.defs as defs +import subprocess +import smtcomp.results as results +from smtcomp.benchexec import get_suffix +from smtcomp.scramble_benchmarks import benchmark_files_dir +from concurrent.futures import ThreadPoolExecutor +from rich.progress import Progress + + +# ./dolmen --time=1h --size=40G --strict=false --check-model=true --report-style=minimal "$2" < "$1" &> error.txt +# EXITSTATUS=$? + +# if [ "$EXITSTATUS" = "0" ]; then +# echo "starexec-result=sat" +# echo "model_validator_status=VALID" +# elif [ "$EXITSTATUS" = "2" ]; then +# echo "starexec-result=unknown" +# echo "model_validator_status=LIMITREACHED" +# elif [ "$EXITSTATUS" = "5" ]; then +# echo "starexec-result=unsat" +# echo "model_validator_status=INVALID" +# else +# echo "starexec-result=unknown" +# echo "model_validator_status=UNKNOWN" +# fi +# echo "dolmenexit=$EXITSTATUS" +# if grep -q '^[EF]:' error.txt; then +# echo "model_validator_error="$(grep '^[EF]:' error.txt | head -1) +# fi +# exit 0 + + +@dataclass +class ValidationResult: + status: defs.Status + stderr: str + + +def check_locally(smt2_file: Path, model: str) -> ValidationResult: + r = subprocess.run( + [ + "dolmen", + "--time=1h", + "--size=40G", + "--strict=false", + "--check-model=true", + "--report-style=minimal", + smt2_file, + ], + input=model.encode(), + capture_output=True, + ) + match r.returncode: + case 0: + status = defs.Status.Sat + case 5: + status = defs.Status.Unsat + case 2: + # LimitReached + status = defs.Status.Unknown + case _: + status = defs.Status.Unknown + return ValidationResult(status, r.stderr.decode()) + + +def check_result_locally( + cachedir: Path, logfiles: results.LogFile, rid: results.RunId, r: results.Run +) -> ValidationResult: + if r.status == "true": + filedir = benchmark_files_dir(cachedir, rid.track) + logic = rid.includefile.removesuffix(get_suffix(rid.track)) + smt2_file = filedir / logic / (r.basename.removesuffix(".yml") + ".smt2") + model = logfiles.get_output(rid, r.basename) + return check_locally(smt2_file, model) + else: + return ValidationResult(defs.Status.Unknown, "") + + +def check_results_locally( + cachedir: Path, resultdir: Path, executor: ThreadPoolExecutor, progress: Progress +) -> list[tuple[results.RunId, results.Run, ValidationResult]]: + with results.LogFile(resultdir) as logfiles: + l = [(r.runid, b) for r in results.parse_results(resultdir) for b in r.runs if b.status == "true"] + return list( + progress.track( + executor.map((lambda v: (v[0], v[1], check_result_locally(cachedir, logfiles, v[0], v[1]))), l), + total=len(l), + description="checking models", + ) + ) diff --git a/smtcomp/results.py b/smtcomp/results.py index 1adacf6d..975cb666 100644 --- a/smtcomp/results.py +++ b/smtcomp/results.py @@ -129,6 +129,10 @@ def parse_xml(file: Path) -> Results: return Results(runid=RunId.unmangle(result.attrib["name"]), options=result.attrib["options"], runs=runs) +def parse_results(resultdir: Path) -> Iterator[Results]: + return map(parse_xml, (resultdir.glob("*.xml.bz2"))) + + def to_pl(r: Results) -> pl.LazyFrame: lf = pl.LazyFrame(r.runs) return lf.with_columns(solver=pl.lit(r.runid.solver), participation=r.runid.participation, track=int(r.runid.track)) diff --git a/smtcomp/scramble_benchmarks.py b/smtcomp/scramble_benchmarks.py index 31d83e68..959f78b0 100644 --- a/smtcomp/scramble_benchmarks.py +++ b/smtcomp/scramble_benchmarks.py @@ -10,6 +10,12 @@ from typing import Optional import re + +def benchmark_files_dir(cachedir: Path, track: defs.Track) -> Path: + suffix = get_suffix(track) + return cachedir / "benchmarks" / f"files{suffix}" + + status_pattern = re.compile(r"(set-info :status (sat|unsat|unknown))") @@ -110,8 +116,7 @@ def select_and_scramble( scrambler: Path, max_workers: int, ) -> None: - suffix = get_suffix(competition_track) - dstdir = cachedir / "benchmarks" / f"files{suffix}" + dstdir = benchmark_files_dir(cachedir, competition_track) dstdir.mkdir(parents=True, exist_ok=True) match competition_track: case defs.Track.SingleQuery: From 0fabdbbe3e419d32e03c7ad773178145cd3ef0be Mon Sep 17 00:00:00 2001 From: Amar Shah Date: Tue, 18 Jun 2024 08:33:50 +0200 Subject: [PATCH 09/25] Adding Algaroba to SMTCOMP 2024 (#42) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Adding algaroba.json * Added the solver type "wrapped" * Adding link to solver executable * Adding executable compiled in Docker environment * Added statically linked executable --------- Co-authored-by: François Bobot --- submissions/algaroba.json | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 submissions/algaroba.json diff --git a/submissions/algaroba.json b/submissions/algaroba.json new file mode 100644 index 00000000..3c330242 --- /dev/null +++ b/submissions/algaroba.json @@ -0,0 +1,19 @@ +{ + "name": "Algaroba", + "contributors": [ + { "name": "Amar Shah", "website": "https://amarshah1.github.io/" }, + { "name": "Federico Mora", "website": "https://federico.morarocha.ca/" }, + { "name": "Sanjit Seshia", "website": "https://people.eecs.berkeley.edu/~sseshia/" } + ], + "contacts": ["Amar Shah "], + "archive": { + "url": "https://github.com/user-attachments/files/15844330/algaroba.tar.gz" + }, + "website": "https://github.com/uclid-org/algaroba", + "system_description": "https://github.com/uclid-org/algaroba/files/15255360/Algaroba_at_the_2024_SMTCOMP.pdf", + "command": ["algaroba/algaroba.exe"], + "solver_type": "wrapped", + "participations": [ + { "tracks": ["SingleQuery"], "logics": ["QF_DT", "QF_UFDT"], "divisions": ["QF_Datatypes"] } + ] +} From 91ed77f4afc49dfc5c13cb75179179eb21c20793 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 18 Jun 2024 08:34:16 +0200 Subject: [PATCH 10/25] Submission for smtinterpol (#45) * Create smtinterpol Draft for the smtinterpol submission. * Updated links * trim trailing whitespace * Add bitvector logics * Added seed * Updated run script, fixed paths * Updated submission - New version uploaded - Added Contact - Added new BV logics to model-validation track * Added BV logics to model-validation * Updated binary --- submissions/smtinterpol.json | 55 ++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 submissions/smtinterpol.json diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json new file mode 100644 index 00000000..6ee63061 --- /dev/null +++ b/submissions/smtinterpol.json @@ -0,0 +1,55 @@ +{ + "name": "SMTInterpol", + "contributors": [ + "Max Barth", "Leon Cacace", + "Jürgen Christ", "Daniel Dietsch", "Leonard Fichtner", + "Joanna Greulich", "Elisabeth Henkel", "Matthias Heizmann", + "Jochen Hoenicke", "Moritz Mohr", "Alexander Nutz", + "Markus Pomrehn", "Pascal Raiola", "Tanja Schindler" + ], + "contacts": [ + "Max Barth ", + "Jochen Hoenicke " + ], + "archive": { + "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1381-g0e9bd0bf.tar.gz", + "h": { "sha256": "3616fff7345b8ef9b12e488d4757bffb487fef3cd118737ede67f22382877c2e" } + }, + "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", + "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2024.pdf", + "command": ["smtinterpol"], + "solver_type": "Standalone", + "seed": "4223469823", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + }, + { + "tracks": ["SingleQuery"], + "logics": "(QF_)?(AX?)?(UF)?BV(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol-bv"] + }, + { + "tracks": ["Incremental"], + "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + }, + { + "tracks": ["Incremental"], + "logics": "(QF_)?(AX?)?(UF)?BV(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol-bv"] + }, + { + "tracks": ["ModelValidation"], + "logics": "(QF_)(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + }, + { + "tracks": ["UnsatCore"], + "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + } + ] +} From 5dd9ca19ae1b20d20f1e5139e23cbcc998f9ce05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Tue, 18 Jun 2024 10:36:52 +0400 Subject: [PATCH 11/25] Submission Colibri (#51) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * COLIBRI submission * [COLIBRI] Fix url --------- Co-authored-by: Martin Jonáš <359542@mail.muni.cz> --- submissions/COLIBRI.json | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 submissions/COLIBRI.json diff --git a/submissions/COLIBRI.json b/submissions/COLIBRI.json new file mode 100644 index 00000000..4daeb6a7 --- /dev/null +++ b/submissions/COLIBRI.json @@ -0,0 +1,21 @@ +{ + "name": "COLIBRI", + "contributors": [ + "Bruno Marre", "François Bobot", "Christophe Junke" + ], + "contacts": ["Christophe Junke "], + "archive": { + "url": "https://drive.google.com/uc?export=download&id=1lJjQNgHRF14sGEW84eJ6tBsZ0-DBPMW2", + "h": { "sha256": "829fb89fc4a61dbc3180f400d75a283e967fef9c910ce4404a824608fb0b1c58" } + }, + "website": "http://colibri.frama-c.com/", + "system_description": "https://drive.google.com/file/d/13c5E0iNMvpTRjmhWKb286V25Dw4f6JOF/view?usp=sharing", + "command": ["smtcomp_2024/bin/starexec_run_default"], + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": "QF_.*FP.*" + } + ] +} From be94528d02c5292015a8239e31b5f88f074b9f33 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Juraj=20S=C3=AD=C4=8D?= Date: Tue, 18 Jun 2024 08:37:08 +0200 Subject: [PATCH 12/25] Z3-Noodler submission (#52) * Create z3-noodler.json * fix trailing commas * change to archive with binary * update command * fix download link + add seed number --- submissions/z3-noodler.json | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 submissions/z3-noodler.json diff --git a/submissions/z3-noodler.json b/submissions/z3-noodler.json new file mode 100644 index 00000000..b7c93bb2 --- /dev/null +++ b/submissions/z3-noodler.json @@ -0,0 +1,22 @@ +{ + "name": "Z3-Noodler", + "contributors": [ + "Vojtěch Havlena", + "Juraj Síč", + "David Chocholatý", + "Lukáš Holík", + "Ondřej Lengál" + ], + "contacts": ["Lukáš Holík "], + "archive": { + "url": "https://drive.google.com/uc?export=download&id=1XSj2PiVJLDx-JQyJRt76OEloC0dWFJqH" + }, + "website": "https://github.com/VeriFIT/z3-noodler", + "system_description": "https://github.com/VeriFIT/z3-noodler/blob/devel/doc/noodler/z3-noodler-system-description-2024.pdf", + "command": ["z3-noodler_linux", "smt.string_solver=noodler"], + "solver_type": "derived", + "participations": [ + { "tracks": ["SingleQuery"], "divisions": ["QF_Strings"] } + ], + "seed": 1465867 +} From 51e53cfbf20fab08ab7fc21ca66c4f9b080fa275 Mon Sep 17 00:00:00 2001 From: Tomaqa Date: Tue, 18 Jun 2024 08:37:25 +0200 Subject: [PATCH 13/25] 2024 solver participant submission: OpenSMT (#53) --- submissions/opensmt.json | 44 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 submissions/opensmt.json diff --git a/submissions/opensmt.json b/submissions/opensmt.json new file mode 100644 index 00000000..837e587d --- /dev/null +++ b/submissions/opensmt.json @@ -0,0 +1,44 @@ +{ + "name": "OpenSMT", + "contributors": [ + { "name": "Tomáš Kolárik", "website": "https://github.com/Tomaqa" } + , + { "name": "Martin Blicha", "website": "https://github.com/blishko" } + ], + "contacts": [ + "Tomáš Kolárik " + , + "Martin Blicha " + ], + "archive": { + "url": "https://zenodo.org/records/11371847/files/opensmt.tgz" + , + "h": { "sha256": "f42b6f25012344f76886305d3177eda610999508224135445bb119582d12b30c" } + }, + "command": ["./opensmt"], + "website": "https://github.com/usi-verification-and-security/opensmt", + "system_description": "https://github.com/usi-verification-and-security/opensmt-doc/blob/master/smt-comp/abstract-2024.pdf", + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["SingleQuery", "Incremental", "UnsatCore"], + "logics": [ + "QF_UF", "QF_AX", + "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", + "QF_UFIDL", "QF_UFLIA", "QF_UFLRA", + "QF_ALIA", + "QF_AUFLIA" + ] + } + , + { + "tracks": ["ModelValidation"], + "logics": [ + "QF_UF", + "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", + "QF_UFIDL", "QF_UFLIA", "QF_UFLRA" + ] + } + ], + "seed": 13 +} From 1dbe5247189c2efbc2ef7faacd49aa05a5771b88 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 17 Jun 2024 23:37:41 -0700 Subject: [PATCH 14/25] Add 2024 Bitwuzla submission. (#54) * Add 2024 Bitwuzla submission. * Update submission. * Add seed. * Fix. * Try. * Update submission. * Fix download link. * Update. * Update. * Update. --- submissions/bitwuzla.json | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 submissions/bitwuzla.json diff --git a/submissions/bitwuzla.json b/submissions/bitwuzla.json new file mode 100644 index 00000000..594f4f43 --- /dev/null +++ b/submissions/bitwuzla.json @@ -0,0 +1,39 @@ +{ + "name": "Bitwuzla", + "contributors": ["Aina Niemetz", "Mathias Preiner"], + "contacts": ["Mathias Preiner "], + + "archive": { + "url": "https://zenodo.org/records/11754739/files/bitwuzla-submission-smtcomp-2024.zip?download=1", + "h": {"sha256": "f5bbe44bc12465ed2e1be9512d8b9a9f2bb9f8f16d1bd2bbef0f348e659a6e4d"} + }, + + "command": ["bin/bitwuzla"], + + "website": "https://bitwuzla.github.io", + "system_description": "https://bitwuzla.github.io/data/smtcomp2024/paper.pdf", + "solver_type": "Standalone", + "seed": "42", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--abstraction", "--abstraction-bv-size=33"] + }, + { + "tracks": ["Incremental"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--no-pp-normalize"] + }, + { + "tracks": ["UnsatCore"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--abstraction", "--abstraction-bv-size=33"] + }, + { + "tracks": ["ModelValidation"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--abstraction", "--abstraction-bv-size=33"] + } + ] +} From 5273d55004b8c70823bd2a329e7cd4fcab19aa94 Mon Sep 17 00:00:00 2001 From: David Ewert <33990711+dewert99@users.noreply.github.com> Date: Mon, 17 Jun 2024 23:38:09 -0700 Subject: [PATCH 15/25] plat-smt submission (#55) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Create plat-smt * Update plat-smt * Add .json extension to plat-smt * fix trailing comman in plat-smt.json * Fix plat-smt.json * Update plat-smt.json * Fix plat-smt.json logics * Update plat-smt.json Fix incremental issue --------- Co-authored-by: François Bobot --- submissions/plat-smt.json | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 submissions/plat-smt.json diff --git a/submissions/plat-smt.json b/submissions/plat-smt.json new file mode 100644 index 00000000..79b01aa8 --- /dev/null +++ b/submissions/plat-smt.json @@ -0,0 +1,35 @@ +{ + "name": "plat-smt", + "contributors": [ + "David Ewert" + ], + "contacts": ["David Ewert "], + "archive": { + "url": "https://github.com/dewert99/plat-smt/releases/download/SMT-COMP2024-v2/plat-smt.zip", + "h": { "sha256": "6f209d0fe11e3aca548a769d39cf5bb8294fda64e3a3667514246ec2b3d95966" } + }, + "website": "https://github.com/dewert99/plat-smt", + "system_description": "https://github.com/user-attachments/files/15831637/PlatSMT_2024_System_Description.pdf", + "command": ["./plat-smt"], + "solver_type": "wrapped", + "seed": 6536, + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": ["QF_UF"] + }, + { + "tracks": ["Incremental"], + "logics": ["QF_UF"], + "command": ["./plat-smt", "-i"] + }, + { + "tracks": ["UnsatCore"], + "logics": ["QF_UF"] + }, + { + "tracks": ["ModelValidation"], + "logics": ["QF_UF"] + } + ] +} From e8e4994fec3342a458925f5db7a69b9f02a7f883 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ondra=20Leng=C3=A1l?= Date: Tue, 18 Jun 2024 08:38:26 +0200 Subject: [PATCH 16/25] Amaya's submission for SMT-COMP 2024 (#57) * copy template * finish initial PR * typo * fix archive * add seed * fixing symlinks * change called script * input format fix * output format * fix behaviour on NIA - return unknown * remove Arith * change to Zenodo --- submissions/Amaya.json | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 submissions/Amaya.json diff --git a/submissions/Amaya.json b/submissions/Amaya.json new file mode 100644 index 00000000..b112b506 --- /dev/null +++ b/submissions/Amaya.json @@ -0,0 +1,22 @@ +{ + "name": "Amaya", + "contributors": [ + "Vojtěch Havlena", "Michal Hečko", "Lukáš Holík", "Ondřej Lengál" + ], + "contacts": ["Michal Hečko ", "Ondřej Lengál "], + "archive": { + "url": "https://zenodo.org/records/11625128/files/amaya-smt-comp-2024-v6.tar.gz", + "h": { "sha256": "5a2e5051741fa5ab1110bb5829304301f222e3aa23e2124fb8ad4e07041bc630" } + }, + "website": "https://github.com/MichalHe/amaya", + "system_description": "https://github.com/VeriFIT/amaya-smt-comp/blob/master/system-description-2024/main.pdf", + "command": ["amaya/run.sh"], + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": ["LIA", "NIA"] + } + ], + "seed": "1337001337" +} From 0e0c955a3a94ceac842e54ae90615d0dda8a3e4a Mon Sep 17 00:00:00 2001 From: ValentinPromies <44966217+ValentinPromies@users.noreply.github.com> Date: Tue, 18 Jun 2024 08:38:40 +0200 Subject: [PATCH 17/25] SMT-RAT submission (#60) * smtrat submission * Remove trailing comma * add seed * update solver --- submissions/smtrat.json | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 submissions/smtrat.json diff --git a/submissions/smtrat.json b/submissions/smtrat.json new file mode 100644 index 00000000..f5a82b9d --- /dev/null +++ b/submissions/smtrat.json @@ -0,0 +1,21 @@ +{ + "name": "SMT-RAT", + "contributors": [ + "Jasper Nalbach", + "Valentin Promies", + "Erika Ábrahám" + ], + "contacts": ["Jasper Nalbach ", "Valentin Promies "], + "archive": { + "url": "https://github.com/ths-rwth/smtrat/releases/download/24.06/smtrat.tgz" + }, + "website": "https://github.com/ths-rwth/smtrat", + "system_description": "https://github.com/ths-rwth/smtrat/blob/master/doc/smtcomp-description/smtcomp-2024.pdf", + "command": [ "./smtrat" ], + "solver_type": "Standalone", + "seed": 174228, + "participations": [ + { "tracks": ["SingleQuery"], "logics": "(QF_)?NRA" }, + { "tracks": ["ModelValidation"], "logics": "QF_NRA" } + ] +} From a3bf6f1a0b73a83e0c85be76dd9be6cc56fe4f3a Mon Sep 17 00:00:00 2001 From: Philipp Ruemmer Date: Tue, 18 Jun 2024 08:38:57 +0200 Subject: [PATCH 18/25] OSTRICH 1.4 (#61) * Create ostrich.json * Update ostrich.json * Update ostrich.json * Update ostrich.json * Update ostrich.json * Update ostrich.json Fixed command line --- submissions/ostrich.json | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 submissions/ostrich.json diff --git a/submissions/ostrich.json b/submissions/ostrich.json new file mode 100644 index 00000000..b51457ae --- /dev/null +++ b/submissions/ostrich.json @@ -0,0 +1,27 @@ +{ + "name": "OSTRICH", + "contributors": [ + "Matthew Hague", + "Denghang Hu", + "Anthony W. Lin", + "Oliver Markgraf", + "Philipp Rümmer", + "Zhilin Wu" + ], + "contacts": [ + "Oliver Markgraf ", + "Philipp Rümmer " + ], + "archive": { + "url": "https://philipp.ruemmer.org/ostrich-2024.tar.gz", + "h": { "sha256": "bd9abdeb26c1b4541fee5ad61ef190c6055ef00b306d62739ad5704cb6e0ca4c" } + }, + "website": "https://github.com/uuverifiers/ostrich", + "system_description": "https://philipp.ruemmer.org/ostrich-2024.pdf", + "command": ["./ostrich", "-portfolio=strings", "+quiet"], + "solver_type": "Standalone", + "seed": "753", + "participations": [ + { "tracks": ["SingleQuery"], "divisions": ["QF_Strings"] } + ] +} From 12225b059f2eb07832a6fa0b13ff09d9aab31d1a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hans-J=C3=B6rg?= Date: Tue, 18 Jun 2024 01:39:11 -0500 Subject: [PATCH 19/25] Solver submission: cvc5 (#64) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add cvc5 preliminary version * Remove cvc5 from parallel track * Fix command for incremental track * Remove cvc5 from the cloud track * Use Zenodo release --------- Co-authored-by: François Bobot --- submissions/cvc5.json | 62 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 submissions/cvc5.json diff --git a/submissions/cvc5.json b/submissions/cvc5.json new file mode 100644 index 00000000..576dfad3 --- /dev/null +++ b/submissions/cvc5.json @@ -0,0 +1,62 @@ +{ + "name": "cvc5", + "contributors": [ + "Leni Aniva", + "Haniel Barbosa", + "Clark Barrett", + "Hanna Lachnitt", + "Daniel Larraz", + "Abdalrhman Mohamed", + "Mudathir Mohamed", + "Aina Niemetz", + "Alex Ozdemir", + "Mathias Preiner", + "Andrew Reynolds", + "Hans-Jörg Schurr", + "Cesare Tinelli", + "Amalee Wilson", + "Yoni Zohar" + ], + "contacts": [ + "Hans-Jörg Schurr ", + "Amalee Wilson ", + "Clark Barrett " + ], + "archive": { + "url": "https://zenodo.org/records/11581520/files/cvc5-default.zip", + "h": { + "sha256": "4e8b6f6aaa8a22afec427633e66d1880f9f106efca4aa35d143cd97f90f2b3bb" + } + }, + "website": "https://cvc5.github.io/", + "system_description": "https://zenodo.org/records/11581520/files/cvc5.pdf", + "command": [ "bin/starexec_run_sq" ], + "solver_type": "Standalone", + "participations": [ + { + "tracks": [ "SingleQuery" ], + "logics": ".*" + }, + { + "tracks": [ "UnsatCore" ], + "logics": ".*", + "command": [ "bin/starexec_run_uc" ] + }, + { + "tracks": [ "ModelValidation" ], + "logics": ".*", + "command": [ "bin/starexec_run_mv" ] + }, + { + "tracks": [ "Incremental" ], + "logics": ".*", + "archive": { + "url": "https://zenodo.org/records/11581520/files/cvc5-inc.zip", + "h": { + "sha256": "25d7fb5461a5b4b96e75145d95700085db81f3b0f6c7af556b47a2aaf1fbcd96" + } + }, + "command": [ "bin/smtcomp_run_incremental" ] + } + ] +} From 48587eaa4384b75f3aab4630fb3a3cdf8d483d89 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?John=20L=C3=9C?= <65240623+JohnLyu2@users.noreply.github.com> Date: Tue, 18 Jun 2024 03:05:38 -0400 Subject: [PATCH 20/25] Z3-alpha draft PR (#65) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Z3-alpha draft PR * Add .json extension to Z3-alpha * first-version submission * second-time submission * third submission --------- Co-authored-by: François Bobot --- submissions/Z3-alpha.json | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 submissions/Z3-alpha.json diff --git a/submissions/Z3-alpha.json b/submissions/Z3-alpha.json new file mode 100644 index 00000000..85e6c680 --- /dev/null +++ b/submissions/Z3-alpha.json @@ -0,0 +1,35 @@ +{ + "name": "Z3-alpha", + "contributors": [ + "Zhengyang John Lu", "Paul Sarnighausen-Cahn", "Stefan Siemer", "Florin Manea", "Vijay Ganesh" + ], + "contacts": ["John Lu "], + "archive": { + "url": "https://zenodo.org/records/11643334/files/z3alpha.tar.gz?download=1" + }, + "website": "https://github.com/JohnLyu2/z3alpha", + "system_description": "https://drive.google.com/uc?export=download&id=17IULX6QpcqKJ51BzeT6XttAtyRwJIFyY", + "solver_type": "derived", + "command": ["z3alpha_submission/z3alpha.py"], + "seed": "1231", + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "Bitvec", + "QF_Bitvec", + "QF_Datatypes", + "QF_Equality", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith", + "QF_Strings" + ] + }, + { + "tracks": ["SingleQuery"], + "logics": ["QF_AUFBV", "QF_UFBV"] + } + ] +} From 4409c58fdef184f52360420c888553a575379355 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> Date: Tue, 18 Jun 2024 12:05:53 +0500 Subject: [PATCH 21/25] Yices2 SMTCOMP 2024 Submission (#66) * draft yices2 submission json file * minor * typo * update * seed * rm trailing whitespace * Update yices2.json * rm h * minor format * Update yices2.json --- submissions/yices2.json | 138 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 138 insertions(+) create mode 100644 submissions/yices2.json diff --git a/submissions/yices2.json b/submissions/yices2.json new file mode 100644 index 00000000..7c65cc0f --- /dev/null +++ b/submissions/yices2.json @@ -0,0 +1,138 @@ +{ + "name": "Yices2", + "contributors": [ + "Bruno Dutertre", + "Aman Goel", + "Stéphane Graham-Lengrand", + "Thomas Hader", + "Ahmed Irfan", + "Dejan Jovanovic", + "Ian A Mason" + ], + "contacts": [ + "Ahmed Irfan ", + "Stéphane Graham-Lengrand " + ], + "archive": { + "url": "https://ahmed-irfan.github.io/smtcomp2024/yices2-smtcomp-2024.zip" + }, + "website": "https://yices.csl.sri.com", + "system_description": "https://ahmed-irfan.github.io/smtcomp2024/yices2-smtcomp-2024.pdf", + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": ["QF_ABV", + "QF_ALIA", + "QF_ANIA", + "QF_AUFBV", + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_AUFLIA", + "QF_AUFNIA", + "QF_AX", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_NIA", + "QF_NIRA", + "QF_NRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_UFNIA", + "QF_UFNRA", + "UF"], + "command": ["./yices_smt2"] + }, + { + "tracks": ["SingleQuery"], + "logics": ["QF_BV"], + "command": ["./yices_smt2", "--delegate=kissat"] + }, + { + "tracks": ["Incremental"], + "logics": ["QF_ABV", + "QF_ALIA", + "QF_ANIA", + "QF_AUFBV", + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_AUFLIA", + "QF_AUFNIA", + "QF_AX", + "QF_BV", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_NIA", + "QF_NIRA", + "QF_NRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_UFNIA", + "QF_UFNRA"], + "command": ["./yices_smt2", "--incremental"] + }, + { + "tracks": ["UnsatCore"], + "logics": ["QF_ABV", + "QF_ALIA", + "QF_AUFBV", + "QF_AUFBVLIA", + "QF_AUFLIA", + "QF_AX", + "QF_BV", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "UF"], + "command": ["./yices_smt2"] + }, + { + "tracks": ["ModelValidation"], + "logics": ["QF_BV", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_NIA", + "QF_NIRA", + "QF_NRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_UFNIA", + "QF_UFNRA"], + "command": ["./yices_smt2"] + } + ], + "seed": 0 +} From b975f0cb5d99340da9257a57c0eeb246f69dea1c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?St=C3=A9phane=20Graham-Lengrand?= Date: Tue, 18 Jun 2024 00:06:07 -0700 Subject: [PATCH 22/25] yicesQS submission to the 2024 SMT comp (#70) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * draft yicesQS submission * archive + system description * fixing json * fixing json * fixing json * tentative final version link on Zenodo --------- Co-authored-by: François Bobot --- submissions/yicesQS.json | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 submissions/yicesQS.json diff --git a/submissions/yicesQS.json b/submissions/yicesQS.json new file mode 100644 index 00000000..09f1eb61 --- /dev/null +++ b/submissions/yicesQS.json @@ -0,0 +1,27 @@ +{ + "name": "YicesQS", + "contributors": [ + "Stéphane Graham-Lengrand" + ], + "contacts": [ + "Stéphane Graham-Lengrand " + ], + "archive": { + "url": "https://zenodo.org/records/11607999/files/yicesQS.zip?download=1" + }, + "website": "https://github.com/disteph/yicesQS", + "system_description": "https://www.csl.sri.com/users/sgl/Work/Reports/2024-yicesQS.pdf", + "solver_type": "derived", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": ["BV", + "LIA", + "LRA", + "NIA", + "NRA" + ], + "command": ["./starexec_run_default"] + } + ] +} From 94d413e034d70b5b4f3f2f1bbf9612357f832afa Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Tue, 18 Jun 2024 17:06:25 +1000 Subject: [PATCH 23/25] STP v2.3.4 submission (#74) * draft * Update with latest release * Replacing with a tar --- submissions/STP.json | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 submissions/STP.json diff --git a/submissions/STP.json b/submissions/STP.json new file mode 100644 index 00000000..8274f04f --- /dev/null +++ b/submissions/STP.json @@ -0,0 +1,40 @@ +{ + "name": "STP", + "contributors": [ + "Vijay Ganesh", + "Trevor Hansen", + "Mate Soos", + "Dan Liew", + "Ryan Govostes", + "Andrew V. Jones" + ], + "contacts": [ + "Trevor Hansen " + ], + "archive": { + "url": "https://github.com/stp/stp/releases/download/2.3.4_cadical/stp.tar", + "h": { "sha256": "33fa567fcc2467107dc147bace4324fe751ca9d65752264d624b7b4c1b52b432" } + }, + "website": "https://stp.github.io/", + "system_description": "https://github.com/stp/docs/tree/master/smt2024-descr/descr.pdf", + "solver_type": "Standalone", + "seed": "1343", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": ["QF_BV"], + "command": ["./stp"] + }, + { + "tracks": ["Incremental"], + "logics": ["QF_BV"], + "command": ["./stp"] + }, + { + "tracks": ["ModelValidation"], + "logics": ["QF_BV"], + "command": ["./stp"] + } + ] +} + From bbc54b4d2fbcaa79e4b185164fd3ece74e48a08f Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Tue, 18 Jun 2024 11:53:03 +0100 Subject: [PATCH 24/25] Create iprover_smtcomp.sh (#96) * Create iprover_smtcomp.sh To run iProver please use cd bin iprover_smtcomp.sh "cd bin" is needed as paths in scripts are relative to bin. * fixed white spaces * pp json * json * json * rm parallel track from json * fix json * fix json * fix json * fix relative paths * smtcomp/test_solver.py: print solver output * smtcomp/test_solver.py: STDERR * smtcomp/test_solver.py: * new version * new version * reverted smtcomp/test_solver.py * new version * smtcomp/test_solver.py: line out * smtcomp/test_solver.py: line out * new version * new version * dbg * venv dbg * venv dbg * venv dbg * dbg * dbg * dbg * dbg * dbg * dbg * dbg * dbg * dbg * dbg * dbg * dbg * dbg * dbg * dbg * final version * final --- submissions/iprover_smtcomp.json | 37 ++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 submissions/iprover_smtcomp.json diff --git a/submissions/iprover_smtcomp.json b/submissions/iprover_smtcomp.json new file mode 100644 index 00000000..d7c630c1 --- /dev/null +++ b/submissions/iprover_smtcomp.json @@ -0,0 +1,37 @@ +{ + "archive" : { + "h" : { + "sha256" : "8f7f4bad13e87d6aaa1bb8ca78b102edaa5495caf65d5fe39c3c16d6f70003d6" + }, + "url" : "https://zenodo.org/records/11671867/files/iprover_v3.9_smt_comp_2024.zip" + }, + "command" : [ + "bin/iprover_smtcomp.sh" + ], + "contacts" : [ + "Konstantin Korovin " + ], + "contributors" : [ + { + "name" : "Konstantin Korovin", + "website" : "http://www.cs.man.ac.uk/~korovink/" + } + ], + "name" : "iProver v3.9", + "participations" : [ + { + "divisions" : [ + "Arith", + "Equality", + "Equality+LinearArith", + "Equality+NonLinearArith" + ], + "tracks" : [ + "SingleQuery" + ] + } + ], + "solver_type" : "wrapped", + "system_description" : "http://www.cs.man.ac.uk/~korovink/iprover-smt-comp-2024.pdf", + "website" : "https://gitlab.com/korovin/iprover" +} From 4825cb5376c59b5b2537fd31ad4ffac837c7d727 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Wed, 19 Jun 2024 15:57:24 +0200 Subject: [PATCH 25/25] AWS and non-AWS track can't be mixed in participation --- smtcomp/defs.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/smtcomp/defs.py b/smtcomp/defs.py index a37de822..75e2da42 100644 --- a/smtcomp/defs.py +++ b/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):