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

author	Tim King <taking@cs.nyu.edu>
	Wed, 5 Dec 2012 19:06:21 +0000 (19:06 +0000)
committer	Tim King <taking@cs.nyu.edu>
	Wed, 5 Dec 2012 19:06:21 +0000 (19:06 +0000)
commit	7f52115ab0dcba4c8ba9403a5f25b8e8c588911a
tree	14b74c89069cd6e9b443853ac1f15cca2ce586a1	tree
parent	7efd777609f7fbc20701402ad949971cbc251f8f	commit \| diff

This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>. Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.

22 files changed:

src/context/Makefile.am		diff \| blob \| history
src/context/cdhashmap.h		diff \| blob \| history
src/context/cdhashmap_forward.h		diff \| blob \| history
src/context/cdhashset.h		diff \| blob \| history
src/context/cdinsert_hashmap.h	[new file with mode: 0644]	blob
src/context/cdinsert_hashmap_forward.h	[new file with mode: 0644]	blob
src/context/cdtrail_hashmap.h	[new file with mode: 0644]	blob
src/context/cdtrail_hashmap_forward.h	[new file with mode: 0644]	blob
src/decision/justification_heuristic.h		diff \| blob \| history
src/decision/relevancy.h		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.h		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/circuit_propagator.h		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history

RSS Atom