From decbf4be115d7b3dbd28ac8838ba8e4b4ac1104d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 29 Apr 2021 14:06:18 -0700
Subject: [PATCH] fix undo record for lblset

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/euf/euf_egraph.cpp | 5 ++++-
 src/ast/euf/euf_egraph.h   | 6 +++++-
 src/util/approx_set.h      | 6 +++++-
 3 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index fab134fdd..a817a5e2b 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -302,7 +302,7 @@ namespace euf {
         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()));
+            m_updates.push_back(update_record(r, update_record::lbl_set()));
             r_lbls.insert(n->m_lbl_hash);
         }
     }
@@ -373,6 +373,9 @@ namespace euf {
             case update_record::tag_t::is_lbl_hash:
                 p.r1->m_lbl_hash = p.m_lbl_hash;
                 break;
+            case update_record::tag_t::is_lbl_set:
+                p.r1->m_lbls.set(p.m_lbls);
+                break;
             default:
                 UNREACHABLE();
                 break;
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 966e34889..1e0252922 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -103,10 +103,11 @@ namespace euf {
             struct inconsistent {};
             struct value_assignment {};
             struct lbl_hash {};
+            struct lbl_set {};
             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_lbl_hash, is_new_th_eq_qhead, is_new_lits_qhead, 
-                    is_inconsistent, is_value_assignment };
+                    is_inconsistent, is_value_assignment, is_lbl_set };
             tag_t  tag;
             enode* r1;
             enode* n1;
@@ -119,6 +120,7 @@ namespace euf {
                 unsigned qhead;
                 bool     m_inconsistent;
                 signed char m_lbl_hash;
+                unsigned long long m_lbls;
             };
             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) {}
@@ -144,6 +146,8 @@ namespace euf {
                 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) {}
+            update_record(enode* n, lbl_set):
+                tag(tag_t::is_lbl_set), r1(n), n1(nullptr), m_lbls(n->m_lbls.get()) {}    
         };
         ast_manager&           m;
         svector<to_merge>      m_to_merge;
diff --git a/src/util/approx_set.h b/src/util/approx_set.h
index 5ef2e650e..bce67f692 100644
--- a/src/util/approx_set.h
+++ b/src/util/approx_set.h
@@ -70,6 +70,10 @@ public:
         m_set(s.m_set) {
     }
 
+    void set(R s) { m_set = s; }
+
+    R get() const { return m_set; }
+
     void insert(T const & e) {
         m_set |= e2s(e);
     }
@@ -162,7 +166,7 @@ class approx_set : public u_approx_set {
 public:
     approx_set():u_approx_set() {}
     approx_set(unsigned e):u_approx_set(e) {}
-
+    
     class iterator {
         unsigned long long m_set;
         unsigned           m_val;