projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f827fb0) | patch
Fixes for strings, explanations for constant split propagations, substr under concat...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 21 Jul 2016 15:56:09 +0000 (10:56 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 21 Jul 2016 15:56:09 +0000 (10:56 -0500)
commitb5956e457da61e4d49cd35e0a73ba423230a25e0
tree26fd0ce8f9bd511d967a2be2cbe9c6cd5dc21b08tree
parentf827fb06c949d421fb32f6629c2c353ca7bd026ecommit | diff
Fixes for strings, explanations for constant split propagations, substr under concat rewrite. Avoid duplicate re.range length lemmas.
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
test/regress/regress0/strings/Makefile.am diff | blob | history
test/regress/regress0/strings/cmu-substr-rw.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/csp-prefix-exp-bug.smt2 [new file with mode: 0644] blob