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

fix(library/simplifier): ordered rewriting

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-20 13:13:16 -08:00
parent 5060bdbf14
commit 56f5657ee7
1 changed files with 4 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/library/simplifier/simplifier.cpp
View file

@ -478,14 +478,6 @@ class simplifier_fn {
return true; return true;
} }
bool sorted_args(unsigned num, expr const * args) {
for (unsigned i = 1; i < num; i++) {
if (!is_lt(args[i-1], args[i], false))
return false;
}
return true;
}
/** /**
\brief Auxiliary function used by m_match_fn, it tries to match the given rule and \brief Auxiliary function used by m_match_fn, it tries to match the given rule and
the expression in the temporary field \c m_target. the expression in the temporary field \c m_target.
@ -500,10 +492,10 @@ class simplifier_fn {
m_new_args.clear(); m_new_args.clear();
m_new_args.resize(num+1); m_new_args.resize(num+1);
if (found_all_args(num)) { if (found_all_args(num)) {
if (rule.is_permutation() && sorted_args(num, m_new_args.begin()+1))
return false;
// easy case: all arguments found // easy case: all arguments found
m_new_rhs = instantiate(rule.get_rhs(), num, m_new_args.data() + 1); m_new_rhs = instantiate(rule.get_rhs(), num, m_new_args.data() + 1);
if (rule.is_permutation() && !is_lt(m_new_rhs, m_target, false))
return false;
if (m_proofs_enabled) { if (m_proofs_enabled) {
if (num > 0) { if (num > 0) {
m_new_args[0] = rule.get_proof(); m_new_args[0] = rule.get_proof();
@ -561,9 +553,9 @@ class simplifier_fn {
result simplify_constant(expr const & e) { result simplify_constant(expr const & e) {
lean_assert(is_constant(e)); lean_assert(is_constant(e));
if (m_unfold || m_eval) { if (m_unfold) {
auto obj = m_env->find_object(const_name(e)); auto obj = m_env->find_object(const_name(e));
if (m_unfold && should_unfold(obj)) { if (should_unfold(obj)) {
expr e = obj->get_value(); expr e = obj->get_value();
if (m_single_pass) { if (m_single_pass) {
return result(e); return result(e);
@ -571,9 +563,6 @@ class simplifier_fn {
return simplify(e); return simplify(e);
} }
} }
if (m_eval && obj->is_builtin()) {
return result(obj->get_value());
}
} }
return rewrite(e, result(e)); return rewrite(e, result(e));
} }