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

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 5c73da1f6..2871d5559 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -309,8 +309,10 @@ class TheoryEngine {
   }
 
   struct SharedLiteral {
-    /** The node/theory pair for the assertion */
-    /** THEORY_LAST indicates this is a SAT literal and should be sent to the SAT solver */
+    /**
+     * The node/theory pair for the assertion. THEORY_LAST indicates this is a SAT
+     * literal and should be sent to the SAT solver
+     */
     NodeTheoryPair toAssert;
     /** This is the node that we will use to explain it */
     Node toExplain;
@@ -319,7 +321,7 @@ class TheoryEngine {
     : toAssert(assertion, receivingTheory),
       toExplain(original)
     { }
-  };/* struct SharedLiteral */
+  };
 
   /**
    * Map from nodes to theories.
@@ -728,6 +730,9 @@ private:
   /** Visitor for collecting shared terms */
   SharedTermsVisitor d_sharedTermsVisitor;
 
+  /** Prints the assertions to the debug stream */
+  void printAssertions(const char* tag);
+
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */