From bd8de964f737dc0e7c3b8fa739771fbf643bc926 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 4 Jan 2022 22:02:28 -0800
Subject: [PATCH] more fixes on relevancy

---
 src/sat/smt/euf_model.cpp     |  4 ++++
 src/sat/smt/euf_relevancy.cpp | 41 +++++++++++++++++++++++++++++------
 src/sat/smt/euf_relevancy.h   |  8 +++++--
 3 files changed, 44 insertions(+), 9 deletions(-)

diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 3d0369287..9540cd016 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -199,6 +199,8 @@ namespace euf {
             expr* e = n->get_expr();
             if (!is_app(e))
                 continue;
+            if (!is_relevant(n))
+                continue;
             app* a = to_app(e);
             func_decl* f = a->get_decl();       
             if (!include_func_interp(f))
@@ -297,6 +299,8 @@ namespace euf {
         ev.set_model_completion(true);
         TRACE("model",
             for (enode* n : m_egraph.nodes()) {
+                if (!is_relevant(n))
+                    continue;
                 unsigned id = n->get_root_id();
                 expr* val = m_values.get(id, nullptr);
                 if (!val)
diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index a24277293..66ed9054c 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -132,6 +132,35 @@ namespace euf {
         m_trail.push_back(std::make_pair(update::relevant_var, lit.var()));
     }
 
+    void relevancy::set_asserted(sat::literal lit) {
+        SASSERT(!is_relevant(lit));
+        SASSERT(ctx.s().value(lit) == l_true);
+        set_relevant(lit);
+        add_to_propagation_queue(lit);
+        ctx.asserted(lit);
+    }
+
+    /**
+    * Boolean variable is set relevant because an E-node is relevant.
+    * 
+    */
+    void relevancy::relevant_eh(sat::bool_var v) {
+        if (is_relevant(v))
+            return;
+        sat::literal lit(v);
+        switch (ctx.s().value(lit)) {
+        case l_undef:
+            set_relevant(lit);
+            break;
+        case l_true:
+            set_asserted(lit);
+            break;
+        case l_false:
+            set_asserted(~lit);
+            break;
+        }
+    }
+
     void relevancy::asserted(sat::literal lit) {
         TRACE("relevancy", tout << "asserted " << lit << " relevant " << is_relevant(lit) << "\n");
         if (!m_enabled)
@@ -239,11 +268,8 @@ namespace euf {
                 }
             }
 
-            if (true_lit != sat::null_literal) {
-                set_relevant(true_lit);
-                add_to_propagation_queue(true_lit);
-                ctx.asserted(true_lit);
-            }
+            if (true_lit != sat::null_literal) 
+                set_asserted(true_lit);            
             else {
                 m_trail.push_back(std::make_pair(update::set_root, idx));
                 m_roots[idx] = true;
@@ -276,8 +302,9 @@ namespace euf {
                 if (!n->is_relevant()) {
                     ctx.get_egraph().set_relevant(n);
                     ctx.relevant_eh(n);
-                    if (n->bool_var() != sat::null_bool_var) 
-                        mark_relevant(sat::literal(n->bool_var()));
+                    sat::bool_var v = n->bool_var();                    
+                    if (v != sat::null_bool_var)
+                        relevant_eh(v);
                     for (euf::enode* sib : euf::enode_class(n))
                         if (!sib->is_relevant())
                             m_todo.push_back(sib);
diff --git a/src/sat/smt/euf_relevancy.h b/src/sat/smt/euf_relevancy.h
index b64b1d7f8..382b054fc 100644
--- a/src/sat/smt/euf_relevancy.h
+++ b/src/sat/smt/euf_relevancy.h
@@ -139,10 +139,14 @@ namespace euf {
 
         void add_to_propagation_queue(sat::literal lit);        
 
-        void propagate_relevant(euf::enode* n);
-
         void set_relevant(sat::literal lit);
 
+        void set_asserted(sat::literal lit);
+
+        void relevant_eh(sat::bool_var v);
+
+        void propagate_relevant(euf::enode* n);
+
     public:
         relevancy(euf::solver& ctx): ctx(ctx) {}