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

feat(kernel/expr): use the expression depth in the hash code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-23 14:16:51 -07:00
parent a3b0200d32
commit 2344fb9476
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/expr.cpp
View file

@ -131,7 +131,9 @@ expr_app::expr_app(expr const & fn, expr const & arg):
fn.has_param_univ() || arg.has_param_univ(), fn.has_param_univ() || arg.has_param_univ(),
std::max(get_depth(fn), get_depth(arg)) + 1, std::max(get_depth(fn), get_depth(arg)) + 1,
std::max(get_free_var_range(fn), get_free_var_range(arg))), std::max(get_free_var_range(fn), get_free_var_range(arg))),
m_fn(fn), m_arg(arg) {} m_fn(fn), m_arg(arg) {
m_hash = ::lean::hash(m_hash, m_depth);
}
void expr_app::dealloc(buffer<expr_cell*> & todelete) { void expr_app::dealloc(buffer<expr_cell*> & todelete) {
dec_ref(m_fn, todelete); dec_ref(m_fn, todelete);
dec_ref(m_arg, todelete); dec_ref(m_arg, todelete);

1
src/kernel/expr.h
View file

@ -214,6 +214,7 @@ public:
/** \brief Composite expressions */ /** \brief Composite expressions */
class expr_composite : public expr_cell { class expr_composite : public expr_cell {
protected:
unsigned m_depth; unsigned m_depth;
unsigned m_free_var_range; unsigned m_free_var_range;
friend unsigned get_depth(expr const & e); friend unsigned get_depth(expr const & e);