From e002c57aa26dc03ecb8b6e1a2ae545212035f6b7 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com> Date: Mon, 30 Dec 2024 17:48:09 +0100 Subject: [PATCH 1/5] Fixed range regex (#7497) --- src/ast/sls/sls_seq_plugin.cpp | 56 +++++++++++++++++++++++----------- src/ast/sls/sls_seq_plugin.h | 1 + 2 files changed, 40 insertions(+), 17 deletions(-) diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index b8835650f..667511e78 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -1925,9 +1925,40 @@ namespace sls { } } + bool seq_plugin::get_bounds(expr* e, unsigned& low, unsigned& high) { + // TODO: remove recursion (though it is probably not deep anyway) + expr* x, * y; + unsigned ch = 0; + if (m.is_and(e, x, y)) { + if (!get_bounds(x, low, high)) + return false; + return get_bounds(y, low, high); + } + if (m.is_eq(e, x, y)) { + if ((is_var(x) && seq.is_const_char(y, ch)) || (is_var(y) && seq.is_const_char(x, ch))) { + if (ch < low || ch > high) + return false; + low = high = ch; + return true; + } + return false; + } + if (seq.is_char_le(e, x, y)) { + if (seq.is_const_char(x, ch)) { + low = std::max(ch, low); + return high >= low; + } + if (seq.is_const_char(y, ch)) { + high = std::min(ch, high); + return high >= low; + } + return false; + } + return false; + } + bool seq_plugin::append_char(expr* r0, expr_ref& r, zstring& s) { - expr* c, * th, * el, * x, * y; - unsigned ch; + expr* c, * th, * el; if (seq.re.is_union(r)) { auto info0 = seq.re.get_info(r0); for (expr* r1 : *to_app(r)) { @@ -1942,21 +1973,12 @@ namespace sls { NOT_IMPLEMENTED_YET(); } if (m.is_ite(r, c, th, el)) { - if (m.is_eq(c, x, y)) { - - if (is_var(x) && seq.is_const_char(y, ch)) { - s += zstring(ch); - r = th; - return true; - } - if (is_var(y) && seq.is_const_char(x, ch)) { - s += zstring(ch); - r = th; - return true; - } - verbose_stream() << "nyi append_char " << mk_bounded_pp(r, m) << "\n"; - NOT_IMPLEMENTED_YET(); - return false; + unsigned low = 0, high = UINT_MAX; + if (get_bounds(c, low, high)) { + SASSERT(low <= high); + s += zstring(low); + r = th; + return true; } verbose_stream() << "nyi append_char " << mk_bounded_pp(r, m) << "\n"; NOT_IMPLEMENTED_YET(); diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h index bd34b3449..c3298cbae 100644 --- a/src/ast/sls/sls_seq_plugin.h +++ b/src/ast/sls/sls_seq_plugin.h @@ -137,6 +137,7 @@ namespace sls { bool is_in_re(zstring const& s, expr* r); bool some_string_in_re(expr* r, zstring& s); + bool get_bounds(expr* e, unsigned& low, unsigned& high); bool append_char(expr* r0, expr_ref& r, zstring& s); // access evaluation From 19c95f856197b137b7eff080f016a6f2efebb5ba Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com> Date: Mon, 30 Dec 2024 17:49:07 +0100 Subject: [PATCH 2/5] Add new string repair heuristic (#7496) * Fixed spurious counterexamples in seq-sls. Updates might not be identity mapping * Removed debug code * One check was missing * Trying different update generation function * Renamed function * Added parameter to select string update function --- src/ast/sls/sls_seq_plugin.cpp | 63 ++++++++++++++++++++++++++++------ src/ast/sls/sls_seq_plugin.h | 10 +++++- src/params/sls_params.pyg | 5 +-- 3 files changed, 64 insertions(+), 14 deletions(-) diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index 667511e78..93e70dfd9 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -95,9 +95,17 @@ Equality solving using stochastic Nelson. #include "ast/sls/sls_seq_plugin.h" #include "ast/sls/sls_context.h" #include "ast/ast_pp.h" +#include "params/sls_params.hpp" namespace sls { + + struct zstring_hash_proc { + unsigned operator()(zstring const & s) const { + auto str = s.encode(); + return string_hash(str.c_str(), static_cast(s.length()), 17); + } + }; seq_plugin::seq_plugin(context& c): plugin(c), @@ -107,6 +115,8 @@ namespace sls { thrw(c.get_manager()) { m_fid = seq.get_family_id(); + sls_params p(c.get_params()); + m_str_update_strategy = p.str_update_strategy() == 0 ? EDIT_CHAR : EDIT_SUBSTR; } void seq_plugin::propagate_literal(sat::literal lit) { @@ -531,12 +541,12 @@ namespace sls { return true; if (len_u < val_x.length()) { for (unsigned i = 0; i + len_u < val_x.length(); ++i) - m_str_updates.push_back({ x, val_x.extract(i, len_u), 1 }); + m_str_updates.push_back({ x, val_x.extract(i, len_u), 1 }); } if (!m_chars.empty()) { zstring ch(m_chars[ctx.rand(m_chars.size())]); m_str_updates.push_back({ x, val_x + ch, 1 }); - m_str_updates.push_back({ x, ch + val_x, 1 }); + m_str_updates.push_back({ x, ch + val_x, 1 }); } return apply_update(); } @@ -619,7 +629,7 @@ namespace sls { if (!is_value(x)) m_str_updates.push_back({ x, strval1(y), 1 }); if (!is_value(y)) - m_str_updates.push_back({ y, strval1(x), 1 }); + m_str_updates.push_back({ y, strval1(x), 1 }); } else { // disequality @@ -665,8 +675,39 @@ namespace sls { return d[n][m]; } - void seq_plugin::add_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars) { + if (m_str_update_strategy == EDIT_CHAR) + add_char_edit_updates(w, val, val_other, chars); + else + add_substr_edit_updates(w, val, val_other, chars); + } + + void seq_plugin::add_substr_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars) { + // all consecutive subsequences of val_other + hashtable> set; + set.insert(zstring("")); + for (unsigned i = 0; i < val_other.length(); ++i) { + for (unsigned j = val_other.length(); j > 0; ++j) { + zstring sub = val_other.extract(i, j); + if (set.contains(sub)) + break; + set.insert(sub); + } + } + + for (auto x : w) { + if (is_value(x)) + continue; + zstring const& a = strval0(x); + for (auto& seq : set) { + if (seq == a) + continue; + m_str_updates.push_back({ x, seq, 1 }); + } + } + } + + void seq_plugin::add_char_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars) { for (auto x : w) { if (is_value(x)) continue; @@ -1057,7 +1098,7 @@ namespace sls { } if (!is_value(xi)) { m_str_updates.push_back({ xi, vi.extract(0, i), score }); - m_str_updates.push_back({ xi, vi.extract(0, i) + zstring(vj[j]), score}); + m_str_updates.push_back({ xi, vi.extract(0, i) + zstring(vj[j]), score}); } if (!is_value(yj)) { m_str_updates.push_back({ yj, vj.extract(0, j), score }); @@ -1236,7 +1277,7 @@ namespace sls { if (!is_value(x)) { m_str_updates.push_back({ x, zstring(), 1 }); if (lenx > r && r >= 0) - m_str_updates.push_back({ x, sx.extract(0, r.get_unsigned()), 1 }); + m_str_updates.push_back({ x, sx.extract(0, r.get_unsigned()), 1 }); } if (!m.is_value(y)) { m_int_updates.push_back({ y, rational(lenx), 1 }); @@ -1287,7 +1328,7 @@ namespace sls { if (value == -1) { m_str_updates.push_back({ y, zstring(m_chars[ctx.rand(m_chars.size())]), 1 }); if (lenx > 0) - m_str_updates.push_back({ x, zstring(), 1 }); + m_str_updates.push_back({ x, zstring(), 1 }); } // change x: // insert y into x at offset @@ -1305,7 +1346,7 @@ namespace sls { if (offset_r.is_unsigned() && 0 <= value && offset_u + value < lenx) { unsigned offs = offset_u + value.get_unsigned(); for (unsigned i = offs; i < lenx; ++i) - m_str_updates.push_back({ y, sx.extract(offs, i - offs + 1), 1 }); + m_str_updates.push_back({ y, sx.extract(offs, i - offs + 1), 1 }); } // change offset: @@ -1436,13 +1477,13 @@ namespace sls { if (idx > 0) su = sa.extract(0, idx); su = su + sa.extract(idx + sb.length(), sa.length() - idx - sb.length()); - m_str_updates.push_back({a, su, 1}); + m_str_updates.push_back({ a, su, 1}); } if (!m_chars.empty() && !is_value(b)) { zstring sb1 = sb + zstring(m_chars[ctx.rand(m_chars.size())]); zstring sb2 = zstring(m_chars[ctx.rand(m_chars.size())]) + sb; - m_str_updates.push_back({b, sb1, 1}); - m_str_updates.push_back({b, sb2, 1}); + m_str_updates.push_back({ b, sb1, 1}); + m_str_updates.push_back({ b, sb2, 1}); } } return apply_update(); diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h index c3298cbae..ff71d257f 100644 --- a/src/ast/sls/sls_seq_plugin.h +++ b/src/ast/sls/sls_seq_plugin.h @@ -42,13 +42,19 @@ namespace sls { ptr_vector lhs, rhs; }; + enum edit_distance_strategy { + EDIT_CHAR, + EDIT_SUBSTR, + }; + seq_util seq; arith_util a; seq_rewriter rw; th_rewriter thrw; scoped_ptr_vector m_values; indexed_uint_set m_chars; // set of characters in the problem - bool m_initialized = false; + bool m_initialized = false; + edit_distance_strategy m_str_update_strategy; struct str_update { expr* e; @@ -122,6 +128,8 @@ namespace sls { unsigned edit_distance_with_updates(string_instance const& a, string_instance const& b); unsigned edit_distance(zstring const& a, zstring const& b); void add_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars); + void add_char_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars); + void add_substr_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars); // regex functionality diff --git a/src/params/sls_params.pyg b/src/params/sls_params.pyg index 854366609..89aa9834f 100644 --- a/src/params/sls_params.pyg +++ b/src/params/sls_params.pyg @@ -3,7 +3,7 @@ def_module_params('sls', description='Experimental Stochastic Local Search Solver (for QFBV only).', params=(max_memory_param(), ('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'), - ('max_repairs', UINT, 1000, 'maximum number of repairs before restart'), + ('max_repairs', UINT, 1000, 'maximum number of repairs before restart'), ('walksat', BOOL, 1, 'use walksat assertion selection (instead of gsat)'), ('walksat_ucb', BOOL, 1, 'use bandit heuristic for walksat assertion selection (instead of random)'), ('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'), @@ -24,5 +24,6 @@ def_module_params('sls', ('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'), ('dt_axiomatic', BOOL, True, 'use axiomatic mode or model reduction for datatype solver'), ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'), - ('random_seed', UINT, 0, 'random seed') + ('random_seed', UINT, 0, 'random seed'), + ('str_update_strategy', UINT, 1, 'string update candidate selection: 0 - single character based update, 1 - subsequence based update') )) From f99e1ee5816aa8645985a67e6e63f5822f2c818d Mon Sep 17 00:00:00 2001 From: Dmitri Date: Mon, 30 Dec 2024 18:49:30 +0200 Subject: [PATCH 3/5] Support BitVectors in the TypeScript Optimize API (#7480) This is just a change in type declarations to allow calling minimize/maximize with BitVectors. --- src/api/js/src/high-level/high-level.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 405d4a5e5..177241bfd 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -1524,11 +1524,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return new AstVectorImpl(check(Z3.optimize_get_assertions(contextPtr, this.ptr))); } - maximize(expr: Arith) { + maximize(expr: Arith | BitVec) { check(Z3.optimize_maximize(contextPtr, this.ptr, expr.ast)); } - minimize(expr: Arith) { + minimize(expr: Arith | BitVec) { check(Z3.optimize_minimize(contextPtr, this.ptr, expr.ast)); } From 322dcec531e58ddf4c24c7a3407bdbf09b84cc46 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 30 Dec 2024 16:49:43 +0000 Subject: [PATCH 4/5] Add 2 new API functions to get depth & groundness of exprs (#7479) * Update api_ast.cpp * Update z3_api.h --- src/api/api_ast.cpp | 14 ++++++++++++++ src/api/z3_api.h | 10 ++++++++++ 2 files changed, 24 insertions(+) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index ecbf86b37..b220443bc 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -425,6 +425,20 @@ extern "C" { RETURN_Z3(of_app(reinterpret_cast(a))); } + bool Z3_API Z3_is_ground(Z3_context c, Z3_ast a) { + LOG_Z3_is_ground(c, a); + RESET_ERROR_CODE(); + CHECK_IS_EXPR(a, 0); + return is_ground(to_expr(a)); + } + + unsigned Z3_API Z3_get_depth(Z3_context c, Z3_ast a) { + LOG_Z3_get_depth(c, a); + RESET_ERROR_CODE(); + CHECK_IS_EXPR(a, 0); + return get_depth(to_expr(a)); + } + Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a) { LOG_Z3_to_func_decl(c, a); RESET_ERROR_CODE(); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 3082e8dc3..aab76ddbc 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4992,6 +4992,16 @@ extern "C" { */ bool Z3_API Z3_is_app(Z3_context c, Z3_ast a); + /** + def_API('Z3_is_ground', BOOL, (_in(CONTEXT), _in(AST))) + */ + bool Z3_API Z3_is_ground(Z3_context c, Z3_ast a); + + /** + def_API('Z3_get_depth', UINT, (_in(CONTEXT), _in(AST))) + */ + unsigned Z3_API Z3_get_depth(Z3_context c, Z3_ast a); + /** def_API('Z3_is_numeral_ast', BOOL, (_in(CONTEXT), _in(AST))) */ From bcf66f214f6924424c9561675f5864617663eed8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Dec 2024 08:51:41 -0800 Subject: [PATCH 5/5] code cleanup, add comments --- src/ast/sls/sls_bv_lookahead.cpp | 156 +++++++++++++++++++------------ src/ast/sls/sls_bv_lookahead.h | 2 +- 2 files changed, 96 insertions(+), 62 deletions(-) diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 13e0146e6..0285a5a3e 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -33,11 +33,23 @@ namespace sls { m(ev.m) { } + /** + * Main entry point. The lookahead solver is invoked periodically + * before any other propagation with the main BV solver. + */ void bv_lookahead::start_propagation() { if (m_stats.m_num_propagations++ % m_config.propagation_base == 0) search(); } + /** + * Main search loop. + * - Selects candidate variables + * - Applies random moves with a small probability + * - Applies guided moves to reduce cost of false literals + * - Applies random updates if no progress is made + */ + void bv_lookahead::search() { updt_params(ctx.get_params()); rescore(); @@ -53,36 +65,87 @@ namespace sls { if (vars.empty()) return; - // random walk with probability 1024/wp + // random walk if (ctx.rand(2047) < m_config.wp && apply_random_move(vars)) continue; + // guided moves, greedily reducing cost of false literals if (apply_guided_move(vars)) continue; + // bail out if no progress, and try random update if (apply_random_update(get_candidate_uninterp())) recalibrate_weights(); } m_config.max_moves_base += 100; } + /** + * guided move: apply lookahead search for the selected variables + * and possible moves + */ bool bv_lookahead::apply_guided_move(ptr_vector const& vars) { m_best_expr = nullptr; m_best_score = m_top_score; unsigned sz = vars.size(); - unsigned start = ctx.rand(sz); + unsigned start = ctx.rand(); for (unsigned i = 0; i < sz; ++i) add_updates(vars[(start + i) % sz]); - TRACE("bv", tout << "guided update " << m_best_score << " " << (m_best_expr?"no update":"") << "\n";); + CTRACE("bv", !m_best_expr, tout << "no guided move\n";); if (!m_best_expr) return false; - apply_update(m_best_expr, m_best_value); - //verbose_stream() << "increasing move " << mk_bounded_pp(m_best_expr, m) - // << " := " << m_best_value << " score: " << m_top_score << "\n"; + apply_update(m_best_expr, m_best_value, "increasing move"); return true; } + /** + * random update: select a variable at random and set bits to random values + */ + bool bv_lookahead::apply_random_update(ptr_vector const& vars) { + expr* e = vars[ctx.rand(vars.size())]; + auto& v = wval(e); + m_v_updated.set_bw(v.bw); + v.get_variant(m_v_updated, m_ev.m_rand); + if (!v.can_set(m_v_updated)) + return false; + apply_update(e, m_v_updated, "random update"); + return true; + } + + /** + * random move: select a variable at random and use one of the moves: flip, add1, sub1 + */ + bool bv_lookahead::apply_random_move(ptr_vector const& vars) { + expr* e = vars[ctx.rand(vars.size())]; + auto& v = wval(e); + m_v_updated.set_bw(v.bw); + v.bits().copy_to(v.nw, m_v_updated); + switch (ctx.rand(3)) { + case 0: { + // flip a random bit + auto bit = ctx.rand(v.bw); + m_v_updated.set(bit, !m_v_updated.get(bit)); + break; + } + case 1: + v.add1(m_v_updated); + break; + default: + v.sub1(m_v_updated); + break; + } + + if (!v.can_set(m_v_updated)) + return false; + apply_update(e, m_v_updated, "random move"); + return true; + } + + /** + * Retrieve a candidate top-level predicate that is false, give preference to + * those with high score, but back off if they are frequently chosen. + */ ptr_vector const& bv_lookahead::get_candidate_uninterp() { auto const& lits = ctx.root_literals(); app* e = nullptr; @@ -93,8 +156,8 @@ namespace sls { continue; auto a = to_app(ctx.atom(lit.var())); auto score = old_score(a); - auto q = score - + m_config.ucb_constant * sqrt(log((double)m_touched) / get_touched(a)) + auto q = score + + m_config.ucb_constant * sqrt(log((double)m_touched) / get_touched(a)) + m_config.ucb_noise * ctx.rand(512); if (q > max) max = q, e = a; @@ -121,47 +184,6 @@ namespace sls { return vars; } - bool bv_lookahead::apply_random_update(ptr_vector const& vars) { - expr* e = vars[ctx.rand(vars.size())]; - auto& v = wval(e); - m_v_updated.set_bw(v.bw); - v.get_variant(m_v_updated, m_ev.m_rand); - if (!v.can_set(m_v_updated)) - return false; - apply_update(e, m_v_updated); - - //verbose_stream() << "random update " << mk_bounded_pp(e, m) << " := " << m_v_updated << " score " << m_top_score << "\n"; - return true; - } - - bool bv_lookahead::apply_random_move(ptr_vector const& vars) { - expr* e = vars[ctx.rand(vars.size())]; - auto& v = wval(e); - m_v_updated.set_bw(v.bw); - v.bits().copy_to(v.nw, m_v_updated); - switch (ctx.rand(3)) { - case 0: { - // flip a random bit - auto bit = ctx.rand(v.bw); - m_v_updated.set(bit, !m_v_updated.get(bit)); - break; - } - case 1: - v.add1(m_v_updated); - break; - default: - v.sub1(m_v_updated); - break; - } - - if (!v.can_set(m_v_updated)) - return false; - apply_update(e, m_v_updated); - TRACE("bv", tout << "random move " << mk_bounded_pp(e, m) << " := " << m_v_updated << "\n";); - // verbose_stream() << "random move " << mk_bounded_pp(e, m) << " := " << m_v_updated << " score " << m_top_score << "\n"; - return true; - } - void bv_lookahead::check_restart() { if (m_stats.m_moves % m_config.restart_base == 0) { @@ -183,6 +205,9 @@ namespace sls { rescore(); } + /** + * Reset variables that occur in false literals. + */ void bv_lookahead::reset_uninterp_in_false_literals() { auto const& lits = ctx.root_literals(); expr_mark marked; @@ -199,7 +224,7 @@ namespace sls { m_v_updated.set_bw(v.bw); m_v_updated.set_zero(); if (v.can_set(m_v_updated)) { - apply_update(e, m_v_updated); + apply_update(e, m_v_updated, "reset"); } } } @@ -225,7 +250,6 @@ namespace sls { void bv_lookahead::updt_params(params_ref const& _p) { sls_params p(_p); - m_config.walksat = p.walksat(); m_config.walksat_repick = p.walksat_repick(); m_config.paws_sp = p.paws_sp(); @@ -236,18 +260,21 @@ namespace sls { m_config.restart_init = p.restart_init(); m_config.early_prune = p.early_prune(); m_config.ucb = p.walksat_ucb(); - m_config.ucb_constant = p.walksat_ucb_constant(); m_config.ucb_forget = p.walksat_ucb_forget(); m_config.ucb_init = p.walksat_ucb_init(); m_config.ucb_noise = p.walksat_ucb_noise(); } + /** + * Score of a predicate based on how close the current + * solution is to satisfying it. The proximity measure is + * based on hamming distance for equalities, and differences + * for inequalities. + */ double bv_lookahead::new_score(app* a) { bool is_true = ctx.is_true(a); bool is_true_new = m_ev.bval1(a); - if (!ctx.is_relevant(a)) - return 0; if (is_true == is_true_new) return 1; expr* x, * y; @@ -327,6 +354,10 @@ namespace sls { return 0; } + /** + * Rehearse an update. The update is revered while a score is computed and returned. + * Walk all parents, until hitting predicates where their scores are computed. + */ double bv_lookahead::lookahead_update(expr* e, bvect const& new_value) { SASSERT(bv.is_bv(e)); SASSERT(is_uninterp(e)); @@ -441,16 +472,18 @@ namespace sls { try_set(u, m_v_updated); } - void bv_lookahead::apply_update(expr* e, bvect const& new_value) { - TRACE("bv", tout << "apply " << mk_bounded_pp(e, m) << " new value " << new_value << "\n"); + /** + * Apply an update to a variable. + * The update is committed. + */ + + void bv_lookahead::apply_update(expr* e, bvect const& new_value, char const* reason) { SASSERT(bv.is_bv(e)); SASSERT(is_uninterp(e)); SASSERT(m_restore.empty()); wval(e).eval = new_value; double old_top_score = m_top_score; - //verbose_stream() << mk_bounded_pp(e, m) << " := " << new_value << "\n"; - VERIFY(wval(e).commit_eval()); insert_update_stack(e); unsigned max_depth = get_depth(e); @@ -461,7 +494,7 @@ namespace sls { m_ev.eval(e); // updates wval(e).eval if (!wval(e).commit_eval()) { TRACE("bv", tout << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); - IF_VERBOSE(0, verbose_stream() << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); + IF_VERBOSE(2, verbose_stream() << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); // bv_plugin::is_sat picks up discrepancies continue; } @@ -484,8 +517,9 @@ namespace sls { m_update_stack[depth].reset(); } m_in_update_stack.reset(); - TRACE("bv", tout << mk_bounded_pp(e, m) << " := " - << new_value << " " << m_top_score << " (" << old_top_score << ")\n"); + TRACE("bv", tout << reason << " " << mk_bounded_pp(m_best_expr, m) + << " := " << new_value + << " score " << m_top_score << "\n";); } bool bv_lookahead::insert_update(expr* e) { diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h index bc34800e4..798ed5ac6 100644 --- a/src/ast/sls/sls_bv_lookahead.h +++ b/src/ast/sls/sls_bv_lookahead.h @@ -108,7 +108,7 @@ namespace sls { void try_set(expr* u, bvect const& new_value); void add_updates(expr* u); - void apply_update(expr* e, bvect const& new_value); + void apply_update(expr* e, bvect const& new_value, char const* reason); bool apply_random_move(ptr_vector const& vars); bool apply_guided_move(ptr_vector const& vars); bool apply_random_update(ptr_vector const& vars);