From 853ce522ccda06788da56198d9c3808df4a6cd73 Mon Sep 17 00:00:00 2001 From: Andreas Froehlich Date: Sun, 9 Mar 2014 15:42:51 +0000 Subject: [PATCH] plenty of new stuff --- src/sat/tactic/sat_tactic.cpp | 4 +- src/tactic/portfolio/default_tactic.cpp | 1 + src/tactic/portfolio/smt_strategic_solver.cpp | 1 + src/tactic/sls/sls_evaluator.h | 323 ++++++++- src/tactic/sls/sls_tactic.cpp | 661 ++++++++++++++++-- src/tactic/sls/sls_tracker.h | 345 ++++++++- versions/z3-wsat-0.01.txt | 4 +- versions/z3-wsat-0.01b.txt | 4 +- 8 files changed, 1235 insertions(+), 108 deletions(-) diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index d48994861..717bf7007 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -66,7 +66,9 @@ 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);); - + //m_solver.display_dimacs(std::cerr); + //exit(0); + lbool r = m_solver.check(); if (r == l_false) { g->assert_expr(m.mk_false(), 0, 0); diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index b28b7bec0..53da9a159 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -33,6 +33,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_sls_tactic(m), + // cond(mk_is_qfbv_probe(), mk_qfbv_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/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 52b0a3c90..f63b4fd8c 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -43,6 +43,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_sls_tactic(m, p); else if (logic=="QF_IDL") return mk_qfidl_tactic(m, p); diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 61305386e..eec9524a9 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -34,6 +34,9 @@ class sls_evaluator { powers & m_powers; expr_ref_buffer m_temp_exprs; vector > m_traversal_stack; +#if _EARLY_PRUNE_ + vector > m_traversal_stack_bool; +#endif public: sls_evaluator(ast_manager & m, bv_util & bvu, sls_tracker & t, unsynch_mpz_manager & mm, powers & p) : @@ -519,11 +522,15 @@ 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; +#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_ + double new_score; +#endif + 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 +540,92 @@ public: (*this)(to_app(cur), new_value); m_tracker.set_value(cur, new_value); - m_tracker.set_score(cur, m_tracker.score(cur)); +#if _REAL_RS_ || _REAL_PBFS_ + if (!m_tracker.has_uplinks(cur)) + { + if (m_mpz_manager.eq(new_value,m_one)) + m_tracker.make_assertion(cur); + else + m_tracker.break_assertion(cur); + } +#endif + +#if _EARLY_PRUNE_ + new_score = m_tracker.score(cur); +#if _CACHE_TOP_SCORE_ + if (!m_tracker.has_uplinks(cur)) + m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); +#endif + m_tracker.set_score(cur, new_score); + m_tracker.set_score_prune(cur, new_score); +#else +#if _CACHE_TOP_SCORE_ + new_score = m_tracker.score(cur); + if (!m_tracker.has_uplinks(cur)) + m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); + m_tracker.set_score(cur, new_score); +#else + m_tracker.set_score(cur, m_tracker.score(cur)); +#endif +#endif + 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; + +#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_ + double new_score; +#endif + + 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); +#if _EARLY_PRUNE_ + new_score = m_tracker.score(cur); +#if _CACHE_TOP_SCORE_ + if (!m_tracker.has_uplinks(cur)) + m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); +#endif + m_tracker.set_score(cur, new_score); + m_tracker.set_score_prune(cur, new_score); +#else +#if _CACHE_TOP_SCORE_ + new_score = m_tracker.score(cur); + if (!m_tracker.has_uplinks(cur)) + m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); + m_tracker.set_score(cur, new_score); +#else + m_tracker.set_score(cur, m_tracker.score(cur)); +#endif +#endif if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); for (unsigned j = 0; j < ups.size(); j++) { @@ -569,8 +660,11 @@ public: m_traversal_stack[cur_depth].push_back(ep); if (cur_depth > max_depth) max_depth = cur_depth; } - +#if _REAL_RS_ || _REAL_PBFS_ + run_serious_update(max_depth); +#else run_update(max_depth); +#endif } void update(func_decl * fd, const mpz & new_value) { @@ -584,6 +678,196 @@ 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); + + run_serious_update(cur_depth); + } + +#if _EARLY_PRUNE_ + 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 _CACHE_TOP_SCORE_ + if (!m_tracker.has_uplinks(cur)) + m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); +#endif + 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); + } + } + } + else + { + } + } + + 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]; + +#if _CACHE_TOP_SCORE_ + new_score = m_tracker.score(cur); + if (!m_tracker.has_uplinks(cur)) + m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); + m_tracker.set_score(cur, new_score); +#else + m_tracker.set_score(cur, m_tracker.score(cur)); +#endif + 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); + // should 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); + } +#endif + + void randomize_local(expr * e, unsigned int flip) { + ptr_vector & unsat_constants = m_tracker.get_constants(e); + + // Randomize _one_ candidate: + unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size(); + func_decl * fd = unsat_constants[r]; +#if _PERC_CHANGE_ + sort * srt = fd->get_range(); + mpz temp; + + if (m_manager.is_bool(srt)) + m_mpz_manager.set(temp, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero); + else + { + mpz temp2, mask; + unsigned bv_sz = m_bv_util.get_bv_size(srt); + m_mpz_manager.set(temp, m_tracker.get_value(fd)); + + for (unsigned bit = 0; bit < bv_sz; bit++) + if (m_tracker.get_random_uint(16) % 100 < _PERC_CHANGE_) + { + m_mpz_manager.set(mask, m_powers(bit)); + m_mpz_manager.bitwise_xor(temp, mask, temp2); + m_mpz_manager.set(temp, temp2); + } + m_mpz_manager.del(mask); + m_mpz_manager.del(temp2); + } +#else + mpz temp = m_tracker.get_random(fd->get_range()); +#endif + update(fd, temp); + m_mpz_manager.del(temp); + } + void randomize_local(goal_ref const & g, unsigned int flip) { ptr_vector & unsat_constants = m_tracker.get_unsat_constants(g, flip); @@ -603,8 +887,37 @@ public: // 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); +#if _PERC_CHANGE_ + sort * srt = fd->get_range(); + mpz temp; + + if (m_manager.is_bool(srt)) + m_mpz_manager.set(temp, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero); + else + { + mpz temp2, mask; + unsigned bv_sz = m_bv_util.get_bv_size(srt); + m_mpz_manager.set(temp, m_tracker.get_value(fd)); + + for (unsigned bit = 0; bit < bv_sz; bit++) + if (m_tracker.get_random_uint(16) % 100 < _PERC_CHANGE_) + { + m_mpz_manager.set(mask, m_powers(bit)); + m_mpz_manager.bitwise_xor(temp, mask, temp2); + m_mpz_manager.set(temp, temp2); + } + m_mpz_manager.del(mask); + m_mpz_manager.del(temp2); + } +#else + mpz temp = m_tracker.get_random(fd->get_range()); +#endif + +#if _REAL_RS_ || _REAL_PBFS_ + serious_update(fd, temp); +#else + update(fd, temp); +#endif m_mpz_manager.del(temp); TRACE("sls", /*tout << "Randomization candidates: "; diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index c84e68730..3d5e3e438 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -35,16 +35,102 @@ Notes: #include"sls_tactic.h" #include"nnf_tactic.h" -#define _CNF_ 0 -#define _BFS_ 1 +// which unsatisfied assertion is selected? only works with _FOCUS_ > 0 +// 0 = random, 1 = #moves, 2 = assertion with min score, 3 = assertion with max score +#define _BFS_ 0 + +// how many terms are considered for variable selection? +// 0 = all terms (GSAT), 1 = only one top level assertion (WSAT), 2 = only one bottom level atom #define _FOCUS_ 1 + +// do we use restarts? +// 0 = no, otherwise the value defines the maximum number of moves #define _RESTARTS_ 0 -#define _TIMELIMIT_ 30 + +// timelimit +#define _TIMELIMIT_ 3600 + +// should score of conjunctions be calculated by average rather than max? #define _SCORE_AND_AVG_ 0 + +// should score of discunctions be calculated by multiplication of the inverse score rather than min? #define _SCORE_OR_MUL_ 0 + +// do we use some kind of variable neighbourhood-search? +// 0 = no, 1 = only consider flipping bits if no better score can be obtained otherwise, 2 = only consider flipping bits until a better score can be obtained #define _VNS_ 0 -#define _WEIGHT_DIST_ 3 -#define _WEIGHT_DIST_FACTOR_ 0.1 + +// do we reduce the score of unsatisfied literals? +// 0 = no +// 1 = yes, by multiplying it with some factor +// 2 = yes, by squaring it +// 3 = yes, by setting it to zero +// 4 = by progessively increasing weight (_TIMELIMIT_ needs to be set appropriately!) +#define _WEIGHT_DIST_ 0 + +// the factor used for _WEIGHT_DIST_ = 1 +#define _WEIGHT_DIST_FACTOR_ 0.25 + +// do we use intensification steps in local minima? if so, how many? +#define _INTENSIFICATION_ 0 +#define _INTENSIFICATION_TRIES_ 0 + +// do we use some UCT-like scheme for assertion-selection? overrides _BFS_ +#define _UCT_ 0 + +// how much diversification is used in the UCT-scheme? +#define _UCT_CONSTANT_ 0.01 + +// is uct clause selection probabilistic similar to variable selection in sparrow? +#define _PROBABILISTIC_UCT_ 0 + +// shall we use addition/subtraction? +#define _USE_ADDSUB_ 1 + +// shall we try multilication and division by 2? +#define _USE_MUL2DIV2_ 1 + +// shall we try multiplication by 3? +#define _USE_MUL3_ 1 + +// shall we try unary minus (= inverting and incrementing) +#define _USE_UNARY_MINUS_ 1 + +// is random selection for assertions uniform? only works with _BFS_ = _UCT_ = 0 +#define _UNIFORM_RANDOM_ 1 + +// should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection? +#define _REAL_RS_ 0 +#define _REAL_PBFS_ 0 + +// how many bits do we neglect in each iteration? +#define _SKIP_BITS_ 0 + +// when randomizing local, what is the probability for changing a single bit? +// 0 = use standard scheme and pick a new value at random (= 50), otherwise the value (as int) gives the percentage +#define _PERC_CHANGE_ 0 + +// do we use random steps for noise? +// 0 = no, 1 = randomize local, 2 = make random move +#define _TYPE_RSTEP_ 0 + +// with what probability _PERM_STEP_/1000 will the random step happen? +#define _PERM_RSTEP_ 0 + +// shall we use early pruning for incremental update? +#define _EARLY_PRUNE_ 1 + +// shall we use caching for top_score? +#define _CACHE_TOP_SCORE_ 1 + + +#if ((_UCT_ > 0) + _UNIFORM_RANDOM_ + _REAL_RS_ + _REAL_PBFS_ > 1) || _BFS_ && (_UCT_ ||_UNIFORM_RANDOM_ ||_REAL_RS_ ||_REAL_PBFS_) + InvalidConfiguration; +#endif +#if (_PROBABILISTIC_UCT_ && !_UCT_) + InvalidConfiguration; +#endif + #include"sls_params.hpp" #include"sls_evaluator.h" @@ -57,12 +143,17 @@ class sls_tactic : public tactic { stopwatch m_stopwatch; unsigned m_full_evals; unsigned m_incr_evals; - unsigned m_moves, m_flips, m_incs, m_decs, m_invs; + unsigned m_moves, m_flips, m_incs, m_decs, m_invs, m_umins, m_mul2s, m_mul3s, m_div2s; + stats() : m_restarts(0), m_full_evals(0), m_incr_evals(0), m_moves(0), + m_umins(0), + m_mul2s(0), + m_mul3s(0), + m_div2s(0), m_flips(0), m_incs(0), m_decs(0), @@ -92,7 +183,9 @@ class sls_tactic : public tactic { unsigned m_max_restarts; unsigned m_plateau_limit; - typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type; + ptr_vector m_old_values; + + typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV, MV_UMIN, MV_MUL2, MV_MUL3, MV_DIV2 } move_type; imp(ast_manager & m, params_ref const & p, stats & s) : m_manager(m), @@ -174,13 +267,20 @@ class sls_tactic : public tactic { #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)); + for (unsigned i = 0; i < sz; i++) { + expr * e = g->form(i); + top_sum += m_tracker.get_score(e); } - TRACE("sls_top", tout << "Score distribution:"; + + 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; ); + +#if _CACHE_TOP_SCORE_ + m_tracker.set_top_sum(top_sum); +#endif + return top_sum / (double) sz; #endif } @@ -191,22 +291,54 @@ class sls_tactic : public tactic { return top_score(g); } - double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value) { - m_evaluator.update(fd, new_value); + double serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value) { + m_evaluator.serious_update(fd, new_value); m_stats.m_incr_evals++; +#if _CACHE_TOP_SCORE_ + return (m_tracker.get_top_sum() / g->size()); +#else return top_score(g); +#endif } + 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++; +#if _CACHE_TOP_SCORE_ + return (m_tracker.get_top_sum() / g->size()); +#else + return top_score(g); +#endif + } + +#if _EARLY_PRUNE_ + double incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value) { + m_stats.m_incr_evals++; + if (m_evaluator.update_prune(fd, new_value)) +#if _CACHE_TOP_SCORE_ + return (m_tracker.get_top_sum() / g->size()); +#else + return top_score(g); +#endif + else + return 0.0; + } +#endif + + // checks whether the score outcome of a given move is better than the previous score 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 +#if _EARLY_PRUNE_ + double r = incremental_score_prune(g, fd, temp); +#else double r = incremental_score(g, fd, temp); - +#endif #ifdef Z3DEBUG TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << " --> " << r << std::endl; ); @@ -214,6 +346,22 @@ class sls_tactic : public tactic { m_mpz_manager.del(old_value); #endif +// if (r >= best_score) { + if (r > best_score) { + best_score = r; + best_const = fd_inx; + m_mpz_manager.set(best_value, temp); + return true; + } + + return false; + } + + // same as what_if, but only applied to the score of a specific atom, not the total score + bool what_if_local(expr * e, func_decl * fd, const unsigned & fd_inx, const mpz & temp, + double & best_score, unsigned & best_const, mpz & best_value) { + m_evaluator.update(fd, temp); + double r = m_tracker.get_score(e); if (r >= best_score) { best_score = r; best_const = fd_inx; @@ -224,7 +372,35 @@ class sls_tactic : public tactic { return false; } - void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented) { + void 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); + + } + + // Andreas: do we really need all those temporary mpzs? + void mk_mul2(unsigned bv_sz, const mpz & old_value, mpz & result) { + mpz temp, mask, mask2; + m_mpz_manager.mul(old_value, m_two, 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 mk_div2(unsigned bv_sz, const mpz & old_value, mpz & result) { + m_mpz_manager.div(old_value, m_two, result); + } + + 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) @@ -261,59 +437,73 @@ class sls_tactic : public tactic { 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; + if (m_stats.m_moves > 10000) + rnd_mv = 0; 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(); - } + mpz new_value; - m_evaluator.update(fd, 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 _USE_ADDSUB_ + 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; - 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); ); + // inversion doesn't make sense, let's do a flip instead. + if (mt == MV_INV) mt = MV_FLIP; +#else + mt = MV_FLIP; +#endif + unsigned bit = 0; - m_mpz_manager.del(new_value); - } + 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.update(fd, new_value); + m_mpz_manager.del(new_value); + } + + // will use VNS to ignore some possible moves and increase the flips per second 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; @@ -359,6 +549,7 @@ class sls_tactic : public tactic { SASSERT(check == score); } + // we can either check the condition once in the beginning or check it repeatedly after every bit #if _VNS_ == 1 for (unsigned j = 1; j < max_bv_sz && new_score <= score; j++) #else @@ -390,9 +581,13 @@ class sls_tactic : public tactic { return new_score; } + // finds the move that increased score the most. returns best_const = -1, if no increasing move exists. 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; +#if _USE_MUL3_ || _USE_UNARY_MINUS_ + mpz temp2; +#endif unsigned bv_sz; double new_score = score; @@ -403,8 +598,12 @@ class sls_tactic : public tactic { 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 ? +#if _SKIP_BITS_ + for (unsigned j = (i + m_stats.m_moves) % (_SKIP_BITS_ + 1); j < bv_sz && new_score < 1.0; j+=(_SKIP_BITS_ + 1)) { +#else + for (unsigned j = 0; j < bv_sz && new_score < 1.0; j++) { +#endif + // 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)) { @@ -414,7 +613,8 @@ class sls_tactic : public tactic { } if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) { - if (!m_mpz_manager.is_even(old_value)) { +#if _USE_ADDSUB_ + 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)) @@ -426,16 +626,99 @@ class sls_tactic : public tactic { if (what_if(g, fd, i, temp, new_score, best_const, best_value)) move = MV_DEC; } - +#endif // 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; + +#if _USE_UNARY_MINUS_ + mk_inc(bv_sz, temp, temp2); + if (what_if(g, fd, i, temp2, new_score, best_const, best_value)) + move = MV_UMIN; +#endif + +#if _USE_MUL2DIV2_ + // try multiplication by 2 + mk_mul2(bv_sz, old_value, temp); + if (what_if(g, fd, i, temp, new_score, best_const, best_value)) + move = MV_MUL2; + +#if _USE_MUL3_ + // try multiplication by 3 + mk_add(bv_sz, old_value, temp, temp2); + if (what_if(g, fd, i, temp2, new_score, best_const, best_value)) + move = MV_MUL3; +#endif + + // try division by 2 + mk_div2(bv_sz, old_value, temp); + if (what_if(g, fd, i, temp, new_score, best_const, best_value)) + move = MV_DIV2; +#endif } // reset to what it was before double check = incremental_score(g, fd, old_value); - SASSERT(check == score); + // Andreas: does not hold anymore now that we use top level score caching + //SASSERT(check == score); + } + + m_mpz_manager.del(old_value); + m_mpz_manager.del(temp); +#if _USE_MUL3_ + m_mpz_manager.del(temp2); +#endif + return new_score; + } + + // same as find_best_move but only considers the score of the current expression instead of the overall score + double find_best_move_local(expr * e, ptr_vector & to_evaluate, + unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) { + mpz old_value, temp; + unsigned bv_sz; + double new_score = m_tracker.get_score(e); + // Andreas: tie breaking not implemented yet + // double tie_score = top_score(g); + 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_local(e, 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_local(e, 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_local(e, fd, i, temp, new_score, best_const, best_value)) + move = MV_DEC; + } + + // try inverting + mk_inv(bv_sz, old_value, temp); + if (what_if_local(e, fd, i, temp, new_score, best_const, best_value)) + move = MV_INV; + } + + // reset to what it was before + m_evaluator.update(fd, old_value); } m_mpz_manager.del(old_value); @@ -443,7 +726,150 @@ class sls_tactic : public tactic { return new_score; } - lbool search(goal_ref const & g) { + // first try of intensification ... does not seem to be efficient + bool handle_plateau(goal_ref const & g) + { + unsigned sz = g->size(); +#if _BFS_ + unsigned pos = m_stats.m_moves % sz; +#else + unsigned pos = m_tracker.get_random_uint(16) % sz; +#endif + expr * e = m_tracker.get_unsat_assertion(g, sz, pos); + if (!e) + return 0; + + expr * q = m_tracker.get_unsat_expression(e); + ptr_vector & to_evaluate = m_tracker.get_constants(q); + for (unsigned i = 0; i < to_evaluate.size(); i++) + { + m_tracker.get_value(to_evaluate[i]); + m_old_values.push_back( & m_tracker.get_value(to_evaluate[i])); + } + unsigned new_const = (unsigned)-1, new_bit = 0; + mpz new_value; + move_type move; + for (unsigned i = 0; i < _INTENSIFICATION_TRIES_; i++) + { + // Andreas: Could be extended to use (best) score but this is computationally more expensive. + find_best_move_local(q, to_evaluate, new_const, new_value, new_bit, move); + + if (new_const == static_cast(-1)) { + // Andreas: Actually this should never happen. + NOT_IMPLEMENTED_YET(); + } else { + m_stats.m_moves++; + func_decl * fd = to_evaluate[new_const]; + + 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; + case MV_UMIN: m_stats.m_umins++; break; + case MV_MUL2: m_stats.m_mul2s++; break; + case MV_MUL3: m_stats.m_mul3s++; break; + case MV_DIV2: m_stats.m_div2s++; break; + } + + m_evaluator.update(fd, new_value); + } + + if (m_mpz_manager.is_one(m_tracker.get_value(q))) + return 1; + } + + for (unsigned i = 0; i < to_evaluate.size(); i++) + m_tracker.set_value(to_evaluate[i], * m_old_values[i]); + + m_old_values.reset(); + + return 0; + } + + // what_if version needed in the context of 2nd intensification try, combining local and global score + bool what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz & temp, + double & best_score, mpz & best_value, unsigned i) { + + double global_score = incremental_score(g, fd, temp); + double local_score = m_tracker.get_score(e); + double new_score = i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_; + + if (new_score >= best_score) { + best_score = new_score; + m_mpz_manager.set(best_value, temp); + return true; + } + + return false; + } + + // find_best_move version needed in the context of 2nd intensification try + double find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i) + { + mpz old_value, temp; + double best_score = 0; + + sort * srt = fd->get_range(); + unsigned 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)); + + for (unsigned j = 0; j < bv_sz && best_score < 1.0; j++) { + mk_flip(srt, old_value, j, temp); + what_if(g, e, fd, temp, best_score, best_value, i); + } + + m_mpz_manager.del(old_value); + m_mpz_manager.del(temp); + + return best_score; + } + + // second try to use intensification ... also not very effective + bool handle_plateau(goal_ref const & g, double old_score) + { + unsigned sz = g->size(); +#if _BFS_ + unsigned new_const = m_stats.m_moves % sz; +#else + unsigned new_const = m_tracker.get_random_uint(16) % sz; +#endif + expr * e = m_tracker.get_unsat_assertion(g, sz, new_const); + if (!e) + return 0; + + expr * q = m_tracker.get_unsat_expression(e); + ptr_vector & to_evaluate = m_tracker.get_constants(q); + + new_const = m_tracker.get_random_uint(16) % to_evaluate.size(); + func_decl * fd = to_evaluate[new_const]; + + mpz new_value; + //m_mpz_manager.set(new_value, m_tracker.get_value(fd)); + unsigned new_bit = 0; + double global_score = old_score, local_score = m_tracker.get_score(q), new_score = old_score; + + for (unsigned i = 1; i <= _INTENSIFICATION_TRIES_; i++) + { + new_score = find_best_move_local(g, q, fd, new_value, i); + + m_stats.m_moves++; + m_stats.m_flips++; + + global_score = incremental_score(g, fd, new_value); + local_score = m_tracker.get_score(q); + + SASSERT(new_score == i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_); + + if (m_mpz_manager.is_one(m_tracker.get_value(q))) + return 1; + } + + return 0; + } + + // main search loop + 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; @@ -463,16 +889,48 @@ class sls_tactic : public tactic { #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_) { + while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && (_RESTARTS_ == 0 || m_stats.m_moves < _RESTARTS_)) { #endif do { + if (m_stats.m_moves == 5590) checkpoint(); + +#if _WEIGHT_DIST_ == 4 + m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); +#endif +#if _TYPE_RSTEP_ + if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_) + { +#if _TYPE_RSTEP_ == 1 + m_evaluator.randomize_local(g, m_stats.m_moves); +#elif _TYPE_RSTEP_ == 2 + mk_random_move(g); +#endif + score = top_score(g); + + if (score >= 1.0) { + 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;); + } + } +#endif old_score = score; new_const = (unsigned)-1; ptr_vector & to_evaluate = m_tracker.get_unsat_constants(g, m_stats.m_moves); - + if (!to_evaluate.size()) + { + res = l_true; + goto bailout; + } 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; ); @@ -525,9 +983,17 @@ class sls_tactic : public tactic { case MV_INC: m_stats.m_incs++; break; case MV_DEC: m_stats.m_decs++; break; case MV_INV: m_stats.m_invs++; break; + case MV_UMIN: m_stats.m_umins++; break; + case MV_MUL2: m_stats.m_mul2s++; break; + case MV_MUL3: m_stats.m_mul3s++; break; + case MV_DIV2: m_stats.m_div2s++; break; } - score = incremental_score(g, fd, new_value); +#if _REAL_RS_ || _REAL_PBFS_ + score = serious_score(g, fd, new_value); +#else + score = incremental_score(g, fd, new_value); +#endif TRACE("sls", tout << "Score distribution:"; for (unsigned i = 0; i < g->size(); i++) @@ -535,9 +1001,10 @@ class sls_tactic : public tactic { tout << " TOP: " << score << std::endl; ); } - if (score >= 1.0) { + if (score >= 0.99999) { +// if (score >= 1.0) { // score could theoretically be imprecise. - // Andreas: Can it only be imprecise in one direction? + // Andreas: it seems using top level score caching can make the score unprecise also in the other 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)))) @@ -568,10 +1035,26 @@ class sls_tactic : public tactic { // 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; ); +#if _INTENSIFICATION_ + handle_plateau(g, score); + //handle_plateau(g); +#else m_evaluator.randomize_local(g, m_stats.m_moves); - //mk_random_move(g); +#endif + //mk_random_move(g); score = top_score(g); - //} + + if (score >= 1.0) { + 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;); + } } } @@ -587,6 +1070,37 @@ class sls_tactic : public tactic { return; } + verbose_stream() << "_BFS_ " << _BFS_ << std::endl; + verbose_stream() << "_FOCUS_ " << _FOCUS_ << std::endl; + verbose_stream() << "_RESTARTS_ " << _RESTARTS_ << std::endl; + verbose_stream() << "_TIMELIMIT_ " << _TIMELIMIT_ << std::endl; + verbose_stream() << "_SCORE_AND_AVG_ " << _SCORE_AND_AVG_ << std::endl; + verbose_stream() << "_SCORE_OR_MUL_ " << _SCORE_OR_MUL_ << std::endl; + verbose_stream() << "_VNS_ " << _VNS_ << std::endl; + verbose_stream() << "_WEIGHT_DIST_ " << _WEIGHT_DIST_ << std::endl; + verbose_stream() << "_WEIGHT_DIST_FACTOR_ " << std::fixed << std::setprecision(2) << _WEIGHT_DIST_FACTOR_ << std::endl; + verbose_stream() << "_INTENSIFICATION_ " << _INTENSIFICATION_ << std::endl; + verbose_stream() << "_INTENSIFICATION_TRIES_ " << _INTENSIFICATION_TRIES_ << std::endl; + verbose_stream() << "_UCT_ " << _UCT_ << std::endl; + verbose_stream() << "_UCT_CONSTANT_ " << std::fixed << std::setprecision(2) << _UCT_CONSTANT_ << std::endl; + verbose_stream() << "_PROBABILISTIC_UCT_ " << _PROBABILISTIC_UCT_ << std::endl; + verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl; + verbose_stream() << "_USE_MUL2DIV2_ " << _USE_MUL2DIV2_ << std::endl; + verbose_stream() << "_USE_MUL3_ " << _USE_MUL3_ << std::endl; + verbose_stream() << "_USE_UNARY_MINUS_ " << _USE_UNARY_MINUS_ << std::endl; + verbose_stream() << "_UNIFORM_RANDOM_ " << _UNIFORM_RANDOM_ << std::endl; + verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl; + verbose_stream() << "_REAL_PBFS_ " << _REAL_PBFS_ << std::endl; + verbose_stream() << "_SKIP_BITS_ " << _SKIP_BITS_ << std::endl; + verbose_stream() << "_PERC_CHANGE_ " << _PERC_CHANGE_ << std::endl; + verbose_stream() << "_TYPE_RSTEP_ " << _TYPE_RSTEP_ << std::endl; + verbose_stream() << "_PERM_RSTEP_ " << _PERM_RSTEP_ << std::endl; + verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl; + verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl; + +#if _WEIGHT_DIST_ == 4 + m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); +#endif m_tracker.initialize(g); lbool res = l_undef; @@ -745,13 +1259,8 @@ 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) { diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 1061bd90e..b26912e5c 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -28,21 +28,32 @@ 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) { }; +#if _EARLY_PRUNE_ + 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) { }; +#else + value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1) { }; +#endif ~value_score() { if (m) m->del(value); } unsynch_mpz_manager * m; mpz value; double score; +#if _EARLY_PRUNE_ + double score_prune; + unsigned has_pos_occ; + unsigned has_neg_occ; +#endif 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; } }; @@ -60,6 +71,20 @@ private: ptr_vector m_constants; ptr_vector m_temp_constants; occ_type m_constants_occ; +#if _UCT_ + unsigned m_touched; +#endif +#if _REAL_RS_ || _REAL_PBFS_ + ptr_vector m_unsat_expr; + obj_map m_where_false; + expr** m_list_false; +#endif +#if _CACHE_TOP_SCORE_ + double m_top_sum; +#endif +#if _WEIGHT_DIST_ == 4 + double m_weight_dist_factor; +#endif public: sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : @@ -79,6 +104,26 @@ public: m_mpz_manager.del(m_two); } +#if _WEIGHT_DIST_ == 4 + inline void set_weight_dist_factor(double val) { + m_weight_dist_factor = val; + } +#endif + +#if _CACHE_TOP_SCORE_ + inline void adapt_top_sum(double add, double sub) { + m_top_sum += add - sub; + } + + inline void set_top_sum(double new_score) { + m_top_sum = new_score; + } + + inline double get_top_sum() { + return m_top_sum; + } +#endif + 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 +168,28 @@ public: return get_score(ep); } +#if _EARLY_PRUNE_ + 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; + } +#endif + inline unsigned get_distance(expr * n) { SASSERT(m_scores.contains(n)); return m_scores.find(n).distance; @@ -297,7 +364,7 @@ public: for (unsigned i = 0; i < sz; i++) { expr * e = g->form(i); // Andreas: Maybe not fully correct. -#if _FOCUS_ == 2 +#if _FOCUS_ == 2 || _INTENSIFICATION_ initialize_recursive(e); #endif ptr_vector t; @@ -310,8 +377,57 @@ public: calculate_expr_distances(g); TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); ); + +#if _REAL_RS_ || _REAL_PBFS_ + m_list_false = new expr*[sz]; + for (unsigned i = 0; i < sz; i++) + if (m_mpz_manager.eq(get_value(g->form(i)),m_zero)) + break_assertion(g->form(i)); +#endif + +#if _EARLY_PRUNE_ + for (unsigned i = 0; i < sz; i++) + setup_occs(g->form(i)); +#endif + +#if _UCT_ + m_touched = 1; +#endif } +#if _REAL_RS_ || _REAL_PBFS_ + void make_assertion(expr * e) + { + 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; + } +// printf("Going in %d\n", m_where_false.size()); + } + //if (m_unsat_expr.contains(e)) + //m_unsat_expr.erase(e); + } + + void break_assertion(expr * e) + { + if (!m_where_false.contains(e)) + { + unsigned pos = m_where_false.size(); + m_list_false[pos] = e; + m_where_false.insert(e, pos); + // printf("Going in %d\n", m_where_false.size()); + } + //if (!m_unsat_expr.contains(e)) + //m_unsat_expr.push_back(e); + } +#endif + void show_model(std::ostream & out) { unsigned sz = get_num_constants(); for (unsigned i = 0; i < sz; i++) { @@ -420,10 +536,45 @@ public: TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); } +#if _EARLY_PRUNE_ + 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++) + setup_occs(args[i]); + } + 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); + if (m_manager.is_and(child) || m_manager.is_or(child)) + NOT_IMPLEMENTED_YET(); + 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(); + } +#endif + double score_bool(expr * n, bool negated = false) { TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; ); - double res = 0.0; + double res = 0.0; if (is_uninterp_const(n)) { const mpz & r = get_value(n); @@ -488,7 +639,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 = " << @@ -648,6 +799,7 @@ public: #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 @@ -656,13 +808,14 @@ public: res *= res; #elif _WEIGHT_DIST_ == 3 if (res < 1.0) res = 0.0; +#elif _WEIGHT_DIST_ == 4 + if (res < 1.0) res *= m_weight_dist_factor; #endif - 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. } @@ -708,6 +861,44 @@ public: NOT_IMPLEMENTED_YET(); } + expr * get_unsat_expression(expr * e) { + if (m_manager.is_bool(e)) { + if (m_manager.is_and(e) || m_manager.is_or(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 get_unsat_expression(q); + } + for (unsigned int i = 0; i < pos; i++) { + expr * q = args[i]; + if (m_mpz_manager.neq(get_value(q), m_one)) + return get_unsat_expression(q); + } + } + } + return e; + } + + 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); + } + return m_temp_constants; + } + ptr_vector & get_unsat_constants_gsat(goal_ref const & g, unsigned sz) { for (unsigned i = 0; i < sz; i++) { expr * q = g->form(i); @@ -743,7 +934,6 @@ public: // 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++) { @@ -754,6 +944,19 @@ public: return m_temp_constants; } + ptr_vector & get_unsat_constants_walksat(expr * e) { + if (!e) + 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 & go_deeper(expr * e) { if (m_manager.is_bool(e)) { if (m_manager.is_and(e)) { @@ -812,44 +1015,138 @@ public: return go_deeper(q); } - ptr_vector & get_unsat_constants(goal_ref const & g, unsigned int flip) { + ptr_vector & get_unsat_constants(goal_ref const & g, unsigned int flip) { unsigned sz = g->size(); if (sz == 1) { - return get_constants(); + if (m_mpz_manager.eq(get_value(g->form(0)), m_one)) + return m_temp_constants; + else + return get_constants(); } 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++) { +#if _UCT_ + unsigned pos = -1; + value_score vscore; +#if _PROBABILISTIC_UCT_ + double sum_score = 0.0; + unsigned start_index = get_random_uint(16) % sz; + for (unsigned i = start_index; i < sz; i++) + { + expr * e = g->form(i); + vscore = m_scores.find(e); + double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); + if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) { + sum_score += q; + if (rand() <= (q * RAND_MAX / sum_score) + 1) + pos = i; + } + } + for (unsigned i = 0; i < start_index; i++) + { + expr * e = g->form(i); + vscore = m_scores.find(e); + double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); + if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) { + sum_score += q; + if (rand() <= (q * RAND_MAX / sum_score) + 1) + pos = i; + } + } +#else + double max = -1.0; + for (unsigned i = 0; i < sz; i++) { + expr * e = g->form(i); + vscore = m_scores.find(e); +#if _UCT_ == 1 + double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched); +#elif _UCT_ == 2 + double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; +#endif + if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } + } +#endif + if (pos == static_cast(-1)) + return m_temp_constants; + +#if _UCT_ == 1 + m_scores.find(g->form(pos)).touched++; + m_touched++; +#elif _UCT_ == 2 + m_scores.find(g->form(pos)).touched = flip; +#endif + expr * e = g->form(pos); + +#elif _BFS_ == 3 + unsigned int pos = -1; + double max = -1.0; + for (unsigned i = 0; 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 m_temp_constants; + expr * e = g->form(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++) { + unsigned int pos = -1; + double min = 2.0; + for (unsigned i = 0; 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; } } + if (pos == static_cast(-1)) + return m_temp_constants; + expr * e = g->form(pos); #elif _BFS_ == 1 - unsigned int pos = flip % m_constants.size(); + // I guess it was buggy ... + // unsigned int pos = flip % m_constants.size(); + unsigned int pos = flip % sz; + expr * e = get_unsat_assertion(g, sz, pos); +#elif _UNIFORM_RANDOM_ + unsigned cnt_unsat = 0, pos = -1; + for (unsigned i = 0; i < sz; i++) + if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; + if (pos == static_cast(-1)) + return m_temp_constants; + expr * e = g->form(pos); +#elif _REAL_RS_ + //unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false]; + //expr * e = get_unsat_assertion(g, sz, pos); + //expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()]; + sz = m_where_false.size(); + if (sz == 0) + return m_temp_constants; + else + expr * e = m_list_false[get_random_uint(16) % sz]; +#elif _REAL_PBFS_ + //unsigned pos = m_false_list[flip % m_cnt_false]; + //expr * e = get_unsat_assertion(g, sz, pos); + //expr * e = m_unsat_expr[flip % m_unsat_expr.size()]; + sz = m_where_false.size(); + if (sz == 0) + return m_temp_constants; + else + expr * e = m_list_false[flip % sz]; #else - unsigned int pos = get_random_uint(16) % m_constants.size(); + // I guess it was buggy ... + // unsigned int pos = get_random_uint(16) % m_constants.size(); + unsigned int pos = get_random_uint(16) % sz; + expr * e = get_unsat_assertion(g, sz, pos); #endif - return get_unsat_constants_walksat(g, sz, pos); + return get_unsat_constants_walksat(e); #elif _FOCUS_ == 2 #if _BFS_ - unsigned int pos = flip % m_constants.size(); + // I guess it was buggy ... + // unsigned int pos = flip % m_constants.size(); + unsigned int pos = flip % sz; #else - unsigned int pos = get_random_uint(16) % m_constants.size(); + // I guess it was buggy ... + // unsigned int pos = get_random_uint(16) % m_constants.size(); + unsigned int pos = get_random_uint(16) % sz; #endif return get_unsat_constants_crsat(g, sz, pos); #else diff --git a/versions/z3-wsat-0.01.txt b/versions/z3-wsat-0.01.txt index 141193f76..fec38518d 100644 --- a/versions/z3-wsat-0.01.txt +++ b/versions/z3-wsat-0.01.txt @@ -9,4 +9,6 @@ No restarts. #define _RESTARTS_ 0 #define _TIMELIMIT_ 300 #define _SCORE_AND_AVG_ 0 -#define _SCORE_OR_MUL_ 0 \ No newline at end of file +#define _SCORE_OR_MUL_ 0 + +BUGGY VERSION! Uses wrong value for modulo operation in assertion selection. \ No newline at end of file diff --git a/versions/z3-wsat-0.01b.txt b/versions/z3-wsat-0.01b.txt index 2c0c0e7ad..8bcf2ffeb 100644 --- a/versions/z3-wsat-0.01b.txt +++ b/versions/z3-wsat-0.01b.txt @@ -9,4 +9,6 @@ No restarts. #define _RESTARTS_ 0 #define _TIMELIMIT_ 300 #define _SCORE_AND_AVG_ 0 -#define _SCORE_OR_MUL_ 0 \ No newline at end of file +#define _SCORE_OR_MUL_ 0 + +BUGGY VERSION! Uses wrong value for modulo operation in assertion selection. \ No newline at end of file