projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: da165b9) | patch
Add the sequence type (#4539)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 30 May 2020 18:10:54 +0000 (13:10 -0500)
committerGitHub <noreply@github.com>
Sat, 30 May 2020 18:10:54 +0000 (13:10 -0500)
commitba659fb1b8bc2f110616ec113892f63f210a5ebb
tree9beaf9be94879a75f4c2cadf8289664b53cc1d1btree
parentda165b9cbee366d4e77716617f2e2c794da9bd46commit | diff
Add the sequence type (#4539)

This adds basic infrastructure for the sequence type, including its type rules, type enumerator and extensions to type functions.

The next step will be to finalize the support in TheoryStrings for sequences and then add front end support for sequences in the API/parsers.
15 files changed:
src/bindings/java/CMakeLists.txt diff | blob | history
src/expr/node_manager.cpp diff | blob | history
src/expr/node_manager.h diff | blob | history
src/expr/type.cpp diff | blob | history
src/expr/type.h diff | blob | history
src/expr/type_node.cpp diff | blob | history
src/expr/type_node.h diff | blob | history
src/theory/strings/kinds diff | blob | history
src/theory/strings/rewrites.cpp diff | blob | history
src/theory/strings/rewrites.h diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history
src/theory/strings/sequences_rewriter.h diff | blob | history
src/theory/strings/theory_strings_type_rules.h diff | blob | history
src/theory/strings/type_enumerator.cpp diff | blob | history
src/theory/strings/type_enumerator.h diff | blob | history