Represent slices with native SMT sequences

.github/workflows/ci.yml

@@ -28,13 +28,30 @@ jobs:
     permissions:
       contents: read
     timeout-minutes: 10
-    env:
-      # see tests/thrust-pcsat-wrapper
-      COAR_IMAGE: ghcr.io/hiroshi-unno/coar@sha256:73144ed27a02b163d1a71b41b58f3b5414f12e91326015600cfdca64ff19f011
     steps:
       - uses: actions/checkout@v7
       - uses: ./.github/actions/setup-z3
-      - run: docker pull "$COAR_IMAGE"
+      - name: Install PCSat dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install \
+            libblas3 \
+            libgcc-s1 \
+            libgmp10 \
+            liblapack3 \
+            libmpfr6 \
+            libstdc++6 \
+            zlib1g
+      - name: Download latest PCSat
+        run: |
+          cd $(mktemp -d)
+          curl -fsS "$PCSAT_URL" -o thrust-pcsat-wrapper.tar.gz
+          echo "$PCSAT_SHA256 thrust-pcsat-wrapper.tar.gz" | sha256sum -c --strict
+          tar --strip-components=1 -xf thrust-pcsat-wrapper.tar.gz
+          mv thrust-pcsat-wrapper "$GITHUB_WORKSPACE/tests/thrust-pcsat-wrapper"
+        env:
+          PCSAT_URL: https://thrust-ci-public.s3.ap-northeast-1.amazonaws.com/pcsat/thrust-pcsat-wrapper-873d558c6a.tar.gz
+          PCSAT_SHA256: cae6829b40cfde196ae231f4a97eed5b873756cb59619f580934b488c1e7a11a
       - run: rustup show
       - uses: Swatinem/rust-cache@v2
       - run: cargo test

src/analyze/annot.rs

@@ -162,6 +162,22 @@ pub fn seq_push_path() -> [Symbol; 3] {
     ]
 }
 
+pub fn seq_store_path() -> [Symbol; 3] {
+    [
+        Symbol::intern("thrust"),
+        Symbol::intern("def"),
+        Symbol::intern("seq_store"),
+    ]
+}
+
+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

@@ -581,17 +581,6 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
         self.type_builder.build(elem_ty)
     }
 
-    fn adt_arg_type_at(
-        &self,
-        expr: &'tcx rustc_hir::Expr<'tcx>,
-        idx: usize,
-    ) -> rty::Type<rty::Closed> {
-        let mir_ty::TyKind::Adt(_, args) = self.expr_ty(expr).kind() else {
-            panic!("expected ADT");
-        };
-        self.type_builder.build(args.type_at(idx))
-    }
-
     fn variant_ctor_term(
         &self,
         ctor_did: rustc_span::def_id::DefId,
@@ -807,18 +796,17 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                 FormulaOrTerm::Term(term.tuple_proj(index))
             }
             ExprKind::Index(array, index, _) => {
-                let array_ty = self.expr_ty(array);
-                let array_term = self.to_term(array);
                 let index_term = self.to_term(index);
-                let is_seq = array_ty
+                let is_seq = self
+                    .expr_ty(array)
                     .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 term = if is_seq {
+                    self.to_term(array).seq_nth(index_term)
                 } else {
-                    array_term
+                    self.to_term(array).select(index_term)
                 };
-                FormulaOrTerm::Term(array_inner.select(index_term))
+                FormulaOrTerm::Term(term)
             }
             ExprKind::MethodCall(method, receiver, args, _) => {
                 if let Some(def_id) = self.typeck.type_dependent_def_id(hir.hir_id) {
@@ -840,28 +828,34 @@ 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.seq_len());
                     }
                     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 new_len = len.add(chc::Term::int(1));
