projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f9899f4) | patch
Refactoring of strings preprocess module. When enabled, apply eager preprocess during...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 7 Jul 2016 20:22:40 +0000 (15:22 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 7 Jul 2016 20:22:50 +0000 (15:22 -0500)
commitf62609d9eca8086d5c68b77cfd0a5d717d24aeab
tree55b504bf063bcbde7e71be13078e9b9a7df4a984tree
parentf9899f4ffc081369f419b8572a5aa397fbaa428acommit | diff
Refactoring of strings preprocess module. When enabled, apply eager preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains.  Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.
src/smt/smt_engine.cpp diff | blob | history
src/theory/sep/theory_sep.cpp 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_preprocess.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.h diff | blob | history
test/regress/regress0/strings/Makefile.am diff | blob | history
test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 [new file with mode: 0644] blob