git.libre-soc.org Git - cvc5.git/commit

projects / cvc5.git / commit

summary | shortlog | log | commit | commitdiff | tree
(parent: f5ca3e5) | patch

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 23 Dec 2019 23:18:19 +0000 (17:18 -0600)
committer	Andres Noetzli <andres.noetzli@gmail.com>
	Mon, 23 Dec 2019 23:18:19 +0000 (15:18 -0800)
commit	b3471b719f1cd031d35e9a431027088b0dec156b
tree	bc5e55a278f9e927471ce99146e9fdc992bc716b	tree
parent	f5ca3e5d09b457ac21b10793eb5d1efe3fbe40f6	commit \| diff

Initial support for string reverse (#3581)

Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`).

Also improves support in a few places for tolower/toupper.

19 files changed:

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/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/strings/theory_strings_rewriter.cpp		diff \| blob \| history
src/theory/strings/theory_strings_rewriter.h		diff \| blob \| history
src/util/regexp.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/strings/parser-syms.cvc	[new file with mode: 0644]	blob
test/regress/regress0/strings/str-rev-simple.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/rev-conv1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/rev-ex1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/rev-ex2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/rev-ex3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/rev-ex4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/rev-ex5.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/str-rev-simple-s.smt2	[new file with mode: 0644]	blob