mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

shave off bv test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-06 17:25:30 -08:00
parent e3e650a249
commit 59fad2b10a
2 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -482,7 +482,7 @@ namespace sls {
if (!wval(t).can_set(new_value))
return -1000000;
wval(t).eval = new_value;
insert_update(t);
insert_update(t, true);
}
else if (m.is_bool(t))
m_ev.set_bool_value_no_log(t, !m_ev.get_bool_value(t));
@ -496,7 +496,7 @@ namespace sls {
if (t != a) {
if (is_bv)
m_ev.eval(a);
insert_update(a);
insert_update(a, is_bv);
}
if (is_root(a)) {
//verbose_stream() << "scores " << mk_bounded_pp(a, m) << " old: " << old_score(a) << " new: " << new_score(a) << "\n";
@ -749,13 +749,15 @@ namespace sls {
return m_stats.m_random_flips % 100 == 0;
}
void bv_lookahead::insert_update(expr* e) {
void bv_lookahead::insert_update(expr* e, bool is_bv) {
TRACE("sls_verbose", tout << "insert update " << mk_bounded_pp(e, m) << "\n");
if (bv.is_bv(e)) {
if (is_bv) {
SASSERT(bv.is_bv(e));
auto& v = wval(e);
v.commit_eval_ignore_tabu();
}
else if (m.is_bool(e)) {
else {
SASSERT(m.is_bool(e));
auto v1 = m_ev.bval1(to_app(e));
m_ev.set_bool_value_no_log(to_app(e), v1);
}

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

@ -95,7 +95,7 @@ namespace sls {
void populate_update_stack(expr* e);
void clear_update_stack();
void insert_update_stack(expr* e);
void insert_update(expr* e);
void insert_update(expr* e, bool is_bv);
bool_info& get_bool_info(expr* e);
double lookahead_update(expr* u, bvect const& new_value);