mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 03:10:25 +00:00
Code Activity

fix merge fails

Browse source
This commit is contained in:
Jakob Rath 2023-12-07 16:24:28 +01:00
parent cd50f2ea88
commit 49800d6da5
4 changed files with 6 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -18,9 +18,6 @@ Notes:
#include "ast/euf/euf_egraph.h" #include "ast/euf/euf_egraph.h"
#include "ast/euf/euf_bv_plugin.h"
#include "ast/euf/euf_arith_plugin.h"
#include "ast/euf/euf_specrel_plugin.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/ast_translation.h" #include "ast/ast_translation.h"
@ -123,10 +120,8 @@ namespace euf {
n->mark_interpreted(); n->mark_interpreted();
if (m_on_make) if (m_on_make)
m_on_make(n); m_on_make(n);
if (num_args == 0)
if (num_args == 0)
return n; return n;
if (m.is_eq(f) && !m.is_iff(f)) { if (m.is_eq(f) && !m.is_iff(f)) {
n->set_is_equality(); n->set_is_equality();
reinsert_equality(n); reinsert_equality(n);
@ -474,7 +469,7 @@ namespace euf {
if (!n1->cgc_enabled() && !n2->cgc_enabled()) if (!n1->cgc_enabled() && !n2->cgc_enabled())
return; return;
SASSERT(n1->get_sort() == n2->get_sort());
enode* r1 = n1->get_root(); enode* r1 = n1->get_root();
enode* r2 = n2->get_root(); enode* r2 = n2->get_root();
if (r1 == r2) if (r1 == r2)
@ -484,7 +479,6 @@ namespace euf {
IF_VERBOSE(20, j.display(verbose_stream() << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n";); IF_VERBOSE(20, j.display(verbose_stream() << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n";);
force_push(); force_push();
SASSERT(m_num_scopes == 0); SASSERT(m_num_scopes == 0);
SASSERT(n1->get_sort() == n2->get_sort());
++m_stats.m_num_merge; ++m_stats.m_num_merge;
if (r1->interpreted() && r2->interpreted()) { if (r1->interpreted() && r2->interpreted()) {
set_conflict(n1, n2, j); set_conflict(n1, n2, j);
@ -510,7 +504,7 @@ namespace euf {
std::swap(r1->m_next, r2->m_next); std::swap(r1->m_next, r2->m_next);
r2->inc_class_size(r1->class_size()); r2->inc_class_size(r1->class_size());
r2->set_is_shared(l_undef); r2->set_is_shared(l_undef);
merge_th_eq(r1, r2, j); merge_th_eq(r1, r2);
reinsert_parents(r1, r2); reinsert_parents(r1, r2);
if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr()))) if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr())))
add_literal(n1, r2); add_literal(n1, r2);
@ -521,7 +515,6 @@ namespace euf {
for (auto& cb : m_on_merge) for (auto& cb : m_on_merge)
cb(r2, r1); cb(r2, r1);
} }
void egraph::remove_parents(enode* r) { void egraph::remove_parents(enode* r) {
@ -568,7 +561,7 @@ namespace euf {
} }
} }
void egraph::merge_th_eq(enode* n, enode* root, justification j) { void egraph::merge_th_eq(enode* n, enode* root) {
SASSERT(n != root); SASSERT(n != root);
for (auto const& iv : enode_th_vars(n)) { for (auto const& iv : enode_th_vars(n)) {
theory_id id = iv.get_id(); theory_id id = iv.get_id();

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

@ -234,7 +234,7 @@ namespace euf {
void force_push(); void force_push();
void set_conflict(enode* n1, enode* n2, justification j); void set_conflict(enode* n1, enode* n2, justification j);
void merge(enode* n1, enode* n2, justification j); void merge(enode* n1, enode* n2, justification j);
void merge_th_eq(enode* n, enode* root, justification j); void merge_th_eq(enode* n, enode* root);
void merge_justification(enode* n1, enode* n2, justification j); void merge_justification(enode* n1, enode* n2, justification j);
void reinsert_parents(enode* r1, enode* r2); void reinsert_parents(enode* r1, enode* r2);
void remove_parents(enode* r); void remove_parents(enode* r);
@ -280,8 +280,6 @@ namespace euf {
void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); } void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); }
void new_diseq(enode* n); void new_diseq(enode* n);
bool can_propagate() const { return !m_to_merge.empty(); }
/** /**
\brief propagate set of merges. \brief propagate set of merges.
This call may detect an inconsistency. Then inconsistent() is true. This call may detect an inconsistency. Then inconsistent() is true.

2
src/sat/smt/bv_solver.cpp
View file

@ -387,7 +387,7 @@ namespace bv {
for (unsigned i = 0; i < c.m_num_literals; ++i) for (unsigned i = 0; i < c.m_num_literals; ++i)
r.push_back(c.m_literals[i]); r.push_back(c.m_literals[i]);
for (unsigned i = 0; i < c.m_num_eqs; ++i) for (unsigned i = 0; i < c.m_num_eqs; ++i)
ctx.add_antecedent(probing, c.m_eqs[i].first, c.m_eqs[i].second); ctx.add_eq_antecedent(probing, c.m_eqs[i].first, c.m_eqs[i].second);
break; break;
} }
default: default:

9
src/util/dependency.h
View file

@ -341,15 +341,6 @@ public:
void linearize(ptr_vector<dependency>& d, vector<value, false> & vs) const { void linearize(ptr_vector<dependency>& d, vector<value, false> & vs) const {
return m_dep_manager.linearize(d, vs); return m_dep_manager.linearize(d, vs);
} }
static vector<value, false> const& s_linearize(dependency* d, vector<value, false>& vs) {
dep_manager::s_linearize(d, vs);
return vs;
}
void linearize(ptr_vector<dependency>& d, vector<value, false> & vs) {
return m_dep_manager.linearize(d, vs);
}
void reset() { void reset() {
m_allocator.reset(); m_allocator.reset();