From 308f39922434c74c192b759d44fa9a1c1b4b91ae Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Apr 2021 16:19:54 -0700
Subject: [PATCH] #5215 converting NYI

---
 src/ast/euf/euf_egraph.cpp | 18 +++++++++++++++++-
 src/ast/euf/euf_egraph.h   |  9 +++++++--
 src/sat/smt/q_solver.cpp   |  1 -
 3 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 4edef1015..fab134fdd 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -291,7 +291,20 @@ namespace euf {
     }
 
     void egraph::set_lbl_hash(enode* n) {
-        NOT_IMPLEMENTED_YET();
+        SASSERT(n->m_lbl_hash == -1);
+        // m_lbl_hash should be different from -1, if and only if,
+        // there is a pattern that contains the enode. So,
+        // I use a trail to restore the value of m_lbl_hash to -1.
+        m_updates.push_back(update_record(n, update_record::lbl_hash()));
+        unsigned h = hash_u(n->get_expr_id());
+        n->m_lbl_hash = h & (APPROX_SET_CAPACITY - 1);
+        // propagate modification to the root m_lbls set.
+        enode* r = n->get_root();
+        approx_set & r_lbls = r->m_lbls;
+        if (!r_lbls.may_contain(n->m_lbl_hash)) {
+            m_updates.push_back(update_record(r, update_record::lbl_hash()));
+            r_lbls.insert(n->m_lbl_hash);
+        }
     }
 
     void egraph::pop(unsigned num_scopes) {
@@ -357,6 +370,9 @@ namespace euf {
                 VERIFY(p.r1->value() != l_undef);
                 p.r1->set_value(l_undef);
                 break;
+            case update_record::tag_t::is_lbl_hash:
+                p.r1->m_lbl_hash = p.m_lbl_hash;
+                break;
             default:
                 UNREACHABLE();
                 break;
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index adb171d19..966e34889 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -102,9 +102,11 @@ namespace euf {
             struct new_lits_qhead {};
             struct inconsistent {};
             struct value_assignment {};
+            struct lbl_hash {};
             enum class tag_t { is_set_parent, is_add_node, is_toggle_merge, 
-                         is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq,
-                         is_new_th_eq_qhead, is_new_lits_qhead, is_inconsistent, is_value_assignment };
+                    is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq,
+                    is_lbl_hash, is_new_th_eq_qhead, is_new_lits_qhead, 
+                    is_inconsistent, is_value_assignment };
             tag_t  tag;
             enode* r1;
             enode* n1;
@@ -116,6 +118,7 @@ namespace euf {
                 };
                 unsigned qhead;
                 bool     m_inconsistent;
+                signed char m_lbl_hash;
             };
             update_record(enode* r1, enode* n1, unsigned r2_num_parents) :
                 tag(tag_t::is_set_parent), r1(r1), n1(n1), r2_num_parents(r2_num_parents) {}
@@ -139,6 +142,8 @@ namespace euf {
                 tag(tag_t::is_inconsistent), r1(nullptr), n1(nullptr), m_inconsistent(inc) {}
             update_record(enode* n, value_assignment) :
                 tag(tag_t::is_value_assignment), r1(n), n1(nullptr), qhead(0) {}
+            update_record(enode* n, lbl_hash):
+                tag(tag_t::is_lbl_hash), r1(n), n1(nullptr), m_lbl_hash(n->m_lbl_hash) {}
         };
         ast_manager&           m;
         svector<to_merge>      m_to_merge;
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 7d6aa3fdc..ebb553365 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -96,7 +96,6 @@ namespace q {
     }
 
     euf::theory_var solver::mk_var(euf::enode* n) {
-        SASSERT(is_forall(n->get_expr()) || is_exists(n->get_expr()));
         auto v = euf::th_euf_solver::mk_var(n);
         ctx.attach_th_var(n, this, v);        
         return v;