From be5a16cc4dfed5d26518fbf3d159beb6ce63b800 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Jan 2025 19:05:33 -0800 Subject: [PATCH] fixup scoring function for sle and ule Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_lookahead.cpp | 23 +++++++++++++++-------- src/ast/sls/sls_bv_tracker.h | 30 ++++++++++++++++++------------ src/tactic/sls/sls_tactic.cpp | 5 +++-- 3 files changed, 36 insertions(+), 22 deletions(-) diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index bc53da2172..e644458118 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -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); } } diff --git a/src/ast/sls/sls_bv_tracker.h b/src/ast/sls/sls_bv_tracker.h index 3d74d55df8..46e14684be 100644 --- a/src/ast/sls/sls_bv_tracker.h +++ b/src/ast/sls/sls_bv_tracker.h @@ -688,8 +688,7 @@ class sls_tracker { 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 @@ class sls_tracker { 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 @@ class sls_tracker { 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); diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 65b7025f7a..5e04900a41 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -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) {