Partial Rewriting and Value Interpretation of Logically Constrained Terms (Full Version)

TL;DR

This paper introduces partial constrained rewriting for logically constrained term rewrite systems, compares it with existing methods, and proposes a novel value interpretation to clarify their differences.

Contribution

It presents the concept of partial constrained rewriting, analyzes its relation to existing constrained rewriting, and introduces value interpretation for better understanding.

Findings

Establishes a correspondence between partial and most general constrained rewriting.

Provides characterizations of constrained rewriting using instantiation interpretation.

Introduces a new value interpretation to distinguish subtle differences.

Abstract

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.