projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7c190dc) | patch
Adds regular expression support, it is actually CFL because of variables.
authorTianyi Liang <tianyi-liang@uiowa.edu>
Fri, 11 Oct 2013 21:54:22 +0000 (16:54 -0500)
committerTianyi Liang <tianyi-liang@uiowa.edu>
Fri, 11 Oct 2013 21:54:22 +0000 (16:54 -0500)
commitc388e89e5253aa6fbde7685fc53126872f578f0b
tree0ace860103f2ad2da266e1f639d170baac73b4datree
parent7c190dcead07d797d475a07522c595f97c7ef2dbcommit | diff
Adds regular expression support, it is actually CFL because of variables.
src/theory/strings/options diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings.h diff | blob | history
src/theory/strings/theory_strings_rewriter.cpp diff | blob | history
src/theory/strings/theory_strings_rewriter.h diff | blob | history
src/theory/strings/theory_strings_type_rules.h diff | blob | history
test/regress/regress0/strings/Makefile.am diff | blob | history
test/regress/regress0/strings/loop005.smt2 diff | blob | history
test/regress/regress0/strings/loop007.smt2 diff | blob | history
test/regress/regress0/strings/loop008.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/regexp001.smt2 [new file with mode: 0644] blob