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

Fix bug in max_sharing

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-23 09:18:18 -07:00
parent dd74284fdc
commit f00d8c4683
2 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/max_sharing.cpp
View file

@ -25,13 +25,15 @@ class max_sharing_functor {
public: public:
expr apply(expr const & a) { expr apply(expr const & a) {
if (a.raw()->max_shared())
return a;
auto r = m_cache.find(a); auto r = m_cache.find(a);
if (r != m_cache.end()) { if (r != m_cache.end()) {
lean_assert((*r).raw()->max_shared()); lean_assert((*r).raw()->max_shared());
return *r; return *r;
} }
if (a.raw()->max_shared()) {
m_cache.insert(a);
return a;
}
switch (a.kind()) { switch (a.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Var: case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
cache(a); cache(a);

11
src/tests/kernel/expr.cpp
View file

@ -187,6 +187,16 @@ void tst6() {
} }
} }
void tst7() {
expr f = constant(name("f"));
expr v = var(0);
expr a1 = max_sharing(app(f, v, v));
expr a2 = max_sharing(app(f, v, v));
lean_assert(!eqp(a1, a2));
expr b = max_sharing(app(f, a1, a2));
lean_assert(eqp(get_arg(b, 1), get_arg(b, 2)));
}
int main() { int main() {
continue_on_violation(true); continue_on_violation(true);
std::cout << "sizeof(expr): " << sizeof(expr) << "\n"; std::cout << "sizeof(expr): " << sizeof(expr) << "\n";
@ -197,6 +207,7 @@ int main() {
tst4(); tst4();
tst5(); tst5();
tst6(); tst6();
tst7();
std::cout << "done" << "\n"; std::cout << "done" << "\n";
return has_violations() ? 1 : 0; return has_violations() ? 1 : 0;
} }