Relaxed the constant requirement for regular expression loop;
authorTianyi Liang <tianyi-liang@uiowa.edu>
Fri, 5 Dec 2014 00:17:55 +0000 (18:17 -0600)
committerTianyi Liang <tianyi-liang@uiowa.edu>
Fri, 5 Dec 2014 00:17:55 +0000 (18:17 -0600)
commitf8c5e78d97eb7ddc3a29392c9ca18c627279fa2b
tree597fe7c703d3d2bc8fc05440d3529d348bb6a1c8
parent31175341b81e26f7373d75f65cddc69386f0ac86
Relaxed the constant requirement for regular expression loop;
Added "ignoring negative membership" option (fragment checking is not provided,
and users must make sure the constraint is in the fragment;
otherwise, the solution may not be correct).
src/theory/strings/options
src/theory/strings/regexp_operation.cpp
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings_rewriter.cpp
src/theory/strings/theory_strings_type_rules.h
test/regress/regress0/strings/Makefile.am
test/regress/regress0/strings/regexp002.smt2