change registration mode for relevant_eh

src/sat/smt/array_axioms.cpp

@@ -539,6 +539,8 @@ namespace array {
             if (!d.m_prop_upward)
                 continue;
             euf::enode* n = var2enode(v);
+            if (!ctx.is_relevant(n))
+                continue;
             if (add_as_array_eqs(n))
                 change = true;
             bool has_default = false;
@@ -567,6 +569,8 @@ namespace array {
             return false;
         for (unsigned i = 0; i < ctx.get_egraph().enodes_of(f).size(); ++i) {
             euf::enode* p = ctx.get_egraph().enodes_of(f)[i];
+            if (!ctx.is_relevant(p))
+                continue;
             expr_ref_vector select(m);
             select.push_back(n->get_expr());
             for (expr* arg : *to_app(p->get_expr()))
@@ -615,7 +619,9 @@ namespace array {
             euf::enode * n = var2enode(i);
             
             if (!is_array(n)) 
-                continue;            
+                continue;
+            if (!ctx.is_relevant(n))
+                continue;
             euf::enode * r = n->get_root();
             if (r->is_marked1()) 
                 continue;            

src/sat/smt/array_internalize.cpp

@@ -124,40 +124,49 @@ namespace array {
             mk_var(n);
         for (auto* arg : euf::enode_args(n))
             ensure_var(arg);  
-        switch (a->get_decl_kind()) {
+        if (ctx.is_relevant(n))
-        case OP_STORE:           
+            relevant_eh(n);
-            internalize_store(n); 
+        return true;
+    }
+
+    void solver::relevant_eh(euf::enode* n) {
+        if (!is_app(n->get_expr()))
+            return;
+        if (n->get_decl()->get_family_id() != a.get_family_id())
+            return;
+        switch (n->get_decl()->get_decl_kind()) {
+        case OP_STORE:
+            internalize_store(n);
             break;
-        case OP_SELECT:          
+        case OP_SELECT:
-            internalize_select(n); 
+            internalize_select(n);
             break;
         case OP_AS_ARRAY:
-        case OP_CONST_ARRAY:     
+        case OP_CONST_ARRAY:
-            internalize_lambda(n); 
+            internalize_lambda(n);
             break;
-        case OP_ARRAY_EXT:       
+        case OP_ARRAY_EXT:
-            internalize_ext(n); 
+            internalize_ext(n);
             break;
-        case OP_ARRAY_DEFAULT:   
+        case OP_ARRAY_DEFAULT:
-            internalize_default(n); 
+            internalize_default(n);
             break;
-        case OP_ARRAY_MAP:       
+        case OP_ARRAY_MAP:
-            internalize_map(n); 
+            internalize_map(n);
             break;
-        case OP_SET_UNION:       
+        case OP_SET_UNION:
-        case OP_SET_INTERSECT:   
+        case OP_SET_INTERSECT:
-        case OP_SET_DIFFERENCE:  
+        case OP_SET_DIFFERENCE:
-        case OP_SET_COMPLEMENT:  
+        case OP_SET_COMPLEMENT:
-        case OP_SET_SUBSET:      
+        case OP_SET_SUBSET:
-        case OP_SET_HAS_SIZE:    
+        case OP_SET_HAS_SIZE:
-        case OP_SET_CARD:        
+        case OP_SET_CARD:
-            ctx.unhandled_function(a->get_decl()); 
+            ctx.unhandled_function(n->get_decl());
             break;
         default:
             UNREACHABLE();
-            break;            
+            break;
         }
-        return true;
     }
 
     /**

src/sat/smt/array_solver.h

@@ -264,6 +264,7 @@ namespace array {
         void apply_sort_cnstr(euf::enode* n, sort* s) override;
         bool is_shared(theory_var v) const override;
         bool enable_self_propagate() const override { return true; }
+        void relevant_eh(euf::enode* n) override;
 
         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}

src/sat/smt/euf_solver.cpp

@@ -739,6 +739,16 @@ namespace euf {
         }
     }
 
+    void solver::relevant_eh(euf::enode* n) {
+        if (m_qsolver)
+            m_qsolver->relevant_eh(n);
+        for (auto thv : enode_th_vars(n)) {
+            auto* th = m_id2solver.get(thv.get_id(), nullptr);
+            if (th && th != m_qsolver)
+                th->relevant_eh(n);
+        }       
+    }
+
     void solver::pre_simplify() {
         for (auto* e : m_solvers)
             e->pre_simplify();

src/sat/smt/euf_solver.h

@@ -398,6 +398,7 @@ namespace euf {
         void add_auto_relevant(sat::literal lit);
         void pop_relevant(unsigned n);
         void push_relevant();
+        void relevant_eh(euf::enode* n);
         smt::relevancy& relevancy() { return m_relevancy; }
 
         // model construction

src/sat/smt/q_ematch.cpp

@@ -70,15 +70,14 @@ namespace q {
 
         };
         ctx.get_egraph().set_on_merge(_on_merge);
-        if (ctx.relevancy().enabled())
+        if (!ctx.relevancy().enabled())
             ctx.get_egraph().set_on_make(_on_make);
-        else
-            ctx.relevancy().add_relevant(&s);
         m_mam = mam::mk(ctx, *this);
     }
 
     void ematch::relevant_eh(euf::enode* n) {
-        m_mam->add_node(n, false);
+        if (ctx.relevancy().enabled())
+            m_mam->add_node(n, false);
     }
 
     void ematch::ensure_ground_enodes(expr* e) {

src/sat/smt/smt_relevant.cpp

@@ -26,8 +26,7 @@ namespace smt {
 
     void relevancy::relevant_eh(euf::enode* n) {
         SASSERT(is_relevant(n));
-        for (auto* th : m_relevant_eh)
+        ctx.relevant_eh(n);
-            th->relevant_eh(n);
     }
 
     void relevancy::relevant_eh(sat::literal lit) {

src/sat/smt/smt_relevant.h

@@ -120,7 +120,6 @@ namespace smt {
         vector<unsigned_vector>              m_occurs;            // where do literals occur
         unsigned                             m_qhead = 0;         // queue head for relevancy
         svector<std::pair<sat::literal, euf::enode*>> m_queue;    // propagation queue for relevancy
-        ptr_vector<euf::th_solver>          m_relevant_eh;
 
         // callbacks during propagation
         void relevant_eh(euf::enode* n);
@@ -160,7 +159,5 @@ namespace smt {
         
         bool enabled() const { return m_enabled; }
         void set_enabled(bool e) { m_enabled = e; }
-
-        void add_relevant(euf::th_solver* th) { m_relevant_eh.push_back(th); }
     };
 }