Add test calls for all sequence functions

SemGuS-git · Mar 20, 2024 · 00b36b9 · 00b36b9
1 parent 1430d42
commit 00b36b9
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 5 deletions.
diff --git a/IntegrationTests/data/sequences.sem b/IntegrationTests/data/sequences.sem
@@ -2,6 +2,8 @@
  ((Start 0))
  ((($main))))
 
+(declare-const X (Seq Int))
+
 (define-funs-rec
     ((Start.Sem ((Start_term_0 Start) (rq (Seq Int)) (x (_ BitVec 32))) Bool))
 
@@ -11,7 +13,17 @@
                       (and (= "Test" (seq.nth rb 7))
                            (= rb (seq.++ ra (seq.unit "a")))
                            (= rb (as seq.empty (Seq String)))
-                           (= rq (seq.rev rq)))))))))
+                           (= rq (seq.rev rq))
+                           (= (seq.len ra) (seq.nth rq 1))
+                           (= (seq.update ra 7 rb) rb)
+                           (= ra (seq.extract rb 3 5))
+                           (= (seq.at rb 4) (seq.at ra 3))
+                           (seq.contains ra rb)
+                           (= 12 (seq.indexof ra rb 7))
+                           (= ra (seq.replace ra ra rb))
+                           (= (seq.replace_all ra ra rb) rb)
+                           (seq.prefixof ra rb)
+                           (seq.suffixof rb ra))))))))
 
 
 (synth-fun MyFunc () Start)