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

author	Morgan Deters <mdeters@cs.nyu.edu>
	Thu, 9 Oct 2014 00:16:58 +0000 (20:16 -0400)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Tue, 14 Oct 2014 20:41:17 +0000 (16:41 -0400)
commit	ef000094d2d6a024c7eac490b241259b38e07225
tree	395250d07c9e589b1ba42316516deddfe1486018	tree
parent	7df24c61c7998e1485ab75219078deaf1455bd71	commit \| diff

Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.

22 files changed:

src/expr/attribute.cpp		diff \| blob \| history
src/expr/attribute.h		diff \| blob \| history
src/expr/expr_manager_template.cpp		diff \| blob \| history
src/expr/expr_manager_template.h		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/quantifiers/first_order_reasoning.cpp		diff \| blob \| history
src/theory/quantifiers/macros.cpp		diff \| blob \| history
test/unit/context/stacking_map_black.h		diff \| blob \| history
test/unit/context/stacking_vector_black.h		diff \| blob \| history
test/unit/expr/attribute_black.h		diff \| blob \| history
test/unit/expr/attribute_white.h		diff \| blob \| history
test/unit/expr/node_black.h		diff \| blob \| history
test/unit/expr/node_builder_black.h		diff \| blob \| history
test/unit/expr/node_manager_black.h		diff \| blob \| history
test/unit/expr/node_manager_white.h		diff \| blob \| history
test/unit/expr/node_self_iterator_black.h		diff \| blob \| history
test/unit/expr/node_white.h		diff \| blob \| history
test/unit/util/boolean_simplification_black.h		diff \| blob \| history