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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 23 May 2013 21:45:47 +0000 (16:45 -0500)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 23 May 2013 21:45:47 +0000 (16:45 -0500)
commit	fbc81b67ac1cfeb3afe37f3299180177faaa1ca6
tree	69b3028b333262b414ed188d1f575012793e0e2b	tree
parent	fee510eacd6ea9d35906218ce3d4b88f7d86f8b1	commit \| diff

Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.

19 files changed:

src/theory/arrays/Makefile.am		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_model.cpp	[deleted file]	blob \| history
src/theory/arrays/theory_arrays_model.h	[deleted file]	blob \| history
src/theory/quantifiers/Makefile.am		diff \| blob \| history
src/theory/quantifiers/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.h		diff \| blob \| history
src/theory/quantifiers/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/full_model_check.h		diff \| blob \| history
src/theory/quantifiers/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/model_builder.h		diff \| blob \| history
src/theory/quantifiers/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/model_engine.h		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp	[deleted file]	blob \| history
src/theory/quantifiers/relevant_domain.h	[deleted file]	blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/rep_set.cpp		diff \| blob \| history
test/Makefile.am		diff \| blob \| history