projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 627b850) | patch
Improvements to rewriter for regexp, contains, indexof. Improvements and fixes for...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 2 Oct 2015 13:10:10 +0000 (15:10 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 2 Oct 2015 13:10:10 +0000 (15:10 +0200)
commitb0feac10d73770819839624dd943eedb14bd4c86
treea5410baf7d47ae6ffc3fe0f177017d157e11be40tree
parent627b8507183ae6c58b2eda80ca14500b1fa87809commit | diff
Improvements to rewriter for regexp, contains, indexof. Improvements and fixes for reduction of indexof. Fixes bugs 612 and 615. Fix bug in find+offset in strings util. Add regressions.
13 files changed:
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/regress0/strings/Makefile.am diff | blob | history
test/regress/regress0/strings/bug612.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/bug615.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/idof-handg.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/idof-nconst-index.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/idof-neg-index.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/norn-simp-rew-sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/norn-simp-rew.smt2 [new file with mode: 0755] blob