Nikolaj Bjørner

Weak monadic second-order logic (wMSO) is a foundational tool for specifying regular properties. Traditional decision procedures for this logic typically translate wMSO formulas into finite automata. Although the logic is decidable, this approach incurs non-elementary complexity in the worst-case. Nearly thirty years ago, the state-of-the-art MONA tool showed that, despite these theoretical limits, wMSO can be decided efficiently in practice through carefully optimized automata constructions. We revisit wMSO from an algebraic perspective by introducing Extended Regular Expressions with Quantifiers (EREQ). Instead of relying on automata determinization, EREQ employs symbolic derivatives to perform incremental quantifier elimination, providing a compositional and symbolic alternative to classical automata-based approaches. We present a linear-time translation of wMSO into EREQ and a derivative-based decision procedure for EREQ. We prove the correctness of the translation and of the derivative construction in the Lean proof assistant. We implement our approach in Rust and evaluate it on a set of established MONA benchmarks, demonstrating competitive performance with state-of-the-art tools. Our results demonstrate the potential of derivative-based methods, opening new avenues for efficient decision procedures in EREQ.

We present a new approach for solving string equations as extensions of Nielsen transformations. Key to our work are the combination of three techniques: a power operator for strings; generalisations of Parikh images; and equality decomposition. Using these methods allows us to solve complex string equations, including less commonly encountered SMT inputs over strings.

The theory of arithmetic is integral to many uses of SMT solvers. Z3 has implemented native solvers for arithmetic reasoning since its first release. We present a full re-implementation of Z3’s original arithmetic solver. It is based on substantial experiences from user feedback, engineering and experimentation. While providing a comprehensive overview of the main components we emphasize selected new insights we arrived at while developing and testing the solver.

We present S p EQ, a quick and correct strategy for detecting semantics in sparse codes and enabling automatic translation to high-performance library calls or domain-specific languages (DSLs). When sparse linear algebra codes contain implicit preconditions about how data is stored that hamper direct translation, S p EQ identifies the high-level computation along with storage details and related preconditions. A run-time check guards the translation and ensures that required preconditions are met. We implement S p EQ using the LLVM framework, the Z3 solver, and egglog library and correctly translate sparse linear algebra codes into two high-performance libraries, NVIDIA cuSPARSE and Intel MKL, and OpenMP (OMP). We evaluate S p EQ on ten diverse benchmarks against two state-of-the-art translation tools. S p EQ achieves geometric mean speedups of 3.25 × , 5.09 × , and 8.04 × on OpenMP, MKL, and cuSPARSE backends, respectively. S p EQ is the only tool that can guarantee the correct translation of sparse computations.

We introduce a calculus for incremental pre-processing for SMT and instantiate it in the context of z3. It identifies when powerful formula simplifications can be retained when adding new constraints. Use cases that could not be solved in incremental mode can now be solved incrementally thanks to the availability of pre-processing. Our approach admits a class of transformations that preserve satisfiability, but not equivalence. We establish a taxonomy of pre-processing techniques that distinguishes cases where new constraints are modified or constraints previously added have to be replayed. We then justify the soundness of the proposed incremental pre-processing calculus.