Encode slice operations with with an array lambda

src/analyze/annot.rs

@@ -162,6 +162,14 @@ pub fn seq_push_path() -> [Symbol; 3] {
     ]
 }
 
+pub fn seq_subsequence_path() -> [Symbol; 3] {
+    [
+        Symbol::intern("thrust"),
+        Symbol::intern("def"),
+        Symbol::intern("seq_subsequence"),
+    ]
+}
+
 pub fn seq_concat_path() -> [Symbol; 3] {
     [
         Symbol::intern("thrust"),

src/analyze/annot_fn.rs

@@ -852,6 +852,16 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                         let new_len = len.add(chc::Term::int(1));
                         return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len]));
                     }
+                    if Some(def_id) == self.def_ids.seq_subsequence() {
+                        assert_eq!(args.len(), 2, "Seq::subsequence takes exactly 2 arguments");
+                        let t = self.to_term(receiver);
+                        let start = self.to_term(&args[0]);
+                        let end = self.to_term(&args[1]);
+                        let arr = t.tuple_proj(0);
+                        let new_len = end.sub(start.clone());
+                        let new_arr = chc::Term::subarray(arr, start, new_len.clone());
+                        return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len]));
+                    }
                     if Some(def_id) == self.def_ids.seq_concat() {
                         assert_eq!(args.len(), 1, "Seq::concat takes exactly 1 argument");
                         let elem_sort = self.adt_arg_type_at(receiver, 0).to_sort();

src/analyze/did_cache.rs

@@ -29,6 +29,7 @@ struct DefIds {
     seq_singleton: OnceCell<Option<DefId>>,
     seq_len: OnceCell<Option<DefId>>,
     seq_push: OnceCell<Option<DefId>>,
+    seq_subsequence: OnceCell<Option<DefId>>,
     seq_concat: OnceCell<Option<DefId>>,
 
     exists: OnceCell<Option<DefId>>,
@@ -222,6 +223,13 @@ impl<'tcx> DefIdCache<'tcx> {
             .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_push_path()))
     }
 
+    pub fn seq_subsequence(&self) -> Option<DefId> {
+        *self
+            .def_ids
+            .seq_subsequence
+            .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_subsequence_path()))
+    }
+
     pub fn seq_concat(&self) -> Option<DefId> {
         *self
             .def_ids

src/chc.rs

@@ -221,6 +221,13 @@ impl Sort {
         }
     }
 
+    pub fn as_array_elem(&self) -> Option<&Sort> {
+        match self {
+            Sort::Array(_, elem) => Some(elem),
+            _ => None,
+        }
+    }
+
     pub fn null() -> Self {
         Sort::Null
     }
@@ -495,6 +502,9 @@ pub enum Term<V = TermVarIdx> {
     MutFinal(Box<Term<V>>),
     App(Function, Vec<Term<V>>),
     ArrayEmpty(Sort, Sort),
+    /// A view whose index `i` reads `array[start + i]` within `[0, length)`.
+    /// Outside the view, a shared default prevents equality from constraining the backing array.
+    Subarray(Box<Term<V>>, Box<Term<V>>, Box<Term<V>>),
     SeqConcat(Sort, Box<SeqConcatTerm<V>>),
     Tuple(Vec<Term<V>>),
     TupleProj(Box<Term<V>>, usize),
@@ -548,6 +558,17 @@ where
                 }
             }
             Term::ArrayEmpty(_, _) => allocator.text("[]"),
