Satisfiability Modulo Theories (SMT) specifications often rely on quantifiers to remain concise and declarative. However, checking the satisfiability of such specifications directly can be inefficient. A common optimization is to ground the specification - that is, to expand quantified formulas into equivalent variable-free formulas. While dedicated tools known as grounders are a cornerstone of Answer Set Programming (ASP) solvers, they are are largely absent from SMT solving workflows. As a result, users frequently resort to writing ad-hoc, error-prone code to perform this transformation. In this work, I propose a theoretical framework for grounding first order logic formulas with aggregates, based on relational algebra. Within this framework, I formulate a method for efficiently grounding such formulas. Remarkably, the method allows certain formulas that quantify over infinite domains to be transformed into equivalent formulas of finite size. I have implemented this method in a new SMT-LIB grounder, called xmt-lib. It leverages an embedded relational database (SQLite) to execute relational operations efficiently. An evaluation on a public benchmark for grounders demonstrates that xmt-lib significantly improves the performance of the Z3 SMT solver compared to its purely declarative use, and makes it com

翻译：暂无翻译