Add offset slice views and split_first_mut

src/analyze/annot.rs

@@ -177,6 +177,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

@@ -649,7 +649,9 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                     .ty_adt_def()
                     .is_some_and(|adt| Some(adt.did()) == self.def_ids.seq_model());
                 let array_inner = if is_seq {
-                    array_term.tuple_proj(0)
+                    let offset = array_term.clone().tuple_proj(1);
+                    let array = array_term.tuple_proj(0);
+                    return FormulaOrTerm::Term(array.select(offset.add(index_term)));
                 } else {
                     array_term
                 };
@@ -675,36 +677,58 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                     if Some(def_id) == self.def_ids.seq_len() {
                         assert!(args.is_empty(), "Seq::len does not take any arguments");
                         let t = self.to_term(receiver);
-                        return FormulaOrTerm::Term(t.tuple_proj(1));
+                        return FormulaOrTerm::Term(t.tuple_proj(2));
                     }
                     if Some(def_id) == self.def_ids.seq_push() {
                         assert_eq!(args.len(), 1, "Seq::push takes exactly 1 argument");
                         let t = self.to_term(receiver);
                         let v = self.to_term(&args[0]);
                         let arr = t.clone().tuple_proj(0);
-                        let len = t.tuple_proj(1);
-                        let new_arr = arr.store(len.clone(), v);
+                        let offset = t.clone().tuple_proj(1);
+                        let len = t.tuple_proj(2);
+                        let new_arr = arr.store(offset.clone().add(len.clone()), v);
                         let new_len = len.add(chc::Term::int(1));
-                        return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len]));
+                        return FormulaOrTerm::Term(chc::Term::tuple(vec![
+                            new_arr, offset, 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.clone().tuple_proj(0);
+                        let offset = t.clone().tuple_proj(1);
+                        return FormulaOrTerm::Term(chc::Term::tuple(vec![
+                            arr,
+                            offset.add(start.clone()),
+                            end.sub(start),
+                        ]));
                     }
                     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();
                         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 a_offset = t.clone().tuple_proj(1);
+                        let a_len = t.tuple_proj(2);
                         let b_arr = other.clone().tuple_proj(0);
-                        let b_len = other.tuple_proj(1);
+                        let b_offset = other.clone().tuple_proj(1);
+                        let b_len = other.tuple_proj(2);
                         let new_arr = chc::Term::array_concat(
                             elem_sort,
                             a_arr,
+                            a_offset.clone(),
                             a_len.clone(),
                             b_arr,
+                            b_offset,
                             b_len.clone(),
                         );
                         let new_len = a_len.add(b_len);
-                        return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len]));
+                        return FormulaOrTerm::Term(chc::Term::tuple(vec![
+                            new_arr, a_offset, new_len,
+                        ]));
                     }
                 }
                 unimplemented!("unsupported method call in formula: {:?}", method)
@@ -787,6 +811,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                             return FormulaOrTerm::Term(chc::Term::tuple(vec![
                                 chc::Term::array_empty(chc::Sort::int(), elem_sort),
                                 chc::Term::int(0),
+                                chc::Term::int(0),
                             ]));
                         }
                         if Some(def_id) == self.def_ids.seq_singleton() {
@@ -797,6 +822,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                                 .store(chc::Term::int(0), v);
                             return FormulaOrTerm::Term(chc::Term::tuple(vec![
                                 new_arr,
+                                chc::Term::int(0),
                                 chc::Term::int(1),
                             ]));
                         }

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>>,
@@ -221,6 +222,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

@@ -439,8 +439,10 @@ impl Function {
 #[derive(Debug, Clone)]
 pub struct ArrayConcatTerm<V = TermVarIdx> {
     pub array1: Term<V>,
+    pub offset1: Term<V>,
     pub len1: Term<V>,
     pub array2: Term<V>,
+    pub offset2: Term<V>,
     pub len2: Term<V>,
 }
 
@@ -457,12 +459,18 @@ where
             .append(self.array1.pretty_atom(allocator))
             .append(allocator.text(","))
             .append(allocator.line())
+            .append(self.offset1.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.offset2.pretty_atom(allocator))
+            .append(allocator.text(","))
+            .append(allocator.line())
             .append(self.len2.pretty_atom(allocator))
             .parens()
     }
