mirror of
https://github.com/Z3Prover/z3
synced 2025-04-20 23:56:37 +00:00
Merge remote-tracking branch 'microsoft/master' into sls-eisenhofer
Use a hashset rather than map
This commit is contained in:
CEisenhofer
commit
64b09d87e4
|
|
@ -1798,9 +1798,9 @@ def write_log_h_preamble(log_h):
|
|||
log_h.write('#include "util/mutex.h"\n')
|
||||
log_h.write('extern atomic<bool> g_z3_log_enabled;\n')
|
||||
log_h.write('void ctx_enable_logging();\n')
|
||||
log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { ATOMIC_EXCHANGE(m_prev, g_z3_log_enabled, false); } ~z3_log_ctx() { if (m_prev) g_z3_log_enabled = true; } bool enabled() const { return m_prev; } };\n')
|
||||
log_h.write('void SetR(void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n')
|
||||
log_h.write('#define RETURN_Z3(Z3RES) do { auto tmp_ret = Z3RES; if (_LOG_CTX.enabled()) { SetR(tmp_ret); } return tmp_ret; } while (0)\n')
|
||||
log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { ATOMIC_EXCHANGE(m_prev, g_z3_log_enabled, false); } ~z3_log_ctx() { if (m_prev) [[unlikely]] g_z3_log_enabled = true; } bool enabled() const { return m_prev; } };\n')
|
||||
log_h.write('void SetR(const void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n')
|
||||
log_h.write('#define RETURN_Z3(Z3RES) do { auto tmp_ret = Z3RES; if (_LOG_CTX.enabled()) [[unlikely]] { SetR(tmp_ret); } return tmp_ret; } while (0)\n')
|
||||
|
||||
|
||||
def write_log_c_preamble(log_c):
|
||||
|
|
|
|||
|
|
@ -209,21 +209,10 @@ namespace api {
|
|||
invoke_error_handler(err);
|
||||
}
|
||||
}
|
||||
|
||||
char * context::mk_external_string(char const * str) {
|
||||
m_string_buffer = str?str:"";
|
||||
return const_cast<char *>(m_string_buffer.c_str());
|
||||
}
|
||||
|
||||
char * context::mk_external_string(char const * str, unsigned n) {
|
||||
m_string_buffer.clear();
|
||||
m_string_buffer.append(str, n);
|
||||
return const_cast<char *>(m_string_buffer.c_str());
|
||||
}
|
||||
|
||||
char * context::mk_external_string(std::string && str) {
|
||||
const char * context::mk_external_string(std::string && str) {
|
||||
m_string_buffer = std::move(str);
|
||||
return const_cast<char *>(m_string_buffer.c_str());
|
||||
return m_string_buffer.c_str();
|
||||
}
|
||||
|
||||
expr * context::mk_numeral_core(rational const & n, sort * s) {
|
||||
|
|
|
|||
|
|
@ -199,9 +199,7 @@ namespace api {
|
|||
|
||||
// Store a copy of str in m_string_buffer, and return a reference to it.
|
||||
// This method is used to communicate local/internal strings with the "external world"
|
||||
char * mk_external_string(char const * str, unsigned n);
|
||||
char * mk_external_string(char const * str);
|
||||
char * mk_external_string(std::string && str);
|
||||
const char * mk_external_string(std::string && str);
|
||||
sbuffer<char> m_char_buffer;
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -559,7 +559,7 @@ extern "C" {
|
|||
param_descrs descrs;
|
||||
to_fixedpoint_ref(d)->collect_param_descrs(descrs);
|
||||
descrs.display(buffer);
|
||||
return mk_c(c)->mk_external_string(buffer.str());
|
||||
return mk_c(c)->mk_external_string(std::move(buffer).str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ static mutex g_log_mux;
|
|||
#endif
|
||||
|
||||
// functions called from api_log_macros.*
|
||||
void SetR(void * obj) {
|
||||
void SetR(const void * obj) {
|
||||
*g_z3_log << "= " << obj << '\n';
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -217,20 +217,20 @@ extern "C" {
|
|||
if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) {
|
||||
switch (rm) {
|
||||
case MPF_ROUND_NEAREST_TEVEN:
|
||||
return mk_c(c)->mk_external_string("roundNearestTiesToEven");
|
||||
return "roundNearestTiesToEven";
|
||||
break;
|
||||
case MPF_ROUND_NEAREST_TAWAY:
|
||||
return mk_c(c)->mk_external_string("roundNearestTiesToAway");
|
||||
return "roundNearestTiesToAway";
|
||||
break;
|
||||
case MPF_ROUND_TOWARD_POSITIVE:
|
||||
return mk_c(c)->mk_external_string("roundTowardPositive");
|
||||
return "roundTowardPositive";
|
||||
break;
|
||||
case MPF_ROUND_TOWARD_NEGATIVE:
|
||||
return mk_c(c)->mk_external_string("roundTowardNegative");
|
||||
return "roundTowardNegative";
|
||||
break;
|
||||
case MPF_ROUND_TOWARD_ZERO:
|
||||
default:
|
||||
return mk_c(c)->mk_external_string("roundTowardZero");
|
||||
return "roundTowardZero";
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -313,7 +313,7 @@ extern "C" {
|
|||
param_descrs descrs;
|
||||
to_optimize_ptr(d)->collect_param_descrs(descrs);
|
||||
descrs.display(buffer);
|
||||
return mk_c(c)->mk_external_string(buffer.str());
|
||||
return mk_c(c)->mk_external_string(std::move(buffer).str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -191,7 +191,7 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_IOB, nullptr);
|
||||
RETURN_Z3(nullptr);
|
||||
}
|
||||
return mk_c(c)->mk_external_string(result);
|
||||
return result;
|
||||
Z3_CATCH_RETURN(nullptr);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -235,9 +235,9 @@ extern "C" {
|
|||
|
||||
Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str) {
|
||||
std::stringstream ous;
|
||||
Z3_TRY;
|
||||
RESET_ERROR_CODE();
|
||||
LOG_Z3_eval_smtlib2_string(c, str);
|
||||
Z3_TRY;
|
||||
if (!mk_c(c)->cmd()) {
|
||||
auto* ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
|
||||
mk_c(c)->cmd() = ctx;
|
||||
|
|
@ -257,15 +257,13 @@ extern "C" {
|
|||
// See api::context::m_parser for a motivation about the reuse of the parser
|
||||
if (!parse_smt2_commands_with_parser(mk_c(c)->m_parser, *ctx.get(), is)) {
|
||||
SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str());
|
||||
RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
|
||||
}
|
||||
}
|
||||
catch (z3_exception& e) {
|
||||
if (ous.str().empty()) ous << e.what();
|
||||
SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str());
|
||||
RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
|
||||
}
|
||||
RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
|
||||
Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str()));
|
||||
Z3_CATCH_CORE();
|
||||
RETURN_Z3(mk_c(c)->mk_external_string(std::move(ous).str()));
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -274,7 +274,7 @@ extern "C" {
|
|||
reset_rcf_cancel(c);
|
||||
std::ostringstream buffer;
|
||||
rcfm(c).display(buffer, to_rcnumeral(a), compact, html);
|
||||
return mk_c(c)->mk_external_string(buffer.str());
|
||||
return mk_c(c)->mk_external_string(std::move(buffer).str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
@ -285,7 +285,7 @@ extern "C" {
|
|||
reset_rcf_cancel(c);
|
||||
std::ostringstream buffer;
|
||||
rcfm(c).display_decimal(buffer, to_rcnumeral(a), prec);
|
||||
return mk_c(c)->mk_external_string(buffer.str());
|
||||
return mk_c(c)->mk_external_string(std::move(buffer).str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -339,7 +339,7 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_IOB, nullptr);
|
||||
return "";
|
||||
}
|
||||
return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str().c_str());
|
||||
return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
@ -359,7 +359,7 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_IOB, nullptr);
|
||||
return "";
|
||||
}
|
||||
return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str().c_str());
|
||||
return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
@ -371,7 +371,7 @@ extern "C" {
|
|||
param_descrs descrs;
|
||||
to_tactic_ref(t)->collect_param_descrs(descrs);
|
||||
descrs.display(buffer);
|
||||
return mk_c(c)->mk_external_string(buffer.str());
|
||||
return mk_c(c)->mk_external_string(std::move(buffer).str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
@ -499,8 +499,8 @@ extern "C" {
|
|||
for (unsigned i = 0; i < sz; i++) {
|
||||
to_apply_result(r)->m_subgoals[i]->display(buffer);
|
||||
}
|
||||
buffer << ")";
|
||||
return mk_c(c)->mk_external_string(buffer.str());
|
||||
buffer << ')';
|
||||
return mk_c(c)->mk_external_string(std::move(buffer).str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
@ -578,7 +578,7 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_IOB, nullptr);
|
||||
return "";
|
||||
}
|
||||
return mk_c(c)->mk_external_string(mk_c(c)->get_simplifier(idx)->get_name().str().c_str());
|
||||
return mk_c(c)->mk_external_string(mk_c(c)->get_simplifier(idx)->get_name().str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
@ -634,7 +634,7 @@ extern "C" {
|
|||
scoped_ptr<dependent_expr_simplifier> simp = (*to_simplifier_ref(t))(m, p, st);
|
||||
simp->collect_param_descrs(descrs);
|
||||
descrs.display(buffer);
|
||||
return mk_c(c)->mk_external_string(buffer.str());
|
||||
return mk_c(c)->mk_external_string(std::move(buffer).str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -671,12 +671,12 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
|
|||
expr* cond2 = nullptr, *t2 = nullptr, *e2 = nullptr;
|
||||
if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2) &&
|
||||
BR_FAILED != try_ite_value(to_app(t), val, result)) {
|
||||
result = m().mk_ite(cond, result, mk_eq(e, val));
|
||||
result = m().mk_ite(cond, result, mk_eq_plain(e, val));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
if (m().is_ite(e, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2) &&
|
||||
BR_FAILED != try_ite_value(to_app(e), val, result)) {
|
||||
result = m().mk_ite(cond, mk_eq(t, val), result);
|
||||
result = m().mk_ite(cond, mk_eq_plain(t, val), result);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
|
|
@ -684,7 +684,7 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
|
|||
}
|
||||
|
||||
|
||||
app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) {
|
||||
app* bool_rewriter::mk_eq_plain(expr* lhs, expr* rhs) {
|
||||
if (m().are_equal(lhs, rhs))
|
||||
return m().mk_true();
|
||||
if (m().are_distinct(lhs, rhs))
|
||||
|
|
|
|||
|
|
@ -135,11 +135,11 @@ public:
|
|||
br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result);
|
||||
br_status mk_not_core(expr * t, expr_ref & result);
|
||||
|
||||
app* mk_eq(expr* lhs, expr* rhs);
|
||||
app* mk_eq_plain(expr* lhs, expr* rhs);
|
||||
|
||||
void mk_eq(expr * lhs, expr * rhs, expr_ref & result) {
|
||||
if (mk_eq_core(lhs, rhs, result) == BR_FAILED)
|
||||
result = mk_eq(lhs, rhs);
|
||||
result = mk_eq_plain(lhs, rhs);
|
||||
}
|
||||
expr_ref mk_eq_rw(expr* lhs, expr* rhs) {
|
||||
expr_ref r(m()), _lhs(lhs, m()), _rhs(rhs, m());
|
||||
|
|
|
|||
|
|
@ -640,8 +640,13 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
|
|||
// use the equivalence to simplify:
|
||||
// #x000f <=_u b <=> b[sz-1:lnz+1] != 0 or #xf <= b[lnz:0])
|
||||
|
||||
result = m.mk_implies(m.mk_eq(m_mk_extract(bv_sz - 1, lnz + 1, b), mk_zero(bv_sz - lnz - 1)),
|
||||
m_util.mk_ule(m_mk_extract(lnz, 0, a), m_mk_extract(lnz, 0, b)));
|
||||
expr_ref e1(m_mk_extract(bv_sz - 1, lnz + 1, b), m);
|
||||
expr_ref e2(mk_zero(bv_sz - lnz - 1), m);
|
||||
e1 = m.mk_eq(e1, e2);
|
||||
expr_ref e3(m_mk_extract(lnz, 0, a), m);
|
||||
expr_ref e4(m_mk_extract(lnz, 0, b), m);
|
||||
e2 = m_util.mk_ule(e3, e4);
|
||||
result = m.mk_implies(e1, e2);
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
}
|
||||
|
|
@ -866,6 +871,13 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
|
|||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
// [....][xx] -> [yy][....] hi <= |[....]| then can extract [hi + k:lo + k]
|
||||
// (ashr t k)[hi:0] -> t[hi+k:k]
|
||||
if (low == 0 && m_util.is_bv_ashr(arg, t, c) && m_util.is_numeral(c, v, sz) && high < sz - v) {
|
||||
result = m_mk_extract(high + v.get_unsigned(), low + v.get_unsigned(), t);
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
@ -2498,8 +2510,8 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
|
|||
expr* a = nullptr, *b = nullptr, *c = nullptr;
|
||||
if (m.is_ite(lhs, a, b, c)) {
|
||||
bool_rewriter rw(m);
|
||||
expr_ref e1(rw.mk_eq(b, rhs), m);
|
||||
expr_ref e2(rw.mk_eq(c, rhs), m);
|
||||
expr_ref e1(rw.mk_eq_rw(b, rhs), m);
|
||||
expr_ref e2(rw.mk_eq_rw(c, rhs), m);
|
||||
result = rw.mk_ite(a, e1, e2);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1656,9 +1656,9 @@ namespace sls {
|
|||
}
|
||||
|
||||
if (result < 0)
|
||||
return 0.1;
|
||||
return 0.0000001;
|
||||
else if (result == 0)
|
||||
return 0.2;
|
||||
return 0.000002;
|
||||
for (int i = m_prob_break.size(); i <= breaks; ++i)
|
||||
m_prob_break.push_back(std::pow(m_config.cb, -i));
|
||||
return m_prob_break[breaks];
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@ namespace sls {
|
|||
bool basic_plugin::is_basic(expr* e) const {
|
||||
if (!e || !is_app(e))
|
||||
return false;
|
||||
if (m.is_ite(e) && !m.is_bool(e) && false)
|
||||
if (m.is_ite(e) && !m.is_bool(e))
|
||||
return true;
|
||||
if (m.is_xor(e) && to_app(e)->get_num_args() != 2)
|
||||
return true;
|
||||
|
|
@ -149,7 +149,6 @@ namespace sls {
|
|||
if (m.is_value(child))
|
||||
return false;
|
||||
bool r = ctx.set_value(child, ctx.get_value(e));
|
||||
verbose_stream() << "repair-ite-down " << mk_bounded_pp(e, m) << " @ " << mk_bounded_pp(child, m) << " := " << ctx.get_value(e) << " success " << r << "\n";
|
||||
return r;
|
||||
}
|
||||
|
||||
|
|
@ -166,7 +165,6 @@ namespace sls {
|
|||
val = eval_distinct(e);
|
||||
else
|
||||
return;
|
||||
verbose_stream() << "repair-up " << mk_bounded_pp(e, m) << " " << val << "\n";
|
||||
if (!ctx.set_value(e, val))
|
||||
ctx.new_value_eh(e);
|
||||
}
|
||||
|
|
@ -176,14 +174,14 @@ namespace sls {
|
|||
|
||||
bool basic_plugin::repair_down(app* e) {
|
||||
if (!is_basic(e))
|
||||
return true;
|
||||
return true;
|
||||
|
||||
if (m.is_xor(e) && eval_xor(e) == ctx.get_value(e))
|
||||
return true;
|
||||
if (m.is_ite(e) && eval_ite(e) == ctx.get_value(e))
|
||||
return true;
|
||||
if (m.is_distinct(e) && eval_distinct(e) == ctx.get_value(e))
|
||||
return true;
|
||||
verbose_stream() << "basic repair down " << mk_bounded_pp(e, m) << "\n";
|
||||
unsigned n = e->get_num_args();
|
||||
unsigned s = ctx.rand(n);
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
|
|
|
|||
|
|
@ -96,7 +96,6 @@ double sls_engine::top_score() {
|
|||
for (expr* e : m_assertions) {
|
||||
top_sum += m_tracker.get_score(e);
|
||||
}
|
||||
|
||||
TRACE("sls_top", tout << "Score distribution:";
|
||||
for (expr* e : m_assertions)
|
||||
tout << " " << m_tracker.get_score(e);
|
||||
|
|
@ -466,7 +465,6 @@ lbool sls_engine::search() {
|
|||
|
||||
// randomize if no increasing move was found
|
||||
if (new_const == static_cast<unsigned>(-1)) {
|
||||
score = old_score;
|
||||
if (m_walksat_repick)
|
||||
m_evaluator.randomize_local(m_assertions);
|
||||
else
|
||||
|
|
@ -477,22 +475,20 @@ lbool sls_engine::search() {
|
|||
// update assertion weights if a weighting is enabled (sp < 1024)
|
||||
if (m_paws)
|
||||
{
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
expr * q = m_assertions[i];
|
||||
for (auto q : m_assertions) {
|
||||
// smooth weights with probability sp / 1024
|
||||
if (m_tracker.get_random_uint(10) < m_paws_sp)
|
||||
{
|
||||
if (m_mpz_manager.eq(m_tracker.get_value(q),m_one))
|
||||
if (m_mpz_manager.eq(m_tracker.get_value(q), m_one))
|
||||
m_tracker.decrease_weight(q);
|
||||
}
|
||||
// increase weights otherwise
|
||||
else
|
||||
{
|
||||
if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero))
|
||||
if (m_mpz_manager.eq(m_tracker.get_value(q), m_zero))
|
||||
m_tracker.increase_weight(q);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
// otherwise, apply most increasing move
|
||||
|
|
|
|||
|
|
@ -48,6 +48,10 @@ namespace sls {
|
|||
}
|
||||
}
|
||||
|
||||
void bv_eval::start_propagation() {
|
||||
m_lookahead.start_propagation();
|
||||
}
|
||||
|
||||
void bv_eval::add_bit_vector(app* e) {
|
||||
if (!bv.is_bv(e))
|
||||
return;
|
||||
|
|
@ -674,13 +678,20 @@ namespace sls {
|
|||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool bv_eval::is_lookahead_phase() {
|
||||
++m_lookahead_steps;
|
||||
if (m_lookahead_steps < m_lookahead_phase_size)
|
||||
return true;
|
||||
if (m_lookahead_steps > 10 * m_lookahead_phase_size)
|
||||
m_lookahead_steps = 0;
|
||||
return false;
|
||||
}
|
||||
|
||||
bool bv_eval::repair_down(app* e, unsigned i) {
|
||||
expr* arg = e->get_arg(i);
|
||||
if (m.is_value(arg))
|
||||
return false;
|
||||
if (m.is_bool(e) && false && m_rand(10) == 0 && m_lookahead.try_repair_down(e))
|
||||
return true;
|
||||
if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
|
||||
commit_eval(e, to_app(arg));
|
||||
IF_VERBOSE(11, verbose_stream() << "repair " << mk_bounded_pp(e, m) << " : " << mk_bounded_pp(arg, m) << " := " << wval(arg) << "\n";);
|
||||
|
|
@ -693,8 +704,6 @@ namespace sls {
|
|||
ctx.new_value_eh(arg);
|
||||
return true;
|
||||
}
|
||||
if (m.is_bool(e) && m_lookahead.try_repair_down(e))
|
||||
return true;
|
||||
|
||||
return false;
|
||||
}
|
||||
|
|
@ -2024,6 +2033,10 @@ namespace sls {
|
|||
return expr_ref(m);
|
||||
}
|
||||
|
||||
void bv_eval::collect_statistics(statistics& st) const {
|
||||
m_lookahead.collect_statistics(st);
|
||||
}
|
||||
|
||||
std::ostream& bv_eval::display(std::ostream& out) const {
|
||||
auto& terms = ctx.subterms();
|
||||
for (expr* e : terms) {
|
||||
|
|
|
|||
|
|
@ -52,6 +52,8 @@ namespace sls {
|
|||
random_gen m_rand;
|
||||
config m_config;
|
||||
bool_vector m_fixed;
|
||||
unsigned m_lookahead_steps = 0;
|
||||
unsigned m_lookahead_phase_size = 10;
|
||||
|
||||
|
||||
scoped_ptr_vector<sls::bv_valuation> m_values; // expr-id -> bv valuation
|
||||
|
|
@ -147,11 +149,15 @@ namespace sls {
|
|||
|
||||
void commit_eval(expr* p, app* e);
|
||||
|
||||
bool is_lookahead_phase();
|
||||
|
||||
public:
|
||||
bv_eval(sls::bv_terms& terms, sls::context& ctx);
|
||||
|
||||
void init() { m_fix.init(); }
|
||||
|
||||
void start_propagation();
|
||||
|
||||
void register_term(expr* e);
|
||||
|
||||
/**
|
||||
|
|
@ -190,6 +196,7 @@ namespace sls {
|
|||
*/
|
||||
bool repair_up(expr* e);
|
||||
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
|
|
|
|||
|
|
@ -658,6 +658,7 @@ public:
|
|||
}
|
||||
|
||||
void serious_update(func_decl * fd, const mpz & new_value) {
|
||||
TRACE("sls", tout << "set: " << fd->get_name() << " to " << m_mpz_manager.to_string(new_value) << std::endl;);
|
||||
m_tracker.set_value(fd, new_value);
|
||||
expr * ep = m_tracker.get_entry_point(fd);
|
||||
unsigned cur_depth = m_tracker.get_distance(ep);
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ namespace sls {
|
|||
ctx(ctx)
|
||||
{}
|
||||
|
||||
void bv_fixed::init() {
|
||||
void bv_fixed::init() {
|
||||
|
||||
for (auto e : ctx.subterms())
|
||||
set_fixed(e);
|
||||
|
|
|
|||
|
|
@ -3,11 +3,13 @@ Copyright (c) 2024 Microsoft Corporation
|
|||
|
||||
Module Name:
|
||||
|
||||
sls_bv_lookahead.h
|
||||
sls_bv_lookahead
|
||||
|
||||
Abstract:
|
||||
|
||||
Lookahead solver for BV, modeled after sls_engine/sls_tracker/sls_evaluator.
|
||||
Lookahead solver for BV, modeled after
|
||||
sls_bv_engine/sls_bv_tracker/sls_bv_evaluator
|
||||
by Froelich and Wintersteiger.
|
||||
|
||||
Author:
|
||||
|
||||
|
|
@ -18,176 +20,437 @@ Author:
|
|||
#include "ast/sls/sls_bv_lookahead.h"
|
||||
#include "ast/sls/sls_bv_eval.h"
|
||||
#include "ast/sls/sls_bv_terms.h"
|
||||
#include "params/sls_params.hpp"
|
||||
#include "ast/ast_pp.h"
|
||||
#include <cmath>
|
||||
|
||||
namespace sls {
|
||||
|
||||
bv_lookahead::bv_lookahead(bv_eval& ev) :
|
||||
bv(ev.m),
|
||||
m_ev(ev),
|
||||
ctx(ev.ctx),
|
||||
m(ev.m) {}
|
||||
|
||||
bool bv_lookahead::try_repair_down(app* e) {
|
||||
if (!m.is_bool(e))
|
||||
return false;
|
||||
if (m_ev.bval1(e) == m_ev.bval0(e))
|
||||
return true;
|
||||
auto const& uninterp = m_ev.terms.uninterp_occurs(e);
|
||||
if (uninterp.empty())
|
||||
return false;
|
||||
reset_updates();
|
||||
|
||||
IF_VERBOSE(4,
|
||||
verbose_stream() << mk_bounded_pp(e, m) << "\n";
|
||||
for (auto e : uninterp)
|
||||
verbose_stream() << mk_bounded_pp(e, m) << " ";
|
||||
verbose_stream() << "\n");
|
||||
|
||||
for (auto e : uninterp)
|
||||
add_updates(e);
|
||||
|
||||
#if 0
|
||||
for (unsigned i = 0; i < m_num_updates; ++i) {
|
||||
auto const& [e, score, new_value] = m_updates[i];
|
||||
verbose_stream() << mk_bounded_pp(e, m) << " " << new_value << " score: " << score << "\n";
|
||||
}
|
||||
#endif
|
||||
|
||||
return apply_update();
|
||||
bv_lookahead::bv_lookahead(bv_eval& ev) :
|
||||
bv(ev.m),
|
||||
m_ev(ev),
|
||||
ctx(ev.ctx),
|
||||
m(ev.m) {
|
||||
}
|
||||
|
||||
double bv_lookahead::lookahead(expr* e, bvect const& new_value) {
|
||||
void bv_lookahead::start_propagation() {
|
||||
if (m_stats.m_num_propagations++ % m_config.propagation_base == 0)
|
||||
search();
|
||||
}
|
||||
|
||||
void bv_lookahead::search() {
|
||||
updt_params(ctx.get_params());
|
||||
rescore();
|
||||
m_config.max_moves = m_stats.m_moves + m_config.max_moves_base;
|
||||
|
||||
while (m.inc() && m_stats.m_moves < m_config.max_moves) {
|
||||
m_stats.m_moves++;
|
||||
check_restart();
|
||||
|
||||
// get candidate variables
|
||||
auto& vars = get_candidate_uninterp();
|
||||
|
||||
if (vars.empty())
|
||||
return;
|
||||
|
||||
// random walk with probability 1024/wp
|
||||
if (ctx.rand(2047) < m_config.wp && apply_random_move(vars))
|
||||
continue;
|
||||
|
||||
if (apply_guided_move(vars))
|
||||
continue;
|
||||
|
||||
if (apply_random_update(get_candidate_uninterp()))
|
||||
recalibrate_weights();
|
||||
}
|
||||
m_config.max_moves_base += 100;
|
||||
}
|
||||
|
||||
bool bv_lookahead::apply_guided_move(ptr_vector<expr> const& vars) {
|
||||
m_best_expr = nullptr;
|
||||
m_best_score = m_top_score;
|
||||
unsigned sz = vars.size();
|
||||
unsigned start = ctx.rand(sz);
|
||||
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";);
|
||||
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";
|
||||
return true;
|
||||
}
|
||||
|
||||
ptr_vector<expr> const& bv_lookahead::get_candidate_uninterp() {
|
||||
auto const& lits = ctx.root_literals();
|
||||
app* e = nullptr;
|
||||
if (m_config.ucb) {
|
||||
double max = -1.0;
|
||||
for (auto lit : ctx.root_literals()) {
|
||||
if (!is_false_bv_literal(lit))
|
||||
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))
|
||||
+ m_config.ucb_noise * ctx.rand(512);
|
||||
if (q > max)
|
||||
max = q, e = a;
|
||||
}
|
||||
if (e) {
|
||||
m_touched++;
|
||||
inc_touched(e);
|
||||
}
|
||||
}
|
||||
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()));
|
||||
}
|
||||
if (!e)
|
||||
return m_empty_vars;
|
||||
|
||||
auto const& vars = m_ev.terms.uninterp_occurs(e);
|
||||
VERIFY(!vars.empty());
|
||||
TRACE("bv", tout << "candidates " << mk_bounded_pp(e, m) << ": ";
|
||||
for (auto e : vars) tout << mk_bounded_pp(e, m) << " ";
|
||||
tout << "\n";);
|
||||
return vars;
|
||||
}
|
||||
|
||||
bool bv_lookahead::apply_random_update(ptr_vector<expr> 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<expr> 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) {
|
||||
ucb_forget();
|
||||
rescore();
|
||||
}
|
||||
|
||||
if (m_stats.m_moves < m_config.restart_next)
|
||||
return;
|
||||
|
||||
++m_stats.m_restarts;
|
||||
|
||||
if (0x1 == (m_stats.m_restarts & 0x1))
|
||||
m_config.restart_next += m_config.restart_base;
|
||||
else
|
||||
m_config.restart_next += (2 << (m_stats.m_restarts >> 1)) * m_config.restart_base;
|
||||
|
||||
reset_uninterp_in_false_literals();
|
||||
rescore();
|
||||
}
|
||||
|
||||
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))
|
||||
continue;
|
||||
app* a = to_app(ctx.atom(lit.var()));
|
||||
auto const& occs = m_ev.terms.uninterp_occurs(a);
|
||||
for (auto e : occs) {
|
||||
if (marked.is_marked(e))
|
||||
continue;
|
||||
marked.mark(e);
|
||||
auto& v = wval(e);
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool bv_lookahead::is_bv_literal(sat::literal lit) {
|
||||
if (!ctx.is_true(lit))
|
||||
return false;
|
||||
auto e = ctx.atom(lit.var());
|
||||
if (!e || !is_app(e))
|
||||
return false;
|
||||
app* a = to_app(e);
|
||||
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));
|
||||
}
|
||||
|
||||
|
||||
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();
|
||||
m_config.paws = m_config.paws_sp < 1024;
|
||||
m_config.wp = p.wp();
|
||||
m_config.restart_base = p.restart_base();
|
||||
m_config.restart_next = m_config.restart_base;
|
||||
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();
|
||||
}
|
||||
|
||||
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;
|
||||
if (is_true && m.is_eq(a, x, y) && bv.is_bv(x)) {
|
||||
auto const& vx = wval(x);
|
||||
auto const& vy = wval(y);
|
||||
// hamming distance between vx.bits() and vy.bits():
|
||||
double delta = 0;
|
||||
for (unsigned i = 0; i < vx.bw; ++i)
|
||||
if (vx.bits().get(i) != vy.bits().get(i))
|
||||
++delta;
|
||||
auto d = 1.0 - (delta / (double)vx.bw);
|
||||
//verbose_stream() << "hamming distance " << mk_bounded_pp(a, m) << " " << d << "\n";
|
||||
return d;
|
||||
}
|
||||
else if (bv.is_ule(a, x, y)) {
|
||||
auto const& vx = wval(x);
|
||||
auto const& vy = wval(y);
|
||||
|
||||
if (is_true)
|
||||
// x > y as unsigned.
|
||||
// x - y > 0
|
||||
// score = (x - y) / 2^bw
|
||||
vx.set_sub(m_ev.m_tmp, vx.bits(), vy.bits());
|
||||
else {
|
||||
// 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();
|
||||
return (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
|
||||
}
|
||||
else if (bv.is_sle(a, x, y)) {
|
||||
auto const& vx = wval(x);
|
||||
auto const& vy = wval(y);
|
||||
// x += 2^bw-1
|
||||
// y += 2^bw-1
|
||||
vy.bits().copy_to(vy.nw, m_ev.m_tmp);
|
||||
vx.bits().copy_to(vx.nw, m_ev.m_tmp2);
|
||||
m_ev.m_tmp.set(vy.bw - 1, !m_ev.m_tmp.get(vy.bw - 1));
|
||||
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
|
||||
vx.set_sub(m_ev.m_tmp3, m_ev.m_tmp2, m_ev.m_tmp);
|
||||
}
|
||||
else {
|
||||
// x <=s y
|
||||
// y' - x' >= 0
|
||||
vx.set_sub(m_ev.m_tmp3, m_ev.m_tmp, m_ev.m_tmp2);
|
||||
vx.add1(m_ev.m_tmp3);
|
||||
}
|
||||
rational n = m_ev.m_tmp3.get_value(vx.nw);
|
||||
n /= rational(rational::power_of_two(vx.bw));
|
||||
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))) {
|
||||
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) {
|
||||
++np;
|
||||
auto const& vj = wval(a->get_arg(j));
|
||||
if (vi.bits() != vj.bits())
|
||||
nd++;
|
||||
}
|
||||
}
|
||||
return nd / np;
|
||||
}
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
double bv_lookahead::lookahead_update(expr* e, bvect const& new_value) {
|
||||
SASSERT(bv.is_bv(e));
|
||||
SASSERT(is_uninterp(e));
|
||||
SASSERT(m_restore.empty());
|
||||
|
||||
bool has_tabu = false;
|
||||
double break_count = 0, make_count = 0;
|
||||
double score = m_top_score;
|
||||
|
||||
wval(e).eval = new_value;
|
||||
if (!insert_update(e)) {
|
||||
restore_lookahead();
|
||||
m_in_update_stack.reset();
|
||||
return -1000000;
|
||||
}
|
||||
insert_update_stack(e);
|
||||
unsigned max_depth = get_depth(e);
|
||||
for (unsigned depth = max_depth; depth <= max_depth; ++depth) {
|
||||
for (unsigned i = 0; !has_tabu && i < m_update_stack[depth].size(); ++i) {
|
||||
auto e = m_update_stack[depth][i];
|
||||
if (bv.is_bv(e)) {
|
||||
auto& v = m_ev.eval(to_app(e));
|
||||
if (insert_update(e)) {
|
||||
for (auto p : ctx.parents(e)) {
|
||||
auto a = m_update_stack[depth][i];
|
||||
if (bv.is_bv(a)) {
|
||||
if (a == e || (m_ev.eval(a), insert_update(a))) { // do not insert e twice
|
||||
for (auto p : ctx.parents(a)) {
|
||||
insert_update_stack(p);
|
||||
max_depth = std::max(max_depth, get_depth(p));
|
||||
}
|
||||
}
|
||||
else
|
||||
else {
|
||||
IF_VERBOSE(1, verbose_stream() << "tabu " << mk_bounded_pp(a, m) << "\n");
|
||||
has_tabu = true;
|
||||
}
|
||||
}
|
||||
else if (m.is_bool(e) && m_ev.can_eval1(to_app(e))) {
|
||||
if (!ctx.is_relevant(e))
|
||||
continue;
|
||||
bool is_true = ctx.is_true(e);
|
||||
bool is_true_new = m_ev.bval1(to_app(e));
|
||||
bool is_true_old = m_ev.bval1_tmp(to_app(e));
|
||||
if (is_true_new == is_true_old)
|
||||
continue;
|
||||
if (is_true == is_true_new)
|
||||
++make_count;
|
||||
if (is_true == is_true_old)
|
||||
++break_count;
|
||||
else if (is_root(a)) {
|
||||
score += get_weight(a) * (new_score(a) - old_score(a));
|
||||
}
|
||||
else if (m.is_bool(a))
|
||||
continue;
|
||||
else {
|
||||
IF_VERBOSE(1, verbose_stream() << "skipping " << mk_bounded_pp(e, m) << "\n");
|
||||
IF_VERBOSE(1, verbose_stream() << "skipping " << mk_bounded_pp(a, m) << "\n");
|
||||
has_tabu = true;
|
||||
}
|
||||
}
|
||||
m_update_stack[depth].reset();
|
||||
}
|
||||
m_in_update_stack.reset();
|
||||
restore_lookahead();
|
||||
// verbose_stream() << has_tabu << " " << new_value << " " << make_count << " " << break_count << "\n";
|
||||
|
||||
TRACE("sls_verbose", tout << mk_bounded_pp(e, m) << " := " << new_value << " score: " << m_top_score << "\n");
|
||||
|
||||
if (has_tabu)
|
||||
return -10000;
|
||||
return make_count - break_count;
|
||||
return score;
|
||||
}
|
||||
|
||||
void bv_lookahead::try_set(expr* e, bvect const& new_value) {
|
||||
if (!wval(e).can_set(new_value))
|
||||
void bv_lookahead::try_set(expr* u, bvect const& new_value) {
|
||||
if (!wval(u).can_set(new_value))
|
||||
return;
|
||||
auto d = lookahead(e, new_value);
|
||||
if (d > 0)
|
||||
add_update(d, e, new_value);
|
||||
auto score = lookahead_update(u, new_value);
|
||||
++m_stats.m_num_updates;
|
||||
//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;
|
||||
m_best_value.set_bw(new_value.bw);
|
||||
new_value.copy_to(new_value.nw, m_best_value);
|
||||
}
|
||||
}
|
||||
|
||||
void bv_lookahead::add_updates(expr* e) {
|
||||
SASSERT(bv.is_bv(e));
|
||||
auto& v = wval(e);
|
||||
double d = 0;
|
||||
void bv_lookahead::add_updates(expr* u) {
|
||||
SASSERT(bv.is_bv(u));
|
||||
auto& v = wval(u);
|
||||
while (m_v_saved.size() < v.bits().size()) {
|
||||
m_v_saved.push_back(0);
|
||||
m_v_updated.push_back(0);
|
||||
m_best_value.push_back(0);
|
||||
}
|
||||
|
||||
m_v_saved.set_bw(v.bw);
|
||||
m_v_updated.set_bw(v.bw);
|
||||
v.bits().copy_to(v.nw, m_v_saved);
|
||||
m_v_saved.copy_to(v.nw, m_v_updated);
|
||||
|
||||
// flip a single bit
|
||||
for (unsigned i = 0; i < v.bw; ++i) {
|
||||
for (unsigned i = 0; i < v.bw && i <= 32; ++i) {
|
||||
m_v_updated.set(i, !m_v_updated.get(i));
|
||||
try_set(e, m_v_updated);
|
||||
//verbose_stream() << "flip " << d << " " << m_v_updated << "\n";
|
||||
try_set(u, m_v_updated);
|
||||
m_v_updated.set(i, !m_v_updated.get(i));
|
||||
}
|
||||
if (v.bw > 32) {
|
||||
unsigned j = ctx.rand(v.bw - 32) + 32;
|
||||
m_v_updated.set(j, !m_v_updated.get(j));
|
||||
try_set(u, m_v_updated);
|
||||
m_v_updated.set(j, !m_v_updated.get(j));
|
||||
}
|
||||
if (v.bw <= 1)
|
||||
return;
|
||||
|
||||
// invert
|
||||
for (unsigned i = 0; i < v.nw; ++i)
|
||||
m_v_updated[i] = ~m_v_updated[i];
|
||||
v.clear_overflow_bits(m_v_updated);
|
||||
try_set(e, m_v_updated);
|
||||
|
||||
// increment
|
||||
m_v_saved.copy_to(v.nw, m_v_updated);
|
||||
v.add1(m_v_updated);
|
||||
try_set(e, m_v_updated);
|
||||
try_set(u, m_v_updated);
|
||||
|
||||
// decrement
|
||||
m_v_saved.copy_to(v.nw, m_v_updated);
|
||||
v.sub1(m_v_updated);
|
||||
try_set(e, m_v_updated);
|
||||
try_set(u, m_v_updated);
|
||||
|
||||
// random
|
||||
v.get_variant(m_v_updated, m_ev.m_rand);
|
||||
try_set(e, m_v_updated);
|
||||
}
|
||||
|
||||
bool bv_lookahead::apply_update() {
|
||||
double sum_score = 0;
|
||||
for (unsigned i = 0; i < m_num_updates; ++i)
|
||||
sum_score += m_updates[i].score;
|
||||
double pos = (sum_score * m_ev.m_rand()) / (double)m_ev.m_rand.max_value();
|
||||
for (unsigned i = 0; i < m_num_updates; ++i) {
|
||||
auto const& [e, score, new_value] = m_updates[i];
|
||||
pos -= score;
|
||||
if (pos <= 0) {
|
||||
//verbose_stream() << "apply " << mk_bounded_pp(e, m) << " new value " << new_value << " " << score << "\n";
|
||||
apply_update(e, new_value);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
// invert
|
||||
m_v_saved.copy_to(v.nw, m_v_updated);
|
||||
for (unsigned i = 0; i < v.nw; ++i)
|
||||
m_v_updated[i] = ~m_v_updated[i];
|
||||
v.clear_overflow_bits(m_v_updated);
|
||||
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");
|
||||
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);
|
||||
|
|
@ -195,29 +458,41 @@ namespace sls {
|
|||
for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
|
||||
auto e = m_update_stack[depth][i];
|
||||
if (bv.is_bv(e)) {
|
||||
m_ev.eval(to_app(e)); // updates wval(e).eval
|
||||
VERIFY(wval(e).commit_eval());
|
||||
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");
|
||||
// bv_plugin::is_sat picks up discrepancies
|
||||
continue;
|
||||
}
|
||||
for (auto p : ctx.parents(e)) {
|
||||
insert_update_stack(p);
|
||||
max_depth = std::max(max_depth, get_depth(p));
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (m.is_bool(e) && m_ev.can_eval1(to_app(e))) {
|
||||
VERIFY(m_ev.repair_up(e));
|
||||
else if (is_root(e)) {
|
||||
double score = new_score(e);
|
||||
m_top_score += get_weight(e) * (score - old_score(e));
|
||||
set_score(e, score);
|
||||
}
|
||||
else if (m.is_bool(e))
|
||||
continue;
|
||||
else {
|
||||
UNREACHABLE();
|
||||
UNREACHABLE();
|
||||
}
|
||||
}
|
||||
m_update_stack[depth].reset();
|
||||
}
|
||||
m_in_update_stack.reset();
|
||||
m_in_update_stack.reset();
|
||||
TRACE("bv", tout << mk_bounded_pp(e, m) << " := "
|
||||
<< new_value << " " << m_top_score << " (" << old_top_score << ")\n");
|
||||
}
|
||||
|
||||
bool bv_lookahead::insert_update(expr* e) {
|
||||
auto& v = wval(e);
|
||||
m_restore.push_back(e);
|
||||
m_on_restore.mark(e);
|
||||
auto& v = wval(e);
|
||||
TRACE("sls_verbose", tout << "insert update " << mk_bounded_pp(e, m) << " " << v << "\n");
|
||||
v.save_value();
|
||||
return v.commit_eval();
|
||||
}
|
||||
|
|
@ -225,18 +500,19 @@ namespace sls {
|
|||
void bv_lookahead::insert_update_stack(expr* e) {
|
||||
unsigned depth = get_depth(e);
|
||||
m_update_stack.reserve(depth + 1);
|
||||
if (!m_in_update_stack.is_marked(e)) {
|
||||
if (!m_in_update_stack.is_marked(e) && is_app(e)) {
|
||||
m_in_update_stack.mark(e);
|
||||
m_update_stack[depth].push_back(e);
|
||||
}
|
||||
m_update_stack[depth].push_back(to_app(e));
|
||||
}
|
||||
}
|
||||
|
||||
void bv_lookahead::restore_lookahead() {
|
||||
for (auto e : m_restore)
|
||||
for (auto e : m_restore) {
|
||||
wval(e).restore_value();
|
||||
TRACE("sls_verbose", tout << "restore value " << mk_bounded_pp(e, m) << " " << wval(e) << "\n");
|
||||
}
|
||||
m_restore.reset();
|
||||
m_on_restore.reset();
|
||||
m_in_update_stack.reset();
|
||||
}
|
||||
|
||||
sls::bv_valuation& bv_lookahead::wval(expr* e) const {
|
||||
|
|
@ -246,4 +522,80 @@ namespace sls {
|
|||
bool bv_lookahead::on_restore(expr* e) const {
|
||||
return m_on_restore.is_marked(e);
|
||||
}
|
||||
|
||||
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});
|
||||
}
|
||||
|
||||
void bv_lookahead::dec_weight(expr* e) {
|
||||
auto& w = get_bool_info(e).weight;
|
||||
w = w > m_config.paws_init ? w - 1 : m_config.paws_init;
|
||||
}
|
||||
|
||||
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()));
|
||||
double score = new_score(a);
|
||||
set_score(a, score);
|
||||
m_top_score += score;
|
||||
m_is_root.mark(a);
|
||||
}
|
||||
}
|
||||
|
||||
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);
|
||||
if (ctx.rand(2047) < m_config.paws_sp) {
|
||||
if (is_true0 == is_true1)
|
||||
dec_weight(a);
|
||||
}
|
||||
else if (is_true0 != is_true1)
|
||||
inc_weight(a);
|
||||
}
|
||||
|
||||
IF_VERBOSE(20, display_weights(verbose_stream()));
|
||||
}
|
||||
|
||||
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
|
||||
<< get_weight(a) << " "
|
||||
<< mk_bounded_pp(a, m) << " "
|
||||
<< old_score(a) << "\n";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
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()));
|
||||
auto touched_old = get_touched(a);
|
||||
auto touched_new = static_cast<unsigned>((touched_old - 1) * m_config.ucb_forget + 1);
|
||||
set_touched(a, touched_new);
|
||||
m_touched += touched_new - touched_old;
|
||||
}
|
||||
}
|
||||
|
||||
void bv_lookahead::collect_statistics(statistics& st) const {
|
||||
st.update("sls-bv-lookahead", m_stats.m_num_lookahead);
|
||||
st.update("sls-bv-updates", m_stats.m_num_updates);
|
||||
st.update("sls-bv-moves", m_stats.m_moves);
|
||||
st.update("sls-bv-restarts", m_stats.m_restarts);
|
||||
}
|
||||
}
|
||||
|
|
@ -24,54 +24,115 @@ namespace sls {
|
|||
class bv_eval;
|
||||
|
||||
class bv_lookahead {
|
||||
|
||||
struct config {
|
||||
double cb = 2.85;
|
||||
unsigned paws_init = 40;
|
||||
unsigned paws_sp = 52;
|
||||
bool paws = true;
|
||||
bool walksat = true;
|
||||
bool walksat_repick = false;
|
||||
unsigned wp = 100;
|
||||
unsigned restart_base = 1000;
|
||||
unsigned restart_next = 1000;
|
||||
unsigned restart_init = 1000;
|
||||
bool early_prune = true;
|
||||
unsigned max_moves = 0;
|
||||
unsigned max_moves_base = 800;
|
||||
unsigned propagation_base = 10000;
|
||||
bool ucb = true;
|
||||
double ucb_constant = 1.0;
|
||||
double ucb_forget = 0.1;
|
||||
bool ucb_init = false;
|
||||
double ucb_noise = 0.1;
|
||||
};
|
||||
|
||||
struct stats {
|
||||
unsigned m_num_lookahead = 0;
|
||||
unsigned m_num_updates = 0;
|
||||
unsigned m_moves = 0;
|
||||
unsigned m_restarts = 0;
|
||||
unsigned m_num_propagations = 0;
|
||||
};
|
||||
|
||||
struct bool_info {
|
||||
unsigned weight = 40;
|
||||
double score = 0;
|
||||
unsigned touched = 1;
|
||||
};
|
||||
|
||||
bv_util bv;
|
||||
bv_eval& m_ev;
|
||||
context& ctx;
|
||||
ast_manager& m;
|
||||
config m_config;
|
||||
stats m_stats;
|
||||
bvect m_v_saved, m_v_updated;
|
||||
|
||||
ptr_vector<expr> m_restore;
|
||||
vector<ptr_vector<expr>> m_update_stack;
|
||||
vector<ptr_vector<app>> m_update_stack;
|
||||
expr_mark m_on_restore, m_in_update_stack;
|
||||
struct update {
|
||||
expr* e;
|
||||
double score;
|
||||
bvect value;
|
||||
};
|
||||
vector<update> m_updates;
|
||||
unsigned m_num_updates = 0;
|
||||
void reset_updates() { m_num_updates = 0; }
|
||||
void add_update(double score, expr* e, bvect const& value) {
|
||||
if (m_num_updates == m_updates.size())
|
||||
m_updates.push_back({ e, score, value });
|
||||
else {
|
||||
auto& u = m_updates[m_num_updates];
|
||||
u.e = e;
|
||||
u.score = score;
|
||||
u.value = value;
|
||||
}
|
||||
m_num_updates++;
|
||||
}
|
||||
|
||||
double m_best_score = 0, m_top_score = 0;
|
||||
bvect m_best_value;
|
||||
expr* m_best_expr = nullptr;
|
||||
ptr_vector<expr> m_empty_vars;
|
||||
obj_map<expr, bool_info> m_bool_info;
|
||||
expr_mark m_is_root;
|
||||
unsigned m_touched = 1;
|
||||
|
||||
std::ostream& display_weights(std::ostream& out);
|
||||
|
||||
bv_valuation& wval(expr* e) const;
|
||||
|
||||
void insert_update_stack(expr* e);
|
||||
bool insert_update(expr* e);
|
||||
void restore_lookahead();
|
||||
double lookahead(expr* e, bvect const& new_value);
|
||||
|
||||
void try_set(expr* e, bvect const& new_value);
|
||||
void add_updates(expr* e);
|
||||
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);
|
||||
|
||||
void rescore();
|
||||
|
||||
unsigned get_weight(expr* e) { return get_bool_info(e).weight; }
|
||||
void inc_weight(expr* e) { ++get_bool_info(e).weight; }
|
||||
void dec_weight(expr* e);
|
||||
void recalibrate_weights();
|
||||
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; }
|
||||
|
||||
void try_set(expr* u, bvect const& new_value);
|
||||
void add_updates(expr* u);
|
||||
void apply_update(expr* e, bvect const& new_value);
|
||||
bool apply_update();
|
||||
bool apply_random_move(ptr_vector<expr> const& vars);
|
||||
bool apply_guided_move(ptr_vector<expr> const& vars);
|
||||
bool apply_random_update(ptr_vector<expr> const& vars);
|
||||
ptr_vector<expr> const& get_candidate_uninterp();
|
||||
|
||||
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();
|
||||
|
||||
|
||||
|
||||
public:
|
||||
bv_lookahead(bv_eval& ev);
|
||||
|
||||
void updt_params(params_ref const& p);
|
||||
|
||||
void start_propagation();
|
||||
|
||||
bool on_restore(expr* e) const;
|
||||
|
||||
bool try_repair_down(app* e);
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
||||
};
|
||||
}
|
||||
|
|
@ -50,6 +50,10 @@ namespace sls {
|
|||
return false;
|
||||
}
|
||||
|
||||
void bv_plugin::start_propagation() {
|
||||
m_eval.start_propagation();
|
||||
}
|
||||
|
||||
void bv_plugin::propagate_literal(sat::literal lit) {
|
||||
SASSERT(ctx.is_true(lit));
|
||||
auto e = ctx.atom(lit.var());
|
||||
|
|
@ -167,6 +171,10 @@ namespace sls {
|
|||
ctx.flip(lit.var());
|
||||
}
|
||||
|
||||
void bv_plugin::collect_statistics(statistics& st) const {
|
||||
m_eval.collect_statistics(st);
|
||||
}
|
||||
|
||||
std::ostream& bv_plugin::trace_repair(bool down, expr* e) {
|
||||
verbose_stream() << (down ? "d #" : "u #")
|
||||
<< e->get_id() << ": "
|
||||
|
|
|
|||
|
|
@ -41,6 +41,7 @@ namespace sls {
|
|||
~bv_plugin() override {}
|
||||
void register_term(expr* e) override;
|
||||
expr_ref get_value(expr* e) override;
|
||||
void start_propagation() override;
|
||||
void initialize() override;
|
||||
void propagate_literal(sat::literal lit) override;
|
||||
bool propagate() override;
|
||||
|
|
@ -53,7 +54,7 @@ namespace sls {
|
|||
void on_restart() override {}
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
bool set_value(expr* e, expr* v) override;
|
||||
void collect_statistics(statistics& st) const override {}
|
||||
void collect_statistics(statistics& st) const override;
|
||||
void reset_statistics() override {}
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -16,6 +16,7 @@ Author:
|
|||
--*/
|
||||
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/sls/sls_bv_terms.h"
|
||||
#include "ast/rewriter/bool_rewriter.h"
|
||||
#include "ast/rewriter/bv_rewriter.h"
|
||||
|
|
@ -23,15 +24,17 @@ Author:
|
|||
namespace sls {
|
||||
|
||||
bv_terms::bv_terms(sls::context& ctx):
|
||||
ctx(ctx),
|
||||
m(ctx.get_manager()),
|
||||
bv(m),
|
||||
m_axioms(m) {}
|
||||
|
||||
void bv_terms::register_term(expr* e) {
|
||||
auto r = ensure_binary(e);
|
||||
if (r != e)
|
||||
m_axioms.push_back(m.mk_eq(e, r));
|
||||
register_uninterp(e);
|
||||
if (r != e) {
|
||||
bool_rewriter br(m);
|
||||
m_axioms.push_back(br.mk_eq_rw(e, r));
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref bv_terms::ensure_binary(expr* e) {
|
||||
|
|
@ -69,10 +72,10 @@ namespace sls {
|
|||
expr_ref absx = br.mk_ite(signx, bvr.mk_bv_neg(x), x);
|
||||
expr_ref absy = br.mk_ite(signy, bvr.mk_bv_neg(y), y);
|
||||
expr_ref d = expr_ref(bv.mk_bv_udiv(absx, absy), m);
|
||||
expr_ref r = br.mk_ite(br.mk_eq(signx, signy), d, bvr.mk_bv_neg(d));
|
||||
r = br.mk_ite(br.mk_eq(z, y),
|
||||
expr_ref r = br.mk_ite(br.mk_eq_rw(signx, signy), d, bvr.mk_bv_neg(d));
|
||||
r = br.mk_ite(br.mk_eq_rw(z, y),
|
||||
br.mk_ite(signx, o, n1),
|
||||
br.mk_ite(br.mk_eq(x, z), z, r));
|
||||
br.mk_ite(br.mk_eq_rw(x, z), z, r));
|
||||
return r;
|
||||
}
|
||||
|
||||
|
|
@ -92,8 +95,8 @@ namespace sls {
|
|||
expr_ref abs_y = br.mk_ite(bvr.mk_sle(z, y), y, bvr.mk_bv_neg(y));
|
||||
expr_ref u = bvr.mk_bv_urem(abs_x, abs_y);
|
||||
expr_ref r(m);
|
||||
r = br.mk_ite(br.mk_eq(u, z), z,
|
||||
br.mk_ite(br.mk_eq(y, z), x,
|
||||
r = br.mk_ite(br.mk_eq_rw(u, z), z,
|
||||
br.mk_ite(br.mk_eq_rw(y, z), x,
|
||||
br.mk_ite(br.mk_and(bvr.mk_sle(z, x), bvr.mk_sle(z, x)), u,
|
||||
br.mk_ite(bvr.mk_sle(z, x), bvr.mk_bv_add(y, u),
|
||||
br.mk_ite(bv.mk_sle(z, y), bvr.mk_bv_sub(y, u), bvr.mk_bv_neg(u))))));
|
||||
|
|
@ -107,10 +110,28 @@ namespace sls {
|
|||
bool_rewriter br(m);
|
||||
bv_rewriter bvr(m);
|
||||
expr_ref z(bv.mk_zero(bv.get_bv_size(x)), m);
|
||||
r = br.mk_ite(br.mk_eq(y, z), x, bvr.mk_bv_sub(x, bvr.mk_bv_mul(y, mk_sdiv(x, y))));
|
||||
r = br.mk_ite(br.mk_eq_rw(y, z), x, bvr.mk_bv_sub(x, bvr.mk_bv_mul(y, mk_sdiv(x, y))));
|
||||
return r;
|
||||
}
|
||||
|
||||
ptr_vector<expr> const& bv_terms::uninterp_occurs(expr* e) {
|
||||
unsigned id = e->get_id();
|
||||
m_uninterp_occurs.reserve(id + 1);
|
||||
if (!m_uninterp_occurs[id].empty())
|
||||
return m_uninterp_occurs[id];
|
||||
register_uninterp(e);
|
||||
return m_uninterp_occurs[id];
|
||||
}
|
||||
|
||||
ptr_vector<expr> const& bv_terms::condition_occurs(expr* e) {
|
||||
unsigned id = e->get_id();
|
||||
m_condition_occurs.reserve(id + 1);
|
||||
if (!m_condition_occurs[id].empty())
|
||||
return m_condition_occurs[id];
|
||||
register_uninterp(e);
|
||||
return m_condition_occurs[id];
|
||||
}
|
||||
|
||||
void bv_terms::register_uninterp(expr* e) {
|
||||
if (!m.is_bool(e))
|
||||
return;
|
||||
|
|
@ -123,7 +144,9 @@ namespace sls {
|
|||
else
|
||||
return;
|
||||
m_uninterp_occurs.reserve(e->get_id() + 1);
|
||||
m_condition_occurs.reserve(e->get_id() + 1);
|
||||
auto& occs = m_uninterp_occurs[e->get_id()];
|
||||
auto& cond_occs = m_condition_occurs[e->get_id()];
|
||||
ptr_vector<expr> todo;
|
||||
todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
|
||||
expr_mark marked;
|
||||
|
|
@ -138,8 +161,11 @@ namespace sls {
|
|||
todo.push_back(arg);
|
||||
}
|
||||
else if (m.is_ite(e, c, th, el)) {
|
||||
todo.push_back(th);
|
||||
todo.push_back(el);
|
||||
cond_occs.push_back(c);
|
||||
if (ctx.is_true(c))
|
||||
todo.push_back(th);
|
||||
else
|
||||
todo.push_back(el);
|
||||
}
|
||||
else if (bv.is_bv(e))
|
||||
occs.push_back(e);
|
||||
|
|
|
|||
|
|
@ -29,10 +29,12 @@ Author:
|
|||
namespace sls {
|
||||
|
||||
class bv_terms {
|
||||
context& ctx;
|
||||
ast_manager& m;
|
||||
bv_util bv;
|
||||
expr_ref_vector m_axioms;
|
||||
vector<ptr_vector<expr>> m_uninterp_occurs;
|
||||
vector<ptr_vector<expr>> m_condition_occurs;
|
||||
|
||||
expr_ref ensure_binary(expr* e);
|
||||
|
||||
|
|
@ -43,12 +45,16 @@ namespace sls {
|
|||
void register_uninterp(expr* e);
|
||||
|
||||
public:
|
||||
bv_terms(sls::context& ctx);
|
||||
bv_terms(context& ctx);
|
||||
|
||||
void register_term(expr* e);
|
||||
|
||||
expr_ref_vector& axioms() { return m_axioms; }
|
||||
|
||||
ptr_vector<expr> const& uninterp_occurs(expr* e) { m_uninterp_occurs.reserve(e->get_id() + 1); return m_uninterp_occurs[e->get_id()]; }
|
||||
ptr_vector<expr> const& uninterp_occurs(expr* e);
|
||||
|
||||
ptr_vector<expr> const& condition_occurs(expr* e);
|
||||
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -23,6 +23,7 @@ Notes:
|
|||
#include "ast/for_each_expr.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/bv_decl_plugin.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "model/model.h"
|
||||
|
||||
#include "params/sls_params.hpp"
|
||||
|
|
@ -34,23 +35,23 @@ class sls_tracker {
|
|||
bv_util & m_bv_util;
|
||||
powers & m_powers;
|
||||
random_gen m_rng;
|
||||
unsigned m_random_bits;
|
||||
unsigned m_random_bits_cnt;
|
||||
unsigned m_random_bits = 0;
|
||||
unsigned m_random_bits_cnt = 0;
|
||||
mpz m_zero, m_one, m_two;
|
||||
|
||||
struct value_score {
|
||||
value_score() : m(nullptr), value(unsynch_mpz_manager::mk_z(0)), score(0.0), score_prune(0.0), has_pos_occ(0), has_neg_occ(0), distance(0), touched(1) {};
|
||||
value_score() : value(unsynch_mpz_manager::mk_z(0)) {};
|
||||
value_score(value_score&&) noexcept = default;
|
||||
~value_score() { if (m) m->del(value); }
|
||||
value_score& operator=(value_score&&) = default;
|
||||
unsynch_mpz_manager * m;
|
||||
unsynch_mpz_manager * m = nullptr;
|
||||
mpz value;
|
||||
double score;
|
||||
double score_prune;
|
||||
unsigned has_pos_occ;
|
||||
unsigned has_neg_occ;
|
||||
unsigned distance; // max distance from any root
|
||||
unsigned touched;
|
||||
double score = 0.0;
|
||||
double score_prune = 0.0;
|
||||
unsigned has_pos_occ = 0;
|
||||
unsigned has_neg_occ = 0;
|
||||
unsigned distance = 0; // max distance from any root
|
||||
unsigned touched = 1;
|
||||
};
|
||||
|
||||
public:
|
||||
|
|
@ -67,21 +68,21 @@ private:
|
|||
ptr_vector<func_decl> m_constants;
|
||||
ptr_vector<func_decl> m_temp_constants;
|
||||
occ_type m_constants_occ;
|
||||
unsigned m_last_pos;
|
||||
unsigned m_walksat;
|
||||
unsigned m_ucb;
|
||||
double m_ucb_constant;
|
||||
unsigned m_ucb_init;
|
||||
double m_ucb_forget;
|
||||
double m_ucb_noise;
|
||||
unsigned m_touched;
|
||||
double m_scale_unsat;
|
||||
unsigned m_paws_init;
|
||||
unsigned m_last_pos = 0;
|
||||
unsigned m_walksat = 0;
|
||||
unsigned m_ucb = 0;
|
||||
double m_ucb_constant = 0;
|
||||
unsigned m_ucb_init = 0;
|
||||
double m_ucb_forget = 0;
|
||||
double m_ucb_noise = 0;
|
||||
unsigned m_touched = 0;
|
||||
double m_scale_unsat = 0;
|
||||
unsigned m_paws_init = 0;
|
||||
obj_map<expr, unsigned> m_where_false;
|
||||
expr** m_list_false;
|
||||
unsigned m_track_unsat;
|
||||
expr** m_list_false = nullptr;
|
||||
unsigned m_track_unsat = 0;
|
||||
obj_map<expr, unsigned> m_weights;
|
||||
double m_top_sum;
|
||||
double m_top_sum = 0;
|
||||
obj_hashtable<expr> m_temp_seen;
|
||||
|
||||
public:
|
||||
|
|
@ -89,8 +90,7 @@ public:
|
|||
m_manager(m),
|
||||
m_mpz_manager(mm),
|
||||
m_bv_util(bvu),
|
||||
m_powers(p),
|
||||
m_random_bits_cnt(0),
|
||||
m_powers(p),
|
||||
m_zero(m_mpz_manager.mk_z(0)),
|
||||
m_one(m_mpz_manager.mk_z(1)),
|
||||
m_two(m_mpz_manager.mk_z(2)) {
|
||||
|
|
@ -144,7 +144,7 @@ public:
|
|||
}*/
|
||||
|
||||
inline void adapt_top_sum(expr * e, double add, double sub) {
|
||||
m_top_sum += m_weights.find(e) * (add - sub);
|
||||
m_top_sum += get_weight(e) * (add - sub);
|
||||
}
|
||||
|
||||
inline void set_top_sum(double new_score) {
|
||||
|
|
@ -160,12 +160,7 @@ public:
|
|||
}
|
||||
|
||||
inline bool is_sat() {
|
||||
for (obj_hashtable<expr>::iterator it = m_top_expr.begin();
|
||||
it != m_top_expr.end();
|
||||
it++)
|
||||
if (!m_mpz_manager.is_one(get_value(*it)))
|
||||
return false;
|
||||
return true;
|
||||
return all_of(m_top_expr, [this](expr* e) { return m_mpz_manager.is_one(get_value(e)); });
|
||||
}
|
||||
|
||||
inline void set_value(expr * n, const mpz & r) {
|
||||
|
|
@ -290,12 +285,9 @@ public:
|
|||
}
|
||||
|
||||
// Update uplinks
|
||||
unsigned na = n->get_num_args();
|
||||
for (unsigned i = 0; i < na; i++) {
|
||||
expr * c = n->get_arg(i);
|
||||
for (auto c : *n)
|
||||
m_uplinks.insert_if_not_there(c, ptr_vector<expr>()).push_back(n);
|
||||
}
|
||||
|
||||
|
||||
func_decl * d = n->get_decl();
|
||||
|
||||
if (n->get_num_args() == 0) {
|
||||
|
|
@ -414,8 +406,7 @@ public:
|
|||
init_proc proc(m_manager, *this);
|
||||
expr_mark visited;
|
||||
unsigned sz = as.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * e = as[i];
|
||||
for (auto e : as) {
|
||||
if (!m_top_expr.contains(e))
|
||||
m_top_expr.insert(e);
|
||||
for_each_expr(proc, visited, e);
|
||||
|
|
@ -423,8 +414,7 @@ public:
|
|||
|
||||
visited.reset();
|
||||
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * e = as[i];
|
||||
for (auto e : as) {
|
||||
ptr_vector<func_decl> t;
|
||||
m_constants_occ.insert_if_not_there(e, t);
|
||||
find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e));
|
||||
|
|
@ -447,16 +437,14 @@ public:
|
|||
}
|
||||
|
||||
m_temp_seen.reset();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
{
|
||||
expr * e = as[i];
|
||||
for (auto e : as) {
|
||||
|
||||
// initialize weights
|
||||
if (!m_weights.contains(e))
|
||||
m_weights.insert(e, m_paws_init);
|
||||
|
||||
// positive/negative occurrences used for early pruning
|
||||
setup_occs(as[i]);
|
||||
setup_occs(e);
|
||||
}
|
||||
|
||||
// initialize ucb total touched value (individual ones are always initialized to 1)
|
||||
|
|
@ -629,7 +617,7 @@ public:
|
|||
}
|
||||
|
||||
void randomize(ptr_vector<expr> const & as) {
|
||||
TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
|
||||
TRACE("sls_verbose", tout << "Abandoned model:" << std::endl; show_model(tout); );
|
||||
|
||||
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
|
||||
func_decl * fd = it->m_key;
|
||||
|
|
@ -643,7 +631,7 @@ public:
|
|||
}
|
||||
|
||||
void reset(ptr_vector<expr> const & as) {
|
||||
TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
|
||||
TRACE("sls_verbose", tout << "Abandoned model:" << std::endl; show_model(tout); );
|
||||
|
||||
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
|
||||
set_value(it->m_value, m_zero);
|
||||
|
|
@ -656,11 +644,7 @@ public:
|
|||
if (m_manager.is_and(n) || m_manager.is_or(n))
|
||||
{
|
||||
SASSERT(!negated);
|
||||
app * a = to_app(n);
|
||||
expr * const * args = a->get_args();
|
||||
for (unsigned i = 0; i < a->get_num_args(); i++)
|
||||
{
|
||||
expr * child = args[i];
|
||||
for (auto child : *to_app(n)) {
|
||||
if (!m_temp_seen.contains(child))
|
||||
{
|
||||
setup_occs(child, false);
|
||||
|
|
@ -706,29 +690,22 @@ public:
|
|||
}
|
||||
else if (m_manager.is_and(n)) {
|
||||
SASSERT(!negated);
|
||||
app * a = to_app(n);
|
||||
expr * const * args = a->get_args();
|
||||
/* 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++)
|
||||
sum += get_score(args[i]);
|
||||
res = sum / (double) a->get_num_args(); */
|
||||
double min = 1.0;
|
||||
for (unsigned i = 0; i < a->get_num_args(); i++) {
|
||||
double cur = get_score(args[i]);
|
||||
if (cur < min) min = cur;
|
||||
}
|
||||
for (auto arg : *to_app(n))
|
||||
min = std::min(get_score(arg), min);
|
||||
|
||||
res = min;
|
||||
}
|
||||
else if (m_manager.is_or(n)) {
|
||||
SASSERT(!negated);
|
||||
app * a = to_app(n);
|
||||
expr * const * args = a->get_args();
|
||||
double max = 0.0;
|
||||
for (unsigned i = 0; i < a->get_num_args(); i++) {
|
||||
double cur = get_score(args[i]);
|
||||
if (cur > max) max = cur;
|
||||
}
|
||||
for (auto arg : *to_app(n))
|
||||
max = std::max(get_score(arg), max);
|
||||
res = max;
|
||||
}
|
||||
else if (m_manager.is_ite(n)) {
|
||||
|
|
@ -776,6 +753,7 @@ public:
|
|||
" ; SZ = " << bv_sz << std::endl; );
|
||||
m_mpz_manager.del(diff);
|
||||
m_mpz_manager.del(diff_m1);
|
||||
//verbose_stream() << "hamming distance: " << mk_bounded_pp(n, m_manager) << " := " << res << "\n";
|
||||
}
|
||||
else
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
|
@ -967,39 +945,35 @@ public:
|
|||
|
||||
ptr_vector<func_decl> & get_unsat_constants_gsat(ptr_vector<expr> const & as) {
|
||||
unsigned sz = as.size();
|
||||
if (sz == 1) {
|
||||
if (m_mpz_manager.neq(get_value(as[0]), m_one))
|
||||
return get_constants();
|
||||
}
|
||||
if (sz == 1 && m_mpz_manager.neq(get_value(as[0]), m_one))
|
||||
return get_constants();
|
||||
|
||||
m_temp_constants.reset();
|
||||
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * q = as[i];
|
||||
for (auto q : as) {
|
||||
if (m_mpz_manager.eq(get_value(q), m_one))
|
||||
continue;
|
||||
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(q);
|
||||
unsigned sz2 = this_decls.size();
|
||||
for (unsigned j = 0; j < sz2; j++) {
|
||||
func_decl * fd = this_decls[j];
|
||||
for (auto fd : this_decls)
|
||||
if (!m_temp_constants.contains(fd))
|
||||
m_temp_constants.push_back(fd);
|
||||
}
|
||||
m_temp_constants.push_back(fd);
|
||||
}
|
||||
TRACE("sls", tout << "candidates "; for (auto f : m_temp_constants) tout << f->get_name() << " "; tout << std::endl;);
|
||||
return m_temp_constants;
|
||||
}
|
||||
|
||||
ptr_vector<func_decl> & get_unsat_constants_walksat(expr * e) {
|
||||
if (!e || !m_temp_constants.empty())
|
||||
return m_temp_constants;
|
||||
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
|
||||
unsigned sz = this_decls.size();
|
||||
for (unsigned j = 0; j < sz; j++) {
|
||||
func_decl * fd = this_decls[j];
|
||||
if (!m_temp_constants.contains(fd))
|
||||
m_temp_constants.push_back(fd);
|
||||
}
|
||||
ptr_vector<func_decl>& get_unsat_constants_walksat(expr* e) {
|
||||
if (!e || !m_temp_constants.empty())
|
||||
return m_temp_constants;
|
||||
ptr_vector<func_decl> const& this_decls = m_constants_occ.find(e);
|
||||
for (auto fd : this_decls)
|
||||
if (!m_temp_constants.contains(fd))
|
||||
m_temp_constants.push_back(fd);
|
||||
|
||||
TRACE("sls", tout << "candidates " << mk_bounded_pp(e, m_manager) << " ";
|
||||
for (auto f : m_temp_constants) tout << f->get_name() << " "; tout << std::endl;);
|
||||
|
||||
return m_temp_constants;
|
||||
}
|
||||
|
||||
ptr_vector<func_decl> & get_unsat_constants(ptr_vector<expr> const & as) {
|
||||
|
|
|
|||
|
|
@ -33,7 +33,7 @@ namespace sls {
|
|||
|
||||
bool operator==(bvect const& a, bvect const& b) {
|
||||
SASSERT(a.nw > 0);
|
||||
return 0 == mpn_manager().compare(a.data(), a.nw, b.data(), a.nw);
|
||||
return 0 == memcmp(a.data(), b.data(), a.nw * sizeof(digit_t));
|
||||
}
|
||||
|
||||
bool operator<(bvect const& a, bvect const& b) {
|
||||
|
|
|
|||
|
|
@ -327,7 +327,7 @@ namespace sls {
|
|||
m_constraint_trail.push_back(e);
|
||||
add_clause(e);
|
||||
m_new_constraint = true;
|
||||
verbose_stream() << "add constraint\n";
|
||||
IF_VERBOSE(3, verbose_stream() << "add constraint " << mk_bounded_pp(e, m) << "\n");
|
||||
++m_stats.m_num_constraints;
|
||||
}
|
||||
|
||||
|
|
@ -565,8 +565,8 @@ namespace sls {
|
|||
SASSERT(m.is_true(get_value(e)) == is_true(v));
|
||||
}
|
||||
}
|
||||
);
|
||||
|
||||
);
|
||||
|
||||
m_repair_down.reserve(e->get_id() + 1);
|
||||
m_repair_up.reserve(e->get_id() + 1);
|
||||
if (!term(e->get_id()))
|
||||
|
|
|
|||
|
|
@ -684,17 +684,14 @@ namespace sls {
|
|||
|
||||
void seq_plugin::add_substr_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars) {
|
||||
// all consecutive subsequences of val_other
|
||||
map<zstring, bool, zstring_hash_proc, default_eq<zstring>> map;
|
||||
vector<zstring> subseqs;
|
||||
map.insert(zstring(""), true);
|
||||
subseqs.push_back(zstring(""));
|
||||
hashtable<zstring, zstring_hash_proc, default_eq<zstring>> 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 (map.contains(sub))
|
||||
if (set.contains(sub))
|
||||
break;
|
||||
map.insert(sub, true);
|
||||
subseqs.push_back(sub);
|
||||
set.insert(sub);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -702,7 +699,7 @@ namespace sls {
|
|||
if (is_value(x))
|
||||
continue;
|
||||
zstring const& a = strval0(x);
|
||||
for (auto& seq : subseqs) {
|
||||
for (auto& seq : set) {
|
||||
if (seq == a)
|
||||
continue;
|
||||
m_str_updates.push_back({ x, seq, 1 });
|
||||
|
|
|
|||
Loading…
Reference in a new issue