From 05f166f736476e628909829e0d5e1da242223d15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Jan 2025 13:40:49 -0800 Subject: [PATCH] add py_value to selected classes in python bindings, add mode for input-assertion based lookahead solving --- src/api/api_parsers.cpp | 2 +- src/api/python/z3/z3.py | 20 ++ src/ast/ast.h | 10 +- src/ast/datatype_decl_plugin.h | 2 +- src/ast/sls/sls_array_plugin.cpp | 8 +- src/ast/sls/sls_basic_plugin.cpp | 8 +- src/ast/sls/sls_bv_eval.cpp | 59 +++--- src/ast/sls/sls_bv_eval.h | 14 +- src/ast/sls/sls_bv_lookahead.cpp | 313 ++++++++++++++++++++----------- src/ast/sls/sls_bv_lookahead.h | 59 +++++- src/ast/sls/sls_bv_terms.cpp | 2 - src/ast/sls/sls_bv_valuation.cpp | 2 + src/ast/sls/sls_context.cpp | 34 +++- src/ast/sls/sls_context.h | 8 +- src/ast/sls/sls_smt_solver.cpp | 4 +- src/params/sls_params.pyg | 2 + src/tactic/sls/sls_tactic.cpp | 9 +- src/util/obj_hashtable.h | 2 +- 18 files changed, 374 insertions(+), 184 deletions(-) diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 8f6c76958..94c882ec8 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -263,7 +263,7 @@ extern "C" { if (ous.str().empty()) ous << e.what(); SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str()); } - Z3_CATCH_CORE(); + Z3_CATCH_CORE({}); RETURN_Z3(mk_c(c)->mk_external_string(std::move(ous).str())); } } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index ccdd719a5..5d8dc6649 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -447,6 +447,10 @@ class AstRef(Z3PPObject): """ return Z3_get_ast_hash(self.ctx_ref(), self.as_ast()) + def py_value(self): + """Return a Python value that is equivalent to `self`.""" + return None + def is_ast(a): """Return `True` if `a` is an AST node. @@ -1611,6 +1615,13 @@ class BoolRef(ExprRef): def __invert__(self): return Not(self) + + def py_value(self): + if is_true(self): + return True + if is_false(self): + return False + return None @@ -3045,6 +3056,9 @@ class IntNumRef(ArithRef): """ return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast()) + def py_value(self): + return Z3_get_numeral_double(self.ctx_ref(), self.as_ast()) + class RatNumRef(ArithRef): """Rational values.""" @@ -3142,6 +3156,9 @@ class RatNumRef(ArithRef): """ return Fraction(self.numerator_as_long(), self.denominator_as_long()) + def py_value(self): + return Z3_get_numeral_double(self.ctx_ref(), self.as_ast()) + class AlgebraicNumRef(ArithRef): """Algebraic irrational values.""" @@ -11005,6 +11022,9 @@ class SeqRef(ExprRef): return string_at(chars, size=string_length.value).decode("latin-1") return Z3_ast_to_string(self.ctx_ref(), self.as_ast()) + def py_value(self): + return self.as_string() + def __le__(self, other): return _to_expr_ref(Z3_mk_str_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx) diff --git a/src/ast/ast.h b/src/ast/ast.h index 053390022..039be4130 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -150,7 +150,7 @@ public: ~parameter(); - parameter& operator=(parameter && other) { + parameter& operator=(parameter && other) noexcept { std::swap(other.m_val, m_val); return *this; } @@ -460,7 +460,7 @@ class ast { protected: friend class ast_manager; - unsigned m_id; + unsigned m_id = UINT_MAX; unsigned m_kind:16; // Warning: the marks should be used carefully, since they are shared. unsigned m_mark1:1; @@ -479,8 +479,8 @@ protected: void mark_so(bool flag) { m_mark_shared_occs = flag; } void reset_mark_so() { m_mark_shared_occs = false; } bool is_marked_so() const { return m_mark_shared_occs; } - unsigned m_ref_count; - unsigned m_hash; + unsigned m_ref_count = 0; + unsigned m_hash = 0; #ifdef Z3DEBUG // In debug mode, we store who is the owner of the mark. void * m_mark1_owner; @@ -497,7 +497,7 @@ protected: --m_ref_count; } - ast(ast_kind k):m_id(UINT_MAX), m_kind(k), m_mark1(false), m_mark2(false), m_mark_shared_occs(false), m_ref_count(0) { + ast(ast_kind k): m_kind(k), m_mark1(false), m_mark2(false), m_mark_shared_occs(false) { DEBUG_CODE({ m_mark1_owner = 0; m_mark2_owner = 0; diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 48033d129..4d91cbf40 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -81,7 +81,7 @@ namespace datatype { symbol m_name; symbol m_recognizer; ptr_vector m_accessors; - def* m_def; + def* m_def = nullptr; public: constructor(symbol n, symbol const& r): m_name(n), m_recognizer(r) {} ~constructor(); diff --git a/src/ast/sls/sls_array_plugin.cpp b/src/ast/sls/sls_array_plugin.cpp index 80681d718..9aa7ea639 100644 --- a/src/ast/sls/sls_array_plugin.cpp +++ b/src/ast/sls/sls_array_plugin.cpp @@ -111,7 +111,7 @@ namespace sls { return; if (are_distinct(nsel, nmap)) { expr_ref eq(m.mk_eq(nmap->get_expr(), nsel->get_expr()), m); - ctx.add_clause(eq); + ctx.add_theory_axiom(eq); } else { g.merge(nmap, nsel, nullptr); @@ -192,7 +192,7 @@ namespace sls { auto nsel = mk_select(g, cn, sel); if (are_distinct(nsel, sel)) { expr_ref eq(m.mk_eq(val->get_expr(), nsel->get_expr()), m); - ctx.add_clause(eq); + ctx.add_theory_axiom(eq); } else { g.merge(nsel, sel, nullptr); @@ -227,7 +227,7 @@ namespace sls { expr_ref sel(a.mk_select(args), m); expr_ref eq(m.mk_eq(sel, to_app(sto)->get_arg(sto->get_num_args() - 1)), m); IF_VERBOSE(3, verbose_stream() << "add store axiom 1 " << mk_bounded_pp(sto, m) << "\n"); - ctx.add_clause(eq); + ctx.add_theory_axiom(eq); } void array_plugin::add_store_axiom2(app* sto, app* sel) { @@ -248,7 +248,7 @@ namespace sls { for (unsigned i = 1; i < sel->get_num_args() - 1; ++i) ors.push_back(m.mk_eq(sel->get_arg(i), sto->get_arg(i))); IF_VERBOSE(3, verbose_stream() << "add store axiom 2 " << mk_bounded_pp(sto, m) << " " << mk_bounded_pp(sel, m) << "\n"); - ctx.add_clause(m.mk_or(ors)); + ctx.add_theory_axiom(m.mk_or(ors)); } void array_plugin::init_egraph(euf::egraph& g) { diff --git a/src/ast/sls/sls_basic_plugin.cpp b/src/ast/sls/sls_basic_plugin.cpp index 7c8ab0fb8..aca1e646b 100644 --- a/src/ast/sls/sls_basic_plugin.cpp +++ b/src/ast/sls/sls_basic_plugin.cpp @@ -47,13 +47,13 @@ namespace sls { auto eq_th = expr_ref(m.mk_eq(e, th), m); auto eq_el = expr_ref(m.mk_eq(e, el), m); - ctx.add_clause(m.mk_or(mk_not(m, c), eq_th)); - ctx.add_clause(m.mk_or(c, eq_el)); + ctx.add_theory_axiom(m.mk_or(mk_not(m, c), eq_th)); + ctx.add_theory_axiom(m.mk_or(c, eq_el)); #if 0 auto eq_th_el = expr_ref(m.mk_eq(th, el), m); verbose_stream() << mk_bounded_pp(eq_th_el, m) << "\n"; - ctx.add_clause(m.mk_or(eq_th_el, c, m.mk_not(eq_th))); - ctx.add_clause(m.mk_or(eq_th_el, m.mk_not(c), m.mk_not(eq_el))); + ctx.add_theory_axiom(m.mk_or(eq_th_el, c, m.mk_not(eq_th))); + ctx.add_theory_axiom(m.mk_or(eq_th_el, m.mk_not(c), m.mk_not(eq_el))); #endif } } diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp index 2d59b8c34..ee4291804 100644 --- a/src/ast/sls/sls_bv_eval.cpp +++ b/src/ast/sls/sls_bv_eval.cpp @@ -97,8 +97,11 @@ namespace sls { eval(e).commit_eval_check_tabu(); } - bool bv_eval::can_eval1(app* e) const { + bool bv_eval::can_eval1(expr* t) const { expr* x, * y; + if (!is_app(t)) + return false; + app* e = to_app(t); if (m.is_eq(e, x, y)) return bv.is_bv(x); if (m.is_ite(e)) @@ -197,27 +200,35 @@ namespace sls { } void bv_eval::set_bool_value(expr* e, bool val) { - m_tmp_bool_values.setx(e->get_id(), to_lbool(val), l_undef); - m_tmp_bool_value_indices.push_back(e->get_id()); + auto id = e->get_id(); + auto old_val = m_tmp_bool_values.get(id, l_undef); + m_tmp_bool_values.setx(id, to_lbool(val), l_undef); + m_tmp_bool_value_updates.push_back({ id, old_val }); } bool bv_eval::get_bool_value(expr* e) const { - auto val = m_tmp_bool_values.get(e->get_id(), l_undef); + SASSERT(m.is_bool(e)); + auto id = e->get_id(); + auto val = m_tmp_bool_values.get(id, l_undef); if (val != l_undef) - return val == l_true; + return val == l_true; + bool b; auto v = ctx.atom2bool_var(e); if (v != sat::null_bool_var) - return ctx.is_true(v); - auto b = bval1_bool(to_app(e)); - m_tmp_bool_values.setx(e->get_id(), to_lbool(val), l_undef); - m_tmp_bool_value_indices.push_back(e->get_id()); + b = ctx.is_true(v); + else + b = bval1(e); + m_tmp_bool_values.setx(id, to_lbool(b), l_undef); + m_tmp_bool_value_updates.push_back({ id, l_undef }); return b; } - void bv_eval::clear_bool_values() { - for (auto i : m_tmp_bool_value_indices) - m_tmp_bool_values[i] = l_undef; - m_tmp_bool_value_indices.reset(); + void bv_eval::restore_bool_values(unsigned r) { + for (auto i = m_tmp_bool_value_updates.size(); i-- > r; ) { + auto& [id, val] = m_tmp_bool_value_updates[i]; + m_tmp_bool_values.set(id, val); + } + m_tmp_bool_value_updates.shrink(r); } bool bv_eval::bval1_bool(app* e) const { @@ -261,23 +272,18 @@ namespace sls { return false; } - bool bv_eval::bval1(app* e) const { + bool bv_eval::bval1(expr* t) const { + app* e = to_app(t); if (e->get_family_id() == bv.get_fid()) return bval1_bv(e); expr* x, * y; - if (m.is_eq(e, x, y) && bv.is_bv(x)) { - return wval(x).bits() == wval(y).bits(); - } + if (m.is_eq(e, x, y) && bv.is_bv(x)) + return wval(x).bits() == wval(y).bits(); if (e->get_family_id() == basic_family_id) return bval1_bool(e); - - verbose_stream() << mk_bounded_pp(e, m) << "\n"; - UNREACHABLE(); - return false; + return ctx.is_true(e); } - // unsigned ddt_orig(expr* e); - sls::bv_valuation& bv_eval::eval(app* e) const { SASSERT(m_values.size() > e->get_id()); SASSERT(m_values[e->get_id()]); @@ -290,7 +296,8 @@ namespace sls { m_values[e->get_id()]->set(val.bits()); } - void bv_eval::eval(app* e, sls::bv_valuation& val) const { + void bv_eval::eval(expr* t, sls::bv_valuation& val) const { + app* e = to_app(t); SASSERT(bv.is_bv(e)); if (m.is_ite(e)) { SASSERT(bv.is_bv(e->get_arg(1))); @@ -2056,11 +2063,11 @@ namespace sls { } bool bv_eval::repair_up(expr* e) { - if (!is_app(e) || !can_eval1(to_app(e))) + if (!can_eval1(e)) return false; if (m.is_bool(e)) { - bool b = bval1(to_app(e)); + bool b = bval1(e); auto v = ctx.atom2bool_var(e); if (v == sat::null_bool_var) ctx.set_value(e, b ? m.mk_true() : m.mk_false()); diff --git a/src/ast/sls/sls_bv_eval.h b/src/ast/sls/sls_bv_eval.h index ef016c7d5..52de4be93 100644 --- a/src/ast/sls/sls_bv_eval.h +++ b/src/ast/sls/sls_bv_eval.h @@ -55,7 +55,7 @@ namespace sls { unsigned m_lookahead_steps = 0; unsigned m_lookahead_phase_size = 10; mutable svector m_tmp_bool_values; - mutable unsigned_vector m_tmp_bool_value_indices; + mutable svector> m_tmp_bool_value_updates; scoped_ptr_vector m_values; // expr-id -> bv valuation @@ -141,7 +141,7 @@ namespace sls { sls::bv_valuation& wval(app* e, unsigned i) { return wval(e->get_arg(i)); } - void eval(app* e, sls::bv_valuation& val) const; + void eval(expr* e, sls::bv_valuation& val) const; bvect const& assign_value(app* e) const { return wval(e).bits(); } @@ -150,7 +150,7 @@ namespace sls { * Retrieve evaluation based on immediate children. */ - bool can_eval1(app* e) const; + bool can_eval1(expr* e) const; void commit_eval(expr* p, app* e); @@ -188,11 +188,13 @@ namespace sls { expr_ref get_value(app* e); bool bval0(expr* e) const { return ctx.is_true(e); } - bool bval1(app* e) const; + bool bval1(expr* e) const; + unsigned bool_value_restore_point() const { return m_tmp_bool_value_updates.size(); } void set_bool_value(expr* e, bool val); - void clear_bool_values(); - bool get_bool_value(expr* e)const; + void restore_bool_values(unsigned restore_point); + void commit_bool_values() { m_tmp_bool_value_updates.reset(); } + bool get_bool_value(expr* e) const; /* * Try to invert value of child to repair value assignment of parent. diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 1bdc5f260..2e9c1949a 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -38,7 +38,6 @@ namespace sls { * before any other propagation with the main BV solver. */ void bv_lookahead::start_propagation() { - //verbose_stream() << "start_propagation " << m_stats.m_num_propagations << "\n"; if (m_stats.m_propagations++ % m_config.propagation_base == 0) search(); } @@ -53,6 +52,7 @@ namespace sls { void bv_lookahead::search() { updt_params(ctx.get_params()); + initialize_bool_values(); rescore(); m_config.max_moves = m_stats.m_moves + m_config.max_moves_base; TRACE("bv", tout << "search " << m_stats.m_moves << " " << m_config.max_moves << "\n";); @@ -65,8 +65,10 @@ namespace sls { // get candidate variables auto& vars = get_candidate_uninterp(); - if (vars.empty()) - return; + if (vars.empty()) { + finalize_bool_values(); + return; + } // random walk if (ctx.rand(2047) < m_config.wp && apply_random_move(vars)) @@ -83,6 +85,36 @@ namespace sls { m_config.max_moves_base += 100; } + void bv_lookahead::initialize_bool_values() { + for (auto t : ctx.subterms()) { + if (bv.is_bv(t)) { + auto& v = m_ev.eval(to_app(t)); + v.commit_eval_ignore_tabu(); + } + else if (m.is_bool(t)) { + auto b = m_ev.bval1(t); + m_ev.set_bool_value(t, b); + } + } + m_ev.commit_bool_values(); + } + + + /** + * 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()); + } + } + /** * guided move: apply lookahead search for the selected variables * and possible moves @@ -106,11 +138,14 @@ namespace sls { return false; expr* e = vars[ctx.rand(vars.size())]; if (m.is_bool(e)) { - auto v = ctx.atom2bool_var(e); - if (ctx.is_unit(v)) - return false ; - TRACE("bv", tout << "random flip " << mk_bounded_pp(e, m) << "\n";); - ctx.flip(v); + if (is_root(e)) + return false; + m_ev.set_bool_value(e, !m_ev.get_bool_value(e)); + if (!m_config.use_top_level_assertions) { + auto v = ctx.atom2bool_var(e); + TRACE("bv", tout << "random flip " << mk_bounded_pp(e, m) << "\n";); + ctx.flip(v); + } return true; } SASSERT(bv.is_bv(e)); @@ -121,6 +156,7 @@ namespace sls { return apply_update(m_last_atom, e, m_v_updated, move_type::random_t); } + /** * random move: select a variable at random and use one of the moves: flip, add1, sub1 */ @@ -129,11 +165,16 @@ namespace sls { return false; expr* e = vars[ctx.rand(vars.size())]; if (m.is_bool(e)) { - TRACE("bv", tout << "random move flip " << mk_bounded_pp(e, m) << "\n";); - auto v = ctx.atom2bool_var(e); - if (ctx.is_unit(v)) + if (is_root(e)) return false; - ctx.flip(v); + m_ev.set_bool_value(e, !m_ev.get_bool_value(e)); + if (!m_config.use_top_level_assertions) { + TRACE("bv", tout << "random move flip " << mk_bounded_pp(e, m) << "\n";); + auto v = ctx.atom2bool_var(e); + if (ctx.is_unit(v)) + return false; + ctx.flip(v); + } return true; } SASSERT(bv.is_bv(e)); @@ -162,13 +203,17 @@ namespace sls { * those with high score, but back off if they are frequently chosen. */ ptr_vector const& bv_lookahead::get_candidate_uninterp() { - app* e = nullptr; + expr* e = nullptr; if (m_config.ucb) { double max = -1.0; - for (auto lit : ctx.root_literals()) { - if (!is_false_bv_literal(lit)) + 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"; + if (assertion_is_true(a)) + continue; + + if (vars.empty()) 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)) @@ -183,9 +228,9 @@ namespace sls { } else { unsigned n = 0; - for (auto lit : ctx.root_literals()) - if (is_false_bv_literal(lit) && ctx.rand() % ++n == 0) - e = to_app(ctx.atom(lit.var())); + for (auto a : get_root_assertions()) + if (!assertion_is_true(a) && !m_ev.terms.uninterp_occurs(e).empty() && ctx.rand() % ++n == 0) + e = a; } CTRACE("bv", !e, ; display_weights(ctx.display(tout << "no candidate\n"));); @@ -228,12 +273,10 @@ namespace sls { * Reset variables that occur in false literals. */ void bv_lookahead::reset_uninterp_in_false_literals() { - auto const& lits = ctx.root_literals(); expr_mark marked; - for (auto lit : ctx.root_literals()) { - if (!is_false_bv_literal(lit)) + for (auto a : get_root_assertions()) { + if (assertion_is_true(a)) continue; - app* a = to_app(ctx.atom(lit.var())); auto const& occs = m_ev.terms.uninterp_occurs(a); for (auto e : occs) { if (!bv.is_bv(e)) @@ -259,13 +302,11 @@ namespace sls { return m_ev.can_eval1(a); } - bool bv_lookahead::is_false_bv_literal(sat::literal lit) { - if (!is_bv_literal(lit)) - return false; - app* a = to_app(ctx.atom(lit.var())); - return m_ev.bval0(a) != m_ev.bval1(a); + bool bv_lookahead::assertion_is_true(expr* a) { + if (m_config.use_top_level_assertions) + return m_ev.get_bool_value(a); + return !m_ev.can_eval1(a) || m_ev.bval0(a) == m_ev.bval1(a); } - void bv_lookahead::updt_params(params_ref const& _p) { sls_params p(_p); @@ -286,6 +327,7 @@ namespace sls { m_config.ucb_forget = p.walksat_ucb_forget(); m_config.ucb_init = p.walksat_ucb_init(); m_config.ucb_noise = p.walksat_ucb_noise(); + m_config.use_top_level_assertions = p.use_top_level_assertions_bv(); } /** @@ -294,12 +336,40 @@ namespace sls { * based on hamming distance for equalities, and differences * for inequalities. */ - double bv_lookahead::new_score(app* a) { - bool is_true = m_ev.get_bool_value(a); - bool is_true_new = m_ev.bval1(a); + double bv_lookahead::new_score(expr* a) { + if (m_config.use_top_level_assertions) + return new_score(a, true); + else + return new_score(a, m_ev.bval0(a)); + } + + double bv_lookahead::new_score(expr* a, bool is_true) { + bool is_true_new = m_ev.get_bool_value(a); + + //verbose_stream() << "compute score " << mk_bounded_pp(a, m) << " is-true " << is_true << " is-true-new " << is_true_new << "\n"; if (is_true == is_true_new) return 1; expr* x, * y; + if (m.is_not(a, x)) + return new_score(x, !is_true); + if ((m.is_and(a) && is_true) || (m.is_or(a) && !is_true)) { + double score = 1; + for (auto arg : *to_app(a)) + score = std::min(score, new_score(arg, is_true)); + return score; + } + if ((m.is_and(a) && !is_true) || (m.is_or(a) && is_true)) { + double score = 0; + for (auto arg : *to_app(a)) + score = std::max(score, new_score(arg, is_true)); + return score; + } + if (m.is_iff(a, x, y)) { + auto v0 = m_ev.get_bool_value(x); + auto v1 = m_ev.get_bool_value(y); + return (is_true == (v0 == v1)) ? 1 : 0; + } + if (is_true && m.is_eq(a, x, y) && bv.is_bv(x)) { auto const& vx = wval(x); auto const& vy = wval(y); @@ -359,13 +429,13 @@ namespace sls { double dbl = n.get_double(); 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(a->get_arg(0))) { + else if (is_true && m.is_distinct(a) && bv.is_bv(to_app(a)->get_arg(0))) { double np = 0, nd = 0; - for (unsigned i = 0; i < a->get_num_args(); ++i) { - auto const& vi = wval(a->get_arg(i)); - for (unsigned j = i + 1; j < a->get_num_args(); ++j) { + for (unsigned i = 0; i < to_app(a)->get_num_args(); ++i) { + auto const& vi = wval(to_app(a)->get_arg(i)); + for (unsigned j = i + 1; j < to_app(a)->get_num_args(); ++j) { ++np; - auto const& vj = wval(a->get_arg(j)); + auto const& vj = wval(to_app(a)->get_arg(j)); if (vi.bits() != vj.bits()) nd++; } @@ -403,31 +473,35 @@ namespace sls { m_ev.set_bool_value(t, !m_ev.bval0(t)); } + TRACE("bv_verbose", tout << "lookahead update " << mk_bounded_pp(t, m) << " := " << new_value << "\n";); + insert_update_stack(t); + unsigned restore_point = m_ev.bool_value_restore_point(); unsigned max_depth = get_depth(t); for (unsigned depth = max_depth; depth <= max_depth; ++depth) { for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) { auto a = m_update_stack[depth][i]; - TRACE("bv_verbose", tout << "update " << mk_bounded_pp(a, m) << " " << depth << " " << i << "\n";); + TRACE("bv_verbose", tout << "update " << mk_bounded_pp(a, m) << " depth: " << depth << "\n";); for (auto p : ctx.parents(a)) { insert_update_stack(p); max_depth = std::max(max_depth, get_depth(p)); } - if (is_root(a)) - score += get_weight(a) * (new_score(a) - old_score(a)); - - if (a == t) - continue; - else if (bv.is_bv(a)) - m_ev.eval(a); - - insert_update(a); + + if (t != a) { + if (bv.is_bv(a)) + m_ev.eval(a); + insert_update(a); + } + if (is_root(a)) { + TRACE("bv_verbose", tout << "scores " << mk_bounded_pp(a, m) << " old: " << old_score(a) << " new: " << new_score(a) << "\n";); + score += get_weight(a) * (new_score(a) - old_score(a)); + } } m_update_stack[depth].reset(); } m_in_update_stack.reset(); restore_lookahead(); - m_ev.clear_bool_values(); + m_ev.restore_bool_values(restore_point); TRACE("sls_verbose", tout << mk_bounded_pp(t, m) << " := " << new_value << " score: " << m_top_score << "\n"); @@ -481,7 +555,7 @@ namespace sls { m_v_saved.copy_to(v.nw, m_v_updated); // flip a single bit - for (unsigned i = 0; i < v.bw && i <= 32; ++i) { + for (unsigned i = 0; i < v.bw && i < 32 ; ++i) { m_v_updated.set(i, !m_v_updated.get(i)); try_set(u, m_v_updated); m_v_updated.set(i, !m_v_updated.get(i)); @@ -543,6 +617,7 @@ namespace sls { insert_update_stack(t); unsigned max_depth = get_depth(t); + unsigned restore_point = m_ev.bool_value_restore_point(); for (unsigned depth = max_depth; depth <= max_depth; ++depth) { for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) { auto e = m_update_stack[depth][i]; @@ -558,49 +633,43 @@ namespace sls { wval(e).commit_eval_ignore_tabu(); } else if (m.is_bool(e)) { - auto v = ctx.atom2bool_var(e); - auto v1 = m_ev.bval1(to_app(e)); - if (v != sat::null_bool_var) { - if (ctx.is_unit(v)) - continue; - if (ctx.is_true(v) == v1) - continue; + auto v1 = m_ev.bval1(e); + + if (m_config.use_top_level_assertions) { + if (m_ev.get_bool_value(e) == v1) + continue; + } + else { if (e == p) continue; - TRACE("bv", tout << "updated truth value " << v << ": " << mk_bounded_pp(e, m) << "\n";); - unsigned num_unsat = ctx.unsat().size(); -#if 0 - - TRACE("bv", tout << "update flip " << mk_bounded_pp(e, m) << "\n";); - auto r = ctx.reward(v); - auto lit = sat::literal(v, !ctx.is_true(v)); - bool is_bv_lit = is_bv_literal(lit); - - sat::bool_var_set rotated; - unsigned budget = 100; - bool rot = ctx.try_rotate(v, rotated, budget); - verbose_stream() << "try-rotate " << rot << " " << rotated.size() << "\n"; - verbose_stream() << "flip " << ((!p || e == p) ? "top " : "not top ") << is_bv_literal(lit) << " " << mk_bounded_pp(e, m) << " " << lit << " " << r << " num unsat " << num_unsat << " -> " << ctx.unsat().size() << "\n"; - verbose_stream() << "new unsat " << ctx.unsat().size() << "\n"; -#endif - + auto v = ctx.atom2bool_var(e); + + if (v != sat::null_bool_var) { + + if (ctx.is_unit(v)) + continue; + if (ctx.is_true(e) == v1) + continue; + + + TRACE("bv", tout << "updated truth value " << v << ": " << mk_bounded_pp(e, m) << "\n";); + unsigned num_unsat = ctx.unsat().size(); + #if 1 - if (allow_costly_flips(mt)) - ctx.flip(v); - else if (true) { - sat::bool_var_set rotated; - unsigned budget = 100; - bool rot = ctx.try_rotate(v, rotated, budget); - if (rot) - ++m_stats.m_rotations; - (void)rot; - TRACE("bv", tout << "rotate " << v << " " << rot << " " << rotated << "\n";); - //verbose_stream() << "rotate " << v << " " << rot << " " << rotated << "\n"; - } + if (allow_costly_flips(mt)) + ctx.flip(v); + else if (true) { + sat::bool_var_set rotated; + unsigned budget = 100; + bool rot = ctx.try_rotate(v, rotated, budget); + if (rot) + ++m_stats.m_rotations; + TRACE("bv", tout << "rotate " << v << " " << rot << " " << rotated << "\n";); + } #endif - + } } m_ev.set_bool_value(to_app(e), v1); } @@ -615,7 +684,10 @@ namespace sls { m_update_stack[depth].reset(); } m_in_update_stack.reset(); - m_ev.clear_bool_values(); + if (m_config.use_top_level_assertions) + m_ev.commit_bool_values(); + else + m_ev.restore_bool_values(restore_point); TRACE("bv", tout << mt << " " << mk_bounded_pp(t, m) << " := " << new_value << " score " << m_top_score << "\n";); @@ -631,7 +703,6 @@ namespace sls { } void bv_lookahead::insert_update(expr* e) { - TRACE("sls_verbose", tout << "insert update " << mk_bounded_pp(e, m) << "\n"); if (bv.is_bv(e)) { auto& v = wval(e); @@ -669,7 +740,8 @@ namespace sls { } bv_lookahead::bool_info& bv_lookahead::get_bool_info(expr* e) { - return m_bool_info.insert_if_not_there(e, { m_config.paws_init, 0, 1}); + m_bool_info.reserve(e->get_id() + 1, { m_config.paws_init, 0, 1 }); + return m_bool_info[e->get_id()]; } void bv_lookahead::dec_weight(expr* e) { @@ -680,29 +752,24 @@ namespace sls { void bv_lookahead::rescore() { m_top_score = 0; m_is_root.reset(); - for (auto lit : ctx.root_literals()) { - if (!is_bv_literal(lit)) - continue; - auto a = to_app(ctx.atom(lit.var())); + for (auto a : get_root_assertions()) { + m_is_root.mark(a); double score = new_score(a); set_score(a, score); m_top_score += score; - m_is_root.mark(a); + + //verbose_stream() << mk_bounded_pp(a, m) << " score: " << score << " assignment: " << m_ev.get_bool_value(a) << "\n"; } + //exit(0); } void bv_lookahead::recalibrate_weights() { - for (auto lit : ctx.root_literals()) { - if (!is_bv_literal(lit)) - continue; - auto a = to_app(ctx.atom(lit.var())); - bool is_true0 = m_ev.bval0(a); - bool is_true1 = m_ev.bval1(a); + for (auto a : get_root_assertions()) { if (ctx.rand(2047) < m_config.paws_sp) { - if (is_true0 == is_true1) + if (assertion_is_true(a)) dec_weight(a); } - else if (is_true0 != is_true1) + else if (!assertion_is_true(a)) inc_weight(a); } @@ -711,12 +778,9 @@ namespace sls { std::ostream& bv_lookahead::display_weights(std::ostream& out) { - for (auto lit : ctx.root_literals()) { - if (!is_bv_literal(lit)) - continue; - auto a = to_app(ctx.atom(lit.var())); - out << lit << ": " - << get_weight(a) << " " + for (auto a : get_root_assertions()) { + out << get_weight(a) << " " + << (assertion_is_true(a)?"T":"F") << " " << mk_bounded_pp(a, m) << " " << old_score(a) << " " << new_score(a) << "\n"; @@ -727,10 +791,7 @@ namespace sls { void bv_lookahead::ucb_forget() { if (m_config.ucb_forget >= 1.0) return; - for (auto lit : ctx.root_literals()) { - if (!is_bv_literal(lit)) - continue; - auto a = to_app(ctx.atom(lit.var())); + for (auto a : get_root_assertions()) { auto touched_old = get_touched(a); auto touched_new = static_cast((touched_old - 1) * m_config.ucb_forget + 1); set_touched(a, touched_new); @@ -744,4 +805,32 @@ namespace sls { st.update("sls-bv-restarts", m_stats.m_restarts); st.update("sls-bv-rotations", m_stats.m_rotations); } + + bv_lookahead::root_assertions::root_assertions(bv_lookahead& la, bool start) : m_la(la) { + if (start) { + idx = 0; + next(); + } + else if (m_la.m_config.use_top_level_assertions) + idx = m_la.ctx.input_assertions().size(); + else + idx = la.ctx.root_literals().size(); + } + + void bv_lookahead::root_assertions::next() { + if (m_la.m_config.use_top_level_assertions) + return; + + while (idx < m_la.ctx.root_literals().size() && !m_la.is_bv_literal(m_la.ctx.root_literals()[idx])) + ++idx; + } + + expr* bv_lookahead::root_assertions::operator*() const { + if (m_la.m_config.use_top_level_assertions) + return m_la.ctx.input_assertions().get(idx); + return m_la.ctx.atom(m_la.ctx.root_literals()[idx].var()); + }; + + + } \ No newline at end of file diff --git a/src/ast/sls/sls_bv_lookahead.h b/src/ast/sls/sls_bv_lookahead.h index c15558d6f..def61b9e7 100644 --- a/src/ast/sls/sls_bv_lookahead.h +++ b/src/ast/sls/sls_bv_lookahead.h @@ -46,6 +46,7 @@ namespace sls { double ucb_forget = 0.1; bool ucb_init = false; double ucb_noise = 0.1; + bool use_top_level_assertions = true; }; struct stats { @@ -78,7 +79,7 @@ namespace sls { expr* m_best_expr = nullptr; expr* m_last_atom = nullptr; ptr_vector m_empty_vars; - obj_map m_bool_info; + vector m_bool_info; expr_mark m_is_root; unsigned m_touched = 1; @@ -92,9 +93,10 @@ namespace sls { bool_info& get_bool_info(expr* e); double lookahead_update(expr* u, bvect const& new_value); - double old_score(app* c) { return get_bool_info(c).score; } - void set_score(app* c, double d) { get_bool_info(c).score = d; } - double new_score(app* c); + double old_score(expr* c) { return get_bool_info(c).score; } + void set_score(expr* c, double d) { get_bool_info(c).score = d; } + double new_score(expr* c, bool is_true); + double new_score(expr* c); double lookahead_flip(sat::bool_var v); @@ -107,9 +109,9 @@ namespace sls { bool is_root(expr* e) { return m_is_root.is_marked(e); } void ucb_forget(); - unsigned get_touched(app* e) { return get_bool_info(e).touched; } - void set_touched(app* e, unsigned t) { get_bool_info(e).touched = t; } - void inc_touched(app* e) { ++get_bool_info(e).touched; } + unsigned get_touched(expr* e) { return get_bool_info(e).touched; } + void set_touched(expr* e, unsigned t) { get_bool_info(e).touched = t; } + void inc_touched(expr* e) { ++get_bool_info(e).touched; } enum class move_type { random_t, guided_t, move_t, reset_t }; friend std::ostream& operator<<(std::ostream& out, move_type mt); @@ -128,10 +130,51 @@ namespace sls { void check_restart(); void reset_uninterp_in_false_literals(); bool is_bv_literal(sat::literal lit); - bool is_false_bv_literal(sat::literal lit); void search(); + class root_assertions { + bv_lookahead& m_la; + unsigned idx = 0; + void next(); + public: + root_assertions(bv_lookahead& la, bool start); + + expr* operator*() const; + + root_assertions& operator++() { + ++idx; + next(); + return *this; + } + + bool operator!=(root_assertions const& other) const { + return idx != other.idx; + } + + bool operator==(root_assertions const& other) const { + return idx == other.idx; + } + }; + class root_assertion_iterator { + bv_lookahead& m_la; + + public: + root_assertion_iterator(bv_lookahead& la) : m_la(la) {} + root_assertions begin() { return root_assertions(m_la, true); } + root_assertions end() { return root_assertions(m_la, false); } + }; + + root_assertion_iterator get_root_assertions() { + return root_assertion_iterator(*this); + } + + bool assertion_is_true(expr* a); + + void initialize_bool_values(); + + void finalize_bool_values(); + public: bv_lookahead(bv_eval& ev); diff --git a/src/ast/sls/sls_bv_terms.cpp b/src/ast/sls/sls_bv_terms.cpp index a46cd589a..0de754edd 100644 --- a/src/ast/sls/sls_bv_terms.cpp +++ b/src/ast/sls/sls_bv_terms.cpp @@ -135,8 +135,6 @@ namespace sls { } void bv_terms::register_uninterp(expr* e) { - if (!is_bv_predicate(e)) - return; m_uninterp_occurs.reserve(e->get_id() + 1); auto& occs = m_uninterp_occurs[e->get_id()]; ptr_vector todo; diff --git a/src/ast/sls/sls_bv_valuation.cpp b/src/ast/sls/sls_bv_valuation.cpp index 9630a9a66..0c9589445 100644 --- a/src/ast/sls/sls_bv_valuation.cpp +++ b/src/ast/sls/sls_bv_valuation.cpp @@ -32,6 +32,8 @@ namespace sls { } bool operator==(bvect const& a, bvect const& b) { + if (a.nw == 1) + return a[0] == b[0]; SASSERT(a.nw > 0); return 0 == memcmp(a.data(), b.data(), a.nw * sizeof(digit_t)); } diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index f67f056b6..e9481984f 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -35,7 +35,7 @@ namespace sls { } context::context(ast_manager& m, sat_solver_context& s) : - m(m), s(s), m_atoms(m), m_allterms(m), + m(m), s(s), m_atoms(m), m_input_assertions(m), m_allterms(m), m_gd(*this), m_ld(*this), m_repair_down(m.get_num_asts(), m_gd), @@ -330,20 +330,20 @@ namespace sls { return; m_constraint_ids.insert(e->get_id()); m_constraint_trail.push_back(e); - add_clause(e); + add_assertion(e, false); m_new_constraint = true; IF_VERBOSE(3, verbose_stream() << "add constraint " << mk_bounded_pp(e, m) << "\n"); ++m_stats.m_num_constraints; } - void context::add_clause(expr* f) { + void context::add_assertion(expr* f, bool is_input) { expr_ref _e(f, m); expr* g, * h, * k; sat::literal_vector clause; if (m.is_true(f)) return; if (m.is_not(f, g) && m.is_not(g, g)) { - add_clause(g); + add_assertion(g, is_input); return; } bool sign = m.is_not(f, f); @@ -352,15 +352,17 @@ namespace sls { for (auto arg : *to_app(f)) clause.push_back(mk_literal(arg)); s.add_clause(clause.size(), clause.data()); + if (is_input) + save_input_assertion(f, sign); } else if (!sign && m.is_and(f)) { for (auto arg : *to_app(f)) - add_clause(arg); + add_assertion(arg, is_input); } else if (sign && m.is_or(f)) { for (auto arg : *to_app(f)) { expr_ref fml(m.mk_not(arg), m); - add_clause(fml); + add_assertion(fml, is_input); } } else if (!sign && m.is_implies(f, g, h)) { @@ -368,17 +370,21 @@ namespace sls { clause.push_back(~mk_literal(g)); clause.push_back(mk_literal(h)); s.add_clause(clause.size(), clause.data()); + if (is_input) + save_input_assertion(f, sign); } else if (sign && m.is_implies(f, g, h)) { expr_ref fml(m.mk_not(h), m); - add_clause(fml); - add_clause(g); + add_assertion(fml, is_input); + add_assertion(g, is_input); } else if (sign && m.is_and(f)) { clause.reset(); for (auto arg : *to_app(f)) clause.push_back(~mk_literal(arg)); s.add_clause(clause.size(), clause.data()); + if (is_input) + save_input_assertion(f, sign); } else if (m.is_iff(f, g, h)) { auto lit1 = mk_literal(g); @@ -387,6 +393,8 @@ namespace sls { sat::literal cls2[2] = { sign ? ~lit1 : lit1, ~lit2 }; s.add_clause(2, cls1); s.add_clause(2, cls2); + if (is_input) + save_input_assertion(f, sign); } else if (m.is_ite(f, g, h, k)) { auto lit1 = mk_literal(g); @@ -399,15 +407,23 @@ namespace sls { sat::literal cls2[2] = { lit1, sign ? ~lit3 : lit3 }; s.add_clause(2, cls1); s.add_clause(2, cls2); + if (is_input) + save_input_assertion(f, sign); } else { sat::literal lit = mk_literal(f); if (sign) lit.neg(); s.add_clause(1, &lit); + if (is_input) + save_input_assertion(f, sign); } } + void context::save_input_assertion(expr* f, bool sign) { + m_input_assertions.push_back(sign ? m.mk_not(f) : f); + } + void context::add_clause(sat::literal_vector const& lits) { s.add_clause(lits.size(), lits.data()); m_new_constraint = true; @@ -511,6 +527,8 @@ namespace sls { for (unsigned i = 0; i < m_atoms.size(); ++i) if (m_atoms.get(i)) register_terms(m_atoms.get(i)); + for (auto e : m_input_assertions) + register_terms(e); for (auto p : m_plugins) if (p) p->initialize(); diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h index 975ce84bc..18d4d32f0 100644 --- a/src/ast/sls/sls_context.h +++ b/src/ast/sls/sls_context.h @@ -120,6 +120,7 @@ namespace sls { bool m_initialized = false; bool m_new_constraint = false; bool m_dirty = false; + expr_ref_vector m_input_assertions; expr_ref_vector m_allterms; ptr_vector m_subterms; greater_depth m_gd; @@ -137,6 +138,9 @@ namespace sls { void register_terms(expr* e); void register_term(expr* e); + void add_assertion(expr* f, bool is_input); + void save_input_assertion(expr* f, bool sign); + void propagate_boolean_assignment(); void propagate_literal(sat::literal lit); void repair_literals(); @@ -173,7 +177,8 @@ namespace sls { expr* term(unsigned id) const { return m_allterms.get(id); } sat::bool_var atom2bool_var(expr* e) const { return m_atom2bool_var.get(e->get_id(), sat::null_bool_var); } sat::literal mk_literal(expr* e); - void add_clause(expr* f); + void add_input_assertion(expr* f) { add_assertion(f, true); } + void add_theory_axiom(expr* f) { add_assertion(f, false); } void add_clause(sat::literal_vector const& lits); void flip(sat::bool_var v) { s.flip(v); } bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) { return s.try_rotate(v, rotated, budget); } @@ -183,6 +188,7 @@ namespace sls { unsigned rand(unsigned n) { return m_rand(n); } sat::literal_vector const& root_literals() const { return m_root_literals; } sat::literal_vector const& unit_literals() const { return m_unit_literals; } + expr_ref_vector const& input_assertions() const { return m_input_assertions; } bool is_unit(sat::literal lit) const { return is_unit(lit.var()); } bool is_unit(sat::bool_var v) const { return m_unit_indices.contains(v); } void reinit_relevant(); diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp index 90ba06f8c..6036b9172 100644 --- a/src/ast/sls/sls_smt_solver.cpp +++ b/src/ast/sls/sls_smt_solver.cpp @@ -92,7 +92,7 @@ namespace sls { unsigned num_vars() const override { return m_ddfw.num_vars(); } indexed_uint_set const& unsat() const override { return m_ddfw.unsat_set(); } sat::bool_var add_var() override { m_dirty = true; return m_ddfw.add_var(); } - void add_clause(expr* f) { m_context.add_clause(f); } + void add_input_assertion(expr* f) { m_context.add_input_assertion(f); } void force_restart() override { m_ddfw.force_restart(); } @@ -146,7 +146,7 @@ namespace sls { lbool smt_solver::check() { for (auto f : m_assertions) - m_solver_ctx->add_clause(f); + m_solver_ctx->add_input_assertion(f); IF_VERBOSE(10, m_solver_ctx->display(verbose_stream())); return m_ddfw.check(0, nullptr); } diff --git a/src/params/sls_params.pyg b/src/params/sls_params.pyg index 89aa9834f..75345379b 100644 --- a/src/params/sls_params.pyg +++ b/src/params/sls_params.pyg @@ -25,5 +25,7 @@ def_module_params('sls', ('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'), + ('use_top_level_assertions_bv', BOOL, False, 'use top-level assertions for BV lookahead solver'), + ('use_lookahead_bv', BOOL, True, 'use lookahead solver for BV'), ('str_update_strategy', UINT, 1, 'string update candidate selection: 0 - single character based update, 1 - subsequence based update') )) diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 59a5c6ac9..65b7025f7 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -131,9 +131,6 @@ public: } }; -tactic* mk_sls_smt_tactic(ast_manager& m, params_ref const& p) { - return alloc(sls_smt_tactic, m, p); -} class sls_tactic : public tactic { ast_manager & m; @@ -264,3 +261,9 @@ tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { return t; } + +tactic* mk_sls_smt_tactic(ast_manager& m, params_ref const& p) { + tactic* t = and_then(mk_preamble(m, p), alloc(sls_smt_tactic, m, p)); + t->updt_params(p); + return t; +} diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 2784439a8..ad347f8e6 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -57,7 +57,7 @@ class obj_map { public: struct key_data { Key * m_key = nullptr; - Value m_value; + Value m_value{}; key_data() = default; key_data(Key * k): m_key(k) {