Automatic static cost analysis infers information about the resources used by programs without actually running them with concrete data, and presents such information as functions of input data sizes. Most of the analysis tools for logic programs (and many for other languages), as CiaoPP, are based on setting up recurrence relations representing (bounds on) the computational cost of predicates, and solving them to find closed-form functions. Such recurrence solving is a bottleneck in current tools: many of the recurrences that arise during the analysis cannot be solved with state-of-the-art solvers, including Computer Algebra Systems (CASs), so that specific methods for different classes of recurrences need to be developed. We address such a challenge by developing a novel, general approach for solving arbitrary, constrained recurrence relations, that uses machine-learning (sparse-linear and symbolic) regression techniques to guess a candidate closed-form function, and a combination of an SMT-solver and a CAS to check if it is actually a solution of the recurrence. Our prototype implementation and its experimental evaluation within the context of the CiaoPP system show quite promising results. Overall, for the considered benchmarks, our approach outperforms state-of-the-art cost analyzers and recurrence solvers, and solves recurrences that cannot be solved by them. Under consideration in Theory and Practice of Logic Programming (TPLP).

翻译：自动静态成本分析可在不实际运行程序具体数据的情况下推断程序使用的资源信息，并以输入数据规模的函数形式呈现此类信息。大多数逻辑程序（及许多其他语言）的分析工具（如CiaoPP）都基于建立表示谓词计算成本（上界）的递归关系，并通过求解这些递归关系来获得闭式函数。此类递归求解是当前工具的瓶颈：分析过程中产生的许多递归关系无法通过现有求解器（包括计算机代数系统）解决，因此需要针对不同类型的递归关系开发特定方法。我们通过开发一种新颖的通用方法来解决这一挑战，该方法可求解任意约束递归关系：首先使用机器学习（稀疏线性与符号）回归技术推测候选闭式函数，然后结合SMT求解器与计算机代数系统验证其是否为递归关系的实际解。我们在CiaoPP系统中实现的原理系统及其实验评估显示出相当有前景的结果。总体而言，在所考虑的基准测试中，我们的方法优于现有成本分析器和递归求解器，并能解决它们无法处理的递归关系。本文已投稿至《逻辑程序设计的理论与实践》（TPLP）期刊。