michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library): add helper function

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-15 15:56:18 -07:00
parent 18742e8ab8
commit d41bff8c43
3 changed files with 13 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/locals.cpp
View file

@ -88,4 +88,8 @@ optional<expr> depends_on(unsigned sz, expr const * es, expr const & h) {
return some_expr(es[i]);
return none_expr();
}
bool depends_on_any(expr const & e, unsigned hs_sz, expr const * hs) {
return std::any_of(hs, hs+hs_sz, [&](expr const & h) { return depends_on(e, h); });
}
}

6
src/library/locals.h
View file

@ -40,4 +40,10 @@ inline bool depends_on(expr const & e, expr const & h) {
/** \brief Return true iff one of \c es contains the local constant \c h */
optional<expr> depends_on(unsigned sz, expr const * es, expr const & h);
/** \brief Return true iff \c e depends on any of the local constants in \c hs */
bool depends_on_any(expr const & e, unsigned hs_sz, expr const * hs);
inline bool depends_on_any(expr const & e, buffer<expr> const & hs) {
return depends_on_any(e, hs.size(), hs.data());
}
}

6
src/library/tactic/inversion_tactic.cpp
View file

@ -190,7 +190,7 @@ class inversion_tac {
}
if (!m_dep_elim) {
expr const & g_type = g.get_type();
if (std::any_of(args.end() - m_nindices, args.end(), [&](expr const & arg) { return depends_on(g_type, arg); }))
if (depends_on_any(g_type, m_nindices, args.end() - m_nindices))
return false;
}
buffer<expr> hyps;
@ -203,7 +203,7 @@ class inversion_tac {
continue;
// h1 is not h nor any of the indices
// Thus, it must not depend on the indices
if (std::any_of(args.end() - m_nindices, args.end(), [&](expr const & arg) { return depends_on(h1, arg); }))
if (depends_on_any(h1, m_nindices, args.end() - m_nindices))
return false;
}
return true;
@ -216,7 +216,7 @@ class inversion_tac {
void split_deps(buffer<expr> const & hyps, expr const & H, buffer<expr> & non_deps, buffer<expr> & deps, bool clear_H = false) {
for (expr const & hyp : hyps) {
expr const & hyp_type = mlocal_type(hyp);
if (depends_on(hyp_type, H) || std::any_of(deps.begin(), deps.end(), [&](expr const & dep) { return depends_on(hyp_type, dep); })) {
if (depends_on(hyp_type, H) || depends_on_any(hyp_type, deps)) {
deps.push_back(hyp);
} else if (hyp != H || !clear_H) {
non_deps.push_back(hyp);