Fix generate graphics and smtcomp stats-of-benchexec-results data

Author: bobot

data/2025/slides/presresults/plan.txt

@@ -1,21 +1,21 @@
-[x] slide1: change authors and affiliations    
-[ ] slide2: OK    
-[ ] slide3: 3 -> change numbers + delta to 2024    
-[ ] slide4-5: OK    
-[ ] slide6: update; proof exhibition track; as last year comment:    
-does it apply?        
-[ ] slide7: update    
-[ ] slide8-10: update    
-[ ] -- solver presentations: unknown at this point      
-[x] slide 11: update    
+[x] slide1: change authors and affiliations
+[ ] slide2: OK
+[ ] slide3: 3 -> change numbers + delta to 2024
+[ ] slide4-5: OK
+[ ] slide6: update; proof exhibition track; as last year comment:
+does it apply?
+[ ] slide7: update
+[ ] slide8-10: update
+[ ] -- solver presentations: unknown at this point
+[x] slide 11: update
 [x] slide 12
-[x] slide 13: OK?    
-[x] slide 14: add best overall metric    
-[ ] slide 15: OK                                   
-[ ] slide 16-28 change/import according to certificates    
-[ ] slide 29: update                        
-[ ] slide 30: remove?      
-[ ] slide 31: update    
-[x] slide 32: update    
-[x] slide 33: update name (rm Amazon)     
+[x] slide 13: OK?
+[x] slide 14: add best overall metric
+[ ] slide 15: OK
+[ ] slide 16-28 change/import according to certificates
+[ ] slide 29: update
+[ ] slide 30: remove?  
+[ ] slide 31: update
+[x] slide 32: update
+[x] slide 33: update name (rm Amazon) 
 [x] slide 34: update  

data/2025/slides/presresults/slides.tex

@@ -476,48 +476,48 @@ \section{Solver Presentation}
 \end{frame}
 }
 
-%\myincludepdf{slides-bitwuzla.pdf}
-
+\myincludepdf{solver/Bitwuzla.pdf}
 %\myincludepdf{slides-colibri.pdf}
 
-%%\myincludepdf{slides-cvc5.pdf}
-
-%\myvideopdf{cvc5-NRA-LS}{slides-cvc5-nra-ls.mp4}
-
-%\myvideopdf{iProver}{slides-iProver.mp4}
-
-%\myvideopdf{ismt, Yices-ismt}{slides-ismt.mp4}
-
-%\myincludepdf{slides-ismt-ppt.pdf}
-
-%\myincludepdf{slides-opensmt.pdf}
+\begin{frame}
+  \frametitle{COLIBRI}
 
-%\myvideopdf{Ostrich}{slides-Ostrich.mkv}
+  \begin{itemize}
+    \item CP/SMT solver, propagation, no learning
+    \item QF\_FParith: propagation at the floating point or bitvector level (no bot-blsting)
+    \item 2025: More propagations for transcendental functions (Could we create a category for them?)
+    \end{itemize}
+    \vfill
+    \includegraphics[height=1cm]{logo_cea.png}
+\end{frame}
 
-%\myincludepdf{slides-smtinterpol.pdf}
 
-%\myincludepdf{slides-smtrat.pdf}
 
-%\myvideopdf{UltimateEliminator+MathSAT}{slides-UltimateEliminator.mkv}
+\begin{frame}
+  \frametitle{colibri2}
 
-%\myincludepdf{slides-vampire.pdf}
+  \begin{itemize}
+    \item First year participation
+    \item CP/SMT solver, propagation, no learning
+    \item Uses Dolmen as parser, so parse all standardized SMT-LIB theories
+    \item For 2025: participation only in QF\_FParith, many propagators from COLIBRI but nearly no propagators for BV
+    \item For 2026: add BV propagators ;), participation in quantified theory?
+    \end{itemize}
+    \vfill
+    \includegraphics[height=1cm]{logo_cea.png}
+\end{frame}
 
