Certificate data generator integrated into the smtcomp tool. (#114)

data/latex-certificates/experimental.csv

@@ -0,0 +1,8 @@
+track,division
+model_validation,QF_ADT+BitVec
+model_validation,QF_ADT+LinArith
+model_validation,QF_Datatypes
+model_validation,QF_Equality+NonLinearArith
+model_validation,QF_FPArith
+model_validation,QF_NonLinearIntArith
+model_validation,QF_NonLinearRealArith

data/latex-certificates/solvers_pretty_name.csv

@@ -0,0 +1,20 @@
+Solver Name,Members
+Algaroba,3
+Amaya,4
+Bitwuzla,2
+COLIBRI,3
+cvc5,15
+cvc5-cloud,5
+iProver v3.9,8
+OpenSMT,2
+OSTRICH,6
+plat-smt,1
+SMTInterpol,5
+SMT-RAT,3
+SMTS,3
+STP,6
+Yices2,7
+YicesQS,1
+Z3-Noodler,5
+Z3-alpha,5
+Z3-Parti-Z3++,2

smtcomp/certificates.py

@@ -191,7 +191,9 @@ def parse_experimental_division(solvers: Any, experimental_division: Path) -> di
  return res
 
 
-def main(website_results: Path, input_for_certificates: Path, pretty_names: Path, experimental_division: Path) -> None:
+def generate_certificates(
+ website_results: Path, input_for_certificates: Path, pretty_names: Path, experimental_division: Path
+) -> None:
  solvers: defaultdict[str, info] = defaultdict(info)
 
  parse_pretty_names(solvers, pretty_names)
@@ -253,11 +255,3 @@ def main(website_results: Path, input_for_certificates: Path, pretty_names: Path
  output.flush()
  else:
  print("solver: ", key, "( no certificate )")
-
-
-main(
- Path("../../../smt-comp.github.io/_results_2023"),
- Path("input_for_certificates.tex"),
- Path("solvers_pretty_name.csv"),
- Path("../experimental.csv"),
-)

smtcomp/main.py

@@ -38,6 +38,7 @@
 from multiprocessing.pool import ThreadPool
 from smtcomp.benchexec import get_suffix
 from smtcomp.scramble_benchmarks import benchmark_files_dir
+import smtcomp.certificates
 from smtcomp.utils import *
 import re
 
@@ -1042,7 +1043,7 @@ def export_results_pages(data: Path, results: list[Path] = typer.Argument(None))
 
 @app.command()
 def build_dolmen(data: Path) -> None:
- f"""
+ """
  build dolmen at version {defs.Config.dolmen_commit}
  """
 
@@ -1064,3 +1065,18 @@ def build_dolmen(data: Path) -> None:
  else:
  print("[red]Binary still missing[/red]")
  exit(1)
+
+
+@app.command()
+def generate_certificates(
+ website_results: Path = Path("web/content/results"),
+ input_for_certificates: Path = Path("data/latex-certificates/input_for_certificates.tex"),
+ pretty_names: Path = Path("data/latex-certificates/solvers_pretty_name.csv"),
+ experimental_division: Path = Path("data/latex-certificates/experimental.csv"),
+) -> None:
+ """
+ generates the input data for the tex certificate generator.
+ """
+ smtcomp.certificates.generate_certificates(
+ website_results, input_for_certificates, pretty_names, experimental_division
+ )