projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 645aaaa) | patch
More improvements to strings rewriter for regexps, contains, indexof, replace and...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 6 Oct 2015 11:26:03 +0000 (13:26 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 6 Oct 2015 11:26:03 +0000 (13:26 +0200)
commit6343fbb0c9b238aeb1addca6449f95a01071c1ac
tree60f872134b3697a88d639ffa5adf73c5db02c5d1tree
parent645aaaa186269c26d96a60c8df3350a2de9b6acbcommit | diff
More improvements to strings rewriter for regexps, contains, indexof, replace and others.  Enable non-recursive flat form inferences in strings theory solver. Refactor extf reductions. Use non-constant length terms when checking length equality. Add option --strings-eager-len.
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/util/regexp.h diff | blob | history
test/regress/regress0/strings/Makefile.am diff | blob | history
test/regress/regress0/strings/idof-rewrites.smt2 [new file with mode: 0644] blob
test/regress/regress0/strings/kaluza-fl.smt2 [new file with mode: 0755] blob
test/regress/regress0/strings/norn-ab.smt2 [new file with mode: 0755] blob