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

翻译：可满足性模理论（SMT）规范通常依赖量词以保持简洁性和声明性。然而，直接检查此类规范的可满足性可能效率低下。一种常见的优化方法是基础化规范——即将量化公式展开为等价的无变量公式。尽管被称为基础化器的专用工具是答案集编程（ASP）求解器的核心组件，但它们在SMT求解工作流中却基本缺失。因此，用户经常需要编写临时性的、易出错的代码来执行此转换。在本工作中，我提出了一个基于关系代数的、包含聚合操作的一阶逻辑公式基础化理论框架。在此框架内，我构建了一种高效基础化此类公式的方法。值得注意的是，该方法允许将某些在无限域上量化的公式转换为有限规模的等价公式。我已将此方法实现于名为xmt-lib的新型SMT-LIB基础化器中。该工具利用嵌入式关系数据库（SQLite）高效执行关系运算。在公开的基础化器基准测试上的评估表明，与纯声明性使用方式相比，xmt-lib显著提升了Z3 SMT求解器的性能，并使其能够处理