diff --git a/RELEASE_NOTES b/RELEASE_NOTES index ad2dcaf00..f185983a3 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -1,9 +1,13 @@ RELEASE NOTES -Version 4.3.3 +Version 4.4 ============= -- Fixed bug in floating point models +- New feature: Stochastic local search engine for bit-vector formulas (see the qfbv-sls tactic). + See also: Froehlich, Biere, Wintersteiger, Hamadi: Stochastic Local Search + for Satisfiability Modulo Theories, AAAI 2015. + +- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, and Codeplex users rsas, clockish, Heizmann. Version 4.3.2 ============= diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 5bbc42da8..9cfe797e6 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -9,7 +9,7 @@ from mk_util import * # Z3 Project definition def init_project_def(): - set_version(4, 3, 3, 0) + set_version(4, 4, 0, 0) add_lib('util', []) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index d48994861..677540991 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -66,7 +66,7 @@ class sat_tactic : public tactic { CASSERT("sat_solver", m_solver.check_invariant()); IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream());); TRACE("sat_dimacs", m_solver.display_dimacs(tout);); - + lbool r = m_solver.check(); if (r == l_false) { g->assert_expr(m.mk_false(), 0, 0); diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index 7a03224cf..5a4a6ff25 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -1091,7 +1091,7 @@ namespace smt { case_split_queue * mk_case_split_queue(context & ctx, smt_params & p) { if (p.m_relevancy_lvl < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { - warning_msg("relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5"); + warning_msg("relevancy must be enabled to use option CASE_SPLIT=3, 4 or 5"); p.m_case_split_strategy = CS_ACTIVITY; } if (p.m_auto_config && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 7053d63ec..163003c01 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -282,6 +282,7 @@ namespace smt { if (!m_fparams) { m_fparams = alloc(smt_params, m_context->get_fparams()); m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free + m_fparams->m_case_split_strategy = CS_ACTIVITY; // avoid warning messages about smt.case_split >= 3. } if (!m_aux_context) { symbol logic; diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp index 45fc868ac..770281923 100644 --- a/src/tactic/arith/probe_arith.cpp +++ b/src/tactic/arith/probe_arith.cpp @@ -198,11 +198,75 @@ struct is_non_qflira_functor { } }; +struct is_non_qfauflira_functor { + struct found {}; + ast_manager & m; + arith_util m_arith_util; + array_util m_array_util; + bool m_int; + bool m_real; + + is_non_qfauflira_functor(ast_manager & _m, bool _int, bool _real) : + m(_m), m_arith_util(_m), m_array_util(_m), m_int(_int), m_real(_real) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + bool compatible_sort(app * n) const { + if (m.is_bool(n)) + return true; + if (m_int && m_arith_util.is_int(n)) + return true; + if (m_real && m_arith_util.is_real(n)) + return true; + if (m_array_util.is_array(n)) + return true; + return false; + } + + void operator()(app * n) { + if (!compatible_sort(n)) + throw found(); + family_id fid = n->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == m_arith_util.get_family_id()) { + switch (n->get_decl_kind()) { + case OP_LE: case OP_GE: case OP_LT: case OP_GT: + case OP_ADD: case OP_NUM: + return; + case OP_MUL: + if (n->get_num_args() != 2) + throw found(); + if (!m_arith_util.is_numeral(n->get_arg(0))) + throw found(); + return; + case OP_TO_REAL: + if (!m_real) + throw found(); + break; + default: + throw found(); + } + return; + } + if (is_uninterp(n)) + return; + throw found(); + } +}; + static bool is_qflia(goal const & g) { is_non_qflira_functor p(g.m(), true, false); return !test(g, p); } +static bool is_qfauflia(goal const & g) { + is_non_qfauflira_functor p(g.m(), true, false); + return !test(g, p); +} + class is_qflia_probe : public probe { public: virtual result operator()(goal const & g) { @@ -210,6 +274,13 @@ public: } }; +class is_qfauflia_probe : public probe { +public: + virtual result operator()(goal const & g) { + return is_qfauflia(g); + } +}; + static bool is_qflra(goal const & g) { is_non_qflira_functor p(g.m(), false, true); return !test(g, p); @@ -289,6 +360,10 @@ probe * mk_is_qflia_probe() { return alloc(is_qflia_probe); } +probe * mk_is_qfauflia_probe() { + return alloc(is_qfauflia_probe); +} + probe * mk_is_qflra_probe() { return alloc(is_qflra_probe); } diff --git a/src/tactic/arith/probe_arith.h b/src/tactic/arith/probe_arith.h index 17e9efb28..83179098d 100644 --- a/src/tactic/arith/probe_arith.h +++ b/src/tactic/arith/probe_arith.h @@ -33,6 +33,7 @@ probe * mk_arith_max_degree_probe(); */ probe * mk_is_qflia_probe(); +probe * mk_is_qfauflia_probe(); probe * mk_is_qflra_probe(); probe * mk_is_qflira_probe(); probe * mk_is_ilp_probe(); @@ -40,6 +41,7 @@ probe * mk_is_mip_probe(); /* ADD_PROBE("is-qflia", "true if the goal is in QF_LIA.", "mk_is_qflia_probe()") + ADD_PROBE("is-qfauflia", "true if the goal is in QF_AUFLIA.", "mk_is_qfauflia_probe()") ADD_PROBE("is-qflra", "true if the goal is in QF_LRA.", "mk_is_qflra_probe()") ADD_PROBE("is-qflira", "true if the goal is in QF_LIRA.", "mk_is_qflira_probe()") ADD_PROBE("is-ilp", "true if the goal is ILP.", "mk_is_ilp_probe()") diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 9ecc16ecf..4bd82b969 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -28,10 +28,14 @@ Notes: #include"probe_arith.h" #include"quant_tactics.h" #include"qffpa_tactic.h" +#include"qfaufbv_tactic.h" +#include"qfauflia_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), + cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m), + cond(mk_is_qfauflia_probe(), mk_qfauflia_tactic(m), cond(mk_is_qflia_probe(), mk_qflia_tactic(m), cond(mk_is_qflra_probe(), mk_qflra_tactic(m), cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m), @@ -39,7 +43,7 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_lira_probe(), mk_lira_tactic(m, p), cond(mk_is_qffpabv_probe(), mk_qffpa_tactic(m, p), - mk_smt_tactic()))))))))), + mk_smt_tactic()))))))))))), p); return st; } diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index ae79446e3..586c3a349 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -41,7 +41,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const if (logic=="QF_UF") return mk_qfuf_tactic(m, p); else if (logic=="QF_BV") - return mk_qfbv_tactic(m, p); + return mk_qfbv_tactic(m, p); else if (logic=="QF_IDL") return mk_qfidl_tactic(m, p); else if (logic=="QF_LIA") diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp index 1a696dc78..30a62fb5c 100644 --- a/src/tactic/probe.cpp +++ b/src/tactic/probe.cpp @@ -316,6 +316,44 @@ probe * mk_is_qfbv_probe() { return alloc(is_qfbv_probe); } +struct is_non_qfaufbv_predicate { + struct found {}; + ast_manager & m; + bv_util m_bv_util; + array_util m_array_util; + + is_non_qfaufbv_predicate(ast_manager & _m) : m(_m), m_bv_util(_m), m_array_util(_m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + if (!m.is_bool(n) && !m_bv_util.is_bv(n) && !m_array_util.is_array(n)) + throw found(); + family_id fid = n->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == m_bv_util.get_family_id() || fid == m_array_util.get_family_id()) + return; + if (is_uninterp(n)) + return; + + throw found(); + } +}; + +class is_qfaufbv_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } +}; + +probe * mk_is_qfaufbv_probe() { + return alloc(is_qfaufbv_probe); +} + class num_consts_probe : public probe { bool m_bool; // If true, track only boolean constants. Otherwise, track only non boolean constants. char const * m_family; // (Ignored if m_bool == true), if != 0 and m_bool == true, then track only constants of the given family. diff --git a/src/tactic/probe.h b/src/tactic/probe.h index 2f61b340f..0cf8122e4 100644 --- a/src/tactic/probe.h +++ b/src/tactic/probe.h @@ -111,10 +111,12 @@ probe * mk_div(probe * p1, probe * p2); probe * mk_is_propositional_probe(); probe * mk_is_qfbv_probe(); +probe * mk_is_qfaufbv_probe(); /* ADD_PROBE("is-propositional", "true if the goal is in propositional logic.", "mk_is_propositional_probe()") ADD_PROBE("is-qfbv", "true if the goal is in QF_BV.", "mk_is_qfbv_probe()") + ADD_PROBE("is-qfaufbv", "true if the goal is in QF_AUFBV.", "mk_is_qfaufbv_probe()") */ #endif diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp new file mode 100644 index 000000000..c0c319ab4 --- /dev/null +++ b/src/tactic/sls/sls_engine.cpp @@ -0,0 +1,621 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + sls_engine.cpp + +Abstract: + + A Stochastic Local Search (SLS) engine + +Author: + + Christoph (cwinter) 2014-03-19 + +Notes: + +--*/ +#include +#include + +#include"map.h" +#include"ast_smt2_pp.h" +#include"ast_pp.h" +#include"var_subst.h" +#include"model_pp.h" +#include"tactic.h" +#include"cooperate.h" +#include"luby.h" + +#include"sls_params.hpp" +#include"sls_engine.h" + + +sls_engine::sls_engine(ast_manager & m, params_ref const & p) : + m_manager(m), + m_powers(m_mpz_manager), + m_zero(m_mpz_manager.mk_z(0)), + m_one(m_mpz_manager.mk_z(1)), + m_two(m_mpz_manager.mk_z(2)), + m_cancel(false), + m_bv_util(m), + m_tracker(m, m_bv_util, m_mpz_manager, m_powers), + m_evaluator(m, m_bv_util, m_tracker, m_mpz_manager, m_powers) +{ + updt_params(p); + m_tracker.updt_params(p); +} + +sls_engine::~sls_engine() { + m_mpz_manager.del(m_zero); + m_mpz_manager.del(m_one); + m_mpz_manager.del(m_two); +} + +void sls_engine::updt_params(params_ref const & _p) { + sls_params p(_p); + m_produce_models = _p.get_bool("model", false); + m_max_restarts = p.max_restarts(); + m_tracker.set_random_seed(p.random_seed()); + m_walksat = p.walksat(); + m_walksat_repick = p.walksat_repick(); + m_paws_sp = p.paws_sp(); + m_paws = m_paws_sp < 1024; + m_wp = p.wp(); + m_vns_mc = p.vns_mc(); + m_vns_repick = p.vns_repick(); + + m_restart_base = p.restart_base(); + m_restart_next = m_restart_base; + m_restart_init = p.restart_init(); + + m_early_prune = p.early_prune(); + m_random_offset = p.random_offset(); + m_rescore = p.rescore(); + + // Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT. + if (m_walksat_repick && !m_walksat) + NOT_IMPLEMENTED_YET(); + if (m_vns_repick && !m_walksat) + NOT_IMPLEMENTED_YET(); +} + +void sls_engine::checkpoint() { + if (m_cancel) + throw tactic_exception(TACTIC_CANCELED_MSG); + cooperate("sls"); +} + +bool sls_engine::full_eval(model & mdl) { + bool res = true; + + unsigned sz = m_assertions.size(); + for (unsigned i = 0; i < sz && res; i++) { + checkpoint(); + expr_ref o(m_manager); + + if (!mdl.eval(m_assertions[i], o, true)) + exit(ERR_INTERNAL_FATAL); + + res = m_manager.is_true(o.get()); + } + + TRACE("sls", tout << "Evaluation: " << res << std::endl;); + + return res; +} + +double sls_engine::top_score() { + double top_sum = 0.0; + unsigned sz = m_assertions.size(); + for (unsigned i = 0; i < sz; i++) { + expr * e = m_assertions[i]; + top_sum += m_tracker.get_score(e); + } + + TRACE("sls_top", tout << "Score distribution:"; + for (unsigned i = 0; i < sz; i++) + tout << " " << m_tracker.get_score(m_assertions[i]); + tout << " AVG: " << top_sum / (double)sz << std::endl;); + + m_tracker.set_top_sum(top_sum); + + return top_sum; +} + +double sls_engine::rescore() { + m_evaluator.update_all(); + m_stats.m_full_evals++; + return top_score(); +} + +double sls_engine::serious_score(func_decl * fd, const mpz & new_value) { + m_evaluator.serious_update(fd, new_value); + m_stats.m_incr_evals++; + return m_tracker.get_top_sum(); +} + +double sls_engine::incremental_score(func_decl * fd, const mpz & new_value) { + m_evaluator.update(fd, new_value); + m_stats.m_incr_evals++; + return m_tracker.get_top_sum(); +} + +double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value) { + m_stats.m_incr_evals++; + if (m_evaluator.update_prune(fd, new_value)) + return m_tracker.get_top_sum(); + else + return -DBL_MAX; +} + +// checks whether the score outcome of a given move is better than the previous score +bool sls_engine::what_if( + func_decl * fd, + const unsigned & fd_inx, + const mpz & temp, + double & best_score, + unsigned & best_const, + mpz & best_value) { + +#ifdef Z3DEBUG + mpz old_value; + m_mpz_manager.set(old_value, m_tracker.get_value(fd)); +#endif + + double r; + if (m_early_prune) + r = incremental_score_prune(fd, temp); + else + r = incremental_score(fd, temp); +#ifdef Z3DEBUG + TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << + " --> " << r << std::endl;); + + m_mpz_manager.del(old_value); +#endif + + // Andreas: Had this idea on my last day. Maybe we could add a noise here similar to the one that worked so well for ucb assertion selection. + // r += 0.0001 * m_tracker.get_random_uint(8); + + // Andreas: For some reason it is important to use > here instead of >=. Probably related to prefering the LSB. + if (r > best_score) { + best_score = r; + best_const = fd_inx; + m_mpz_manager.set(best_value, temp); + return true; + } + + return false; +} + +void sls_engine::mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result) { + mpz temp, mask, mask2; + m_mpz_manager.add(old_value, add_value, temp); + m_mpz_manager.set(mask, m_powers(bv_sz)); + m_mpz_manager.bitwise_not(bv_sz, mask, mask2); + m_mpz_manager.bitwise_and(temp, mask2, result); + m_mpz_manager.del(temp); + m_mpz_manager.del(mask); + m_mpz_manager.del(mask2); + +} + +void sls_engine::mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented) { + unsigned shift; + m_mpz_manager.add(old_value, m_one, incremented); + if (m_mpz_manager.is_power_of_two(incremented, shift) && shift == bv_sz) + m_mpz_manager.set(incremented, m_zero); +} + +void sls_engine::mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented) { + if (m_mpz_manager.is_zero(old_value)) { + m_mpz_manager.set(decremented, m_powers(bv_sz)); + m_mpz_manager.dec(decremented); + } + else + m_mpz_manager.sub(old_value, m_one, decremented); +} + +void sls_engine::mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted) { + m_mpz_manager.bitwise_not(bv_sz, old_value, inverted); +} + +void sls_engine::mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped) { + m_mpz_manager.set(flipped, m_zero); + + if (m_bv_util.is_bv_sort(s)) { + mpz mask; + m_mpz_manager.set(mask, m_powers(bit)); + m_mpz_manager.bitwise_xor(old_value, mask, flipped); + m_mpz_manager.del(mask); + } + else if (m_manager.is_bool(s)) + m_mpz_manager.set(flipped, (m_mpz_manager.is_zero(old_value)) ? m_one : m_zero); + else + NOT_IMPLEMENTED_YET(); +} + +void sls_engine::mk_random_move(ptr_vector & unsat_constants) +{ + unsigned rnd_mv = 0; + unsigned ucc = unsat_constants.size(); + unsigned rc = (m_tracker.get_random_uint((ucc < 16) ? 4 : (ucc < 256) ? 8 : (ucc < 4096) ? 12 : (ucc < 65536) ? 16 : 32)) % ucc; + func_decl * fd = unsat_constants[rc]; + + mpz new_value; + + sort * srt = fd->get_range(); + if (m_manager.is_bool(srt)) + m_mpz_manager.set(new_value, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero); + else + { + if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv = 2; + if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++; + + // Andreas: The other option would be to scale the probability for flips according to the bit-width. + /* unsigned bv_sz2 = m_bv_util.get_bv_size(srt); + rnd_mv = m_tracker.get_random_uint(16) % (bv_sz2 + 3); + if (rnd_mv > 3) rnd_mv = 0; */ + + move_type mt = (move_type)rnd_mv; + + // Andreas: Christoph claimed inversion doesn't make sense, let's do a flip instead. Is this really true? + if (mt == MV_INV) mt = MV_FLIP; + unsigned bit = 0; + + switch (mt) + { + case MV_FLIP: { + unsigned bv_sz = m_bv_util.get_bv_size(srt); + bit = (m_tracker.get_random_uint((bv_sz < 16) ? 4 : (bv_sz < 256) ? 8 : (bv_sz < 4096) ? 12 : (bv_sz < 65536) ? 16 : 32)) % bv_sz; + mk_flip(fd->get_range(), m_tracker.get_value(fd), bit, new_value); + break; + } + case MV_INC: + mk_inc(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); + break; + case MV_DEC: + mk_dec(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); + break; + case MV_INV: + mk_inv(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); + break; + default: + NOT_IMPLEMENTED_YET(); + } + + TRACE("sls", tout << "Randomization candidates: "; + for (unsigned i = 0; i < unsat_constants.size(); i++) + tout << unsat_constants[i]->get_name() << ", "; + tout << std::endl; + tout << "Random move: "; + switch (mt) { + case MV_FLIP: tout << "Flip #" << bit << " in " << fd->get_name() << std::endl; break; + case MV_INC: tout << "+1 for " << fd->get_name() << std::endl; break; + case MV_DEC: tout << "-1 for " << fd->get_name() << std::endl; break; + case MV_INV: tout << "NEG for " << fd->get_name() << std::endl; break; + } + tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout);); + } + + m_evaluator.serious_update(fd, new_value); + m_mpz_manager.del(new_value); +} + +// finds the move that increased score the most. returns best_const = -1, if no increasing move exists. +double sls_engine::find_best_move( + ptr_vector & to_evaluate, + double score, + unsigned & best_const, + mpz & best_value, + unsigned & new_bit, + move_type & move) +{ + mpz old_value, temp; + unsigned bv_sz; + double new_score = score; + + // Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list. + unsigned sz = to_evaluate.size(); + unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0; + for (unsigned j = 0; j < sz; j++) { + unsigned i = j + offset; + if (i >= sz) i -= sz; + //for (unsigned i = 0; i < to_evaluate.size(); i++) { + func_decl * fd = to_evaluate[i]; + sort * srt = fd->get_range(); + bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); + m_mpz_manager.set(old_value, m_tracker.get_value(fd)); + + // first try to flip every bit + for (unsigned j = 0; j < bv_sz; j++) { + // What would happen if we flipped bit #i ? + mk_flip(srt, old_value, j, temp); + + if (what_if(fd, i, temp, new_score, best_const, best_value)) { + new_bit = j; + move = MV_FLIP; + } + } + + if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) { + if (!m_mpz_manager.is_even(old_value)) { + // for odd values, try +1 + mk_inc(bv_sz, old_value, temp); + if (what_if(fd, i, temp, new_score, best_const, best_value)) + move = MV_INC; + } + else { + // for even values, try -1 + mk_dec(bv_sz, old_value, temp); + if (what_if(fd, i, temp, new_score, best_const, best_value)) + move = MV_DEC; + } + // try inverting + mk_inv(bv_sz, old_value, temp); + if (what_if(fd, i, temp, new_score, best_const, best_value)) + move = MV_INV; + } + // reset to what it was before + incremental_score(fd, old_value); + } + + m_mpz_manager.del(old_value); + m_mpz_manager.del(temp); + + return new_score; +} + +// finds the move that increased score the most. returns best_const = -1, if no increasing move exists. +double sls_engine::find_best_move_mc(ptr_vector & to_evaluate, double score, + unsigned & best_const, mpz & best_value) { + mpz old_value, temp, temp2; + unsigned bv_sz; + double new_score = score; + + // Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list. + unsigned sz = to_evaluate.size(); + unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0; + for (unsigned j = 0; j < sz; j++) { + unsigned i = j + offset; + if (i >= sz) i -= sz; + //for (unsigned i = 0; i < to_evaluate.size(); i++) { + func_decl * fd = to_evaluate[i]; + sort * srt = fd->get_range(); + bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); + m_mpz_manager.set(old_value, m_tracker.get_value(fd)); + + if (m_bv_util.is_bv_sort(srt) && bv_sz > 2) { + for (unsigned j = 0; j < bv_sz; j++) { + mk_flip(srt, old_value, j, temp); + for (unsigned l = 0; l < m_vns_mc && l < bv_sz / 2; l++) + { + unsigned k = m_tracker.get_random_uint(16) % bv_sz; + while (k == j) + k = m_tracker.get_random_uint(16) % bv_sz; + mk_flip(srt, temp, k, temp2); + what_if(fd, i, temp2, new_score, best_const, best_value); + } + } + } + // reset to what it was before + incremental_score(fd, old_value); + } + + m_mpz_manager.del(old_value); + m_mpz_manager.del(temp); + m_mpz_manager.del(temp2); + + return new_score; +} + +// main search loop +lbool sls_engine::search() { + lbool res = l_undef; + double score = 0.0, old_score = 0.0; + unsigned new_const = (unsigned)-1, new_bit; + mpz new_value; + move_type move; + + score = rescore(); + unsigned sz = m_assertions.size(); + + while (check_restart(m_stats.m_moves)) { + checkpoint(); + m_stats.m_moves++; + + // Andreas: Every base restart interval ... + if (m_stats.m_moves % m_restart_base == 0) + { + // ... potentially smooth the touched counters ... + m_tracker.ucb_forget(m_assertions); + // ... or normalize the top-level score. + if (m_rescore) score = rescore(); + } + + // get candidate variables + ptr_vector & to_evaluate = m_tracker.get_unsat_constants(m_assertions); + if (!to_evaluate.size()) + { + res = l_true; + goto bailout; + } + + // random walk with probability wp / 1024 + if (m_wp && m_tracker.get_random_uint(10) < m_wp) + { + mk_random_move(to_evaluate); + score = m_tracker.get_top_sum(); + continue; + } + + old_score = score; + new_const = (unsigned)-1; + + // find best increasing move + score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move); + + // use Monte Carlo 2-bit-flip sampling if no increasing move was found previously + if (m_vns_mc && (new_const == static_cast(-1))) + score = find_best_move_mc(to_evaluate, score, new_const, new_value); + + // repick assertion if no increasing move was found previously + if (m_vns_repick && (new_const == static_cast(-1))) + { + expr * q = m_tracker.get_new_unsat_assertion(m_assertions); + // only apply if another unsatisfied assertion actually exists + if (q) + { + ptr_vector & to_evaluate2 = m_tracker.get_unsat_constants_walksat(q); + score = find_best_move(to_evaluate2, score, new_const, new_value, new_bit, move); + + if (new_const != static_cast(-1)) { + func_decl * fd = to_evaluate2[new_const]; + score = serious_score(fd, new_value); + continue; + } + } + } + + // randomize if no increasing move was found + if (new_const == static_cast(-1)) { + score = old_score; + if (m_walksat_repick) + m_evaluator.randomize_local(m_assertions); + else + m_evaluator.randomize_local(to_evaluate); + + score = m_tracker.get_top_sum(); + + // update assertion weights if a weigthing is enabled (sp < 1024) + if (m_paws) + { + for (unsigned i = 0; i < sz; i++) + { + expr * q = m_assertions[i]; + // 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)) + m_tracker.decrease_weight(q); + } + // increase weights otherwise + else + { + if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero)) + m_tracker.increase_weight(q); + } + } + } + } + // otherwise, apply most increasing move + else { + func_decl * fd = to_evaluate[new_const]; + score = serious_score(fd, new_value); + } + } + +bailout: + m_mpz_manager.del(new_value); + + return res; +} + +void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { + if (g->inconsistent()) { + mc = 0; + return; + } + + m_produce_models = g->models_enabled(); + + for (unsigned i = 0; i < g->size(); i++) + assert_expr(g->form(i)); + + lbool res = operator()(); + + if (res == l_true) { + report_tactic_progress("Number of flips:", m_stats.m_moves); + for (unsigned i = 0; i < g->size(); i++) + if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) + { + verbose_stream() << "Terminated before all assertions were SAT!" << std::endl; + NOT_IMPLEMENTED_YET(); + } + + if (m_produce_models) { + model_ref mdl = m_tracker.get_model(); + mc = model2model_converter(mdl.get()); + TRACE("sls_model", mc->display(tout);); + } + g->reset(); + } + else + mc = 0; +} + +lbool sls_engine::operator()() { + m_tracker.initialize(m_assertions); + lbool res = l_undef; + + do { + checkpoint(); + + report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts); + res = search(); + + if (res == l_undef) + { + if (m_restart_init) + m_tracker.randomize(m_assertions); + else + m_tracker.reset(m_assertions); + } + } while (res != l_true && m_stats.m_restarts++ < m_max_restarts); + + verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " time: " << std::fixed << std::setprecision(2) << m_stats.m_stopwatch.get_current_seconds() << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl; + + return res; +} + +/* Andreas: Needed for Armin's restart scheme if we don't want to use loops. +double sls_engine::get_restart_armin(unsigned cnt_restarts) +{ + unsigned outer_id = (unsigned)(0.5 + sqrt(0.25 + 2 * cnt_restarts)); + unsigned inner_id = cnt_restarts - (outer_id - 1) * outer_id / 2; + return pow((double) _RESTART_CONST_ARMIN_, (int) inner_id + 1); +} +*/ + +unsigned sls_engine::check_restart(unsigned curr_value) +{ + if (curr_value > m_restart_next) + { + /* Andreas: My own scheme (= 1) seems to work best. Other schemes are disabled so that we save one parameter. + I leave the other versions as comments in case you want to try it again somewhen. +#if _RESTART_SCHEME_ == 5 + m_restart_next += (unsigned)(m_restart_base * pow(_RESTART_CONST_ARMIN_, m_stats.m_restarts)); +#elif _RESTART_SCHEME_ == 4 + m_restart_next += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? m_restart_base : (m_restart_base * m_stats.m_restarts + 1); +#elif _RESTART_SCHEME_ == 3 + m_restart_next += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * m_restart_base; +#elif _RESTART_SCHEME_ == 2 + m_restart_next += get_luby(m_stats.m_restarts + 1) * m_restart_base; +#elif _RESTART_SCHEME_ == 1 + if (m_stats.m_restarts & 1) + m_restart_next += m_restart_base; + else + m_restart_next += (2 << (m_stats.m_restarts >> 1)) * m_restart_base; +#else + m_restart_limit += m_restart_base; +#endif */ + if (m_stats.m_restarts & 1) + m_restart_next += m_restart_base; + else + m_restart_next += (2 << (m_stats.m_restarts >> 1)) * m_restart_base; + return 0; + } + return 1; +} diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h new file mode 100644 index 000000000..b056c438e --- /dev/null +++ b/src/tactic/sls/sls_engine.h @@ -0,0 +1,143 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + sls_engine.h + +Abstract: + + A Stochastic Local Search (SLS) engine + +Author: + + Christoph (cwinter) 2014-03-19 + +Notes: + +--*/ +#ifndef _SLS_ENGINE_H_ +#define _SLS_ENGINE_H_ + +#include"stopwatch.h" +#include"lbool.h" +#include"model_converter.h" +#include"goal.h" + +#include"sls_tracker.h" +#include"sls_evaluator.h" + +class sls_engine { +public: + class stats { + public: + unsigned m_restarts; + stopwatch m_stopwatch; + unsigned m_full_evals; + unsigned m_incr_evals; + unsigned m_moves, m_flips, m_incs, m_decs, m_invs; + + stats() : + m_restarts(0), + m_full_evals(0), + m_incr_evals(0), + m_moves(0), + m_flips(0), + m_incs(0), + m_decs(0), + m_invs(0) { + m_stopwatch.reset(); + m_stopwatch.start(); + } + void reset() { + m_full_evals = m_flips = m_incr_evals = 0; + m_stopwatch.reset(); + m_stopwatch.start(); + } + }; + +protected: + ast_manager & m_manager; + stats m_stats; + unsynch_mpz_manager m_mpz_manager; + powers m_powers; + mpz m_zero, m_one, m_two; + bool m_produce_models; + volatile bool m_cancel; + bv_util m_bv_util; + sls_tracker m_tracker; + sls_evaluator m_evaluator; + ptr_vector m_assertions; + + unsigned m_max_restarts; + unsigned m_walksat; + unsigned m_walksat_repick; + unsigned m_wp; + unsigned m_vns_mc; + unsigned m_vns_repick; + unsigned m_paws; + unsigned m_paws_sp; + unsigned m_restart_base; + unsigned m_restart_next; + unsigned m_restart_init; + unsigned m_early_prune; + unsigned m_random_offset; + unsigned m_rescore; + + typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type; + +public: + sls_engine(ast_manager & m, params_ref const & p); + ~sls_engine(); + + ast_manager & m() const { return m_manager; } + + void set_cancel(bool f) { m_cancel = f; } + void cancel() { set_cancel(true); } + void reset_cancel() { set_cancel(false); } + + void updt_params(params_ref const & _p); + + void assert_expr(expr * e) { m_assertions.push_back(e); } + + stats const & get_stats(void) { return m_stats; } + void reset_statistics(void) { m_stats.reset(); } + + bool full_eval(model & mdl); + + void mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result); + void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented); + void mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented); + void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted); + void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped); + + lbool search(void); + + lbool operator()(); + void operator()(goal_ref const & g, model_converter_ref & mc); + +protected: + void checkpoint(); + + bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, + double & best_score, unsigned & best_const, mpz & best_value); + + double top_score(); + double rescore(); + double serious_score(func_decl * fd, const mpz & new_value); + double incremental_score(func_decl * fd, const mpz & new_value); + + double incremental_score_prune(func_decl * fd, const mpz & new_value); + double find_best_move(ptr_vector & to_evaluate, double score, + unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move); + + double find_best_move_mc(ptr_vector & to_evaluate, double score, + unsigned & best_const, mpz & best_value); + + void mk_random_move(ptr_vector & unsat_constants); + + //double get_restart_armin(unsigned cnt_restarts); + unsigned check_restart(unsigned curr_value); +}; + +#endif diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 77ff50454..61afb7457 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -20,6 +20,8 @@ Notes: #ifndef _SLS_EVALUATOR_H_ #define _SLS_EVALUATOR_H_ +#include"model_evaluator.h" + #include"sls_powers.h" #include"sls_tracker.h" @@ -34,6 +36,7 @@ class sls_evaluator { powers & m_powers; expr_ref_buffer m_temp_exprs; vector > m_traversal_stack; + vector > m_traversal_stack_bool; public: sls_evaluator(ast_manager & m, bv_util & bvu, sls_tracker & t, unsynch_mpz_manager & mm, powers & p) : @@ -93,7 +96,7 @@ public: SASSERT(n_args == 1); const mpz & child = m_tracker.get_value(args[0]); SASSERT(m_mpz_manager.is_one(child) || m_mpz_manager.is_zero(child)); - m_mpz_manager.set(result, (m_mpz_manager.is_zero(child)) ? m_one : m_zero); + m_mpz_manager.set(result, (m_mpz_manager.is_zero(child)) ? m_one : m_zero); break; } case OP_EQ: { @@ -519,11 +522,13 @@ public: } } - void run_update(unsigned cur_depth) { + void run_serious_update(unsigned cur_depth) { // precondition: m_traversal_stack contains the entry point(s) expr_fast_mark1 visited; mpz new_value; + double new_score; + SASSERT(cur_depth < m_traversal_stack.size()); while (cur_depth != static_cast(-1)) { ptr_vector & cur_depth_exprs = m_traversal_stack[cur_depth]; @@ -533,8 +538,61 @@ public: (*this)(to_app(cur), new_value); m_tracker.set_value(cur, new_value); - m_tracker.set_score(cur, m_tracker.score(cur)); + new_score = m_tracker.score(cur); + if (m_tracker.is_top_expr(cur)) + { + m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); + if (m_mpz_manager.eq(new_value,m_one)) + m_tracker.make_assertion(cur); + else + m_tracker.break_assertion(cur); + } + + m_tracker.set_score(cur, new_score); + m_tracker.set_score_prune(cur, new_score); + + if (m_tracker.has_uplinks(cur)) { + ptr_vector & ups = m_tracker.get_uplinks(cur); + for (unsigned j = 0; j < ups.size(); j++) { + expr * next = ups[j]; + unsigned next_d = m_tracker.get_distance(next); + SASSERT(next_d < cur_depth); + if (!visited.is_marked(next)) { + m_traversal_stack[next_d].push_back(next); + visited.mark(next); + } + } + } + } + + cur_depth_exprs.reset(); + cur_depth--; + } + + m_mpz_manager.del(new_value); + } + + void run_update(unsigned cur_depth) { + // precondition: m_traversal_stack contains the entry point(s) + expr_fast_mark1 visited; + mpz new_value; + + double new_score; + + SASSERT(cur_depth < m_traversal_stack.size()); + while (cur_depth != static_cast(-1)) { + ptr_vector & cur_depth_exprs = m_traversal_stack[cur_depth]; + + for (unsigned i = 0; i < cur_depth_exprs.size(); i++) { + expr * cur = cur_depth_exprs[i]; + + (*this)(to_app(cur), new_value); + m_tracker.set_value(cur, new_value); + new_score = m_tracker.score(cur); + if (m_tracker.is_top_expr(cur)) + m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); + m_tracker.set_score(cur, new_score); if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); for (unsigned j = 0; j < ups.size(); j++) { @@ -569,8 +627,7 @@ public: m_traversal_stack[cur_depth].push_back(ep); if (cur_depth > max_depth) max_depth = cur_depth; } - - run_update(max_depth); + run_serious_update(max_depth); } void update(func_decl * fd, const mpz & new_value) { @@ -584,36 +641,174 @@ public: run_update(cur_depth); } - void randomize_local(goal_ref const & g) { - ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g); + void serious_update(func_decl * fd, const mpz & new_value) { + m_tracker.set_value(fd, new_value); + expr * ep = m_tracker.get_entry_point(fd); + unsigned cur_depth = m_tracker.get_distance(ep); + if (m_traversal_stack.size() <= cur_depth) + m_traversal_stack.resize(cur_depth+1); + m_traversal_stack[cur_depth].push_back(ep); - // Randomize _all_ candidates: + run_serious_update(cur_depth); + } - //// bool did_something = false; - //for (unsigned i = 0; i < unsat_constants.size(); i++) { - // func_decl * fd = unsat_constants[i]; - // mpz temp = m_tracker.get_random(fd->get_range()); - // // if (m_mpz_manager.neq(temp, m_tracker.get_value(fd))) { - // // did_something = true; - // // } - // update(fd, temp); - // m_mpz_manager.del(temp); - //} + unsigned run_update_bool_prune(unsigned cur_depth) { + expr_fast_mark1 visited; + double prune_score, new_score; + unsigned pot_benefits = 0; + SASSERT(cur_depth < m_traversal_stack_bool.size()); + + ptr_vector & cur_depth_exprs = m_traversal_stack_bool[cur_depth]; + + for (unsigned i = 0; i < cur_depth_exprs.size(); i++) { + expr * cur = cur_depth_exprs[i]; + + new_score = m_tracker.score(cur); + if (m_tracker.is_top_expr(cur)) + m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); + + prune_score = m_tracker.get_score_prune(cur); + m_tracker.set_score(cur, new_score); + + if ((new_score > prune_score) && (m_tracker.has_pos_occ(cur))) + pot_benefits = 1; + if ((new_score <= prune_score) && (m_tracker.has_neg_occ(cur))) + pot_benefits = 1; + + if (m_tracker.has_uplinks(cur)) { + ptr_vector & ups = m_tracker.get_uplinks(cur); + for (unsigned j = 0; j < ups.size(); j++) { + expr * next = ups[j]; + unsigned next_d = m_tracker.get_distance(next); + SASSERT(next_d < cur_depth); + if (!visited.is_marked(next)) { + m_traversal_stack_bool[next_d].push_back(next); + visited.mark(next); + } + } + } + } + + cur_depth_exprs.reset(); + cur_depth--; + + while (cur_depth != static_cast(-1)) { + ptr_vector & cur_depth_exprs = m_traversal_stack_bool[cur_depth]; + if (pot_benefits) + { + unsigned cur_size = cur_depth_exprs.size(); + for (unsigned i = 0; i < cur_size; i++) { + expr * cur = cur_depth_exprs[i]; + + new_score = m_tracker.score(cur); + if (m_tracker.is_top_expr(cur)) + m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); + m_tracker.set_score(cur, new_score); + + if (m_tracker.has_uplinks(cur)) { + ptr_vector & ups = m_tracker.get_uplinks(cur); + for (unsigned j = 0; j < ups.size(); j++) { + expr * next = ups[j]; + unsigned next_d = m_tracker.get_distance(next); + SASSERT(next_d < cur_depth); + if (!visited.is_marked(next)) { + m_traversal_stack_bool[next_d].push_back(next); + visited.mark(next); + } + } + } + } + } + cur_depth_exprs.reset(); + cur_depth--; + } + + return pot_benefits; + } + + void run_update_prune(unsigned max_depth) { + // precondition: m_traversal_stack contains the entry point(s) + expr_fast_mark1 visited; + mpz new_value; + + unsigned cur_depth = max_depth; + SASSERT(cur_depth < m_traversal_stack.size()); + while (cur_depth != static_cast(-1)) { + ptr_vector & cur_depth_exprs = m_traversal_stack[cur_depth]; + + for (unsigned i = 0; i < cur_depth_exprs.size(); i++) { + expr * cur = cur_depth_exprs[i]; + + (*this)(to_app(cur), new_value); + m_tracker.set_value(cur, new_value); + // Andreas: Should actually always have uplinks ... + if (m_tracker.has_uplinks(cur)) { + ptr_vector & ups = m_tracker.get_uplinks(cur); + for (unsigned j = 0; j < ups.size(); j++) { + expr * next = ups[j]; + unsigned next_d = m_tracker.get_distance(next); + SASSERT(next_d < cur_depth); + if (!visited.is_marked(next)) { + if (m_manager.is_bool(next)) + m_traversal_stack_bool[max_depth].push_back(next); + else + m_traversal_stack[next_d].push_back(next); + visited.mark(next); + } + } + } + } + + cur_depth_exprs.reset(); + cur_depth--; + } + + m_mpz_manager.del(new_value); + } + + unsigned update_prune(func_decl * fd, const mpz & new_value) { + m_tracker.set_value(fd, new_value); + expr * ep = m_tracker.get_entry_point(fd); + unsigned cur_depth = m_tracker.get_distance(ep); + + if (m_traversal_stack_bool.size() <= cur_depth) + m_traversal_stack_bool.resize(cur_depth+1); + if (m_traversal_stack.size() <= cur_depth) + m_traversal_stack.resize(cur_depth+1); + + if (m_manager.is_bool(ep)) + m_traversal_stack_bool[cur_depth].push_back(ep); + else + { + m_traversal_stack[cur_depth].push_back(ep); + run_update_prune(cur_depth); + } + return run_update_bool_prune(cur_depth); + } + + void randomize_local(ptr_vector & unsat_constants) { // Randomize _one_ candidate: unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size(); func_decl * fd = unsat_constants[r]; mpz temp = m_tracker.get_random(fd->get_range()); - update(fd, temp); + + serious_update(fd, temp); + m_mpz_manager.del(temp); - TRACE("sls", /*tout << "Randomization candidates: "; - for (unsigned i = 0; i < unsat_constants.size(); i++) - tout << unsat_constants[i]->get_name() << ", "; - tout << std::endl;*/ - tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl; + TRACE("sls", tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl; tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout); ); + + } + + void randomize_local(expr * e) { + randomize_local(m_tracker.get_constants(e)); + } + + void randomize_local(ptr_vector const & as) { + randomize_local(m_tracker.get_unsat_constants(as)); } }; diff --git a/src/tactic/sls/sls_params.pyg b/src/tactic/sls/sls_params.pyg index cc3e05966..bf5bd181a 100644 --- a/src/tactic/sls/sls_params.pyg +++ b/src/tactic/sls/sls_params.pyg @@ -2,7 +2,25 @@ def_module_params('sls', export=True, description='Experimental Stochastic Local Search Solver (for QFBV only).', params=(max_memory_param(), - ('restarts', UINT, UINT_MAX, '(max) number of restarts'), - ('plateau_limit', UINT, 10, 'pleateau limit'), - ('random_seed', UINT, 0, 'random seed') + ('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'), + ('walksat', BOOL, 1, 'use walksat assertion selection (instead of gsat)'), + ('walksat_ucb', BOOL, 1, 'use bandit heuristic for walksat assertion selection (instead of random)'), + ('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'), + ('walksat_ucb_init', BOOL, 0, 'initialize total ucb touched to formula size'), + ('walksat_ucb_forget', DOUBLE, 1.0, 'scale touched by this factor every base restart interval'), + ('walksat_ucb_noise', DOUBLE, 0.0002, 'add noise 0 <= 256 * ucb_noise to ucb score for assertion selection'), + ('walksat_repick', BOOL, 1, 'repick assertion if randomizing in local minima'), + ('scale_unsat', DOUBLE, 0.5, 'scale score of unsat expressions by this factor'), + ('paws_init', UINT, 40, 'initial/minimum assertion weights'), + ('paws_sp', UINT, 52, 'smooth assertion weights with probability paws_sp / 1024'), + ('wp', UINT, 100, 'random walk with probability wp / 1024'), + ('vns_mc', UINT, 0, 'in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit'), + ('vns_repick', BOOL, 0, 'in local minima, try picking a different assertion (only for walksat)'), + ('restart_base', UINT, 100, 'base restart interval given by moves per run'), + ('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'), + ('early_prune', BOOL, 1, 'use early pruning for score prediction'), + ('random_offset', BOOL, 1, 'use random offset for candidate evaluation'), + ('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'), + ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'), + ('random_seed', UINT, 0, 'random seed') )) diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 6783d9621..b06a047f7 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -16,507 +16,30 @@ Author: Notes: --*/ -#include -#include"map.h" #include"nnf.h" -#include"cooperate.h" -#include"ast_smt2_pp.h" -#include"ast_pp.h" -#include"var_subst.h" -#include"model_pp.h" -#include"model_evaluator.h" #include"solve_eqs_tactic.h" -#include"elim_uncnstr_tactic.h" #include"bv_size_reduction_tactic.h" #include"max_bv_sharing_tactic.h" #include"simplify_tactic.h" -#include"stopwatch.h" #include"propagate_values_tactic.h" -#include"sls_tactic.h" +#include"ctx_simplify_tactic.h" +#include"elim_uncnstr_tactic.h" #include"nnf_tactic.h" - +#include"stopwatch.h" +#include"sls_tactic.h" #include"sls_params.hpp" -#include"sls_evaluator.h" -#include"sls_tracker.h" +#include"sls_engine.h" -class sls_tactic : public tactic { - class stats { - public: - unsigned m_restarts; - stopwatch m_stopwatch; - unsigned m_full_evals; - unsigned m_incr_evals; - unsigned m_moves, m_flips, m_incs, m_decs, m_invs; - stats() : - m_restarts(0), - m_full_evals(0), - m_incr_evals(0), - m_moves(0), - m_flips(0), - m_incs(0), - m_decs(0), - m_invs(0) { - m_stopwatch.reset(); - m_stopwatch.start(); - } - void reset() { - m_full_evals = m_flips = m_incr_evals = 0; - m_stopwatch.reset(); - m_stopwatch.start(); - } - }; - - struct imp { - ast_manager & m_manager; - stats & m_stats; - unsynch_mpz_manager m_mpz_manager; - powers m_powers; - mpz m_zero, m_one, m_two; - bool m_produce_models; - volatile bool m_cancel; - bv_util m_bv_util; - sls_tracker m_tracker; - sls_evaluator m_evaluator; - - unsigned m_max_restarts; - unsigned m_plateau_limit; - - typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type; - - imp(ast_manager & m, params_ref const & p, stats & s) : - m_manager(m), - m_stats(s), - m_powers(m_mpz_manager), - m_zero(m_mpz_manager.mk_z(0)), - m_one(m_mpz_manager.mk_z(1)), - m_two(m_mpz_manager.mk_z(2)), - m_cancel(false), - m_bv_util(m), - m_tracker(m, m_bv_util, m_mpz_manager, m_powers), - m_evaluator(m, m_bv_util, m_tracker, m_mpz_manager, m_powers) - { - updt_params(p); - } - - ~imp() { - m_mpz_manager.del(m_zero); - m_mpz_manager.del(m_one); - m_mpz_manager.del(m_two); - } - - ast_manager & m() const { return m_manager; } - - void set_cancel(bool f) { m_cancel = f; } - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } - - static void collect_param_descrs(param_descrs & r) { - sls_params::collect_param_descrs(r); - } - - void updt_params(params_ref const & _p) { - sls_params p(_p); - m_produce_models = _p.get_bool("model", false); - m_max_restarts = p.restarts(); - m_tracker.set_random_seed(p.random_seed()); - m_plateau_limit = p.plateau_limit(); - } - - void checkpoint() { - if (m_cancel) - throw tactic_exception(TACTIC_CANCELED_MSG); - cooperate("sls"); - } - - bool full_eval(goal_ref const & g, model & mdl) { - bool res = true; - - unsigned sz = g->size(); - for (unsigned i = 0; i < sz && res; i++) { - checkpoint(); - expr_ref o(m_manager); - - if (!mdl.eval(g->form(i), o, true)) - exit(ERR_INTERNAL_FATAL); - - res = m_manager.is_true(o.get()); - } - - TRACE("sls", tout << "Evaluation: " << res << std::endl;); - - return res; - } - - double top_score(goal_ref const & g) { - #if 0 - double min = m_tracker.get_score(g->form(0)); - unsigned sz = g->size(); - for (unsigned i = 1; i < sz; i++) { - double q = m_tracker.get_score(g->form(i)); - if (q < min) min = q; - } - TRACE("sls_top", tout << "Score distribution:"; - for (unsigned i = 0; i < sz; i++) - tout << " " << m_tracker.get_score(g->form(i)); - tout << " MIN: " << min << std::endl; ); - return min; - #else - double top_sum = 0.0; - unsigned sz = g->size(); - for (unsigned i = 0; i < sz; i++) { - top_sum += m_tracker.get_score(g->form(i)); - } - TRACE("sls_top", tout << "Score distribution:"; - for (unsigned i = 0; i < sz; i++) - tout << " " << m_tracker.get_score(g->form(i)); - tout << " AVG: " << top_sum / (double) sz << std::endl; ); - return top_sum / (double) sz; - #endif - } - - double rescore(goal_ref const & g) { - m_evaluator.update_all(); - m_stats.m_full_evals++; - return top_score(g); - } - - double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value) { - m_evaluator.update(fd, new_value); - m_stats.m_incr_evals++; - return top_score(g); - } - - bool what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp, - double & best_score, unsigned & best_const, mpz & best_value) { - - #ifdef Z3DEBUG - mpz old_value; - m_mpz_manager.set(old_value, m_tracker.get_value(fd)); - #endif - - double r = incremental_score(g, fd, temp); - - #ifdef Z3DEBUG - TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << - " --> " << r << std::endl; ); - - m_mpz_manager.del(old_value); - #endif - - if (r >= best_score) { - best_score = r; - best_const = fd_inx; - m_mpz_manager.set(best_value, temp); - return true; - } - - return false; - } - - void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented) { - unsigned shift; - m_mpz_manager.add(old_value, m_one, incremented); - if (m_mpz_manager.is_power_of_two(incremented, shift) && shift == bv_sz) - m_mpz_manager.set(incremented, m_zero); - } - - void mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented) { - if (m_mpz_manager.is_zero(old_value)) { - m_mpz_manager.set(decremented, m_powers(bv_sz)); - m_mpz_manager.dec(decremented); - } - else - m_mpz_manager.sub(old_value, m_one, decremented); - } - - void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted) { - m_mpz_manager.bitwise_not(bv_sz, old_value, inverted); - } - - void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped) { - m_mpz_manager.set(flipped, m_zero); - - if (m_bv_util.is_bv_sort(s)) { - mpz mask; - m_mpz_manager.set(mask, m_powers(bit)); - m_mpz_manager.bitwise_xor(old_value, mask, flipped); - m_mpz_manager.del(mask); - } - else if (m_manager.is_bool(s)) - m_mpz_manager.set(flipped, (m_mpz_manager.is_zero(old_value)) ? m_one : m_zero); - else - NOT_IMPLEMENTED_YET(); - } - - void mk_random_move(goal_ref const & g) { - unsigned rnd_mv = 0; - if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv=2; - if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++; - move_type mt = (move_type) rnd_mv; - - // inversion doesn't make sense, let's do a flip instead. - if (mt == MV_INV) mt = MV_FLIP; - - ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g); - unsigned ucc = unsat_constants.size(); - unsigned rc = (m_tracker.get_random_uint((ucc < 16) ? 4 : (ucc < 256) ? 8 : (ucc < 4096) ? 12 : (ucc < 65536) ? 16 : 32)) % ucc; - func_decl * fd = unsat_constants[rc]; - mpz new_value; - unsigned bit = 0; - - switch (mt) - { - case MV_FLIP: { - unsigned bv_sz = m_bv_util.get_bv_size(fd->get_range()); - bit = (m_tracker.get_random_uint((bv_sz < 16) ? 4 : (bv_sz < 256) ? 8 : (bv_sz < 4096) ? 12 : (bv_sz < 65536) ? 16 : 32)) % bv_sz; - mk_flip(fd->get_range(), m_tracker.get_value(fd), bit, new_value); - break; - } - case MV_INC: - mk_inc(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); - break; - case MV_DEC: - mk_dec(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); - break; - case MV_INV: - mk_inv(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value); - break; - default: - NOT_IMPLEMENTED_YET(); - } - - m_evaluator.update(fd, new_value); - - TRACE("sls", tout << "Randomization candidates: "; - for (unsigned i = 0; i < unsat_constants.size(); i++) - tout << unsat_constants[i]->get_name() << ", "; - tout << std::endl; - tout << "Random move: "; - switch (mt) { - case MV_FLIP: tout << "Flip #" << bit << " in " << fd->get_name() << std::endl; break; - case MV_INC: tout << "+1 for " << fd->get_name() << std::endl; break; - case MV_DEC: tout << "-1 for " << fd->get_name() << std::endl; break; - case MV_INV: tout << "NEG for " << fd->get_name() << std::endl; break; - } - tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout); ); - - m_mpz_manager.del(new_value); - } - - double find_best_move(goal_ref const & g, ptr_vector & to_evaluate, double score, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) { - mpz old_value, temp; - unsigned bv_sz; - double new_score = score; - - for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0 ; i++) { - func_decl * fd = to_evaluate[i]; - sort * srt = fd->get_range(); - bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); - m_mpz_manager.set(old_value, m_tracker.get_value(fd)); - - // first try to flip every bit - for (unsigned j = 0; j < bv_sz && new_score < 1.0; j++) { - // What would happen if we flipped bit #i ? - mk_flip(srt, old_value, j, temp); - - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) { - new_bit = j; - move = MV_FLIP; - } - } - - if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) { - if (!m_mpz_manager.is_even(old_value)) { - // for odd values, try +1 - mk_inc(bv_sz, old_value, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) - move = MV_INC; - } - else { - // for even values, try -1 - mk_dec(bv_sz, old_value, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) - move = MV_DEC; - } - - // try inverting - mk_inv(bv_sz, old_value, temp); - if (what_if(g, fd, i, temp, new_score, best_const, best_value)) - move = MV_INV; - } - - // reset to what it was before - double check = incremental_score(g, fd, old_value); - SASSERT(check == score); - } - - m_mpz_manager.del(old_value); - m_mpz_manager.del(temp); - return new_score; - } - - lbool search(goal_ref const & g) { - lbool res = l_undef; - double score = 0.0, old_score = 0.0; - unsigned new_const = (unsigned)-1, new_bit = 0; - mpz new_value; - move_type move; - - score = rescore(g); - TRACE("sls", tout << "Starting search, initial score = " << std::setprecision(32) << score << std::endl; - tout << "Score distribution:"; - for (unsigned i = 0; i < g->size(); i++) - tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i)); - tout << " TOP: " << score << std::endl; ); - - unsigned plateau_cnt = 0; - - while (plateau_cnt < m_plateau_limit) { - - do { - checkpoint(); - - old_score = score; - new_const = (unsigned)-1; - - ptr_vector & to_evaluate = m_tracker.get_unsat_constants(g); - - TRACE("sls_constants", tout << "Evaluating these constants: " << std::endl; - for (unsigned i = 0 ; i < to_evaluate.size(); i++) - tout << to_evaluate[i]->get_name() << std::endl; ); - - score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move); - - if (new_const == static_cast(-1)) { - TRACE("sls", tout << "Local maximum reached; unsatisfied constraints: " << std::endl; - for (unsigned i = 0; i < g->size(); i++) { - if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) - tout << mk_ismt2_pp(g->form(i), m_manager) << std::endl; - }); - - TRACE("sls_max", m_tracker.show_model(tout); - tout << "Scores: " << std::endl; - for (unsigned i = 0; i < g->size(); i++) - tout << mk_ismt2_pp(g->form(i), m_manager) << " ---> " << - m_tracker.get_score(g->form(i)) << std::endl; ); - score = old_score; - } - else { - m_stats.m_moves++; - func_decl * fd = to_evaluate[new_const]; - - TRACE("sls", tout << "Setting " << fd->get_name() << " to " << m_mpz_manager.to_string(new_value) << " (Move: "; - switch (move) { - case MV_FLIP: - tout << "Flip"; - if (!m_manager.is_bool(fd->get_range())) tout << " #" << new_bit; - break; - case MV_INC: - tout << "+1"; - break; - case MV_DEC: - tout << "-1"; - break; - case MV_INV: - tout << "NEG"; - break; - }; - tout << ") ; new score = " << std::setprecision(32) << score << std::endl; ); - - switch (move) { - case MV_FLIP: m_stats.m_flips++; break; - case MV_INC: m_stats.m_incs++; break; - case MV_DEC: m_stats.m_decs++; break; - case MV_INV: m_stats.m_invs++; break; - } - - score = incremental_score(g, fd, new_value); - - TRACE("sls", tout << "Score distribution:"; - for (unsigned i = 0; i < g->size(); i++) - tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i)); - tout << " TOP: " << score << std::endl; ); - } - - if (score >= 1.0) { - // score could theoretically be imprecise. - bool all_true = true; - for (unsigned i = 0; i < g->size() && all_true; i++) - if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i)))) - all_true=false; - if (all_true) { - res = l_true; // sat - goto bailout; - } else - TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;); - } - } - while (score > old_score && res == l_undef); - - if (score != old_score) - plateau_cnt = 0; - else { - plateau_cnt++; - if (plateau_cnt < m_plateau_limit) { - TRACE("sls", tout << "In a plateau (" << plateau_cnt << "/" << m_plateau_limit << "); randomizing locally." << std::endl; ); - m_evaluator.randomize_local(g); - //mk_random_move(g); - score = top_score(g); - } - } - } - - bailout: - m_mpz_manager.del(new_value); - - return res; - } - - void operator()(goal_ref const & g, model_converter_ref & mc) { - if (g->inconsistent()) { - mc = 0; - return; - } - - m_tracker.initialize(g); - lbool res = l_undef; - - do { - checkpoint(); - if ((m_stats.m_restarts % 100) == 0) - report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts); - - res = search(g); - - if (res == l_undef) - m_tracker.randomize(); - } - while (res != l_true && m_stats.m_restarts++ < m_max_restarts); - - if (res == l_true) { - if (m_produce_models) { - model_ref mdl = m_tracker.get_model(); - mc = model2model_converter(mdl.get()); - TRACE("sls_model", mc->display(tout); ); - } - g->reset(); - } - else - mc = 0; - } - }; - +class sls_tactic : public tactic { ast_manager & m; params_ref m_params; - imp * m_imp; - stats m_stats; + sls_engine * m_engine; public: sls_tactic(ast_manager & _m, params_ref const & p): m(_m), m_params(p) { - m_imp = alloc(imp, m, p, m_stats); + m_engine = alloc(sls_engine, m, p); } virtual tactic * translate(ast_manager & m) { @@ -524,16 +47,16 @@ public: } virtual ~sls_tactic() { - dealloc(m_imp); + dealloc(m_engine); } virtual void updt_params(params_ref const & p) { m_params = p; - m_imp->updt_params(p); + m_engine->updt_params(p); } virtual void collect_param_descrs(param_descrs & r) { - imp::collect_param_descrs(r); + sls_params::collect_param_descrs(r); } virtual void operator()(goal_ref const & g, @@ -541,14 +64,13 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - SASSERT(g->is_well_sorted()); - m_imp->m_produce_models = g->models_enabled(); + SASSERT(g->is_well_sorted()); mc = 0; pc = 0; core = 0; result.reset(); TRACE("sls", g->display(tout);); tactic_report report("sls", *g); - m_imp->operator()(g, mc); + m_engine->operator()(g, mc); g->inc_depth(); result.push_back(g.get()); @@ -557,35 +79,36 @@ public: } virtual void cleanup() { - imp * d = alloc(imp, m, m_params, m_stats); + sls_engine * d = alloc(sls_engine, m, m_params); #pragma omp critical (tactic_cancel) { - std::swap(d, m_imp); + std::swap(d, m_engine); } dealloc(d); } virtual void collect_statistics(statistics & st) const { - double seconds = m_stats.m_stopwatch.get_current_seconds(); - st.update("sls restarts", m_stats.m_restarts); - st.update("sls full evals", m_stats.m_full_evals); - st.update("sls incr evals", m_stats.m_incr_evals); - st.update("sls incr evals/sec", m_stats.m_incr_evals/ seconds); - st.update("sls FLIP moves", m_stats.m_flips); - st.update("sls INC moves", m_stats.m_incs); - st.update("sls DEC moves", m_stats.m_decs); - st.update("sls INV moves", m_stats.m_invs); - st.update("sls moves", m_stats.m_moves); - st.update("sls moves/sec", m_stats.m_moves / seconds); + sls_engine::stats const & stats = m_engine->get_stats(); + double seconds = stats.m_stopwatch.get_current_seconds(); + st.update("sls restarts", stats.m_restarts); + st.update("sls full evals", stats.m_full_evals); + st.update("sls incr evals", stats.m_incr_evals); + st.update("sls incr evals/sec", stats.m_incr_evals / seconds); + st.update("sls FLIP moves", stats.m_flips); + st.update("sls INC moves", stats.m_incs); + st.update("sls DEC moves", stats.m_decs); + st.update("sls INV moves", stats.m_invs); + st.update("sls moves", stats.m_moves); + st.update("sls moves/sec", stats.m_moves / seconds); } virtual void reset_statistics() { - m_stats.reset(); + m_engine->reset_statistics(); } virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); + if (m_engine) + m_engine->set_cancel(f); } }; @@ -620,6 +143,9 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) { // conservative gaussian elimination. gaussian_p.set_uint("gaussian_max_occs", 2); + params_ref ctx_p; + ctx_p.set_uint("max_depth", 32); + ctx_p.set_uint("max_steps", 5000000); return and_then(and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), using_params(mk_solve_eqs_tactic(m), gaussian_p), @@ -632,7 +158,7 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) { } tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { - tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m)); + tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m, p)); t->updt_params(p); return t; } diff --git a/src/tactic/sls/sls_tactic.h b/src/tactic/sls/sls_tactic.h index 50b8f0d5b..82ac1ce88 100644 --- a/src/tactic/sls/sls_tactic.h +++ b/src/tactic/sls/sls_tactic.h @@ -23,8 +23,8 @@ Notes: class ast_manager; class tactic; -tactic * mk_sls_tactic(ast_manager & m, params_ref const & p = params_ref()); tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p = params_ref()); + /* ADD_TACTIC("qfbv-sls", "(try to) solve using stochastic local search for QF_BV.", "mk_qfbv_sls_tactic(m, p)") */ diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 7fbafec60..87c0f962c 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -20,6 +20,16 @@ Notes: #ifndef _SLS_TRACKER_H_ #define _SLS_TRACKER_H_ +#include + +#include"for_each_expr.h" +#include"ast_smt2_pp.h" +#include"bv_decl_plugin.h" +#include"model.h" + +#include"sls_params.hpp" +#include"sls_powers.h" + class sls_tracker { ast_manager & m_manager; unsynch_mpz_manager & m_mpz_manager; @@ -28,21 +38,26 @@ class sls_tracker { random_gen m_rng; unsigned m_random_bits; unsigned m_random_bits_cnt; - mpz m_zero, m_one, m_two; - + mpz m_zero, m_one, m_two; + struct value_score { - value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0) { }; + value_score() : m(0), 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() { if (m) m->del(value); } unsynch_mpz_manager * m; mpz value; double score; + double score_prune; + unsigned has_pos_occ; + unsigned has_neg_occ; unsigned distance; // max distance from any root + unsigned touched; value_score & operator=(const value_score & other) { SASSERT(m == 0 || m == other.m); if (m) m->set(value, 0); else m = other.m; m->set(value, other.value); score = other.score; distance = other.distance; + touched = other.touched; return *this; } }; @@ -54,12 +69,29 @@ private: typedef obj_map scores_type; typedef obj_map > uplinks_type; typedef obj_map > occ_type; + obj_hashtable m_top_expr; scores_type m_scores; uplinks_type m_uplinks; entry_point_type m_entry_points; ptr_vector m_constants; ptr_vector 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; + obj_map m_where_false; + expr** m_list_false; + unsigned m_track_unsat; + obj_map m_weights; + double m_top_sum; + obj_hashtable m_temp_seen; public: sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : @@ -79,6 +111,59 @@ public: m_mpz_manager.del(m_two); } + void updt_params(params_ref const & _p) { + sls_params p(_p); + m_walksat = p.walksat(); + m_ucb = p.walksat_ucb(); + m_ucb_constant = p.walksat_ucb_constant(); + m_ucb_init = p.walksat_ucb_init(); + m_ucb_forget = p.walksat_ucb_forget(); + m_ucb_noise = p.walksat_ucb_noise(); + m_scale_unsat = p.scale_unsat(); + m_paws_init = p.paws_init(); + // Andreas: track_unsat is currently disabled because I cannot guarantee that it is not buggy. + // If you want to use it, you will also need to change comments in the assertion selection. + m_track_unsat = 0;//p.track_unsat(); + } + + /* Andreas: Tried to give some measure for the formula size by the following two methods but both are not used currently. + unsigned get_formula_size() { + return m_scores.size(); + } + + double get_avg_bw(goal_ref const & g) { + double sum = 0.0; + unsigned count = 0; + + for (unsigned i = 0; i < g->size(); i++) + { + m_temp_constants.reset(); + ptr_vector const & this_decls = m_constants_occ.find(g->form(i)); + unsigned sz = this_decls.size(); + for (unsigned i = 0; i < sz; i++) { + func_decl * fd = this_decls[i]; + m_temp_constants.push_back(fd); + sort * srt = fd->get_range(); + sum += (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); + count++; + } + } + + return sum / count; + }*/ + + inline void adapt_top_sum(expr * e, double add, double sub) { + m_top_sum += m_weights.find(e) * (add - sub); + } + + inline void set_top_sum(double new_score) { + m_top_sum = new_score; + } + + inline double get_top_sum() { + return m_top_sum; + } + inline void set_value(expr * n, const mpz & r) { SASSERT(m_scores.contains(n)); m_mpz_manager.set(m_scores.find(n).value, r); @@ -123,6 +208,26 @@ public: return get_score(ep); } + inline void set_score_prune(expr * n, double score) { + SASSERT(m_scores.contains(n)); + m_scores.find(n).score_prune = score; + } + + inline double & get_score_prune(expr * n) { + SASSERT(m_scores.contains(n)); + return m_scores.find(n).score_prune; + } + + inline unsigned has_pos_occ(expr * n) { + SASSERT(m_scores.contains(n)); + return m_scores.find(n).has_pos_occ; + } + + inline unsigned has_neg_occ(expr * n) { + SASSERT(m_scores.contains(n)); + return m_scores.find(n).has_neg_occ; + } + inline unsigned get_distance(expr * n) { SASSERT(m_scores.contains(n)); return m_scores.find(n).distance; @@ -146,11 +251,32 @@ public: return m_uplinks.contains(n); } + inline bool is_top_expr(expr * n) { + return m_top_expr.contains(n); + } + inline ptr_vector & get_uplinks(expr * n) { SASSERT(m_uplinks.contains(n)); return m_uplinks.find(n); } + inline void ucb_forget(ptr_vector & as) { + if (m_ucb_forget < 1.0) + { + expr * e; + unsigned touched_old, touched_new; + + for (unsigned i = 0; i < as.size(); i++) + { + e = as[i]; + touched_old = m_scores.find(e).touched; + touched_new = (unsigned)((touched_old - 1) * m_ucb_forget + 1); + m_scores.find(e).touched = touched_new; + m_touched += touched_new - touched_old; + } + } + } + void initialize(app * n) { // Build score table if (!m_scores.contains(n)) { @@ -226,12 +352,12 @@ public: } }; - void calculate_expr_distances(goal_ref const & g) { + void calculate_expr_distances(ptr_vector const & as) { // precondition: m_scores is set up. - unsigned sz = g->size(); + unsigned sz = as.size(); ptr_vector stack; for (unsigned i = 0; i < sz; i++) - stack.push_back(to_app(g->form(i))); + stack.push_back(to_app(as[i])); while (!stack.empty()) { app * cur = stack.back(); stack.pop_back(); @@ -249,19 +375,53 @@ public: } } - void initialize(goal_ref const & g) { + /* Andreas: Used this at some point to have values for the non-top-level expressions. + However, it did not give better performance but even cause some additional m/o - is not used currently. + void initialize_recursive(init_proc proc, expr_mark visited, expr * e) { + if (m_manager.is_and(e) || m_manager.is_or(e)) { + app * a = to_app(e); + expr * const * args = a->get_args(); + unsigned int sz = a->get_num_args(); + for (unsigned int i = 0; i < sz; i++) { + expr * q = args[i]; + initialize_recursive(proc, visited, q); + } + } + for_each_expr(proc, visited, e); + } + + void initialize_recursive(expr * e) { + if (m_manager.is_and(e) || m_manager.is_or(e)) { + app * a = to_app(e); + expr * const * args = a->get_args(); + unsigned int sz = a->get_num_args(); + for (unsigned int i = 0; i < sz; i++) { + expr * q = args[i]; + initialize_recursive(q); + } + } + ptr_vector t; + m_constants_occ.insert_if_not_there(e, t); + find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); + expr_fast_mark1 visited; + quick_for_each_expr(ffd_proc, visited, e); + }*/ + + void initialize(ptr_vector const & as) { init_proc proc(m_manager, *this); expr_mark visited; - unsigned sz = g->size(); + unsigned sz = as.size(); for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); + expr * e = as[i]; + if (!m_top_expr.contains(e)) + m_top_expr.insert(e); for_each_expr(proc, visited, e); } visited.reset(); for (unsigned i = 0; i < sz; i++) { - expr * e = g->form(i); + expr * e = as[i]; ptr_vector t; m_constants_occ.insert_if_not_there(e, t); find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); @@ -269,9 +429,82 @@ public: quick_for_each_expr(ffd_proc, visited, e); } - calculate_expr_distances(g); + calculate_expr_distances(as); TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); ); + + if (m_track_unsat) + { + m_list_false = new expr*[sz]; + for (unsigned i = 0; i < sz; i++) + { + if (m_mpz_manager.eq(get_value(as[i]), m_zero)) + break_assertion(as[i]); + } + } + + m_temp_seen.reset(); + for (unsigned i = 0; i < sz; i++) + { + expr * e = as[i]; + + // initialize weights + if (!m_weights.contains(e)) + m_weights.insert(e, m_paws_init); + + // positive/negative occurences used for early pruning + setup_occs(as[i]); + } + + // initialize ucb total touched value (individual ones are always initialized to 1) + m_touched = m_ucb_init ? as.size() : 1; + } + + void increase_weight(expr * e) + { + m_weights.find(e)++; + } + + void decrease_weight(expr * e) + { + unsigned old_weight = m_weights.find(e); + m_weights.find(e) = old_weight > m_paws_init ? old_weight - 1 : m_paws_init; + } + + unsigned get_weight(expr * e) + { + return m_weights.find(e); + } + + void make_assertion(expr * e) + { + if (m_track_unsat) + { + if (m_where_false.contains(e)) + { + unsigned pos = m_where_false.find(e); + m_where_false.erase(e); + if (pos != m_where_false.size()) + { + expr * q = m_list_false[m_where_false.size()]; + m_list_false[pos] = q; + m_where_false.find(q) = pos; + } + } + } + } + + void break_assertion(expr * e) + { + if (m_track_unsat) + { + if (!m_where_false.contains(e)) + { + unsigned pos = m_where_false.size(); + m_list_false[pos] = e; + m_where_false.insert(e, pos); + } + } } void show_model(std::ostream & out) { @@ -368,7 +601,7 @@ public: NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. } - void randomize() { + void randomize(ptr_vector const & as) { TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { @@ -382,7 +615,54 @@ public: TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); } -#define _SCORE_AND_MIN + void reset(ptr_vector const & as) { + TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); + + for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { + mpz temp = m_zero; + set_value(it->m_value, temp); + m_mpz_manager.del(temp); + } + } + + void setup_occs(expr * n, bool negated = false) { + if (m_manager.is_bool(n)) + { + 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]; + if (!m_temp_seen.contains(child)) + { + setup_occs(child, false); + m_temp_seen.insert(child); + } + } + } + else if (m_manager.is_not(n)) + { + SASSERT(!negated); + app * a = to_app(n); + SASSERT(a->get_num_args() == 1); + expr * child = a->get_arg(0); + SASSERT(!m_manager.is_and(child) && !m_manager.is_or(child)); + setup_occs(child, true); + } + else + { + if (negated) + m_scores.find(n).has_neg_occ = 1; + else + m_scores.find(n).has_pos_occ = 1; + } + } + else + NOT_IMPLEMENTED_YET(); + } double score_bool(expr * n, bool negated = false) { TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; ); @@ -400,19 +680,17 @@ public: SASSERT(!negated); app * a = to_app(n); expr * const * args = a->get_args(); - #ifdef _SCORE_AND_MIN + /* 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; } res = min; - #else - 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(); - #endif } else if (m_manager.is_or(n)) { SASSERT(!negated); @@ -441,7 +719,7 @@ public: expr * arg1 = a->get_arg(1); const mpz & v0 = get_value(arg0); const mpz & v1 = get_value(arg1); - + if (negated) { res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0; TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << @@ -457,24 +735,14 @@ public: m_mpz_manager.bitwise_xor(v0, v1, diff); unsigned hamming_distance = 0; unsigned bv_sz = m_bv_util.get_bv_size(arg0); - #if 1 // unweighted hamming distance + // unweighted hamming distance while (!m_mpz_manager.is_zero(diff)) { - //m_mpz_manager.set(diff_m1, diff); - //m_mpz_manager.dec(diff_m1); - //m_mpz_manager.bitwise_and(diff, diff_m1, diff); - //hamming_distance++; if (!m_mpz_manager.is_even(diff)) { hamming_distance++; } m_mpz_manager.machine_div(diff, m_two, diff); } - res = 1.0 - (hamming_distance / (double) bv_sz); - #else - rational r(diff); - r /= m_powers(bv_sz); - double dbl = r.get_double(); - res = (dbl < 0.0) ? 1.0 : (dbl > 1.0) ? 0.0 : 1.0 - dbl; - #endif + res = 1.0 - (hamming_distance / (double) bv_sz); TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << m_mpz_manager.to_string(v1) << " ; HD = " << hamming_distance << " ; SZ = " << bv_sz << std::endl; ); @@ -489,7 +757,7 @@ public: SASSERT(a->get_num_args() == 2); const mpz & x = get_value(a->get_arg(0)); const mpz & y = get_value(a->get_arg(1)); - unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); + int bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); if (negated) { if (m_mpz_manager.gt(x, y)) @@ -515,7 +783,7 @@ public: rational n(diff); n /= rational(m_powers(bv_sz)); double dbl = n.get_double(); - res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; + res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; m_mpz_manager.del(diff); } } @@ -535,7 +803,7 @@ public: if (negated) { if (x > y) - res = 1.0; + res = 1.0; else { mpz diff; m_mpz_manager.sub(y, x, diff); @@ -551,14 +819,15 @@ public: } else { if (x <= y) - res = 1.0; + res = 1.0; else { mpz diff; m_mpz_manager.sub(x, y, diff); + SASSERT(!m_mpz_manager.is_neg(diff)); rational n(diff); n /= p; double dbl = n.get_double(); - res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; + res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; m_mpz_manager.del(diff); } TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << @@ -572,7 +841,9 @@ public: app * a = to_app(n); SASSERT(a->get_num_args() == 1); expr * child = a->get_arg(0); - if (m_manager.is_and(child) || m_manager.is_or(child)) // Precondition: Assertion set is in NNF. + // Precondition: Assertion set is in NNF. + // Also: careful about the unsat assertion scaling further down. + if (m_manager.is_and(child) || m_manager.is_or(child)) NOT_IMPLEMENTED_YET(); res = score_bool(child, true); } @@ -598,10 +869,16 @@ public: SASSERT(res >= 0.0 && res <= 1.0); + app * a = to_app(n); + family_id afid = a->get_family_id(); + + if (afid == m_bv_util.get_family_id()) + if (res < 1.0) res *= m_scale_unsat; + TRACE("sls_score", tout << "SCORE = " << res << std::endl; ); return res; } - + double score_bv(expr * n) { return 0.0; // a bv-expr is always scored as 0.0; we won't use those scores. } @@ -647,29 +924,143 @@ public: NOT_IMPLEMENTED_YET(); } - ptr_vector & get_unsat_constants(goal_ref const & g) { - unsigned sz = g->size(); - - if (sz == 1) { - return get_constants(); + ptr_vector & get_constants(expr * e) { + ptr_vector const & this_decls = m_constants_occ.find(e); + unsigned sz = this_decls.size(); + for (unsigned i = 0; i < sz; i++) { + func_decl * fd = this_decls[i]; + if (!m_temp_constants.contains(fd)) + m_temp_constants.push_back(fd); } - else { - m_temp_constants.reset(); - for (unsigned i = 0; i < sz; i++) { - expr * q = g->form(i); - if (m_mpz_manager.eq(get_value(q), m_one)) - continue; - ptr_vector 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]; - if (!m_temp_constants.contains(fd)) - m_temp_constants.push_back(fd); - } + return m_temp_constants; + } + + ptr_vector & get_unsat_constants_gsat(ptr_vector const & as) { + unsigned sz = as.size(); + if (sz == 1) { + if (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]; + if (m_mpz_manager.eq(get_value(q), m_one)) + continue; + ptr_vector 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]; + if (!m_temp_constants.contains(fd)) + m_temp_constants.push_back(fd); + } + } + return m_temp_constants; + } + + ptr_vector & get_unsat_constants_walksat(expr * e) { + if (!e || m_temp_constants.size()) + return m_temp_constants; + ptr_vector 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); } return m_temp_constants; + } + + ptr_vector & get_unsat_constants(ptr_vector const & as) { + if (m_walksat) + { + expr * e = get_unsat_assertion(as); + + if (!e) + { + m_temp_constants.reset(); + return m_temp_constants; + } + + return get_unsat_constants_walksat(e); } + else + return get_unsat_constants_gsat(as); + } + + expr * get_unsat_assertion(ptr_vector const & as) { + unsigned sz = as.size(); + if (sz == 1) { + if (m_mpz_manager.neq(get_value(as[0]), m_one)) + return as[0]; + else + return 0; + } + m_temp_constants.reset(); + + unsigned pos = -1; + if (m_ucb) + { + value_score vscore; + double max = -1.0; + // Andreas: Commented things here might be used for track_unsat data structures as done in SLS for SAT. But seems to have no benefit. + /* for (unsigned i = 0; i < m_where_false.size(); i++) { + expr * e = m_list_false[i]; */ + for (unsigned i = 0; i < sz; i++) { + expr * e = as[i]; + if (m_mpz_manager.neq(get_value(e), m_one)) + { + vscore = m_scores.find(e); + // Andreas: Select the assertion with the greatest ucb score. Potentially add some noise. + // double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched); + double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + m_ucb_noise * get_random_uint(8); + if (q > max) { max = q; pos = i; } + } + } + if (pos == static_cast(-1)) + return 0; + + m_touched++; + m_scores.find(as[pos]).touched++; + // Andreas: Also part of track_unsat data structures. Additionally disable the previous line! + /* m_last_pos = pos; + m_scores.find(m_list_false[pos]).touched++; + return m_list_false[pos]; */ + } + else + { + // Andreas: The track_unsat data structures for random assertion selection. + /* sz = m_where_false.size(); + if (sz == 0) + return 0; + return m_list_false[get_random_uint(16) % sz]; */ + + unsigned cnt_unsat = 0; + for (unsigned i = 0; i < sz; i++) + if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; + if (pos == static_cast(-1)) + return 0; + } + + m_last_pos = pos; + return as[pos]; + } + + expr * get_new_unsat_assertion(ptr_vector const & as) { + unsigned sz = as.size(); + if (sz == 1) + return 0; + m_temp_constants.reset(); + + unsigned cnt_unsat = 0, pos = -1; + for (unsigned i = 0; i < sz; i++) + if ((i != m_last_pos) && m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; + + if (pos == static_cast(-1)) + return 0; + return as[pos]; } }; -#endif \ No newline at end of file +#endif