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的分析与应用中已隐式出现。我们考察这两种约束重写概念之间的差异。首先，我们通过适当地利用约束项的包含关系与等价性，在二者之间建立直接对应关系。随后，我们借助存在约束项的实例化解释，分别给出二者的特征刻画。我们进一步引入值解释这一新概念，以凸显部分重写与最一般重写之间的微妙差异。