* 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, 9 insertions, 7 deletions

diff --git a/src/context/stacking_map.h b/src/context/stacking_map.h
index 2dec1845c..ba644596e 100644
--- a/src/context/stacking_map.h
+++ b/src/context/stacking_map.h
@@ -96,6 +96,14 @@ class StackingMap : context::ContextNotifyObj {
   /** Our current offset in the d_trace stack (context-dependent). */
   context::CDO<size_t> d_offset;
 
+protected:
+
+  /**
+   * Called by the Context when a pop occurs.  Cancels everything to the
+   * current context level.  Overrides ContextNotifyObj::contextNotifyPop().
+   */
+  void contextNotifyPop();
+
 public:
   typedef typename MapType::const_iterator const_iterator;
 
@@ -128,12 +136,6 @@ public:
    */
   void set(ArgType n, const ValueType& newValue);
 
-  /**
-   * Called by the Context when a pop occurs.  Cancels everything to the
-   * current context level.  Overrides ContextNotifyObj::notify().
-   */
-  void notify();
-
 };/* class StackingMap<> */
 
 template <class KeyType, class ValueType, class KeyHash>
@@ -146,7 +148,7 @@ void StackingMap<KeyType, ValueType, KeyHash>::set(ArgType n, const ValueType& n
 }
 
 template <class KeyType, class ValueType, class KeyHash>
-void StackingMap<KeyType, ValueType, KeyHash>::notify() {
+void StackingMap<KeyType, ValueType, KeyHash>::contextNotifyPop() {
   Trace("sm") << "SM cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl;
   while(d_offset < d_trace.size()) {
     std::pair<ArgType, ValueType> p = d_trace.back();