Front end support for sequences (#4690)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 6 Jul 2020 23:48:10 +0000 (18:48 -0500)
committerGitHub <noreply@github.com>
Mon, 6 Jul 2020 23:48:10 +0000 (18:48 -0500)
commit9678f58a7fedab4fc061761c58382f4023686108
tree5ccc2e13b00a32a2e8fa87604b4a2f3a92b12e7e
parentae0bfbdacfec8b2d21b10cbc4955305f49a62a54
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.++).
34 files changed:
NEWS
src/api/cvc4cpp.cpp
src/api/cvc4cpp.h
src/api/cvc4cppkind.h
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/expr_sequence.h
src/expr/sequence.h
src/expr/type_node.cpp
src/parser/cvc/Cvc.g
src/parser/parser.cpp
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/printer/cvc/cvc_printer.cpp
src/printer/smt2/smt2_printer.cpp
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
src/theory/strings/strings_entail.cpp
src/theory/strings/term_registry.cpp
src/theory/strings/theory_strings_type_rules.h
src/theory/strings/type_enumerator.cpp
src/theory/strings/word.cpp
test/regress/CMakeLists.txt
test/regress/regress0/seq/seq-2var.smt2 [new file with mode: 0644]
test/regress/regress0/seq/seq-ex1.smt2 [new file with mode: 0644]
test/regress/regress0/seq/seq-ex2.smt2 [new file with mode: 0644]
test/regress/regress0/seq/seq-ex3.smt2 [new file with mode: 0644]
test/regress/regress0/seq/seq-ex4.smt2 [new file with mode: 0644]
test/regress/regress0/seq/seq-ex5-dd.smt2 [new file with mode: 0644]
test/regress/regress0/seq/seq-ex5.smt2 [new file with mode: 0644]
test/regress/regress0/seq/seq-nemp.smt2 [new file with mode: 0644]
test/regress/regress0/seq/seq-rewrites.smt2 [new file with mode: 0644]
test/unit/api/solver_black.h
test/unit/api/sort_black.h
test/unit/api/term_black.h