diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index 8e52596e0..d2b899dd8 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -36,17 +36,21 @@ Notes: // do we use dirty unit propagation to get rid of nested top level assertions? #define _DIRTY_UP_ 0 +// shall we use additive weighting scheme? +#define _PAWS_ 5 +#define _PAWS_INIT_ 40 + // do we use restarts? // 0 = no, 1 = use #moves, 2 = use #plateaus, 3 = use time -#define _RESTARTS_ 3 +#define _RESTARTS_ 1 // limit of moves/plateaus/seconds until first restart occurs -#define _RESTART_LIMIT_ 10 +#define _RESTART_LIMIT_ 100 // 0 = initialize with all zero, 1 initialize with random value #define _RESTART_INIT_ 0 -// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid +// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid, 5 = minisat #define _RESTART_SCHEME_ 1 // base value c for armin restart scheme using c^inner - only applies for _RESTART_SCHEME_ 3 -#define _RESTART_CONST_ARMIN_ 3.0 +#define _RESTART_CONST_ARMIN_ 2.0 // timelimit #define _TIMELIMIT_ 3600 @@ -61,6 +65,21 @@ Notes: // 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 +// shall we check 2-bit flips in plateaus using Monte Carlo? +#define _VNS_MC_ 0 + +// how many 2-bit flips shall we try per bit? +#define _VNS_MC_TRIES_ 1 + +// shall we check another assertion if no improving step was found in the first one? +#define _VNS_REPICK_ 0 + +// what is the probability of doing so (percentage)? +#define _VNS_PERC_ 100 + +// do a decreasing move with percentage ... +#define _INSIST_PERC_ 0 + // do we reduce the score of unsatisfied literals? // 0 = no // 1 = yes, by multiplying it with some factor @@ -70,7 +89,7 @@ Notes: #define _WEIGHT_DIST_ 1 // the factor used for _WEIGHT_DIST_ = 1 -#define _WEIGHT_DIST_FACTOR_ 0.25 +#define _WEIGHT_DIST_FACTOR_ 0.5 // shall we toggle the weight after each restart? #define _WEIGHT_TOGGLE_ 0 @@ -82,14 +101,15 @@ Notes: // what is the percentage of random moves in plateaus (instead of full randomization)? #define _PERC_PLATEAU_MOVES_ 0 -// shall we repick clause when randomizing in a plateau or use the current one? +// shall we repick assertion when randomizing in a plateau or use the current one? +// 0 = use old one, 1 = repick according to usual scheme, 2 = repick randomly and force different one #define _REPICK_ 1 // do we use some UCT-like scheme for assertion-selection? overrides _BFS_ #define _UCT_ 1 // how much diversification is used in the UCT-scheme? -#define _UCT_CONSTANT_ 10.0 +#define _UCT_CONSTANT_ 20.0 // is uct clause selection probabilistic similar to variable selection in sparrow? // 0 = no, 1 = yes, use uct-value, 2 = yes, use score-value (_UCT_CONSTANT_ = 0.0) with squared score @@ -103,7 +123,11 @@ Notes: // how shall we initialize the _UCT_ total touched counter? // 0 = initialize with one, 1 = initialize with number of assertions -#define _UCT_INIT_ 1 +#define _UCT_INIT_ 0 + +// do we gradually reduce the touched values of _UCT_? +#define _UCT_FORGET_ 0 +#define _UCT_FORGET_FACTOR_ 0.9 // shall we use addition/subtraction? #define _USE_ADDSUB_ 1 diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index dc4451bb5..342e649af 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -74,15 +74,15 @@ void sls_engine::checkpoint() { cooperate("sls"); } -bool sls_engine::full_eval(model & mdl) { +bool sls_engine::full_eval(goal_ref const & g, model & mdl) { bool res = true; - unsigned sz = m_assertions.size(); + unsigned sz = g->size(); for (unsigned i = 0; i < sz && res; i++) { checkpoint(); expr_ref o(m_manager); - if (!mdl.eval(m_assertions[i], o, true)) + if (!mdl.eval(g->form(i), o, true)) exit(ERR_INTERNAL_FATAL); res = m_manager.is_true(o.get()); @@ -93,7 +93,7 @@ bool sls_engine::full_eval(model & mdl) { return res; } -double sls_engine::top_score() { +double sls_engine::top_score(goal_ref const & g) { #if 0 double min = m_tracker.get_score(g->form(0)); unsigned sz = g->size(); @@ -108,15 +108,15 @@ double sls_engine::top_score() { return min; #else double top_sum = 0.0; - unsigned sz = m_assertions.size(); + unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) { - expr * e = m_assertions[i]; + expr * e = g->form(i); top_sum += m_tracker.get_score(e); } TRACE("sls_top", tout << "Score distribution:"; for (unsigned i = 0; i < sz; i++) - tout << " " << m_tracker.get_score(m_assertions[i]); + tout << " " << m_tracker.get_score(g->form(i)); tout << " AVG: " << top_sum / (double)sz << std::endl;); #if _CACHE_TOP_SCORE_ @@ -127,40 +127,40 @@ double sls_engine::top_score() { #endif } -double sls_engine::rescore() { +double sls_engine::rescore(goal_ref const & g) { m_evaluator.update_all(); m_stats.m_full_evals++; - return top_score(); + return top_score(g); } -double sls_engine::serious_score(func_decl * fd, const mpz & new_value) { +double sls_engine::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() / m_assertions.size()); + return (m_tracker.get_top_sum() / g->size()); #else - return top_score(); + return top_score(g); #endif } -double sls_engine::incremental_score(func_decl * fd, const mpz & new_value) { +double sls_engine::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() / m_assertions.size()); + return (m_tracker.get_top_sum() / g->size()); #else - return top_score(); + return top_score(g); #endif } -double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value) { +double sls_engine::incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value) { #if _EARLY_PRUNE_ m_stats.m_incr_evals++; if (m_evaluator.update_prune(fd, new_value)) #if _CACHE_TOP_SCORE_ - return (m_tracker.get_top_sum() / m_assertions.size()); + return (m_tracker.get_top_sum() / g->size()); #else - return top_score(); + return top_score(g); #endif else return 0.0; @@ -169,14 +169,17 @@ double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value #endif } +double sls_engine::incremental_score_prune_new(goal_ref const & g, func_decl * fd, const mpz & new_value) { + m_stats.m_incr_evals++; + if (m_evaluator.update_prune_new(fd, new_value)) + return (m_tracker.get_top_sum() / g->size()); + else + return 0.0; +} + // checks whether the score outcome of a given move is better than the previous score -bool sls_engine::what_if( - func_decl * fd, - const unsigned & fd_inx, - const mpz & temp, - double & best_score, - unsigned & best_const, - mpz & best_value) { +bool sls_engine::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; @@ -184,9 +187,9 @@ bool sls_engine::what_if( #endif #if _EARLY_PRUNE_ - double r = incremental_score_prune(fd, temp); + double r = incremental_score_prune(g, fd, temp); #else - double r = incremental_score(fd, temp); + 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) << @@ -195,8 +198,33 @@ bool sls_engine::what_if( m_mpz_manager.del(old_value); #endif - // if (r >= best_score) { + //if (r >= best_score) { if (r > best_score) { + m_tracker.reset_equal_scores(); + best_score = r; + best_const = fd_inx; + m_mpz_manager.set(best_value, temp); + return true; + } + /*else if (r == best_score) { + if (m_tracker.get_random_uint(16) % m_tracker.inc_equal_scores() == 0) + { + best_score = r; + best_const = fd_inx; + m_mpz_manager.set(best_value, temp); + return true; + } + }*/ + + return false; +} + +bool sls_engine::what_if_new(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp, + double & best_score, unsigned & best_const, mpz & best_value) { + + double r = incremental_score_prune_new(g, fd, temp); + + if (r >= best_score) { best_score = r; best_const = fd_inx; m_mpz_manager.set(best_value, temp); @@ -207,15 +235,8 @@ bool sls_engine::what_if( } // same as what_if, but only applied to the score of a specific atom, not the total score -bool sls_engine::what_if_local( - expr * e, - func_decl * fd, - const unsigned & fd_inx, - const mpz & temp, - double & best_score, - unsigned & best_const, - mpz & best_value) -{ +bool sls_engine::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) { @@ -356,19 +377,13 @@ void sls_engine::mk_random_move(ptr_vector & unsat_constants) m_mpz_manager.del(new_value); } -void sls_engine::mk_random_move() { - mk_random_move(m_tracker.get_unsat_constants(m_assertions, m_stats.m_moves)); +void sls_engine::mk_random_move(goal_ref const & g) { + mk_random_move(m_tracker.get_unsat_constants(g, m_stats.m_moves)); } // will use VNS to ignore some possible moves and increase the flips per second -double sls_engine::find_best_move_vns( - ptr_vector & to_evaluate, - double score, - unsigned & best_const, - mpz & best_value, - unsigned & new_bit, - move_type & move) -{ +double sls_engine::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; @@ -384,31 +399,31 @@ double sls_engine::find_best_move_vns( if (!m_mpz_manager.is_even(old_value)) { // for odd values, try +1 mk_inc(bv_sz, old_value, temp); - if (what_if(fd, i, temp, new_score, best_const, best_value)) + 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(fd, i, temp, new_score, best_const, best_value)) + 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(fd, i, temp, new_score, best_const, best_value)) + 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(fd, i, temp, new_score, best_const, best_value)) { + 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(fd, old_value); + double check = incremental_score(g, fd, old_value); SASSERT(check == score); } @@ -430,13 +445,13 @@ double sls_engine::find_best_move_vns( { mk_flip(srt, old_value, j, temp); - if (what_if(fd, i, temp, new_score, best_const, best_value)) { + 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(fd, old_value); + double check = incremental_score(g, fd, old_value); SASSERT(check == score); } m_mpz_manager.del(old_value); @@ -444,23 +459,99 @@ double sls_engine::find_best_move_vns( return new_score; } +double sls_engine::find_best_move_lsb(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(); 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) { + // 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 (!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 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); + } + + for (unsigned j = 1; j < max_bv_sz; j++) + { + 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)); + + // 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; +} + // finds the move that increased score the most. returns best_const = -1, if no increasing move exists. -double sls_engine::find_best_move( - ptr_vector & to_evaluate, - double score, - unsigned & best_const, - mpz & best_value, - unsigned & new_bit, - move_type & move) -{ +double sls_engine::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; +#if _INSIST_PERC_ + double new_score = m_tracker.get_random_uint(16) % 100 < _INSIST_PERC_ ? 0.0 : score; +#else double new_score = score; +#endif - for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0; i++) { + m_tracker.reset_equal_scores(); + +// for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0; i++) { + for (unsigned i = 0; i < to_evaluate.size(); i++) { +// for (unsigned i = m_tracker.get_random_uint(16) % to_evaluate.size(); i != to_evaluate.size(); i = to_evaluate.size()) { +// for (unsigned i = to_evaluate.size(); i-- > 0; ) { 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); @@ -470,15 +561,28 @@ double sls_engine::find_best_move( #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++) { +// for (unsigned j = 0; j < bv_sz && new_score < 1.0; j++) { + for (unsigned j = 0; j < bv_sz; j++) { +// for (unsigned j = bv_sz; j-- > 0; ) { #endif // What would happen if we flipped bit #i ? mk_flip(srt, old_value, j, temp); - if (what_if(fd, i, temp, new_score, best_const, best_value)) { + //if (m_tracker.get_random_uint(1)) + //if ((move != MV_FLIP) || (new_bit > j)) + //{ + //if (what_if_new(g, fd, i, temp, new_score, best_const, best_value)) { + // new_bit = j; + // move = MV_FLIP; + //} + //} + //else + //{ + 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) { @@ -486,19 +590,22 @@ double sls_engine::find_best_move( if (!m_mpz_manager.is_even(old_value)) { // for odd values, try +1 mk_inc(bv_sz, old_value, temp); - if (what_if(fd, i, temp, new_score, best_const, best_value)) + //if (m_tracker.get_random_uint(1)) + 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(fd, i, temp, new_score, best_const, best_value)) + //if (m_tracker.get_random_uint(1)) + 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(fd, i, temp, new_score, best_const, best_value)) + //if (m_tracker.get_random_uint(1)) + if (what_if(g, fd, i, temp, new_score, best_const, best_value)) move = MV_INV; #if _USE_UNARY_MINUS_ @@ -528,7 +635,7 @@ double sls_engine::find_best_move( } // reset to what it was before - double check = incremental_score(fd, old_value); + double check = incremental_score(g, fd, old_value); // Andreas: does not hold anymore now that we use top level score caching //SASSERT(check == score); } @@ -538,6 +645,50 @@ double sls_engine::find_best_move( #if _USE_MUL3_ m_mpz_manager.del(temp2); #endif + + if ((new_score == score) && 1)// (m_tracker.get_random_uint(1))) + best_const = -1; + + return new_score; +} + +// finds the move that increased score the most. returns best_const = -1, if no increasing move exists. +double sls_engine::find_best_move_mc(goal_ref const & g, ptr_vector & to_evaluate, double score, + unsigned & best_const, mpz & best_value) { + mpz old_value, temp, temp2; + unsigned bv_sz; + double new_score = score; + +// for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0; i++) { + for (unsigned i = 0; i < to_evaluate.size(); i++) { + func_decl * fd = to_evaluate[i]; + sort * srt = fd->get_range(); + bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); + m_mpz_manager.set(old_value, m_tracker.get_value(fd)); + + if (m_bv_util.is_bv_sort(srt) && bv_sz > 2) { +// for (unsigned j = 0; j < bv_sz && new_score < 1.0; j++) { + for (unsigned j = 0; j < bv_sz; j++) { + mk_flip(srt, old_value, j, temp); + for (unsigned l = 0; l < _VNS_MC_TRIES_ && l < bv_sz / 2; l++) + { + unsigned k = m_tracker.get_random_uint(16) % bv_sz; + while (k == j) + k = m_tracker.get_random_uint(16) % bv_sz; + mk_flip(srt, temp, k, temp2); + what_if(g, fd, i, temp2, new_score, best_const, best_value); + } + } + } + + // reset to what it was before + double check = incremental_score(g, fd, old_value); + } + + m_mpz_manager.del(old_value); + m_mpz_manager.del(temp); + m_mpz_manager.del(temp2); + return new_score; } @@ -596,15 +747,15 @@ double sls_engine::find_best_move_local(expr * e, ptr_vector & to_eva } // first try of intensification ... does not seem to be efficient -bool sls_engine::handle_plateau() +bool sls_engine::handle_plateau(goal_ref const & g) { - unsigned sz = m_assertions.size(); + 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(sz, pos); + expr * e = m_tracker.get_unsat_assertion(g, sz, pos); if (!e) return 0; @@ -658,15 +809,10 @@ bool sls_engine::handle_plateau() } // what_if version needed in the context of 2nd intensification try, combining local and global score -bool sls_engine::what_if( - expr * e, - func_decl * fd, - const mpz & temp, - double & best_score, - mpz & best_value, - unsigned i) -{ - double global_score = incremental_score(fd, temp); +bool sls_engine::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_; @@ -680,7 +826,7 @@ bool sls_engine::what_if( } // find_best_move version needed in the context of 2nd intensification try -double sls_engine::find_best_move_local(expr * e, func_decl * fd, mpz & best_value, unsigned i) +double sls_engine::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; @@ -691,7 +837,7 @@ double sls_engine::find_best_move_local(expr * e, func_decl * fd, mpz & best_val for (unsigned j = 0; j < bv_sz && best_score < 1.0; j++) { mk_flip(srt, old_value, j, temp); - what_if(e, fd, temp, best_score, best_value, i); + what_if(g, e, fd, temp, best_score, best_value, i); } m_mpz_manager.del(old_value); @@ -701,15 +847,15 @@ double sls_engine::find_best_move_local(expr * e, func_decl * fd, mpz & best_val } // second try to use intensification ... also not very effective -bool sls_engine::handle_plateau(double old_score) +bool sls_engine::handle_plateau(goal_ref const & g, double old_score) { - unsigned sz = m_assertions.size(); + 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(m_assertions, sz, new_const); + expr * e = m_tracker.get_unsat_assertion(g, sz, new_const); if (!e) return 0; @@ -726,12 +872,12 @@ bool sls_engine::handle_plateau(double old_score) for (unsigned i = 1; i <= _INTENSIFICATION_TRIES_; i++) { - new_score = find_best_move_local(q, fd, new_value, 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(fd, new_value); + 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_); @@ -744,7 +890,7 @@ bool sls_engine::handle_plateau(double old_score) } // main search loop -lbool sls_engine::search() { +lbool sls_engine::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; @@ -752,8 +898,15 @@ lbool sls_engine::search() { move_type move; unsigned plateau_cnt = 0; - score = rescore(); - unsigned sz = m_assertions.size(); + score = rescore(g); + unsigned sz = g->size(); + + 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;); + #if _PERC_STICKY_ expr * e = m_tracker.get_unsat_assertion(g, m_stats.m_moves); #endif @@ -767,9 +920,18 @@ lbool sls_engine::search() { #else while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) { #endif + //if (m_stats.m_stopwatch.get_current_seconds() > 10.0) + //{printf("Got %f fps and size is %d with avg bw %f\n", m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds(), m_tracker.get_formula_size(), m_tracker.get_avg_bw(g)); exit(0);} + checkpoint(); m_stats.m_moves++; +#if _UCT_FORGET_ + //if (m_stats.m_moves % sz == 0) + if (m_stats.m_moves % _UCT_FORGET_ == 0) + m_tracker.uct_forget(g); +#endif + #if _REAL_RS_ || _REAL_PBFS_ //m_tracker.debug_real(g, m_stats.m_moves); #endif @@ -779,13 +941,14 @@ lbool sls_engine::search() { if (m_tracker.get_random_uint(16) % 100 >= _PERC_STICKY_ || m_mpz_manager.eq(m_tracker.get_value(e), m_one)) e = m_tracker.get_unsat_assertion(g, m_stats.m_moves); #else - expr * e = m_tracker.get_unsat_assertion(m_assertions, m_stats.m_moves); + expr * e = m_tracker.get_unsat_assertion(g, m_stats.m_moves); #endif if (!e) { res = l_true; goto bailout; } + //ptr_vector & to_evaluate = m_tracker.get_unsat_constants_only(e); ptr_vector & to_evaluate = m_tracker.get_unsat_constants_walksat(e); #else ptr_vector & to_evaluate = m_tracker.get_unsat_constants_gsat(g, sz); @@ -818,13 +981,69 @@ lbool sls_engine::search() { #endif old_score = score; new_const = (unsigned)-1; + move = MV_FLIP; + new_bit = 0; #if _VNS_ score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move); #else - score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move); + score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move); #endif +#if _VNS_MC_ > _VNS_REPICK_ +#if _VNS_MC_ + if (new_const == static_cast(-1)) + if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_) + score = find_best_move_mc(g, to_evaluate, score, new_const, new_value); +#endif +#if _VNS_REPICK_ + if (new_const == static_cast(-1)) + if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_) { + expr * q = m_tracker.get_new_unsat_assertion(g, e); + if (q) + { + ptr_vector & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e); + score = find_best_move(g, to_evaluate2, score, new_const, new_value, new_bit, move); + } + } +#endif +#endif + +#if _VNS_MC_ < _VNS_REPICK_ +#if _VNS_REPICK_ + if (new_const == static_cast(-1)) + if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_) { + expr * q = m_tracker.get_new_unsat_assertion(g, e); + if (q) + { + ptr_vector & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e); + score = find_best_move(g, to_evaluate2, score, new_const, new_value, new_bit, move); + } + } +#endif +#if _VNS_MC_ + if (new_const == static_cast(-1)) + if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_) + score = find_best_move_mc(g, to_evaluate, score, new_const, new_value); +#endif +#endif + +#if (_VNS_MC_ == _VNS_REPICK_) && _VNS_MC_ && _VNS_REPICK_ + if (new_const == static_cast(-1)) { + if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_) + score = find_best_move_mc(g, to_evaluate, score, new_const, new_value); + else { + expr * q = m_tracker.get_new_unsat_assertion(g, e); + if (q) + { + ptr_vector & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e); + score = find_best_move(g, to_evaluate2, score, new_const, new_value, new_bit, move); + } + } + } +#endif + + if (new_const == static_cast(-1)) { score = old_score; plateau_cnt++; @@ -839,25 +1058,52 @@ lbool sls_engine::search() { mk_random_move(to_evaluate); else #endif -#if _REPICK_ - m_evaluator.randomize_local(m_assertions, m_stats.m_moves); +#if _REPICK_ == 1 + m_evaluator.randomize_local(g, m_stats.m_moves); +#elif _REPICK_ == 2 + { + expr * q = m_tracker.get_new_unsat_assertion(g, e); + if (q) + m_evaluator.randomize_local(q); + else + m_evaluator.randomize_local(e); + } #else - m_evaluator.randomize_local(to_evaluate); + m_evaluator.randomize_local_n(g, to_evaluate); + //m_evaluator.randomize_local(to_evaluate); #endif #endif #if _CACHE_TOP_SCORE_ - score = m_tracker.get_top_sum() / m_assertions.size(); + score = m_tracker.get_top_sum() / g->size(); #else score = top_score(g); #endif + +#if _PAWS_ + for (unsigned i = 0; i < sz; i++) + { + expr * q = g->form(i); + if (m_tracker.get_random_uint(16) % 100 < _PAWS_) + { + if (m_mpz_manager.eq(m_tracker.get_value(q),m_one)) + m_tracker.decrease_weight(q); + } + else + { + if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero)) + m_tracker.increase_weight(q); + } + } +#endif + } else { func_decl * fd = to_evaluate[new_const]; -#if _REAL_RS_ || _REAL_PBFS_ +#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_ score = serious_score(g, fd, new_value); #else - score = incremental_score(fd, new_value); + score = incremental_score(g, fd, new_value); #endif } } @@ -868,20 +1114,19 @@ bailout: return res; } -#if 0 // Old code. // main search loop -lbool sls_engine::search_old() { +lbool sls_engine::search_old(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(); + score = rescore(g); TRACE("sls", tout << "Starting search, initial score = " << std::setprecision(32) << score << std::endl; tout << "Score distribution:"; - for (unsigned i = 0; i < m_assertions.size(); i++) - tout << " " << std::setprecision(3) << m_tracker.get_score(m_assertions[i]); + 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; @@ -927,7 +1172,7 @@ lbool sls_engine::search_old() { old_score = score; new_const = (unsigned)-1; - ptr_vector & to_evaluate = m_tracker.get_unsat_constants(m_assertions, m_stats.m_moves); + ptr_vector & to_evaluate = m_tracker.get_unsat_constants(g, m_stats.m_moves); if (!to_evaluate.size()) { res = l_true; @@ -938,22 +1183,22 @@ lbool sls_engine::search_old() { tout << to_evaluate[i]->get_name() << std::endl;); #if _VNS_ - score = find_best_move_vns(to_evaluate, score, new_const, new_value, new_bit, move); + score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move); #else - score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move); + 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 < m_assertions.size(); i++) { - if (!m_mpz_manager.is_one(m_tracker.get_value(m_assertions[i]))) - tout << mk_ismt2_pp(m_assertions[i], m_manager) << 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 < m_assertions.size(); i++) - tout << mk_ismt2_pp(m_assertions[i], m_manager) << " ---> " << - m_tracker.get_score(m_assertions[i]) << 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; } @@ -991,15 +1236,15 @@ lbool sls_engine::search_old() { case MV_DIV2: m_stats.m_div2s++; break; } -#if _REAL_RS_ || _REAL_PBFS_ - score = serious_score(fd, new_value); +#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_ + score = serious_score(g, fd, new_value); #else - score = incremental_score(fd, new_value); + score = incremental_score(g, fd, new_value); #endif TRACE("sls", tout << "Score distribution:"; - for (unsigned i = 0; i < m_assertions.size(); i++) - tout << " " << std::setprecision(3) << m_tracker.get_score(m_assertions[i]); + for (unsigned i = 0; i < g->size(); i++) + tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i)); tout << " TOP: " << score << std::endl;); } @@ -1008,8 +1253,8 @@ lbool sls_engine::search_old() { // score could theoretically be imprecise. // 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 < m_assertions.size() && all_true; i++) - if (!m_mpz_manager.is_one(m_tracker.get_value(m_assertions[i]))) + 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 @@ -1040,17 +1285,17 @@ lbool sls_engine::search_old() { TRACE("sls", tout << "In a plateau (" << plateau_cnt << "/" << m_plateau_limit << "); randomizing locally." << std::endl;); #if _INTENSIFICATION_ handle_plateau(g, score); - //handle_plateau(); + //handle_plateau(g); #else - m_evaluator.randomize_local(m_assertions, m_stats.m_moves); + m_evaluator.randomize_local(g, m_stats.m_moves); #endif - //mk_random_move(); - score = top_score(); + //mk_random_move(g); + score = top_score(g); if (score >= 1.0) { bool all_true = true; - for (unsigned i = 0; i < m_assertions.size() && all_true; i++) - if (!m_mpz_manager.is_one(m_tracker.get_value(m_assertions[i]))) + 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 @@ -1067,17 +1312,6 @@ bailout: return res; } -#endif - -void sls_engine::init_tracker() { -#if _WEIGHT_DIST_ == 4 - m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); -#endif -#if _WEIGHT_TOGGLE_ - m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_); -#endif - m_tracker.initialize(m_assertions); -} void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { if (g->inconsistent()) { @@ -1087,9 +1321,6 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { m_produce_models = g->models_enabled(); - for (unsigned i = 0; i < g->size(); i++) - assert_expr(g->form(i)); - verbose_stream() << "_BFS_ " << _BFS_ << std::endl; verbose_stream() << "_FOCUS_ " << _FOCUS_ << std::endl; verbose_stream() << "_PERC_STICKY_ " << _PERC_STICKY_ << std::endl; @@ -1100,7 +1331,14 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { 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() << "_PAWS_ " << _PAWS_ << std::endl; + verbose_stream() << "_PAWS_INIT_ " << _PAWS_INIT_ << std::endl; verbose_stream() << "_VNS_ " << _VNS_ << std::endl; + verbose_stream() << "_VNS_MC_ " << _VNS_MC_ << std::endl; + verbose_stream() << "_VNS_MC_TRIES_ " << _VNS_MC_TRIES_ << std::endl; + verbose_stream() << "_VNS_REPICK_ " << _VNS_REPICK_ << std::endl; + verbose_stream() << "_VNS_PERC_ " << _VNS_PERC_ << std::endl; + verbose_stream() << "_INSIST_PERC_ " << _INSIST_PERC_ << 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; @@ -1111,6 +1349,8 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { verbose_stream() << "_UCT_CONSTANT_ " << std::fixed << std::setprecision(2) << _UCT_CONSTANT_ << std::endl; verbose_stream() << "_UCT_RESET_ " << _UCT_RESET_ << std::endl; verbose_stream() << "_UCT_INIT_ " << _UCT_INIT_ << std::endl; + verbose_stream() << "_UCT_FORGET_ " << _UCT_FORGET_ << std::endl; + verbose_stream() << "_UCT_FORGET_FACTOR_ " << std::fixed << std::setprecision(2) << _UCT_FORGET_FACTOR_ << std::endl; verbose_stream() << "_PROBABILISTIC_UCT_ " << _PROBABILISTIC_UCT_ << std::endl; verbose_stream() << "_UCT_EPS_ " << std::fixed << std::setprecision(4) << _UCT_EPS_ << std::endl; verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl; @@ -1125,9 +1365,36 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { 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; + verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl; - lbool res = operator()(); +#if _WEIGHT_DIST_ == 4 + m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_); +#endif +#if _WEIGHT_TOGGLE_ + m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_); +#endif + m_tracker.initialize(g); + lbool res = l_undef; + + m_restart_limit = _RESTART_LIMIT_; + + do { + checkpoint(); + + report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts); + res = search(g); + + if (res == l_undef) + { +#if _RESTART_INIT_ + m_tracker.randomize(g); +#else + m_tracker.reset(g); +#endif + } + } 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); @@ -1149,38 +1416,13 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { mc = 0; } -lbool sls_engine::operator()() { - init_tracker(); - lbool res = l_undef; - - m_restart_limit = _RESTART_LIMIT_; - - do { - checkpoint(); - - report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts); - res = search(); - - if (res == l_undef) - { -#if _RESTART_INIT_ - m_tracker.randomize(); -#else - m_tracker.reset(m_assertions); -#endif - } - } 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; - - return res; -} - unsigned sls_engine::check_restart(unsigned curr_value) { if (curr_value > m_restart_limit) { -#if _RESTART_SCHEME_ == 4 +#if _RESTART_SCHEME_ == 5 + m_restart_limit += (unsigned)(_RESTART_LIMIT_ * pow(_RESTART_CONST_ARMIN_, m_stats.m_restarts)); +#elif _RESTART_SCHEME_ == 4 m_restart_limit += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? _RESTART_LIMIT_ : (_RESTART_LIMIT_ * m_stats.m_restarts + 1); #elif _RESTART_SCHEME_ == 3 m_restart_limit += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * _RESTART_LIMIT_; @@ -1188,9 +1430,11 @@ unsigned sls_engine::check_restart(unsigned curr_value) m_restart_limit += get_luby(m_stats.m_restarts + 1) * _RESTART_LIMIT_; #elif _RESTART_SCHEME_ == 1 if (m_stats.m_restarts & 1) + //if (m_stats.m_restarts % 3 == 2) m_restart_limit += _RESTART_LIMIT_; else m_restart_limit += (2 << (m_stats.m_restarts >> 1)) * _RESTART_LIMIT_; + //m_restart_limit += (2 << (m_stats.m_restarts / 3)) * _RESTART_LIMIT_; #else m_restart_limit += _RESTART_LIMIT_; #endif @@ -1201,4 +1445,4 @@ unsigned sls_engine::check_restart(unsigned curr_value) return 0; } return 1; -} +} \ No newline at end of file diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index c6e3af155..902c6b7a0 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -22,7 +22,6 @@ Notes: #include"stopwatch.h" #include"lbool.h" #include"model_converter.h" -#include"goal.h" #include"sls_compilation_settings.h" #include"sls_tracker.h" @@ -72,7 +71,6 @@ protected: bv_util m_bv_util; sls_tracker m_tracker; sls_evaluator m_evaluator; - ptr_vector m_assertions; unsigned m_restart_limit; unsigned m_max_restarts; @@ -94,12 +92,11 @@ public: void updt_params(params_ref const & _p); - void assert_expr(expr * e) { m_assertions.push_back(e); } - stats const & get_stats(void) { return m_stats; } void reset_statistics(void) { m_stats.reset(); } - bool full_eval(model & mdl); + bool full_eval(goal_ref const & g, model & mdl); + void mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result); void mk_mul2(unsigned bv_sz, const mpz & old_value, mpz & result); @@ -107,48 +104,66 @@ public: void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented); void mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented); void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted); - void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped); + void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped); - void init_tracker(void); + 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); - lbool search(void); + double find_best_move_lsb(goal_ref const & g, ptr_vector & to_evaluate, double score, + unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move); + + double find_best_move_mc(goal_ref const & g, ptr_vector & to_evaluate, double score, + unsigned & best_const, mpz & best_value); + + double find_best_move_local(expr * e, ptr_vector & to_evaluate, + unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move); + + + + bool what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz & temp, + double & best_score, mpz & best_value, unsigned i); + + double find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i); + + + lbool search(goal_ref const & g); - lbool operator()(); void operator()(goal_ref const & g, model_converter_ref & mc); protected: void checkpoint(); + lbool search_old(goal_ref const & g); double get_restart_armin(unsigned cnt_restarts); - bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, + 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); - bool what_if(expr * e, func_decl * fd, const mpz & temp, - double & best_score, mpz & best_value, unsigned i); + + bool what_if_new(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp, + double & best_score, unsigned & best_const, mpz & best_value); + double incremental_score_prune_new(goal_ref const & g, func_decl * fd, const mpz & new_value); + 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); - double top_score(); - double rescore(); - double serious_score(func_decl * fd, const mpz & new_value); - double incremental_score(func_decl * fd, const mpz & new_value); + double top_score(goal_ref const & g); + double rescore(goal_ref const & g); + double serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value); + double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value); #if _EARLY_PRUNE_ - double incremental_score_prune(func_decl * fd, const mpz & new_value); + double incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value); #endif - double find_best_move(ptr_vector & to_evaluate, double score, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move); - double find_best_move_local(expr * e, func_decl * fd, mpz & best_value, unsigned i); - double find_best_move_local(expr * e, ptr_vector & to_evaluate, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move); - double find_best_move_vns(ptr_vector & to_evaluate, double score, - unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move); - void mk_random_move(ptr_vector & unsat_constants); - void mk_random_move(); - bool handle_plateau(void); - bool handle_plateau(double old_score); + 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); + + void mk_random_move(ptr_vector & unsat_constants); + void mk_random_move(goal_ref const & g); + + bool handle_plateau(goal_ref const & g); + bool handle_plateau(goal_ref const & g, double old_score); inline unsigned check_restart(unsigned curr_value); }; -#endif +#endif \ No newline at end of file diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 7638ba5f4..78f2cb79a 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -575,7 +575,7 @@ public: #if _CACHE_TOP_SCORE_ //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); + m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); #endif m_tracker.set_score(cur, new_score); m_tracker.set_score_prune(cur, new_score); @@ -584,12 +584,13 @@ public: new_score = m_tracker.score(cur); //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); + m_tracker.adapt_top_sum(cur, 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 +#endif + if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); for (unsigned j = 0; j < ups.size(); j++) { @@ -634,7 +635,7 @@ public: #if _CACHE_TOP_SCORE_ //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); + m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); #endif m_tracker.set_score(cur, new_score); m_tracker.set_score_prune(cur, new_score); @@ -643,12 +644,12 @@ public: new_score = m_tracker.score(cur); //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); + m_tracker.adapt_top_sum(cur, 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 +#endif if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); for (unsigned j = 0; j < ups.size(); j++) { @@ -683,7 +684,7 @@ public: m_traversal_stack[cur_depth].push_back(ep); if (cur_depth > max_depth) max_depth = cur_depth; } -#if _REAL_RS_ || _REAL_PBFS_ +#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_ run_serious_update(max_depth); #else run_update(max_depth); @@ -729,14 +730,16 @@ public: #if _CACHE_TOP_SCORE_ //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); + m_tracker.adapt_top_sum(cur, 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))) + //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))) + //if ((new_score < prune_score) && (m_tracker.has_neg_occ(cur))) pot_benefits = 1; if (m_tracker.has_uplinks(cur)) { @@ -771,7 +774,7 @@ public: new_score = m_tracker.score(cur); //if (!m_tracker.has_uplinks(cur)) if (m_tracker.is_top_expr(cur)) - m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur)); + m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); m_tracker.set_score(cur, new_score); #else m_tracker.set_score(cur, m_tracker.score(cur)); @@ -858,6 +861,104 @@ public: } #endif + unsigned run_update_bool_prune_new(unsigned cur_depth) { + expr_fast_mark1 visited; + + double prune_score, new_score; + unsigned pot_benefits = 0; + SASSERT(cur_depth < m_traversal_stack_bool.size()); + + ptr_vector & cur_depth_exprs = m_traversal_stack_bool[cur_depth]; + + for (unsigned i = 0; i < cur_depth_exprs.size(); i++) { + expr * cur = cur_depth_exprs[i]; + + new_score = m_tracker.score(cur); + //if (!m_tracker.has_uplinks(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); + } + } + } + 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]; + + new_score = m_tracker.score(cur); + //if (!m_tracker.has_uplinks(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; + } + + unsigned update_prune_new(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_new(cur_depth); + } + void randomize_local(ptr_vector & unsat_constants) { // Randomize _all_ candidates: @@ -901,7 +1002,7 @@ public: mpz temp = m_tracker.get_random(fd->get_range()); #endif -#if _REAL_RS_ || _REAL_PBFS_ +#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_ serious_update(fd, temp); #else update(fd, temp); @@ -922,9 +1023,36 @@ public: randomize_local(m_tracker.get_constants(e)); } - void randomize_local(ptr_vector const & as, unsigned int flip) { - randomize_local(m_tracker.get_unsat_constants(as, flip)); + void randomize_local(goal_ref const & g, unsigned int flip) { + randomize_local(m_tracker.get_unsat_constants(g, flip)); } + + void randomize_local_n(goal_ref const & g, ptr_vector & unsat_constants) { + unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size(); + func_decl * fd = unsat_constants[r]; + sort * srt = fd->get_range(); + unsigned bv_sz = m_manager.is_bool(srt) ? 1 : m_bv_util.get_bv_size(srt); + mpz max_val = m_tracker.get_random(srt); + update(fd, max_val); + double max_score = m_tracker.get_top_sum() / g->size(); + mpz temp_val; + double temp_score; + for (unsigned i = 1; i < 2; i++) + //for (unsigned i = 1; i < bv_sz; i++) + { + m_mpz_manager.set(temp_val, m_tracker.get_random(srt)); + update(fd, temp_val); + temp_score = m_tracker.get_top_sum() / g->size(); + if (temp_score > max_score) + { + m_mpz_manager.set(max_val, temp_val); + max_score = temp_score; + } + } + update(fd, max_val); + m_mpz_manager.del(temp_val); + m_mpz_manager.del(max_val); + } }; #endif \ No newline at end of file diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index b2b7035e0..0b6b01e7c 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -1509,14 +1509,14 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) { mk_max_bv_sharing_tactic(m), // Andreas: It would be cool to get rid of shared top level assertions but which simplification is doing this? //mk_ctx_simplify_tactic(m, ctx_p), - // Andreas: This one at least eliminates top level duplicates ... + // Andreas: This one at least eliminates top level duplicates ... but has very bad effects on performance! //mk_simplify_tactic(m), - // Andreas: How does a NNF actually look like? Can it contain ITE operators? mk_nnf_tactic(m, p)); } tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m)); +// tactic * t = and_then(mk_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 537492213..87c90f1f8 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -20,9 +20,7 @@ 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"goal.h" #include"model.h" #include"sls_compilation_settings.h" @@ -88,12 +86,17 @@ private: obj_map m_where_false; expr** m_list_false; #endif +#if _PAWS_ + obj_map m_weights; + //obj_map m_weights; +#endif #if _CACHE_TOP_SCORE_ double m_top_sum; #endif #if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_ double m_weight_dist_factor; #endif + unsigned m_equal_scores; public: sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : @@ -113,15 +116,52 @@ public: m_mpz_manager.del(m_two); } + 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; + } + #if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_ inline void set_weight_dist_factor(double val) { m_weight_dist_factor = val; } #endif + void reset_equal_scores() { + m_equal_scores = 1; + } + + unsigned inc_equal_scores() { + return ++m_equal_scores; + } + #if _CACHE_TOP_SCORE_ - inline void adapt_top_sum(double add, double sub) { + inline void adapt_top_sum(expr * e, double add, double sub) { +#if _PAWS_ + m_top_sum += m_weights.find(e) * (add - sub); +#else m_top_sum += add - sub; +#endif } inline void set_top_sum(double new_score) { @@ -278,19 +318,21 @@ public: } #endif - void uct_forget(ptr_vector & as) { +#if _UCT_ + void uct_forget(goal_ref const & g) { expr * e; unsigned touched_old, touched_new; - for (unsigned i = 0; i < as.size(); i++) + for (unsigned i = 0; i < g->size(); i++) { - e = as[i]; + e = g->form(i); touched_old = m_scores.find(e).touched; touched_new = (unsigned)((touched_old - 1) * _UCT_FORGET_FACTOR_ + 1); m_scores.find(e).touched = touched_new; m_touched += touched_new - touched_old; } } +#endif void initialize(app * n) { // Build score table @@ -367,12 +409,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(); @@ -420,12 +462,12 @@ public: 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]; + expr * e = g->form(i); if (!m_top_expr.contains(e)) m_top_expr.insert(e); else @@ -440,7 +482,7 @@ public: 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 || _INTENSIFICATION_ initialize_recursive(e); @@ -452,7 +494,7 @@ 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); ); @@ -465,16 +507,49 @@ public: //} #endif +#if _PAWS_ + for (unsigned i = 0; i < sz; i++) + { + expr * e = g->form(i); + if (!m_weights.contains(e)) + m_weights.insert(e, _PAWS_INIT_); + } +#endif + #if _EARLY_PRUNE_ for (unsigned i = 0; i < sz; i++) - setup_occs(as[i]); + setup_occs(g->form(i)); #endif #if _UCT_ - m_touched = _UCT_INIT_ ? as.size() : 1; + m_touched = _UCT_INIT_ ? g->size() : 1; #endif } +#if _PAWS_ + void increase_weight(expr * e) + { + //printf("Increasing %d to", m_weights.find(e)); + m_weights.find(e)++; + //m_weights.find(e) *= 1.1; + //printf(" %d\n", m_weights.find(e)); + } + + void decrease_weight(expr * e) + { + unsigned old_weight = m_weights.find(e); + m_weights.find(e) = old_weight > _PAWS_INIT_ ? old_weight - 1 : _PAWS_INIT_; + //m_weights.find(e) = old_weight > 1.1 ? old_weight / 1.1 : 1; + //printf("Decreasing %d to %d\n", old_weight, m_weights.find(e)); + } + + unsigned get_weight(expr * e) + //double get_weight(expr * e) + { + return m_weights.find(e); + } +#endif + #if _REAL_RS_ || _REAL_PBFS_ void make_assertion(expr * e) { @@ -608,7 +683,7 @@ public: NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. } - void randomize(ptr_vector const & as) { + void randomize(goal_ref const & g) { 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++) { @@ -622,13 +697,13 @@ public: TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); #if _UCT_RESET_ - m_touched = _UCT_INIT_ ? as.size() : 1; - for (unsigned i = 0; i < as.size(); i++) - m_scores.find(as[i]).touched = 1; + m_touched = _UCT_INIT_ ? g->size() : 1; + for (unsigned i = 0; i < g->size(); i++) + m_scores.find(g->form(i)).touched = 1; #endif } - void reset(ptr_vector const & as) { + void reset(goal_ref const & g) { 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++) { @@ -638,9 +713,9 @@ public: } #if _UCT_RESET_ - m_touched = _UCT_INIT_ ? as.size() : 1; - for (unsigned i = 0; i < as.size(); i++) - m_scores.find(as[i]).touched = 1; + m_touched = _UCT_INIT_ ? g->size() : 1; + for (unsigned i = 0; i < g->size(); i++) + m_scores.find(g->form(i)).touched = 1; #endif } @@ -765,6 +840,7 @@ public: const mpz & v1 = get_value(arg1); if (negated) { + //res = (m_mpz_manager.eq(v0, v1)) ? 0.5 * (m_bv_util.get_bv_size(arg0) - 1.0) / m_bv_util.get_bv_size(arg0) : 1.0; res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0; TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << m_mpz_manager.to_string(v1) << std::endl; ); @@ -811,40 +887,209 @@ public: SASSERT(a->get_num_args() == 2); const mpz & x = get_value(a->get_arg(0)); const mpz & y = get_value(a->get_arg(1)); - unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); + int bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); if (negated) { if (m_mpz_manager.gt(x, y)) + { + /*mpz diff; + m_mpz_manager.sub(x, y, diff); + m_mpz_manager.inc(diff); + rational n(diff); + n /= rational(m_powers(bv_sz)); + double dbl = n.get_double(); + // In extreme cases, n is 0.9999 but to_double returns something > 1.0 + m_mpz_manager.del(diff); + res = 1.0 + 0.5 * dbl;*/ res = 1.0; + } else { + //res = (bv_sz - 1.0) / bv_sz; +/* mpz x_copy, y_copy; + m_mpz_manager.set(x_copy, x); + m_mpz_manager.set(y_copy, y); + unsigned lower_gt = 0; + unsigned curr_gt = 0; + int last_pos = -1; + for (int i = 0; i < bv_sz; i++) + { + if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy)) + { + lower_gt = curr_gt; + curr_gt = 1; + last_pos = i; + } + else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy)) + { + lower_gt = curr_gt; + curr_gt = 0; + last_pos = i; + } + + m_mpz_manager.machine_div(x_copy, m_two, x_copy); + m_mpz_manager.machine_div(y_copy, m_two, y_copy); + } + + res = (double)(bv_sz - last_pos - 1 + 2 * lower_gt) / (double)(bv_sz + 2); + m_mpz_manager.del(x_copy); + m_mpz_manager.del(y_copy);*/ +#if 1 mpz diff; m_mpz_manager.sub(y, x, diff); m_mpz_manager.inc(diff); rational n(diff); n /= rational(m_powers(bv_sz)); + double dbl = 1.0 - n.get_double(); + // In extreme cases, n is 0.9999 but to_double returns something > 1.0 + res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; + //res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; + m_mpz_manager.del(diff); +#endif + } + } + else { + if (m_mpz_manager.le(x, y)) + { + /*mpz diff; + m_mpz_manager.sub(y, x, diff); + m_mpz_manager.inc(diff); + rational n(diff); + n /= rational(m_powers(bv_sz)); 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); - } - } - else { - if (m_mpz_manager.le(x, y)) + res = 1.0 + 0.5 * dbl;*/ res = 1.0; + } else { + //res = (bv_sz - 1.0) / bv_sz; +/* mpz x_copy, y_copy; + m_mpz_manager.set(x_copy, x); + m_mpz_manager.set(y_copy, y); + unsigned lower_le = 1; + unsigned curr_le = 1; + int last_pos = -1; + for (int i = 0; i < bv_sz; i++) + { + if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy)) + { + lower_le = curr_le; + curr_le = 0; + last_pos = i; + } + else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy)) + { + lower_le = curr_le; + curr_le = 1; + last_pos = i; + } + + m_mpz_manager.machine_div(x_copy, m_two, x_copy); + m_mpz_manager.machine_div(y_copy, m_two, y_copy); + } + + res = (double)(bv_sz - last_pos - 1 + 2 * lower_le) / (double)(bv_sz + 2);*/ +#if 1 mpz diff; m_mpz_manager.sub(x, y, diff); rational n(diff); n /= rational(m_powers(bv_sz)); - double dbl = n.get_double(); + double dbl = 1.0 - n.get_double(); res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; m_mpz_manager.del(diff); +#endif } } TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); } - else if (m_bv_util.is_bv_sle(n)) { // x <= y +/* else if (m_bv_util.is_bv_sle(n)) { // x <= y + app * a = to_app(n); + 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]); + + mpz x_unsigned; + mpz y_unsigned; + const mpz & p = m_powers(bv_sz); + const mpz & p_half = m_powers(bv_sz-1); + if (x >= p_half) { m_mpz_manager.sub(x, p, x_unsigned); } + if (y >= p_half) { m_mpz_manager.sub(y, p, y_unsigned); } + + if (negated) { + if (x_unsigned > y_unsigned) + res = 1.0; + else { + mpz x_copy, y_copy; + m_mpz_manager.set(x_copy, x); + m_mpz_manager.set(y_copy, y); + unsigned lower_gt = 0; + unsigned curr_gt = 0; + int last_pos = -1; + for (int i = 0; i < bv_sz; i++) + { + if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy)) + { + lower_gt = curr_gt; + curr_gt = 1; + last_pos = i; + } + else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy)) + { + lower_gt = curr_gt; + curr_gt = 0; + last_pos = i; + } + + m_mpz_manager.machine_div(x_copy, m_two, x_copy); + m_mpz_manager.machine_div(y_copy, m_two, y_copy); + } + + res = (double)(bv_sz - last_pos - 1 + 2 * lower_gt) / (double)(bv_sz + 2); + m_mpz_manager.del(x_copy); + m_mpz_manager.del(y_copy); + } + } + else { + if (x_unsigned <= y_unsigned) + res = 1.0; + else { + mpz x_copy, y_copy; + m_mpz_manager.set(x_copy, x); + m_mpz_manager.set(y_copy, y); + unsigned lower_le = 1; + unsigned curr_le = 1; + int last_pos = -1; + for (int i = 0; i < bv_sz; i++) + { + if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy)) + { + lower_le = curr_le; + curr_le = 0; + last_pos = i; + } + else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy)) + { + lower_le = curr_le; + curr_le = 1; + last_pos = i; + } + + m_mpz_manager.machine_div(x_copy, m_two, x_copy); + m_mpz_manager.machine_div(y_copy, m_two, y_copy); + } + + res = (double)(bv_sz - last_pos - 1 + 2 * lower_le) / (double)(bv_sz + 2); + } + } + 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_unsigned); + m_mpz_manager.del(y_unsigned); + }*/ + else if (m_bv_util.is_bv_sle(n)) { // x <= y app * a = to_app(n); SASSERT(a->get_num_args() == 2); mpz x; m_mpz_manager.set(x, get_value(a->get_arg(0))); @@ -857,31 +1102,61 @@ public: if (negated) { if (x > y) - res = 1.0; + { + /*mpz diff; + m_mpz_manager.sub(x, y, diff); + m_mpz_manager.inc(diff); + rational n(diff); + n /= rational(m_powers(bv_sz)); + double dbl = n.get_double(); + // In extreme cases, n is 0.9999 but to_double returns something > 1.0 + m_mpz_manager.del(diff); + res = 1.0 + 0.5 * dbl;*/ + res = 1.0; + } else { + //res = (bv_sz - 1.0) / bv_sz; +#if 1 mpz diff; m_mpz_manager.sub(y, x, diff); m_mpz_manager.inc(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; + double dbl = 1.0 - 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); +#endif } TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); } else { if (x <= y) - res = 1.0; + { + /*mpz diff; + m_mpz_manager.sub(y, x, diff); + m_mpz_manager.inc(diff); + rational n(diff); + n /= rational(m_powers(bv_sz)); + double dbl = n.get_double(); + // In extreme cases, n is 0.9999 but to_double returns something > 1.0 + m_mpz_manager.del(diff); + res = 1.0 + 0.5 * dbl;*/ + res = 1.0; + } else { + //res = (bv_sz - 1.0) / bv_sz; +#if 1 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(); + double dbl = 1.0 - n.get_double(); res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl; m_mpz_manager.del(diff); +#endif } TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); @@ -1031,13 +1306,13 @@ public: return m_temp_constants; } - ptr_vector & get_unsat_constants_gsat(ptr_vector const & as, unsigned sz) { + ptr_vector & get_unsat_constants_gsat(goal_ref const & g, unsigned sz) { if (sz == 1) 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); @@ -1051,22 +1326,22 @@ public: return m_temp_constants; } - expr * get_unsat_assertion(ptr_vector const & as, unsigned sz, unsigned int pos) { + expr * get_unsat_assertion(goal_ref const & g, unsigned sz, unsigned int pos) { for (unsigned i = pos; i < sz; i++) { - expr * q = as[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 = as[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(ptr_vector const & as, unsigned sz, unsigned int pos) { - expr * q = get_unsat_assertion(as, sz, pos); + 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; @@ -1143,20 +1418,66 @@ public: return m_temp_constants; } - ptr_vector & get_unsat_constants_crsat(ptr_vector const & as, unsigned sz, unsigned int pos) { - expr * q = get_unsat_assertion(as, sz, pos); + 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(ptr_vector const & as, unsigned int flip) { - unsigned sz = as.size(); + void go_deeper_only(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(); + unsigned int sz = a->get_num_args(); + unsigned cnt_unsat = 0, pos = -1; + for (unsigned int i = 0; i < sz; i++) { + expr * q = args[i]; + if (m_mpz_manager.neq(get_value(q), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; + //if (m_mpz_manager.neq(get_value(q), m_one)) go_deeper(q); + } + go_deeper(args[pos]); + } + 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(); + for (unsigned int i = 0; i < sz; i++) { + expr * q = args[i]; + go_deeper(q); + } + } + //} + else + { + 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); + } + } + } + + ptr_vector & get_unsat_constants_only(expr * e) { + if (e && !m_temp_constants.size()) + go_deeper_only(e); + + return m_temp_constants; + } + + ptr_vector & get_unsat_constants(goal_ref const & g, unsigned int flip) { + unsigned sz = g->size(); if (sz == 1) { - if (m_mpz_manager.eq(get_value(as[0]), m_one)) + if (m_mpz_manager.eq(get_value(g->form(0)), m_one)) + { + m_temp_constants.reset(); return m_temp_constants; + } else return get_constants(); } @@ -1169,11 +1490,12 @@ public: #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); + #if _PROBABILISTIC_UCT_ == 2 double q = vscore.score * vscore.score; #else @@ -1203,7 +1525,7 @@ public: #else double max = -1.0; for (unsigned i = 0; i < sz; i++) { - expr * e = as[i]; + expr * e = g->form(i); // for (unsigned i = 0; i < m_where_false.size(); i++) { // expr * e = m_list_false[i]; vscore = m_scores.find(e); @@ -1221,12 +1543,12 @@ public: return m_temp_constants; #if _UCT_ == 1 || _UCT_ == 3 - m_scores.find(as[pos]).touched++; + m_scores.find(g->form(pos)).touched++; m_touched++; #elif _UCT_ == 2 - m_scores.find(as[pos]).touched = flip; + m_scores.find(g->form(pos)).touched = flip; #endif - expr * e = as[pos]; + expr * e = g->form(pos); // expr * e = m_list_false[pos]; #elif _BFS_ == 3 @@ -1304,12 +1626,15 @@ public: } } + expr * get_unsat_assertion(goal_ref const & g, unsigned int flip) { + unsigned sz = g->size(); - expr * get_unsat_assertion(ptr_vector const & as, unsigned int flip) { - unsigned sz = as.size(); - - if (sz == 1) - return as[0]; + if (sz == 1) { + if (m_mpz_manager.eq(get_value(g->form(0)), m_zero)) + return g->form(0); + else + return 0; + } m_temp_constants.reset(); #if _FOCUS_ == 1 @@ -1353,12 +1678,12 @@ public: #else double max = -1.0; for (unsigned i = 0; i < sz; i++) { - expr * e = as[i]; + expr * e = g->form(i); // for (unsigned i = 0; i < m_where_false.size(); i++) { // expr * e = m_list_false[i]; vscore = m_scores.find(e); #if _UCT_ == 1 - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched) / vscore.touched); + double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched) / vscore.touched); #elif _UCT_ == 2 double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; #elif _UCT_ == 3 @@ -1371,13 +1696,13 @@ public: return 0; #if _UCT_ == 1 || _UCT_ == 3 - m_scores.find(as[pos]).touched++; + m_scores.find(g->form(pos)).touched++; m_touched++; #elif _UCT_ == 2 m_scores.find(g->form(pos)).touched = flip; #endif // return m_list_false[pos]; - return as[pos]; + return g->form(pos); #elif _BFS_ == 3 unsigned int pos = -1; @@ -1431,7 +1756,7 @@ public: unsigned int pos = get_random_uint(16) % sz; return get_unsat_assertion(g, sz, pos); #endif - return as[pos]; + return g->form(pos); #elif _FOCUS_ == 2 #if _BFS_ unsigned int pos = flip % sz; @@ -1441,6 +1766,23 @@ public: return get_unsat_constants_crsat(g, sz, pos); #endif } + + expr * get_new_unsat_assertion(goal_ref const & g, expr * e) { + unsigned sz = g->size(); + + if (sz == 1) + return 0; + + m_temp_constants.reset(); + + 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) && (g->form(i) != e)) pos = i; + + if (pos == static_cast(-1)) + return 0; + return g->form(pos); + } }; #endif \ No newline at end of file diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index ac53ca0c8..a7870176d 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -28,6 +28,8 @@ Notes: #include"bv_size_reduction_tactic.h" #include"aig_tactic.h" #include"sat_tactic.h" +//#include"nnf_tactic.h" +//#include"sls_tactic.h" #define MEMLIMIT 300 @@ -93,6 +95,32 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { mk_sat_tactic(m)); #endif + /* use full sls + tactic * st = using_params(and_then(preamble_st, + cond(mk_is_qfbv_probe(), + cond(mk_is_qfbv_eq_probe(), + and_then(mk_bv1_blaster_tactic(m), + using_params(mk_smt_tactic(), solver_p)), + and_then(mk_nnf_tactic(m, p), mk_sls_tactic(m))), + mk_smt_tactic())), + main_p);*/ + + /* use pure dpll + tactic * st = using_params(and_then(mk_simplify_tactic(m), + cond(mk_is_qfbv_probe(), + and_then(mk_bit_blaster_tactic(m), + when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), + and_then(using_params(and_then(mk_simplify_tactic(m), + mk_solve_eqs_tactic(m)), + local_ctx_p), + if_no_proofs(cond(mk_produce_unsat_cores_probe(), + mk_aig_tactic(), + using_params(mk_aig_tactic(), + big_aig_p))))), + new_sat), + mk_smt_tactic())), + main_p);*/ + tactic * st = using_params(and_then(preamble_st, // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function // symbols. In this case, we should not use