cache is_shared information in the enode

observed perf overhead for QF_NIA is that assume_eqs in theory_lra incurs significant overhead when calling is_relevant_and_shared. The call to context::is_shared and the loop checking for beta redexes is a main bottleneck. The bottleneck is avoided by caching the result if is_shared inside the enode. It is invalidated for every merge/unmerge.

src/ast/euf/euf_egraph.cpp

@@ -476,6 +476,7 @@ namespace euf {
             c->m_root = r2;
         std::swap(r1->m_next, r2->m_next);
         r2->inc_class_size(r1->class_size());   
+        r2->set_is_shared(l_undef);
         merge_th_eq(r1, r2);
         reinsert_parents(r1, r2);
         if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr())))
@@ -553,6 +554,7 @@ namespace euf {
         enode* r2 = r1->get_root();
         TRACE("euf", tout << "undo-eq old-root: " << bpp(r1) << " current-root " << bpp(r2) << " node: " << bpp(n1) << "\n";);
         r2->dec_class_size(r1->class_size());
+        r2->set_is_shared(l_undef);
         std::swap(r1->m_next, r2->m_next);
         auto begin = r2->begin_parents() + r2_num_parents, end = r2->end_parents();
         for (auto it = begin; it != end; ++it) {

src/ast/euf/euf_enode.h

@@ -52,6 +52,7 @@ namespace euf {
         bool          m_merge_tf_enabled = false;
         bool          m_is_equality = false;    // Does the expression represent an equality
         bool          m_is_relevant = false;
+        lbool         m_is_shared = l_undef;
         lbool         m_value = l_undef;        // Assignment by SAT solver for Boolean node
         sat::bool_var m_bool_var = sat::null_bool_var;    // SAT solver variable associated with Boolean node
         unsigned      m_class_size = 1;         // Size of the equivalence class if the enode is the root.
@@ -181,6 +182,9 @@ namespace euf {
         void unmark3() { m_mark3 = false; }
         bool is_marked3() { return m_mark3; }
 
+        lbool is_shared() const { return m_is_shared; }
+        void set_is_shared(lbool s) { m_is_shared = s; }
+
         template<bool m> void mark1_targets() {
             enode* n = this;
             while (n) {

src/sat/smt/euf_internalize.cpp

@@ -355,8 +355,16 @@ namespace euf {
     bool solver::is_shared(enode* n) const {
         n = n->get_root();
 
-        if (m.is_ite(n->get_expr()))
+        switch (n->is_shared()) {
+        case l_true: return true;
+        case l_false: return false;
+        default: break;
+        }
+
+        if (m.is_ite(n->get_expr())) {
+            n->set_is_shared(l_true);
             return true;
+        }
 
         // the variable is shared if the equivalence class of n
         // contains a parent application.
@@ -366,21 +374,27 @@ namespace euf {
             family_id id = p.get_id();
             if (m.get_basic_family_id() != id) {
                 
-                if (th_id != m.get_basic_family_id())
+                if (th_id != m.get_basic_family_id()) {
+                    n->set_is_shared(l_true);
                     return true;
+                }
                 th_id = id;               
             }
         }
-        if (m.is_bool(n->get_expr()) && th_id != m.get_basic_family_id())
+        if (m.is_bool(n->get_expr()) && th_id != m.get_basic_family_id()) {
+            n->set_is_shared(l_true);
             return true;
+        }
         
         for (enode* parent : euf::enode_parents(n)) {
             app* p = to_app(parent->get_expr());
             family_id fid = p->get_family_id();
             if (is_beta_redex(parent, n))
                 continue;
-            if (fid != th_id && fid != m.get_basic_family_id())
+            if (fid != th_id && fid != m.get_basic_family_id()) {
+                n->set_is_shared(l_true);
                 return true;
+            }
         }
 
         // Some theories implement families of theories. Examples:
@@ -411,9 +425,12 @@ namespace euf {
         // not marked as shared.
 
         for (auto const& p : euf::enode_th_vars(n)) 
-            if (fid2solver(p.get_id())->is_shared(p.get_var()))
+            if (fid2solver(p.get_id())->is_shared(p.get_var())) {
+                n->set_is_shared(l_true);
                 return true;
+            }
 
+        n->set_is_shared(l_false);
         return false;
     }
 

src/smt/smt_context.cpp

@@ -560,6 +560,7 @@ namespace smt {
 
             // Update "equivalence" class size
             r2->m_class_size += r1->m_class_size;
+            r2->m_is_shared = 2;
 
             CASSERT("add_eq", check_invariant());
         }
@@ -920,6 +921,7 @@ namespace smt {
 
         // restore r2 class size
         r2->m_class_size -= r1->m_class_size;
+        r2->m_is_shared = 2;
 
         // unmerge "equivalence" classes
         std::swap(r1->m_next, r2->m_next);
@@ -4504,8 +4506,15 @@ namespace smt {
 
     bool context::is_shared(enode * n) const {
         n = n->get_root();
+        switch (n->is_shared()) {
+        case l_true: return true;
+        case l_false: return false;
+        default: break;
+        }
+
         unsigned num_th_vars = n->get_num_th_vars();
         if (m.is_ite(n->get_expr())) {
+            n->set_is_shared(l_true);
             return true;
         }
         switch (num_th_vars) {
@@ -4531,6 +4540,7 @@ namespace smt {
                     TRACE("is_shared", tout << enode_pp(n, *this) 
                           << "\nis shared because of:\n" 
                           << enode_pp(parent, *this) << "\n";);
+                    n->set_is_shared(l_true);
                     return true;
                 }
             }
@@ -4561,7 +4571,9 @@ namespace smt {
             // the theories of (array int int) and (array (array int int) int).
             // Remark: The inconsistency is not going to be detected if they are
             // not marked as shared.
-            return get_theory(th_id)->is_shared(l->get_var());
+            bool r = get_theory(th_id)->is_shared(l->get_var());
+            n->set_is_shared(to_lbool(r));
+            return r;
         }
         default:
             return true;

src/smt/smt_enode.cpp

@@ -49,6 +49,7 @@ namespace smt {
         n->m_iscope_lvl       = iscope_lvl;
         n->m_lbl_hash         = -1;
         n->m_proof_is_logged = false;
+        n->m_is_shared        = 2;
         unsigned num_args     = n->get_num_args();
         for (unsigned i = 0; i < num_args; i++) {            
             enode * arg  = app2enode[owner->get_arg(i)->get_id()];

src/smt/smt_enode.h

@@ -77,6 +77,7 @@ namespace smt {
         unsigned            m_bool:1;           //!< True if it is a boolean enode
         unsigned            m_merge_tf:1;       //!< True if the enode should be merged with true/false when the associated boolean variable is assigned.
         unsigned            m_cgc_enabled:1;    //!< True if congruence closure is enabled for this enode.
+        unsigned            m_is_shared:2;      //!< 0 - not shared, 1 - shared, 2 - invalid state
         unsigned            m_iscope_lvl;       //!< When the enode was internalized
         bool                m_proof_is_logged;  //!< Indicates that the proof for the enode being equal to its root is in the log.
         signed char         m_lbl_hash;         //!< It is different from -1, if enode is used in a pattern
@@ -179,6 +180,21 @@ namespace smt {
             return m_owner->hash();
         }
 
+        lbool is_shared() const { 
+            switch (m_is_shared) {
+            case 0: return l_false;
+            case 1: return l_true;
+            default: return l_undef;
+            }
+        }
+
+        void set_is_shared(lbool s) {
+            switch (s) {
+            case l_true: m_is_shared = 1; break;
+            case l_false: m_is_shared = 0; break;
+            default: m_is_shared = 2; break;
+            }
+        }
 
         enode * get_root() const { 
             return m_root;