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

fixup scoring function for sle and ule

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-05 19:05:33 -08:00
parent b3e410b5e4
commit be5a16cc4d
3 changed files with 36 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -81,7 +81,7 @@ namespace sls {
continue;
// bail out if no progress, and try random update
if (apply_random_update(get_candidate_uninterp()))
if (apply_random_update(m_config.walksat_repick?get_candidate_uninterp():vars))
recalibrate_weights();
}
m_config.max_moves_base += 100;
@ -379,18 +379,24 @@ namespace sls {
auto const& vx = wval(x);
auto const& vy = wval(y);
if (is_true)
if (is_true) {
if (vx.bits() <= vy.bits())
return 1.0;
// x > y as unsigned.
// x - y > 0
// score = (x - y) / 2^bw
vx.set_sub(m_ev.m_tmp, vx.bits(), vy.bits());
}
else {
if (!(vx.bits() <= vy.bits()))
return 1.0;
// x <= y as unsigned.
// y - x >= 0
// score = (y - x + 1) / 2^bw
vx.set_sub(m_ev.m_tmp, vy.bits(), vx.bits());
vx.add1(m_ev.m_tmp);
}
rational n = m_ev.m_tmp.get_value(vx.nw);
n /= rational(rational::power_of_two(vx.bw));
double dbl = n.get_double();
@ -407,13 +413,15 @@ namespace sls {
m_ev.m_tmp2.set(vx.bw - 1, !m_ev.m_tmp2.get(vx.bw - 1));
if (is_true) {
// x >s y
// x' - y' > 0
if (m_ev.m_tmp2 <= m_ev.m_tmp)
return 1.0;
// otherwise x' > y'
vx.set_sub(m_ev.m_tmp3, m_ev.m_tmp2, m_ev.m_tmp);
}
else {
// x <=s y
// y' - x' >= 0
if (!(m_ev.m_tmp2 <= m_ev.m_tmp))
return 1.0;
// x' <= y'
vx.set_sub(m_ev.m_tmp3, m_ev.m_tmp, m_ev.m_tmp2);
vx.add1(m_ev.m_tmp3);
}
@ -642,7 +650,7 @@ namespace sls {
auto v1 = m_ev.bval1(e);
CTRACE("bv", m_ev.get_bool_value(e) != v1, tout << "updated truth value " << mk_bounded_pp(e, m) << " := " << v1 << "\n";);
CTRACE("bv_verbose", m_ev.get_bool_value(e) != v1, tout << "updated truth value " << mk_bounded_pp(e, m) << " := " << v1 << "\n";);
if (m_config.use_top_level_assertions) {
if (m_ev.get_bool_value(e) == v1)
@ -681,7 +689,6 @@ namespace sls {
if (is_root(e)) {
double score = new_score(e);
m_top_score += get_weight(e) * (score - old_score(e));
//verbose_stream() << "set score " << mk_bounded_pp(e, m) << " := " << score << "\n";
set_score(e, score);
}
}

30
src/ast/sls/sls_bv_tracker.h
View file

@ -688,8 +688,7 @@ public:
else
res = (m_mpz_manager.is_one(r)) ? 1.0 : 0.0;
}
else if (m_manager.is_and(n)) {
SASSERT(!negated);
else if (m_manager.is_and(n) && !negated) {
/* Andreas: Seems to have no effect. But maybe you want to try it again at some point.
double sum = 0.0;
for (unsigned i = 0; i < a->get_num_args(); i++)
@ -697,25 +696,37 @@ public:
res = sum / (double) a->get_num_args(); */
double min = 1.0;
for (auto arg : *to_app(n))
min = std::min(get_score(arg), min);
min = std::min(score(arg), min);
res = min;
}
else if (m_manager.is_or(n)) {
SASSERT(!negated);
else if (m_manager.is_and(n) && negated) {
double r = 0.0;
for (auto arg : *to_app(n))
r = std::max(score(arg), r);
res = 1.0 - r;
}
else if (m_manager.is_or(n) && !negated) {
double max = 0.0;
for (auto arg : *to_app(n))
max = std::max(get_score(arg), max);
res = max;
}
else if (m_manager.is_or(n) && negated) {
double r = 1.0;
for (auto arg : *to_app(n))
r = std::min(get_score(arg), r);
res = 1.0 - r;
}
else if (m_manager.is_ite(n)) {
SASSERT(!negated);
app * a = to_app(n);
SASSERT(a->get_num_args() == 3);
const mpz & cond = get_value(a->get_arg(0));
double s_t = get_score(a->get_arg(1));
double s_f = get_score(a->get_arg(2));
res = (m_mpz_manager.is_one(cond)) ? s_t : s_f;
if (negated)
res = 1.0 - res;
}
else if (m_manager.is_eq(n) || m_manager.is_iff(n)) {
app * a = to_app(n);
@ -843,15 +854,10 @@ public:
m_mpz_manager.del(y);
}
else if (m_manager.is_not(n)) {
SASSERT(!negated);
app * a = to_app(n);
SASSERT(a->get_num_args() == 1);
expr * child = a->get_arg(0);
// Precondition: Assertion set is in NNF.
// Also: careful about the unsat assertion scaling further down.
if (m_manager.is_and(child) || m_manager.is_or(child))
NOT_IMPLEMENTED_YET();
res = score_bool(child, true);
res = score_bool(child, !negated);
}
else if (m_manager.is_distinct(n)) {
app * a = to_app(n);

5
src/tactic/sls/sls_tactic.cpp
View file

@ -251,8 +251,9 @@ static tactic * mk_preamble(ast_manager & m, params_ref const & p) {
mk_bv_size_reduction_tactic(m),
using_params(mk_simplify_tactic(m), simp2_p)),
using_params(mk_simplify_tactic(m), hoist_p),
mk_max_bv_sharing_tactic(m),
mk_nnf_tactic(m, p));
mk_max_bv_sharing_tactic(m)//,
// mk_nnf_tactic(m, p)
);
}
tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {