mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

fix stack overflow regression in bool_rewriter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-12-28 18:21:59 -08:00
parent 3526d03cca
commit 6ea68310c9
3 changed files with 17 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/rewriter/bool_rewriter.cpp
View file

@ -775,8 +775,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
std::swap(lhs, rhs); std::swap(lhs, rhs);
if (m().is_not(lhs, lhs)) { if (m().is_not(lhs, lhs)) {
mk_eq(lhs, rhs, result); result = m().mk_not(m().mk_eq(lhs, rhs));
mk_not(result, result);
return BR_REWRITE2; return BR_REWRITE2;
} }

17
src/ast/sls/sls_bv_lookahead.cpp
View file

@ -91,12 +91,11 @@ namespace sls {
auto const& vars = m_ev.terms.uninterp_occurs(a); auto const& vars = m_ev.terms.uninterp_occurs(a);
VERIFY(!vars.empty()); VERIFY(!vars.empty());
TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": "; TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": ";
for (auto e : vars) for (auto e : vars) tout << mk_bounded_pp(e, m) << " ";
tout << mk_bounded_pp(e, m) << " ";
tout << "\n";); tout << "\n";);
return vars; return vars;
} }
return m_vars; return m_empty_vars;
} }
@ -258,10 +257,10 @@ namespace sls {
else else
has_tabu = true; has_tabu = true;
} }
else if (m.is_bool(a) && m_ev.can_eval1(a)) { else if (is_root(a))
rescore(a); rescore(a);
} else if (m.is_bool(a))
continue;
else { else {
IF_VERBOSE(1, verbose_stream() << "skipping " << mk_bounded_pp(a, m) << "\n"); IF_VERBOSE(1, verbose_stream() << "skipping " << mk_bounded_pp(a, m) << "\n");
has_tabu = true; has_tabu = true;
@ -379,9 +378,11 @@ namespace sls {
max_depth = std::max(max_depth, get_depth(p)); max_depth = std::max(max_depth, get_depth(p));
} }
} }
else if (m.is_bool(e) && m_ev.can_eval1(e)) { else if (is_root(e)) {
rescore(e); rescore(e);
} }
else if (m.is_bool(e))
continue;
else { else {
UNREACHABLE(); UNREACHABLE();
} }
@ -450,6 +451,7 @@ namespace sls {
void bv_lookahead::rescore() { void bv_lookahead::rescore() {
m_top_score = 0; m_top_score = 0;
m_rescore = false; m_rescore = false;
m_is_root.reset();
for (auto lit : ctx.root_literals()) { for (auto lit : ctx.root_literals()) {
auto e = ctx.atom(lit.var()); auto e = ctx.atom(lit.var());
if (!e || !is_app(e)) if (!e || !is_app(e))
@ -461,6 +463,7 @@ namespace sls {
double score = new_score(a); double score = new_score(a);
set_score(a, score); set_score(a, score);
m_top_score += score; m_top_score += score;
m_is_root.mark(a);
} }
verbose_stream() << "top score " << m_top_score << "\n"; verbose_stream() << "top score " << m_top_score << "\n";

7
src/ast/sls/sls_bv_lookahead.h
View file

@ -67,7 +67,9 @@ namespace sls {
bvect m_best_value; bvect m_best_value;
expr* m_best_expr = nullptr; expr* m_best_expr = nullptr;
bool m_rescore = true; bool m_rescore = true;
ptr_vector<expr> m_vars; ptr_vector<expr> m_empty_vars;
obj_map<expr, bool_info> m_bool_info;
expr_mark m_is_root;
void init_updates(); void init_updates();
@ -84,11 +86,12 @@ namespace sls {
void rescore(); void rescore();
obj_map<expr, bool_info> m_bool_info;
unsigned get_weight(expr* e); unsigned get_weight(expr* e);
void inc_weight(expr* e); void inc_weight(expr* e);
void dec_weight(expr* e); void dec_weight(expr* e);
void recalibrate_weights(); void recalibrate_weights();
bool is_root(expr* e) { return m_is_root.is_marked(e); }
void try_set(expr* u, bvect const& new_value); void try_set(expr* u, bvect const& new_value);
void add_updates(expr* u); void add_updates(expr* u);