git.libre-soc.org Git - cvc5.git/commit

author	Tianyi Liang <tianyi-liang@uiowa.edu>
	Fri, 28 Feb 2014 17:05:09 +0000 (11:05 -0600)
committer	Tianyi Liang <tianyi-liang@uiowa.edu>
	Fri, 28 Feb 2014 17:05:09 +0000 (11:05 -0600)
commit	cdefee8664d3e99a4cd97c4affbc639937187d50
tree	d13b964dc8c176fbb226baa810c0e0d4eaadb303	tree
parent	7a6c462b0ce3adf52a9d44a5f98c53065fedc33d	commit \| diff

a new regular expression engine for solving both positive and negative membership constraints

21 files changed:

src/parser/smt2/Smt2.g		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/strings/kinds		diff \| blob \| history
src/theory/strings/options		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/regexp_operation.h		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
src/theory/strings/theory_strings_rewriter.cpp		diff \| blob \| history
src/theory/strings/theory_strings_type_rules.h		diff \| blob \| history
test/regress/regress0/strings/Makefile.am		diff \| blob \| history
test/regress/regress0/strings/fmf001.smt2		diff \| blob \| history
test/regress/regress0/strings/fmf002.smt2		diff \| blob \| history
test/regress/regress0/strings/loop007.smt2		diff \| blob \| history
test/regress/regress0/strings/loop008.smt2		diff \| blob \| history
test/regress/regress0/strings/loop009.smt2		diff \| blob \| history
test/regress/regress0/strings/regexp001.smt2		diff \| blob \| history
test/regress/regress0/strings/regexp002.smt2		diff \| blob \| history