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>
	Tue, 24 Sep 2013 19:19:25 +0000 (14:19 -0500)
commit	dc7cf88e7d14748ed3227e552e15bf93f6ad22f9
tree	3ef699307030fbfdb9c533d988b79a052d9945de	tree
parent	5d1f359e22927f2bec78ba6a407485f65bc6ae0b	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