* simplifying equality engine interface

* notifications are now through the interface subclass instead of a template
* notifications include constants being merged
* changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed
* sat solver now has explicit methods to make true and false constants
* 0-level literals are removed from explanations of propagations

1 files changed, 2 insertions, 2 deletions

diff --git a/src/context/stacking_vector.h b/src/context/stacking_vector.h
index 9987731d4..ed311b952 100644
--- a/src/context/stacking_vector.h
+++ b/src/context/stacking_vector.h
@@ -82,7 +82,7 @@ public:
    * Called by the Context when a pop occurs.  Cancels everything to the
    * current context level.  Overrides ContextNotifyObj::notify().
    */
-  void notify();
+  void contextNotifyPop();
 
 };/* class StackingVector<> */
 
@@ -99,7 +99,7 @@ void StackingVector<T>::set(size_t n, const T& newValue) {
 }
 
 template <class T>
-void StackingVector<T>::notify() {
+void StackingVector<T>::contextNotifyPop() {
   Trace("sv") << "SV cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl;
   while(d_offset < d_trace.size()) {
     std::pair<size_t, T> p = d_trace.back();