1 files changed, 17 insertions, 6 deletions
diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h
index 383b9f8e8..ce78f281a 100644
--- a/src/theory/arith/unate_propagator.h
+++ b/src/theory/arith/unate_propagator.h
@@ -55,6 +55,7 @@
 #include "theory/arith/ordered_set.h"
 
 #include <ext/hash_map>
+#include <queue>
 
 namespace CVC4 {
 namespace theory {
@@ -62,11 +63,9 @@ namespace arith {
 
 class ArithUnatePropagator {
 private:
-  /**
-   * OutputChannel for the theory of arithmetic.
-   * The propagator uses this to pass implications back to the SAT solver.
-   */
-  OutputChannel& d_arithOut;
+  typedef std::queue<Node> LemmaQueue;
+  /** Unate implication queue */
+  LemmaQueue d_lemmas;
 
   struct OrderedSetTriple {
     OrderedSet d_leqSet;
@@ -79,7 +78,7 @@ private:
   NodeToOrderedSetMap d_orderedListMap;
 
 public:
-  ArithUnatePropagator(context::Context* cxt, OutputChannel& arith);
+  ArithUnatePropagator(context::Context* cxt);
 
   /**
    * Adds an atom to the propagator.
@@ -90,7 +89,19 @@ public:
   /** Returns true if v has been added as a left hand side in an atom */
   bool hasAnyAtoms(TNode v);
 
+  bool hasMoreLemmas() const { return !d_lemmas.empty(); }
+
+  Node getNextLemma() {
+    Node lemma = d_lemmas.front();
+    d_lemmas.pop();
+    return lemma;
+  }
 private:
+  void addLemma(Node lemma) {
+    d_lemmas.push(lemma);
+  }
+
+
   OrderedSetTriple& getOrderedSetTriple(TNode left);
   OrderedSet& getEqSet(TNode left);
   OrderedSet& getLeqSet(TNode left);