Remove ExprSequence (#4724)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 13 Jul 2020 00:37:03 +0000 (17:37 -0700)
committerGitHub <noreply@github.com>
Mon, 13 Jul 2020 00:37:03 +0000 (19:37 -0500)
commit090d8bc3c31404140856e51d2cc5a5aa1335b3b3
tree0edb9c6a4b37ea22ca0729061659ecfc95738393
parent64a7db86206aa0993f75446a3e7f77f3c0c023c6
Remove ExprSequence (#4724)

Now that we can break the old API, we don't need an ExprSequence
anymore. This commit removes ExprSequence and replaces all of its uses
with Sequence. Note that I had to temporarily make sequence.h public
because we currently include it in a "public" header because we still
generate the code for Expr::mkConst<Sequence>().
15 files changed:
src/CMakeLists.txt
src/api/cvc4cpp.cpp
src/expr/CMakeLists.txt
src/expr/expr_sequence.cpp [deleted file]
src/expr/expr_sequence.h [deleted file]
src/expr/sequence.cpp
src/expr/sequence.h
src/printer/cvc/cvc_printer.cpp
src/printer/smt2/smt2_printer.cpp
src/theory/strings/base_solver.cpp
src/theory/strings/kinds
src/theory/strings/sequences_rewriter.cpp
src/theory/strings/theory_strings_type_rules.h
src/theory/strings/type_enumerator.cpp
src/theory/strings/word.cpp