mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-16 07:45:27 +00:00
Code Activity

removed tabs

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-03-19 09:40:01 +00:00
parent e310ab5cd7
commit e33e637ad8
3 changed files with 756 additions and 756 deletions
Download patch file Download diff file Expand all files Collapse all files

572
src/tactic/sls/sls_tactic.cpp
View file

@ -125,10 +125,10 @@ Notes:
#if ((_UCT_ > 0) + _UNIFORM_RANDOM_ + _REAL_RS_ + _REAL_PBFS_ > 1) || _BFS_ && (_UCT_ ||_UNIFORM_RANDOM_ ||_REAL_RS_ ||_REAL_PBFS_)
InvalidConfiguration;
InvalidConfiguration;
#endif
#if (_PROBABILISTIC_UCT_ && !_UCT_)
InvalidConfiguration;
InvalidConfiguration;
#endif
@ -150,10 +150,10 @@ class sls_tactic : public tactic {
m_full_evals(0),
m_incr_evals(0),
m_moves(0),
m_umins(0),
m_mul2s(0),
m_mul3s(0),
m_div2s(0),
m_umins(0),
m_mul2s(0),
m_mul3s(0),
m_div2s(0),
m_flips(0),
m_incs(0),
m_decs(0),
@ -183,8 +183,8 @@ class sls_tactic : public tactic {
unsigned m_max_restarts;
unsigned m_plateau_limit;
ptr_vector<mpz> m_old_values;
ptr_vector<mpz> m_old_values;
typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV, MV_UMIN, MV_MUL2, MV_MUL3, MV_DIV2 } move_type;
imp(ast_manager & m, params_ref const & p, stats & s) :
@ -267,18 +267,18 @@ class sls_tactic : public tactic {
#else
double top_sum = 0.0;
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
top_sum += m_tracker.get_score(e);
}
TRACE("sls_top", tout << "Score distribution:";
TRACE("sls_top", tout << "Score distribution:";
for (unsigned i = 0; i < sz; i++)
tout << " " << m_tracker.get_score(g->form(i));
tout << " AVG: " << top_sum / (double) sz << std::endl; );
#if _CACHE_TOP_SCORE_
m_tracker.set_top_sum(top_sum);
m_tracker.set_top_sum(top_sum);
#endif
return top_sum / (double) sz;
@ -292,20 +292,20 @@ class sls_tactic : public tactic {
}
double serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value) {
m_evaluator.serious_update(fd, 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() / g->size());
#else
return top_score(g);
#endif
}
double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value) {
m_evaluator.update(fd, new_value);
m_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() / g->size());
#else
return top_score(g);
#endif
@ -314,18 +314,18 @@ class sls_tactic : public tactic {
#if _EARLY_PRUNE_
double incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value) {
m_stats.m_incr_evals++;
if (m_evaluator.update_prune(fd, new_value))
if (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() / g->size());
#else
return top_score(g);
return top_score(g);
#endif
else
return 0.0;
else
return 0.0;
}
#endif
// checks whether the score outcome of a given move is better than the previous score
// checks whether the score outcome of a given move is better than the previous score
bool what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value) {
@ -357,11 +357,11 @@ class sls_tactic : public tactic {
return false;
}
// same as what_if, but only applied to the score of a specific atom, not the total score
// same as what_if, but only applied to the score of a specific atom, not the total score
bool what_if_local(expr * e, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value) {
m_evaluator.update(fd, temp);
double r = m_tracker.get_score(e);
double r = m_tracker.get_score(e);
if (r >= best_score) {
best_score = r;
best_const = fd_inx;
@ -378,29 +378,29 @@ class sls_tactic : public tactic {
m_mpz_manager.set(mask, m_powers(bv_sz));
m_mpz_manager.bitwise_not(bv_sz, mask, mask2);
m_mpz_manager.bitwise_and(temp, mask2, result);
m_mpz_manager.del(temp);
m_mpz_manager.del(mask);
m_mpz_manager.del(mask2);
m_mpz_manager.del(temp);
m_mpz_manager.del(mask);
m_mpz_manager.del(mask2);
}
}
// Andreas: do we really need all those temporary mpzs?
void mk_mul2(unsigned bv_sz, const mpz & old_value, mpz & result) {
// Andreas: do we really need all those temporary mpzs?
void mk_mul2(unsigned bv_sz, const mpz & old_value, mpz & result) {
mpz temp, mask, mask2;
m_mpz_manager.mul(old_value, m_two, temp);
m_mpz_manager.set(mask, m_powers(bv_sz));
m_mpz_manager.bitwise_not(bv_sz, mask, mask2);
m_mpz_manager.bitwise_and(temp, mask2, result);
m_mpz_manager.del(temp);
m_mpz_manager.del(mask);
m_mpz_manager.del(mask2);
m_mpz_manager.del(temp);
m_mpz_manager.del(mask);
m_mpz_manager.del(mask2);
}
void mk_div2(unsigned bv_sz, const mpz & old_value, mpz & result) {
m_mpz_manager.div(old_value, m_two, result);
}
void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented) {
void mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented) {
unsigned shift;
m_mpz_manager.add(old_value, m_one, incremented);
if (m_mpz_manager.is_power_of_two(incremented, shift) && shift == bv_sz)
@ -437,73 +437,73 @@ class sls_tactic : public tactic {
void mk_random_move(goal_ref const & g) {
unsigned rnd_mv = 0;
if (m_stats.m_moves > 10000)
rnd_mv = 0;
if (m_stats.m_moves > 10000)
rnd_mv = 0;
ptr_vector<func_decl> & unsat_constants = m_tracker.get_unsat_constants(g, m_stats.m_moves);
ptr_vector<func_decl> & unsat_constants = m_tracker.get_unsat_constants(g, m_stats.m_moves);
unsigned ucc = unsat_constants.size();
unsigned rc = (m_tracker.get_random_uint((ucc < 16) ? 4 : (ucc < 256) ? 8 : (ucc < 4096) ? 12 : (ucc < 65536) ? 16 : 32)) % ucc;
func_decl * fd = unsat_constants[rc];
mpz new_value;
mpz new_value;
sort * srt = fd->get_range();
sort * srt = fd->get_range();
if (m_manager.is_bool(srt))
m_mpz_manager.set(new_value, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero);
else
{
m_mpz_manager.set(new_value, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero);
else
{
#if _USE_ADDSUB_
if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv=2;
if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++;
move_type mt = (move_type) rnd_mv;
if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv=2;
if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++;
move_type mt = (move_type) rnd_mv;
// inversion doesn't make sense, let's do a flip instead.
if (mt == MV_INV) mt = MV_FLIP;
// inversion doesn't make sense, let's do a flip instead.
if (mt == MV_INV) mt = MV_FLIP;
#else
mt = MV_FLIP;
mt = MV_FLIP;
#endif
unsigned bit = 0;
unsigned bit = 0;
switch (mt)
{
case MV_FLIP: {
unsigned bv_sz = m_bv_util.get_bv_size(srt);
bit = (m_tracker.get_random_uint((bv_sz < 16) ? 4 : (bv_sz < 256) ? 8 : (bv_sz < 4096) ? 12 : (bv_sz < 65536) ? 16 : 32)) % bv_sz;
mk_flip(fd->get_range(), m_tracker.get_value(fd), bit, new_value);
break;
}
case MV_INC:
mk_inc(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
break;
case MV_DEC:
mk_dec(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
break;
case MV_INV:
mk_inv(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
break;
default:
NOT_IMPLEMENTED_YET();
}
switch (mt)
{
case MV_FLIP: {
unsigned bv_sz = m_bv_util.get_bv_size(srt);
bit = (m_tracker.get_random_uint((bv_sz < 16) ? 4 : (bv_sz < 256) ? 8 : (bv_sz < 4096) ? 12 : (bv_sz < 65536) ? 16 : 32)) % bv_sz;
mk_flip(fd->get_range(), m_tracker.get_value(fd), bit, new_value);
break;
}
case MV_INC:
mk_inc(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
break;
case MV_DEC:
mk_dec(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
break;
case MV_INV:
mk_inv(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
break;
default:
NOT_IMPLEMENTED_YET();
}
TRACE("sls", tout << "Randomization candidates: ";
for (unsigned i = 0; i < unsat_constants.size(); i++)
tout << unsat_constants[i]->get_name() << ", ";
tout << std::endl;
tout << "Random move: ";
switch (mt) {
case MV_FLIP: tout << "Flip #" << bit << " in " << fd->get_name() << std::endl; break;
case MV_INC: tout << "+1 for " << fd->get_name() << std::endl; break;
case MV_DEC: tout << "-1 for " << fd->get_name() << std::endl; break;
case MV_INV: tout << "NEG for " << fd->get_name() << std::endl; break;
}
tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout); );
}
TRACE("sls", tout << "Randomization candidates: ";
for (unsigned i = 0; i < unsat_constants.size(); i++)
tout << unsat_constants[i]->get_name() << ", ";
tout << std::endl;
tout << "Random move: ";
switch (mt) {
case MV_FLIP: tout << "Flip #" << bit << " in " << fd->get_name() << std::endl; break;
case MV_INC: tout << "+1 for " << fd->get_name() << std::endl; break;
case MV_DEC: tout << "-1 for " << fd->get_name() << std::endl; break;
case MV_INV: tout << "NEG for " << fd->get_name() << std::endl; break;
}
tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout); );
}
m_evaluator.update(fd, new_value);
m_mpz_manager.del(new_value);
}
m_evaluator.update(fd, new_value);
m_mpz_manager.del(new_value);
}
// will use VNS to ignore some possible moves and increase the flips per second
// will use VNS to ignore some possible moves and increase the flips per second
double find_best_move_vns(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) {
mpz old_value, temp;
@ -514,7 +514,7 @@ class sls_tactic : public tactic {
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;
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) {
@ -536,12 +536,12 @@ class sls_tactic : public tactic {
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
move = MV_INV;
// try to flip lsb
mk_flip(srt, old_value, 0, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value)) {
new_bit = 0;
move = MV_FLIP;
}
// 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
@ -549,12 +549,12 @@ class sls_tactic : public tactic {
SASSERT(check == score);
}
// we can either check the condition once in the beginning or check it repeatedly after every bit
// we can either check the condition once in the beginning or check it repeatedly after every bit
#if _VNS_ == 1
for (unsigned j = 1; j < max_bv_sz && new_score <= score; j++)
for (unsigned j = 1; j < max_bv_sz && new_score <= score; j++)
#else
if (new_score <= score)
for (unsigned j = 1; j < max_bv_sz && new_score < 1.0; j++)
if (new_score <= score)
for (unsigned j = 1; j < max_bv_sz && new_score < 1.0; j++)
#endif
for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0 ; i++) {
func_decl * fd = to_evaluate[i];
@ -563,30 +563,30 @@ class sls_tactic : public tactic {
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 (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;
}
}
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(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.
// finds the move that increased score the most. returns best_const = -1, if no increasing move exists.
double find_best_move(goal_ref const & g, ptr_vector<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;
mpz temp2;
#endif
unsigned bv_sz;
double new_score = score;
@ -599,11 +599,11 @@ class sls_tactic : public tactic {
// first try to flip every bit
#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)) {
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++) {
#endif
// What would happen if we flipped bit #i ?
// 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)) {
@ -614,7 +614,7 @@ class sls_tactic : public tactic {
if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) {
#if _USE_ADDSUB_
if (!m_mpz_manager.is_even(old_value)) {
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))
@ -660,7 +660,7 @@ class sls_tactic : public tactic {
// reset to what it was before
double check = incremental_score(g, fd, old_value);
// Andreas: does not hold anymore now that we use top level score caching
// Andreas: does not hold anymore now that we use top level score caching
//SASSERT(check == score);
}
@ -669,17 +669,17 @@ class sls_tactic : public tactic {
#if _USE_MUL3_
m_mpz_manager.del(temp2);
#endif
return new_score;
return new_score;
}
// same as find_best_move but only considers the score of the current expression instead of the overall score
double find_best_move_local(expr * e, ptr_vector<func_decl> & to_evaluate,
// same as find_best_move but only considers the score of the current expression instead of the overall score
double find_best_move_local(expr * e, ptr_vector<func_decl> & to_evaluate,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move) {
mpz old_value, temp;
unsigned bv_sz;
double new_score = m_tracker.get_score(e);
// Andreas: tie breaking not implemented yet
// double tie_score = top_score(g);
double new_score = m_tracker.get_score(e);
// Andreas: tie breaking not implemented yet
// double tie_score = top_score(g);
for (unsigned i = 0; i < to_evaluate.size(); i++) {
func_decl * fd = to_evaluate[i];
sort * srt = fd->get_range();
@ -718,7 +718,7 @@ class sls_tactic : public tactic {
}
// reset to what it was before
m_evaluator.update(fd, old_value);
m_evaluator.update(fd, old_value);
}
m_mpz_manager.del(old_value);
@ -726,37 +726,37 @@ class sls_tactic : public tactic {
return new_score;
}
// first try of intensification ... does not seem to be efficient
bool handle_plateau(goal_ref const & g)
{
unsigned sz = g->size();
// first try of intensification ... does not seem to be efficient
bool handle_plateau(goal_ref const & g)
{
unsigned sz = g->size();
#if _BFS_
unsigned pos = m_stats.m_moves % sz;
unsigned pos = m_stats.m_moves % sz;
#else
unsigned pos = m_tracker.get_random_uint(16) % sz;
unsigned pos = m_tracker.get_random_uint(16) % sz;
#endif
expr * e = m_tracker.get_unsat_assertion(g, sz, pos);
if (!e)
return 0;
expr * e = m_tracker.get_unsat_assertion(g, sz, pos);
if (!e)
return 0;
expr * q = m_tracker.get_unsat_expression(e);
ptr_vector<func_decl> & to_evaluate = m_tracker.get_constants(q);
for (unsigned i = 0; i < to_evaluate.size(); i++)
{
m_tracker.get_value(to_evaluate[i]);
m_old_values.push_back( & m_tracker.get_value(to_evaluate[i]));
}
unsigned new_const = (unsigned)-1, new_bit = 0;
expr * q = m_tracker.get_unsat_expression(e);
ptr_vector<func_decl> & to_evaluate = m_tracker.get_constants(q);
for (unsigned i = 0; i < to_evaluate.size(); i++)
{
m_tracker.get_value(to_evaluate[i]);
m_old_values.push_back( & m_tracker.get_value(to_evaluate[i]));
}
unsigned new_const = (unsigned)-1, new_bit = 0;
mpz new_value;
move_type move;
for (unsigned i = 0; i < _INTENSIFICATION_TRIES_; i++)
{
// Andreas: Could be extended to use (best) score but this is computationally more expensive.
for (unsigned i = 0; i < _INTENSIFICATION_TRIES_; i++)
{
// Andreas: Could be extended to use (best) score but this is computationally more expensive.
find_best_move_local(q, to_evaluate, new_const, new_value, new_bit, move);
if (new_const == static_cast<unsigned>(-1)) {
// Andreas: Actually this should never happen.
NOT_IMPLEMENTED_YET();
// Andreas: Actually this should never happen.
NOT_IMPLEMENTED_YET();
} else {
m_stats.m_moves++;
func_decl * fd = to_evaluate[new_const];
@ -767,35 +767,35 @@ class sls_tactic : public tactic {
case MV_DEC: m_stats.m_decs++; break;
case MV_INV: m_stats.m_invs++; break;
case MV_UMIN: m_stats.m_umins++; break;
case MV_MUL2: m_stats.m_mul2s++; break;
case MV_MUL3: m_stats.m_mul3s++; break;
case MV_DIV2: m_stats.m_div2s++; break;
case MV_MUL2: m_stats.m_mul2s++; break;
case MV_MUL3: m_stats.m_mul3s++; break;
case MV_DIV2: m_stats.m_div2s++; break;
}
m_evaluator.update(fd, new_value);
m_evaluator.update(fd, new_value);
}
if (m_mpz_manager.is_one(m_tracker.get_value(q)))
return 1;
}
if (m_mpz_manager.is_one(m_tracker.get_value(q)))
return 1;
}
for (unsigned i = 0; i < to_evaluate.size(); i++)
m_tracker.set_value(to_evaluate[i], * m_old_values[i]);
for (unsigned i = 0; i < to_evaluate.size(); i++)
m_tracker.set_value(to_evaluate[i], * m_old_values[i]);
m_old_values.reset();
m_old_values.reset();
return 0;
}
return 0;
}
// what_if version needed in the context of 2nd intensification try, combining local and global score
// what_if version needed in the context of 2nd intensification try, combining local and global score
bool what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz & temp,
double & best_score, mpz & best_value, unsigned i) {
double global_score = incremental_score(g, fd, temp);
double local_score = m_tracker.get_score(e);
double local_score = m_tracker.get_score(e);
double new_score = i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_;
if (new_score >= best_score) {
if (new_score >= best_score) {
best_score = new_score;
m_mpz_manager.set(best_value, temp);
return true;
@ -804,17 +804,17 @@ class sls_tactic : public tactic {
return false;
}
// find_best_move version needed in the context of 2nd intensification try
// find_best_move version needed in the context of 2nd intensification try
double find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i)
{
mpz old_value, temp;
{
mpz old_value, temp;
double best_score = 0;
sort * srt = fd->get_range();
unsigned bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
m_mpz_manager.set(old_value, m_tracker.get_value(fd));
for (unsigned j = 0; j < bv_sz && best_score < 1.0; j++) {
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);
}
@ -822,54 +822,54 @@ class sls_tactic : public tactic {
m_mpz_manager.del(old_value);
m_mpz_manager.del(temp);
return best_score;
return best_score;
}
// second try to use intensification ... also not very effective
bool handle_plateau(goal_ref const & g, double old_score)
{
unsigned sz = g->size();
// second try to use intensification ... also not very effective
bool handle_plateau(goal_ref const & g, double old_score)
{
unsigned sz = g->size();
#if _BFS_
unsigned new_const = m_stats.m_moves % sz;
unsigned new_const = m_stats.m_moves % sz;
#else
unsigned new_const = m_tracker.get_random_uint(16) % sz;
unsigned new_const = m_tracker.get_random_uint(16) % sz;
#endif
expr * e = m_tracker.get_unsat_assertion(g, sz, new_const);
if (!e)
return 0;
expr * e = m_tracker.get_unsat_assertion(g, sz, new_const);
if (!e)
return 0;
expr * q = m_tracker.get_unsat_expression(e);
ptr_vector<func_decl> & to_evaluate = m_tracker.get_constants(q);
expr * q = m_tracker.get_unsat_expression(e);
ptr_vector<func_decl> & to_evaluate = m_tracker.get_constants(q);
new_const = m_tracker.get_random_uint(16) % to_evaluate.size();
func_decl * fd = to_evaluate[new_const];
new_const = m_tracker.get_random_uint(16) % to_evaluate.size();
func_decl * fd = to_evaluate[new_const];
mpz new_value;
//m_mpz_manager.set(new_value, m_tracker.get_value(fd));
unsigned new_bit = 0;
double global_score = old_score, local_score = m_tracker.get_score(q), new_score = old_score;
for (unsigned i = 1; i <= _INTENSIFICATION_TRIES_; i++)
{
mpz new_value;
//m_mpz_manager.set(new_value, m_tracker.get_value(fd));
unsigned new_bit = 0;
double global_score = old_score, local_score = m_tracker.get_score(q), new_score = old_score;
for (unsigned i = 1; i <= _INTENSIFICATION_TRIES_; i++)
{
new_score = find_best_move_local(g, q, fd, new_value, i);
m_stats.m_moves++;
m_stats.m_flips++;
global_score = incremental_score(g, fd, new_value);
local_score = m_tracker.get_score(q);
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_);
SASSERT(new_score == i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_);
if (m_mpz_manager.is_one(m_tracker.get_value(q)))
return 1;
}
if (m_mpz_manager.is_one(m_tracker.get_value(q)))
return 1;
}
return 0;
}
return 0;
}
// main search loop
lbool search(goal_ref const & g) {
// main search loop
lbool search(goal_ref const & g) {
lbool res = l_undef;
double score = 0.0, old_score = 0.0;
unsigned new_const = (unsigned)-1, new_bit = 0;
@ -885,52 +885,52 @@ class sls_tactic : public tactic {
unsigned plateau_cnt = 0;
// Andreas: Why do we only allow so few plateaus?
// Andreas: Why do we only allow so few plateaus?
#if _RESTARTS_
while (plateau_cnt < m_plateau_limit && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {
while (plateau_cnt < m_plateau_limit && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {
#else
while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && (_RESTARTS_ == 0 || m_stats.m_moves < _RESTARTS_)) {
while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && (_RESTARTS_ == 0 || m_stats.m_moves < _RESTARTS_)) {
#endif
do {
if (m_stats.m_moves == 5590)
if (m_stats.m_moves == 5590)
checkpoint();
#if _WEIGHT_DIST_ == 4
m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_);
m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_);
#endif
#if _TYPE_RSTEP_
if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_)
{
if (m_tracker.get_random_uint(16) % 1000 < _PERM_RSTEP_)
{
#if _TYPE_RSTEP_ == 1
m_evaluator.randomize_local(g, m_stats.m_moves);
m_evaluator.randomize_local(g, m_stats.m_moves);
#elif _TYPE_RSTEP_ == 2
mk_random_move(g);
mk_random_move(g);
#endif
score = top_score(g);
if (score >= 1.0) {
bool all_true = true;
for (unsigned i = 0; i < g->size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
all_true=false;
if (all_true) {
res = l_true; // sat
goto bailout;
} else
TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;);
}
}
if (score >= 1.0) {
bool all_true = true;
for (unsigned i = 0; i < g->size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
all_true=false;
if (all_true) {
res = l_true; // sat
goto bailout;
} else
TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;);
}
}
#endif
old_score = score;
new_const = (unsigned)-1;
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(g, m_stats.m_moves);
if (!to_evaluate.size())
{
res = l_true;
goto bailout;
}
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(g, m_stats.m_moves);
if (!to_evaluate.size())
{
res = l_true;
goto bailout;
}
TRACE("sls_constants", tout << "Evaluating these constants: " << std::endl;
for (unsigned i = 0 ; i < to_evaluate.size(); i++)
tout << to_evaluate[i]->get_name() << std::endl; );
@ -952,11 +952,11 @@ class sls_tactic : public tactic {
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?
// Andreas: If new_const == -1, shouldn't score = old_score anyway?
score = old_score;
}
else {
// Andreas: Why does randomizing not count as a move? (Now it does.)
// Andreas: Why does randomizing not count as a move? (Now it does.)
m_stats.m_moves++;
func_decl * fd = to_evaluate[new_const];
@ -984,15 +984,15 @@ class sls_tactic : public tactic {
case MV_DEC: m_stats.m_decs++; break;
case MV_INV: m_stats.m_invs++; break;
case MV_UMIN: m_stats.m_umins++; break;
case MV_MUL2: m_stats.m_mul2s++; break;
case MV_MUL3: m_stats.m_mul3s++; break;
case MV_DIV2: m_stats.m_div2s++; break;
case MV_MUL2: m_stats.m_mul2s++; break;
case MV_MUL3: m_stats.m_mul3s++; break;
case MV_DIV2: m_stats.m_div2s++; break;
}
#if _REAL_RS_ || _REAL_PBFS_
score = serious_score(g, fd, new_value);
score = serious_score(g, fd, new_value);
#else
score = incremental_score(g, fd, new_value);
score = incremental_score(g, fd, new_value);
#endif
TRACE("sls", tout << "Score distribution:";
@ -1004,7 +1004,7 @@ class sls_tactic : public tactic {
if (score >= 0.99999) {
// if (score >= 1.0) {
// score could theoretically be imprecise.
// Andreas: it seems using top level score caching can make the score unprecise also in the other direction!
// Andreas: it seems using top level score caching can make the score unprecise also in the other direction!
bool all_true = true;
for (unsigned i = 0; i < g->size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
@ -1015,43 +1015,43 @@ class sls_tactic : public tactic {
} else
TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;);
}
/*
if (m_stats.m_moves % 100 == 0)
{
verbose_stream() << "(" << std::fixed << std::setprecision(10) << score << ")" << std::endl;
verbose_stream() << "(" << std::fixed << std::setprecision(2) << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl;
}*/
/*
if (m_stats.m_moves % 100 == 0)
{
verbose_stream() << "(" << std::fixed << std::setprecision(10) << score << ")" << std::endl;
verbose_stream() << "(" << std::fixed << std::setprecision(2) << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl;
}*/
}
while (score > old_score && res == l_undef);
// Andreas: Why do you check for old_score? This should always be equal due to the loop invariant.
// Andreas: Why do you check for old_score? This should always be equal due to the loop invariant.
if (score != old_score) {
report_tactic_progress("This should not happen I guess.", plateau_cnt);
report_tactic_progress("This should not happen I guess.", plateau_cnt);
plateau_cnt = 0;
} else {
m_stats.m_moves++;
} else {
m_stats.m_moves++;
plateau_cnt++;
//report_tactic_progress("Plateau.", plateau_cnt);
// Andreas: Right now, a useless assignment is created in case of a restart. But we don't want to use restarts anyway.
//report_tactic_progress("Plateau.", plateau_cnt);
// Andreas: Right now, a useless assignment is created in case of a restart. But we don't want to use restarts anyway.
//if (plateau_cnt < m_plateau_limit) {
TRACE("sls", tout << "In a plateau (" << plateau_cnt << "/" << m_plateau_limit << "); randomizing locally." << std::endl; );
#if _INTENSIFICATION_
handle_plateau(g, score);
//handle_plateau(g);
handle_plateau(g, score);
//handle_plateau(g);
#else
m_evaluator.randomize_local(g, m_stats.m_moves);
m_evaluator.randomize_local(g, m_stats.m_moves);
#endif
//mk_random_move(g);
//mk_random_move(g);
score = top_score(g);
if (score >= 1.0) {
bool all_true = true;
for (unsigned i = 0; i < g->size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
all_true=false;
if (all_true) {
res = l_true; // sat
goto bailout;
if (score >= 1.0) {
bool all_true = true;
for (unsigned i = 0; i < g->size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
all_true=false;
if (all_true) {
res = l_true; // sat
goto bailout;
} else
TRACE("sls", tout << "Imprecise 1.0 score" << std::endl;);
}
@ -1070,43 +1070,43 @@ class sls_tactic : public tactic {
return;
}
verbose_stream() << "_BFS_ " << _BFS_ << std::endl;
verbose_stream() << "_FOCUS_ " << _FOCUS_ << std::endl;
verbose_stream() << "_RESTARTS_ " << _RESTARTS_ << std::endl;
verbose_stream() << "_TIMELIMIT_ " << _TIMELIMIT_ << std::endl;
verbose_stream() << "_SCORE_AND_AVG_ " << _SCORE_AND_AVG_ << std::endl;
verbose_stream() << "_SCORE_OR_MUL_ " << _SCORE_OR_MUL_ << std::endl;
verbose_stream() << "_VNS_ " << _VNS_ << std::endl;
verbose_stream() << "_WEIGHT_DIST_ " << _WEIGHT_DIST_ << std::endl;
verbose_stream() << "_WEIGHT_DIST_FACTOR_ " << std::fixed << std::setprecision(2) << _WEIGHT_DIST_FACTOR_ << std::endl;
verbose_stream() << "_INTENSIFICATION_ " << _INTENSIFICATION_ << std::endl;
verbose_stream() << "_INTENSIFICATION_TRIES_ " << _INTENSIFICATION_TRIES_ << std::endl;
verbose_stream() << "_UCT_ " << _UCT_ << std::endl;
verbose_stream() << "_UCT_CONSTANT_ " << std::fixed << std::setprecision(2) << _UCT_CONSTANT_ << std::endl;
verbose_stream() << "_PROBABILISTIC_UCT_ " << _PROBABILISTIC_UCT_ << std::endl;
verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl;
verbose_stream() << "_USE_MUL2DIV2_ " << _USE_MUL2DIV2_ << std::endl;
verbose_stream() << "_USE_MUL3_ " << _USE_MUL3_ << std::endl;
verbose_stream() << "_USE_UNARY_MINUS_ " << _USE_UNARY_MINUS_ << std::endl;
verbose_stream() << "_UNIFORM_RANDOM_ " << _UNIFORM_RANDOM_ << std::endl;
verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl;
verbose_stream() << "_REAL_PBFS_ " << _REAL_PBFS_ << std::endl;
verbose_stream() << "_SKIP_BITS_ " << _SKIP_BITS_ << std::endl;
verbose_stream() << "_PERC_CHANGE_ " << _PERC_CHANGE_ << std::endl;
verbose_stream() << "_TYPE_RSTEP_ " << _TYPE_RSTEP_ << std::endl;
verbose_stream() << "_PERM_RSTEP_ " << _PERM_RSTEP_ << std::endl;
verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl;
verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl;
verbose_stream() << "_BFS_ " << _BFS_ << std::endl;
verbose_stream() << "_FOCUS_ " << _FOCUS_ << std::endl;
verbose_stream() << "_RESTARTS_ " << _RESTARTS_ << std::endl;
verbose_stream() << "_TIMELIMIT_ " << _TIMELIMIT_ << std::endl;
verbose_stream() << "_SCORE_AND_AVG_ " << _SCORE_AND_AVG_ << std::endl;
verbose_stream() << "_SCORE_OR_MUL_ " << _SCORE_OR_MUL_ << std::endl;
verbose_stream() << "_VNS_ " << _VNS_ << std::endl;
verbose_stream() << "_WEIGHT_DIST_ " << _WEIGHT_DIST_ << std::endl;
verbose_stream() << "_WEIGHT_DIST_FACTOR_ " << std::fixed << std::setprecision(2) << _WEIGHT_DIST_FACTOR_ << std::endl;
verbose_stream() << "_INTENSIFICATION_ " << _INTENSIFICATION_ << std::endl;
verbose_stream() << "_INTENSIFICATION_TRIES_ " << _INTENSIFICATION_TRIES_ << std::endl;
verbose_stream() << "_UCT_ " << _UCT_ << std::endl;
verbose_stream() << "_UCT_CONSTANT_ " << std::fixed << std::setprecision(2) << _UCT_CONSTANT_ << std::endl;
verbose_stream() << "_PROBABILISTIC_UCT_ " << _PROBABILISTIC_UCT_ << std::endl;
verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl;
verbose_stream() << "_USE_MUL2DIV2_ " << _USE_MUL2DIV2_ << std::endl;
verbose_stream() << "_USE_MUL3_ " << _USE_MUL3_ << std::endl;
verbose_stream() << "_USE_UNARY_MINUS_ " << _USE_UNARY_MINUS_ << std::endl;
verbose_stream() << "_UNIFORM_RANDOM_ " << _UNIFORM_RANDOM_ << std::endl;
verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl;
verbose_stream() << "_REAL_PBFS_ " << _REAL_PBFS_ << std::endl;
verbose_stream() << "_SKIP_BITS_ " << _SKIP_BITS_ << std::endl;
verbose_stream() << "_PERC_CHANGE_ " << _PERC_CHANGE_ << std::endl;
verbose_stream() << "_TYPE_RSTEP_ " << _TYPE_RSTEP_ << std::endl;
verbose_stream() << "_PERM_RSTEP_ " << _PERM_RSTEP_ << std::endl;
verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl;
verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl;
#if _WEIGHT_DIST_ == 4
m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_);
m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_);
#endif
m_tracker.initialize(g);
lbool res = l_undef;
do {
checkpoint();
// Andreas: I think restarts are too impotant to ignore 99% of them are happening...
// Andreas: I think restarts are too impotant to ignore 99% of them are happening...
//if ((m_stats.m_restarts % 100) == 0)
report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts);
@ -1115,12 +1115,12 @@ class sls_tactic : public tactic {
if (res == l_undef)
m_tracker.randomize();
}
while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && res != l_true && m_stats.m_restarts++ < m_max_restarts);
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;
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);
report_tactic_progress("Number of flips:", m_stats.m_moves);
if (m_produce_models) {
model_ref mdl = m_tracker.get_model();
mc = model2model_converter(mdl.get());
@ -1254,7 +1254,7 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) {
using_params(mk_simplify_tactic(m), simp2_p)),
using_params(mk_simplify_tactic(m), hoist_p),
mk_max_bv_sharing_tactic(m),
// Andreas: How does a NNF actually look like? Can it contain ITE operators?
// Andreas: How does a NNF actually look like? Can it contain ITE operators?
mk_nnf_tactic(m, p));
}