From ee5d0b2f589278f4dc6102aeac128188de12c9b2 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 1 Jul 2026 20:24:03 +0000 Subject: [PATCH 1/2] Make seq concatenation operate on sequence tuples Rename `ArrayConcat`/`ArrayConcatTerm` to `SeqConcat`/`SeqConcatTerm` and the SMT `concat_int_array` definition to `seq_concat`, and have them carry the two sequences as whole `(array, length)` tuples (`seq1`/`seq2`) rather than four destructured array/length terms. The `seq_concat` definition now takes two tuple parameters and projects their fields internally instead of accepting the array and length as separate parameters, and the select peephole projects the tuple fields accordingly. The `(array, length)` tuple datatype is now always declared for every int-array element sort a `seq_concat` definition is emitted for, so the definition type-checks even when no sequence value of that element sort otherwise appears in the system. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi --- src/analyze/annot_fn.rs | 14 ++---- src/chc.rs | 89 ++++++++++++++------------------------- src/chc/format_context.rs | 17 ++++++-- src/chc/smtlib2.rs | 26 ++++++++---- src/chc/unbox.rs | 26 +++--------- src/rty.rs | 2 +- 6 files changed, 74 insertions(+), 100 deletions(-) diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs index 2392d112..aa733308 100644 --- a/src/analyze/annot_fn.rs +++ b/src/analyze/annot_fn.rs @@ -714,17 +714,9 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> { let elem_sort = self.adt_arg_type_at(receiver, 0).to_sort(); let t = self.to_term(receiver); let other = self.to_term(&args[0]); - let a_arr = t.clone().tuple_proj(0); - let a_len = t.tuple_proj(1); - let b_arr = other.clone().tuple_proj(0); - let b_len = other.tuple_proj(1); - let new_arr = chc::Term::array_concat( - elem_sort, - a_arr, - a_len.clone(), - b_arr, - b_len.clone(), - ); + let a_len = t.clone().tuple_proj(1); + let b_len = other.clone().tuple_proj(1); + let new_arr = chc::Term::seq_concat(elem_sort, t, other); let new_len = a_len.add(b_len); return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len])); } diff --git a/src/chc.rs b/src/chc.rs index 1dba68d5..f98a3111 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -437,14 +437,14 @@ impl Function { } #[derive(Debug, Clone)] -pub struct ArrayConcatTerm { - pub array1: Term, - pub len1: Term, - pub array2: Term, - pub len2: Term, +pub struct SeqConcatTerm { + /// The first sequence, as a `(array, length)` tuple term. + pub seq1: Term, + /// The second sequence, as a `(array, length)` tuple term. + pub seq2: Term, } -impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &ArrayConcatTerm +impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &SeqConcatTerm where V: Var, D: pretty::DocAllocator<'a, termcolor::ColorSpec>, @@ -454,44 +454,30 @@ where allocator .text("concat") .append(allocator.line()) - .append(self.array1.pretty_atom(allocator)) + .append(self.seq1.pretty_atom(allocator)) .append(allocator.text(",")) .append(allocator.line()) - .append(self.len1.pretty_atom(allocator)) - .append(allocator.text(",")) - .append(allocator.line()) - .append(self.array2.pretty_atom(allocator)) - .append(allocator.text(",")) - .append(allocator.line()) - .append(self.len2.pretty_atom(allocator)) + .append(self.seq2.pretty_atom(allocator)) .parens() } } -impl ArrayConcatTerm { +impl SeqConcatTerm { pub fn iter_args(&self) -> impl Iterator> { - std::iter::once(&self.array1) - .chain(std::iter::once(&self.len1)) - .chain(std::iter::once(&self.array2)) - .chain(std::iter::once(&self.len2)) + std::iter::once(&self.seq1).chain(std::iter::once(&self.seq2)) } pub fn iter_args_mut(&mut self) -> impl Iterator> { - std::iter::once(&mut self.array1) - .chain(std::iter::once(&mut self.len1)) - .chain(std::iter::once(&mut self.array2)) - .chain(std::iter::once(&mut self.len2)) + std::iter::once(&mut self.seq1).chain(std::iter::once(&mut self.seq2)) } - pub fn subst_var(self, mut f: F) -> ArrayConcatTerm + pub fn subst_var(self, mut f: F) -> SeqConcatTerm where F: FnMut(V) -> Term, { - ArrayConcatTerm { - array1: self.array1.subst_var(&mut f), - len1: self.len1.subst_var(&mut f), - array2: self.array2.subst_var(&mut f), - len2: self.len2.subst_var(f), + SeqConcatTerm { + seq1: self.seq1.subst_var(&mut f), + seq2: self.seq2.subst_var(f), } } } @@ -511,7 +497,7 @@ pub enum Term { MutFinal(Box>), App(Function, Vec>), ArrayEmpty(Sort, Sort), - ArrayConcat(Sort, Box>), + SeqConcat(Sort, Box>), Tuple(Vec>), TupleProj(Box>, usize), DatatypeCtor(DatatypeSort, DatatypeSymbol, Vec>), @@ -564,7 +550,7 @@ where } } Term::ArrayEmpty(_, _) => allocator.text("[]"), - Term::ArrayConcat(_, t) => t.pretty(allocator), + Term::SeqConcat(_, t) => t.pretty(allocator), Term::Tuple(ts) => { let separator = allocator.text(",").append(allocator.line()); if ts.len() == 1 { @@ -629,7 +615,7 @@ impl Term { Term::App(fun, args.into_iter().map(|t| t.subst_var(&mut f)).collect()) } Term::ArrayEmpty(s1, s2) => Term::ArrayEmpty(s1, s2), - Term::ArrayConcat(s, t) => Term::ArrayConcat(s, Box::new(t.subst_var(f))), + Term::SeqConcat(s, t) => Term::SeqConcat(s, Box::new(t.subst_var(f))), Term::Tuple(ts) => Term::Tuple(ts.into_iter().map(|t| t.subst_var(&mut f)).collect()), Term::TupleProj(t, i) => Term::TupleProj(Box::new(t.subst_var(f)), i), Term::DatatypeCtor(sort, c_sym, args) => Term::DatatypeCtor( @@ -677,7 +663,7 @@ impl Term { fun.sort(args.iter().map(|t| t.sort(&mut var_sort))) } Term::ArrayEmpty(index, elem) => Sort::array(index.clone(), elem.clone()), - Term::ArrayConcat(elem, _) => Sort::array(Sort::int(), elem.clone()), + Term::SeqConcat(elem, _) => Sort::array(Sort::int(), elem.clone()), Term::Tuple(ts) => { // TODO: remove this let mut var_sort: Box Sort> = Box::new(var_sort); @@ -705,7 +691,7 @@ impl Term { Term::MutCurrent(t) => t.fv_impl(), Term::MutFinal(t) => t.fv_impl(), Term::App(_, args) => Box::new(args.iter().flat_map(|t| t.fv_impl())), - Term::ArrayConcat(_, t) => Box::new(t.iter_args().flat_map(|t| t.fv_impl())), + Term::SeqConcat(_, t) => Box::new(t.iter_args().flat_map(|t| t.fv_impl())), Term::Tuple(ts) => Box::new(ts.iter().flat_map(|t| t.fv_impl())), Term::TupleProj(t, _) => t.fv_impl(), Term::DatatypeCtor(_, _, args) => Box::new(args.iter().flat_map(|t| t.fv_impl())), @@ -772,22 +758,8 @@ impl Term { Term::ArrayEmpty(index, elem) } - pub fn array_concat( - elem_sort: Sort, - array1: Term, - len1: Term, - array2: Term, - len2: Term, - ) -> Self { - Term::ArrayConcat( - elem_sort, - Box::new(ArrayConcatTerm { - array1, - len1, - array2, - len2, - }), - ) + pub fn seq_concat(elem_sort: Sort, seq1: Term, seq2: Term) -> Self { + Term::SeqConcat(elem_sort, Box::new(SeqConcatTerm { seq1, seq2 })) } pub fn boxed(self) -> Self { @@ -893,18 +865,21 @@ impl Term { ], ); } - // Peephole 2: inline one step of the `concat_int_array` recursive definitions to reduce + // Peephole 2: inline one step of the `seq_concat` recursive definitions to reduce // indexed access to terms over the underlying sequences. The SMT-defined functions are // still emitted (so the rewrites use exactly their unfolded form), but pcsat can prove // indexed properties against the inlined ITE for *any* recursion bound, where unfolding // through `define-fun-rec` would require an inductive invariant pcsat can't find. // - // `select(concat_int_array(sa, sn, ta, tn), i) - // ↦ ite(i < sn, select(sa, i), select(ta, i - sn))` - if let Term::ArrayConcat(_, t) = self { - let cond = index.clone().lt(t.len1.clone()); - let then_ = t.array1.select(index.clone()); - let else_ = t.array2.select(index.sub(t.len1)); + // `select(seq_concat(s, t), i) + // ↦ ite(i < len(s), select(array(s), i), select(array(t), i - len(s)))` + // where `s`/`t` are `(array, length)` tuples. + if let Term::SeqConcat(_, t) = self { + let SeqConcatTerm { seq1, seq2 } = *t; + let len1 = seq1.clone().tuple_proj(1); + let cond = index.clone().lt(len1.clone()); + let then_ = seq1.tuple_proj(0).select(index.clone()); + let else_ = seq2.tuple_proj(0).select(index.sub(len1)); return Term::ite(cond, then_, else_); } Term::App(Function::SELECT, vec![self, index]) diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index 7b0a76ff..86752f78 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -47,7 +47,7 @@ fn term_sorts(clause: &chc::Clause, t: &chc::Term, sorts: &mut BTreeSet {} - chc::Term::ArrayConcat(_, t) => { + chc::Term::SeqConcat(_, t) => { for arg in t.iter_args() { term_sorts(clause, arg, sorts); } @@ -269,7 +269,7 @@ fn monomorphize_datatype( impl FormatContext { pub fn from_system(system: &chc::System) -> Self { - let sorts = collect_sorts(system); + let mut sorts = collect_sorts(system); let mut datatypes = system.datatypes.clone(); for sort in sorts.iter().flat_map(|s| s.as_datatype()) { if let Some(mono_datatype) = monomorphize_datatype(sort, &datatypes) { @@ -283,6 +283,15 @@ impl FormatContext { _ => None, }) .collect(); + // The `seq_concat` definitions operate on `(array, length)` sequence tuples, so + // make sure that tuple datatype is declared for every element sort we emit one for, even + // when no sequence value of that element sort otherwise appears in the system. + for elem in &int_array_elem_sorts { + sorts.insert(chc::Sort::tuple(vec![ + chc::Sort::array(chc::Sort::int(), elem.clone()), + chc::Sort::int(), + ])); + } let datatypes: Vec<_> = sorts .into_iter() .flat_map(builtin_sort_datatype) @@ -369,9 +378,9 @@ impl FormatContext { format!("matcher_pred<{}>", self.fmt_datatype_symbol(sym)) } - pub fn concat_int_array(&self, elem: &chc::Sort) -> impl std::fmt::Display { + pub fn seq_concat(&self, elem: &chc::Sort) -> impl std::fmt::Display { let elem = SortSymbol::new(elem); - format!("concat_int_array<{}>", elem) + format!("seq_concat<{}>", elem) } fn fmt_sort_impl(&self, sort: &chc::Sort) -> Box { diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 89e1710d..c95bf75a 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -169,8 +169,8 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> { Term::new(self.ctx, self.clause, &default) ) } - chc::Term::ArrayConcat(elem, t) => { - let name = self.ctx.concat_int_array(elem); + chc::Term::SeqConcat(elem, t) => { + let name = self.ctx.seq_concat(elem); write!( f, "({} {})", @@ -639,17 +639,27 @@ impl<'a> std::fmt::Display for System<'a> { } for elem in self.ctx.int_array_elem_sorts() { - let name = self.ctx.concat_int_array(elem); + let name = self.ctx.seq_concat(elem); let elem_ty = self.ctx.fmt_sort(elem); + // The sequences are passed as `(array, length)` tuples; project their fields + // instead of taking the array and length as separate parameters. + let seq_fields = [ + chc::Sort::array(chc::Sort::int(), elem.clone()), + chc::Sort::int(), + ]; + let seq_ty = self.ctx.fmt_sort(&chc::Sort::tuple(seq_fields.to_vec())); + let ctor = self.ctx.tuple_ctor(&seq_fields); + let array = self.ctx.tuple_proj(&seq_fields, 0); + let len = self.ctx.tuple_proj(&seq_fields, 1); writeln!( f, "(define-fun-rec {name} \ - ((sa (Array Int {elem_ty})) (sn Int) (ta (Array Int {elem_ty})) (tn Int)) \ + ((s {seq_ty}) (t {seq_ty})) \ (Array Int {elem_ty}) \ - (ite (<= tn 0) sa \ - (store ({name} sa sn ta (- tn 1)) \ - (+ sn (- tn 1)) \ - (select ta (- tn 1)))))\n", + (ite (<= ({len} t) 0) ({array} s) \ + (store ({name} s ({ctor} ({array} t) (- ({len} t) 1))) \ + (+ ({len} s) (- ({len} t) 1)) \ + (select ({array} t) (- ({len} t) 1)))))\n", )?; } diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index b13ab96c..3fa22595 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -2,23 +2,11 @@ use super::*; -fn unbox_array_concat_term(t: ArrayConcatTerm) -> ArrayConcatTerm { - let ArrayConcatTerm { - array1, - len1, - array2, - len2, - } = t; - let array1 = unbox_term(array1); - let len1 = unbox_term(len1); - let array2 = unbox_term(array2); - let len2 = unbox_term(len2); - ArrayConcatTerm { - array1, - len1, - array2, - len2, - } +fn unbox_seq_concat_term(t: SeqConcatTerm) -> SeqConcatTerm { + let SeqConcatTerm { seq1, seq2 } = t; + let seq1 = unbox_term(seq1); + let seq2 = unbox_term(seq2); + SeqConcatTerm { seq1, seq2 } } fn unbox_term(term: Term) -> Term { @@ -31,8 +19,8 @@ fn unbox_term(term: Term) -> Term { Term::MutFinal(t) => Term::MutFinal(Box::new(unbox_term(*t))), Term::App(fun, args) => Term::App(fun, args.into_iter().map(unbox_term).collect()), Term::ArrayEmpty(s1, s2) => Term::ArrayEmpty(unbox_sort(s1), unbox_sort(s2)), - Term::ArrayConcat(s, t) => { - Term::ArrayConcat(unbox_sort(s), Box::new(unbox_array_concat_term(*t))) + Term::SeqConcat(s, t) => { + Term::SeqConcat(unbox_sort(s), Box::new(unbox_seq_concat_term(*t))) } Term::Tuple(ts) => Term::Tuple(ts.into_iter().map(unbox_term).collect()), Term::TupleProj(t, i) => Term::TupleProj(Box::new(unbox_term(*t)), i), diff --git a/src/rty.rs b/src/rty.rs index 35e07769..ed3d8529 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1978,7 +1978,7 @@ fn subst_ty_params_in_term(term: &mut chc::Term, subst: &TypeParamSubst subst_ty_params_in_sort(s1, subst); subst_ty_params_in_sort(s2, subst); } - chc::Term::ArrayConcat(sort, t) => { + chc::Term::SeqConcat(sort, t) => { subst_ty_params_in_sort(sort, subst); for arg in t.iter_args_mut() { subst_ty_params_in_term(arg, subst); From afa938f0005d86700a535cd65065ee12d59a4d6c Mon Sep 17 00:00:00 2001 From: coord_e Date: Thu, 2 Jul 2026 18:49:37 +0900 Subject: [PATCH 2/2] fixup! Make seq concatenation operate on sequence tuples --- src/chc.rs | 2 -- src/chc/format_context.rs | 3 +-- src/chc/smtlib2.rs | 3 +-- 3 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/chc.rs b/src/chc.rs index f98a3111..b70112c0 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -438,9 +438,7 @@ impl Function { #[derive(Debug, Clone)] pub struct SeqConcatTerm { - /// The first sequence, as a `(array, length)` tuple term. pub seq1: Term, - /// The second sequence, as a `(array, length)` tuple term. pub seq2: Term, } diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs index 86752f78..b0f5f782 100644 --- a/src/chc/format_context.rs +++ b/src/chc/format_context.rs @@ -284,8 +284,7 @@ impl FormatContext { }) .collect(); // The `seq_concat` definitions operate on `(array, length)` sequence tuples, so - // make sure that tuple datatype is declared for every element sort we emit one for, even - // when no sequence value of that element sort otherwise appears in the system. + // make sure that tuple datatype is declared for every element sort we emit one for for elem in &int_array_elem_sorts { sorts.insert(chc::Sort::tuple(vec![ chc::Sort::array(chc::Sort::int(), elem.clone()), diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index c95bf75a..b27982a9 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -641,8 +641,7 @@ impl<'a> std::fmt::Display for System<'a> { for elem in self.ctx.int_array_elem_sorts() { let name = self.ctx.seq_concat(elem); let elem_ty = self.ctx.fmt_sort(elem); - // The sequences are passed as `(array, length)` tuples; project their fields - // instead of taking the array and length as separate parameters. + // The sequences are passed as `(array, length)` tuples let seq_fields = [ chc::Sort::array(chc::Sort::int(), elem.clone()), chc::Sort::int(),