From 89a5d00714b92c21f12e958735e663b916c75531 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Dec 2015 08:52:24 -0800 Subject: [PATCH] chore(library/blast): style --- src/library/blast/discr_tree.cpp | 16 +++++++++++----- src/library/blast/discr_tree.h | 13 ++++++------- src/library/blast/state.cpp | 2 +- src/library/blast/state.h | 2 +- 4 files changed, 19 insertions(+), 14 deletions(-) diff --git a/src/library/blast/discr_tree.cpp b/src/library/blast/discr_tree.cpp index b4f2eb243a..495b5e9a0c 100644 --- a/src/library/blast/discr_tree.cpp +++ b/src/library/blast/discr_tree.cpp @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include +#include #include "util/rb_map.h" #include "util/memory_pool.h" #include "library/blast/trace.h" @@ -26,6 +28,10 @@ struct discr_tree::node_cmp { int operator()(node const & n1, node const & n2) const; }; +void discr_tree::swap(node & n1, node & n2) { + std::swap(n1.m_ptr, n2.m_ptr); +} + struct discr_tree::edge { edge_kind m_kind; bool m_fn; @@ -246,7 +252,7 @@ void discr_tree::insert_erase(expr const & k, expr const & v, bool ins) { lean_trace("discr_tree", tout() << "\n"; trace();); } -bool discr_tree::find_atom(node const & n, edge const & e, list> todo, std::function const & fn) { +bool discr_tree::find_atom(node const & n, edge const & e, list> todo, std::function const & fn) { // NOLINT if (auto child = n.m_ptr->m_children.find(e)) { return find(*child, todo, fn); } else { @@ -254,7 +260,7 @@ bool discr_tree::find_atom(node const & n, edge const & e, list } } -bool discr_tree::find_star(node const & n, list> todo, std::function const & fn) { +bool discr_tree::find_star(node const & n, list> todo, std::function const & fn) { // NOLINT bool cont = true; n.m_ptr->m_skip.for_each([&](node const & skip_child) { if (cont && !find(skip_child, todo, fn)) @@ -270,7 +276,7 @@ bool discr_tree::find_star(node const & n, list> todo, std::fun return cont; } -bool discr_tree::find_app(node const & n, expr const & e, list> todo, std::function const & fn) { +bool discr_tree::find_app(node const & n, expr const & e, list> todo, std::function const & fn) { // NOLINT lean_assert(is_app(e)); buffer args; expr const & f = get_app_args(e, args); @@ -296,7 +302,7 @@ bool discr_tree::find_app(node const & n, expr const & e, list> } } -bool discr_tree::find(node const & n, list> todo, std::function const & fn) { +bool discr_tree::find(node const & n, list> todo, std::function const & fn) { // NOLINT if (!todo) { bool cont = true; n.m_ptr->m_values.for_each([&](expr const & v) { @@ -330,7 +336,7 @@ bool discr_tree::find(node const & n, list> todo, std::function lean_unreachable(); } -void discr_tree::find(expr const & e, std::function const & fn) const { +void discr_tree::find(expr const & e, std::function const & fn) const { // NOLINT if (m_root) find(m_root, to_list(mk_pair(e, false)), fn); } diff --git a/src/library/blast/discr_tree.h b/src/library/blast/discr_tree.h index 9678b0b808..c2580916b0 100644 --- a/src/library/blast/discr_tree.h +++ b/src/library/blast/discr_tree.h @@ -48,9 +48,8 @@ private: bool is_shared() const; node steal() { node r; swap(r, *this); return r; } void trace(optional const & e, unsigned depth, bool disj) const; - friend void swap(node & n1, node & n2) { std::swap(n1.m_ptr, n2.m_ptr); } }; - + static void swap(node & n1, node & n2); static node ensure_unshared(node && n); static node insert_erase_atom(node && n, edge const & e, buffer> & todo, expr const & v, buffer> & skip, bool ins); static node insert_erase_star(node && n, buffer> & todo, expr const & v, buffer> & skip, bool ins); @@ -59,10 +58,10 @@ private: static node insert_erase(node && n, bool is_root, buffer> & todo, expr const & v, buffer> & skip, bool ins); void insert_erase(expr const & k, expr const & v, bool ins); - static bool find_atom(node const & n, edge const & e, list> todo, std::function const & fn); - static bool find_star(node const & n, list> todo, std::function const & fn); - static bool find_app(node const & n, expr const & e, list> todo, std::function const & fn); - static bool find(node const & n, list> todo, std::function const & fn); + static bool find_atom(node const & n, edge const & e, list> todo, std::function const & fn); // NOLINT + static bool find_star(node const & n, list> todo, std::function const & fn); // NOLINT + static bool find_app(node const & n, expr const & e, list> todo, std::function const & fn); // NOLINT + static bool find(node const & n, list> todo, std::function const & fn); // NOLINT node m_root; public: @@ -71,7 +70,7 @@ public: void erase(expr const & k, expr const & v) { insert_erase(k, v, false); } void erase(expr const & k) { erase(k, k); } - void find(expr const & e, std::function const & fn) const; + void find(expr const & e, std::function const & fn) const; // NOLINT void collect(expr const & e, buffer & r) const; void trace() const; diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 250cdd3523..3bea1985b9 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -807,7 +807,7 @@ void state::remove_from_indices(hypothesis const & h, hypothesis_idx hidx) { m_branch.m_hyp_index.erase(get_key_for(h.get_type()), h.get_self()); } -void state::find_hypotheses(expr const & e, std::function const & fn) const { +void state::find_hypotheses(expr const & e, std::function const & fn) const { // NOLINT m_branch.m_hyp_index.find(get_key_for(e), [&](expr const & h) { return fn(href_index(h)); }); } diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 8366329a29..a40a8b1984 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -321,7 +321,7 @@ public: optional contains_hypothesis(expr const & type) const; /** \brief Find hypotheses whose type may unify with \c e or its negation */ - void find_hypotheses(expr const & e, std::function const & fn) const; + void find_hypotheses(expr const & e, std::function const & fn) const; // NOLINT /************************ Abstracting hypotheses