Make seq concatenation operate on sequence tuples

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