projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f26ea80) | patch
Basic support for regular expression complement (#3437)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 26 Feb 2020 19:54:41 +0000 (13:54 -0600)
committerGitHub <noreply@github.com>
Wed, 26 Feb 2020 19:54:41 +0000 (13:54 -0600)
commitb320aa323923822a7702997bbca05e8512da55a4
tree62ed510b54bbfef908296a264002052efc4fff98tree
parentf26ea8026e94252e4f1418be473d10a5f957b988commit | diff
Basic support for regular expression complement (#3437)

Fixes #3408 .

Adds basic rewriter, parsing, type checking and implements the required cases in regexp_operation.cpp. It also adds some missing documentation in regexp_operation.h
12 files changed:
src/api/cvc4cpp.cpp diff | blob | history
src/api/cvc4cppkind.h diff | blob | history
src/parser/cvc/Cvc.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/strings/kinds diff | blob | history
src/theory/strings/regexp_operation.cpp diff | blob | history
src/theory/strings/regexp_operation.h diff | blob | history
src/theory/strings/theory_strings_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/complement-simple.smt2 [new file with mode: 0644] blob
test/regress/regress1/strings/complement-test.smt2 [new file with mode: 0644] blob