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

author	Tianyi Liang <tianyi-liang@uiowa.edu>
	Mon, 23 Sep 2013 21:54:32 +0000 (16:54 -0500)
committer	Tianyi Liang <tianyi-liang@uiowa.edu>
	Fri, 27 Sep 2013 14:25:52 +0000 (09:25 -0500)
commit	4612dd66cee87b7d4b735b416785d539083757fa
tree	f8cf493cfc3a8edfe7421cfc40b02b59cdd0d395	tree
parent	ccd1ca4c32e8a3eac8b18911a7b2d32b55203707	commit \| diff

adds model generation for strings, and a hacked way in arith engine for models

src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.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/type_enumerator.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/util/regexp.h		diff \| blob \| history
test/regress/regress0/strings/Makefile.am		diff \| blob \| history
test/regress/regress0/strings/model001.smt2	[new file with mode: 0644]	blob