mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix undo record for lblset

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-29 14:06:18 -07:00
parent a8ccbd7103
commit decbf4be11
3 changed files with 14 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/euf/euf_egraph.cpp
View file

@ -302,7 +302,7 @@ namespace euf {
enode* r = n->get_root(); enode* r = n->get_root();
approx_set & r_lbls = r->m_lbls; approx_set & r_lbls = r->m_lbls;
if (!r_lbls.may_contain(n->m_lbl_hash)) { 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); r_lbls.insert(n->m_lbl_hash);
} }
} }
@ -373,6 +373,9 @@ namespace euf {
case update_record::tag_t::is_lbl_hash: case update_record::tag_t::is_lbl_hash:
p.r1->m_lbl_hash = p.m_lbl_hash; p.r1->m_lbl_hash = p.m_lbl_hash;
break; break;
case update_record::tag_t::is_lbl_set:
p.r1->m_lbls.set(p.m_lbls);
break;
default: default:
UNREACHABLE(); UNREACHABLE();
break; break;

6
src/ast/euf/euf_egraph.h
View file

@ -103,10 +103,11 @@ namespace euf {
struct inconsistent {}; struct inconsistent {};
struct value_assignment {}; struct value_assignment {};
struct lbl_hash {}; struct lbl_hash {};
struct lbl_set {};
enum class tag_t { is_set_parent, is_add_node, is_toggle_merge, 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_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_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; tag_t tag;
enode* r1; enode* r1;
enode* n1; enode* n1;
@ -119,6 +120,7 @@ namespace euf {
unsigned qhead; unsigned qhead;
bool m_inconsistent; bool m_inconsistent;
signed char m_lbl_hash; signed char m_lbl_hash;
unsigned long long m_lbls;
}; };
update_record(enode* r1, enode* n1, unsigned r2_num_parents) : 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) {} 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) {} tag(tag_t::is_value_assignment), r1(n), n1(nullptr), qhead(0) {}
update_record(enode* n, lbl_hash): update_record(enode* n, lbl_hash):
tag(tag_t::is_lbl_hash), r1(n), n1(nullptr), m_lbl_hash(n->m_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; ast_manager& m;
svector<to_merge> m_to_merge; svector<to_merge> m_to_merge;

6
src/util/approx_set.h
View file

@ -70,6 +70,10 @@ public:
m_set(s.m_set) { m_set(s.m_set) {
} }
void set(R s) { m_set = s; }
R get() const { return m_set; }
void insert(T const & e) { void insert(T const & e) {
m_set |= e2s(e); m_set |= e2s(e);
} }
@ -162,7 +166,7 @@ class approx_set : public u_approx_set {
public: public:
approx_set():u_approx_set() {} approx_set():u_approx_set() {}
approx_set(unsigned e):u_approx_set(e) {} approx_set(unsigned e):u_approx_set(e) {}
class iterator { class iterator {
unsigned long long m_set; unsigned long long m_set;
unsigned m_val; unsigned m_val;