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.++).

13 files changed, 190 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 10e2f414e..5f82aedf1 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -861,6 +861,15 @@ set(regress_0_tests
   regress0/sep/skolem_emp.smt2
   regress0/sep/trees-1.smt2
   regress0/sep/wand-crash.smt2
+  regress0/seq/seq-2var.smt2
+  regress0/seq/seq-ex1.smt2
+  regress0/seq/seq-ex2.smt2
+  regress0/seq/seq-ex3.smt2
+  regress0/seq/seq-ex4.smt2
+  regress0/seq/seq-ex5-dd.smt2
+  regress0/seq/seq-ex5.smt2
+  regress0/seq/seq-nemp.smt2
+  regress0/seq/seq-rewrites.smt2
   regress0/sets/abt-min.smt2
   regress0/sets/abt-te-exh.smt2
   regress0/sets/abt-te-exh2.smt2
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)
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index ddff63352..4a7b74c8e 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -46,6 +46,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkPredicateSort();
   void testMkRecordSort();
   void testMkSetSort();
+  void testMkSequenceSort();
   void testMkSortConstructorSort();
   void testMkTupleSort();
   void testMkUninterpretedSort();
@@ -56,6 +57,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkConst();
   void testMkConstArray();
   void testMkEmptySet();
+  void testMkEmptySequence();
   void testMkFalse();
   void testMkFloatingPoint();
   void testMkNaN();
@@ -388,6 +390,17 @@ void SolverBlack::testMkSetSort()
                    CVC4ApiException&);
 }
 
+void SolverBlack::testMkSequenceSort()
+{
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver->mkSequenceSort(d_solver->getBooleanSort()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkSequenceSort(
+      d_solver->mkSequenceSort(d_solver->getIntegerSort())));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkSequenceSort(d_solver->getIntegerSort()),
+                   CVC4ApiException&);
+}
+
 void SolverBlack::testMkUninterpretedSort()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->mkUninterpretedSort("u"));
@@ -540,6 +553,16 @@ void SolverBlack::testMkEmptySet()
   TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&);
 }
 
+void SolverBlack::testMkEmptySequence()
+{
+  Solver slv;
+  Sort s = d_solver->mkSequenceSort(d_solver->getBooleanSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySequence(s));
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver->mkEmptySequence(d_solver->getBooleanSort()));
+  TS_ASSERT_THROWS(slv.mkEmptySequence(s), CVC4ApiException&);
+}
+
 void SolverBlack::testMkFalse()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->mkFalse());
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index 944b9309f..abaded5a1 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -35,6 +35,7 @@ class SortBlack : public CxxTest::TestSuite
   void testGetArrayIndexSort();
   void testGetArrayElementSort();
   void testGetSetElementSort();
+  void testGetSequenceElementSort();
   void testGetUninterpretedSortName();
   void testIsUninterpretedSortParameterized();
   void testGetUninterpretedSortParamSorts();
@@ -196,6 +197,16 @@ void SortBlack::testGetSetElementSort()
   TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&);
 }
 
+void SortBlack::testGetSequenceElementSort()
+{
+  Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort());
+  TS_ASSERT(seqSort.isSequence());
+  TS_ASSERT_THROWS_NOTHING(seqSort.getSequenceElementSort());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT(!bvSort.isSequence());
+  TS_ASSERT_THROWS(bvSort.getSequenceElementSort(), CVC4ApiException&);
+}
+
 void SortBlack::testGetUninterpretedSortName()
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index d23f560ae..6ca02c9f1 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -44,6 +44,7 @@ class TermBlack : public CxxTest::TestSuite
   void testSubstitute();
   void testIsConst();
   void testConstArray();
+  void testConstSequenceElements();
 
  private:
   Solver d_solver;
@@ -110,6 +111,13 @@ void TermBlack::testGetKind()
   TS_ASSERT_THROWS_NOTHING(p_0.getKind());
   Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
   TS_ASSERT_THROWS_NOTHING(p_f_y.getKind());
+
+  // Sequence kinds do not exist internally, test that the API properly
+  // converts them back.
+  Sort seqSort = d_solver.mkSequenceSort(intSort);
+  Term s = d_solver.mkConst(seqSort, "s");
+  Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s);
+  TS_ASSERT(ss.getKind() == SEQ_CONCAT);
 }
 
 void TermBlack::testGetSort()
@@ -769,3 +777,22 @@ void TermBlack::testConstArray()
   TS_ASSERT_EQUALS(constarr.getConstArrayBase(), one);
   TS_ASSERT_THROWS(a.getConstArrayBase(), CVC4ApiException&);
 }
+
+void TermBlack::testConstSequenceElements()
+{
+  Sort realsort = d_solver.getRealSort();
+  Sort seqsort = d_solver.mkSequenceSort(realsort);
+  Term s = d_solver.mkEmptySequence(seqsort);
+
+  TS_ASSERT(s.isConst());
+
+  TS_ASSERT_EQUALS(s.getKind(), CONST_SEQUENCE);
+  // empty sequence has zero elements
+  std::vector<Term> cs = s.getConstSequenceElements();
+  TS_ASSERT(cs.empty());
+
+  // A seq.unit app is not a constant sequence (regardless of whether it is
+  // applied to a constant).
+  Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1));
+  TS_ASSERT_THROWS(su.getConstSequenceElements(), CVC4ApiException&);
+}