一句话：提出反馈驱动的 Orax 框架，在 SMT 求解器与 oracle 处理器间闭环反馈 oracle 映射信息，高效求解 SMTO 问题。
开放程序常依赖第三方库等缺少形式规约的组件，其行为可观测但实现未知，这类 oracle 使传统 SMT 求解器难以推理，形成可满足性模理论与预言机（SMTO）问题。现有 Delphi 与 Saadhak 难以有效结合构建可行解所需的 oracle 映射信息与 SMT 推理能力。本文提出 Orax 求解框架，在 SMT 求解器与 oracle 处理器之间建立 oracle 映射信息反馈闭环：求解器分析自身已有映射信息的不足并反馈，处理器据此提供最合适的补充映射信息；Orax 还采用双聚类策略选择初始映射信息，并用基于松弛的方法分析映射信息缺陷。基准实验表明，Orax 比 Delphi 和 Saadhak 分别多求解 118.37% 与 13.83% 的基准，PAR-2 为 1.39，显著优于后两者的 669.13 和 173.31。
Recent advancements in Satisfiability Modulo Theory (SMT) solving have significantly improved formula-driven techniques for verification, testing, repair, and synthesis. However, addressing open programs that lack formal specifications, such as those relying on third-party libraries, remains a challenge. The problem of Satisfiability Modulo Theories and Oracles (SMTO) has emerged as a critical issue where oracles, representing components with observable behavior but unknown implementation, hinder SMT solver from reasoning. Existing approaches like Delphi and Saadhak struggle to effectively combine sufficient oracle mapping information that is crucial for feasible solution construction with the reasoning capabilities of the SMT solver, leading to inefficient solving of SMTO problems. In this work, we propose a novel solving framework for SMTO problems, Orax , which establishes an oracle mapping information feedback loop between the SMT solver and the oracle handler. In Orax , the SMT solver analyzes the deficiency in oracle mapping information it has and feeds this back to the oracle handler. The oracle handler then provides the most suitable additional oracle mapping information back to the SMT solver. Orax employs a dual-clustering strategy to select the initial oracle mapping information provided to the SMT solver and a relaxation-based method to analyze the deficiency in the oracle mapping information the SMT solver knows. Experimental results on the benchmark suite demonstrate that Orax outperforms existing methods, solving 118.37% and 13.83% more benchmarks than Delphi and Saadhak, respectively. In terms of efficiency, Orax achieves a PAR-2 score of 1.39, significantly exceeding Delphi’s score of 669.13 and Saadhak’s score of 173.31.
@article{paperbot3183,
title = {Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles},
author = {Zhineng Zhong and Ziqi Zhang and Hanqin Guan and Ding Li},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720438}
}