diff --git a/smtcomp/defs.py b/smtcomp/defs.py index d99c6204..05c0ead2 100644 --- a/smtcomp/defs.py +++ b/smtcomp/defs.py @@ -1456,8 +1456,22 @@ class Config: "logic": int(Logic.QF_LIA), "family": "20210219-Dartagnan/ConcurrencySafety-Main", "name": "39_rand_lock_p0_vs-O0.smt2", - } + } # scrambler segfault (perhaps stack limit) + ] + """ + Benchmarks to remove before selection (currently just for aws) + """ + + removed_results = [ + { + "logic": int(Logic.QF_BV), + "family": "20230221-oisc-gurtner", + "name": "SLL-NESTED-8-32-sp-not-excluded.smt2", + } # wrong status in SMTLIB ] + """ + Benchmarks to remove after running the solvers. Can be used when the selection has already been done. + """ def __init__(self, data: Path | None) -> None: self.id = self.__class__.__next_id__ diff --git a/smtcomp/main.py b/smtcomp/main.py index 1115d05e..13ef77e4 100644 --- a/smtcomp/main.py +++ b/smtcomp/main.py @@ -205,6 +205,7 @@ def store_results( config = defs.Config(data) lf = pl.concat(pl.read_ipc(results / "parsed.feather").lazy() for results in lresults) + benchmarks = pl.read_ipc(config.cached_non_incremental_benchmarks).lazy() benchmarks_inc = pl.read_ipc(config.cached_incremental_benchmarks).lazy() for track, dst in config.current_results.items(): @@ -221,11 +222,15 @@ def store_results( print("[bold][red]Validation as not been attempted for all the results[/red][/bold]") exit(1) if track == defs.Track.UnsatCore: - df = lf.filter(track=int(track), answer=int(defs.Answer.Unsat), validation_attempted=False).collect() + df = lf.filter(track=int(track), answer=int(defs.Answer.Unsat)).collect() if len(df) > 0: - print("[bold][red]Validation as not been attempted for all the results[/red][/bold]") - print(df["answer"].unique()) - exit(1) + # Tested in two phases, because validation_attempted is not always present + df = df.filter(validation_attempted=False) + if len(df) > 0: + print("[bold][red]Validation as not been attempted for all the results[/red][/bold]") + print(df.select("logic", "solver")) + exit(1) + removed_results = pl.LazyFrame(config.removed_results) df = ( add_columns( lf.filter(track=int(track)).drop("logic"), @@ -233,6 +238,7 @@ def store_results( on=["file"], defaults={"logic": -1, "family": "", "name": ""}, ) + .join(removed_results, on=["logic", "family", "name"], how="anti") .sort("file", "solver") .collect() ) @@ -257,7 +263,12 @@ def store_results( for d in df.to_dicts() ] ) - write_cin(dst, results_track.model_dump_json(indent=1)) + write_cin( + dst, + results_track.model_dump_json( + indent=1, exclude_defaults=(track not in [defs.Track.Incremental, defs.Track.UnsatCore]) + ), + ) @app.command(rich_help_panel=benchexec_panel)