Make seq concatenation operate on sequence tuples (#162)

* 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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi

* fixup! Make seq concatenation operate on sequence tuples

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: coord-e

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]));
                     }

src/chc.rs

@@ -437,14 +437,12 @@ impl Function {
 }
 
 #[derive(Debug, Clone)]
-pub struct ArrayConcatTerm<V = TermVarIdx> {
-    pub array1: Term<V>,
-    pub len1: Term<V>,
-    pub array2: Term<V>,
-    pub len2: Term<V>,
+pub struct SeqConcatTerm<V = TermVarIdx> {
+    pub seq1: Term<V>,
+    pub seq2: Term<V>,
 }
 
-impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &ArrayConcatTerm<V>
+impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &SeqConcatTerm<V>
 where
     V: Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
@@ -454,44 +452,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<V> ArrayConcatTerm<V> {
+impl<V> SeqConcatTerm<V> {
     pub fn iter_args(&self) -> impl Iterator<Item = &Term<V>> {
-        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<Item = &mut Term<V>> {
-        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<F, W>(self, mut f: F) -> ArrayConcatTerm<W>
+    pub fn subst_var<F, W>(self, mut f: F) -> SeqConcatTerm<W>
     where
         F: FnMut(V) -> Term<W>,
     {
-        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 +495,7 @@ pub enum Term<V = TermVarIdx> {
     MutFinal(Box<Term<V>>),
     App(Function, Vec<Term<V>>),
     ArrayEmpty(Sort, Sort),
-    ArrayConcat(Sort, Box<ArrayConcatTerm<V>>),
+    SeqConcat(Sort, Box<SeqConcatTerm<V>>),
     Tuple(Vec<Term<V>>),
     TupleProj(Box<Term<V>>, usize),
     DatatypeCtor(DatatypeSort, DatatypeSymbol, Vec<Term<V>>),
@@ -564,7 +548,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 +613,7 @@ impl<V> Term<V> {
                 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 +661,7 @@ impl<V> Term<V> {
                 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<dyn FnMut(&V) -> Sort> = Box::new(var_sort);
@@ -705,7 +689,7 @@ impl<V> Term<V> {
             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 +756,8 @@ impl<V> Term<V> {
         Term::ArrayEmpty(index, elem)
     }
 
-    pub fn array_concat(
-        elem_sort: Sort,
-        array1: Term<V>,
-        len1: Term<V>,
-        array2: Term<V>,
-        len2: Term<V>,
-    ) -> Self {
-        Term::ArrayConcat(
-            elem_sort,
-            Box::new(ArrayConcatTerm {
-                array1,
-                len1,
-                array2,
-                len2,
-            }),
-        )
+    pub fn seq_concat(elem_sort: Sort, seq1: Term<V>, seq2: Term<V>) -> Self {
+        Term::SeqConcat(elem_sort, Box::new(SeqConcatTerm { seq1, seq2 }))
     }
 
     pub fn boxed(self) -> Self {
@@ -893,18 +863,21 @@ impl<V> Term<V> {
                 ],
             );
         }
-        // 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])

src/chc/format_context.rs

@@ -47,7 +47,7 @@ fn term_sorts(clause: &chc::Clause, t: &chc::Term, sorts: &mut BTreeSet<chc::Sor
             }
         }
         chc::Term::ArrayEmpty(_, _) => {}
-        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,14 @@ 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
+        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 +377,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<dyn std::fmt::Display> {

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,26 @@ 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
+            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",
             )?;
         }
 

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),

src/rty.rs

@@ -1978,7 +1978,7 @@ fn subst_ty_params_in_term<T, V>(term: &mut chc::Term<V>, 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);