-%\myincludepdf{slides-yaga.pdf}
+\myincludepdf{solver/cvc5.pdf}
 
-%\myincludepdf{slides-Yices-2023.pdf}
+\myincludepdf{solver/opensmt.pdf}
 
-%\myincludepdf{slides-YicesQS-2025.pdf}
+\myincludepdf{solver/ostrich-smt-comp-2025.pdf}
 
-%\myvideopdf{Z3-Z3++}{slides-z3-z3++.mp4}
-\begin{frame}
-\textcolor{red}{TODO: Add solver slides received through the call}
-%
-  %\frametitle{Z3-Z3++}
+\myincludepdf{solver/smtinterpol.pdf}
 
-  %\begin{center}
-    %\url{https://youtu.be/fBB0Wxxf9vA}
-  %\end{center}
-\end{frame}
+% \begin{frame}
+% \textcolor{red}{TODO: Add solver slides received through the call}
+% \end{frame}
 
 \begin{frame}
   \frametitle{Other participants}
@@ -903,15 +903,38 @@ \section{Solver Presentation}
   \end{itemize}
 \end{frame}
 
+%http://localhost:1313/2025/results/qf_fparith-single-query-chart/
+%http://localhost:1313/2025/results/lia-single-query-chart/
+%http://localhost:1313/2025/results/qf_bitvec-single-query/
+%http://localhost:1313/2025/results/qf_strings-single-query/
+
+
+\begin{frame}{Derived Solver: like any solver?}
 
-\begin{frame}{Derived Solver}
-  
   Derived Tool: A derived tool is defined as any solver that is based on and \textbf{extends another SMT
 solver} (the base solver) \textbf{from a different group of authors}. In contrast to a wrapper tool, a derived
 tool solving a benchmark of \textbf{logic A} is allowed to call an SMT solver to solve a problem for \textbf{logic
 A}.
 \end{frame}
 
+\begin{frame}
+\frametitle{Derived Solver: like any solver?}
+\begin{itemize}
+  \item Some derived solver are very different from the base solver
+  \item Some derived solver had only a small increment
+\end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Derived Solver: like any solver?}
+  \begin{itemize}[<+->]
+    \item The comparison with the base solver should help see the improvement
+    \item "Best Family of solver"? Give credit to the base solver
+    \item Different podium? but we have derived of derived solver
+    \item What means different enough?
+  \end{itemize}
+\end{frame}
+
 %\begin{frame}{SMT-COMP organizing committee}
   %Three people organize the SMT-COMP.  In 2026:
   %\begin{itemize}

smtcomp/defs.py

@@ -1527,7 +1527,7 @@ class Config:
         "Z3-Inc-Z3++": "Z3-Inc-Z3++-base",
         "Z3-Noodler-Mocha": "Z3-Noodler-Mocha-base",
         "Z3-Owl": "Z3-Owl-base",
-        "Z3-Noodler": "Z3-Noodler",
+        "Z3-Noodler": "Z3-Noodler-base",
         "z3siri": "z3siri-base",
         "Z3-alpha": "Z3-alpha-base",
     }

smtcomp/generate_graphics.py

@@ -80,9 +80,7 @@ def create_output(
 ) -> alt.api.ChartType:
 
     # We are computing the buckets offline because we have too much data