@@ -471,15 +479,19 @@ where
 impl<V> ArrayConcatTerm<V> {
     pub fn iter_args(&self) -> impl Iterator<Item = &Term<V>> {
         std::iter::once(&self.array1)
+            .chain(std::iter::once(&self.offset1))
             .chain(std::iter::once(&self.len1))
             .chain(std::iter::once(&self.array2))
+            .chain(std::iter::once(&self.offset2))
             .chain(std::iter::once(&self.len2))
     }
 
     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.offset1))
             .chain(std::iter::once(&mut self.len1))
             .chain(std::iter::once(&mut self.array2))
+            .chain(std::iter::once(&mut self.offset2))
             .chain(std::iter::once(&mut self.len2))
     }
 
@@ -489,8 +501,10 @@ impl<V> ArrayConcatTerm<V> {
     {
         ArrayConcatTerm {
             array1: self.array1.subst_var(&mut f),
+            offset1: self.offset1.subst_var(&mut f),
             len1: self.len1.subst_var(&mut f),
             array2: self.array2.subst_var(&mut f),
+            offset2: self.offset2.subst_var(&mut f),
             len2: self.len2.subst_var(f),
         }
     }
@@ -775,16 +789,20 @@ impl<V> Term<V> {
     pub fn array_concat(
         elem_sort: Sort,
         array1: Term<V>,
+        offset1: Term<V>,
         len1: Term<V>,
         array2: Term<V>,
+        offset2: Term<V>,
         len2: Term<V>,
     ) -> Self {
         Term::ArrayConcat(
             elem_sort,
             Box::new(ArrayConcatTerm {
                 array1,
+                offset1,
                 len1,
                 array2,
+                offset2,
                 len2,
             }),
         )
@@ -899,12 +917,13 @@ 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(sa, so, sn, ta, to, tn), i)`
+        //   ↦ ite(i < so + sn, select(sa, i), select(ta, to + i - (so + sn)))`
         if let Term::ArrayConcat(_, t) = self {
-            let cond = index.clone().lt(t.len1.clone());
+            let split = t.offset1.clone().add(t.len1.clone());
+            let cond = index.clone().lt(split.clone());
             let then_ = t.array1.select(index.clone());
-            let else_ = t.array2.select(index.sub(t.len1));
+            let else_ = t.array2.select(t.offset2.add(index.sub(split)));
             return Term::ite(cond, then_, else_);
         }
         Term::App(Function::SELECT, vec![self, index])

src/chc/smtlib2.rs

@@ -644,12 +644,12 @@ impl<'a> std::fmt::Display for System<'a> {
             writeln!(
                 f,
                 "(define-fun-rec {name} \
-                  ((sa (Array Int {elem_ty})) (sn Int) (ta (Array Int {elem_ty})) (tn Int)) \
+                  ((sa (Array Int {elem_ty})) (so Int) (sn Int) (ta (Array Int {elem_ty})) (to Int) (tn Int)) \
                   (Array Int {elem_ty}) \
                   (ite (<= tn 0) sa \
-                       (store ({name} sa sn ta (- tn 1)) \
-                              (+ sn (- tn 1)) \
-                              (select ta (- tn 1)))))\n",
+                       (store ({name} sa so sn ta to (- tn 1)) \
+                              (+ so sn (- tn 1)) \
+                              (select ta (+ to (- tn 1))))))\n",
             )?;
         }
 

src/chc/unbox.rs

@@ -5,18 +5,24 @@ use super::*;
 fn unbox_array_concat_term(t: ArrayConcatTerm) -> ArrayConcatTerm {
     let ArrayConcatTerm {
         array1,
+        offset1,
         len1,
         array2,
+        offset2,
         len2,
     } = t;
     let array1 = unbox_term(array1);
+    let offset1 = unbox_term(offset1);
     let len1 = unbox_term(len1);
     let array2 = unbox_term(array2);
+    let offset2 = unbox_term(offset2);
     let len2 = unbox_term(len2);
     ArrayConcatTerm {
         array1,
+        offset1,
         len1,
         array2,
+        offset2,
         len2,
     }
 }