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 great 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.

翻译：求解约束霍恩子句（CHC）是广泛验证与分析任务背后的基础性挑战。数据驱动方法在无需人工费心构建与调整各种启发式策略的前提下，为改进CHC求解展现了巨大潜力。然而，数据驱动型CHC求解器与基于符号推理的求解器之间仍存在显著的性能差距。本研究提出了一种简洁而高效的框架——"符号时间学习"，该框架将符号信息与数值数据点相统一，以高效求解CHC系统。同时，我们给出了符号时间学习的一个简单实例，其中包含数据驱动学习器与BMC风格推理器。尽管其设计极为简洁，实验结果表明我们的工具具有高效性与鲁棒性。该工具在包含288个基准测试的数据集上超越了现有最先进的CHC求解器，其中涵盖大量含非线性整数算术的实例。