Make seq concatenation operate on sequence tuples

[coord-e]

Summary

PR 2 of 4 restructuring #153. Now that #161 is merged, this is based directly on main.

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. The select peephole projects the tuple fields accordingly.

Details

• 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.

Validation

• cargo build, cargo fmt --all -- --check, cargo clippy -- -D warnings
• cargo test — Spacer-backed tests pass.
• The rewritten define-fun-rec was dumped via THRUST_OUTPUT_DIR and checked directly with z3: it emits as seq_concat<…>, parses, and on a ground instance evaluates the concatenation exactly as before. (PCSat-backed tests require the CoAR Docker image and were not run here.)

Stack

1. named fields (Give the Seq model named array and length fields #161, merged)
2. this PR — seq concatenation on sequence tuples
3. offset field (Add an offset field to the Seq model #163)
4. subsequence + split_first/split_last(_mut) (Add subsequence and slice split operations #164)

🤖 Generated with Claude Code

https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi

[coord-e]

@codex review

[Copilot]

Pull request overview

This PR is part of the #153 restructuring stack and refactors sequence concatenation in the CHC/SMT encoding to operate on whole sequence tuples (array, length) rather than separate (array1, len1, array2, len2) arguments. This aligns the concat machinery with the named-field Seq { array, length } representation introduced in #161 and centralizes tuple field projection inside the emitted SMT definition.

Changes:

• Renamed ArrayConcat/ArrayConcatTerm to SeqConcat/SeqConcatTerm, and renamed the SMT definition concat_int_array to seq_concat.
• Updated the SMT define-fun-rec emission so seq_concat takes two sequence tuple parameters and projects (array, length) internally.
• Updated the select peephole rewrite to project tuple fields (array(s), len(s)) from concat arguments, and ensured needed tuple datatypes are declared for all emitted seq_concat element sorts.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
src/rty.rs	Updates type-parameter substitution logic to handle the renamed SeqConcat term variant.
src/chc/unbox.rs	Updates term unboxing to handle SeqConcatTerm { seq1, seq2 } rather than four concat components.
src/chc/smtlib2.rs	Switches SMT printing/emission from concat_int_array to tuple-based seq_concat and updates the define-fun-rec signature/body accordingly.
src/chc/format_context.rs	Ensures (array, length) tuple datatypes are included in declared sorts for every element sort that gets a seq_concat definition; renames formatter helper to seq_concat.
src/chc.rs	Renames the term/term-struct, updates free-var/substitution/sort/pretty plumbing, and updates the select peephole to project tuple fields from concat args.
src/analyze/annot_fn.rs	Updates Seq::concat lowering to emit chc::Term::seq_concat(elem_sort, seq1, seq2) and compute the new length separately.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. What shall we delve into next?

Reviewed commit: afa938f000

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".