+            Term::Subarray(arr, start, length) => allocator
+                .text("subarray")
+                .append(allocator.line())
+                .append(arr.pretty_atom(allocator))
+                .append(allocator.text(","))
+                .append(allocator.line())
+                .append(start.pretty_atom(allocator))
+                .append(allocator.text(","))
+                .append(allocator.line())
+                .append(length.pretty_atom(allocator))
+                .parens(),
             Term::SeqConcat(_, t) => t.pretty(allocator),
             Term::Tuple(ts) => {
                 let separator = allocator.text(",").append(allocator.line());
@@ -613,6 +634,11 @@ 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::Subarray(arr, start, length) => Term::Subarray(
+                Box::new(arr.subst_var(&mut f)),
+                Box::new(start.subst_var(&mut f)),
+                Box::new(length.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),
@@ -661,6 +687,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::Subarray(arr, _, _) => arr.sort(var_sort),
             Term::SeqConcat(elem, _) => Sort::array(Sort::int(), elem.clone()),
             Term::Tuple(ts) => {
                 // TODO: remove this
@@ -689,6 +716,9 @@ 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::Subarray(arr, start, length) => {
+                Box::new(arr.fv_impl().chain(start.fv_impl()).chain(length.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(),
@@ -760,6 +790,10 @@ impl<V> Term<V> {
         Term::SeqConcat(elem_sort, Box::new(SeqConcatTerm { seq1, seq2 }))
     }
 
+    pub fn subarray(array: Term<V>, start: Term<V>, length: Term<V>) -> Self {
+        Term::Subarray(Box::new(array), Box::new(start), Box::new(length))
+    }
+
     pub fn boxed(self) -> Self {
         Term::Box(Box::new(self))
     }
@@ -863,23 +897,6 @@ impl<V> Term<V> {
                 ],
             );
         }
-        // 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(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

@@ -21,7 +21,6 @@ use crate::chc::{self, hoice::HoiceDatatypeRenamer};
 pub struct FormatContext {
     renamer: HoiceDatatypeRenamer,
     datatypes: Vec<chc::Datatype>,
-    int_array_elem_sorts: BTreeSet<chc::Sort>,
 }
 
 // FIXME: this is obviously ineffective and should be replaced
@@ -47,6 +46,11 @@ fn term_sorts(clause: &chc::Clause, t: &chc::Term, sorts: &mut BTreeSet<chc::Sor
             }
         }
         chc::Term::ArrayEmpty(_, _) => {}
+        chc::Term::Subarray(arr, start, length) => {
+            term_sorts(clause, arr, sorts);
+            term_sorts(clause, start, sorts);
+            term_sorts(clause, length, sorts);
+        }
         chc::Term::SeqConcat(_, t) => {
             for arg in t.iter_args() {
                 term_sorts(clause, arg, sorts);
@@ -302,43 +306,20 @@ impl FormatContext {
             }
         }
 
-        let int_array_elem_sorts: BTreeSet<_> = sorts
-            .iter()
-            .filter_map(|s| match s {
-                chc::Sort::Array(index, elem) if **index == chc::Sort::int() => Some(*elem.clone()),
-                _ => 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)
             .chain(datatypes)
             .filter(|d| d.params == 0)
             .collect();
         let renamer = HoiceDatatypeRenamer::new(&datatypes);
-        FormatContext {
-            renamer,
-            datatypes,
-            int_array_elem_sorts,
-        }
+        FormatContext { renamer, datatypes }
     }
 
     pub fn datatypes(&self) -> &[chc::Datatype] {
         &self.datatypes
     }
 
-    pub fn int_array_elem_sorts(&self) -> &BTreeSet<chc::Sort> {
-        &self.int_array_elem_sorts
-    }
-
     pub fn box_ctor(&self, sort: &chc::Sort) -> impl std::fmt::Display {
         let ss = SortSymbol::new(sort).sorts();
         format!("box{ss}")
@@ -403,11 +384,6 @@ impl FormatContext {
         format!("matcher_pred<{}>", self.fmt_datatype_symbol(sym))
     }
 
-    pub fn seq_concat(&self, elem: &chc::Sort) -> impl std::fmt::Display {
-        let elem = SortSymbol::new(elem);
-        format!("seq_concat<{}>", elem)
-    }
-
     fn fmt_sort_impl(&self, sort: &chc::Sort) -> Box<dyn std::fmt::Display> {
         match sort {
             chc::Sort::Array(s1, s2) => {

src/chc/smtlib2.rs

@@ -169,13 +169,45 @@ impl<'ctx, 'a> std::fmt::Display for Term<'ctx, 'a> {
                     Term::new(self.ctx, self.clause, &default)
                 )
             }
+            chc::Term::Subarray(arr, start, length) => {
+                let elem = self
+                    .clause
+                    .term_sort(arr)
+                    .as_array_elem()
+                    .expect("Subarray applied to a non-array term")
+                    .clone();
+                let default = chc::Term::default_for(&elem);
+                write!(
+                    f,
+                    "(lambda ((sub!idx Int)) \
+                       (ite (and (<= 0 sub!idx) (< sub!idx {len})) \
+                            (select {arr} (+ {start} sub!idx)) \
+                            {default}))",
+                    len = Term::new(self.ctx, self.clause, length),
+                    arr = Term::new(self.ctx, self.clause, arr),
+                    start = Term::new(self.ctx, self.clause, start),
+                    default = Term::new(self.ctx, self.clause, &default),
+                )
+            }
             chc::Term::SeqConcat(elem, t) => {
-                let name = self.ctx.seq_concat(elem);
+                let arr1 = t.seq1.clone().tuple_proj(0);
+                let arr2 = t.seq2.clone().tuple_proj(0);
+                let len1 = t.seq1.clone().tuple_proj(1);
+                let len2 = t.seq2.clone().tuple_proj(1);
+                let default = chc::Term::default_for(elem);
                 write!(
                     f,
-                    "({} {})",
-                    name,
-                    List::open(t.iter_args().map(|t| Term::new(self.ctx, self.clause, t)))
+                    "(lambda ((concat!idx Int)) \
+                       (ite (and (<= 0 concat!idx) (< concat!idx (+ {len1} {len2}))) \
+                            (ite (< concat!idx {len1}) \
+                                 (select {arr1} concat!idx) \
+                                 (select {arr2} (- concat!idx {len1}))) \
+                            {default}))",
+                    arr1 = Term::new(self.ctx, self.clause, &arr1),
+                    arr2 = Term::new(self.ctx, self.clause, &arr2),
+                    len1 = Term::new(self.ctx, self.clause, &len1),
+                    len2 = Term::new(self.ctx, self.clause, &len2),
+                    default = Term::new(self.ctx, self.clause, &default),
                 )
             }
             chc::Term::Tuple(ts) => {
@@ -638,30 +670,6 @@ impl<'a> std::fmt::Display for System<'a> {
             writeln!(f, "{}", MatcherPredFun::new(&self.ctx, datatype))?;
         }
 
-        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
-            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} \
-                  ((s {seq_ty}) (t {seq_ty})) \
-                  (Array Int {elem_ty}) \
-                  (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",
-            )?;
-        }
-
         // insert command from #![thrust::raw_command()] here
         for raw_command in &self.inner.raw_commands {
             writeln!(f, "{}\n", RawCommand::new(raw_command))?;

src/chc/unbox.rs

@@ -19,6 +19,11 @@ 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::Subarray(arr, start, length) => Term::Subarray(
+            Box::new(unbox_term(*arr)),
+            Box::new(unbox_term(*start)),
+            Box::new(unbox_term(*length)),
+        ),
         Term::SeqConcat(s, t) => {
             Term::SeqConcat(unbox_sort(s), Box::new(unbox_seq_concat_term(*t)))
         }

src/rty.rs

@@ -1990,6 +1990,11 @@ 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::Subarray(arr, start, length) => {
+            subst_ty_params_in_term(arr, subst);
+            subst_ty_params_in_term(start, subst);
+            subst_ty_params_in_term(length, subst);
+        }
         chc::Term::SeqConcat(sort, t) => {
             subst_ty_params_in_sort(sort, subst);
             for arg in t.iter_args_mut() {