fix(kernel): incorrect optimization in max_sharing_fn class

The resultant expression may failed to be fully shared.
Add an example that demonstrates the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/expr.cpp

@@ -59,8 +59,8 @@ void expr_cell::dec_ref(expr & e, buffer<expr_cell*> & todelete) {
 }
 
 optional<bool> expr_cell::is_arrow() const {
-    // it is stored in bits 1-2
-    unsigned r = (m_flags & (2+4)) >> 1;
+    // it is stored in bits 0-1
+    unsigned r = (m_flags & (1+2));
     if (r == 0) {
         return optional<bool>();
     } else if (r == 1) {
@@ -72,7 +72,7 @@ optional<bool> expr_cell::is_arrow() const {
 }
 
 void expr_cell::set_is_arrow(bool flag) {
-    unsigned mask = flag ? 2 : 4;
+    unsigned mask = flag ? 1 : 2;
     m_flags |= mask;
     lean_assert(is_arrow() && *is_arrow() == flag);
 }

src/kernel/expr.h

@@ -44,8 +44,7 @@ class expr_cell {
 protected:
     unsigned short     m_kind;
     // The bits of the following field mean:
-    //    0    - term is maximally shared
-    //    1-2  - term is an arrow (0 - not initialized, 1 - is arrow, 2 - is not arrow)
+    //    0-1  - term is an arrow (0 - not initialized, 1 - is arrow, 2 - is not arrow)
     // Remark: we use atomic_uchar because these flags are computed lazily (i.e., after the expression is created)
     atomic_uchar       m_flags;
     unsigned           m_has_mv:1;         // term contains metavariables
@@ -56,10 +55,6 @@ protected:
     MK_LEAN_RC(); // Declare m_rc counter
     void dealloc();
 
-    bool max_shared() const { return (m_flags & 1) != 0; }
-    void set_max_shared() { m_flags |= 1; }
-    friend class max_sharing_fn;
-
     optional<bool> is_arrow() const;
     void set_is_arrow(bool flag);
     friend bool is_arrow(expr const & e);

src/kernel/max_sharing.cpp

@@ -21,22 +21,11 @@ struct max_sharing_fn::imp {
 
     expr_cache m_cache;
 
-    void cache(expr const & a) {
-        a.raw()->set_max_shared();
-        m_cache.insert(a);
-    }
-
     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());
+        if (r != m_cache.end())
             return *r;
-        }
-        if (a.raw()->max_shared()) {
-            m_cache.insert(a);
-            return a;
-        }
         expr res;
         switch (a.kind()) {
         case expr_kind::Constant: case expr_kind::Var:
@@ -56,7 +45,7 @@ struct max_sharing_fn::imp {
             res = update_mlocal(a, apply(mlocal_type(a)));
             break;
         }
-        cache(res);
+        m_cache.insert(a);
         return res;
     }
     expr operator()(expr const & a) { return apply(a); }
@@ -68,9 +57,6 @@ expr max_sharing_fn::operator()(expr const & a) { return (*m_ptr)(a); }
 void max_sharing_fn::clear() { m_ptr->m_cache.clear(); }
 
 expr max_sharing(expr const & a) {
-    if (a.raw()->max_shared())
-        return a;
-    else
-        return max_sharing_fn::imp()(a);
+    return max_sharing_fn::imp()(a);
 }
 }

src/tests/kernel/expr.cpp

@@ -146,12 +146,13 @@ static void tst5() {
 static void tst6() {
     expr f = Const("f");
     expr r = mk_redundant_dag(f, 12);
+    max_sharing_fn s;
     for (unsigned i = 0; i < 1000; i++) {
-        r = max_sharing(r);
+        r = s(r);
     }
     r = mk_big(f, 16, 0);
     for (unsigned i = 0; i < 1000000; i++) {
-        r = max_sharing(r);
+        r = s(r);
     }
 }
 

src/tests/library/max_sharing.cpp

@@ -32,8 +32,22 @@ static void tst1() {
     lean_assert(is_eqp(app_arg(app_fn(F2)), app_arg(F2)));
 }
 
+static void tst2() {
+    max_sharing_fn max_fn1;
+    max_sharing_fn max_fn2;
+    expr x   = Const("x");
+    expr f   = Const("f");
+    expr g   = Const("g");
+    expr t1  = max_fn2(max_fn1(f(g(x))));
+    expr t2  = max_fn2(f(t1, g(x)));
+    expr arg1 = app_arg(app_arg(app_fn(t2)));
+    expr arg2 = app_arg(t2);
+    lean_assert(is_eqp(arg1, arg2));
+}
+
 int main() {
     save_stack_info();
     tst1();
+    tst2();
     return has_violations() ? 1 : 0;
 }