mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

add is_hypothesis() method

Browse source
This commit is contained in:
Arie Gurfinkel 2017-06-20 20:09:33 -04:00
parent e48e7ef7be
commit 69a3e984aa
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.h
View file

@ -2082,6 +2082,7 @@ public:
bool is_undef_proof(expr const * e) const { return e == m_undef_proof; } 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_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_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_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); } 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); } 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_asserted);
MATCH_UNARY(is_hypothesis);
MATCH_UNARY(is_lemma); MATCH_UNARY(is_lemma);
bool has_fact(proof const * p) const { bool has_fact(proof const * p) const {