* 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

2 files changed, 9 insertions, 1 deletions

diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index 33863e848..1a50d0637 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -37,7 +37,7 @@ struct MyContextNotifyObj : public ContextNotifyObj {
     nCalls(0) {
   }
 
-  void notify() {
+  void contextNotifyPop() {
     ++nCalls;
   }
 };
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 63ba95b57..c24104acc 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -59,6 +59,14 @@ public:
     return d_nextVar++;
   }
 
+  SatVariable trueVar() {
+    return d_nextVar++;
+  }
+
+  SatVariable falseVar() {
+    return d_nextVar++;
+  }
+
   void addClause(SatClause& c, bool lemma) {
     d_addClauseCalled = true;
   }