From dfe2d945e94eb22b1e59958525a3ca0731f6aedb Mon Sep 17 00:00:00 2001 From: Andreas Froehlich Date: Tue, 18 Feb 2014 14:01:47 +0000 Subject: [PATCH] some extensions/modifications. versions added. --- src/tactic/portfolio/default_tactic.cpp | 2 +- src/tactic/sls/sls_evaluator.h | 243 +-------- src/tactic/sls/sls_tactic.cpp | 661 ++++++++++++++++++++++-- src/tactic/sls/sls_tracker.h | 640 ++++++++--------------- versions/z3-wsat-0.01.txt | 4 +- versions/z3-wsat-0.01b.txt | 4 +- 6 files changed, 872 insertions(+), 682 deletions(-) diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 5a5cbcf94..b28b7bec0 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -32,7 +32,7 @@ Notes: 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_qfbv_probe(), mk_qfbv_sls_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), diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 61afb7457..61305386e 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -20,8 +20,6 @@ Notes: #ifndef _SLS_EVALUATOR_H_ #define _SLS_EVALUATOR_H_ -#include"model_evaluator.h" - #include"sls_powers.h" #include"sls_tracker.h" @@ -36,7 +34,6 @@ 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) : @@ -96,7 +93,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: { @@ -522,64 +519,11 @@ public: } } - 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]; - - 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)); - 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]; @@ -589,10 +533,8 @@ public: (*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); + m_tracker.set_score(cur, m_tracker.score(cur)); + if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); for (unsigned j = 0; j < ups.size(); j++) { @@ -627,7 +569,8 @@ public: m_traversal_stack[cur_depth].push_back(ep); if (cur_depth > max_depth) max_depth = cur_depth; } - run_serious_update(max_depth); + + run_update(max_depth); } void update(func_decl * fd, const mpz & new_value) { @@ -641,174 +584,36 @@ public: run_update(cur_depth); } - 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); + void randomize_local(goal_ref const & g, unsigned int flip) { + ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g, flip); - run_serious_update(cur_depth); - } + // Randomize _all_ candidates: - unsigned run_update_bool_prune(unsigned cur_depth) { - expr_fast_mark1 visited; + //// 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); + //} - 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()); - - serious_update(fd, temp); - + update(fd, temp); m_mpz_manager.del(temp); - TRACE("sls", tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl; + 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; 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_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 9bbed20bb..c194af267 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -16,30 +16,619 @@ 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"propagate_values_tactic.h" -#include"ctx_simplify_tactic.h" -#include"elim_uncnstr_tactic.h" -#include"nnf_tactic.h" #include"stopwatch.h" +#include"propagate_values_tactic.h" #include"sls_tactic.h" -#include"sls_params.hpp" -#include"sls_engine.h" +#include"nnf_tactic.h" -class sls_tactic : public tactic { +#define _CNF_ 0 +#define _BFS_ 1 +#define _FOCUS_ 1 +#define _RESTARTS_ 0 +#define _TIMELIMIT_ 30 +#define _SCORE_AND_AVG_ 0 +#define _SCORE_OR_MUL_ 0 +#define _VNS_ 0 +#define _WEIGHT_DIST_ 3 +#define _WEIGHT_DIST_FACTOR_ 0.1 + +#include"sls_params.hpp" +#include"sls_evaluator.h" +#include"sls_tracker.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, m_stats.m_moves); + 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_vns(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, max_bv_sz = 0; + 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); + if (max_bv_sz < bv_sz) max_bv_sz = bv_sz; + m_mpz_manager.set(old_value, m_tracker.get_value(fd)); + + 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; + + // try to flip lsb + mk_flip(srt, old_value, 0, temp); + if (what_if(g, fd, i, temp, new_score, best_const, best_value)) { + new_bit = 0; + move = MV_FLIP; + } + } + + // reset to what it was before + double check = incremental_score(g, fd, old_value); + SASSERT(check == score); + } + +#if _VNS_ == 1 + for (unsigned j = 1; j < max_bv_sz && new_score <= score; j++) +#else + if (new_score <= score) + for (unsigned j = 1; j < max_bv_sz && new_score < 1.0; j++) +#endif + 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)); + + // What would happen if we flipped bit #j ? + if (j < bv_sz) + { + 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; + } + } + // 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; + } + + 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; + + // Andreas: Why do we only allow so few plateaus? +#if _RESTARTS_ + while (plateau_cnt < m_plateau_limit && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { +#else + while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { +#endif + do { + checkpoint(); + + old_score = score; + new_const = (unsigned)-1; + + ptr_vector & to_evaluate = m_tracker.get_unsat_constants(g, m_stats.m_moves); + + 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; ); + +#if _VNS_ + score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move); +#else + score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move); +#endif + 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; ); + // Andreas: If new_const == -1, shouldn't score = old_score anyway? + score = old_score; + } + else { + // Andreas: Why does randomizing not count as a move? (Now it does.) + 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. + // Andreas: Can it only be imprecise in one direction? + 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;); + } + /* + if (m_stats.m_moves % 100 == 0) + { + verbose_stream() << "(" << std::fixed << std::setprecision(10) << score << ")" << std::endl; + verbose_stream() << "(" << std::fixed << std::setprecision(2) << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl; + }*/ + } + while (score > old_score && res == l_undef); + + // Andreas: Why do you check for old_score? This should always be equal due to the loop invariant. + if (score != old_score) { + report_tactic_progress("This should not happen I guess.", plateau_cnt); + plateau_cnt = 0; + } else { + m_stats.m_moves++; + plateau_cnt++; + //report_tactic_progress("Plateau.", plateau_cnt); + // Andreas: Right now, a useless assignment is created in case of a restart. But we don't want to use restarts anyway. + //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, m_stats.m_moves); + //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(); + // Andreas: I think restarts are too impotant to ignore 99% of them are happening... + //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 (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && 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; + + if (res == l_true) { + report_tactic_progress("Number of flips:", m_stats.m_moves); + 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; + } + }; + ast_manager & m; params_ref m_params; - sls_engine * m_engine; + imp * m_imp; + stats m_stats; public: sls_tactic(ast_manager & _m, params_ref const & p): m(_m), m_params(p) { - m_engine = alloc(sls_engine, m, p); + m_imp = alloc(imp, m, p, m_stats); } virtual tactic * translate(ast_manager & m) { @@ -47,16 +636,16 @@ public: } virtual ~sls_tactic() { - dealloc(m_engine); + dealloc(m_imp); } virtual void updt_params(params_ref const & p) { m_params = p; - m_engine->updt_params(p); + m_imp->updt_params(p); } virtual void collect_param_descrs(param_descrs & r) { - sls_params::collect_param_descrs(r); + imp::collect_param_descrs(r); } virtual void operator()(goal_ref const & g, @@ -64,13 +653,14 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - SASSERT(g->is_well_sorted()); + SASSERT(g->is_well_sorted()); + m_imp->m_produce_models = g->models_enabled(); mc = 0; pc = 0; core = 0; result.reset(); TRACE("sls", g->display(tout);); tactic_report report("sls", *g); - m_engine->operator()(g, mc); + m_imp->operator()(g, mc); g->inc_depth(); result.push_back(g.get()); @@ -79,36 +669,35 @@ public: } virtual void cleanup() { - sls_engine * d = alloc(sls_engine, m, m_params); + imp * d = alloc(imp, m, m_params, m_stats); #pragma omp critical (tactic_cancel) { - std::swap(d, m_engine); + std::swap(d, m_imp); } dealloc(d); } virtual void collect_statistics(statistics & st) const { - 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); + 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); } virtual void reset_statistics() { - m_engine->reset_statistics(); + m_stats.reset(); } virtual void set_cancel(bool f) { - if (m_engine) - m_engine->set_cancel(f); + if (m_imp) + m_imp->set_cancel(f); } }; @@ -143,9 +732,6 @@ 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), @@ -154,12 +740,17 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) { using_params(mk_simplify_tactic(m), simp2_p)), using_params(mk_simplify_tactic(m), hoist_p), mk_max_bv_sharing_tactic(m), +#if _CNF_ + // Andreas: We will probably never use this. CNF sucks. + mk_cnf_tactic(m, p)); +#else + // Andreas: How does a NNF actually look like? Can it contain ITE operators? mk_nnf_tactic(m, p)); +#endif } 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_simplify_tactic(m), mk_nnf_tactic(m, p), mk_sls_tactic(m)); t->updt_params(p); return t; } diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 89ef57871..1061bd90e 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -20,14 +20,6 @@ Notes: #ifndef _SLS_TRACKER_H_ #define _SLS_TRACKER_H_ -#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; @@ -36,26 +28,21 @@ 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), touched(1), score_prune(0.0), has_pos_occ(0), has_neg_occ(0) { }; + value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0) { }; ~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; } }; @@ -67,29 +54,12 @@ 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) : @@ -109,59 +79,6 @@ 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); @@ -206,26 +123,6 @@ 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; @@ -249,32 +146,11 @@ 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)) { @@ -350,12 +226,12 @@ public: } }; - void calculate_expr_distances(ptr_vector const & as) { + void calculate_expr_distances(goal_ref const & g) { // precondition: m_scores is set up. - unsigned sz = as.size(); + unsigned sz = g->size(); ptr_vector stack; for (unsigned i = 0; i < sz; i++) - stack.push_back(to_app(as[i])); + stack.push_back(to_app(g->form(i))); while (!stack.empty()) { app * cur = stack.back(); stack.pop_back(); @@ -373,53 +249,57 @@ public: } } - /* 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(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; + 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) { + void initialize(goal_ref const & g) { init_proc proc(m_manager, *this); expr_mark visited; - unsigned sz = as.size(); + unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) { - expr * e = as[i]; - if (!m_top_expr.contains(e)) - m_top_expr.insert(e); + expr * e = g->form(i); + // Andreas: Maybe not fully correct. +#if _FOCUS_ == 2 + initialize_recursive(proc, visited, e); +#endif for_each_expr(proc, visited, e); } visited.reset(); for (unsigned i = 0; i < sz; i++) { - expr * e = as[i]; + expr * e = g->form(i); + // Andreas: Maybe not fully correct. +#if _FOCUS_ == 2 + initialize_recursive(e); +#endif 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)); @@ -427,82 +307,9 @@ public: quick_for_each_expr(ffd_proc, visited, e); } - calculate_expr_distances(as); + calculate_expr_distances(g); 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) { @@ -599,7 +406,7 @@ public: NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. } - void randomize(ptr_vector const & as) { + void randomize() { 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++) { @@ -613,55 +420,6 @@ public: TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); } - 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; ); @@ -678,28 +436,41 @@ public: 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. + // Andreas: Seems to have no effect. Probably it does not even occur. +#if _SCORE_AND_AVG_ 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; + res = sum / (double) a->get_num_args(); +#else + 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; +#endif } else if (m_manager.is_or(n)) { SASSERT(!negated); app * a = to_app(n); expr * const * args = a->get_args(); - double max = 0.0; + // Andreas: Seems to have no effect. Probably it is still too similar to the original version. +#if _SCORE_OR_MUL_ + double inv = 1.0; + for (unsigned i = 0; i < a->get_num_args(); i++) { + double cur = get_score(args[i]); + inv *= (1.0 - get_score(args[i])); + } + res = 1.0 - inv; +#else + 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; } res = max; +#endif } else if (m_manager.is_ite(n)) { SASSERT(!negated); @@ -717,7 +488,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 = " << @@ -733,14 +504,24 @@ public: m_mpz_manager.bitwise_xor(v0, v1, diff); unsigned hamming_distance = 0; unsigned bv_sz = m_bv_util.get_bv_size(arg0); - // unweighted hamming distance + #if 1 // 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 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; ); @@ -755,7 +536,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)); - int bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); + unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); if (negated) { if (m_mpz_manager.gt(x, y)) @@ -769,7 +550,7 @@ public: double dbl = n.get_double(); // In extreme cases, n is 0.9999 but to_double returns something > 1.0 res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; - m_mpz_manager.del(diff); + m_mpz_manager.del(diff); } } else { @@ -781,7 +562,7 @@ public: rational n(diff); n /= rational(m_powers(bv_sz)); double dbl = n.get_double(); - res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; + res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; m_mpz_manager.del(diff); } } @@ -801,7 +582,7 @@ public: if (negated) { if (x > y) - res = 1.0; + res = 1.0; else { mpz diff; m_mpz_manager.sub(y, x, diff); @@ -817,21 +598,20 @@ 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) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; + res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; m_mpz_manager.del(diff); } TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); } - m_mpz_manager.del(x); + m_mpz_manager.del(x); m_mpz_manager.del(y); } else if (m_manager.is_not(n)) { @@ -839,9 +619,7 @@ public: app * a = to_app(n); SASSERT(a->get_num_args() == 1); expr * child = a->get_arg(0); - // Precondition: Assertion set is in NNF. - // Also: careful about the unsat assertion scaling further down. - if (m_manager.is_and(child) || m_manager.is_or(child)) + if (m_manager.is_and(child) || m_manager.is_or(child)) // Precondition: Assertion set is in NNF. NOT_IMPLEMENTED_YET(); res = score_bool(child, true); } @@ -867,16 +645,24 @@ public: SASSERT(res >= 0.0 && res <= 1.0); - app * a = to_app(n); - family_id afid = a->get_family_id(); +#if _WEIGHT_DIST_ + app * a = to_app(n); + family_id afid = a->get_family_id(); + if (afid == m_bv_util.get_family_id()) +#endif +#if _WEIGHT_DIST_ == 1 + if (res < 1.0) res *= _WEIGHT_DIST_FACTOR_; +#elif _WEIGHT_DIST_ == 2 + res *= res; +#elif _WEIGHT_DIST_ == 3 + if (res < 1.0) res = 0.0; +#endif - 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. } @@ -922,28 +708,9 @@ public: NOT_IMPLEMENTED_YET(); } - ptr_vector & get_constants(expr * e) { - ptr_vector const & this_decls = m_constants_occ.find(e); - unsigned sz = this_decls.size(); + ptr_vector & get_unsat_constants_gsat(goal_ref const & g, unsigned sz) { 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); - } - 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]; + 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); @@ -955,110 +722,141 @@ public: } } 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++) { + expr * get_unsat_assertion(goal_ref const & g, unsigned sz, unsigned int pos) { + for (unsigned i = pos; i < sz; i++) { + expr * q = g->form(i); + if (m_mpz_manager.neq(get_value(q), m_one)) + return q; + } + for (unsigned i = 0; i < pos; i++) { + expr * q = g->form(i); + if (m_mpz_manager.neq(get_value(q), m_one)) + return q; + } + return 0; + } + + ptr_vector & get_unsat_constants_walksat(goal_ref const & g, unsigned sz, unsigned int pos) { + expr * q = get_unsat_assertion(g, sz, pos); + // Andreas: I should probably fix this. If this is the case then the formula is SAT anyway but this is not checked in the first iteration. + if (!q) + return m_temp_constants; + + 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; - } + 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; + ptr_vector & go_deeper(expr * e) { + if (m_manager.is_bool(e)) { + if (m_manager.is_and(e)) { + app * a = to_app(e); + expr * const * args = a->get_args(); + // Andreas: might be used for guided branching + //for (unsigned i = 0; i < a->get_num_args(); i++) { + //double cur = get_score(args[i]); + //} + // Andreas: A random number is better here since reusing flip will cause patterns. + unsigned int sz = a->get_num_args(); + unsigned int pos = get_random_uint(16) % sz; + for (unsigned int i = pos; i < sz; i++) { + expr * q = args[i]; + if (m_mpz_manager.neq(get_value(q), m_one)) + return go_deeper(q); + } + for (unsigned int i = 0; i < pos; i++) { + expr * q = args[i]; + if (m_mpz_manager.neq(get_value(q), m_one)) + return go_deeper(q); + } + } + else if (m_manager.is_or(e)) { + app * a = to_app(e); + expr * const * args = a->get_args(); + unsigned int sz = a->get_num_args(); + unsigned int pos = get_random_uint(16) % sz; + for (unsigned int i = pos; i < sz; i++) { + expr * q = args[i]; + if (m_mpz_manager.neq(get_value(q), m_one)) + return go_deeper(q); + } + for (unsigned int i = 0; i < pos; i++) { + expr * q = args[i]; + if (m_mpz_manager.neq(get_value(q), m_one)) + return go_deeper(q); + } + } + } + ptr_vector const & this_decls = m_constants_occ.find(e); + 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_crsat(goal_ref const & g, unsigned sz, unsigned int pos) { + expr * q = get_unsat_assertion(g, sz, pos); + if (!q) + return m_temp_constants; + + return go_deeper(q); + } + + ptr_vector & get_unsat_constants(goal_ref const & g, unsigned int flip) { + unsigned sz = g->size(); - 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; + return get_constants(); } - 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; } - } + else { + m_temp_constants.reset(); +#if _FOCUS_ == 1 +#if _BFS_ == 3 + unsigned int pos = 0; + double max = get_score(g->form(0)); + unsigned sz = g->size(); + for (unsigned i = 1; i < sz; i++) { + expr * e = g->form(i); + double q = get_score(e); + if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { 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]; */ +#elif _BFS_ == 2 + unsigned int pos = 0; + double min = get_score(g->form(0)); + unsigned sz = g->size(); + for (unsigned i = 1; i < sz; i++) { + expr * e = g->form(i); + double q = get_score(e); + if (q < min && m_mpz_manager.neq(get_value(e), m_one) ) { min = q; pos = i; } + } +#elif _BFS_ == 1 + unsigned int pos = flip % m_constants.size(); +#else + unsigned int pos = get_random_uint(16) % m_constants.size(); +#endif + return get_unsat_constants_walksat(g, sz, pos); +#elif _FOCUS_ == 2 +#if _BFS_ + unsigned int pos = flip % m_constants.size(); +#else + unsigned int pos = get_random_uint(16) % m_constants.size(); +#endif + return get_unsat_constants_crsat(g, sz, pos); +#else + return get_unsat_constants_gsat(g, sz); +#endif } - 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 +#endif \ No newline at end of file diff --git a/versions/z3-wsat-0.01.txt b/versions/z3-wsat-0.01.txt index fec38518d..141193f76 100644 --- a/versions/z3-wsat-0.01.txt +++ b/versions/z3-wsat-0.01.txt @@ -9,6 +9,4 @@ No restarts. #define _RESTARTS_ 0 #define _TIMELIMIT_ 300 #define _SCORE_AND_AVG_ 0 -#define _SCORE_OR_MUL_ 0 - -BUGGY VERSION! Uses wrong value for modulo operation in assertion selection. \ No newline at end of file +#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-wsat-0.01b.txt b/versions/z3-wsat-0.01b.txt index 8bcf2ffeb..2c0c0e7ad 100644 --- a/versions/z3-wsat-0.01b.txt +++ b/versions/z3-wsat-0.01b.txt @@ -9,6 +9,4 @@ No restarts. #define _RESTARTS_ 0 #define _TIMELIMIT_ 300 #define _SCORE_AND_AVG_ 0 -#define _SCORE_OR_MUL_ 0 - -BUGGY VERSION! Uses wrong value for modulo operation in assertion selection. \ No newline at end of file +#define _SCORE_OR_MUL_ 0 \ No newline at end of file