Lifting Boolean-reasoning techniques to the SMT level most often requires producing theory lemmas that rule out theory-inconsistent truth assignments. With standard SMT solving, it is common to "lazily" generate such lemmas on demand during the search; with some harder SMT-level tasks -- such as unsat-core extraction, MaxSMT, T-OBDD or T-SDD compilation -- it may be beneficial or even necessary to "eagerly" pre-compute all the needed theory lemmas upfront. Whereas in principle "classic" eager SMT encodings could do the job, they are specific for very few and easy theories, they do not comply with theory combination, and may produce lots of unnecessary lemmas. In this paper, we present theory-agnostic methods for enumerating complete sets of theory lemmas tailored to a given formula. Starting from AllSMT as a baseline approach, we propose improved lemma-enumeration techniques, including divide&conquer, projected enumeration, and theory-driven partitioning, which are highly parallelizable and which may drastically improve scalability. An experimental evaluation demonstrates that these techniques significantly enhance efficiency and enable the method to scale to substantially more complex instances.

翻译：将布尔推理技术提升至SMT层面通常需要生成能够排除理论不一致真值赋值的理论引理。在标准SMT求解中，通常采用"惰性"方式在搜索过程中按需生成此类引理；而对于某些更复杂的SMT层面任务——例如不可满足核提取、MaxSMT、T-OBDD或T-SDD编译——"急切"地预先计算所有所需理论引理可能更为有利甚至必要。尽管原则上"经典"的急切SMT编码能够完成此任务，但它们仅适用于极少数简单理论，不满足理论组合要求，且可能产生大量不必要的引理。本文提出了针对给定公式枚举完备理论引理集的理论无关方法。以AllSMT作为基准方法，我们提出了改进的引理枚举技术，包括分治法、投影枚举和理论驱动的划分策略，这些技术具有高度可并行性，并能显著提升可扩展性。实验评估表明，这些技术能有效提高效率，使方法能够扩展到更复杂的实例。