Front end support for sequences (#4690)

With this PR, we now support a preliminary draft of a theory of sequences.

This PR adds front end support for sequences in the smt2 parser, in the new API, adds regressions and unit tests for them.

As discussed offline, many of the string kinds are given a sequence version in the external API, but not in the internal one. This means that a special case for such kinds, getKindHelper was added to Term.

We do not yet support proper smt2 printing of sequences, which will require access to this code for Kind conversions (to distinguish e.g. str.++ from seq.++).

9 files changed, 120 insertions, 0 deletions

diff --git a/test/regress/regress0/seq/seq-2var.smt2 b/test/regress/regress0/seq/seq-2var.smt2
new file mode 100644
index 000000000..3a0d8934f
--- /dev/null
+++ b/test/regress/regress0/seq/seq-2var.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+
+(assert (not (= x y)))
+
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex1.smt2 b/test/regress/regress0/seq/seq-ex1.smt2
new file mode 100644
index 000000000..817ee5f8e
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex1.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_UFSLIA)
+(set-info :status sat)
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+(declare-fun f ((Seq Int)) (Seq Bool))
+
+(assert (not (= x y)))
+(assert (not (= (f x) (f y))))
+
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex2.smt2 b/test/regress/regress0/seq/seq-ex2.smt2
new file mode 100644
index 000000000..89b9d3100
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex2.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+(declare-fun z () Int)
+(assert (> z 10))
+(assert (= (seq.len x) (seq.len y)))
+(assert (= (seq.++ x (seq.unit z)) (seq.++ y (seq.unit 5))))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex3.smt2 b/test/regress/regress0/seq/seq-ex3.smt2
new file mode 100644
index 000000000..abafdeddf
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex3.smt2
@@ -0,0 +1,18 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun x () (Seq (Seq Int)))
+(declare-fun xp () (Seq (Seq Int)))
+(declare-fun y () (Seq (Seq Int)))
+(declare-fun yp () (Seq (Seq Int)))
+(declare-fun z () (Seq Int))
+(declare-fun w () (Seq Int))
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun n () Int)
+(assert (> i j))
+(assert (= (seq.extract z n 1) (seq.unit i)))
+(assert (= (seq.extract w n 1) (seq.unit j)))
+(assert (= x (seq.++ (seq.unit z) xp)))
+(assert (= y (seq.++ (seq.unit w) yp)))
+(assert (= x y))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex4.smt2 b/test/regress/regress0/seq/seq-ex4.smt2
new file mode 100644
index 000000000..93fed72c7
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex4.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun z () (Seq Int))
+(declare-fun i () Int)
+(declare-fun n () Int)
+(assert (= (seq.extract z n 1) (seq.unit i)))
+(assert (< (seq.len z) n))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex5-dd.smt2 b/test/regress/regress0/seq/seq-ex5-dd.smt2
new file mode 100644
index 000000000..d9ef5c8ba
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex5-dd.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-fun z () (Seq Int))
+(declare-fun i () Int)
+(declare-fun n () Int)
+(assert (> i 777))
+(assert (= (seq.extract z n 1) (seq.unit i)))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex5.smt2 b/test/regress/regress0/seq/seq-ex5.smt2
new file mode 100644
index 000000000..9fa72bc6b
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex5.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_SLIA)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun z () (Seq Int))
+(declare-fun w () (Seq Int))
+(declare-fun i () Int)
+(assert (> i 777))
+(assert (not (= (seq.replace z (seq.unit i) w) z)))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-nemp.smt2 b/test/regress/regress0/seq/seq-nemp.smt2
new file mode 100644
index 000000000..4eaee062f
--- /dev/null
+++ b/test/regress/regress0/seq/seq-nemp.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-fun x () (Seq Int))
+(assert (not (= x (as seq.empty (Seq Int)))))
+(assert (= (seq.len x) 16))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-rewrites.smt2 b/test/regress/regress0/seq/seq-rewrites.smt2
new file mode 100644
index 000000000..a8bd7c1f2
--- /dev/null
+++ b/test/regress/regress0/seq/seq-rewrites.smt2
@@ -0,0 +1,44 @@
+(set-logic QF_UFSLIA)
+(set-info :status unsat)
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+(declare-fun z () Int)
+
+(assert 
+(or
+
+(not (=
+(seq.replace (seq.++ (seq.unit 0) x) (seq.unit 1) (seq.unit 2))
+(seq.++ (seq.unit 0) (seq.replace x (seq.unit 1) (seq.unit 2)))
+))
+
+(not (=
+(seq.at (seq.++ x (seq.unit 14)) (seq.len x))
+(seq.unit 14)
+))
+
+(not (=
+(seq.at x z)
+(seq.extract x z 1)
+))
+
+(not (=
+(seq.contains (seq.++ x y) y)
+true
+))
+
+(not (=
+(seq.prefixof (seq.unit z) (seq.unit 4))
+(seq.suffixof (seq.unit z) (seq.unit 4))
+))
+
+(not (=
+(seq.rev (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))
+(seq.++ (seq.unit 3) (seq.unit 2) (seq.unit 1))
+))
+
+))
+
+
+
+(check-sat)