* 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

4 files changed, 23 insertions, 17 deletions

diff --git a/src/context/context.cpp b/src/context/context.cpp
index abb1575d4..da60a5bc4 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -80,7 +80,7 @@ void Context::pop() {
   while(pCNO != NULL) {
     // pre-store the "next" pointer in case pCNO deletes itself on notify()
     ContextNotifyObj* next = pCNO->d_pCNOnext;
-    pCNO->notify();
+    pCNO->contextNotifyPop();
     pCNO = next;
   }
 
@@ -101,7 +101,7 @@ void Context::pop() {
   while(pCNO != NULL) {
     // pre-store the "next" pointer in case pCNO deletes itself on notify()
     ContextNotifyObj* next = pCNO->d_pCNOnext;
-    pCNO->notify();
+    pCNO->contextNotifyPop();
     pCNO = next;
   }
 
diff --git a/src/context/context.h b/src/context/context.h
index f0dbff72b..165c35c58 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -658,6 +658,7 @@ public:
  * the ContextObj objects have been restored).
  */
 class ContextNotifyObj {
+
   /**
    * Context is our friend so that when the Context is deleted, any
    * remaining ContextNotifyObj can be removed from the Context list.
@@ -686,6 +687,15 @@ class ContextNotifyObj {
    */
   ContextNotifyObj**& prev() throw() { return d_ppCNOprev; }
 
+protected:
+
+  /**
+   * This is the method called to notify the object of a pop.  It must be
+   * implemented by the subclass. It is protected since context is out
+   * friend.
+   */
+  virtual void contextNotifyPop() = 0;
+
 public:
 
   /**
@@ -703,12 +713,6 @@ public:
    */
   virtual ~ContextNotifyObj() throw(AssertionException);
 
-  /**
-   * This is the method called to notify the object of a pop.  It must be
-   * implemented by the subclass.
-   */
-  virtual void notify() = 0;
-
 };/* class ContextNotifyObj */
 
 inline void ContextObj::makeCurrent() throw(AssertionException) {
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();
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();