mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

removed dependency of bvsls on goal_refs

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-03-26 17:26:06 +00:00
parent 1e55b3bfb5
commit dfd2566e25
4 changed files with 195 additions and 170 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

219
src/tactic/sls/sls_engine.cpp
View file

@ -74,15 +74,15 @@ void sls_engine::checkpoint() {
cooperate("sls");
}
bool sls_engine::full_eval(goal_ref const & g, model & mdl) {
bool sls_engine::full_eval(model & mdl) {
bool res = true;
unsigned sz = g->size();
unsigned sz = m_assertions.size();
for (unsigned i = 0; i < sz && res; i++) {
checkpoint();
expr_ref o(m_manager);
if (!mdl.eval(g->form(i), o, true))
if (!mdl.eval(m_assertions[i], o, true))
exit(ERR_INTERNAL_FATAL);
res = m_manager.is_true(o.get());
@ -93,7 +93,7 @@ bool sls_engine::full_eval(goal_ref const & g, model & mdl) {
return res;
}
double sls_engine::top_score(goal_ref const & g) {
double sls_engine::top_score() {
#if 0
double min = m_tracker.get_score(g->form(0));
unsigned sz = g->size();
@ -108,15 +108,15 @@ double sls_engine::top_score(goal_ref const & g) {
return min;
#else
double top_sum = 0.0;
unsigned sz = g->size();
unsigned sz = m_assertions.size();
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
expr * e = m_assertions[i];
top_sum += m_tracker.get_score(e);
}
TRACE("sls_top", tout << "Score distribution:";
for (unsigned i = 0; i < sz; i++)
tout << " " << m_tracker.get_score(g->form(i));
tout << " " << m_tracker.get_score(m_assertions[i]);
tout << " AVG: " << top_sum / (double)sz << std::endl;);
#if _CACHE_TOP_SCORE_
@ -127,40 +127,40 @@ double sls_engine::top_score(goal_ref const & g) {
#endif
}
double sls_engine::rescore(goal_ref const & g) {
double sls_engine::rescore() {
m_evaluator.update_all();
m_stats.m_full_evals++;
return top_score(g);
return top_score();
}
double sls_engine::serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value) {
double sls_engine::serious_score(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());
return (m_tracker.get_top_sum() / m_assertions.size());
#else
return top_score(g);
return top_score();
#endif
}
double sls_engine::incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value) {
double sls_engine::incremental_score(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());
return (m_tracker.get_top_sum() / m_assertions.size());
#else
return top_score(g);
return top_score();
#endif
}
double sls_engine::incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value) {
double sls_engine::incremental_score_prune(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() / g->size());
return (m_tracker.get_top_sum() / m_assertions.size());
#else
return top_score(g);
return top_score();
#endif
else
return 0.0;
@ -170,8 +170,13 @@ double sls_engine::incremental_score_prune(goal_ref const & g, func_decl * fd, c
}
// checks whether the score outcome of a given move is better than the previous score
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) {
bool sls_engine::what_if(
func_decl * fd,
const unsigned & fd_inx,
const mpz & temp,
double & best_score,
unsigned & best_const,
mpz & best_value) {
#ifdef Z3DEBUG
mpz old_value;
@ -179,9 +184,9 @@ bool sls_engine::what_if(goal_ref const & g, func_decl * fd, const unsigned & fd
#endif
#if _EARLY_PRUNE_
double r = incremental_score_prune(g, fd, temp);
double r = incremental_score_prune(fd, temp);
#else
double r = incremental_score(g, fd, temp);
double r = incremental_score(fd, temp);
#endif
#ifdef Z3DEBUG
TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) <<
@ -202,8 +207,15 @@ bool sls_engine::what_if(goal_ref const & g, func_decl * fd, const unsigned & fd
}
// 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) {
@ -344,13 +356,19 @@ void sls_engine::mk_random_move(ptr_vector<func_decl> & unsat_constants)
m_mpz_manager.del(new_value);
}
void sls_engine::mk_random_move(goal_ref const & g) {
mk_random_move(m_tracker.get_unsat_constants(g, m_stats.m_moves));
void sls_engine::mk_random_move() {
mk_random_move(m_tracker.get_unsat_constants(m_assertions, 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(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) {
double sls_engine::find_best_move_vns(
ptr_vector<func_decl> & 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;
@ -366,31 +384,31 @@ double sls_engine::find_best_move_vns(goal_ref const & g, ptr_vector<func_decl>
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))
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_INC;
}
else {
// for even values, try -1
mk_dec(bv_sz, old_value, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_DEC;
}
// try inverting
mk_inv(bv_sz, old_value, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_INV;
// try to flip lsb
mk_flip(srt, old_value, 0, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value)) {
if (what_if(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);
double check = incremental_score(fd, old_value);
SASSERT(check == score);
}
@ -412,13 +430,13 @@ double sls_engine::find_best_move_vns(goal_ref const & g, ptr_vector<func_decl>
{
mk_flip(srt, old_value, j, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value)) {
if (what_if(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);
double check = incremental_score(fd, old_value);
SASSERT(check == score);
}
m_mpz_manager.del(old_value);
@ -427,8 +445,14 @@ double sls_engine::find_best_move_vns(goal_ref const & g, ptr_vector<func_decl>
}
// finds the move that increased score the most. returns best_const = -1, if no increasing move exists.
double sls_engine::find_best_move(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) {
double sls_engine::find_best_move(
ptr_vector<func_decl> & 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;
@ -451,7 +475,7 @@ double sls_engine::find_best_move(goal_ref const & g, ptr_vector<func_decl> & to
// 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)) {
if (what_if(fd, i, temp, new_score, best_const, best_value)) {
new_bit = j;
move = MV_FLIP;
}
@ -462,19 +486,19 @@ double sls_engine::find_best_move(goal_ref const & g, ptr_vector<func_decl> & to
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))
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_INC;
}
else {
// for even values, try -1
mk_dec(bv_sz, old_value, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
if (what_if(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))
if (what_if(fd, i, temp, new_score, best_const, best_value))
move = MV_INV;
#if _USE_UNARY_MINUS_
@ -504,7 +528,7 @@ double sls_engine::find_best_move(goal_ref const & g, ptr_vector<func_decl> & to
}
// reset to what it was before
double check = incremental_score(g, fd, old_value);
double check = incremental_score(fd, old_value);
// Andreas: does not hold anymore now that we use top level score caching
//SASSERT(check == score);
}
@ -572,15 +596,15 @@ double sls_engine::find_best_move_local(expr * e, ptr_vector<func_decl> & to_eva
}
// first try of intensification ... does not seem to be efficient
bool sls_engine::handle_plateau(goal_ref const & g)
bool sls_engine::handle_plateau()
{
unsigned sz = g->size();
unsigned sz = m_assertions.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);
expr * e = m_tracker.get_unsat_assertion(sz, pos);
if (!e)
return 0;
@ -634,10 +658,15 @@ bool sls_engine::handle_plateau(goal_ref const & g)
}
// what_if version needed in the context of 2nd intensification try, combining local and global score
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);
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);
double local_score = m_tracker.get_score(e);
double new_score = i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_;
@ -651,7 +680,7 @@ bool sls_engine::what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz
}
// find_best_move version needed in the context of 2nd intensification try
double sls_engine::find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i)
double sls_engine::find_best_move_local(expr * e, func_decl * fd, mpz & best_value, unsigned i)
{
mpz old_value, temp;
double best_score = 0;
@ -662,7 +691,7 @@ double sls_engine::find_best_move_local(goal_ref const & g, expr * e, func_decl
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);
what_if(e, fd, temp, best_score, best_value, i);
}
m_mpz_manager.del(old_value);
@ -672,15 +701,15 @@ double sls_engine::find_best_move_local(goal_ref const & g, expr * e, func_decl
}
// second try to use intensification ... also not very effective
bool sls_engine::handle_plateau(goal_ref const & g, double old_score)
bool sls_engine::handle_plateau(double old_score)
{
unsigned sz = g->size();
unsigned sz = m_assertions.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);
expr * e = m_tracker.get_unsat_assertion(m_assertions, sz, new_const);
if (!e)
return 0;
@ -697,12 +726,12 @@ bool sls_engine::handle_plateau(goal_ref const & g, double old_score)
for (unsigned i = 1; i <= _INTENSIFICATION_TRIES_; i++)
{
new_score = find_best_move_local(g, q, fd, new_value, i);
new_score = find_best_move_local(q, fd, new_value, i);
m_stats.m_moves++;
m_stats.m_flips++;
global_score = incremental_score(g, fd, new_value);
global_score = incremental_score(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_);
@ -715,7 +744,7 @@ bool sls_engine::handle_plateau(goal_ref const & g, double old_score)
}
// main search loop
lbool sls_engine::search(goal_ref const & g) {
lbool sls_engine::search() {
lbool res = l_undef;
double score = 0.0, old_score = 0.0;
unsigned new_const = (unsigned)-1, new_bit = 0;
@ -723,8 +752,8 @@ lbool sls_engine::search(goal_ref const & g) {
move_type move;
unsigned plateau_cnt = 0;
score = rescore(g);
unsigned sz = g->size();
score = rescore();
unsigned sz = m_assertions.size();
#if _PERC_STICKY_
expr * e = m_tracker.get_unsat_assertion(g, m_stats.m_moves);
#endif
@ -750,7 +779,7 @@ lbool sls_engine::search(goal_ref const & g) {
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(g, m_stats.m_moves);
expr * e = m_tracker.get_unsat_assertion(m_assertions, m_stats.m_moves);
#endif
if (!e)
{
@ -793,7 +822,7 @@ lbool sls_engine::search(goal_ref const & g) {
#if _VNS_
score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move);
#else
score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move);
score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move);
#endif
if (new_const == static_cast<unsigned>(-1)) {
@ -811,14 +840,14 @@ lbool sls_engine::search(goal_ref const & g) {
else
#endif
#if _REPICK_
m_evaluator.randomize_local(g, m_stats.m_moves);
m_evaluator.randomize_local(m_assertions, m_stats.m_moves);
#else
m_evaluator.randomize_local(to_evaluate);
#endif
#endif
#if _CACHE_TOP_SCORE_
score = m_tracker.get_top_sum() / g->size();
score = m_tracker.get_top_sum() / m_assertions.size();
#else
score = top_score(g);
#endif
@ -828,7 +857,7 @@ lbool sls_engine::search(goal_ref const & g) {
#if _REAL_RS_ || _REAL_PBFS_
score = serious_score(g, fd, new_value);
#else
score = incremental_score(g, fd, new_value);
score = incremental_score(fd, new_value);
#endif
}
}
@ -840,18 +869,18 @@ bailout:
}
// main search loop
lbool sls_engine::search_old(goal_ref const & g) {
lbool sls_engine::search_old() {
lbool res = l_undef;
double score = 0.0, old_score = 0.0;
unsigned new_const = (unsigned)-1, new_bit = 0;
mpz new_value;
move_type move;
score = rescore(g);
score = rescore();
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));
for (unsigned i = 0; i < m_assertions.size(); i++)
tout << " " << std::setprecision(3) << m_tracker.get_score(m_assertions[i]);
tout << " TOP: " << score << std::endl;);
unsigned plateau_cnt = 0;
@ -897,7 +926,7 @@ lbool sls_engine::search_old(goal_ref const & g) {
old_score = score;
new_const = (unsigned)-1;
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(g, m_stats.m_moves);
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(m_assertions, m_stats.m_moves);
if (!to_evaluate.size())
{
res = l_true;
@ -908,22 +937,22 @@ lbool sls_engine::search_old(goal_ref const & g) {
tout << to_evaluate[i]->get_name() << std::endl;);
#if _VNS_
score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move);
score = find_best_move_vns(to_evaluate, score, new_const, new_value, new_bit, move);
#else
score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move);
score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move);
#endif
if (new_const == static_cast<unsigned>(-1)) {
TRACE("sls", tout << "Local maximum reached; unsatisfied constraints: " << std::endl;
for (unsigned i = 0; i < g->size(); i++) {
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
tout << mk_ismt2_pp(g->form(i), m_manager) << std::endl;
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;
});
TRACE("sls_max", m_tracker.show_model(tout);
tout << "Scores: " << std::endl;
for (unsigned i = 0; i < g->size(); i++)
tout << mk_ismt2_pp(g->form(i), m_manager) << " ---> " <<
m_tracker.get_score(g->form(i)) << std::endl;);
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;);
// Andreas: If new_const == -1, shouldn't score = old_score anyway?
score = old_score;
}
@ -962,14 +991,14 @@ lbool sls_engine::search_old(goal_ref const & g) {
}
#if _REAL_RS_ || _REAL_PBFS_
score = serious_score(g, fd, new_value);
score = serious_score(fd, new_value);
#else
score = incremental_score(g, fd, new_value);
score = incremental_score(fd, new_value);
#endif
TRACE("sls", tout << "Score distribution:";
for (unsigned i = 0; i < g->size(); i++)
tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i));
for (unsigned i = 0; i < m_assertions.size(); i++)
tout << " " << std::setprecision(3) << m_tracker.get_score(m_assertions[i]);
tout << " TOP: " << score << std::endl;);
}
@ -978,8 +1007,8 @@ lbool sls_engine::search_old(goal_ref const & g) {
// 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 < g->size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
for (unsigned i = 0; i < m_assertions.size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(m_assertions[i])))
all_true = false;
if (all_true) {
res = l_true; // sat
@ -1010,17 +1039,17 @@ lbool sls_engine::search_old(goal_ref const & g) {
TRACE("sls", tout << "In a plateau (" << plateau_cnt << "/" << m_plateau_limit << "); randomizing locally." << std::endl;);
#if _INTENSIFICATION_
handle_plateau(g, score);
//handle_plateau(g);
//handle_plateau();
#else
m_evaluator.randomize_local(g, m_stats.m_moves);
m_evaluator.randomize_local(m_assertions, m_stats.m_moves);
#endif
//mk_random_move(g);
score = top_score(g);
//mk_random_move();
score = top_score();
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))))
for (unsigned i = 0; i < m_assertions.size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(m_assertions[i])))
all_true = false;
if (all_true) {
res = l_true; // sat
@ -1046,6 +1075,10 @@ 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;
@ -1089,7 +1122,7 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
#if _WEIGHT_TOGGLE_
m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_);
#endif
m_tracker.initialize(g);
m_tracker.initialize(m_assertions);
lbool res = l_undef;
m_restart_limit = _RESTART_LIMIT_;
@ -1098,14 +1131,14 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
checkpoint();
report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts);
res = search(g);
res = search();
if (res == l_undef)
{
#if _RESTART_INIT_
m_tracker.randomize(g);
m_tracker.randomize();
#else
m_tracker.reset(g);
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);

58
src/tactic/sls/sls_engine.h
View file

@ -71,6 +71,7 @@ protected:
bv_util m_bv_util;
sls_tracker m_tracker;
sls_evaluator m_evaluator;
ptr_vector<expr> m_assertions;
unsigned m_restart_limit;
unsigned m_max_restarts;
@ -92,11 +93,12 @@ 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(goal_ref const & g, model & mdl);
bool full_eval(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);
@ -104,54 +106,44 @@ 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);
double find_best_move(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double find_best_move_local(expr * e, ptr_vector<func_decl> & 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 search(void);
void operator()(goal_ref const & g, model_converter_ref & mc);
protected:
void checkpoint();
lbool search_old(goal_ref const & g);
lbool search_old(void);
double get_restart_armin(unsigned cnt_restarts);
bool what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
bool what_if(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_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(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);
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);
#if _EARLY_PRUNE_
double incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value);
double incremental_score_prune(func_decl * fd, const mpz & new_value);
#endif
double find_best_move_vns(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double find_best_move(ptr_vector<func_decl> & 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<func_decl> & to_evaluate,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double find_best_move_vns(ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
void mk_random_move(ptr_vector<func_decl> & unsat_constants);
void mk_random_move(goal_ref const & g);
void mk_random_move();
bool handle_plateau(goal_ref const & g);
bool handle_plateau(goal_ref const & g, double old_score);
bool handle_plateau(void);
bool handle_plateau(double old_score);
inline unsigned check_restart(unsigned curr_value);
};

4
src/tactic/sls/sls_evaluator.h
View file

@ -922,8 +922,8 @@ public:
randomize_local(m_tracker.get_constants(e));
}
void randomize_local(goal_ref const & g, unsigned int flip) {
randomize_local(m_tracker.get_unsat_constants(g, flip));
void randomize_local(ptr_vector<expr> const & as, unsigned int flip) {
randomize_local(m_tracker.get_unsat_constants(as, flip));
}
};

84
src/tactic/sls/sls_tracker.h
View file

@ -20,7 +20,7 @@ Notes:
#ifndef _SLS_TRACKER_H_
#define _SLS_TRACKER_H_
#include"goal.h"
#include"bv_decl_plugin.h"
#include"model.h"
#include"sls_compilation_settings.h"
@ -365,12 +365,12 @@ public:
}
};
void calculate_expr_distances(goal_ref const & g) {
void calculate_expr_distances(ptr_vector<expr> const & as) {
// precondition: m_scores is set up.
unsigned sz = g->size();
unsigned sz = as.size();
ptr_vector<app> stack;
for (unsigned i = 0; i < sz; i++)
stack.push_back(to_app(g->form(i)));
stack.push_back(to_app(as[i]));
while (!stack.empty()) {
app * cur = stack.back();
stack.pop_back();
@ -418,12 +418,12 @@ public:
quick_for_each_expr(ffd_proc, visited, e);
}
void initialize(goal_ref const & g) {
void initialize(ptr_vector<expr> const & as) {
init_proc proc(m_manager, *this);
expr_mark visited;
unsigned sz = g->size();
unsigned sz = as.size();
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
expr * e = as[i];
if (!m_top_expr.contains(e))
m_top_expr.insert(e);
else
@ -438,7 +438,7 @@ public:
visited.reset();
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
expr * e = as[i];
// Andreas: Maybe not fully correct.
#if _FOCUS_ == 2 || _INTENSIFICATION_
initialize_recursive(e);
@ -450,7 +450,7 @@ public:
quick_for_each_expr(ffd_proc, visited, e);
}
calculate_expr_distances(g);
calculate_expr_distances(as);
TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); );
@ -465,11 +465,11 @@ public:
#if _EARLY_PRUNE_
for (unsigned i = 0; i < sz; i++)
setup_occs(g->form(i));
setup_occs(as[i]);
#endif
#if _UCT_
m_touched = _UCT_INIT_ ? g->size() : 1;
m_touched = _UCT_INIT_ ? as.size() : 1;
#endif
}
@ -606,7 +606,7 @@ public:
NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now.
}
void randomize(goal_ref const & g) {
void randomize(ptr_vector<expr> const & as) {
TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
@ -620,13 +620,13 @@ public:
TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); );
#if _UCT_RESET_
m_touched = _UCT_INIT_ ? g->size() : 1;
for (unsigned i = 0; i < g->size(); i++)
m_scores.find(g->form(i)).touched = 1;
m_touched = _UCT_INIT_ ? as.size() : 1;
for (unsigned i = 0; i < as.size(); i++)
m_scores.find(as[i]).touched = 1;
#endif
}
void reset(goal_ref const & g) {
void reset(ptr_vector<expr> const & as) {
TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
@ -636,9 +636,9 @@ public:
}
#if _UCT_RESET_
m_touched = _UCT_INIT_ ? g->size() : 1;
for (unsigned i = 0; i < g->size(); i++)
m_scores.find(g->form(i)).touched = 1;
m_touched = _UCT_INIT_ ? as.size() : 1;
for (unsigned i = 0; i < as.size(); i++)
m_scores.find(as[i]).touched = 1;
#endif
}
@ -1029,13 +1029,13 @@ public:
return m_temp_constants;
}
ptr_vector<func_decl> & get_unsat_constants_gsat(goal_ref const & g, unsigned sz) {
ptr_vector<func_decl> & get_unsat_constants_gsat(ptr_vector<expr> const & as, unsigned sz) {
if (sz == 1)
return get_constants();
m_temp_constants.reset();
for (unsigned i = 0; i < sz; i++) {
expr * q = g->form(i);
expr * q = as[i];
if (m_mpz_manager.eq(get_value(q), m_one))
continue;
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(q);
@ -1049,22 +1049,22 @@ public:
return m_temp_constants;
}
expr * get_unsat_assertion(goal_ref const & g, unsigned sz, unsigned int pos) {
expr * get_unsat_assertion(ptr_vector<expr> const & as, unsigned sz, unsigned int pos) {
for (unsigned i = pos; i < sz; i++) {
expr * q = g->form(i);
expr * q = as[i];
if (m_mpz_manager.neq(get_value(q), m_one))
return q;
}
for (unsigned i = 0; i < pos; i++) {
expr * q = g->form(i);
expr * q = as[i];
if (m_mpz_manager.neq(get_value(q), m_one))
return q;
}
return 0;
}
ptr_vector<func_decl> & get_unsat_constants_walksat(goal_ref const & g, unsigned sz, unsigned int pos) {
expr * q = get_unsat_assertion(g, sz, pos);
ptr_vector<func_decl> & get_unsat_constants_walksat(ptr_vector<expr> const & as, unsigned sz, unsigned int pos) {
expr * q = get_unsat_assertion(as, 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;
@ -1141,19 +1141,19 @@ public:
return m_temp_constants;
}
ptr_vector<func_decl> & get_unsat_constants_crsat(goal_ref const & g, unsigned sz, unsigned int pos) {
expr * q = get_unsat_assertion(g, sz, pos);
ptr_vector<func_decl> & get_unsat_constants_crsat(ptr_vector<expr> const & as, unsigned sz, unsigned int pos) {
expr * q = get_unsat_assertion(as, sz, pos);
if (!q)
return m_temp_constants;
return go_deeper(q);
}
ptr_vector<func_decl> & get_unsat_constants(goal_ref const & g, unsigned int flip) {
unsigned sz = g->size();
ptr_vector<func_decl> & get_unsat_constants(ptr_vector<expr> const & as, unsigned int flip) {
unsigned sz = as.size();
if (sz == 1) {
if (m_mpz_manager.eq(get_value(g->form(0)), m_one))
if (m_mpz_manager.eq(get_value(as[0]), m_one))
return m_temp_constants;
else
return get_constants();
@ -1201,7 +1201,7 @@ public:
#else
double max = -1.0;
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
expr * e = as[i];
// for (unsigned i = 0; i < m_where_false.size(); i++) {
// expr * e = m_list_false[i];
vscore = m_scores.find(e);
@ -1219,12 +1219,12 @@ public:
return m_temp_constants;
#if _UCT_ == 1 || _UCT_ == 3
m_scores.find(g->form(pos)).touched++;
m_scores.find(as[pos]).touched++;
m_touched++;
#elif _UCT_ == 2
m_scores.find(g->form(pos)).touched = flip;
m_scores.find(as[pos]).touched = flip;
#endif
expr * e = g->form(pos);
expr * e = as[pos];
// expr * e = m_list_false[pos];
#elif _BFS_ == 3
@ -1303,11 +1303,11 @@ public:
}
expr * get_unsat_assertion(goal_ref const & g, unsigned int flip) {
unsigned sz = g->size();
expr * get_unsat_assertion(ptr_vector<expr> const & as, unsigned int flip) {
unsigned sz = as.size();
if (sz == 1)
return g->form(0);
return as[0];
m_temp_constants.reset();
#if _FOCUS_ == 1
@ -1351,7 +1351,7 @@ public:
#else
double max = -1.0;
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
expr * e = as[i];
// for (unsigned i = 0; i < m_where_false.size(); i++) {
// expr * e = m_list_false[i];
vscore = m_scores.find(e);
@ -1369,13 +1369,13 @@ public:
return 0;
#if _UCT_ == 1 || _UCT_ == 3
m_scores.find(g->form(pos)).touched++;
m_scores.find(as[pos]).touched++;
m_touched++;
#elif _UCT_ == 2
m_scores.find(g->form(pos)).touched = flip;
#endif
// return m_list_false[pos];
return g->form(pos);
return as[pos];
#elif _BFS_ == 3
unsigned int pos = -1;
@ -1429,7 +1429,7 @@ public:
unsigned int pos = get_random_uint(16) % sz;
return get_unsat_assertion(g, sz, pos);
#endif
return g->form(pos);
return as[pos];
#elif _FOCUS_ == 2
#if _BFS_
unsigned int pos = flip % sz;