Make concat_int_array operate on sequence tuples

src/analyze/annot_fn.rs

@@ -716,17 +716,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::array_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

@@ -438,10 +438,10 @@ 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>,
+    /// The first sequence, as a `(array, length)` tuple term.
+    pub seq1: Term<V>,
+    /// The second sequence, as a `(array, length)` tuple term.
+    pub seq2: Term<V>,
 }
 
 impl<'a, D, V> Pretty<'a, D, termcolor::ColorSpec> for &ArrayConcatTerm<V>
@@ -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<V> ArrayConcatTerm<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>
     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),
+            seq1: self.seq1.subst_var(&mut f),
+            seq2: self.seq2.subst_var(f),
         }
     }
 }
@@ -772,22 +758,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 array_concat(elem_sort: Sort, seq1: Term<V>, seq2: Term<V>) -> Self {
+        Term::ArrayConcat(elem_sort, Box::new(ArrayConcatTerm { seq1, seq2 }))
     }
 
     pub fn boxed(self) -> Self {
@@ -899,12 +871,15 @@ impl<V> Term<V> {
         // 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))`
+        // `select(concat_int_array(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::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));
+            let ArrayConcatTerm { 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

@@ -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 `concat_int_array` 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)

src/chc/smtlib2.rs

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

src/chc/unbox.rs

@@ -3,22 +3,10 @@
 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,
-    }
+    let ArrayConcatTerm { seq1, seq2 } = t;
+    let seq1 = unbox_term(seq1);
+    let seq2 = unbox_term(seq2);
+    ArrayConcatTerm { seq1, seq2 }
 }
 
 fn unbox_term(term: Term) -> Term {