From cd22e76d6934416d279396b0a2472b1bd81174c9 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 14 Jun 2012 07:26:09 +0000
Subject: changing to a more natural propagation order in uf, seems to pay off

---
 src/theory/uf/equality_engine.h | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/theory/uf/equality_engine.h')

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index e7e8893a3..5a5b62105 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -22,6 +22,7 @@
 #pragma once
 
 #include <queue>
+#include <deque>
 #include <vector>
 #include <ext/hash_map>
 
@@ -415,10 +416,10 @@ private:
   EqualityNodeId newNode(TNode t);
 
   /** Propagation queue */
-  std::queue<MergeCandidate> d_propagationQueue;
+  std::deque<MergeCandidate> d_propagationQueue;
 
   /** Enqueue to the propagation queue */
-  void enqueue(const MergeCandidate& candidate);
+  void enqueue(const MergeCandidate& candidate, bool back = true);
 
   /** Do the propagation */
   void propagate();
-- 
cgit v1.2.3