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

author	Clark Barrett <barrett@cs.nyu.edu>
	Wed, 7 Jul 2010 02:18:42 +0000 (02:18 +0000)
committer	Clark Barrett <barrett@cs.nyu.edu>
	Wed, 7 Jul 2010 02:18:42 +0000 (02:18 +0000)
commit	daf3b024547deaf1cf53b66ed046fbb15584b9d3
tree	91a2b7ebfe804041ad531ae897a037bdde61a4a7	tree
parent	34ef50c2fcfa4d6aa8337c3096defa56d7dc0093	commit \| diff

Added shared term manager. Basic mechanism for identifying shared terms is
working. Still need to implement theory-specific shared term propagation.

22 files changed:

src/prop/sat.h		diff \| blob \| history
src/theory/Makefile.am		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/booleans/theory_bool.h		diff \| blob \| history
src/theory/builtin/theory_builtin.h		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/shared_data.cpp	[new file with mode: 0644]	blob
src/theory/shared_data.h	[new file with mode: 0644]	blob
src/theory/shared_term_manager.cpp	[new file with mode: 0644]	blob
src/theory/shared_term_manager.h	[new file with mode: 0644]	blob
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
test/unit/theory/theory_arith_white.h		diff \| blob \| history
test/unit/theory/theory_black.h		diff \| blob \| history
test/unit/theory/theory_engine_white.h		diff \| blob \| history
test/unit/theory/theory_uf_white.h		diff \| blob \| history