Fix unsat core results (#125)

* Fix validation criteria for unsat cores. * Add fixed unsat core results. * Use 0 for missing results. * Blackify. --------- Co-authored-by: Martin Jonáš <[email protected]>
SMT-COMP · Jul 30, 2024 · b433fcb · b433fcb
1 parent dd9d55b
commit b433fcb
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 8 deletions.
diff --git a/data/results-uc-2024.json.gz b/data/results-uc-2024.json.gz
diff --git a/smtcomp/results.py b/smtcomp/results.py
@@ -411,16 +411,23 @@ def parse_dir(dir: Path) -> pl.LazyFrame:
  vr = (
  vr.select("answer", "unsat_core", scramble_id="scramble_id_orig")
  .group_by("scramble_id", "unsat_core")
- .agg(unsat=(pl.col("answer") == int(defs.Answer.Unsat)).any(), validation_attempted=True)
+ .agg(
+ sat=(pl.col("answer") == int(defs.Answer.Sat)).count(),
+ unsat=(pl.col("answer") == int(defs.Answer.Unsat)).count(),
+ validation_attempted=True,
+ )
  )
  results = add_columns(
- results, vr, on=["scramble_id", "unsat_core"], defaults={"unsat": False, "validation_attempted": False}
+ results,
+ vr,
+ on=["scramble_id", "unsat_core"],
+ defaults={"sat": 0, "unsat": 0, "validation_attempted": False},
  )
  results = results.with_columns(
- answer=pl.when((pl.col("answer") == int(defs.Answer.Unsat)) & (pl.col("unsat")).not_())
+ answer=pl.when((pl.col("answer") == int(defs.Answer.Unsat)) & (pl.col("sat") > pl.col("unsat")))
  .then(int(defs.Answer.UnsatCoreNotValidated))
  .otherwise("answer")
- ).drop("unsat", "unsat_core")
+ ).drop("sat", "unsat", "unsat_core")
 
  return results
 
@@ -471,10 +478,10 @@ def helper_get_results(
  on=["file", "solver", "track"],
  defaults={
  "answer": -1,
- "cputime_s": -1,
- "memory_B": -1,
- "walltime_s": -1,
- "nb_answers": -1,
+ "cputime_s": 0,
+ "memory_B": 0,
+ "walltime_s": 0,
+ "nb_answers": 0,
  },
  )