AI 中文总结
本文提出理论模块化框架 Mosaic，结合位向量理论与整数算术理论推理判定约束 Horn 子句可满足性，其原型在比特操作基准上的性能显著优于 Spacer。
AI 中文摘要
在固定大小位向量理论（$\boldsymbol{\tau}_B$）下判定约束 Horn 子句（CHC）的可满足性是比特精确程序验证的基础，但现有最先进的 CHC 求解器常难以处理 $\boldsymbol{\tau}_B$，限制了比特精确推理的可扩展性。本文提出 Mosaic——一种理论模块化框架，用于在 $\boldsymbol{\tau}_B$ 下判定 CHC 的可满足性，方法是结合 $\boldsymbol{\tau}_B$ 与整数算术理论（$\boldsymbol{\tau}_I$）的推理。给定在 $\boldsymbol{\tau}_B$ 下的 CHC 集合，Mosaic 将其划分为分别在 $\boldsymbol{\tau}_B$ 和 $\boldsymbol{\tau}_I$ 下解释的两个片段，实现了模块化推理片段的算法，通过跨理论的可靠翻译在片段间交换信息，并判定原始 CHC 集合的可满足性。我们使用 Z3 和 Spacer 实现了 Mosaic 的原型，并在位操作基准上进行评估，结果显示 Mosaic 在这些基准上的性能显著优于 Spacer。
英文摘要
Deciding satisfiability of Constrained Horn Clauses (CHCs) modulo the theory of fixed-size bit-vectors ($\mathcal{T}_B$) is fundamental to bit-precise program verification. However, state-of-the-art CHC-solvers often struggle with $\mathcal{T}_B$, limiting scalability in bit-precise reasoning. We present Mosaic, a theory-modular framework for deciding satisfiability of CHCs modulo $\mathcal{T}_B$ by combining reasoning in $\mathcal{T}_B$ and the theory of Integer Arithmetic ($\mathcal{T}_I$). Given a CHC set modulo $\mathcal{T}_B$, Mosaic partitions it into two fragments interpreted over $\mathcal{T}_B$ and $\mathcal{T}_I$. Moreover, it implements an algorithm that reasons about the fragments in a modular fashion, exchanges information between them via sound translations across theories, and determines satisfiability w.r.t. the original CHC set. We implemented a prototype of Mosaic using Z3 and Spacer and evaluated it on bit-manipulating benchmarks. Our evaluation shows that Mosaic significantly outperforms Spacer on these benchmarks.
CommentsAccepted at ATVA 2026
