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

make ite evaluation sensitive to using temporary Boolean assignment

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-05 20:59:14 -08:00
parent be5a16cc4d
commit e45f186e67
4 changed files with 17 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/sls/sls_bv_eval.cpp
View file

@ -307,7 +307,8 @@ namespace sls {
SASSERT(bv.is_bv(e->get_arg(1)));
auto& val_th = wval(e->get_arg(1));
auto& val_el = wval(e->get_arg(2));
if (bval0(e->get_arg(0)))
bool b = m_use_tmp_bool_value ? get_bool_value(e->get_arg(0)) : bval0(e->get_arg(0));
if (b)
val.set(val_th.bits());
else
val.set(val_el.bits());

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

@ -177,6 +177,8 @@ namespace sls {
bool is_fixed0(expr* e) const { return m_is_fixed.get(e->get_id(), false); }
// control whether if-then-else is eavaluated based on SAT solver or temporary values.
bool m_use_tmp_bool_value = false;
sls::bv_valuation& eval(app* e) const;
void set_random(app* e);

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

@ -54,6 +54,7 @@ namespace sls {
updt_params(ctx.get_params());
if (!m_config.use_lookahead_bv)
return;
flet<bool> _set_use_tmp(m_ev.m_use_tmp_bool_value, true);
initialize_bool_values();
rescore();
m_config.max_moves = m_stats.m_moves + m_config.max_moves_base;
@ -88,6 +89,7 @@ namespace sls {
}
void bv_lookahead::initialize_bool_values() {
m_ev.restore_bool_values(0);
for (auto t : ctx.subterms()) {
if (bv.is_bv(t)) {
auto& v = m_ev.eval(to_app(t));
@ -106,14 +108,12 @@ namespace sls {
* Flip truth values of root literals if they are updated.
*/
void bv_lookahead::finalize_bool_values() {
if (false && !m_config.use_top_level_assertions)
return;
for (auto lit : ctx.root_literals()) {
auto a = ctx.atom(lit.var());
auto v0 = ctx.is_true(lit.var());
auto v1 = m_ev.get_bool_value(a);
if (v0 != v1)
ctx.flip(lit.var());
for (unsigned v = ctx.num_bool_vars(); v-- > 0; ) {
auto a = ctx.atom(v);
if (!a)
continue;
if (m_ev.get_bool_value(a) != ctx.is_true(v))
ctx.flip(v);
}
}
@ -197,6 +197,7 @@ namespace sls {
expr* e = nullptr;
if (m_config.ucb) {
double max = -1.0;
TRACE("bv", tout << "select\n");
for (auto a : get_root_assertions()) {
auto const& vars = m_ev.terms.uninterp_occurs(a);
//verbose_stream() << mk_bounded_pp(a, m) << " " << assertion_is_true(a) << " num vars " << vars.size() << "\n";
@ -206,6 +207,7 @@ namespace sls {
if (vars.empty())
continue;
auto score = old_score(a);
TRACE("bv", tout << "score " << score << " " << mk_bounded_pp(a, m) << "\n");
auto q = score
+ m_config.ucb_constant * sqrt(log((double)m_touched) / get_touched(a))
+ m_config.ucb_noise * ctx.rand(512);
@ -428,6 +430,7 @@ namespace sls {
rational n = m_ev.m_tmp3.get_value(vx.nw);
n /= rational(rational::power_of_two(vx.bw));
double dbl = n.get_double();
verbose_stream() << mk_bounded_pp(a, m) << " x:" <<vx << " y:" << vy << " " << dbl << "\n";
return (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
}
else if (is_true && m.is_distinct(a) && bv.is_bv(to_app(a)->get_arg(0))) {
@ -518,7 +521,6 @@ namespace sls {
auto score = lookahead_update(u, new_value);
++m_stats.m_lookaheads;
//verbose_stream() << "lookahead set " << mk_bounded_pp(u, m) << " := " << new_value << " score: " << score << " best score: " << m_best_score << "\n";
//verbose_stream() << mk_bounded_pp(u, m) << " := " << new_value << " score: " << score << "\n";
if (score > m_best_score) {
m_best_score = score;
m_best_expr = u;

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

@ -156,9 +156,9 @@ namespace sls {
}
else if (m.is_ite(e, c, th, el)) {
todo.push_back(c);
if (ctx.is_true(c))
//if (ctx.is_true(c))
todo.push_back(th);
else
//else
todo.push_back(el);
}
else if (is_uninterp(e) && (m.is_bool(e) || bv.is_bv(e)))