-                        return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len]));
+                        return FormulaOrTerm::Term(t.seq_concat(v.seq_unit()));
+                    }
+                    if Some(def_id) == self.def_ids.seq_store() {
+                        assert_eq!(args.len(), 2, "Seq::store takes exactly 2 arguments");
+                        let seq = self.to_term(receiver);
+                        let index = self.to_term(&args[0]);
+                        let value = self.to_term(&args[1]);
+                        return FormulaOrTerm::Term(seq.seq_store(index, value));
+                    }
+                    if Some(def_id) == self.def_ids.seq_subsequence() {
+                        assert_eq!(args.len(), 2, "Seq::subsequence takes exactly 2 arguments");
+                        let seq = self.to_term(receiver);
+                        let start = self.to_term(&args[0]);
+                        let end = self.to_term(&args[1]);
+                        let length = end.sub(start.clone());
+                        return FormulaOrTerm::Term(seq.seq_extract(start, length));
                     }
                     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 seq = self.to_term(receiver);
                         let other = self.to_term(&args[0]);
-                        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]));
+                        return FormulaOrTerm::Term(seq.seq_concat(other));
                     }
                 }
                 unimplemented!("unsupported method call in formula: {:?}", method)
@@ -941,21 +935,12 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                         if Some(def_id) == self.def_ids.seq_empty() {
                             assert!(args.is_empty(), "Seq::empty does not take any arguments");
                             let elem_sort = self.node_arg_type_at(func_expr.hir_id, 0).to_sort();
-                            return FormulaOrTerm::Term(chc::Term::tuple(vec![
-                                chc::Term::array_empty(chc::Sort::int(), elem_sort),
-                                chc::Term::int(0),
-                            ]));
+                            return FormulaOrTerm::Term(chc::Term::seq_empty(elem_sort));
                         }
                         if Some(def_id) == self.def_ids.seq_singleton() {
                             assert_eq!(args.len(), 1, "Seq::singleton takes exactly 1 argument");
                             let v = self.to_term(&args[0]);
-                            let elem_sort = self.node_arg_type_at(func_expr.hir_id, 0).to_sort();
-                            let new_arr = chc::Term::array_empty(chc::Sort::int(), elem_sort)
-                                .store(chc::Term::int(0), v);
-                            return FormulaOrTerm::Term(chc::Term::tuple(vec![
-                                new_arr,
-                                chc::Term::int(1),
-                            ]));
+                            return FormulaOrTerm::Term(v.seq_unit());
                         }
                         if let rustc_hir::def::DefKind::Ctor(ctor_of, _) = def_kind {
                             let terms = args.iter().map(|e| self.to_term(e)).collect();

src/analyze/basic_block.rs

@@ -544,29 +544,19 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             Rvalue::Aggregate(kind, fields) => {
                 match *kind {
                     mir::AggregateKind::Array(mir_elem_ty) => {
-                        // Build Seq<T> = (Box<Array<Int,T>>, Box<Int>) from array literal elements,
-                        // pinning each element at its index via store folds.
-                        //
                         // TODO: Stop embedding knowledge of `<[T; N] as Model>::Ty` in the analyzer
                         let mut builder = PlaceTypeBuilder::default();
                         let elem_ty = self.type_builder.build(mir_elem_ty).vacuous();
-                        let mut arr_term =
-                            chc::Term::array_empty(chc::Sort::int(), elem_ty.to_sort());
-                        for (i, field) in fields.iter().enumerate() {
+                        let mut seq = chc::Term::seq_empty(elem_ty.to_sort());
+                        for field in fields.iter() {
                             let pty = self.operand_type(field.clone());
                             let (_, elem_term) = builder.subsume(pty);
-                            arr_term = arr_term.store(chc::Term::int(i as i64), elem_term);
+                            seq = seq.seq_concat(elem_term.seq_unit());
                         }
-                        let arr_pty = builder.build(
-                            rty::ArrayType::new(rty::Type::int(), elem_ty).into(),
-                            arr_term,
-                        );
-                        let size = fields.len();
-                        let size_pty = PlaceType::with_ty_and_term(
-                            rty::Type::int(),
-                            chc::Term::int(size as i64),
-                        );
-                        PlaceType::tuple(vec![arr_pty.boxed(), size_pty.boxed()])
+                        builder.build(
+                            rty::Type::Seq(Box::new(rty::RefinedType::unrefined(elem_ty))),
+                            seq,
+                        )
                     }
                     mir::AggregateKind::Adt(did, variant_idx, args, _, _)
                         if self.tcx.def_kind(did) == DefKind::Enum =>

src/analyze/did_cache.rs

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