From daef2b7b24d3efed4238af80281aa6894e8407f7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Dec 2013 10:53:53 -0800
Subject: [PATCH] feat(util/sexpr/options): add is_eqp predicate for options

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/options.cpp | 12 ++++++++++++
 src/util/sexpr/options.h   |  2 ++
 2 files changed, 14 insertions(+)

diff --git a/src/tests/util/options.cpp b/src/tests/util/options.cpp
index 7209218ee7..be7c9738c2 100644
--- a/src/tests/util/options.cpp
+++ b/src/tests/util/options.cpp
@@ -124,6 +124,17 @@ static void tst5() {
     lean_assert(it2 == decls.end());
 }
 
+static void tst6() {
+    options opt, opt2;
+    lean_assert(is_eqp(opt, opt2));
+    opt = update(opt, name{"test", "foo"}, 10);
+    lean_assert(!is_eqp(opt, opt2));
+    opt2 = update(opt2, name{"test", "foo"}, 10);
+    lean_assert(!is_eqp(opt, opt2));
+    opt2 = opt;
+    lean_assert(is_eqp(opt, opt2));
+}
+
 int main() {
     save_stack_info();
     tst1();
@@ -131,5 +142,6 @@ int main() {
     tst3();
     tst4();
     tst5();
+    tst6();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h
index c7f831b468..c2d4dae045 100644
--- a/src/util/sexpr/options.h
+++ b/src/util/sexpr/options.h
@@ -53,6 +53,8 @@ public:
     options update(char const * n, sexpr const & v) const { return update(name(n), v); }
     template<typename T> options update(char const * n, T v) const { return update(n, sexpr(v)); }
 
+    friend bool is_eqp(options const & a, options const & b) { return is_eqp(a.m_value, b.m_value); }
+
     /**
        \brief Combine the options opts1 and opts2. The assignment in
        opts2 overrides the ones in opts1.