* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,
authorMorgan Deters <mdeters@gmail.com>
Fri, 12 Mar 2010 19:41:04 +0000 (19:41 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 12 Mar 2010 19:41:04 +0000 (19:41 +0000)
commit20b3dabb4823ede8147a08a47f8d909980414bee
tree6d6ea617bef8d840de8f8ff737e00acadb6675f9
parent3cf73e344987c2449943ca3a97054565eb9d5726
* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,
  DecisionEngine, and Theory.  These are triggered from the SmtEngine
  dtor before the other engines are deleted.  This is important
  because of potential issues with outstanding TNodes in Theory
  implementations (which fail if the destruction is done in the wrong
  order, in certain cases).

* Favor "FactQueueResetter" instead of clearAssertionQueues() for
  resetting facts queue in Theory implementations.

* Better theory-rewriting code.

* Minor cleanups.
src/prop/minisat/core/Solver.C
src/prop/prop_engine.h
src/prop/sat.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/theory_uf.cpp
src/util/decision_engine.cpp
src/util/decision_engine.h