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.

11 files changed, 203 insertions, 3 deletions

diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt
index 6421a3263..bd6361b5c 100644
--- a/examples/api/CMakeLists.txt
+++ b/examples/api/CMakeLists.txt
@@ -7,6 +7,7 @@ set(CVC4_EXAMPLES_API
   helloworld
   linear_arith
   sets
+  sequences
   strings
   sygus-fun
   sygus-grammar
diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
index 6e255c5b1..e3966fa2d 100644
--- a/examples/api/python/CMakeLists.txt
+++ b/examples/api/python/CMakeLists.txt
@@ -1,5 +1,6 @@
 set(EXAMPLES_API_PYTHON
   exceptions
+  sequences
 )
 
 find_package(PythonInterp REQUIRED)
diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py
new file mode 100644
index 000000000..4498e5153
--- /dev/null
+++ b/examples/api/python/sequences.py
@@ -0,0 +1,60 @@
+#!/usr/bin/env python
+
+#####################
+#! \file sequences.py
+## \verbatim
+## Top contributors (to current version):
+##   Andres Noetzli
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory) and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.\endverbatim
+##
+## \brief A simple demonstration of the solving capabilities of the CVC4
+## strings solver through the Python API. This is a direct translation
+## of sequences.cpp.
+import pycvc4
+from pycvc4 import kinds
+
+if __name__ == "__main__":
+    slv = pycvc4.Solver()
+    # Set the logic
+    slv.setLogic("QF_SLIA")
+    # Produce models
+    slv.setOption("produce-models", "true")
+    # The option strings-exp is needed
+    slv.setOption("strings-exp", "true")
+    # Set output language to SMTLIB2
+    slv.setOption("output-language", "smt2")
+
+    # Sequence sort
+    int_seq = slv.mkSequenceSort(slv.getIntegerSort())
+
+    # Sequence variables
+    x = slv.mkConst(int_seq, "x")
+    y = slv.mkConst(int_seq, "y")
+
+    # Empty sequence
+    empty = slv.mkEmptySequence(slv.getIntegerSort())
+    # Sequence concatenation: x.y.empty
+    concat = slv.mkTerm(kinds.SeqConcat, x, y, empty)
+    # Sequence length: |x.y.empty|
+    concat_len = slv.mkTerm(kinds.SeqLength, concat)
+    # |x.y.empty| > 1
+    formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkReal(1))
+    # Sequence unit: seq(1)
+    unit = slv.mkTerm(kinds.SeqUnit, slv.mkReal(1))
+    # x = seq(1)
+    formula2 = slv.mkTerm(kinds.Equal, x, unit)
+
+    # Make a query
+    q = slv.mkTerm(kinds.And, formula1, formula2)
+
+    # Check satisfiability
+    result = slv.checkSatAssuming(q)
+    print("CVC4 reports:", q, "is", result)
+
+    if result:
+        print("x = {}".format(slv.getValue(x)))
+        print("y = {}".format(slv.getValue(y)))
diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py
index 5c8e91997..58a6f6508 100755
--- a/examples/api/python/strings.py
+++ b/examples/api/python/strings.py
@@ -20,7 +20,7 @@ from pycvc4 import kinds
 if __name__ == "__main__":
     slv = pycvc4.Solver()
     # Set the logic
-    slv.setLogic("S")
+    slv.setLogic("QF_SLIA")
     # Produce models
     slv.setOption("produce-models", "true")
     # The option strings-exp is needed
diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp
new file mode 100644
index 000000000..53bb584ce
--- /dev/null
+++ b/examples/api/sequences.cpp
@@ -0,0 +1,68 @@
+/*********************                                                        */
+/*! \file sequences.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Reasoning about sequences with CVC4 via C++ API.
+ **
+ ** A simple demonstration of reasoning about sequences with CVC4 via C++ API.
+ **/
+
+#include <cvc4/api/cvc4cpp.h>
+
+#include <iostream>
+
+using namespace CVC4::api;
+
+int main()
+{
+  Solver slv;
+
+  // Set the logic
+  slv.setLogic("QF_SLIA");
+  // Produce models
+  slv.setOption("produce-models", "true");
+  // The option strings-exp is needed
+  slv.setOption("strings-exp", "true");
+  // Set output language to SMTLIB2
+  slv.setOption("output-language", "smt2");
+
+  // Sequence sort
+  Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort());
+
+  // Sequence variables
+  Term x = slv.mkConst(intSeq, "x");
+  Term y = slv.mkConst(intSeq, "y");
+
+  // Empty sequence
+  Term empty = slv.mkEmptySequence(slv.getIntegerSort());
+  // Sequence concatenation: x.y.empty
+  Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty);
+  // Sequence length: |x.y.empty|
+  Term concat_len = slv.mkTerm(SEQ_LENGTH, concat);
+  // |x.y.empty| > 1
+  Term formula1 = slv.mkTerm(GT, concat_len, slv.mkReal(1));
+  // Sequence unit: seq(1)
+  Term unit = slv.mkTerm(SEQ_UNIT, slv.mkReal(1));
+  // x = seq(1)
+  Term formula2 = slv.mkTerm(EQUAL, x, unit);
+
+  // Make a query
+  Term q = slv.mkTerm(AND, formula1, formula2);
+
+  // check sat
+  Result result = slv.checkSatAssuming(q);
+  std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl;
+
+  if (result.isSat())
+  {
+    std::cout << "  x = " << slv.getValue(x) << std::endl;
+    std::cout << "  y = " << slv.getValue(y) << std::endl;
+  }
+}
diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
index 6a0e10918..cd2a60cb1 100644
--- a/examples/api/strings.cpp
+++ b/examples/api/strings.cpp
@@ -25,7 +25,7 @@ int main()
   Solver slv;
 
   // Set the logic
