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求解器，其中包含许多涉及非线性整数算术的实例。