diff --git a/data/2025/slides/future/1280px-Amazon_Web_Services_Logo.svg.png b/data/2025/slides/future/1280px-Amazon_Web_Services_Logo.svg.png new file mode 100644 index 00000000..aa9e753c Binary files /dev/null and b/data/2025/slides/future/1280px-Amazon_Web_Services_Logo.svg.png differ diff --git a/data/2025/slides/future/512px-OOjs_UI_icon_laptop-progressive.svg.png b/data/2025/slides/future/512px-OOjs_UI_icon_laptop-progressive.svg.png new file mode 100644 index 00000000..360c7203 Binary files /dev/null and b/data/2025/slides/future/512px-OOjs_UI_icon_laptop-progressive.svg.png differ diff --git a/data/2025/slides/future/Google-Cloud-Emblem.png b/data/2025/slides/future/Google-Cloud-Emblem.png new file mode 100644 index 00000000..84294711 Binary files /dev/null and b/data/2025/slides/future/Google-Cloud-Emblem.png differ diff --git a/data/2025/slides/future/Google__G__Logo.svg.png b/data/2025/slides/future/Google__G__Logo.svg.png new file mode 100644 index 00000000..aa2cc166 Binary files /dev/null and b/data/2025/slides/future/Google__G__Logo.svg.png differ diff --git a/data/2025/slides/future/Microsoft-Azure.png b/data/2025/slides/future/Microsoft-Azure.png new file mode 100644 index 00000000..c4cf8839 Binary files /dev/null and b/data/2025/slides/future/Microsoft-Azure.png differ diff --git a/data/2025/slides/future/You've_got_mail.png b/data/2025/slides/future/You've_got_mail.png new file mode 100644 index 00000000..062d8d4c Binary files /dev/null and b/data/2025/slides/future/You've_got_mail.png differ diff --git a/data/2025/slides/future/free-github-163-761603.png b/data/2025/slides/future/free-github-163-761603.png new file mode 100644 index 00000000..bf66cd79 Binary files /dev/null and b/data/2025/slides/future/free-github-163-761603.png differ diff --git a/data/2025/slides/future/iowa_university.png b/data/2025/slides/future/iowa_university.png new file mode 100644 index 00000000..e1153383 Binary files /dev/null and b/data/2025/slides/future/iowa_university.png differ diff --git a/data/2025/slides/future/prover.json b/data/2025/slides/future/prover.json new file mode 100644 index 00000000..48842ad7 --- /dev/null +++ b/data/2025/slides/future/prover.json @@ -0,0 +1,30 @@ +{ + "name": "bub4", + "authors": ["you"], + "logics": { + "sq": ["UF"], + "uc": "^QF_(LRA)?(UF)?$", + "mv": { + "theories": ["QF", "+-UF", "+-BV", "+-A"], + "except": ["QF_UFBVA"], + "logics": ["QF_LRA"] + } + }, + "versions": [ + { + "name": "10/05/24", + "url": "http://...", + "sha256": "123434ac", + "competing": true, + "cmd": { + "mv": ["bub4", "--model"] + } + }, + { + "name": "fixed", + "url": "http://...", + "sha256": "123434ac", + "competing": false + } + ] +} diff --git a/data/2025/slides/future/smtcomp_futur.tex b/data/2025/slides/future/smtcomp_futur.tex new file mode 100644 index 00000000..d16300cb --- /dev/null +++ b/data/2025/slides/future/smtcomp_futur.tex @@ -0,0 +1,341 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% SMT-COMP 2023 - Futur of SMTCOMP without starexec +% +% 1 hour +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\documentclass[table]{beamer} +\usepackage[utf8]{inputenc} +\usepackage{xcolor} +\usepackage{tikz} +\usetikzlibrary{shapes,shapes.callouts,automata,trees} +\usetikzlibrary{decorations.pathmorphing,external,fit} +\usetikzlibrary{calc} +\usetikzlibrary{backgrounds} %used for the CEGAR figure +\usepackage{amssymb} +\usepackage{clrscode} +\usepackage{pifont} +\usepackage{pdfpages} +\usepackage{graphicx} +\usepackage{listings} +\geometry{papersize={16cm,9cm}} +%\tikzexternalize + +\colorlet{MYred}{red!70!black} +\definecolor{MYgreen}{rgb}{.1,.5,0} +\definecolor{MYblue}{rgb}{0,.42,.714} +\colorlet{MYgray}{white!95!MYblue} +\colorlet{MYorange}{orange!80!black} +\definecolor{gold}{rgb}{.8,.6,0} +\colorlet{silver}{white!55!black} +\colorlet{bronze}{brown!70!black} +\def\tick{\ding{52}} +\def\cross{\ding{54}} + +%%%%%%%%%%%%%%%%%%%% +%%% Beamer stuff %%% +%%%%%%%%%%%%%%%%%%%% +\usetheme{default} +\useinnertheme{rounded} +\setbeamertemplate{frametitle}[default][center] +\setbeamertemplate{footline}{\quad\hfill\footnotesize\insertframenumber\strut\kern1em\vskip2pt} +\setbeamertemplate{navigation symbols}{} +\setbeamertemplate{itemize/enumerate subbody begin}{\normalsize} +\usefonttheme[onlymath]{serif} % Nicer formulas +\setbeamercolor{block body}{bg=black!10} +\setbeamercolor{block title}{bg=black!20} + +\AtBeginSection[]{ + \begin{frame} + \vfill + \centering + \begin{beamercolorbox}[sep=8pt,center,shadow=true,rounded=true]{title} + \usebeamerfont{title}\insertsectionhead\par% + \end{beamercolorbox} + \vfill + \end{frame} +} + +\def\emph#1{\textcolor{MYblue}{#1}} + +%%% Titel, Autor und Datum des Vortrags: +\title{Discussion on Future of SMT-COMP} +\author{Martin Bromberger \and Jochen Hoenicke \and \emph{Fran\c{c}ois Bobot}} +\date{July 5, 2023} + +%% Institut +\institute{ +CEA List, France \and +MPI für Informatik, Germany \and +Certora, Israel +} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% MACROS + +% database symbol (from stackexchange) + +\makeatletter +\tikzset{ + database/.style={ + path picture={ + \draw (0, 1.5*\database@segmentheight) circle [x radius=\database@radius,y radius=\database@aspectratio*\database@radius]; + \draw (-\database@radius, 0.5*\database@segmentheight) arc [start angle=180,end angle=360,x radius=\database@radius, y radius=\database@aspectratio*\database@radius]; + \draw (-\database@radius,-0.5*\database@segmentheight) arc [start angle=180,end angle=360,x radius=\database@radius, y radius=\database@aspectratio*\database@radius]; + \draw (-\database@radius,1.5*\database@segmentheight) -- ++(0,-3*\database@segmentheight) arc [start angle=180,end angle=360,x radius=\database@radius, y radius=\database@aspectratio*\database@radius] -- ++(0,3*\database@segmentheight); + }, + minimum width=2*\database@radius + \pgflinewidth, + minimum height=3*\database@segmentheight + 2*\database@aspectratio*\database@radius + \pgflinewidth, + }, + database segment height/.store in=\database@segmentheight, + database radius/.store in=\database@radius, + database aspect ratio/.store in=\database@aspectratio, + database segment height=0.1cm, + database radius=0.25cm, + database aspect ratio=0.35, +} +\makeatother + +%%%%% json lstlisting %%%%%%%%% + +\definecolor{eclipseStrings}{RGB}{42,0.0,255} +\definecolor{eclipseKeywords}{RGB}{127,0,85} +\colorlet{numb}{magenta!60!black} + +\lstdefinelanguage{json}{ + basicstyle=\normalfont\ttfamily, + commentstyle=\color{eclipseStrings}, % style of comment + stringstyle=\color{eclipseKeywords}, % style of strings + % numbers=left, + numberstyle=\scriptsize, + stepnumber=1, + numbersep=8pt, + showstringspaces=false, + breaklines=true, + frame=lines, +% backgroundcolor=\color{gray}, %only if you like + string=[s]{"}{"}, + comment=[l]{:\ "}, + morecomment=[l]{:"}, + literate= + *{0}{{{\color{numb}0}}}{1} + {1}{{{\color{numb}1}}}{1} + {2}{{{\color{numb}2}}}{1} + {3}{{{\color{numb}3}}}{1} + {4}{{{\color{numb}4}}}{1} + {5}{{{\color{numb}5}}}{1} + {6}{{{\color{numb}6}}}{1} + {7}{{{\color{numb}7}}}{1} + {8}{{{\color{numb}8}}}{1} + {9}{{{\color{numb}9}}}{1} +} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand\vitem{\vfill\item} + +\begin{document} + +\begin{frame} + \titlepage +\end{frame} + +\newcommand{\mylogo}[1]{\includegraphics[height=1.5em]{#1}} + +\newbox{\logostarexec} +\savebox{\logostarexec}{\mylogo{starlogo.png}} + +\newcommand{\logolaptop}{\mylogo{512px-OOjs_UI_icon_laptop-progressive.svg.png}} + +\begin{frame} + \frametitle{Current infrastructure} + \pause + \begin{tabular}{cl} + \mylogo{iowa_university.png}\usebox{\logostarexec} & Benchmark uploaded to StarExec from Iowa Gitlab \\\pause + \mylogo{Google__G__Logo.svg.png} & Applications through Google form \\\pause + \usebox{\logostarexec} & Solvers are uploaded to StarExec \\\pause + \mylogo{You've_got_mail.png} & Modification of the applications handled by mail \\\pause + \logolaptop & Solvers downloaded, wrapped locally, uploaded to StarExec \\\pause + \logolaptop & Benchmark selection and job created locally \\\pause + \usebox{\logostarexec} & Jobs sent to StarExec and run \\\pause + \usebox{\logostarexec} & Download results from StarExec \\\pause + \logolaptop \usebox{\logostarexec} & Fix benchmark selection, add fixed + version of the solvers, run jobs on Starexec \\\pause + \logolaptop & Score the results, generate data for the website \\ + \end{tabular} +\end{frame} + +\newcommand{\onlystarexec}{\only<1>{\usebox{\logostarexec}}} +\newcommand{\onlylaptop}{\only<1-4>{\logolaptop}} +\newcommand{\logocloud}{\mylogo{1280px-Amazon_Web_Services_Logo.svg.png} +\mylogo{Google-Cloud-Emblem.png} +\mylogo{Microsoft-Azure.png}} +\newcommand{\onlycloudfirst}{\only<4->{\logocloud}} +\newcommand{\onlycloudsecond}{\only<5->{\logocloud}} +\newcommand{\logogithub}{\mylogo{free-github-163-761603.png}} +\newcommand{\logozenodo}{\mylogo{zenodo.png}} + +\frame<1>[label=summary]{ + \frametitle{Needed infrastructure} + \begin{itemize} + \item Store benchmark : \mylogo{iowa_university.png}\onlystarexec %iowa and starexec + \item Participants registration : \only<-4>{\mylogo{Google__G__Logo.svg.png}\mylogo{You've_got_mail.png}} + \only<5->{\logogithub} + %google and starexec + \item Select the benchmarks: \onlylaptop\onlycloudsecond + \item Run the jobs : \onlystarexec\onlycloudfirst%starexec + \item Store the datas : \onlystarexec\onlycloudfirst%starexec + \item Archive the datas : \onlystarexec\only<3->{\logozenodo}%starexec +% \item Store the raw results (sq csv 148Mo, 16Mo compressed) : \usebox{\logostarexec}%starexec +% \item Store the artifacts (mv Go proof Go) : \usebox{\logostarexec} %starexec + \item Run scoring script and generate website : \onlylaptop\onlycloudsecond\logogithub%localy and github + \end{itemize} +} + +\begin{frame} + \frametitle{StarExec} + Since 2013, StarExec has run 80 competitions and events across its 16 registered communities(SAT, TPTP, Termination,...). + StarExec is supported by a \$1.85 million USD grant (NSF) + +%Several people have contributed in various capacities to the StarExec project +%so far. +\vfill +Shepherded by Aaron Stump +\vfill +Involved in the development: {\small Eric Burns, Todd Elvers, +Albert Giegerich, Pat Hawks, Tyler Jensen, Wyatt Kaiser, Ben McCune, Muhammad +Nassar, CJ Palmer, Vivek Sardeshmukh, Skylar Stark, and Ruoyu Zhang.} +\vfill +Computer system support and assistance: {\small Hugh Brown, Dan Holstad, Jamie +Tisdale, and JJ Ulrich} + +%In addition to the members of the Advisory Board, the following people have +%provided useful feedback and input: Clark Barrett, Christoph Benzmüller, Armin +%Biere, David Cok, Morgan Deters, Jürgen Giesl, Alberto Griggio, Thomas +%Krennwallner, Jens Otten, Andrei Paskevich, Olivier Roussel, Martina Seidl, +%Stephan Schulz, Michael Tautschnig, Christoph Wintersteiger, and Harald Zankl. +\end{frame} + +\begin{frame} + \frametitle{StarExec: job pairs} +\begin{center} + \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{statistics_starexec.png} +\end{center} + +\end{frame} +\begin{frame} + \frametitle{StarExec is closing} + + \begin{center} + + \huge{Decommissioned starting August 2024} + \end{center} + +\end{frame} + +\againframe<2>{summary} + +\begin{frame} + \frametitle{Archive: Past results and Artifacts} + + \begin{itemize} + \item Solvers + \item Raw results + \item Solver output + \end{itemize} + \vfill + \pause + \logozenodo: EC funded research. Leveraging CERN developed tools for Big Data management and extended Digital Library capabilities for Open Data + \begin{itemize} + \item Open + \item Max 50 GB per dataset + \item DOI + \end{itemize} +\vfill + NB: StarExec should do the upload (because downloading from StarExec is very slow) + +\end{frame} + +\againframe<3>{summary} + + +% \begin{frame} +% \frametitle{Future competition} + +% \begin{itemize} +% \item CPU +% \item Intermediate Data-storage +% \item Permanent Data-storage (like past competition) +% \end{itemize} + +% \end{frame} + + + +\begin{frame} + \frametitle{Future competitions: Cloud? \logocloud} +\begin{columns} + \column{0.5\textwidth} + Slurm (open-source job scheduler): + \begin{itemize} + \item Available in cloud providers + \item Could be available in academic clusters + \item Allows to do the selection in the cloud + \end{itemize} + \column{0.5\textwidth} + Batch + \begin{itemize} + \item Each provider as its own API + \item Simpler + \item e.g. \url{https://github.com/Z3Prover/PerformanceTest} + \end{itemize} +\end{columns} + \pause + \vfill + \begin{center} + \large + Who already used cloud for benchmarking? + \end{center} +\end{frame} + + +\againframe<4>{summary} + +\begin{frame} + \frametitle{Participant registration} + Github Merge Request with \lstinline{bub4.json}: + + \lstinputlisting[language=json]{prover.json} +\end{frame} + +\againframe<5>{summary} + +\begin{frame} + \frametitle{Other simplifications} + \begin{itemize} + \item Currently 3 repositories $\implies$ 1 repository + \item Bash, sed, awk, python $\implies$ python + \item Tests? + \end{itemize} +\pause +\vfill + \begin{center} + {\large Is the secrecy of the result important to keep?} + \end{center} +\end{frame} + +\begin{frame} + \frametitle{Questions?} + + \begin{itemize} + \item Zenodo? For longterm archive + \item Reproducibility of the result? + \item Experience with cloud computing? + \item Need for sponsorship + \end{itemize} +\end{frame} + +\end{document} diff --git a/data/2025/slides/future/starlogo.png b/data/2025/slides/future/starlogo.png new file mode 100644 index 00000000..c88c5e15 Binary files /dev/null and b/data/2025/slides/future/starlogo.png differ diff --git a/data/2025/slides/future/statistics_starexec.png b/data/2025/slides/future/statistics_starexec.png new file mode 100644 index 00000000..c9732b12 Binary files /dev/null and b/data/2025/slides/future/statistics_starexec.png differ diff --git a/data/2025/slides/future/zenodo.png b/data/2025/slides/future/zenodo.png new file mode 100644 index 00000000..c3743606 Binary files /dev/null and b/data/2025/slides/future/zenodo.png differ diff --git a/data/2025/slides/presresults/input_for_certificates.tex b/data/2025/slides/presresults/input_for_certificates.tex new file mode 100644 index 00000000..e293670e --- /dev/null +++ b/data/2025/slides/presresults/input_for_certificates.tex @@ -0,0 +1,26 @@ +\MakeOnePage{Bitwuzla}{\withtrack{Biggest Lead}{\inc}}{\withtrack{Bitvec}{\sat,\fast}, \withtrack{Equality+MachineArith}{\inc}, \withtrack{FPArith}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}, \withtrack{QF\_ADT+BitVec}{\mv}, \withtrack{QF\_Bitvec}{\inc}, \withtrack{QF\_Equality+Bitvec}{\seq,\paral,\sat,\unsat,\fast,\inc,\mv}, \withtrack{QF\_FPArith}{\seq,\paral,\sat,\unsat,\fast,\inc,\mv}}{\withtrack{ABVFP}{\sat,\fast}, \withtrack{ABVFPLRA}{\fast}, \withtrack{AUFBV}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{AUFBVFP}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{QF\_ABVFP}{\uc}, \withtrack{QF\_ABVFPLRA}{\uc}, \withtrack{QF\_BVFP}{\uc}, \withtrack{QF\_BVFPLRA}{\uc}, \withtrack{UFBV}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{UFBVFP}{\seq,\paral,\unsat}}{s}{s} +\newpage +\MakeOnePage{COLIBRI}{}{}{\withtrack{QF\_ABVFPLRA}{\seq,\paral,\unsat,\fast}, \withtrack{QF\_FP}{\unsat,\fast}, \withtrack{QF\_FPLRA}{\unsat,\fast}}{}{s} +\newpage +\MakeOnePage{cvc5}{\withtrack{Biggest Lead}{\seq,\paral,\sat,\unsat,\uc}, \withtrack{Largest Contribution}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}}{\withtrack{Arith}{\seq,\paral,\unsat,\inc,\uc}, \withtrack{Bitvec}{\seq,\paral,\unsat,\inc,\uc}, \withtrack{Equality}{\seq,\paral,\sat,\unsat,\inc,\uc,\cloud}, \withtrack{Equality+LinearArith}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc,\cloud}, \withtrack{Equality+MachineArith}{\seq,\paral,\sat,\unsat,\fast,\uc}, \withtrack{Equality+NonLinearArith}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}, \withtrack{QF\_Datatypes}{\seq,\paral,\sat,\unsat,\uc\textsuperscript\seq}, \withtrack{QF\_Equality}{\inc}, \withtrack{QF\_Equality+Bitvec+Arith}{\inc}, \withtrack{QF\_Equality+NonLinearArith}{\seq,\paral,\unsat,\fast,\inc,\uc,\mv}, \withtrack{QF\_FPArith}{\uc}, \withtrack{QF\_LinearIntArith}{\unsat}, \withtrack{QF\_LinearRealArith}{\unsat}, \withtrack{QF\_NonLinearRealArith}{\unsat,\fast}, \withtrack{QF\_Strings}{\seq,\paral,\sat,\unsat}}{\withtrack{LIA}{\sat,\fast}, \withtrack{NIA}{\sat,\fast}, \withtrack{QF\_ALIA}{\inc}, \withtrack{QF\_AUFLIA}{\uc,\mv}, \withtrack{QF\_AX}{\mv}, \withtrack{QF\_BVFPLRA}{\inc}, \withtrack{QF\_FP}{\sat,\mv}, \withtrack{QF\_IDL}{\uc}, \withtrack{QF\_NIRA}{\seq,\paral,\unsat}, \withtrack{QF\_UFBVDT}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{QF\_UFDTLIRA}{\seq,\paral,\sat,\unsat,\fast,\uc}, \withtrack{QF\_UFLRA}{\uc}, \withtrack{QF\_UFNIA}{\sat}, \withtrack{UFDT}{\fast}, \withtrack{UFNIA}{\cloud}}{s}{s} +\newpage +\MakeOnePage{iProver}{}{\withtrack{Equality}{\paralTrack}, \withtrack{Equality+LinearArith}{\paralTrack}}{\withtrack{ANIA}{\unsat}}{s}{} +\newpage +\MakeOnePage{OpenSMT}{}{\withtrack{QF\_Equality+LinearArith}{\unsat}, \withtrack{QF\_LinearRealArith}{\sat,\inc,\mv}}{\withtrack{QF\_LIA}{\seq,\paral}, \withtrack{QF\_LRA}{\seq,\paral,\unsat,\fast}, \withtrack{QF\_UFIDL}{\seq,\paral,\sat,\mv}}{s}{s} +\newpage +\MakeOnePage{OSTRICH}{}{}{\withtrack{QF\_S}{\seq,\paral,\unsat}}{}{} +\newpage +\MakeOnePage{SMTInterpol}{\withtrack{Biggest Lead}{\fast}}{\withtrack{QF\_ADT+LinArith}{\mv}, \withtrack{QF\_Datatypes}{\fast,\uc\textsuperscript\paral,\mv}, \withtrack{QF\_Equality+LinearArith}{\seq,\paral,\sat,\inc,\mv}, \withtrack{QF\_NonLinearIntArith}{\inc}}{\withtrack{ALIA}{\sat,\uc}, \withtrack{AUFDTLIA}{\uc}, \withtrack{QF\_ALIA}{\uc}, \withtrack{QF\_ANIA}{\seq,\paral,\sat,\unsat,\fast,\inc,\uc}, \withtrack{QF\_AUFNIA}{\seq,\paral,\sat,\unsat,\fast,\uc}, \withtrack{QF\_LIA}{\unsat}, \withtrack{QF\_UF}{\uc\textsuperscript\paral}, \withtrack{QF\_UFDT}{\uc\textsuperscript\seq}, \withtrack{QF\_UFDTLIA}{\unsat,\fast,\uc}, \withtrack{UFIDL}{\sat}, \withtrack{UFLIA}{\sat}}{s}{s} +\newpage +\MakeOnePage{STP}{}{\withtrack{QF\_Bitvec}{\seq,\paral,\sat,\unsat,\fast,\mv}}{}{}{} +\newpage +\MakeOnePage{Vampire}{\withtrack{Biggest Lead}{\cloud,\paralTrack}}{\withtrack{Arith}{\cloud,\paralTrack}, \withtrack{Equality}{\fast}, \withtrack{Equality+NonLinearArith}{\cloud,\paralTrack}}{\withtrack{ALIA}{\seq,\paral,\unsat,\fast}, \withtrack{AUFLIA}{\unsat,\fast,\cloud,\paralTrack}, \withtrack{AUFLIRA}{\fast}, \withtrack{AUFNIRA}{\paral,\unsat,\fast}, \withtrack{UF}{\seq,\paral,\sat}, \withtrack{UFDTLIA}{\fast,\uc}, \withtrack{UFDTNIA}{\seq,\paral,\unsat,\fast,\uc}, \withtrack{UFLIA}{\cloud,\paralTrack}}{s}{s} +\newpage +\MakeOnePage{Yices2}{}{\withtrack{QF\_Bitvec}{\uc}, \withtrack{QF\_Equality}{\seq,\paral,\sat,\unsat,\fast,\uc,\mv}, \withtrack{QF\_Equality+Bitvec}{\uc}, \withtrack{QF\_Equality+LinearArith}{\fast,\uc}, \withtrack{QF\_Equality+NonLinearArith}{\sat}, \withtrack{QF\_LinearIntArith}{\fast,\inc,\uc}, \withtrack{QF\_LinearRealArith}{\seq,\paral,\fast,\uc}}{\withtrack{QF\_ALIA}{\unsat}, \withtrack{QF\_AUFBV}{\fast}, \withtrack{QF\_AUFBVLIA}{\inc}, \withtrack{QF\_AUFLIA}{\seq,\paral,\sat,\unsat}, \withtrack{QF\_LIRA}{\seq,\paral,\sat,\unsat,\mv}, \withtrack{QF\_RDL}{\sat,\unsat,\mv}, \withtrack{QF\_UFBVLIA}{\inc}, \withtrack{QF\_UFLIA}{\unsat,\inc}, \withtrack{QF\_UFLRA}{\seq,\paral,\sat,\unsat,\inc,\mv}, \withtrack{QF\_UFNRA}{\seq,\paral,\unsat,\fast,\inc,\mv}}{s}{s} +\newpage +\MakeOnePage{YicesQS}{}{\withtrack{Arith}{\sat,\fast}}{\withtrack{LRA}{\seq,\paral,\unsat}, \withtrack{NRA}{\seq,\paral,\unsat}}{}{s} +\newpage +\MakeOnePage{Z3-Z3++}{\withtrack{Biggest Lead}{\mv}, \withtrack{Largest Contribution}{\mv}}{\withtrack{QF\_LinearIntArith}{\seq,\paral,\sat,\mv}, \withtrack{QF\_NonLinearIntArith}{\seq,\paral,\sat,\unsat,\fast,\mv}, \withtrack{QF\_NonLinearRealArith}{\seq,\paral,\sat,\mv}}{\withtrack{QF\_IDL}{\unsat}}{s}{} +\newpage +\MakeOnePage{z3-alpha}{}{\withtrack{QF\_Strings}{\fast}}{\withtrack{QF\_S}{\sat}, \withtrack{QF\_SNIA}{\seq,\paral,\sat}}{}{s} +\newpage diff --git a/data/2025/slides/presresults/plan.txt b/data/2025/slides/presresults/plan.txt new file mode 100644 index 00000000..88a05145 --- /dev/null +++ b/data/2025/slides/presresults/plan.txt @@ -0,0 +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] 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 34: update   diff --git a/data/2025/slides/presresults/powered-by-aws.png b/data/2025/slides/presresults/powered-by-aws.png new file mode 100644 index 00000000..234fd60d Binary files /dev/null and b/data/2025/slides/presresults/powered-by-aws.png differ diff --git a/data/2025/slides/presresults/slides-Yices-2023.pdf b/data/2025/slides/presresults/slides-Yices-2023.pdf new file mode 100644 index 00000000..f2882fd7 Binary files /dev/null and b/data/2025/slides/presresults/slides-Yices-2023.pdf differ diff --git a/data/2025/slides/presresults/slides-YicesQS-2023.pdf b/data/2025/slides/presresults/slides-YicesQS-2023.pdf new file mode 100644 index 00000000..3598155d Binary files /dev/null and b/data/2025/slides/presresults/slides-YicesQS-2023.pdf differ diff --git a/data/2025/slides/presresults/slides-bitwuzla.pdf b/data/2025/slides/presresults/slides-bitwuzla.pdf new file mode 100644 index 00000000..714177fe Binary files /dev/null and b/data/2025/slides/presresults/slides-bitwuzla.pdf differ diff --git a/data/2025/slides/presresults/slides-colibri.pdf b/data/2025/slides/presresults/slides-colibri.pdf new file mode 100644 index 00000000..3cf9c0b9 Binary files /dev/null and b/data/2025/slides/presresults/slides-colibri.pdf differ diff --git a/data/2025/slides/presresults/slides-ismt-ppt.pdf b/data/2025/slides/presresults/slides-ismt-ppt.pdf new file mode 100644 index 00000000..e46d6763 Binary files /dev/null and b/data/2025/slides/presresults/slides-ismt-ppt.pdf differ diff --git a/data/2025/slides/presresults/slides-opensmt.pdf b/data/2025/slides/presresults/slides-opensmt.pdf new file mode 100644 index 00000000..d3d9ae8f Binary files /dev/null and b/data/2025/slides/presresults/slides-opensmt.pdf differ diff --git a/data/2025/slides/presresults/slides-smtinterpol.pdf b/data/2025/slides/presresults/slides-smtinterpol.pdf new file mode 100644 index 00000000..6a844050 Binary files /dev/null and b/data/2025/slides/presresults/slides-smtinterpol.pdf differ diff --git a/data/2025/slides/presresults/slides-smtrat.pdf b/data/2025/slides/presresults/slides-smtrat.pdf new file mode 100644 index 00000000..5b6f9778 Binary files /dev/null and b/data/2025/slides/presresults/slides-smtrat.pdf differ diff --git a/data/2025/slides/presresults/slides-vampire.pdf b/data/2025/slides/presresults/slides-vampire.pdf new file mode 100644 index 00000000..c93c3033 Binary files /dev/null and b/data/2025/slides/presresults/slides-vampire.pdf differ diff --git a/data/2025/slides/presresults/slides-yaga.pdf b/data/2025/slides/presresults/slides-yaga.pdf new file mode 100644 index 00000000..1c24dc5b Binary files /dev/null and b/data/2025/slides/presresults/slides-yaga.pdf differ diff --git a/data/2025/slides/presresults/slides.tex b/data/2025/slides/presresults/slides.tex new file mode 100644 index 00000000..e2a95144 --- /dev/null +++ b/data/2025/slides/presresults/slides.tex @@ -0,0 +1,1024 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% SMT-COMP 2025 - +% +% 1 hour +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\documentclass[table]{beamer} +\usepackage[utf8]{inputenc} +\usepackage{xcolor} +\usepackage{tikz} +\usetikzlibrary{shapes,shapes.callouts,automata,trees} +\usetikzlibrary{decorations.pathmorphing,external,fit} +\usetikzlibrary{calc} +\usetikzlibrary{backgrounds} %used for the CEGAR figure +\usepackage{amssymb} +\usepackage{clrscode} +\usepackage{pifont} +\usepackage{pdfpages} +\usepackage{booktabs} +\geometry{papersize={16cm,9cm}} +%\tikzexternalize +\usepackage{multicol} +\usepackage{wasysym} + +\colorlet{MYred}{red!70!black} +\definecolor{MYgreen}{rgb}{.1,.5,0} +\definecolor{MYblue}{rgb}{0,.42,.714} +\colorlet{MYgray}{white!95!MYblue} +\colorlet{MYorange}{orange!80!black} +\definecolor{gold}{rgb}{.8,.6,0} +\colorlet{silver}{white!55!black} +\colorlet{bronze}{brown!70!black} +\def\tick{\ding{52}} +\def\cross{\ding{54}} + +%%%%%%%%%%%%%%%%%%%% +%%% Beamer stuff %%% +%%%%%%%%%%%%%%%%%%%% +\usetheme{default} +\useinnertheme{rounded} +\setbeamertemplate{frametitle}[default][center] +\setbeamertemplate{footline}{\quad\hfill\footnotesize\insertframenumber\strut\kern1em\vskip2pt} +\setbeamertemplate{navigation symbols}{} +\setbeamertemplate{itemize/enumerate subbody begin}{\normalsize} +\usefonttheme[onlymath]{serif} % Nicer formulas +\setbeamercolor{block body}{bg=black!10} +\setbeamercolor{block title}{bg=black!20} + +\AtBeginSection[]{ + \begin{frame} + \vfill + \centering + \begin{beamercolorbox}[sep=8pt,center,shadow=true,rounded=true]{title} + \usebeamerfont{title}\insertsectionhead\par% + \end{beamercolorbox} + \vfill + \end{frame} +} + +\def\emph#1{\textcolor{MYblue}{#1}} + +%%% Titel, Autor und Datum des Vortrags: +\title{SMT-COMP 2025\\ +20th International Satisfiability Modulo Theory Competition} +\author{Martin Jonáš \and \emph{Fran\c{c}ois Bobot} \and David Déharbe \and Dominik Winterer} +\date{August 11, 2025} + +%% Institut +\institute{ +Masaryk University, Czechia \and +CEA List, France \and +CLEARSY, France \and +ETH Zurich, Switzerland +} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% MACROS + +% database symbol (from stackexchange) + +\makeatletter +\tikzset{ + database/.style={ + path picture={ + \draw (0, 1.5*\database@segmentheight) circle [x radius=\database@radius,y radius=\database@aspectratio*\database@radius]; + \draw (-\database@radius, 0.5*\database@segmentheight) arc [start angle=180,end angle=360,x radius=\database@radius, y radius=\database@aspectratio*\database@radius]; + \draw (-\database@radius,-0.5*\database@segmentheight) arc [start angle=180,end angle=360,x radius=\database@radius, y radius=\database@aspectratio*\database@radius]; + \draw (-\database@radius,1.5*\database@segmentheight) -- ++(0,-3*\database@segmentheight) arc [start angle=180,end angle=360,x radius=\database@radius, y radius=\database@aspectratio*\database@radius] -- ++(0,3*\database@segmentheight); + }, + minimum width=2*\database@radius + \pgflinewidth, + minimum height=3*\database@segmentheight + 2*\database@aspectratio*\database@radius + \pgflinewidth, + }, + database segment height/.store in=\database@segmentheight, + database radius/.store in=\database@radius, + database aspect ratio/.store in=\database@aspectratio, + database segment height=0.1cm, + database radius=0.25cm, + database aspect ratio=0.35, +} +\makeatother + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand\vitem{\vfill\item} + +\begin{document} + +\begin{frame} + \titlepage +\end{frame} + + +\begin{frame} + \frametitle{SMT-COMP} + + \begin{minipage}[b]{.5\textwidth} + Annual competition for \emph{SMT solvers}\\ + on (a selection of) benchmarks from \\ \emph{SMT-LIB} + \end{minipage}% + \begin{minipage}{.5\textwidth} + \begin{block}{History} + \begin{tabular}{rp{5cm}} + \textbf{2005} & first competition \\ + \textbf{2013} & evaluation instead of competition\\ + \textbf{2014} & hosted by \emph{StarExec} \\ + \textbf{2024} & hosted by \emph{LMU Munich} BenchCloud Cluster \\ + \end{tabular} + \end{block} + \end{minipage} + + \textbf{Goals} + \begin{itemize} + \item spur development of SMT solver implementations + \item promote SMT solvers and their usage + \item support the SMT-LIB project + \begin{itemize} + \item to promote and develop the SMT-LIB format (e.g., model validation) + \item to collect relevant benchmarks + \end{itemize} + \item engage and include new members + \end{itemize} + +\end{frame} + +\begin{frame} + \frametitle{SMT Solvers and SMT-LIB} + \textbf{SMT Solver} + \begin{itemize} + \item checks formulas + in \emph{SMT-LIB} format + for \emph{satisfiability modulo theories} + \end{itemize} + \bigskip + + \textbf{SMT-LIB} + \begin{enumerate} + \item a \emph{language} in which benchmarks are written + \item a community effort to \emph{collect benchmarks} + \end{enumerate} + \medskip + + \begin{columns} + \begin{column}{0.4\textwidth} + \begin{block}{Non-incremental} + 450\,474 instances \\ + with 1 query each \\ + in 90 logics + \end{block} + \end{column} + \begin{column}{0.4\textwidth} + \begin{block}{Incremental} + 44\,708 instances \\ + with 34\,163\,848 total queries \\ + in 42 logics + \end{block} + \end{column} + \begin{column}{0.08\textwidth} + \end{column} + \end{columns} + \pause + \begin{columns} + \begin{column}{0.4\textwidth} + \begin{block}{Selected Non-incremental} + 260\,089 instances (4 tracks) + \end{block} + \end{column} + \begin{column}{0.4\textwidth} + \begin{block}{Selected Incremental} + 22\,942 instances (1 track) + \end{block} + \end{column} + \begin{column}{0.08\textwidth} + \end{column} + \end{columns} + +\end{frame} + +\begin{frame} + \frametitle{Competition Overview} + + \begin{tikzpicture} + \node at (0,6) {SMT-LIB}; + \node at (3,6) {Tracks}; + \node[anchor=west] at (5,6) {Divisions}; + \node[anchor=west] at (9,6) {Logics}; + + \node[database,label=below:{\begin{tabular}{c}non-\\incremental\end{tabular}}] (nonincbench) at (0,2) {}; + \node[database,label=below:{incremental}] (incbench) at (0,0) {}; + + \node[draw,text width=1.8cm,align=center](sq) at (3,5) {single que.}; + \node[draw,text width=1.8cm,align=center](uc) at (3,4) {unsat core}; + \node[draw,text width=1.8cm,align=center](mv) at (3,3) {model val.}; + \node[draw,text width=1.8cm,align=center](par) at (3,2) {parallel}; + %\node[draw,text width=1.8cm,align=center](cloud) at (3,1) {cloud}; + \node[draw,text width=1.8cm,align=center](inc) at (3,0) {incremental}; + + \node[anchor=west] (div1) at (5,5) {Arith}; + \node[anchor=west] at (9,5) {\small LIA}; + \node[anchor=west] at (9,4.6) {\small LRA}; + \node[anchor=west] at (10,5) {\small NIA}; + \node[anchor=west] at (10,4.6) {\small NRA}; + \node[anchor=west] (div2) at (5,4) {Bitvec}; + \node[anchor=west] at (9,4) {\small BV}; + \node[anchor=west] (div3) at (5,3.4) {Equality}; + \node[anchor=west] at (9,3.4) {\small UF}; + \node[anchor=west] at (9,3) {\small UFDT}; + \node[anchor=west] (div4) at (5,2.4) {Equality+LinearArith}; + \node[anchor=west] at (9,2.4) {\small UFIDL}; + \node[anchor=west] at (9,2) {\small UFLIA}; + \node[anchor=west] at (9,1.6) {\small UFLRA}; + \node[anchor=west] at (10.5,2.4) {\small ALIA}; + \node[anchor=west] at (10.5,2) {\small AUFLIA}; + \node[anchor=west] at (10.5,1.6) {\small AUFLIRA}; + \node[anchor=west] at (12.5,2) {$\hdots$}; + \node[anchor=west] (div5) at (5,1) {Equality+MachineArith}; + \node[anchor=west] at (9,1) {\small ABV}; + \node[anchor=west] at (9,.6) {\small ABVFP}; + \node[anchor=west] at (9,.2) {\small AUFBV}; + \node[anchor=west] at (10.5,1) {\small AUFBVFP}; + \node[anchor=west] at (10.5,.6) {\small AUFBVDTLIA}; + \node[anchor=west] at (10.5,.2) {\small AUFBVDTNIA}; + \node[anchor=west] at (12.5,1) {$\hdots$}; + \node[anchor=west] (div6) at (5,-.2) {$\vdots$}; + + \draw[->,shorten <=.3em] (nonincbench) to[bend left=15] (sq.west); + \draw[->,shorten <=.3em] (nonincbench) to[bend left=7] (uc.west); + \draw[->,shorten <=.3em] (nonincbench) to[bend left=5] (mv.west); + \draw[->,shorten <=.3em] (nonincbench) to (par.west); + %\draw[->,shorten <=.3em] (nonincbench) to[bend right=4] (cloud.west); + \draw[->,shorten <=.3em] (incbench) to (inc.west); + + \draw (sq.east) to (div1.west); + \draw (sq.east) to (div2.west); + \draw (sq.east) to (div3.west); + \draw (sq.east) to (div4.west); + \draw (sq.east) to (div5.west); + \draw (sq.east) to (div6.west); + + \draw (uc.east) to (div1.west); + \draw (uc.east) to (div2.west); + \draw (uc.east) to (div3.west); + \draw (uc.east) to (div4.west); + \draw (uc.east) to (div5.west); + \draw (uc.east) to (div6.west); + + \draw (mv.east) to (div1.west); + \draw (mv.east) to (div2.west); + \draw (mv.east) to (div3.west); + \draw (mv.east) to (div4.west); + \draw (mv.east) to (div5.west); + \draw (mv.east) to (div6.west); + + %\draw (cloud.east) to (div1.west); + %\draw (cloud.east) to (div2.west); + %\draw (cloud.east) to (div3.west); + %\draw (cloud.east) to (div4.west); + %\draw (cloud.east) to (div5.west); + %\draw (cloud.east) to (div6.west); + + \draw (par.east) to (div1.west); + \draw (par.east) to (div2.west); + \draw (par.east) to (div3.west); + \draw (par.east) to (div4.west); + \draw (par.east) to (div5.west); + \draw (par.east) to (div6.west); + + \draw (inc.east) to (div1.west); + \draw (inc.east) to (div2.west); + \draw (inc.east) to (div3.west); + \draw (inc.east) to (div4.west); + \draw (inc.east) to (div5.west); + \draw (inc.east) to (div6.west); + \end{tikzpicture} + +\end{frame} + +\begin{frame}[fragile]{SMT-COMP Tracks} + \emph{Single Query (SQ) Track} + \begin{itemize} + \item determine satisfiability of one problem + \item solver answers \emph{sat/unsat/unknown} + \end{itemize} + \medskip + + \emph{Unsat Core Track} + \begin{itemize} + \item find small unsatisfiable subset of input + \item solver answers \emph{unsat + list of formulas} + \end{itemize} + \medskip + + \emph{Model Validation Track} + \begin{itemize} + \item find a model for a satisfiable problem + \item solver answers \emph{sat + value} for each toplevel symbol + \end{itemize} + \medskip + + \emph{Incremental Track} + \begin{itemize} + \item solve many small problems interactively + \item solver reads commands and answers \emph{sat/unsat} for each check + \end{itemize} + + \emph{Parallel Track} + \begin{itemize} + \item solve a complicated problem on a parallel machine (128 cores) + \item solver answers \emph{sat/unsat/unknown} + \end{itemize} +\end{frame} + +%\begin{frame}[fragile]{SMT-COMP Tracks} + +%% \emph{Model Validation} + %%\begin{itemize} + %%\item Division with quantifier-free floating-point logics + %%\item Model validation with Dolmen (thanks to Gillaume Bury and Fran\c{c}ois + %%Bobot) + %%\end{itemize} + %%\bigskip + +%% \emph{Cloud and Parallel Track} (sponsored by AWS, led by Mike Whalen) + %%\begin{itemize} + %%\item Solve a large problem over the cloud (or a big computer) + %%\begin{itemize} + %%\item 100 machines, 1600 cores, 6400 GB of memory (cloud) + %%\item 64 cores, 256 GB of memory (parallel) + %%\end{itemize} + %%\item Solver answers sat/unsat/unknown + %%\end{itemize} + + %%\pause\bigskip + + %\emph{Proof Exhibition Track} + %\begin{itemize} + %\item Solver submitted together with a checker for unsatisfiability proofs + %\item No predefined format or checker + %\item No ranking + %\item Qualitative assessment +%\end{itemize} + +%\medskip +%\pause + %\emph{As last year} the sat/unsat results from sound solvers in SQ were used to + %include benchmarks on the MV, UC and PE tracks. + +%\end{frame} + +\begin{frame}{Tracks, Solvers, Divisions, and Benchmarks} + Solvers: 26 (+6) %2022 20 + \bigskip + + \begin{center} + \begin{tabular}{lr@{}lr@{}rr} + \toprule + Track & \multicolumn{2}{c}{Solvers} & \multicolumn{2}{c}{Divisions} & Benchmarks \\ + \midrule + Single Query & 21&(+4) & &19 & 129\,361 \\ + Incremental & 7& & & 17 & 22\,942 \\ + Unsat Core & 7&(+1) && 19 & 70\,578 \\ + Model Validation & 6&(-2) & & 13 & 59\,750 \\ + Parallel & 6&(+3) & & 19 & 400 \\ + \bottomrule + \end{tabular} + \end{center} + \bigskip + + Number in parenthesis shows changes from 2024 +\end{frame} + +\begin{frame}{Infrastructure} + \textbf{Hardware} + \begin{itemize} + \item everything executed on LMU Munich machines (thanks to Dirk Beyer!) + \item cluster of 168 machines with Intel Xeon E3-1230 v5 @ 3.40 GHz CPU and 32 GiB of RAM (SQ, Incremental, UC, MV) + \item parallel machine with AMD EPYC 7713 processor -- \emph{128 virtual cores} -- and 1 TiB of RAM + \end{itemize} + + \bigskip + + \textbf{Software} + \begin{itemize} + \item everything (benchmark selection, job generation, result processing, $\ldots$) orchestrated by a Python tool \texttt{smtcomp} + \item Dolmen for model validation + \item SMT-COMP scrambler for benchmark scrambling + \item Benchexec+BenchCloud for benchmark definition and execution + \item solver submission via GitHub pull requests with JSON files + \end{itemize} +\end{frame} + +\begin{frame}{New in SMT-COMP 2025} + \begin{itemize} + \item best overall ranking + \item mandatory submission of a base solver for each derived solver + \item parallel track executed on LMU Munich machine + \item no cloud track + \item changes in resource limits + \item charts on website and comparison in results with base solver + \end{itemize} +\end{frame} + +\begin{frame} + \frametitle{Participants} + + \textbf{Multiple reasoning frameworks} + \begin{itemize} + \item CDCL(T), Saturation, MCSAT, CP + \item automata + \item finite domain + \item local search + \item besides wrappers extending the scope of existing solvers + \end{itemize} + + \bigskip + \textbf{Seven new solvers} + \begin{itemize} +%\item iProver {\footnotesize (Korovin et al.)} +%\item SMT-RAT-MCSAT {\footnotesize (Jasper Nalbach et al.)} +%\item UltimateIntBlastingWrapper+SMTInterpol {\footnotesize (Max Barth et al.)} +%\item Yaga {\footnotesize (Hanák et al.)} +%\item Z3-alpha {\footnotesize (Lu et al.)} +%\item Z3-Noodler {\footnotesize (Havlena et al.)} +%\item Z3-Owl {\footnotesize (Ma et al.)} +\item Bitwuzla-MachBV {\footnotesize (Zhang et al.)} +\item UltimateEliminator+MathSAT {\footnotesize (Barth et al.)} +\item Z3-Inc-Z3++ {\footnotesize (Li et al.)} +\item Z3-Noodler-Mocha {\footnotesize (Cui et al.)} +\item Z3-Owl {\footnotesize (Zuo et al.)} +\item bv\_decide {\footnotesize (Böving et al.)} +\item z3siri {\footnotesize (Zhou et al.)} +\item colibri2 {\footnotesize (Bobot et al.)} +\end{itemize} + +\end{frame} + +\section{Solver Presentation} + +\newcommand{\myincludepdf}[1]{ +\begin{frame} + \vspace*{-1pt}% + \noindent\makebox[\textwidth]{% + \includegraphics[height=\paperheight]{#1}} +\end{frame} +} + +\newcommand{\myvideopdf}[2]{ +\begin{frame} + \frametitle{#1} + \begin{center} + video: \texttt{#2} + \end{center} +\end{frame} +} + +\myincludepdf{solver/Bitwuzla.pdf} +%\myincludepdf{slides-colibri.pdf} + +\begin{frame} + \frametitle{COLIBRI} + + \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} + + + +\begin{frame} + \frametitle{colibri2} + + \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{solver/cvc5.pdf} + +\myincludepdf{solver/opensmt.pdf} + +\myincludepdf{solver/ostrich-smt-comp-2025.pdf} + +\myincludepdf{solver/smtinterpol.pdf} + +% \begin{frame} +% \textcolor{red}{TODO: Add solver slides received through the call} +% \end{frame} + +\begin{frame} + \frametitle{Other participants} + + \begin{center} + \begin{minipage}{0.49\textwidth} % Adjust 0.8 to control how wide the content is + \begin{itemize} + \item Amaya + \item Bitwuzla + \item Bitwuzla-MachBV + \item bv\_decide + \item bv\_decide-nokernel + \item COLIBRI + \item colibri2 + \item cvc5 + \item iProver v3.9.3 + \item OpenSMT + \item OpenSMT (min-ucore) + \item OSTRICH + \item SMT-RAT + \end{itemize} + \end{minipage} + \begin{minipage}{0.49\textwidth} % Adjust 0.8 to control how wide the content is + \begin{itemize} + \item SMTInterpol + \item SMTS + \item STP-Parti-Bitwuzla + \item UltimateEliminator+MathSAT + \item Yices2 + \item YicesQS + \item Z3-alpha + \item Z3-Inc-Z3++ + \item Z3-Noodler + \item Z3-Noodler-Mocha + \item Z3-Owl + \item Z3-Parti-Z3pp + \item z3siri + \end{itemize} + \end{minipage} + \end{center} + +\end{frame} + + + +\begin{frame} + \frametitle{Non-Competitive Solvers} + + Mandatory submission by solver authors + \begin{itemize} + \item base solver for each \emph{derived} solvers (Bitwuzla, Z3, Z3-Noodler) + \item new rule this year + \end{itemize} + + \bigskip + + Voluntary submission to show parallel speedup + \begin{itemize} + \item parallel track solvers with varied number of cores (e.g, 64, 32, 16, 8) + \end{itemize} + + \bigskip + +% Submitted by participants + %\begin{itemize} + %\item Fixed solvers (OSTRICH, Z3-Owl, Bitwuzla, Yices2, Z3-Noodler, iProver) + %\end{itemize} +\end{frame} + +\begin{frame}{Scoring} + \textbf{Computing scores} + \begin{itemize} + \item \emph{Single Query/Parallel}: number of solved \emph{instances} + \item \emph{Incremental}: number of solved \emph{queries} + \item \emph{Unsat Core}: number of top-level assertions \emph{removed} + \item \emph{Model Validation}: number of solved instances with correct \emph{models} + \end{itemize} + + \bigskip + + \textbf{Error scores} + \begin{itemize} + \item \emph{All Tracks}: given for sat reply for unsat instance, or vice versa + \item \emph{Unsat Core}: given if returned core is satisfiable. + \item \emph{Model Validation}: given if given model evaluates formula to \emph{false} + \end{itemize} + + \bigskip + Error scores are \textbf{draconian}. +\end{frame} + +\begin{frame}{Score and Ranking} + In each track we collect different scores: + \begin{itemize} + \item \emph{Sequential score} (SQ, UC, MV): all time limits apply to CPU time + \item \emph{Parallel score} (all): all time limits apply to wallclock time + \item \emph{SAT score} (SQ): parallel score for \emph{satisfiable} instances + \item \emph{UNSAT score} (SQ): parallel score for \emph{unsatisfiable} instances + \item \emph{24s} (SQ): parallel score with time limit of \emph{24s} + \end{itemize} + \bigskip + + Division ranking (for each score) + \begin{itemize} + \item For each division, one winner is declared + \end{itemize} + + \bigskip + + Competition-wide rankings (for each score) + \begin{itemize} + \item \emph{Best overall ranking}: select solver that is most universal + \item \emph{Largest contribution}: improvement each solver provided to a virtual best solver + \item \emph{Biggest lead}: division winner with most score difference to second place + \end{itemize} + +\end{frame} + +\newcommand{\seq}{\texttt{;}} +\newcommand{\paral}{\textbardbl} +\newcommand{\sat}{$\top$} +\newcommand{\unsat}{$\bot$} +\newcommand{\fast}{\texttt{24}} +\newcommand{\inc}{inc} +\newcommand{\uc}{uc} +\newcommand{\mv}{mv} +\newcommand{\cloud}{cloud} +\newcommand{\paralTrack}{parallel} + +\begin{frame} + \frametitle{Results} + + \begin{center} + \begin{tabular}{|cl|cl|} + \hline + \sat & satisfiable & \unsat & unsatisfiable \\ + \seq & sequential & \paral & parallel \\ + \fast & less than 24s & \inc & incremental \\ + \uc & unsat core & \mv & model validation \\ + \hline +\end{tabular} +\end{center} +%\vfill +%Experimental track are added in the slides but are not present +%in the certificates +\end{frame} + +{ + %\newcommand{\all}{{\footnotesize (\seq,\paral,\sat,\unsat,\fast,\inc,\uc\seq,\uc\paral,\mv)}} + \newcommand{\withtrack}[2]{\textsc{#1}{{\footnotesize (#2)}}} + +\def\newpage{} + +\newcommand{\MakeOnePage}[6]{ + \begin{frame} + \frametitle{#1} + + \medskip + \ifstrempty{#2}{}{ + \textcolor{red!30!black!90} + {\textit{Overall Winner}} + + + \textcolor{black}{\large #2} + + \medskip + } + + \ifstrempty{#3}{}{ + \textcolor{red!30!black!90} {\textit{Winner of the Division#5}} + + \textcolor{black}{\large#3} + + \medskip + } + + \ifstrempty{#4}{}{ + \textcolor{red!30!black!90} {\textit{Winner of the Logic#6 + \ifstrempty{#3}{}{(where it did not win the corresponding division)}}} + + \textcolor{black}{\large #4} + } + \vspace{2mm} + \end{frame} +} + + +\input{../../../latex-certificates/input_for_certificates.tex} + +} + +% \begin{frame}{Division Winners} +% \pause +% \emph{Single Query, sequential score} +% \begin{itemize} +% \item \emph{Bitwuzla}: {\small FPArith, QF\_Bitvec, QF\_Equality+Bitvec, QF\_FPArith} + +% \item \emph{cvc5}: \begin{minipage}{.8\textwidth}\raggedright \tiny Arith, +% Bitvec, Equality, Equality+LinearArith, Equality+MachineArith, +% Equality+NonLinearArith, QF\_Datatypes, QF\_Equality+NonLinearArith, QF\_NonLinearIntArith, QF\_NonLinearRealArith, QF\_Strings\end{minipage} + +% \item \emph{OpenSMT}: {\small QF\_LinearIntArith} + +% \item \emph{SMTInterpol}: {\small QF\_Equality+LinearArith} + +% \item \emph{Yices2}: {\small QF\_Equality, QF\_LinearRealArith} +% \end{itemize} + +% \medskip + +% \pause +% \emph{Unsat Core} +% \begin{itemize} +% \item \emph{cvc5}: Arith, Bitvec, Equality+LinearArith, Equality+MachineArith,Equality+NonLinearArith,Equality(Seq), QF\_Datatypes +% \item \emph{Vampire}: Equality(Par) +% \item \emph{Bitwuzla}: QF\_EqualityBitvec, QF\_FPArith +% \item \emph{Yices2}: QF\_Bitvec, QF\_Equality+LinearArith, QF\_Equality, QF\_LinearIntArith, QF\_LinearRealArith +% \item \emph{SMTInterpol}: QF\_Equality+NonLinearArith +% \item \emph{UltimateEliminator+MathSAT}: FPArith + +% \end{itemize} + +% \end{frame} + +% \begin{frame}{Division Winners} +% \emph{Incremental} +% \begin{itemize} +% \item \emph{cvc5}: Arith, Bitvec, Equality+LinearArith,EqualityNonLinearArith,Equality +% \item \emph{UltimateEliminator+MathSAT}: Equality+MachineArith +% \item \emph{Bitwuzla}: FPArith, QF\_FPArith +% \item \emph{Yices2}: QF\_Bitvec, QF\_Equality+Bitvec, QF\_Equality, QF\_LinearIntArith +% \item \emph{SMTInterpol}: QF\_Equality+LinearArith, QF\_Equality+NonLinearArith, QF\_NonLinearIntArith +% \item \emph{OpenSMT}: QF\_LinearRealArith +% \end{itemize} +% \medskip + +% \pause +% \emph{Model Validation (competitive only)} +% \begin{itemize} +% \item \emph{Bitwuzla}: QF\_Bitvec, QF\_Equality+Bitvec, +% \item \emph{smtinterpol}: QF\_Equality+LinearArith +% \item \emph{Yices2}: QF\_Equality +% \item \emph{Z3++}: QF\_LinearIntArith +% \item \emph{OpenSMT}: QF\_LinearRealArith + +% \item experimental: QF\_FPArith : Bitwuzla, cvc5 + +% \end{itemize} +% \end{frame} + +% \begin{frame}{Largest contribution} +% \begin{tabular}{r|c@{}lc@{}lc@{}l} +% &\textcolor{gold}{\textbf{1st Place}} && +% \textcolor{silver}{\textbf{2nd Place}} && +% \textcolor{bronze}{\textbf{3rd Place}}\\ +% \hline +% \emph{Single Query}\\ +% seq & cvc5&{\tiny(Eq+MA)} & YicesQS&{\tiny(Arith)} & Bitwuzla&{\tiny(FPArith)} \\ +% par & cvc5&{\tiny(Eq+MA)} & YicesQS&{\tiny(Arith)} & Bitwuzla&{\tiny(FPArith)} \\ +% sat & cvc5&{\tiny(Eq+LA)} & YicesQS&{\tiny(Arith)} & Bitwuzla&{\tiny(FPArith)} \\ +% unsat & cvc5&{\tiny(Eq+MA)} & Z3++&{\tiny(QF\_NonLIA)} & OSTRICH&{\tiny(QF\_Strings)}\\ +% 24 & Vampire&{\tiny(Eq+NA)} & Vampire&{\tiny(Equality)} & Yices2&{\tiny(QF\_LinIA)}\\[3pt] +% \pause +% \emph{Incremental}\\ +% par & cvc5&{\tiny(Eq+NA)} &Yices2&{\tiny(QF\_Eq+LA)} +% &SMTInterpol&{\tiny(QF\_Eq+NA)}\\[3pt] +% \pause + +% \emph{Unsat Core}\\ +% seq & cvc5&{\tiny(Eq+LA)} & +% Bitwuzla&{\tiny(QF\_Eq+Bitvec)}\\ + +% par & cvc5&{\tiny(Eq+NA)}& +% Bitwuzla&{\tiny(QF\_Eq+Bitvec)}\\ +% \\[3pt] +% \pause +% \emph{Model Validation}\\ +% seq & Z3++&{\tiny(QF\_LinIA)} & Bitwuzla&{\tiny(QF\_Bitvec)} +% & smtinterpol&{\tiny(QF\_Eq+LIA)}\\ +% par & Z3++&{\tiny(QF\_LinIA)} & Bitwuzla&{\tiny(QF\_Bitvec)} +% & smtinterpol&{\tiny(QF\_Eq+LIA)}\\ +% \end{tabular} +% \end{frame} + + +% \begin{frame}{Biggest Lead} +% \begin{tabular}{r|c@{}lc@{}lc@{}l} +% &\textcolor{gold}{\textbf{1st Place}} && +% \textcolor{silver}{\textbf{2nd Place}} && +% \textcolor{bronze}{\textbf{3rd Place}}\\ +% \hline +% \emph{Single Query}\\ +% seq & cvc5&{\tiny(QF\_DT)} & Bitwuzla&{\tiny(FPArith)} & Yices2&{\tiny(QF\_LinRA)} \\ +% par & cvc5&{\tiny(QF\_DT)} & Bitwuzla&{\tiny(FPArith)} & Yices2&{\tiny(QF\_LinRA)} \\ +% sat & cvc5&{\tiny(QF\_DT)} & Bitwuzla&{\tiny(FPArith)} & Z3++&{\tiny(QF\_NonRA)} \\ +% unsat & cvc5&{\tiny(QF\_DT)} & Z3++&{\tiny(QF\_NonIA)} & Bitwuzla&{\tiny(FPArith)} \\ +% 24 & cvc5&{\tiny(Eq+MA)} & smtinterpol&{\tiny(QF\_DT)} & Vampire&{\tiny(Equality)}\\[3pt] +% \pause +% \emph{Incremental}\\ +% par & SMTInterpol&{\tiny(QF\_NIA)} +% &Yices2&{\tiny(QF\_LinIA)} & cvc5&{\tiny(Eq+NonLA)} \\[3pt] +% \pause +% \emph{Unsat Core}\\ +% seq & cvc5&{\tiny(Eq+MA)} & Yices2&{\tiny(QF\_Eq+LA)} & smtinterpol&{\tiny(QF\_Eq+NA)} \\ +% par & cvc5&{\tiny(Eq+MA)} & Yices2&{\tiny(QF\_Eq+LA)} & smtinterpol&{\tiny(QF\_Eq+NA)} \\ +% \pause +% \emph{Model Validation}\\ +% seq & Z3++&{\tiny(QF\_LinIA)} & smtinterpol&{\tiny(QF\_LinA)} & OpenSMT&{\tiny(QF\_LinRA)} \\ +% par & Z3++&{\tiny(QF\_LinIA)} & smtinterpol&{\tiny(QF\_LinA)} & OpenSMT&{\tiny(QF\_LinRA)} \\ +% \end{tabular} +% \end{frame} + +\begin{frame}{Checking Disagreements} + + \begin{itemize} + \item 50\,978 of selected 129\,361 single query benchmarks have no known status + + \vitem 59 benchmarks with disagreements (% + NIA, + QF\_ABVFP, + QF\_S, + UFDTLIRA) + + \vitem We had 7 solvers with soundness issues: + \begin{columns} + \column{0.42\textwidth} + \begin{itemize} + \item Amaya + \item SMTInterpol + \item COLIBRI + \item UltimateEliminator+MathSAT (invalid unsat cores) + \end{itemize} + \column{0.40\textwidth} + \begin{itemize} + \item OpenSMT (invalid unsat cores) + \item OpenSMT (min-ucore) \\ (invalid unsat cores) + \item Yices2 (unsatisfiable models) + \end{itemize} +\end{columns} + + \end{itemize} + \end{frame} + +%\begin{frame}[fragile] + %\frametitle{Plans for SMT-COMP 2026} + %\begin{itemize} + %\item "Revelations are found in clouds” --- Serge King + %\item MV: Algebraic number $\implies$ non experimental +%\begin{verbatim} +%(root-of-with-ordering (coeffs p_0 p_1 ... p_n) i) + +%(root-of-with-interval (coeffs p_0 p_1 ... p_n) min max) +%(root-of-with-enclosure (coeffs p_0 p_1 ... p_n) min max) +%\end{verbatim} + %Thanks for the solvers that implemented one of them! + %\item MV: partial function more discussion needed + %\item MV: array theory more discussion needed + %\end{itemize} +%\end{frame} + +\begin{frame}{Plans for SMT-COMP 2026?} + \textbf{Resource requirements} + \begin{itemize} + \item This year: around 1 million of solver-benchmark pairs + \item Number of benchmarks and solvers steadily growing + \item How to make this sustainable? + \item Modify benchmark selection rules? + \item Reduce RAM to allow more parallel runs? + \end{itemize} + + \bigskip + \textbf{Derived Solvers} + \begin{itemize} + \item Should we allow derived solvers? + \item Should they compete in the same divisions? + \end{itemize} + + \bigskip + + \textbf{Instability track} + \begin{itemize} + \item Previous presentation \smiley + \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?} + + 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} + %\item Martin Jonáš + %\item David Déharbe + %\item Fran\c{c}ois Bobot + %\item Dominik Winterer + %\item AWS contact + %\end{itemize} + %%Fran\c{c}ois has been organizer for four-years! He can rest happy. + %\bigskip + %%We need a successor for next year's competition. + %%Contact us if you would like to volunteer! +%\end{frame} + + +\begin{frame}{Acknowledgements} + \begin{itemize} + %\item \emph{Andrea Micheli}: pysmt + %\item \emph{Guillaume Bury, FB.}: Model Validator + \item \emph{Clark Barrett, Pascal Fontaine, Aina Niemetz, Mathias Preiner, Hans-Jörg Schurr}: SMT-LIB benchmarks + %\item \emph{Aaron Stump}: StarExec support + %\item \emph{Mike Whalen and team}: Cloud/Parallel Track + \item \emph{Dirk Beyer, Philipp Wendler, and team}: BenchCloud instance at LMU + \end{itemize} + \bigskip + + \begin{columns} + \begin{column}{.3\textwidth} + \includegraphics[width=0.8\textwidth]{sosylogo.png} + \end{column} +% \begin{column}{.17\textwidth} + %\includegraphics[width=\textwidth]{powered-by-aws} + %\end{column} + \end{columns} +\end{frame} + +\begin{frame}[shrink=0.95]{Benchmark contributors} + In 2025 \emph{new benchmarks} were contributed by: + + \small + \begin{itemize} +% \item Alex Coffin + %\item Alex Ozdemir + %\item Ali Uncu, James Davenport and Matthew England + %\item Bohan Li + %\item Elizabeth Polgreen + %\item Fuqi Jia + %\item Johann-Tobias Aaron and Raphael Schäg + %\item Matthew England and Miguel Del Rio Almajano + %\item Nicolas Amat + %\item Yannick Moy + %\item Yoni Zohar + \item Johannes Bauer + \item Shaoke Cui + \item Michal Hečko + \item Hongjian Jiang + \item Bohan Li + \item Oliver Markgraf + \item Hernan Ponce de Leon + \item Hans-Jörg Schurr + \item Amar Shah + \item Yoni Zohar + \end{itemize} +\end{frame} + +\begin{frame} + + \begin{center} + \Large\emph{Thanks} + \end{center} + + \begin{center} + to all participants + \end{center} + + \bigskip + \pause + + + \begin{center} + and to you for listening + \end{center} + +\end{frame} + +\end{document} diff --git a/data/2025/slides/presresults/sosylogo.png b/data/2025/slides/presresults/sosylogo.png new file mode 100644 index 00000000..380b042a Binary files /dev/null and b/data/2025/slides/presresults/sosylogo.png differ diff --git a/data/2025/slides/presresults/starlogo.png b/data/2025/slides/presresults/starlogo.png new file mode 100644 index 00000000..b62b3575 Binary files /dev/null and b/data/2025/slides/presresults/starlogo.png differ diff --git a/smtcomp/defs.py b/smtcomp/defs.py index 1859df16..8193dcf5 100644 --- a/smtcomp/defs.py +++ b/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", } diff --git a/smtcomp/generate_graphics.py b/smtcomp/generate_graphics.py index 2c19d993..3caf7149 100644 --- a/smtcomp/generate_graphics.py +++ b/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()) diff --git a/smtcomp/results.py b/smtcomp/results.py index 3aacecd5..5de43d5b 100644 --- a/smtcomp/results.py +++ b/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, ) diff --git a/smtcomp/utils.py b/smtcomp/utils.py index 87df9295..858e6d9f 100644 --- a/smtcomp/utils.py +++ b/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)