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

feat(library/simplifier): enforce max_steps option

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-21 12:12:17 -08:00
parent 1ccfac5873
commit ead54bbf57
3 changed files with 40 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -139,6 +139,8 @@ class simplifier_fn {
cache m_cache;
max_sharing_fn m_max_sharing;
unsigned m_num_steps; // number of steps performed
// Configuration
bool m_proofs_enabled;
bool m_contextual;
@ -556,7 +558,7 @@ class simplifier_fn {
return false;
}
} else {
// failed the argument is not a proposition
// failed, the argument is not a proposition
return false;
}
}
@ -737,6 +739,9 @@ class simplifier_fn {
result simplify(expr e) {
check_system("simplifier");
m_num_steps++;
if (m_num_steps > m_max_steps)
throw exception("simplifier failed, maximum number of steps exceeded");
if (m_memoize) {
e = m_max_sharing(e);
auto it = m_cache.find(e);
@ -780,6 +785,7 @@ public:
expr_pair operator()(expr const & e, context const & ctx) {
set_context set(*this, ctx);
m_num_steps = 0;
auto r = simplify(e);
if (r.m_proof) {
return mk_pair(r.m_out, *(r.m_proof));

19
tests/lean/simp11.lean Normal file
View file

@ -0,0 +1,19 @@
variables a b c d e f : Nat
rewrite_set simple
add_rewrite Nat::add_assoc Nat::add_comm Nat::add_left_comm Nat::distributer Nat::distributel : simple
(*
local opts = options({"simplifier", "max_steps"}, 100)
local t = parse_lean("f + (c + f + d) + (e * (a + c) + (d + a))")
local t2, pr = simplify(t, "simple", get_environment(), context(), opts)
*)
print "trying again with more steps"
(*
local opts = options({"simplifier", "max_steps"}, 100000)
local t = parse_lean("f + (c + f + d) + (e * (a + c) + (d + a))")
local t2, pr = simplify(t, "simple", get_environment(), context(), opts)
print(t)
print("====>")
print(t2)
*)

14
tests/lean/simp11.lean.expected.out Normal file
View file

@ -0,0 +1,14 @@
Set: pp::colors
Set: pp::unicode
Assumed: a
Assumed: b
Assumed: c
Assumed: d
Assumed: e
Assumed: f
simp11.lean:7: error: executing script
error: simplifier failed, maximum number of steps exceeded
trying again with more steps
f + (c + f + d) + (e * (a + c) + (d + a))
====>
a + (c + (d + (d + (f + (f + (e * a + e * c))))))