-  slv.setLogic("S");
+  slv.setLogic("QF_SLIA");
   // Produce models
   slv.setOption("produce-models", "true");
   // The option strings-exp is needed
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 940922052..eea263a96 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -132,6 +132,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Sort mkPredicateSort(const vector[Sort]& sorts) except +
         Sort mkRecordSort(const vector[pair[string, Sort]]& fields) except +
         Sort mkSetSort(Sort elemSort) except +
+        Sort mkSequenceSort(Sort elemSort) except +
         Sort mkUninterpretedSort(const string& symbol) except +
         Sort mkSortConstructorSort(const string& symbol, size_t arity) except +
         Sort mkTupleSort(const vector[Sort]& sorts) except +
@@ -153,6 +154,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Term mkSepNil(Sort sort) except +
         Term mkString(const string& s) except +
         Term mkString(const vector[unsigned]& s) except +
+        Term mkEmptySequence(Sort sort) except +
         Term mkUniverseSet(Sort sort) except +
         Term mkBitVector(uint32_t size) except +
         Term mkBitVector(uint32_t size, uint64_t val) except +
@@ -246,6 +248,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint isRecord() except +
         bint isArray() except +
         bint isSet() except +
+        bint isSequence() except +
         bint isUninterpretedSort() except +
         bint isSortConstructor() except +
         bint isFirstClass() except +
@@ -263,6 +266,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Sort getArrayIndexSort() except +
         Sort getArrayElementSort() except +
         Sort getSetElementSort() except +
+        Sort getSequenceElementSort() except +
         string getUninterpretedSortName() except +
         bint isUninterpretedSortParameterized() except +
         vector[Sort] getUninterpretedSortParamSorts() except +
@@ -293,6 +297,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint isNull() except +
         bint isConst() except +
         Term getConstArrayBase() except +
+        vector[Term] getConstSequenceElements() except +
         Term notTerm() except +
         Term andTerm(const Term& t) except +
         Term orTerm(const Term& t) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 01660e206..133bd4660 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -459,6 +459,11 @@ cdef class Solver:
         sort.csort = self.csolver.mkSetSort(elemSort.csort)
         return sort
 
+    def mkSequenceSort(self, Sort elemSort):
+        cdef Sort sort = Sort()
+        sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
+        return sort
+
     def mkUninterpretedSort(self, str name):
         cdef Sort sort = Sort()
         sort.csort = self.csolver.mkUninterpretedSort(name.encode())
@@ -613,6 +618,11 @@ cdef class Solver:
                              " but got: {}".format(str_or_vec))
         return term
 
+    def mkEmptySequence(self, Sort sort):
+        cdef Term term = Term()
+        term.cterm = self.csolver.mkEmptySequence(sort.csort)
+        return term
+
     def mkUniverseSet(self, Sort sort):
         cdef Term term = Term()
         term.cterm = self.csolver.mkUniverseSet(sort.csort)
@@ -1081,6 +1091,9 @@ cdef class Sort:
     def isSet(self):
         return self.csort.isSet()
 
+    def isSequence(self):
+        return self.csort.isSequence()
+
     def isUninterpretedSort(self):
         return self.csort.isUninterpretedSort()
 
@@ -1159,6 +1172,11 @@ cdef class Sort:
         sort.csort = self.csort.getSetElementSort()
         return sort
 
+    def getSequenceElementSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.csort.getSequenceElementSort()
+        return sort
+
     def getUninterpretedSortName(self):
         return self.csort.getUninterpretedSortName().decode()
 
@@ -1282,6 +1300,14 @@ cdef class Term:
         term.cterm = self.cterm.getConstArrayBase()
         return term
 
+    def getConstSequenceElements(self):
+        elems = []
+        for e in self.cterm.getConstSequenceElements():
+            term = Term()
+            term.cterm = e
+            elems.append(term)
+        return elems
+
     def notTerm(self):
         cdef Term term = Term()
         term.cterm = self.cterm.notTerm()
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2bf425f2b..c9d0b95b5 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -242,7 +242,7 @@ bool PropEngine::isSatLiteral(TNode node) const {
 
 bool PropEngine::hasValue(TNode node, bool& value) const {
   Assert(node.getType().isBoolean());
-  Assert(d_cnfStream->hasLiteral(node));
+  Assert(d_cnfStream->hasLiteral(node)) << node;
 
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
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