projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bfeedc8) | patch
Improve rewriting for string contains part 2 (#1300)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 6 Nov 2017 05:14:16 +0000 (23:14 -0600)
committerGitHub <noreply@github.com>
Mon, 6 Nov 2017 05:14:16 +0000 (23:14 -0600)
commitd72fcccb19e43d0140b8a6ac954c2858dd3a239a
treefb09b00709495c3c6fd2a26169269843e989a060tree
parentbfeedc822f39875c7d54dac0a744a63c5dc838bdcommit | diff
Improve rewriting for string contains part 2 (#1300)

* Generalize component contains, some infrastructure.

* Length entailment, substr for component contains, int.to.str for constant can contain concat.

* Disable rewrite.

* Fix, reenable length entailment for contains.

* Clang format, minor.

* Comment

* Minor fixes and improvements for comments.

* Improvements

* Clang format

* Fixes

* Clang format

* Fix, improve.

* Format

* Fix assertion
src/theory/strings/theory_strings_rewriter.cpp diff | blob | history
src/theory/strings/theory_strings_rewriter.h diff | blob | history
test/regress/regress0/strings/Makefile.am diff | blob | history
test/regress/regress0/strings/rewrites-v2.smt2 [new file with mode: 0644] blob