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

reset kv map consistently with egraph

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-27 17:09:38 -08:00
parent 57a5474ab4
commit a8279dd9d5
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/sls/sls_array_plugin.cpp
View file

@ -33,8 +33,8 @@ namespace sls {
bool array_plugin::is_sat() { bool array_plugin::is_sat() {
if (!m_has_arrays) if (!m_has_arrays)
return true; return true;
m_g = alloc(euf::egraph, m);
m_kv = nullptr; m_kv = nullptr;
m_g = alloc(euf::egraph, m);
init_egraph(*m_g); init_egraph(*m_g);
saturate(*m_g); saturate(*m_g);
if (m_g->inconsistent()) { if (m_g->inconsistent()) {
@ -382,6 +382,7 @@ namespace sls {
expr_ref array_plugin::get_value(expr* e) { expr_ref array_plugin::get_value(expr* e) {
SASSERT(a.is_array(e)); SASSERT(a.is_array(e));
if (!m_g) { if (!m_g) {
m_kv = nullptr;
m_g = alloc(euf::egraph, m); m_g = alloc(euf::egraph, m);
init_egraph(*m_g); init_egraph(*m_g);
flet<bool> _strong(m_add_conflicts, false); flet<bool> _strong(m_add_conflicts, false);
@ -395,7 +396,8 @@ namespace sls {
auto& kv = *m_kv; auto& kv = *m_kv;
auto n = m_g->find(e)->get_root(); auto n = m_g->find(e)->get_root();
expr_ref r(n->get_expr(), m), key(m); expr_ref r(n->get_expr(), m), key(m);
expr_mark visited; expr_mark visited;
SASSERT(kv.contains(n));
for (auto [k, v] : kv[n]) { for (auto [k, v] : kv[n]) {
ptr_vector<expr> args; ptr_vector<expr> args;
key = ctx.get_value(k.sel->get_arg(1)->get_expr()); key = ctx.get_value(k.sel->get_arg(1)->get_expr());