diff --git a/src/library/class.cpp b/src/library/class.cpp index 0947f022a..7d7d0363a 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -346,6 +346,19 @@ bool is_instance(environment const & env, name const & i) { return s.is_instance(i); } +name_predicate mk_class_pred(environment const & env) { + class_state const & s = class_ext::get_state(env); + class_state::class_instances cs = s.m_instances; + return [=](name const & n) { return cs.contains(n); }; // NOLINT +} + +name_predicate mk_instance_pred(environment const & env) { + class_state const & s = class_ext::get_state(env); + class_state::instance_priorities insts = s.m_priorities; + name_set der_insts = s.m_derived_trans_instance_set; + return [=](name const & n) { return insts.contains(n) || der_insts.contains(n); }; // NOLINT +} + bool is_derived_trans_instance(environment const & env, name const & i) { class_state const & s = class_ext::get_state(env); return s.is_derived_trans_instance(i); diff --git a/src/library/class.h b/src/library/class.h index f0f439bf9..71b34d70d 100644 --- a/src/library/class.h +++ b/src/library/class.h @@ -23,6 +23,10 @@ environment add_trans_instance(environment const & env, name const & n, unsigned bool is_class(environment const & env, name const & c); /** \brief Return true iff \c i was declared with \c add_instance. */ bool is_instance(environment const & env, name const & i); +/** \brief Return the set of active classes (as a predicate) for the given environment */ +name_predicate mk_class_pred(environment const & env); +/** \brief Return the set of active instances (as a predicate) for the given environment */ +name_predicate mk_instance_pred(environment const & env); /** \brief Return true iff \c i is a derived transitive instance. */ bool is_derived_trans_instance(environment const & env, name const & i); /** \brief Return the instances of the given class. */