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

diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 78221a617..f5e4f4630 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -79,17 +79,17 @@ private:
   template <class T>
   class DataClearer : context::ContextNotifyObj {
     T& d_data;
+  protected:
+    void contextNotifyPop() {
+      Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
+                            << "(size was " << d_data.size() << ")" << std::endl;
+      d_data.clear();
+    }
   public:
     DataClearer(context::Context* context, T& data) :
       context::ContextNotifyObj(context),
       d_data(data) {
     }
-
-    void notify() {
-      Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
-                            << "(size was " << d_data.size() << ")" << std::endl;
-      d_data.clear();
-    }
   };/* class DataClearer<T> */
 
   /**