diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-14 07:26:09 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-14 07:26:09 +0000 |
| commit | cd22e76d6934416d279396b0a2472b1bd81174c9 (patch) | |
| tree | 8a5946ef0e6afa3f3b6b0c586a337b901467d743 /src/theory/uf/equality_engine.h | |
| parent | 4dad25f2c1377603ff1f035887acce3b30d40d56 (diff) | |
changing to a more natural propagation order in uf, seems to pay off
Diffstat (limited to 'src/theory/uf/equality_engine.h')
| -rw-r--r-- | src/theory/uf/equality_engine.h | 5 |
1 files changed, 3 insertions, 2 deletions
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(); |