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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-02-27 07:06:05 -08:00
parent f46c3782d6
commit 9888d87294
3 changed files with 30 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/ast/sls/bv_sls.cpp
View file

@ -83,16 +83,16 @@ namespace bv {
} }
if (!m_repair_up.empty()) { if (!m_repair_up.empty()) {
unsigned index = m_rand(m_repair_up.size()); unsigned index = m_repair_up.elem_at(m_rand(m_repair_up.size()));
m_repair_up.remove(index); m_repair_up.remove(index);
e = m_terms.term(m_repair_up.elem_at(index)); e = m_terms.term(index);
return { false, e }; return { false, e };
} }
if (!m_repair_roots.empty()) { if (!m_repair_roots.empty()) {
unsigned index = m_rand(m_repair_up.size()); unsigned index = m_repair_roots.elem_at(m_rand(m_repair_roots.size()));
e = m_terms.term(m_repair_up.elem_at(index)); e = m_terms.term(index);
m_repair_roots.remove(index); m_repair_root = index;
return { true, e }; return { true, e };
} }
@ -107,8 +107,6 @@ namespace bv {
auto [down, e] = next_to_repair(); auto [down, e] = next_to_repair();
if (!e) if (!e)
return l_true; return l_true;
if (eval_is_correct(e))
continue;
trace_repair(down, e); trace_repair(down, e);
@ -138,10 +136,23 @@ namespace bv {
} }
void sls::try_repair_down(app* e) { void sls::try_repair_down(app* e) {
if (eval_is_correct(e)) {
m_repair_roots.remove(m_repair_root);
m_repair_root = UINT_MAX;
return;
}
unsigned n = e->get_num_args(); unsigned n = e->get_num_args();
if (n == 0) { if (n == 0) {
m_eval.wval(e).commit_eval(); auto& v = m_eval.wval(e);
m_repair_up.insert(e->get_id()); v.commit_eval();
verbose_stream() << mk_pp(e, m) << " := " << v << "\n";
for (auto p : m_terms.parents(e))
m_repair_up.insert(p->get_id());
m_repair_roots.remove(m_repair_root);
m_repair_root = UINT_MAX;
return;
} }
unsigned s = m_rand(n); unsigned s = m_rand(n);
@ -152,7 +163,6 @@ namespace bv {
return; return;
} }
} }
// search a new root / random walk to repair // search a new root / random walk to repair
} }

1
src/ast/sls/bv_sls.h
View file

@ -46,6 +46,7 @@ namespace bv {
sls_stats m_stats; sls_stats m_stats;
indexed_uint_set m_repair_up, m_repair_roots; indexed_uint_set m_repair_up, m_repair_roots;
unsigned m_repair_down = UINT_MAX; unsigned m_repair_down = UINT_MAX;
unsigned m_repair_root = UINT_MAX;
ptr_vector<expr> m_todo; ptr_vector<expr> m_todo;
random_gen m_rand; random_gen m_rand;
config m_config; config m_config;

8
src/ast/sls/bv_sls_eval.cpp
View file

@ -299,6 +299,7 @@ namespace bv {
sls_valuation& sls_eval::eval(app* e) const { sls_valuation& sls_eval::eval(app* e) const {
auto& val = *m_values[e->get_id()]; auto& val = *m_values[e->get_id()];
eval(e, val); eval(e, val);
verbose_stream() << "eval " << mk_pp(e, m) << " := " << val << " " << val.eval << "\n";
return val; return val;
} }
@ -1020,6 +1021,7 @@ namespace bv {
unsigned parity_e = b.parity(e); unsigned parity_e = b.parity(e);
unsigned parity_b = b.parity(b.bits()); unsigned parity_b = b.parity(b.bits());
verbose_stream() << e << " := " << a << " * " << b << "\n";
if (b.is_zero(e)) { if (b.is_zero(e)) {
a.get_variant(m_tmp, m_rand); a.get_variant(m_tmp, m_rand);
for (unsigned i = 0; i < b.bw - parity_b; ++i) for (unsigned i = 0; i < b.bw - parity_b; ++i)
@ -1027,6 +1029,12 @@ namespace bv {
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
if (b.is_zero()) {
a.get_variant(m_tmp, m_rand);
return a.set_repair(random_bool(), m_tmp);
}
auto& x = m_tmp; auto& x = m_tmp;
auto& y = m_tmp2; auto& y = m_tmp2;
auto& quot = m_tmp3; auto& quot = m_tmp3;