From e3dc552c39bc73af9f0f17bd89a46974f323af2f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 31 Jan 2014 15:55:12 -0800 Subject: [PATCH] fix(library/simplifier): nontermination The example tests/lua/simp1.lua demonstrates the issue. The higher-order matcher matches closed terms that are definitionally equal. So, given a definition definition a := 1 it will match 'a' with '1' since they are definitionally equal. Then, if we have a theorem theorem a_eq_1 : a = 1 as a rewrite rule, it was triggering the following infinite loop when simplifying the expression "a" a --> 1 --> 1 --> 1 ... The first simplification is expected. The other ones are not. The problem is that "1" is definitionally equal to "a", and they match. The rewrite_rule_set manager accepts the rule a --> 1 since the left-hand-side does not occur in the right-hand-side. To avoid this loop, we test if the new expression is not equal to the previous one. Signed-off-by: Leonardo de Moura --- src/library/simplifier/simplifier.cpp | 17 +++++++++++++---- src/library/simplifier/simplifier.h | 2 +- tests/lean/simp3.lean.expected.out | 2 +- tests/lua/simp1.lua | 1 + 4 files changed, 16 insertions(+), 6 deletions(-) diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 25317e82f..119400cb7 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -911,6 +911,12 @@ class simplifier_cell::imp { i = i + 1; } } + if (new_rhs == target) { + if (m_monitor) + m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(), + 0, simplifier_monitor::failure_kind::LoopPrevention); + return false; + } if (m_proofs_enabled) { if (num > 0) { new_args[0] = rule.get_proof(); @@ -990,10 +996,10 @@ class simplifier_cell::imp { } new_proof = mk_app(proof_args); new_rhs = arg(ceq, num_args(ceq) - 1); - if (rule.is_permutation() && !is_lt(new_rhs, target, false)) { + if (new_rhs == target || (rule.is_permutation() && !is_lt(new_rhs, target, false))) { if (m_monitor) m_monitor->failed_rewrite_eh(ro_simplifier(m_this), target, rule.get_ceq(), rule.get_id(), - 0, simplifier_monitor::failure_kind::PermutationGe); + 0, simplifier_monitor::failure_kind::LoopPrevention); return false; } if (m_monitor) @@ -1800,7 +1806,10 @@ static int simplify_core(lua_State * L, ro_shared_environment const & env) { options opts; if (nargs >= 3) opts = to_options(L, 3); - auto r = simplify(e, env, opts, rules.size(), rules.data()); + optional menv; + if (nargs >= 5) + menv = some_ro_menv(to_metavar_env(L, 5)); + auto r = simplify(e, env, opts, rules.size(), rules.data(), menv, get_simplifier_monitor(L, 6)); push_expr(L, r.get_expr()); push_optional_expr(L, r.get_proof()); lua_pushboolean(L, r.is_heq_proof()); @@ -1885,7 +1894,7 @@ void open_simplifier(lua_State * L) { SET_ENUM("TypeMismatch", simplifier_monitor::failure_kind::TypeMismatch); SET_ENUM("AssumptionNotProved", simplifier_monitor::failure_kind::AssumptionNotProved); SET_ENUM("MissingArgument", simplifier_monitor::failure_kind::MissingArgument); - SET_ENUM("PermutationGe", simplifier_monitor::failure_kind::PermutationGe); + SET_ENUM("LoopPrevention", simplifier_monitor::failure_kind::LoopPrevention); SET_ENUM("AbstractionBody", simplifier_monitor::failure_kind::AbstractionBody); lua_setglobal(L, "simplifier_failure"); diff --git a/src/library/simplifier/simplifier.h b/src/library/simplifier/simplifier.h index a6f83c31e..96455d6d0 100644 --- a/src/library/simplifier/simplifier.h +++ b/src/library/simplifier/simplifier.h @@ -102,7 +102,7 @@ public: */ virtual void rewrite_eh(ro_simplifier const & s, expr const & e, expr const & new_e, expr const & ceq, name const & ceq_id) = 0; - enum class failure_kind { Unsupported, TypeMismatch, AssumptionNotProved, MissingArgument, PermutationGe, AbstractionBody }; + enum class failure_kind { Unsupported, TypeMismatch, AssumptionNotProved, MissingArgument, LoopPrevention, AbstractionBody }; /** \brief This method is invoked when the simplifier fails to rewrite an application \c e. diff --git a/tests/lean/simp3.lean.expected.out b/tests/lean/simp3.lean.expected.out index e6e2c7f99..3158f973d 100644 --- a/tests/lean/simp3.lean.expected.out +++ b/tests/lean/simp3.lean.expected.out @@ -31,5 +31,5 @@ trans (congr (congr2 (λ x : ℕ, eq ((λ x : ℕ, x + 10) x)) a * a + (a * b + (b * a + b * b)) ⊤ → ⊥ refl (⊤ → ⊥) false ⊤ → ⊤ refl (⊤ → ⊤) false -⊥ → ⊥ refl (⊥ → ⊥) false +⊥ → ⊤ imp_congr (refl ⊥) (λ C::1 : ⊥, eqt_intro C::1) false ⊥ refl ⊥ false diff --git a/tests/lua/simp1.lua b/tests/lua/simp1.lua index 16841d36a..fff92f267 100644 --- a/tests/lua/simp1.lua +++ b/tests/lua/simp1.lua @@ -17,6 +17,7 @@ parse_lean_cmds([[ add_rewrite_rules("a_eq_1") add_rewrite_rules("f_id") add_rewrite_rules("eq_id") + -- set_option({"lean", "pp", "implicit"}, true) e, pr = simplify(parse_lean('fun x, f (f x (0 + a)) (g (b + 0))')) print(e)