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

feat(kernel/max_sharing): check for imminent stack overflows and interruptions in the expression sharing maximizer

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-21 14:33:32 -08:00
parent 2089b85532
commit 95b6e61738
2 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/max_sharing.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <unordered_set>
#include <functional>
#include "util/buffer.h"
#include "util/interrupt.h"
#include "kernel/max_sharing.h"
namespace lean {
@ -33,6 +34,7 @@ struct max_sharing_fn::imp {
}
expr apply(expr const & a) {
check_system("max_sharing");
auto r = m_cache.find(a);
if (r != m_cache.end()) {
lean_assert((*r).raw()->max_shared());

1
src/kernel/max_sharing.h
View file

@ -29,7 +29,6 @@ public:
void clear();
};
/**
\brief The resultant expression is structurally identical to the input one, but
it uses maximally shared sub-expressions.