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

diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 27c1a2b69..958f50276 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -73,16 +73,16 @@ private:
   /** Helper class to invalidate cache on user pop */
   class CacheInvalidator : public context::ContextNotifyObj {
     bool& d_cacheInvalidated;
-
+  protected:
+    void contextNotifyPop() {
+      d_cacheInvalidated = true;
+    }
   public:
     CacheInvalidator(context::Context* context, bool& cacheInvalidated) :
       context::ContextNotifyObj(context),
       d_cacheInvalidated(cacheInvalidated) {
     }
 
-    void notify() {
-      d_cacheInvalidated = true;
-    }
   };/* class SubstitutionMap::CacheInvalidator */
 
   /**