projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cca1537) | patch
Add support for is_digit and regular expression difference (#3828)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 27 Feb 2020 03:54:29 +0000 (21:54 -0600)
committerGitHub <noreply@github.com>
Thu, 27 Feb 2020 03:54:29 +0000 (21:54 -0600)
commit87f3741db6ed41d3a776774bc1b60fd696585391
tree26f2498075d175ecc6c18743cb21ff3998ccc008tree
parentcca153771119b70cbf01a3d05d8e2fd8d7e8636acommit | diff
Add support for is_digit and regular expression difference (#3828)

Towards support for the strings standard. This adds support for str.is_digit and re.diff, which both can be eliminated eager during preprocessing.
src/api/cvc4cpp.cpp diff | blob | history
src/api/cvc4cppkind.h diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/theory/strings/kinds diff | blob | history
src/theory/strings/theory_strings_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/is_digit_simple.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/re_diff.smt2 [new file with mode: 0644] blob