mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

#5215 converting NYI

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-27 16:19:54 -07:00
parent 89373d5bf9
commit 308f399224
3 changed files with 24 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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;

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

@ -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;

1
src/sat/smt/q_solver.cpp
View file

@ -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;