Logically constrained term rewrite systems (LCTRSs) are a rewriting formalism that naturally supports built-in data structures, including integers and bit-vectors. The recent framework of existentially constrained terms and most general constrained rewriting on them (Takahata et al., 2025) has many advantages over the original approach of rewriting constrained terms. In this paper, we introduce partial constrained rewriting, a variant of rewriting existentially constrained terms whose underlying idea has already appeared implicitly in previous analyses and applications of LCTRSs. We examine the differences between these two notions of constrained rewriting. First, we establish a direct correspondence between them, leveraging subsumption and equivalence of constrained terms where appropriate. Then we give characterizations of each of them, using the interpretation of existentially constrained terms by instantiation. We further introduce the novel notion of value interpretation, that highlights subtle differences between partial and most general rewriting.

翻译：逻辑约束项重写系统（LCTRSs）是一种自然支持内置数据结构（包括整数和位向量）的重写形式体系。最近提出的存在约束项及其上的最一般约束重写框架（Takahata等人，2025）相较于原始的约束项重写方法具有诸多优势。本文引入部分约束重写，这是存在约束项重写的一种变体，其基本思想已隐含出现在先前LCTRSs的分析与应用中。我们深入考察了这两种约束重写概念之间的差异。首先，通过恰当地利用约束项的蕴含与等价关系，我们在二者之间建立了直接对应关系。随后，借助存在约束项的实例化解释，我们分别给出了二者的形式化刻画。进一步地，我们引入了新颖的值解释概念，该概念凸显了部分重写与最一般重写之间的微妙差异。