mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix dirty flag setting

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-10-21 19:57:47 -07:00
parent b0dd83cc60
commit 93086143b3
3 changed files with 20 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -80,13 +80,13 @@ void elim_unconstrained::eliminate() {
continue;
}
expr* e = get_parent(v);
IF_VERBOSE(11, for (expr* p : n.m_parents) verbose_stream() << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";);
TRACE("elim_unconstrained", for (expr* p : n.m_parents) tout << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";);
if (!e || !is_app(e) || !is_ground(e)) {
n.m_refcount = 0;
continue;
}
if (m_heap.contains(root(e))) {
IF_VERBOSE(11, verbose_stream() << "already in heap " << mk_bounded_pp(e, m) << "\n");
TRACE("elim_unconstrained", tout << "already in heap " << mk_bounded_pp(e, m) << "\n");
continue;
}
app* t = to_app(e);
@ -107,7 +107,7 @@ void elim_unconstrained::eliminate() {
n.m_refcount = 0;
m_args.shrink(sz);
if (!inverted) {
IF_VERBOSE(11, verbose_stream() << "not inverted " << mk_bounded_pp(e, m) << "\n");
TRACE("elim_unconstrained", tout << "not inverted " << mk_bounded_pp(e, m) << "\n");
continue;
}
@ -147,10 +147,10 @@ expr* elim_unconstrained::get_parent(unsigned n) const {
}
void elim_unconstrained::invalidate_parents(expr* e) {
ptr_vector<expr> todo;
ptr_buffer<expr> todo;
do {
node& n = get_node(e);
if (!n.m_dirty) {
if (!n.m_dirty && e == n.m_term) {
n.m_dirty = true;
for (expr* e : n.m_parents)
todo.push_back(e);
@ -299,7 +299,7 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
return expr_ref(t, m);
if (!is_node(t))
return expr_ref(t, m);
ptr_vector<expr> todo;
ptr_buffer<expr> todo;
todo.push_back(t);
while (!todo.empty()) {
t = todo.back();
@ -310,6 +310,7 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
unsigned sz0 = todo.size();
if (is_app(t)) {
if (n.m_term != t) {
n.m_dirty = false;
todo.pop_back();
continue;
}

4
src/ast/sls/sls_bv_plugin.cpp
View file

@ -57,8 +57,10 @@ namespace sls {
return;
auto a = to_app(e);
if (!m_eval.eval_is_correct(a))
if (!m_eval.eval_is_correct(a)) {
IF_VERBOSE(20, verbose_stream() << "repair " << lit << " " << mk_bounded_pp(e, m) << "\n");
ctx.new_value_eh(e);
}
}
bool bv_plugin::propagate() {

18
src/sat/smt/sls_solver.cpp
View file

@ -234,18 +234,20 @@ namespace sls {
}
void export_phase_to_smt() {
if (m_has_new_sls_phase) {
IF_VERBOSE(1, verbose_stream() << "new SLS -> SMT phase\n");
std::lock_guard<std::mutex> lock(s.m_mutex);
for (unsigned i = 0; i < m_sls_phase.size(); ++i)
s.s().set_phase(sat::literal(i, !m_sls_phase[i]));
m_has_new_sls_phase = false;
}
if (!m_has_new_sls_phase)
return;
IF_VERBOSE(1, verbose_stream() << "new SLS -> SMT phase\n");
std::lock_guard<std::mutex> lock(s.m_mutex);
for (unsigned i = 0; i < m_sls_phase.size(); ++i)
s.s().set_phase(sat::literal(i, !m_sls_phase[i]));
m_has_new_sls_phase = false;
}
void import_phase_from_smt() {
IF_VERBOSE(1, verbose_stream() << "new SMT -> SLS phase\n");
if (m_has_new_sat_phase)
return;
m_has_new_sat_phase = true;
IF_VERBOSE(1, verbose_stream() << "new SMT -> SLS phase\n");
s.s().set_has_new_best_phase(false);
std::lock_guard<std::mutex> lock(s.m_mutex);
for (auto v : m_shared_vars)