feat(kernel/default_converter): cache failures for (f t =?= f s) heuristic

See item 4 at
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/oJXwW5wT2Ds/d1Dgr8B-pE0J

See also
https://github.com/leanprover/lean/pull/659
This commit is contained in:
Leonardo de Moura 2015-06-08 10:41:30 -07:00
parent e59400b58c
commit 496189feed
7 changed files with 92 additions and 23 deletions

View file

@ -432,6 +432,25 @@ bool default_converter::is_def_eq_proof_irrel(expr const & t, expr const & s, co
return false;
}
bool default_converter::failed_before(expr const & t, expr const & s) const {
if (t.hash() < s.hash()) {
return m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end();
} else if (t.hash() > s.hash()) {
return m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
} else {
return
m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end() ||
m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
}
}
void default_converter::cache_failure(expr const & t, expr const & s) {
if (t.hash() <= s.hash())
m_failure_cache.insert(mk_pair(t, s));
else
m_failure_cache.insert(mk_pair(s, t));
}
pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, expr const & s) {
check_system("is_definitionally_equal");
constraint_seq cs;
@ -480,11 +499,14 @@ pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, exp
// skip the delta-reduction step.
// If the flag use_conv_opt() is not true, then we skip this optimization
constraint_seq tmp_cs;
if (!is_opaque(*d_t) && d_t->use_conv_opt() &&
is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n)), tmp_cs) &&
if (!is_opaque(*d_t) && d_t->use_conv_opt() && !failed_before(t_n, s_n)) {
if (is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n)), tmp_cs) &&
is_def_eq_args(t_n, s_n, tmp_cs)) {
cs += tmp_cs;
return to_bcs(true, cs);
} else {
cache_failure(t_n, s_n);
}
}
}
}

View file

@ -5,22 +5,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <unordered_set>
#include "util/lbool.h"
#include "kernel/justification.h"
#include "kernel/environment.h"
#include "kernel/converter.h"
#include "kernel/expr_maps.h"
#include "kernel/equiv_manager.h"
#include "kernel/expr_pair.h"
namespace lean {
/** \breif Converter used in the kernel */
class default_converter : public converter {
protected:
typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> expr_pair_set;
environment m_env;
bool m_memoize;
expr_struct_map<expr> m_whnf_core_cache;
expr_struct_map<pair<expr, constraint_seq>> m_whnf_cache;
equiv_manager m_eqv_manager;
expr_pair_set m_failure_cache;
// The two auxiliary fields are set when the public methods whnf and is_def_eq are invoked.
// The goal is to avoid to keep carrying them around.
@ -66,6 +70,9 @@ protected:
bool is_def_eq_app(expr const & t, expr const & s, constraint_seq & cs);
bool is_def_eq_proof_irrel(expr const & t, expr const & s, constraint_seq & cs);
bool failed_before(expr const & t, expr const & s) const;
void cache_failure(expr const & t, expr const & s);
pair<bool, constraint_seq> is_prop(expr const & e);
pair<expr, constraint_seq> whnf(expr const & e_prime);
pair<bool, constraint_seq> is_def_eq_core(expr const & t, expr const & s);

27
src/kernel/expr_pair.h Normal file
View file

@ -0,0 +1,27 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
namespace lean {
typedef pair<expr, expr> expr_pair;
/** \brief Functional object for hashing expression pairs. */
struct expr_pair_hash {
unsigned operator()(expr_pair const & p) const { return hash(p.first.hash(), p.second.hash()); }
};
/** \brief Functional object for hashing expression pairs (based on their allocation time). */
struct expr_pair_hash_alloc {
unsigned operator()(expr_pair const & p) const { return hash(p.first.hash_alloc(), p.second.hash_alloc()); }
};
/** \brief Functional object for comparing expression pairs. */
struct expr_pair_eq {
bool operator()(expr_pair const & p1, expr_pair const & p2) const { return p1.first == p2.first && p1.second == p2.second; }
};
/** \brief Functional object for comparing expression pairs using pointer equality. */
struct expr_pair_eqp {
bool operator()(expr_pair const & p1, expr_pair const & p2) const { return is_eqp(p1.first, p2.first) && is_eqp(p1.second, p2.second); }
};
}

View file

@ -7,27 +7,10 @@ Author: Leonardo de Moura
#pragma once
#include <utility>
#include "util/hash.h"
#include "kernel/expr.h"
#include "kernel/expr_pair.h"
#include "library/expr_lt.h"
namespace lean {
typedef pair<expr, expr> expr_pair;
/** \brief Functional object for hashing expression pairs. */
struct expr_pair_hash {
unsigned operator()(expr_pair const & p) const { return hash(p.first.hash(), p.second.hash()); }
};
/** \brief Functional object for hashing expression pairs (based on their allocation time). */
struct expr_pair_hash_alloc {
unsigned operator()(expr_pair const & p) const { return hash(p.first.hash_alloc(), p.second.hash_alloc()); }
};
/** \brief Functional object for comparing expression pairs. */
struct expr_pair_eq {
bool operator()(expr_pair const & p1, expr_pair const & p2) const { return p1.first == p2.first && p1.second == p2.second; }
};
/** \brief Functional object for comparing expression pairs using pointer equality. */
struct expr_pair_eqp {
bool operator()(expr_pair const & p1, expr_pair const & p2) const { return is_eqp(p1.first, p2.first) && is_eqp(p1.second, p2.second); }
};
inline bool is_lt(expr_pair const & p1, expr_pair const & p2, bool use_hash) {
return is_lt(p1.first, p2.first, use_hash) || (p1.first == p2.first && is_lt(p1.second, p2.second, use_hash));
}

View file

@ -49,6 +49,9 @@ add_test(NAME "issue_597"
add_test(NAME "issue_616"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
COMMAND bash "./issue_616.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
add_test(NAME "normalizer_perf"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
COMMAND bash "./timeout.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "1" "slow1.lean")
# LEAN TESTS
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")

View file

@ -0,0 +1,11 @@
open nat
definition f (a : nat) : nat := a
definition g (a : nat) : nat := zero
example (a b : nat) :
@eq nat
(g (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f a))))))))))))))))))))))
(g (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f b))))))))))))))))))))))
:=
@eq.refl nat (g (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f a))))))))))))))))))))))

16
tests/lean/extra/timeout.sh Executable file
View file

@ -0,0 +1,16 @@
#!/bin/sh
# Execute lean with timeout
set -e
if [ $# -ne 3 ]; then
echo "Usage: timeout.sh [lean-executable-path] [timeout] [benchmark]"
exit 1
fi
LEAN=$1
TIMEOUT=$2
BENCH=$3
export LEAN_PATH=../../../library:.
ulimit -t $2
if ! $LEAN $BENCH; then
echo "Failed to execute $BENCH in $TIMEOUT second(s)"
exit 1
fi