Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version)
Kanta Takahata, Jonas Schöpf, Naoki Nishida, Takahito Aoto
TL;DR
This paper tackles the practical challenge in logically constrained term rewriting (LCTRSs) where rewrite steps and equivalence transformations create combinatorial search spaces. It introduces most general constrained rewriting on existentially constrained terms, proving well-definedness, and establishing uniqueness of reducts and commutation with equivalence for pattern-general terms. By relating to and embedding existing non-quantified constrained rewriting, it provides a solid theoretical bridge and foundation for correct, efficient implementations. A key contribution is transforming arbitrary constrained rewrite rules into left-value-free form (lvf) and proving that commutation with equivalence can be preserved, enabling postponement of equivalence steps in rewrite sequences and improving tool scalability.
Abstract
Logically constrained term rewriting is a relatively new rewriting formalism that naturally supports built-in data structures, such as integers and bit vectors. In the analysis of logically constrained term rewrite systems (LCTRSs), rewriting constrained terms plays a crucial role. However, this combines rewrite rule applications and equivalence transformations in a closely intertwined way. This intertwining makes it difficult to establish useful theoretical properties for this kind of rewriting and causes problems in implementations -- namely, that impractically large search spaces are often required. To address this issue, we propose in this paper a novel notion of most general constrained rewriting, which operates on existentially constrained terms, a concept recently introduced by the authors. We define a class of left-linear, left-value-free LCTRSs that are general enough to simulate all left-linear LCTRSs and exhibit the desired key property: most general constrained rewriting commutes with equivalence. This property ensures that equivalence transformations can be deferred until after the application of rewrite rules, which helps mitigate the issue of large search spaces in implementations. In addition to that, we show that the original rewriting formalism on constrained terms can be embedded into our new rewriting formalism on existentially constrained terms. Thus, our results are expected to have significant implications for achieving correct and efficient implementations in tools operating on LCTRSs.