mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
removed tabs
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
140d28b6b3
commit
664fa82c6c
|
@ -528,7 +528,7 @@ public:
|
|||
mpz new_value;
|
||||
|
||||
#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_
|
||||
double new_score;
|
||||
double new_score;
|
||||
#endif
|
||||
|
||||
SASSERT(cur_depth < m_traversal_stack.size());
|
||||
|
@ -542,33 +542,33 @@ public:
|
|||
m_tracker.set_value(cur, new_value);
|
||||
|
||||
#if _REAL_RS_ || _REAL_PBFS_
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
{
|
||||
if (m_mpz_manager.eq(new_value,m_one))
|
||||
m_tracker.make_assertion(cur);
|
||||
else
|
||||
m_tracker.break_assertion(cur);
|
||||
}
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
{
|
||||
if (m_mpz_manager.eq(new_value,m_one))
|
||||
m_tracker.make_assertion(cur);
|
||||
else
|
||||
m_tracker.break_assertion(cur);
|
||||
}
|
||||
#endif
|
||||
|
||||
#if _EARLY_PRUNE_
|
||||
new_score = m_tracker.score(cur);
|
||||
new_score = m_tracker.score(cur);
|
||||
#if _CACHE_TOP_SCORE_
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
#endif
|
||||
m_tracker.set_score(cur, new_score);
|
||||
m_tracker.set_score_prune(cur, new_score);
|
||||
m_tracker.set_score(cur, new_score);
|
||||
m_tracker.set_score_prune(cur, new_score);
|
||||
#else
|
||||
#if _CACHE_TOP_SCORE_
|
||||
new_score = m_tracker.score(cur);
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
m_tracker.set_score(cur, new_score);
|
||||
new_score = m_tracker.score(cur);
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
m_tracker.set_score(cur, new_score);
|
||||
#else
|
||||
m_tracker.set_score(cur, m_tracker.score(cur));
|
||||
m_tracker.set_score(cur, m_tracker.score(cur));
|
||||
#endif
|
||||
#endif
|
||||
#endif
|
||||
if (m_tracker.has_uplinks(cur)) {
|
||||
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
|
||||
for (unsigned j = 0; j < ups.size(); j++) {
|
||||
|
@ -596,7 +596,7 @@ public:
|
|||
mpz new_value;
|
||||
|
||||
#if _EARLY_PRUNE_ || _CACHE_TOP_SCORE_
|
||||
double new_score;
|
||||
double new_score;
|
||||
#endif
|
||||
|
||||
SASSERT(cur_depth < m_traversal_stack.size());
|
||||
|
@ -609,23 +609,23 @@ public:
|
|||
(*this)(to_app(cur), new_value);
|
||||
m_tracker.set_value(cur, new_value);
|
||||
#if _EARLY_PRUNE_
|
||||
new_score = m_tracker.score(cur);
|
||||
new_score = m_tracker.score(cur);
|
||||
#if _CACHE_TOP_SCORE_
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
#endif
|
||||
m_tracker.set_score(cur, new_score);
|
||||
m_tracker.set_score_prune(cur, new_score);
|
||||
m_tracker.set_score(cur, new_score);
|
||||
m_tracker.set_score_prune(cur, new_score);
|
||||
#else
|
||||
#if _CACHE_TOP_SCORE_
|
||||
new_score = m_tracker.score(cur);
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
m_tracker.set_score(cur, new_score);
|
||||
new_score = m_tracker.score(cur);
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
m_tracker.set_score(cur, new_score);
|
||||
#else
|
||||
m_tracker.set_score(cur, m_tracker.score(cur));
|
||||
m_tracker.set_score(cur, m_tracker.score(cur));
|
||||
#endif
|
||||
#endif
|
||||
#endif
|
||||
if (m_tracker.has_uplinks(cur)) {
|
||||
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
|
||||
for (unsigned j = 0; j < ups.size(); j++) {
|
||||
|
@ -661,7 +661,7 @@ public:
|
|||
if (cur_depth > max_depth) max_depth = cur_depth;
|
||||
}
|
||||
#if _REAL_RS_ || _REAL_PBFS_
|
||||
run_serious_update(max_depth);
|
||||
run_serious_update(max_depth);
|
||||
#else
|
||||
run_update(max_depth);
|
||||
#endif
|
||||
|
@ -693,27 +693,27 @@ public:
|
|||
unsigned run_update_bool_prune(unsigned cur_depth) {
|
||||
expr_fast_mark1 visited;
|
||||
|
||||
double prune_score, new_score;
|
||||
unsigned pot_benefits = 0;
|
||||
SASSERT(cur_depth < m_traversal_stack_bool.size());
|
||||
double prune_score, new_score;
|
||||
unsigned pot_benefits = 0;
|
||||
SASSERT(cur_depth < m_traversal_stack_bool.size());
|
||||
|
||||
ptr_vector<expr> & 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);
|
||||
new_score = m_tracker.score(cur);
|
||||
#if _CACHE_TOP_SCORE_
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
#endif
|
||||
prune_score = m_tracker.get_score_prune(cur);
|
||||
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 ((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<expr> & ups = m_tracker.get_uplinks(cur);
|
||||
|
@ -722,54 +722,54 @@ public:
|
|||
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);
|
||||
m_traversal_stack_bool[next_d].push_back(next);
|
||||
visited.mark(next);
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
}
|
||||
}
|
||||
|
||||
cur_depth_exprs.reset();
|
||||
cur_depth_exprs.reset();
|
||||
cur_depth--;
|
||||
|
||||
while (cur_depth != static_cast<unsigned>(-1)) {
|
||||
ptr_vector<expr> & 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];
|
||||
while (cur_depth != static_cast<unsigned>(-1)) {
|
||||
ptr_vector<expr> & cur_depth_exprs = m_traversal_stack_bool[cur_depth];
|
||||
if (pot_benefits)
|
||||
{
|
||||
unsigned cur_size = cur_depth_exprs.size();
|
||||
for (unsigned i = 0; i < cur_size; i++) {
|
||||
expr * cur = cur_depth_exprs[i];
|
||||
|
||||
#if _CACHE_TOP_SCORE_
|
||||
new_score = m_tracker.score(cur);
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
m_tracker.set_score(cur, new_score);
|
||||
new_score = m_tracker.score(cur);
|
||||
if (!m_tracker.has_uplinks(cur))
|
||||
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
|
||||
m_tracker.set_score(cur, new_score);
|
||||
#else
|
||||
m_tracker.set_score(cur, m_tracker.score(cur));
|
||||
m_tracker.set_score(cur, m_tracker.score(cur));
|
||||
#endif
|
||||
if (m_tracker.has_uplinks(cur)) {
|
||||
ptr_vector<expr> & 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--;
|
||||
}
|
||||
if (m_tracker.has_uplinks(cur)) {
|
||||
ptr_vector<expr> & 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;
|
||||
return pot_benefits;
|
||||
}
|
||||
|
||||
void run_update_prune(unsigned max_depth) {
|
||||
|
@ -777,7 +777,7 @@ public:
|
|||
expr_fast_mark1 visited;
|
||||
mpz new_value;
|
||||
|
||||
unsigned cur_depth = max_depth;
|
||||
unsigned cur_depth = max_depth;
|
||||
SASSERT(cur_depth < m_traversal_stack.size());
|
||||
while (cur_depth != static_cast<unsigned>(-1)) {
|
||||
ptr_vector<expr> & cur_depth_exprs = m_traversal_stack[cur_depth];
|
||||
|
@ -787,7 +787,7 @@ public:
|
|||
|
||||
(*this)(to_app(cur), new_value);
|
||||
m_tracker.set_value(cur, new_value);
|
||||
// should always have uplinks ...
|
||||
// should always have uplinks ...
|
||||
if (m_tracker.has_uplinks(cur)) {
|
||||
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
|
||||
for (unsigned j = 0; j < ups.size(); j++) {
|
||||
|
@ -795,10 +795,10 @@ public:
|
|||
unsigned next_d = m_tracker.get_distance(next);
|
||||
SASSERT(next_d < cur_depth);
|
||||
if (!visited.is_marked(next)) {
|
||||
if (m_manager.is_bool(next))
|
||||
m_traversal_stack_bool[max_depth].push_back(next);
|
||||
else
|
||||
m_traversal_stack[next_d].push_back(next);
|
||||
if (m_manager.is_bool(next))
|
||||
m_traversal_stack_bool[max_depth].push_back(next);
|
||||
else
|
||||
m_traversal_stack[next_d].push_back(next);
|
||||
visited.mark(next);
|
||||
}
|
||||
}
|
||||
|
@ -817,23 +817,23 @@ public:
|
|||
expr * ep = m_tracker.get_entry_point(fd);
|
||||
unsigned cur_depth = m_tracker.get_distance(ep);
|
||||
|
||||
if (m_traversal_stack_bool.size() <= cur_depth)
|
||||
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_traversal_stack.size() <= cur_depth)
|
||||
m_traversal_stack.resize(cur_depth+1);
|
||||
|
||||
if (m_manager.is_bool(ep))
|
||||
m_traversal_stack_bool[cur_depth].push_back(ep);
|
||||
else
|
||||
{
|
||||
m_traversal_stack[cur_depth].push_back(ep);
|
||||
run_update_prune(cur_depth);
|
||||
}
|
||||
return run_update_bool_prune(cur_depth);
|
||||
if (m_manager.is_bool(ep))
|
||||
m_traversal_stack_bool[cur_depth].push_back(ep);
|
||||
else
|
||||
{
|
||||
m_traversal_stack[cur_depth].push_back(ep);
|
||||
run_update_prune(cur_depth);
|
||||
}
|
||||
return run_update_bool_prune(cur_depth);
|
||||
}
|
||||
#endif
|
||||
|
||||
void randomize_local(expr * e, unsigned int flip) {
|
||||
void randomize_local(expr * e, unsigned int flip) {
|
||||
ptr_vector<func_decl> & unsat_constants = m_tracker.get_constants(e);
|
||||
|
||||
// Randomize _one_ candidate:
|
||||
|
@ -841,30 +841,30 @@ public:
|
|||
func_decl * fd = unsat_constants[r];
|
||||
#if _PERC_CHANGE_
|
||||
sort * srt = fd->get_range();
|
||||
mpz temp;
|
||||
mpz temp;
|
||||
|
||||
if (m_manager.is_bool(srt))
|
||||
if (m_manager.is_bool(srt))
|
||||
m_mpz_manager.set(temp, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero);
|
||||
else
|
||||
else
|
||||
{
|
||||
mpz temp2, mask;
|
||||
unsigned bv_sz = m_bv_util.get_bv_size(srt);
|
||||
m_mpz_manager.set(temp, m_tracker.get_value(fd));
|
||||
mpz temp2, mask;
|
||||
unsigned bv_sz = m_bv_util.get_bv_size(srt);
|
||||
m_mpz_manager.set(temp, m_tracker.get_value(fd));
|
||||
|
||||
for (unsigned bit = 0; bit < bv_sz; bit++)
|
||||
if (m_tracker.get_random_uint(16) % 100 < _PERC_CHANGE_)
|
||||
{
|
||||
m_mpz_manager.set(mask, m_powers(bit));
|
||||
m_mpz_manager.bitwise_xor(temp, mask, temp2);
|
||||
m_mpz_manager.set(temp, temp2);
|
||||
}
|
||||
m_mpz_manager.del(mask);
|
||||
m_mpz_manager.del(temp2);
|
||||
}
|
||||
for (unsigned bit = 0; bit < bv_sz; bit++)
|
||||
if (m_tracker.get_random_uint(16) % 100 < _PERC_CHANGE_)
|
||||
{
|
||||
m_mpz_manager.set(mask, m_powers(bit));
|
||||
m_mpz_manager.bitwise_xor(temp, mask, temp2);
|
||||
m_mpz_manager.set(temp, temp2);
|
||||
}
|
||||
m_mpz_manager.del(mask);
|
||||
m_mpz_manager.del(temp2);
|
||||
}
|
||||
#else
|
||||
mpz temp = m_tracker.get_random(fd->get_range());
|
||||
mpz temp = m_tracker.get_random(fd->get_range());
|
||||
#endif
|
||||
update(fd, temp);
|
||||
update(fd, temp);
|
||||
m_mpz_manager.del(temp);
|
||||
}
|
||||
|
||||
|
@ -889,34 +889,34 @@ public:
|
|||
func_decl * fd = unsat_constants[r];
|
||||
#if _PERC_CHANGE_
|
||||
sort * srt = fd->get_range();
|
||||
mpz temp;
|
||||
mpz temp;
|
||||
|
||||
if (m_manager.is_bool(srt))
|
||||
if (m_manager.is_bool(srt))
|
||||
m_mpz_manager.set(temp, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero);
|
||||
else
|
||||
else
|
||||
{
|
||||
mpz temp2, mask;
|
||||
unsigned bv_sz = m_bv_util.get_bv_size(srt);
|
||||
m_mpz_manager.set(temp, m_tracker.get_value(fd));
|
||||
mpz temp2, mask;
|
||||
unsigned bv_sz = m_bv_util.get_bv_size(srt);
|
||||
m_mpz_manager.set(temp, m_tracker.get_value(fd));
|
||||
|
||||
for (unsigned bit = 0; bit < bv_sz; bit++)
|
||||
if (m_tracker.get_random_uint(16) % 100 < _PERC_CHANGE_)
|
||||
{
|
||||
m_mpz_manager.set(mask, m_powers(bit));
|
||||
m_mpz_manager.bitwise_xor(temp, mask, temp2);
|
||||
m_mpz_manager.set(temp, temp2);
|
||||
}
|
||||
m_mpz_manager.del(mask);
|
||||
m_mpz_manager.del(temp2);
|
||||
}
|
||||
for (unsigned bit = 0; bit < bv_sz; bit++)
|
||||
if (m_tracker.get_random_uint(16) % 100 < _PERC_CHANGE_)
|
||||
{
|
||||
m_mpz_manager.set(mask, m_powers(bit));
|
||||
m_mpz_manager.bitwise_xor(temp, mask, temp2);
|
||||
m_mpz_manager.set(temp, temp2);
|
||||
}
|
||||
m_mpz_manager.del(mask);
|
||||
m_mpz_manager.del(temp2);
|
||||
}
|
||||
#else
|
||||
mpz temp = m_tracker.get_random(fd->get_range());
|
||||
mpz temp = m_tracker.get_random(fd->get_range());
|
||||
#endif
|
||||
|
||||
#if _REAL_RS_ || _REAL_PBFS_
|
||||
serious_update(fd, temp);
|
||||
serious_update(fd, temp);
|
||||
#else
|
||||
update(fd, temp);
|
||||
update(fd, temp);
|
||||
#endif
|
||||
m_mpz_manager.del(temp);
|
||||
|
||||
|
|
|
@ -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));
|
||||
}
|
||||
|
||||
|
|
|
@ -29,31 +29,31 @@ class sls_tracker {
|
|||
unsigned m_random_bits;
|
||||
unsigned m_random_bits_cnt;
|
||||
mpz m_zero, m_one, m_two;
|
||||
|
||||
|
||||
struct value_score {
|
||||
#if _EARLY_PRUNE_
|
||||
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1), score_prune(0.0), has_pos_occ(0), has_neg_occ(0) { };
|
||||
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1), score_prune(0.0), has_pos_occ(0), has_neg_occ(0) { };
|
||||
#else
|
||||
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1) { };
|
||||
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0), touched(1) { };
|
||||
#endif
|
||||
~value_score() { if (m) m->del(value); }
|
||||
unsynch_mpz_manager * m;
|
||||
mpz value;
|
||||
double score;
|
||||
#if _EARLY_PRUNE_
|
||||
double score_prune;
|
||||
unsigned has_pos_occ;
|
||||
unsigned has_neg_occ;
|
||||
double score_prune;
|
||||
unsigned has_pos_occ;
|
||||
unsigned has_neg_occ;
|
||||
#endif
|
||||
unsigned distance; // max distance from any root
|
||||
unsigned touched;
|
||||
unsigned touched;
|
||||
value_score & operator=(const value_score & other) {
|
||||
SASSERT(m == 0 || m == other.m);
|
||||
if (m) m->set(value, 0); else m = other.m;
|
||||
m->set(value, other.value);
|
||||
score = other.score;
|
||||
distance = other.distance;
|
||||
touched = other.touched;
|
||||
touched = other.touched;
|
||||
return *this;
|
||||
}
|
||||
};
|
||||
|
@ -72,18 +72,18 @@ private:
|
|||
ptr_vector<func_decl> m_temp_constants;
|
||||
occ_type m_constants_occ;
|
||||
#if _UCT_
|
||||
unsigned m_touched;
|
||||
unsigned m_touched;
|
||||
#endif
|
||||
#if _REAL_RS_ || _REAL_PBFS_
|
||||
ptr_vector<expr> m_unsat_expr;
|
||||
obj_map<expr, unsigned> m_where_false;
|
||||
expr** m_list_false;
|
||||
ptr_vector<expr> m_unsat_expr;
|
||||
obj_map<expr, unsigned> m_where_false;
|
||||
expr** m_list_false;
|
||||
#endif
|
||||
#if _CACHE_TOP_SCORE_
|
||||
double m_top_sum;
|
||||
double m_top_sum;
|
||||
#endif
|
||||
#if _WEIGHT_DIST_ == 4
|
||||
double m_weight_dist_factor;
|
||||
double m_weight_dist_factor;
|
||||
#endif
|
||||
|
||||
public:
|
||||
|
@ -105,23 +105,23 @@ public:
|
|||
}
|
||||
|
||||
#if _WEIGHT_DIST_ == 4
|
||||
inline void set_weight_dist_factor(double val) {
|
||||
m_weight_dist_factor = val;
|
||||
}
|
||||
inline void set_weight_dist_factor(double val) {
|
||||
m_weight_dist_factor = val;
|
||||
}
|
||||
#endif
|
||||
|
||||
#if _CACHE_TOP_SCORE_
|
||||
inline void adapt_top_sum(double add, double sub) {
|
||||
m_top_sum += add - sub;
|
||||
}
|
||||
inline void adapt_top_sum(double add, double sub) {
|
||||
m_top_sum += add - sub;
|
||||
}
|
||||
|
||||
inline void set_top_sum(double new_score) {
|
||||
m_top_sum = new_score;
|
||||
}
|
||||
inline void set_top_sum(double new_score) {
|
||||
m_top_sum = new_score;
|
||||
}
|
||||
|
||||
inline double get_top_sum() {
|
||||
return m_top_sum;
|
||||
}
|
||||
inline double get_top_sum() {
|
||||
return m_top_sum;
|
||||
}
|
||||
#endif
|
||||
|
||||
inline void set_value(expr * n, const mpz & r) {
|
||||
|
@ -174,20 +174,20 @@ public:
|
|||
m_scores.find(n).score_prune = score;
|
||||
}
|
||||
|
||||
inline double & get_score_prune(expr * n) {
|
||||
inline double & get_score_prune(expr * n) {
|
||||
SASSERT(m_scores.contains(n));
|
||||
return m_scores.find(n).score_prune;
|
||||
}
|
||||
|
||||
inline unsigned has_pos_occ(expr * n) {
|
||||
inline unsigned has_pos_occ(expr * n) {
|
||||
SASSERT(m_scores.contains(n));
|
||||
return m_scores.find(n).has_pos_occ;
|
||||
}
|
||||
}
|
||||
|
||||
inline unsigned has_neg_occ(expr * n) {
|
||||
inline unsigned has_neg_occ(expr * n) {
|
||||
SASSERT(m_scores.contains(n));
|
||||
return m_scores.find(n).has_neg_occ;
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
inline unsigned get_distance(expr * n) {
|
||||
|
@ -316,45 +316,45 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
void initialize_recursive(init_proc proc, expr_mark visited, expr * e) {
|
||||
if (m_manager.is_and(e) || m_manager.is_or(e)) {
|
||||
app * a = to_app(e);
|
||||
expr * const * args = a->get_args();
|
||||
unsigned int sz = a->get_num_args();
|
||||
for (unsigned int i = 0; i < sz; i++) {
|
||||
expr * q = args[i];
|
||||
initialize_recursive(proc, visited, q);
|
||||
}
|
||||
}
|
||||
for_each_expr(proc, visited, e);
|
||||
}
|
||||
void initialize_recursive(init_proc proc, expr_mark visited, expr * e) {
|
||||
if (m_manager.is_and(e) || m_manager.is_or(e)) {
|
||||
app * a = to_app(e);
|
||||
expr * const * args = a->get_args();
|
||||
unsigned int sz = a->get_num_args();
|
||||
for (unsigned int i = 0; i < sz; i++) {
|
||||
expr * q = args[i];
|
||||
initialize_recursive(proc, visited, q);
|
||||
}
|
||||
}
|
||||
for_each_expr(proc, visited, e);
|
||||
}
|
||||
|
||||
void initialize_recursive(expr * e) {
|
||||
if (m_manager.is_and(e) || m_manager.is_or(e)) {
|
||||
app * a = to_app(e);
|
||||
expr * const * args = a->get_args();
|
||||
unsigned int sz = a->get_num_args();
|
||||
for (unsigned int i = 0; i < sz; i++) {
|
||||
expr * q = args[i];
|
||||
initialize_recursive(q);
|
||||
}
|
||||
}
|
||||
ptr_vector<func_decl> t;
|
||||
void initialize_recursive(expr * e) {
|
||||
if (m_manager.is_and(e) || m_manager.is_or(e)) {
|
||||
app * a = to_app(e);
|
||||
expr * const * args = a->get_args();
|
||||
unsigned int sz = a->get_num_args();
|
||||
for (unsigned int i = 0; i < sz; i++) {
|
||||
expr * q = args[i];
|
||||
initialize_recursive(q);
|
||||
}
|
||||
}
|
||||
ptr_vector<func_decl> t;
|
||||
m_constants_occ.insert_if_not_there(e, t);
|
||||
find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e));
|
||||
expr_fast_mark1 visited;
|
||||
quick_for_each_expr(ffd_proc, visited, e);
|
||||
}
|
||||
}
|
||||
|
||||
void initialize(goal_ref const & g) {
|
||||
void initialize(goal_ref const & g) {
|
||||
init_proc proc(m_manager, *this);
|
||||
expr_mark visited;
|
||||
unsigned sz = g->size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * e = g->form(i);
|
||||
// Andreas: Maybe not fully correct.
|
||||
// Andreas: Maybe not fully correct.
|
||||
#if _FOCUS_ == 2
|
||||
initialize_recursive(proc, visited, e);
|
||||
initialize_recursive(proc, visited, e);
|
||||
#endif
|
||||
for_each_expr(proc, visited, e);
|
||||
}
|
||||
|
@ -363,9 +363,9 @@ public:
|
|||
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * e = g->form(i);
|
||||
// Andreas: Maybe not fully correct.
|
||||
// Andreas: Maybe not fully correct.
|
||||
#if _FOCUS_ == 2 || _INTENSIFICATION_
|
||||
initialize_recursive(e);
|
||||
initialize_recursive(e);
|
||||
#endif
|
||||
ptr_vector<func_decl> t;
|
||||
m_constants_occ.insert_if_not_there(e, t);
|
||||
|
@ -379,53 +379,53 @@ public:
|
|||
TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); );
|
||||
|
||||
#if _REAL_RS_ || _REAL_PBFS_
|
||||
m_list_false = new expr*[sz];
|
||||
m_list_false = new expr*[sz];
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
if (m_mpz_manager.eq(get_value(g->form(i)),m_zero))
|
||||
break_assertion(g->form(i));
|
||||
if (m_mpz_manager.eq(get_value(g->form(i)),m_zero))
|
||||
break_assertion(g->form(i));
|
||||
#endif
|
||||
|
||||
#if _EARLY_PRUNE_
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
setup_occs(g->form(i));
|
||||
setup_occs(g->form(i));
|
||||
#endif
|
||||
|
||||
#if _UCT_
|
||||
m_touched = 1;
|
||||
m_touched = 1;
|
||||
#endif
|
||||
}
|
||||
|
||||
#if _REAL_RS_ || _REAL_PBFS_
|
||||
void make_assertion(expr * e)
|
||||
{
|
||||
if (m_where_false.contains(e))
|
||||
{
|
||||
unsigned pos = m_where_false.find(e);
|
||||
m_where_false.erase(e);
|
||||
if (pos != m_where_false.size())
|
||||
{
|
||||
expr * q = m_list_false[m_where_false.size()];
|
||||
m_list_false[pos] = q;
|
||||
m_where_false.find(q) = pos;
|
||||
}
|
||||
// printf("Going in %d\n", m_where_false.size());
|
||||
}
|
||||
//if (m_unsat_expr.contains(e))
|
||||
//m_unsat_expr.erase(e);
|
||||
}
|
||||
void make_assertion(expr * e)
|
||||
{
|
||||
if (m_where_false.contains(e))
|
||||
{
|
||||
unsigned pos = m_where_false.find(e);
|
||||
m_where_false.erase(e);
|
||||
if (pos != m_where_false.size())
|
||||
{
|
||||
expr * q = m_list_false[m_where_false.size()];
|
||||
m_list_false[pos] = q;
|
||||
m_where_false.find(q) = pos;
|
||||
}
|
||||
// printf("Going in %d\n", m_where_false.size());
|
||||
}
|
||||
//if (m_unsat_expr.contains(e))
|
||||
//m_unsat_expr.erase(e);
|
||||
}
|
||||
|
||||
void break_assertion(expr * e)
|
||||
{
|
||||
if (!m_where_false.contains(e))
|
||||
{
|
||||
unsigned pos = m_where_false.size();
|
||||
m_list_false[pos] = e;
|
||||
m_where_false.insert(e, pos);
|
||||
// printf("Going in %d\n", m_where_false.size());
|
||||
}
|
||||
//if (!m_unsat_expr.contains(e))
|
||||
//m_unsat_expr.push_back(e);
|
||||
}
|
||||
void break_assertion(expr * e)
|
||||
{
|
||||
if (!m_where_false.contains(e))
|
||||
{
|
||||
unsigned pos = m_where_false.size();
|
||||
m_list_false[pos] = e;
|
||||
m_where_false.insert(e, pos);
|
||||
// printf("Going in %d\n", m_where_false.size());
|
||||
}
|
||||
//if (!m_unsat_expr.contains(e))
|
||||
//m_unsat_expr.push_back(e);
|
||||
}
|
||||
#endif
|
||||
|
||||
void show_model(std::ostream & out) {
|
||||
|
@ -537,35 +537,35 @@ public:
|
|||
}
|
||||
|
||||
#if _EARLY_PRUNE_
|
||||
void setup_occs(expr * n, bool negated = false) {
|
||||
if (m_manager.is_bool(n))
|
||||
{
|
||||
if (m_manager.is_and(n) || m_manager.is_or(n))
|
||||
{
|
||||
SASSERT(!negated);
|
||||
app * a = to_app(n);
|
||||
expr * const * args = a->get_args();
|
||||
for (unsigned i = 0; i < a->get_num_args(); i++)
|
||||
setup_occs(args[i]);
|
||||
}
|
||||
else if (m_manager.is_not(n))
|
||||
{
|
||||
SASSERT(!negated);
|
||||
app * a = to_app(n);
|
||||
SASSERT(a->get_num_args() == 1);
|
||||
expr * child = a->get_arg(0);
|
||||
if (m_manager.is_and(child) || m_manager.is_or(child))
|
||||
NOT_IMPLEMENTED_YET();
|
||||
setup_occs(child, true);
|
||||
}
|
||||
else
|
||||
{
|
||||
if (negated)
|
||||
m_scores.find(n).has_neg_occ = 1;
|
||||
else
|
||||
m_scores.find(n).has_pos_occ = 1;
|
||||
}
|
||||
}
|
||||
void setup_occs(expr * n, bool negated = false) {
|
||||
if (m_manager.is_bool(n))
|
||||
{
|
||||
if (m_manager.is_and(n) || m_manager.is_or(n))
|
||||
{
|
||||
SASSERT(!negated);
|
||||
app * a = to_app(n);
|
||||
expr * const * args = a->get_args();
|
||||
for (unsigned i = 0; i < a->get_num_args(); i++)
|
||||
setup_occs(args[i]);
|
||||
}
|
||||
else if (m_manager.is_not(n))
|
||||
{
|
||||
SASSERT(!negated);
|
||||
app * a = to_app(n);
|
||||
SASSERT(a->get_num_args() == 1);
|
||||
expr * child = a->get_arg(0);
|
||||
if (m_manager.is_and(child) || m_manager.is_or(child))
|
||||
NOT_IMPLEMENTED_YET();
|
||||
setup_occs(child, true);
|
||||
}
|
||||
else
|
||||
{
|
||||
if (negated)
|
||||
m_scores.find(n).has_neg_occ = 1;
|
||||
else
|
||||
m_scores.find(n).has_pos_occ = 1;
|
||||
}
|
||||
}
|
||||
else
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
@ -574,7 +574,7 @@ public:
|
|||
double score_bool(expr * n, bool negated = false) {
|
||||
TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; );
|
||||
|
||||
double res = 0.0;
|
||||
double res = 0.0;
|
||||
|
||||
if (is_uninterp_const(n)) {
|
||||
const mpz & r = get_value(n);
|
||||
|
@ -587,14 +587,14 @@ public:
|
|||
SASSERT(!negated);
|
||||
app * a = to_app(n);
|
||||
expr * const * args = a->get_args();
|
||||
// Andreas: Seems to have no effect. Probably it does not even occur.
|
||||
// Andreas: Seems to have no effect. Probably it does not even occur.
|
||||
#if _SCORE_AND_AVG_
|
||||
double sum = 0.0;
|
||||
for (unsigned i = 0; i < a->get_num_args(); i++)
|
||||
sum += get_score(args[i]);
|
||||
res = sum / (double) a->get_num_args();
|
||||
#else
|
||||
double min = 1.0;
|
||||
double min = 1.0;
|
||||
for (unsigned i = 0; i < a->get_num_args(); i++) {
|
||||
double cur = get_score(args[i]);
|
||||
if (cur < min) min = cur;
|
||||
|
@ -606,16 +606,16 @@ public:
|
|||
SASSERT(!negated);
|
||||
app * a = to_app(n);
|
||||
expr * const * args = a->get_args();
|
||||
// Andreas: Seems to have no effect. Probably it is still too similar to the original version.
|
||||
// Andreas: Seems to have no effect. Probably it is still too similar to the original version.
|
||||
#if _SCORE_OR_MUL_
|
||||
double inv = 1.0;
|
||||
double inv = 1.0;
|
||||
for (unsigned i = 0; i < a->get_num_args(); i++) {
|
||||
double cur = get_score(args[i]);
|
||||
inv *= (1.0 - get_score(args[i]));
|
||||
}
|
||||
res = 1.0 - inv;
|
||||
#else
|
||||
double max = 0.0;
|
||||
double max = 0.0;
|
||||
for (unsigned i = 0; i < a->get_num_args(); i++) {
|
||||
double cur = get_score(args[i]);
|
||||
if (cur > max) max = cur;
|
||||
|
@ -639,7 +639,7 @@ public:
|
|||
expr * arg1 = a->get_arg(1);
|
||||
const mpz & v0 = get_value(arg0);
|
||||
const mpz & v1 = get_value(arg1);
|
||||
|
||||
|
||||
if (negated) {
|
||||
res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0;
|
||||
TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " <<
|
||||
|
@ -701,7 +701,7 @@ public:
|
|||
double dbl = n.get_double();
|
||||
// In extreme cases, n is 0.9999 but to_double returns something > 1.0
|
||||
res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
|
||||
m_mpz_manager.del(diff);
|
||||
m_mpz_manager.del(diff);
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
@ -762,7 +762,7 @@ public:
|
|||
TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " <<
|
||||
m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; );
|
||||
}
|
||||
m_mpz_manager.del(x);
|
||||
m_mpz_manager.del(x);
|
||||
m_mpz_manager.del(y);
|
||||
}
|
||||
else if (m_manager.is_not(n)) {
|
||||
|
@ -797,25 +797,25 @@ public:
|
|||
SASSERT(res >= 0.0 && res <= 1.0);
|
||||
|
||||
#if _WEIGHT_DIST_
|
||||
app * a = to_app(n);
|
||||
family_id afid = a->get_family_id();
|
||||
app * a = to_app(n);
|
||||
family_id afid = a->get_family_id();
|
||||
|
||||
if (afid == m_bv_util.get_family_id())
|
||||
if (afid == m_bv_util.get_family_id())
|
||||
#endif
|
||||
#if _WEIGHT_DIST_ == 1
|
||||
if (res < 1.0) res *= _WEIGHT_DIST_FACTOR_;
|
||||
if (res < 1.0) res *= _WEIGHT_DIST_FACTOR_;
|
||||
#elif _WEIGHT_DIST_ == 2
|
||||
res *= res;
|
||||
res *= res;
|
||||
#elif _WEIGHT_DIST_ == 3
|
||||
if (res < 1.0) res = 0.0;
|
||||
if (res < 1.0) res = 0.0;
|
||||
#elif _WEIGHT_DIST_ == 4
|
||||
if (res < 1.0) res *= m_weight_dist_factor;
|
||||
if (res < 1.0) res *= m_weight_dist_factor;
|
||||
#endif
|
||||
|
||||
TRACE("sls_score", tout << "SCORE = " << res << std::endl; );
|
||||
return res;
|
||||
}
|
||||
|
||||
|
||||
double score_bv(expr * n) {
|
||||
return 0.0; // a bv-expr is always scored as 0.0; we won't use those scores.
|
||||
}
|
||||
|
@ -861,34 +861,34 @@ public:
|
|||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
expr * get_unsat_expression(expr * e) {
|
||||
if (m_manager.is_bool(e)) {
|
||||
if (m_manager.is_and(e) || m_manager.is_or(e)) {
|
||||
app * a = to_app(e);
|
||||
expr * const * args = a->get_args();
|
||||
// Andreas: might be used for guided branching
|
||||
//for (unsigned i = 0; i < a->get_num_args(); i++) {
|
||||
//double cur = get_score(args[i]);
|
||||
//}
|
||||
// Andreas: A random number is better here since reusing flip will cause patterns.
|
||||
unsigned int sz = a->get_num_args();
|
||||
unsigned int pos = get_random_uint(16) % sz;
|
||||
for (unsigned int i = pos; i < sz; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return get_unsat_expression(q);
|
||||
}
|
||||
for (unsigned int i = 0; i < pos; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return get_unsat_expression(q);
|
||||
}
|
||||
}
|
||||
}
|
||||
return e;
|
||||
}
|
||||
expr * get_unsat_expression(expr * e) {
|
||||
if (m_manager.is_bool(e)) {
|
||||
if (m_manager.is_and(e) || m_manager.is_or(e)) {
|
||||
app * a = to_app(e);
|
||||
expr * const * args = a->get_args();
|
||||
// Andreas: might be used for guided branching
|
||||
//for (unsigned i = 0; i < a->get_num_args(); i++) {
|
||||
//double cur = get_score(args[i]);
|
||||
//}
|
||||
// Andreas: A random number is better here since reusing flip will cause patterns.
|
||||
unsigned int sz = a->get_num_args();
|
||||
unsigned int pos = get_random_uint(16) % sz;
|
||||
for (unsigned int i = pos; i < sz; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return get_unsat_expression(q);
|
||||
}
|
||||
for (unsigned int i = 0; i < pos; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return get_unsat_expression(q);
|
||||
}
|
||||
}
|
||||
}
|
||||
return e;
|
||||
}
|
||||
|
||||
ptr_vector<func_decl> & get_constants(expr * e) {
|
||||
ptr_vector<func_decl> & get_constants(expr * e) {
|
||||
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
|
||||
unsigned sz = this_decls.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
|
@ -897,9 +897,9 @@ public:
|
|||
m_temp_constants.push_back(fd);
|
||||
}
|
||||
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(goal_ref const & g, unsigned sz) {
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * q = g->form(i);
|
||||
if (m_mpz_manager.eq(get_value(q), m_one))
|
||||
|
@ -913,244 +913,244 @@ public:
|
|||
}
|
||||
}
|
||||
return m_temp_constants;
|
||||
}
|
||||
}
|
||||
|
||||
expr * get_unsat_assertion(goal_ref const & g, unsigned sz, unsigned int pos) {
|
||||
for (unsigned i = pos; i < sz; i++) {
|
||||
expr * get_unsat_assertion(goal_ref const & g, unsigned sz, unsigned int pos) {
|
||||
for (unsigned i = pos; i < sz; i++) {
|
||||
expr * q = g->form(i);
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return q;
|
||||
}
|
||||
for (unsigned i = 0; i < pos; i++) {
|
||||
expr * q = g->form(i);
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return q;
|
||||
return q;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
for (unsigned i = 0; i < pos; i++) {
|
||||
expr * q = g->form(i);
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return q;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
ptr_vector<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(goal_ref const & g, unsigned sz, unsigned int pos) {
|
||||
expr * q = get_unsat_assertion(g, sz, pos);
|
||||
// Andreas: I should probably fix this. If this is the case then the formula is SAT anyway but this is not checked in the first iteration.
|
||||
if (!q)
|
||||
return m_temp_constants;
|
||||
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(q);
|
||||
if (!q)
|
||||
return m_temp_constants;
|
||||
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(q);
|
||||
unsigned sz2 = this_decls.size();
|
||||
for (unsigned j = 0; j < sz2; j++) {
|
||||
func_decl * fd = this_decls[j];
|
||||
if (!m_temp_constants.contains(fd))
|
||||
m_temp_constants.push_back(fd);
|
||||
}
|
||||
return m_temp_constants;
|
||||
}
|
||||
return m_temp_constants;
|
||||
}
|
||||
|
||||
ptr_vector<func_decl> & get_unsat_constants_walksat(expr * e) {
|
||||
if (!e)
|
||||
return m_temp_constants;
|
||||
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
|
||||
ptr_vector<func_decl> & get_unsat_constants_walksat(expr * e) {
|
||||
if (!e)
|
||||
return m_temp_constants;
|
||||
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
|
||||
unsigned sz = this_decls.size();
|
||||
for (unsigned j = 0; j < sz; j++) {
|
||||
func_decl * fd = this_decls[j];
|
||||
if (!m_temp_constants.contains(fd))
|
||||
m_temp_constants.push_back(fd);
|
||||
}
|
||||
return m_temp_constants;
|
||||
}
|
||||
return m_temp_constants;
|
||||
}
|
||||
|
||||
ptr_vector<func_decl> & go_deeper(expr * e) {
|
||||
if (m_manager.is_bool(e)) {
|
||||
if (m_manager.is_and(e)) {
|
||||
app * a = to_app(e);
|
||||
expr * const * args = a->get_args();
|
||||
// Andreas: might be used for guided branching
|
||||
//for (unsigned i = 0; i < a->get_num_args(); i++) {
|
||||
//double cur = get_score(args[i]);
|
||||
//}
|
||||
// Andreas: A random number is better here since reusing flip will cause patterns.
|
||||
unsigned int sz = a->get_num_args();
|
||||
unsigned int pos = get_random_uint(16) % sz;
|
||||
for (unsigned int i = pos; i < sz; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return go_deeper(q);
|
||||
}
|
||||
for (unsigned int i = 0; i < pos; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return go_deeper(q);
|
||||
}
|
||||
}
|
||||
else if (m_manager.is_or(e)) {
|
||||
app * a = to_app(e);
|
||||
expr * const * args = a->get_args();
|
||||
unsigned int sz = a->get_num_args();
|
||||
unsigned int pos = get_random_uint(16) % sz;
|
||||
for (unsigned int i = pos; i < sz; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return go_deeper(q);
|
||||
}
|
||||
for (unsigned int i = 0; i < pos; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return go_deeper(q);
|
||||
}
|
||||
}
|
||||
}
|
||||
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
|
||||
ptr_vector<func_decl> & go_deeper(expr * e) {
|
||||
if (m_manager.is_bool(e)) {
|
||||
if (m_manager.is_and(e)) {
|
||||
app * a = to_app(e);
|
||||
expr * const * args = a->get_args();
|
||||
// Andreas: might be used for guided branching
|
||||
//for (unsigned i = 0; i < a->get_num_args(); i++) {
|
||||
//double cur = get_score(args[i]);
|
||||
//}
|
||||
// Andreas: A random number is better here since reusing flip will cause patterns.
|
||||
unsigned int sz = a->get_num_args();
|
||||
unsigned int pos = get_random_uint(16) % sz;
|
||||
for (unsigned int i = pos; i < sz; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return go_deeper(q);
|
||||
}
|
||||
for (unsigned int i = 0; i < pos; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return go_deeper(q);
|
||||
}
|
||||
}
|
||||
else if (m_manager.is_or(e)) {
|
||||
app * a = to_app(e);
|
||||
expr * const * args = a->get_args();
|
||||
unsigned int sz = a->get_num_args();
|
||||
unsigned int pos = get_random_uint(16) % sz;
|
||||
for (unsigned int i = pos; i < sz; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return go_deeper(q);
|
||||
}
|
||||
for (unsigned int i = 0; i < pos; i++) {
|
||||
expr * q = args[i];
|
||||
if (m_mpz_manager.neq(get_value(q), m_one))
|
||||
return go_deeper(q);
|
||||
}
|
||||
}
|
||||
}
|
||||
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e);
|
||||
unsigned sz2 = this_decls.size();
|
||||
for (unsigned j = 0; j < sz2; j++) {
|
||||
func_decl * fd = this_decls[j];
|
||||
if (!m_temp_constants.contains(fd))
|
||||
m_temp_constants.push_back(fd);
|
||||
}
|
||||
return m_temp_constants;
|
||||
}
|
||||
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(goal_ref const & g, unsigned sz, unsigned int pos) {
|
||||
expr * q = get_unsat_assertion(g, sz, pos);
|
||||
if (!q)
|
||||
return m_temp_constants;
|
||||
return m_temp_constants;
|
||||
|
||||
return go_deeper(q);
|
||||
}
|
||||
return go_deeper(q);
|
||||
}
|
||||
|
||||
ptr_vector<func_decl> & get_unsat_constants(goal_ref const & g, unsigned int flip) {
|
||||
ptr_vector<func_decl> & get_unsat_constants(goal_ref const & g, unsigned int flip) {
|
||||
unsigned sz = g->size();
|
||||
|
||||
if (sz == 1) {
|
||||
if (m_mpz_manager.eq(get_value(g->form(0)), m_one))
|
||||
return m_temp_constants;
|
||||
else
|
||||
return get_constants();
|
||||
if (m_mpz_manager.eq(get_value(g->form(0)), m_one))
|
||||
return m_temp_constants;
|
||||
else
|
||||
return get_constants();
|
||||
}
|
||||
else {
|
||||
m_temp_constants.reset();
|
||||
#if _FOCUS_ == 1
|
||||
#if _UCT_
|
||||
unsigned pos = -1;
|
||||
value_score vscore;
|
||||
unsigned pos = -1;
|
||||
value_score vscore;
|
||||
#if _PROBABILISTIC_UCT_
|
||||
double sum_score = 0.0;
|
||||
unsigned start_index = get_random_uint(16) % sz;
|
||||
for (unsigned i = start_index; i < sz; i++)
|
||||
{
|
||||
expr * e = g->form(i);
|
||||
vscore = m_scores.find(e);
|
||||
double sum_score = 0.0;
|
||||
unsigned start_index = get_random_uint(16) % sz;
|
||||
for (unsigned i = start_index; i < sz; i++)
|
||||
{
|
||||
expr * e = g->form(i);
|
||||
vscore = m_scores.find(e);
|
||||
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched);
|
||||
if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
|
||||
sum_score += q;
|
||||
if (rand() <= (q * RAND_MAX / sum_score) + 1)
|
||||
pos = i;
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < start_index; i++)
|
||||
{
|
||||
expr * e = g->form(i);
|
||||
vscore = m_scores.find(e);
|
||||
if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
|
||||
sum_score += q;
|
||||
if (rand() <= (q * RAND_MAX / sum_score) + 1)
|
||||
pos = i;
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < start_index; i++)
|
||||
{
|
||||
expr * e = g->form(i);
|
||||
vscore = m_scores.find(e);
|
||||
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched);
|
||||
if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
|
||||
sum_score += q;
|
||||
if (rand() <= (q * RAND_MAX / sum_score) + 1)
|
||||
pos = i;
|
||||
}
|
||||
}
|
||||
if (m_mpz_manager.neq(get_value(g->form(i)), m_one)) {
|
||||
sum_score += q;
|
||||
if (rand() <= (q * RAND_MAX / sum_score) + 1)
|
||||
pos = i;
|
||||
}
|
||||
}
|
||||
#else
|
||||
double max = -1.0;
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * e = g->form(i);
|
||||
vscore = m_scores.find(e);
|
||||
double max = -1.0;
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * e = g->form(i);
|
||||
vscore = m_scores.find(e);
|
||||
#if _UCT_ == 1
|
||||
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched);
|
||||
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched);
|
||||
#elif _UCT_ == 2
|
||||
double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz;
|
||||
double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz;
|
||||
#endif
|
||||
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
|
||||
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
|
||||
}
|
||||
#endif
|
||||
if (pos == static_cast<unsigned>(-1))
|
||||
return m_temp_constants;
|
||||
if (pos == static_cast<unsigned>(-1))
|
||||
return m_temp_constants;
|
||||
|
||||
#if _UCT_ == 1
|
||||
m_scores.find(g->form(pos)).touched++;
|
||||
m_touched++;
|
||||
m_scores.find(g->form(pos)).touched++;
|
||||
m_touched++;
|
||||
#elif _UCT_ == 2
|
||||
m_scores.find(g->form(pos)).touched = flip;
|
||||
m_scores.find(g->form(pos)).touched = flip;
|
||||
#endif
|
||||
expr * e = g->form(pos);
|
||||
expr * e = g->form(pos);
|
||||
|
||||
#elif _BFS_ == 3
|
||||
unsigned int pos = -1;
|
||||
double max = -1.0;
|
||||
unsigned int pos = -1;
|
||||
double max = -1.0;
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * e = g->form(i);
|
||||
expr * e = g->form(i);
|
||||
double q = get_score(e);
|
||||
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
|
||||
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
|
||||
}
|
||||
if (pos == static_cast<unsigned>(-1))
|
||||
return m_temp_constants;
|
||||
expr * e = g->form(pos);
|
||||
if (pos == static_cast<unsigned>(-1))
|
||||
return m_temp_constants;
|
||||
expr * e = g->form(pos);
|
||||
#elif _BFS_ == 2
|
||||
unsigned int pos = -1;
|
||||
double min = 2.0;
|
||||
unsigned int pos = -1;
|
||||
double min = 2.0;
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * e = g->form(i);
|
||||
expr * e = g->form(i);
|
||||
double q = get_score(e);
|
||||
if (q < min && m_mpz_manager.neq(get_value(e), m_one) ) { min = q; pos = i; }
|
||||
if (q < min && m_mpz_manager.neq(get_value(e), m_one) ) { min = q; pos = i; }
|
||||
}
|
||||
if (pos == static_cast<unsigned>(-1))
|
||||
return m_temp_constants;
|
||||
expr * e = g->form(pos);
|
||||
if (pos == static_cast<unsigned>(-1))
|
||||
return m_temp_constants;
|
||||
expr * e = g->form(pos);
|
||||
#elif _BFS_ == 1
|
||||
// I guess it was buggy ...
|
||||
// unsigned int pos = flip % m_constants.size();
|
||||
unsigned int pos = flip % sz;
|
||||
expr * e = get_unsat_assertion(g, sz, pos);
|
||||
// I guess it was buggy ...
|
||||
// unsigned int pos = flip % m_constants.size();
|
||||
unsigned int pos = flip % sz;
|
||||
expr * e = get_unsat_assertion(g, sz, pos);
|
||||
#elif _UNIFORM_RANDOM_
|
||||
unsigned cnt_unsat = 0, pos = -1;
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i;
|
||||
if (pos == static_cast<unsigned>(-1))
|
||||
return m_temp_constants;
|
||||
expr * e = g->form(pos);
|
||||
unsigned cnt_unsat = 0, pos = -1;
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i;
|
||||
if (pos == static_cast<unsigned>(-1))
|
||||
return m_temp_constants;
|
||||
expr * e = g->form(pos);
|
||||
#elif _REAL_RS_
|
||||
//unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false];
|
||||
//expr * e = get_unsat_assertion(g, sz, pos);
|
||||
//expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()];
|
||||
sz = m_where_false.size();
|
||||
if (sz == 0)
|
||||
return m_temp_constants;
|
||||
else
|
||||
expr * e = m_list_false[get_random_uint(16) % sz];
|
||||
//unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false];
|
||||
//expr * e = get_unsat_assertion(g, sz, pos);
|
||||
//expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()];
|
||||
sz = m_where_false.size();
|
||||
if (sz == 0)
|
||||
return m_temp_constants;
|
||||
else
|
||||
expr * e = m_list_false[get_random_uint(16) % sz];
|
||||
#elif _REAL_PBFS_
|
||||
//unsigned pos = m_false_list[flip % m_cnt_false];
|
||||
//expr * e = get_unsat_assertion(g, sz, pos);
|
||||
//expr * e = m_unsat_expr[flip % m_unsat_expr.size()];
|
||||
sz = m_where_false.size();
|
||||
if (sz == 0)
|
||||
return m_temp_constants;
|
||||
else
|
||||
expr * e = m_list_false[flip % sz];
|
||||
//unsigned pos = m_false_list[flip % m_cnt_false];
|
||||
//expr * e = get_unsat_assertion(g, sz, pos);
|
||||
//expr * e = m_unsat_expr[flip % m_unsat_expr.size()];
|
||||
sz = m_where_false.size();
|
||||
if (sz == 0)
|
||||
return m_temp_constants;
|
||||
else
|
||||
expr * e = m_list_false[flip % sz];
|
||||
#else
|
||||
// I guess it was buggy ...
|
||||
// unsigned int pos = get_random_uint(16) % m_constants.size();
|
||||
unsigned int pos = get_random_uint(16) % sz;
|
||||
expr * e = get_unsat_assertion(g, sz, pos);
|
||||
// I guess it was buggy ...
|
||||
// unsigned int pos = get_random_uint(16) % m_constants.size();
|
||||
unsigned int pos = get_random_uint(16) % sz;
|
||||
expr * e = get_unsat_assertion(g, sz, pos);
|
||||
#endif
|
||||
return get_unsat_constants_walksat(e);
|
||||
return get_unsat_constants_walksat(e);
|
||||
#elif _FOCUS_ == 2
|
||||
#if _BFS_
|
||||
// I guess it was buggy ...
|
||||
// unsigned int pos = flip % m_constants.size();
|
||||
unsigned int pos = flip % sz;
|
||||
// I guess it was buggy ...
|
||||
// unsigned int pos = flip % m_constants.size();
|
||||
unsigned int pos = flip % sz;
|
||||
#else
|
||||
// I guess it was buggy ...
|
||||
// unsigned int pos = get_random_uint(16) % m_constants.size();
|
||||
unsigned int pos = get_random_uint(16) % sz;
|
||||
// I guess it was buggy ...
|
||||
// unsigned int pos = get_random_uint(16) % m_constants.size();
|
||||
unsigned int pos = get_random_uint(16) % sz;
|
||||
#endif
|
||||
return get_unsat_constants_crsat(g, sz, pos);
|
||||
return get_unsat_constants_crsat(g, sz, pos);
|
||||
#else
|
||||
return get_unsat_constants_gsat(g, sz);
|
||||
return get_unsat_constants_gsat(g, sz);
|
||||
#endif
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue