Python API: Add support for sequences (#4757)

Commit 9678f58a7fedab4fc061761c58382f4023686108 added front end support
for sequences. This commit extends that support to the Python API. It
also adds simple C++ and Python examples that demonstrate how the API
works for sequences.

2 files changed, 39 insertions, 0 deletions

diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index 507aff2ae..cd40fc807 100644
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -157,6 +157,16 @@ def testGetSetElementSort():
     with pytest.raises(Exception):
         bvSort.getSetElementSort()
 
+def testGetSequenceElementSort():
+    solver = pycvc4.Solver()
+    seqSort = solver.mkSequenceSort(solver.getIntegerSort())
+    seqSort.getSequenceElementSort()
+    bvSort = solver.mkBitVectorSort(32)
+    assert not bvSort.isSequence()
+
+    with pytest.raises(Exception):
+        bvSort.getSetElementSort()
+
 def testGetUninterpretedSortName():
     solver = pycvc4.Solver()
     uSort = solver.mkUninterpretedSort("u")
diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index 43e541412..b135e4510 100644
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -19,6 +19,13 @@ def test_get_kind():
     fx = solver.mkTerm(kinds.ApplyUf, f, x)
     assert fx.getKind() == kinds.ApplyUf
 
+    # Sequence kinds do not exist internally, test that the API properly
+    # converts them back.
+    seqsort = solver.mkSequenceSort(intsort)
+    s = solver.mkConst(seqsort, 's')
+    ss = solver.mkTerm(kinds.SeqConcat, s, s)
+    assert ss.getKind() == kinds.SeqConcat
+
 
 def test_eq():
     solver = pycvc4.Solver()
@@ -86,3 +93,25 @@ def test_is_const():
     assert one.isConst()
     assert not xpone.isConst()
     assert not onepone.isConst()
+
+def test_const_sequence_elements():
+    solver = pycvc4.Solver()
+    realsort = solver.getRealSort()
+    seqsort = solver.mkSequenceSort(realsort)
+    s = solver.mkEmptySequence(seqsort)
+
+    assert s.isConst()
+
+    assert s.getKind() == kinds.ConstSequence
+    # empty sequence has zero elements
+    cs = s.getConstSequenceElements()
+    assert len(cs) == 0
+
+    # A seq.unit app is not a constant sequence (regardless of whether it is
+    # applied to a constant).
+    su = solver.mkTerm(kinds.SeqUnit, solver.mkReal(1))
+    try:
+        su.getConstSequenceElements()
+        assert False
+    except:
+        assert True