From 77f742ae8e5c51225601bd6480f8ca6d29e646cc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 27 May 2015 12:07:06 -0700
Subject: [PATCH] feat(library/relation_manager): add auxiliary functions

---
 src/library/relation_manager.cpp | 4 ++++
 src/library/relation_manager.h   | 5 +++++
 2 files changed, 9 insertions(+)

diff --git a/src/library/relation_manager.cpp b/src/library/relation_manager.cpp
index 8dacca1e4..b7dd74f9c 100644
--- a/src/library/relation_manager.cpp
+++ b/src/library/relation_manager.cpp
@@ -226,6 +226,10 @@ optional<std::tuple<name, name, unsigned>> get_trans_extra_info(environment cons
     }
 }
 
+bool is_subst_relation(environment const & env, name const & op) {
+    return rel_ext::get_state(env).m_subst_table.contains(op);
+}
+
 optional<name> get_refl_info(environment const & env, name const & op) {
     if (auto it = get_refl_extra_info(env, op))
         return optional<name>(std::get<0>(*it));
diff --git a/src/library/relation_manager.h b/src/library/relation_manager.h
index f1a6d14f1..74f694b29 100644
--- a/src/library/relation_manager.h
+++ b/src/library/relation_manager.h
@@ -41,6 +41,11 @@ optional<std::tuple<name, name, unsigned>> get_trans_extra_info(environment cons
 optional<name> get_refl_info(environment const & env, name const & op);
 optional<name> get_symm_info(environment const & env, name const & op);
 optional<name> get_trans_info(environment const & env, name const & op);
+bool is_subst_relation(environment const & env, name const & op);
+inline bool is_trans_relation(environment const & env, name const & op) { return static_cast<bool>(get_trans_info(env, op)); }
+inline bool is_symm_relation(environment const & env, name const & op) { return static_cast<bool>(get_symm_info(env, op)); }
+inline bool is_refl_relation(environment const & env, name const & op) { return static_cast<bool>(get_refl_info(env, op)); }
+
 void initialize_relation_manager();
 void finalize_relation_manager();
 }