邏輯限制重寫系統(LCTRSs)是一種通用且高效的重寫形式，可用于對來自各種程式設計範例的程式模組化，也可用于編譯器和SMT求解器中的簡化系統。在本文中，我們研究了分析LCTRSs的最壞情況運作複雜度的技術。為此，我們利用Avanzini等人先前開發的用于标準項重寫的分解技術與Brockschmidt等人的整數程式的時間和大小邊界交替逼近之間的協同效應，并将這些技術适應于LCTRSs。此外，我們提供了新的子產品化技術，以利用循環方程的環界産生次線性界。我們已經在TCT中實施了該方法，用以檢驗我們的方法的可行性。
原文：Logically constrained rewrite systems (LCTRSs) are a versatile and efficient rewriting formalism that can be used to model programs from various programming paradigms, as well as simplification systems in compilers and SMT solvers. In this paper, we investigate techniques to analyse the worst-case runtime complexity of LCTRSs. For that, we exploit synergies between previously developed decomposition techniques for standard term rewriting by Avanzini et al. in conjunction with alternating time and size bound approximations for integer programs by Brockschmidt et al. and adapt these techniques suitably to LCTRSs. Furthermore, we provide novel modularization techniques to exploit loop bounds from recurrence equations which yield sublinear bounds. We have implemented the method in TCT to test the viability of our method.
Runtime Complexity Analysis of Logically Constrained Rewriting.pdf