From 69a3e984aa12aaaaa7a1318aad7913dbb035313d Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Tue, 20 Jun 2017 20:09:33 -0400
Subject: [PATCH] add is_hypothesis() method

---
 src/ast/ast.h | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ast/ast.h b/src/ast/ast.h
index 6bb3b01c9..475e58ac7 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -2082,6 +2082,7 @@ public:
 
     bool is_undef_proof(expr const * e) const { return e == m_undef_proof; }
     bool is_asserted(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_ASSERTED); }
+    bool is_hypothesis (expr const *e) const {return is_app_of (e, m_basic_family_id, PR_HYPOTHESIS);}
     bool is_goal(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_GOAL); }
     bool is_modus_ponens(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_MODUS_PONENS); }
     bool is_reflexivity(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_REFLEXIVITY); }
@@ -2112,6 +2113,7 @@ public:
     bool is_skolemize(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_SKOLEMIZE); }
 
     MATCH_UNARY(is_asserted);
+    MATCH_UNARY(is_hypothesis);
     MATCH_UNARY(is_lemma);
 
     bool has_fact(proof const * p) const {