From c1392e60be77633aa8d81cfcbf1e05628b696d16 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Nov 2015 17:10:49 -0800
Subject: [PATCH] feat(util/rb_tree): add double_cmp

---
 src/util/rb_tree.h | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/util/rb_tree.h b/src/util/rb_tree.h
index 45b8dbad3..742b4bf3c 100644
--- a/src/util/rb_tree.h
+++ b/src/util/rb_tree.h
@@ -415,4 +415,7 @@ struct unsigned_cmp {
 struct int_cmp {
     int operator()(int i1, int i2) const { return i1 < i2 ? -1 : (i1 == i2 ? 0 : 1); }
 };
+struct double_cmp {
+    int operator()(double i1, double i2) const { return i1 < i2 ? -1 : (i1 > i2 ? 1 : 0); }
+};
 }