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>
	Sat, 1 Mar 2014 04:59:00 +0000 (22:59 -0600)
commit	acb79cbe43ddcd855db042b7c937fc2eacaa0ac3
tree	e8af21bba458cbc2a00d3512519cea3e07af3b65	tree
parent	76f497ef9444a81143ad35b2eda899e119b8e662	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