diff options
Diffstat (limited to 'src/theory/arith/unate_propagator.h')
-rw-r--r-- | src/theory/arith/unate_propagator.h | 23 |
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); |