Solving Constrained Horn Clauses (CHCs) is a fundamental challenge behind a wide range of verification and analysis tasks. Data-driven approaches show great promise in improving CHC solving without the painstaking manual effort of creating and tuning various heuristics. However, a large performance gap exists between data-driven CHC solvers and symbolic reasoning-based solvers. In this work, we develop a simple but effective framework, "Chronosymbolic Learning", which unifies symbolic information and numerical data points to solve a CHC system efficiently. We also present a simple instance of Chronosymbolic Learning with a data-driven learner and a BMC-styled reasoner. Despite its relative simplicity, experimental results show the efficacy and robustness of our tool. It outperforms state-of-the-art CHC solvers on a dataset consisting of 288 benchmarks, including many instances with non-linear integer arithmetics.

翻译：求解约束霍恩子句（CHCs）是众多验证与分析任务背后的核心挑战。数据驱动方法在改进CHC求解方面展现出巨大潜力，无需耗费大量人力手工构建与调整各类启发式策略。然而，当前数据驱动的CHC求解器与基于符号推理的求解器之间仍存在显著的性能差距。本研究提出一种简洁而有效的框架——“时序符号学习”，通过融合符号信息与数值数据点来实现对CHC系统的高效求解。我们同时展示了一个结合数据驱动学习器与BMC风格推理器的时序符号学习基础实例。尽管该框架相对简单，实验结果表明我们的工具具有优异的效能与鲁棒性。在包含288个基准测试（含大量非线性整数算术实例）的数据集上，本工具性能优于当前最先进的CHC求解器。