-    results = results.filter(
-        c_run == True, c_logic.is_in(set(map(int, logics))) | c_division.is_in(set(map(int, divisions)))
-    ).select(
+    results = results.filter(c_logic.is_in(set(map(int, logics))) | c_division.is_in(set(map(int, divisions)))).select(
         c_file,
         c_logic,
         c_division,
@@ -94,6 +92,7 @@ def create_output(
     )
 
     results_with = results.select(c_file, solver2=c_solver, bucket2=c_bucket, cputime_s2=c_cputime_s, answer2=c_answer)
+
     results = results.join(results_with, on=c_file, how="left")
 
     corr = (
@@ -273,7 +272,7 @@ def generate_pages(config: defs.Config, results: pl.LazyFrame, track: defs.Track
     dst = config.web_results
     dst.mkdir(parents=True, exist_ok=True)
 
-    df_results = results.filter(c_run == True).collect()
+    df_results = results.filter(c_answer != -1).collect()
     results = df_results.lazy()
 
     divisions = list(df_results["division"].unique())

smtcomp/results.py

@@ -479,7 +479,16 @@ def helper_get_results(config: defs.Config, results: List[Path], track: defs.Tra
         lf = lf.drop("logic", "participation")  # Hack for participation 0 bug move "participation" to on= for 2025,
         lf = lf.drop("benchmark_yml", "unsat_core")
 
-    selection = smtcomp.selection.helper(config, track).with_columns(track=int(track))
+    if False:
+        selection = smtcomp.selection.helper(config, track).drop("result")
+    else:
+        if track == defs.Track.Incremental:
+            selection = pl.read_ipc(config.cached_incremental_benchmarks).lazy()
+        else:
+            selection = pl.read_ipc(config.cached_non_incremental_benchmarks).lazy()
+        selection = intersect(selection, lf.select("file").unique(), on=["file"]).with_columns(selected=True)
+
+    selection = selection.with_columns(track=int(track))
 
     selection = (
         selection.unique()
@@ -491,36 +500,48 @@ def helper_get_results(config: defs.Config, results: List[Path], track: defs.Tra
         .lazy()
     )
 
-    defaults = {
-        "division": -1,
-        "family": -1,
-        "logic": -1,
-        "name": "",
-        "participation": -1,
-        "selected": True,
-    }
+    # defaults = {
+    #     "division": -1,
+    #     "family": -1,
+    #     "logic": -1,
+    #     "name": "",
+    #     "participation": -1,
+    #     "selected": True,
+    # }
+
+    defaults = {}
 
     if track == defs.Track.Incremental:
-        defaults["check_sats"] = -1
+        # defaults["check_sats"] = -1
+        pass
     else:
-        defaults["status"] = -1
-        defaults["asserts"] = -1
+        # defaults["status"] = -1
+        # defaults["asserts"] = -1
+        pass
 
     if track == defs.Track.Parallel:
-        defaults["hard"] = True
-        defaults["unsolved"] = False
+        # defaults["hard"] = True
+        # defaults["unsolved"] = False
+        pass
     else:
-        defaults["current_result"] = -1
-        defaults["new"] = False
-        defaults["result"] = -1
-        defaults["run"] = True
-        defaults["trivial"] = False
-        defaults["file_right"] = ""
+        # defaults["current_result"] = -1
+        # defaults["new"] = False
+        # defaults["run"] = True
+        # defaults["trivial"] = False
+        # defaults["file_right"] = ""
+        pass
+
+    defaults["cputime_s"] = 0
+    defaults["nb_answers"] = 0
+    defaults["memory_B"] = 0
+    defaults["walltime_s"] = 0
+    defaults["answer"] = -1
 
     selected = intersect(selection, smtcomp.selection.solver_competing_logics(config), on=["logic", "track"])
+
     selected = add_columns(
-        lf,
         selected,
+        lf,
         on=["file", "solver", "track"],
         defaults=defaults,
     )

smtcomp/utils.py

@@ -34,6 +34,9 @@ def add_columns(dst: pl.LazyFrame, from_: pl.LazyFrame, on: list[str], defaults:
     assert on_cols.issubset(dst_cols)
     assert on_cols.issubset(from_cols)
     assert dst_cols.isdisjoint(from_cols.difference(on_cols))
+    if from_cols.difference(on_cols) != defaults.keys():
+        print(set(defaults.keys()).difference(from_cols.difference(on_cols)))
+        print(from_cols.difference(on_cols).difference(defaults.keys()))
     assert from_cols.difference(on_cols) == defaults.keys()
     fill_nulls = [pl.col(k).fill_null(value=v) for k, v in defaults.items()]
     return dst.join(from_, how="left", on=on, coalesce=True).with_columns(*fill_nulls)