mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

Current version before integration ...

Browse source
This commit is contained in:
Andreas Froehlich 2014-04-20 16:38:49 +01:00 committed by Christoph M. Wintersteiger
parent f88b034b8b
commit 42702c8d8a
7 changed files with 1068 additions and 287 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/tactic/sls/sls_compilation_settings.h
View file

@ -36,17 +36,21 @@ Notes:
// do we use dirty unit propagation to get rid of nested top level assertions?
#define _DIRTY_UP_ 0
// shall we use additive weighting scheme?
#define _PAWS_ 5
#define _PAWS_INIT_ 40
// do we use restarts?
// 0 = no, 1 = use #moves, 2 = use #plateaus, 3 = use time
#define _RESTARTS_ 3
#define _RESTARTS_ 1
// limit of moves/plateaus/seconds until first restart occurs
#define _RESTART_LIMIT_ 10
#define _RESTART_LIMIT_ 100
// 0 = initialize with all zero, 1 initialize with random value
#define _RESTART_INIT_ 0
// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid
// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid, 5 = minisat
#define _RESTART_SCHEME_ 1
// base value c for armin restart scheme using c^inner - only applies for _RESTART_SCHEME_ 3
#define _RESTART_CONST_ARMIN_ 3.0
#define _RESTART_CONST_ARMIN_ 2.0
// timelimit
#define _TIMELIMIT_ 3600
@ -61,6 +65,21 @@ Notes:
// 0 = no, 1 = only consider flipping bits if no better score can be obtained otherwise, 2 = only consider flipping bits until a better score can be obtained
#define _VNS_ 0
// shall we check 2-bit flips in plateaus using Monte Carlo?
#define _VNS_MC_ 0
// how many 2-bit flips shall we try per bit?
#define _VNS_MC_TRIES_ 1
// shall we check another assertion if no improving step was found in the first one?
#define _VNS_REPICK_ 0
// what is the probability of doing so (percentage)?
#define _VNS_PERC_ 100
// do a decreasing move with percentage ...
#define _INSIST_PERC_ 0
// do we reduce the score of unsatisfied literals?
// 0 = no
// 1 = yes, by multiplying it with some factor
@ -70,7 +89,7 @@ Notes:
#define _WEIGHT_DIST_ 1
// the factor used for _WEIGHT_DIST_ = 1
#define _WEIGHT_DIST_FACTOR_ 0.25
#define _WEIGHT_DIST_FACTOR_ 0.5
// shall we toggle the weight after each restart?
#define _WEIGHT_TOGGLE_ 0
@ -82,14 +101,15 @@ Notes:
// what is the percentage of random moves in plateaus (instead of full randomization)?
#define _PERC_PLATEAU_MOVES_ 0
// shall we repick clause when randomizing in a plateau or use the current one?
// shall we repick assertion when randomizing in a plateau or use the current one?
// 0 = use old one, 1 = repick according to usual scheme, 2 = repick randomly and force different one
#define _REPICK_ 1
// do we use some UCT-like scheme for assertion-selection? overrides _BFS_
#define _UCT_ 1
// how much diversification is used in the UCT-scheme?
#define _UCT_CONSTANT_ 10.0
#define _UCT_CONSTANT_ 20.0
// is uct clause selection probabilistic similar to variable selection in sparrow?
// 0 = no, 1 = yes, use uct-value, 2 = yes, use score-value (_UCT_CONSTANT_ = 0.0) with squared score
@ -103,7 +123,11 @@ Notes:
// how shall we initialize the _UCT_ total touched counter?
// 0 = initialize with one, 1 = initialize with number of assertions
#define _UCT_INIT_ 1
#define _UCT_INIT_ 0
// do we gradually reduce the touched values of _UCT_?
#define _UCT_FORGET_ 0
#define _UCT_FORGET_FACTOR_ 0.9
// shall we use addition/subtraction?
#define _USE_ADDSUB_ 1

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

@ -74,15 +74,15 @@ void sls_engine::checkpoint() {
cooperate("sls");
}
bool sls_engine::full_eval(model & mdl) {
bool sls_engine::full_eval(goal_ref const & g, model & mdl) {
bool res = true;
unsigned sz = m_assertions.size();
unsigned sz = g->size();
for (unsigned i = 0; i < sz && res; i++) {
checkpoint();
expr_ref o(m_manager);
if (!mdl.eval(m_assertions[i], o, true))
if (!mdl.eval(g->form(i), o, true))
exit(ERR_INTERNAL_FATAL);
res = m_manager.is_true(o.get());
@ -93,7 +93,7 @@ bool sls_engine::full_eval(model & mdl) {
return res;
}
double sls_engine::top_score() {
double sls_engine::top_score(goal_ref const & g) {
#if 0
double min = m_tracker.get_score(g->form(0));
unsigned sz = g->size();
@ -108,15 +108,15 @@ double sls_engine::top_score() {
return min;
#else
double top_sum = 0.0;
unsigned sz = m_assertions.size();
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
expr * e = m_assertions[i];
expr * e = g->form(i);
top_sum += m_tracker.get_score(e);
}
TRACE("sls_top", tout << "Score distribution:";
for (unsigned i = 0; i < sz; i++)
tout << " " << m_tracker.get_score(m_assertions[i]);
tout << " " << m_tracker.get_score(g->form(i));
tout << " AVG: " << top_sum / (double)sz << std::endl;);
#if _CACHE_TOP_SCORE_
@ -127,40 +127,40 @@ double sls_engine::top_score() {
#endif
}
double sls_engine::rescore() {
double sls_engine::rescore(goal_ref const & g) {
m_evaluator.update_all();
m_stats.m_full_evals++;
return top_score();
return top_score(g);
}
double sls_engine::serious_score(func_decl * fd, const mpz & new_value) {
double sls_engine::serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value) {
m_evaluator.serious_update(fd, new_value);
m_stats.m_incr_evals++;
#if _CACHE_TOP_SCORE_
return (m_tracker.get_top_sum() / m_assertions.size());
return (m_tracker.get_top_sum() / g->size());
#else
return top_score();
return top_score(g);
#endif
}
double sls_engine::incremental_score(func_decl * fd, const mpz & new_value) {
double sls_engine::incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value) {
m_evaluator.update(fd, new_value);
m_stats.m_incr_evals++;
#if _CACHE_TOP_SCORE_
return (m_tracker.get_top_sum() / m_assertions.size());
return (m_tracker.get_top_sum() / g->size());
#else
return top_score();
return top_score(g);
#endif
}
double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value) {
double sls_engine::incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value) {
#if _EARLY_PRUNE_
m_stats.m_incr_evals++;
if (m_evaluator.update_prune(fd, new_value))
#if _CACHE_TOP_SCORE_
return (m_tracker.get_top_sum() / m_assertions.size());
return (m_tracker.get_top_sum() / g->size());
#else
return top_score();
return top_score(g);
#endif
else
return 0.0;
@ -169,14 +169,17 @@ double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value
#endif
}
double sls_engine::incremental_score_prune_new(goal_ref const & g, func_decl * fd, const mpz & new_value) {
m_stats.m_incr_evals++;
if (m_evaluator.update_prune_new(fd, new_value))
return (m_tracker.get_top_sum() / g->size());
else
return 0.0;
}
// checks whether the score outcome of a given move is better than the previous score
bool sls_engine::what_if(
func_decl * fd,
const unsigned & fd_inx,
const mpz & temp,
double & best_score,
unsigned & best_const,
mpz & best_value) {
bool sls_engine::what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value) {
#ifdef Z3DEBUG
mpz old_value;
@ -184,9 +187,9 @@ bool sls_engine::what_if(
#endif
#if _EARLY_PRUNE_
double r = incremental_score_prune(fd, temp);
double r = incremental_score_prune(g, fd, temp);
#else
double r = incremental_score(fd, temp);
double r = incremental_score(g, fd, temp);
#endif
#ifdef Z3DEBUG
TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) <<
@ -197,6 +200,31 @@ bool sls_engine::what_if(
//if (r >= best_score) {
if (r > best_score) {
m_tracker.reset_equal_scores();
best_score = r;
best_const = fd_inx;
m_mpz_manager.set(best_value, temp);
return true;
}
/*else if (r == best_score) {
if (m_tracker.get_random_uint(16) % m_tracker.inc_equal_scores() == 0)
{
best_score = r;
best_const = fd_inx;
m_mpz_manager.set(best_value, temp);
return true;
}
}*/
return false;
}
bool sls_engine::what_if_new(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value) {
double r = incremental_score_prune_new(g, fd, temp);
if (r >= best_score) {
best_score = r;
best_const = fd_inx;
m_mpz_manager.set(best_value, temp);
@ -207,15 +235,8 @@ bool sls_engine::what_if(
}
// same as what_if, but only applied to the score of a specific atom, not the total score
bool sls_engine::what_if_local(
expr * e,
func_decl * fd,
const unsigned & fd_inx,
const mpz & temp,
double & best_score,
unsigned & best_const,
mpz & best_value)
{
bool sls_engine::what_if_local(expr * e, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value) {
m_evaluator.update(fd, temp);
double r = m_tracker.get_score(e);
if (r >= best_score) {
@ -356,19 +377,13 @@ void sls_engine::mk_random_move(ptr_vector<func_decl> & unsat_constants)
m_mpz_manager.del(new_value);
}
void sls_engine::mk_random_move() {
mk_random_move(m_tracker.get_unsat_constants(m_assertions, m_stats.m_moves));
void sls_engine::mk_random_move(goal_ref const & g) {
mk_random_move(m_tracker.get_unsat_constants(g, m_stats.m_moves));
}
// will use VNS to ignore some possible moves and increase the flips per second
double sls_engine::find_best_move_vns(
ptr_vector<func_decl> & to_evaluate,
double score,
unsigned & best_const,
mpz & best_value,
unsigned & new_bit,
move_type & move)
{
double sls_engine::find_best_move_vns(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;
unsigned bv_sz, max_bv_sz = 0;
double new_score = score;
@ -384,31 +399,31 @@ double sls_engine::find_best_move_vns(
if (!m_mpz_manager.is_even(old_value)) {
// for odd values, try +1
mk_inc(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
move = MV_INC;
}
else {
// for even values, try -1
mk_dec(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
move = MV_DEC;
}
// try inverting
mk_inv(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
move = MV_INV;
// try to flip lsb
mk_flip(srt, old_value, 0, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value)) {
if (what_if(g, fd, i, temp, new_score, best_const, best_value)) {
new_bit = 0;
move = MV_FLIP;
}
}
// reset to what it was before
double check = incremental_score(fd, old_value);
double check = incremental_score(g, fd, old_value);
SASSERT(check == score);
}
@ -430,13 +445,13 @@ double sls_engine::find_best_move_vns(
{
mk_flip(srt, old_value, j, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value)) {
if (what_if(g, fd, i, temp, new_score, best_const, best_value)) {
new_bit = j;
move = MV_FLIP;
}
}
// reset to what it was before
double check = incremental_score(fd, old_value);
double check = incremental_score(g, fd, old_value);
SASSERT(check == score);
}
m_mpz_manager.del(old_value);
@ -444,23 +459,99 @@ double sls_engine::find_best_move_vns(
return new_score;
}
// finds the move that increased score the most. returns best_const = -1, if no increasing move exists.
double sls_engine::find_best_move(
ptr_vector<func_decl> & to_evaluate,
double score,
unsigned & best_const,
mpz & best_value,
unsigned & new_bit,
move_type & move)
double sls_engine::find_best_move_lsb(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;
unsigned bv_sz, max_bv_sz = 0;
double new_score = score;
for (unsigned i = 0; i < to_evaluate.size(); i++) {
func_decl * fd = to_evaluate[i];
sort * srt = fd->get_range();
bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
if (max_bv_sz < bv_sz) max_bv_sz = bv_sz;
m_mpz_manager.set(old_value, m_tracker.get_value(fd));
if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) {
// try inverting
mk_inv(bv_sz, old_value, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
move = MV_INV;
if (!m_mpz_manager.is_even(old_value)) {
// for odd values, try +1
mk_inc(bv_sz, old_value, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
move = MV_INC;
}
else {
// for even values, try -1
mk_dec(bv_sz, old_value, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
move = MV_DEC;
}
// try to flip lsb
mk_flip(srt, old_value, 0, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value)) {
new_bit = 0;
move = MV_FLIP;
}
}
// reset to what it was before
double check = incremental_score(g, fd, old_value);
SASSERT(check == score);
}
for (unsigned j = 1; j < max_bv_sz; j++)
{
for (unsigned i = 0; i < to_evaluate.size(); i++) {
func_decl * fd = to_evaluate[i];
sort * srt = fd->get_range();
bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
m_mpz_manager.set(old_value, m_tracker.get_value(fd));
// What would happen if we flipped bit #j ?
if (j < bv_sz)
{
mk_flip(srt, old_value, j, temp);
if (what_if(g, fd, i, temp, new_score, best_const, best_value)) {
new_bit = j;
move = MV_FLIP;
}
}
// reset to what it was before
double check = incremental_score(g, fd, old_value);
SASSERT(check == score);
}
}
m_mpz_manager.del(old_value);
m_mpz_manager.del(temp);
return new_score;
}
// finds the move that increased score the most. returns best_const = -1, if no increasing move exists.
double sls_engine::find_best_move(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;
#endif
unsigned bv_sz;
#if _INSIST_PERC_
double new_score = m_tracker.get_random_uint(16) % 100 < _INSIST_PERC_ ? 0.0 : score;
#else
double new_score = score;
#endif
for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0; i++) {
m_tracker.reset_equal_scores();
// for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0; i++) {
for (unsigned i = 0; i < to_evaluate.size(); i++) {
// for (unsigned i = m_tracker.get_random_uint(16) % to_evaluate.size(); i != to_evaluate.size(); i = to_evaluate.size()) {
// for (unsigned i = to_evaluate.size(); i-- > 0; ) {
func_decl * fd = to_evaluate[i];
sort * srt = fd->get_range();
bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
@ -470,15 +561,28 @@ double sls_engine::find_best_move(
#if _SKIP_BITS_
for (unsigned j = (i + m_stats.m_moves) % (_SKIP_BITS_ + 1); j < bv_sz && new_score < 1.0; j += (_SKIP_BITS_ + 1)) {
#else
for (unsigned j = 0; j < bv_sz && new_score < 1.0; j++) {
// for (unsigned j = 0; j < bv_sz && new_score < 1.0; j++) {
for (unsigned j = 0; j < bv_sz; j++) {
// for (unsigned j = bv_sz; j-- > 0; ) {
#endif
// What would happen if we flipped bit #i ?
mk_flip(srt, old_value, j, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value)) {
//if (m_tracker.get_random_uint(1))
//if ((move != MV_FLIP) || (new_bit > j))
//{
//if (what_if_new(g, fd, i, temp, new_score, best_const, best_value)) {
// new_bit = j;
// move = MV_FLIP;
//}
//}
//else
//{
if (what_if(g, fd, i, temp, new_score, best_const, best_value)) {
new_bit = j;
move = MV_FLIP;
}
//}
}
if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) {
@ -486,19 +590,22 @@ double sls_engine::find_best_move(
if (!m_mpz_manager.is_even(old_value)) {
// for odd values, try +1
mk_inc(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
//if (m_tracker.get_random_uint(1))
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
move = MV_INC;
}
else {
// for even values, try -1
mk_dec(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
//if (m_tracker.get_random_uint(1))
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
move = MV_DEC;
}
#endif
// try inverting
mk_inv(bv_sz, old_value, temp);
if (what_if(fd, i, temp, new_score, best_const, best_value))
//if (m_tracker.get_random_uint(1))
if (what_if(g, fd, i, temp, new_score, best_const, best_value))
move = MV_INV;
#if _USE_UNARY_MINUS_
@ -528,7 +635,7 @@ double sls_engine::find_best_move(
}
// reset to what it was before
double check = incremental_score(fd, old_value);
double check = incremental_score(g, fd, old_value);
// Andreas: does not hold anymore now that we use top level score caching
//SASSERT(check == score);
}
@ -538,6 +645,50 @@ double sls_engine::find_best_move(
#if _USE_MUL3_
m_mpz_manager.del(temp2);
#endif
if ((new_score == score) && 1)// (m_tracker.get_random_uint(1)))
best_const = -1;
return new_score;
}
// finds the move that increased score the most. returns best_const = -1, if no increasing move exists.
double sls_engine::find_best_move_mc(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value) {
mpz old_value, temp, temp2;
unsigned bv_sz;
double new_score = score;
// for (unsigned i = 0; i < to_evaluate.size() && new_score < 1.0; i++) {
for (unsigned i = 0; i < to_evaluate.size(); i++) {
func_decl * fd = to_evaluate[i];
sort * srt = fd->get_range();
bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
m_mpz_manager.set(old_value, m_tracker.get_value(fd));
if (m_bv_util.is_bv_sort(srt) && bv_sz > 2) {
// for (unsigned j = 0; j < bv_sz && new_score < 1.0; j++) {
for (unsigned j = 0; j < bv_sz; j++) {
mk_flip(srt, old_value, j, temp);
for (unsigned l = 0; l < _VNS_MC_TRIES_ && l < bv_sz / 2; l++)
{
unsigned k = m_tracker.get_random_uint(16) % bv_sz;
while (k == j)
k = m_tracker.get_random_uint(16) % bv_sz;
mk_flip(srt, temp, k, temp2);
what_if(g, fd, i, temp2, new_score, best_const, best_value);
}
}
}
// reset to what it was before
double check = incremental_score(g, fd, old_value);
}
m_mpz_manager.del(old_value);
m_mpz_manager.del(temp);
m_mpz_manager.del(temp2);
return new_score;
}
@ -596,15 +747,15 @@ double sls_engine::find_best_move_local(expr * e, ptr_vector<func_decl> & to_eva
}
// first try of intensification ... does not seem to be efficient
bool sls_engine::handle_plateau()
bool sls_engine::handle_plateau(goal_ref const & g)
{
unsigned sz = m_assertions.size();
unsigned sz = g->size();
#if _BFS_
unsigned pos = m_stats.m_moves % sz;
#else
unsigned pos = m_tracker.get_random_uint(16) % sz;
#endif
expr * e = m_tracker.get_unsat_assertion(sz, pos);
expr * e = m_tracker.get_unsat_assertion(g, sz, pos);
if (!e)
return 0;
@ -658,15 +809,10 @@ bool sls_engine::handle_plateau()
}
// what_if version needed in the context of 2nd intensification try, combining local and global score
bool sls_engine::what_if(
expr * e,
func_decl * fd,
const mpz & temp,
double & best_score,
mpz & best_value,
unsigned i)
{
double global_score = incremental_score(fd, temp);
bool sls_engine::what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz & temp,
double & best_score, mpz & best_value, unsigned i) {
double global_score = incremental_score(g, fd, temp);
double local_score = m_tracker.get_score(e);
double new_score = i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_;
@ -680,7 +826,7 @@ bool sls_engine::what_if(
}
// find_best_move version needed in the context of 2nd intensification try
double sls_engine::find_best_move_local(expr * e, func_decl * fd, mpz & best_value, unsigned i)
double sls_engine::find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i)
{
mpz old_value, temp;
double best_score = 0;
@ -691,7 +837,7 @@ double sls_engine::find_best_move_local(expr * e, func_decl * fd, mpz & best_val
for (unsigned j = 0; j < bv_sz && best_score < 1.0; j++) {
mk_flip(srt, old_value, j, temp);
what_if(e, fd, temp, best_score, best_value, i);
what_if(g, e, fd, temp, best_score, best_value, i);
}
m_mpz_manager.del(old_value);
@ -701,15 +847,15 @@ double sls_engine::find_best_move_local(expr * e, func_decl * fd, mpz & best_val
}
// second try to use intensification ... also not very effective
bool sls_engine::handle_plateau(double old_score)
bool sls_engine::handle_plateau(goal_ref const & g, double old_score)
{
unsigned sz = m_assertions.size();
unsigned sz = g->size();
#if _BFS_
unsigned new_const = m_stats.m_moves % sz;
#else
unsigned new_const = m_tracker.get_random_uint(16) % sz;
#endif
expr * e = m_tracker.get_unsat_assertion(m_assertions, sz, new_const);
expr * e = m_tracker.get_unsat_assertion(g, sz, new_const);
if (!e)
return 0;
@ -726,12 +872,12 @@ bool sls_engine::handle_plateau(double old_score)
for (unsigned i = 1; i <= _INTENSIFICATION_TRIES_; i++)
{
new_score = find_best_move_local(q, fd, new_value, i);
new_score = find_best_move_local(g, q, fd, new_value, i);
m_stats.m_moves++;
m_stats.m_flips++;
global_score = incremental_score(fd, new_value);
global_score = incremental_score(g, fd, new_value);
local_score = m_tracker.get_score(q);
SASSERT(new_score == i * local_score / _INTENSIFICATION_TRIES_ + (_INTENSIFICATION_TRIES_ - i) * global_score / _INTENSIFICATION_TRIES_);
@ -744,7 +890,7 @@ bool sls_engine::handle_plateau(double old_score)
}
// main search loop
lbool sls_engine::search() {
lbool sls_engine::search(goal_ref const & g) {
lbool res = l_undef;
double score = 0.0, old_score = 0.0;
unsigned new_const = (unsigned)-1, new_bit = 0;
@ -752,8 +898,15 @@ lbool sls_engine::search() {
move_type move;
unsigned plateau_cnt = 0;
score = rescore();
unsigned sz = m_assertions.size();
score = rescore(g);
unsigned sz = g->size();
TRACE("sls", tout << "Starting search, initial score = " << std::setprecision(32) << score << std::endl;
tout << "Score distribution:";
for (unsigned i = 0; i < g->size(); i++)
tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i));
tout << " TOP: " << score << std::endl;);
#if _PERC_STICKY_
expr * e = m_tracker.get_unsat_assertion(g, m_stats.m_moves);
#endif
@ -767,9 +920,18 @@ lbool sls_engine::search() {
#else
while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_) {
#endif
//if (m_stats.m_stopwatch.get_current_seconds() > 10.0)
//{printf("Got %f fps and size is %d with avg bw %f\n", m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds(), m_tracker.get_formula_size(), m_tracker.get_avg_bw(g)); exit(0);}
checkpoint();
m_stats.m_moves++;
#if _UCT_FORGET_
//if (m_stats.m_moves % sz == 0)
if (m_stats.m_moves % _UCT_FORGET_ == 0)
m_tracker.uct_forget(g);
#endif
#if _REAL_RS_ || _REAL_PBFS_
//m_tracker.debug_real(g, m_stats.m_moves);
#endif
@ -779,13 +941,14 @@ lbool sls_engine::search() {
if (m_tracker.get_random_uint(16) % 100 >= _PERC_STICKY_ || m_mpz_manager.eq(m_tracker.get_value(e), m_one))
e = m_tracker.get_unsat_assertion(g, m_stats.m_moves);
#else
expr * e = m_tracker.get_unsat_assertion(m_assertions, m_stats.m_moves);
expr * e = m_tracker.get_unsat_assertion(g, m_stats.m_moves);
#endif
if (!e)
{
res = l_true;
goto bailout;
}
//ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants_only(e);
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants_walksat(e);
#else
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants_gsat(g, sz);
@ -818,13 +981,69 @@ lbool sls_engine::search() {
#endif
old_score = score;
new_const = (unsigned)-1;
move = MV_FLIP;
new_bit = 0;
#if _VNS_
score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move);
#else
score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move);
score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move);
#endif
#if _VNS_MC_ > _VNS_REPICK_
#if _VNS_MC_
if (new_const == static_cast<unsigned>(-1))
if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_)
score = find_best_move_mc(g, to_evaluate, score, new_const, new_value);
#endif
#if _VNS_REPICK_
if (new_const == static_cast<unsigned>(-1))
if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_) {
expr * q = m_tracker.get_new_unsat_assertion(g, e);
if (q)
{
ptr_vector<func_decl> & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e);
score = find_best_move(g, to_evaluate2, score, new_const, new_value, new_bit, move);
}
}
#endif
#endif
#if _VNS_MC_ < _VNS_REPICK_
#if _VNS_REPICK_
if (new_const == static_cast<unsigned>(-1))
if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_) {
expr * q = m_tracker.get_new_unsat_assertion(g, e);
if (q)
{
ptr_vector<func_decl> & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e);
score = find_best_move(g, to_evaluate2, score, new_const, new_value, new_bit, move);
}
}
#endif
#if _VNS_MC_
if (new_const == static_cast<unsigned>(-1))
if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_)
score = find_best_move_mc(g, to_evaluate, score, new_const, new_value);
#endif
#endif
#if (_VNS_MC_ == _VNS_REPICK_) && _VNS_MC_ && _VNS_REPICK_
if (new_const == static_cast<unsigned>(-1)) {
if (m_tracker.get_random_uint(16) % 100 < _VNS_PERC_)
score = find_best_move_mc(g, to_evaluate, score, new_const, new_value);
else {
expr * q = m_tracker.get_new_unsat_assertion(g, e);
if (q)
{
ptr_vector<func_decl> & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e);
score = find_best_move(g, to_evaluate2, score, new_const, new_value, new_bit, move);
}
}
}
#endif
if (new_const == static_cast<unsigned>(-1)) {
score = old_score;
plateau_cnt++;
@ -839,25 +1058,52 @@ lbool sls_engine::search() {
mk_random_move(to_evaluate);
else
#endif
#if _REPICK_
m_evaluator.randomize_local(m_assertions, m_stats.m_moves);
#if _REPICK_ == 1
m_evaluator.randomize_local(g, m_stats.m_moves);
#elif _REPICK_ == 2
{
expr * q = m_tracker.get_new_unsat_assertion(g, e);
if (q)
m_evaluator.randomize_local(q);
else
m_evaluator.randomize_local(e);
}
#else
m_evaluator.randomize_local(to_evaluate);
m_evaluator.randomize_local_n(g, to_evaluate);
//m_evaluator.randomize_local(to_evaluate);
#endif
#endif
#if _CACHE_TOP_SCORE_
score = m_tracker.get_top_sum() / m_assertions.size();
score = m_tracker.get_top_sum() / g->size();
#else
score = top_score(g);
#endif
#if _PAWS_
for (unsigned i = 0; i < sz; i++)
{
expr * q = g->form(i);
if (m_tracker.get_random_uint(16) % 100 < _PAWS_)
{
if (m_mpz_manager.eq(m_tracker.get_value(q),m_one))
m_tracker.decrease_weight(q);
}
else
{
if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero))
m_tracker.increase_weight(q);
}
}
#endif
}
else {
func_decl * fd = to_evaluate[new_const];
#if _REAL_RS_ || _REAL_PBFS_
#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_
score = serious_score(g, fd, new_value);
#else
score = incremental_score(fd, new_value);
score = incremental_score(g, fd, new_value);
#endif
}
}
@ -868,20 +1114,19 @@ bailout:
return res;
}
#if 0 // Old code.
// main search loop
lbool sls_engine::search_old() {
lbool sls_engine::search_old(goal_ref const & g) {
lbool res = l_undef;
double score = 0.0, old_score = 0.0;
unsigned new_const = (unsigned)-1, new_bit = 0;
mpz new_value;
move_type move;
score = rescore();
score = rescore(g);
TRACE("sls", tout << "Starting search, initial score = " << std::setprecision(32) << score << std::endl;
tout << "Score distribution:";
for (unsigned i = 0; i < m_assertions.size(); i++)
tout << " " << std::setprecision(3) << m_tracker.get_score(m_assertions[i]);
for (unsigned i = 0; i < g->size(); i++)
tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i));
tout << " TOP: " << score << std::endl;);
unsigned plateau_cnt = 0;
@ -927,7 +1172,7 @@ lbool sls_engine::search_old() {
old_score = score;
new_const = (unsigned)-1;
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(m_assertions, m_stats.m_moves);
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(g, m_stats.m_moves);
if (!to_evaluate.size())
{
res = l_true;
@ -938,22 +1183,22 @@ lbool sls_engine::search_old() {
tout << to_evaluate[i]->get_name() << std::endl;);
#if _VNS_
score = find_best_move_vns(to_evaluate, score, new_const, new_value, new_bit, move);
score = find_best_move_vns(g, to_evaluate, score, new_const, new_value, new_bit, move);
#else
score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move);
score = find_best_move(g, to_evaluate, score, new_const, new_value, new_bit, move);
#endif
if (new_const == static_cast<unsigned>(-1)) {
TRACE("sls", tout << "Local maximum reached; unsatisfied constraints: " << std::endl;
for (unsigned i = 0; i < m_assertions.size(); i++) {
if (!m_mpz_manager.is_one(m_tracker.get_value(m_assertions[i])))
tout << mk_ismt2_pp(m_assertions[i], m_manager) << std::endl;
for (unsigned i = 0; i < g->size(); i++) {
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
tout << mk_ismt2_pp(g->form(i), m_manager) << std::endl;
});
TRACE("sls_max", m_tracker.show_model(tout);
tout << "Scores: " << std::endl;
for (unsigned i = 0; i < m_assertions.size(); i++)
tout << mk_ismt2_pp(m_assertions[i], m_manager) << " ---> " <<
m_tracker.get_score(m_assertions[i]) << std::endl;);
for (unsigned i = 0; i < g->size(); i++)
tout << mk_ismt2_pp(g->form(i), m_manager) << " ---> " <<
m_tracker.get_score(g->form(i)) << std::endl;);
// Andreas: If new_const == -1, shouldn't score = old_score anyway?
score = old_score;
}
@ -991,15 +1236,15 @@ lbool sls_engine::search_old() {
case MV_DIV2: m_stats.m_div2s++; break;
}
#if _REAL_RS_ || _REAL_PBFS_
score = serious_score(fd, new_value);
#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_
score = serious_score(g, fd, new_value);
#else
score = incremental_score(fd, new_value);
score = incremental_score(g, fd, new_value);
#endif
TRACE("sls", tout << "Score distribution:";
for (unsigned i = 0; i < m_assertions.size(); i++)
tout << " " << std::setprecision(3) << m_tracker.get_score(m_assertions[i]);
for (unsigned i = 0; i < g->size(); i++)
tout << " " << std::setprecision(3) << m_tracker.get_score(g->form(i));
tout << " TOP: " << score << std::endl;);
}
@ -1008,8 +1253,8 @@ lbool sls_engine::search_old() {
// score could theoretically be imprecise.
// Andreas: it seems using top level score caching can make the score unprecise also in the other direction!
bool all_true = true;
for (unsigned i = 0; i < m_assertions.size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(m_assertions[i])))
for (unsigned i = 0; i < g->size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
all_true = false;
if (all_true) {
res = l_true; // sat
@ -1040,17 +1285,17 @@ lbool sls_engine::search_old() {
TRACE("sls", tout << "In a plateau (" << plateau_cnt << "/" << m_plateau_limit << "); randomizing locally." << std::endl;);
#if _INTENSIFICATION_
handle_plateau(g, score);
//handle_plateau();
//handle_plateau(g);
#else
m_evaluator.randomize_local(m_assertions, m_stats.m_moves);
m_evaluator.randomize_local(g, m_stats.m_moves);
#endif
//mk_random_move();
score = top_score();
//mk_random_move(g);
score = top_score(g);
if (score >= 1.0) {
bool all_true = true;
for (unsigned i = 0; i < m_assertions.size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(m_assertions[i])))
for (unsigned i = 0; i < g->size() && all_true; i++)
if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
all_true = false;
if (all_true) {
res = l_true; // sat
@ -1067,17 +1312,6 @@ bailout:
return res;
}
#endif
void sls_engine::init_tracker() {
#if _WEIGHT_DIST_ == 4
m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_);
#endif
#if _WEIGHT_TOGGLE_
m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_);
#endif
m_tracker.initialize(m_assertions);
}
void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
if (g->inconsistent()) {
@ -1087,9 +1321,6 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
m_produce_models = g->models_enabled();
for (unsigned i = 0; i < g->size(); i++)
assert_expr(g->form(i));
verbose_stream() << "_BFS_ " << _BFS_ << std::endl;
verbose_stream() << "_FOCUS_ " << _FOCUS_ << std::endl;
verbose_stream() << "_PERC_STICKY_ " << _PERC_STICKY_ << std::endl;
@ -1100,7 +1331,14 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
verbose_stream() << "_TIMELIMIT_ " << _TIMELIMIT_ << std::endl;
verbose_stream() << "_SCORE_AND_AVG_ " << _SCORE_AND_AVG_ << std::endl;
verbose_stream() << "_SCORE_OR_MUL_ " << _SCORE_OR_MUL_ << std::endl;
verbose_stream() << "_PAWS_ " << _PAWS_ << std::endl;
verbose_stream() << "_PAWS_INIT_ " << _PAWS_INIT_ << std::endl;
verbose_stream() << "_VNS_ " << _VNS_ << std::endl;
verbose_stream() << "_VNS_MC_ " << _VNS_MC_ << std::endl;
verbose_stream() << "_VNS_MC_TRIES_ " << _VNS_MC_TRIES_ << std::endl;
verbose_stream() << "_VNS_REPICK_ " << _VNS_REPICK_ << std::endl;
verbose_stream() << "_VNS_PERC_ " << _VNS_PERC_ << std::endl;
verbose_stream() << "_INSIST_PERC_ " << _INSIST_PERC_ << std::endl;
verbose_stream() << "_WEIGHT_DIST_ " << _WEIGHT_DIST_ << std::endl;
verbose_stream() << "_WEIGHT_DIST_FACTOR_ " << std::fixed << std::setprecision(2) << _WEIGHT_DIST_FACTOR_ << std::endl;
verbose_stream() << "_INTENSIFICATION_ " << _INTENSIFICATION_ << std::endl;
@ -1111,6 +1349,8 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
verbose_stream() << "_UCT_CONSTANT_ " << std::fixed << std::setprecision(2) << _UCT_CONSTANT_ << std::endl;
verbose_stream() << "_UCT_RESET_ " << _UCT_RESET_ << std::endl;
verbose_stream() << "_UCT_INIT_ " << _UCT_INIT_ << std::endl;
verbose_stream() << "_UCT_FORGET_ " << _UCT_FORGET_ << std::endl;
verbose_stream() << "_UCT_FORGET_FACTOR_ " << std::fixed << std::setprecision(2) << _UCT_FORGET_FACTOR_ << std::endl;
verbose_stream() << "_PROBABILISTIC_UCT_ " << _PROBABILISTIC_UCT_ << std::endl;
verbose_stream() << "_UCT_EPS_ " << std::fixed << std::setprecision(4) << _UCT_EPS_ << std::endl;
verbose_stream() << "_USE_ADDSUB_ " << _USE_ADDSUB_ << std::endl;
@ -1127,7 +1367,34 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl;
verbose_stream() << "_CACHE_TOP_SCORE_ " << _CACHE_TOP_SCORE_ << std::endl;
lbool res = operator()();
#if _WEIGHT_DIST_ == 4
m_tracker.set_weight_dist_factor(m_stats.m_stopwatch.get_current_seconds() / _TIMELIMIT_);
#endif
#if _WEIGHT_TOGGLE_
m_tracker.set_weight_dist_factor(_WEIGHT_DIST_FACTOR_);
#endif
m_tracker.initialize(g);
lbool res = l_undef;
m_restart_limit = _RESTART_LIMIT_;
do {
checkpoint();
report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts);
res = search(g);
if (res == l_undef)
{
#if _RESTART_INIT_
m_tracker.randomize(g);
#else
m_tracker.reset(g);
#endif
}
} while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && res != l_true && m_stats.m_restarts++ < m_max_restarts);
verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " time: " << std::fixed << std::setprecision(2) << m_stats.m_stopwatch.get_current_seconds() << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl;
if (res == l_true) {
report_tactic_progress("Number of flips:", m_stats.m_moves);
@ -1149,38 +1416,13 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
mc = 0;
}
lbool sls_engine::operator()() {
init_tracker();
lbool res = l_undef;
m_restart_limit = _RESTART_LIMIT_;
do {
checkpoint();
report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts);
res = search();
if (res == l_undef)
{
#if _RESTART_INIT_
m_tracker.randomize();
#else
m_tracker.reset(m_assertions);
#endif
}
} while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && res != l_true && m_stats.m_restarts++ < m_max_restarts);
verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " time: " << std::fixed << std::setprecision(2) << m_stats.m_stopwatch.get_current_seconds() << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl;
return res;
}
unsigned sls_engine::check_restart(unsigned curr_value)
{
if (curr_value > m_restart_limit)
{
#if _RESTART_SCHEME_ == 4
#if _RESTART_SCHEME_ == 5
m_restart_limit += (unsigned)(_RESTART_LIMIT_ * pow(_RESTART_CONST_ARMIN_, m_stats.m_restarts));
#elif _RESTART_SCHEME_ == 4
m_restart_limit += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? _RESTART_LIMIT_ : (_RESTART_LIMIT_ * m_stats.m_restarts + 1);
#elif _RESTART_SCHEME_ == 3
m_restart_limit += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * _RESTART_LIMIT_;
@ -1188,9 +1430,11 @@ unsigned sls_engine::check_restart(unsigned curr_value)
m_restart_limit += get_luby(m_stats.m_restarts + 1) * _RESTART_LIMIT_;
#elif _RESTART_SCHEME_ == 1
if (m_stats.m_restarts & 1)
//if (m_stats.m_restarts % 3 == 2)
m_restart_limit += _RESTART_LIMIT_;
else
m_restart_limit += (2 << (m_stats.m_restarts >> 1)) * _RESTART_LIMIT_;
//m_restart_limit += (2 << (m_stats.m_restarts / 3)) * _RESTART_LIMIT_;
#else
m_restart_limit += _RESTART_LIMIT_;
#endif

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

@ -22,7 +22,6 @@ Notes:
#include"stopwatch.h"
#include"lbool.h"
#include"model_converter.h"
#include"goal.h"
#include"sls_compilation_settings.h"
#include"sls_tracker.h"
@ -72,7 +71,6 @@ protected:
bv_util m_bv_util;
sls_tracker m_tracker;
sls_evaluator m_evaluator;
ptr_vector<expr> m_assertions;
unsigned m_restart_limit;
unsigned m_max_restarts;
@ -94,12 +92,11 @@ public:
void updt_params(params_ref const & _p);
void assert_expr(expr * e) { m_assertions.push_back(e); }
stats const & get_stats(void) { return m_stats; }
void reset_statistics(void) { m_stats.reset(); }
bool full_eval(model & mdl);
bool full_eval(goal_ref const & g, model & mdl);
void mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result);
void mk_mul2(unsigned bv_sz, const mpz & old_value, mpz & result);
@ -109,44 +106,62 @@ public:
void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted);
void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped);
void init_tracker(void);
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);
lbool search(void);
double find_best_move_lsb(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double find_best_move_mc(goal_ref const & g, ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value);
double find_best_move_local(expr * e, ptr_vector<func_decl> & to_evaluate,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
bool what_if(goal_ref const & g, expr * e, func_decl * fd, const mpz & temp,
double & best_score, mpz & best_value, unsigned i);
double find_best_move_local(goal_ref const & g, expr * e, func_decl * fd, mpz & best_value, unsigned i);
lbool search(goal_ref const & g);
lbool operator()();
void operator()(goal_ref const & g, model_converter_ref & mc);
protected:
void checkpoint();
lbool search_old(goal_ref const & g);
double get_restart_armin(unsigned cnt_restarts);
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
bool what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value);
bool what_if(expr * e, func_decl * fd, const mpz & temp,
double & best_score, mpz & best_value, unsigned i);
bool what_if_new(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value);
double incremental_score_prune_new(goal_ref const & g, func_decl * fd, const mpz & new_value);
bool what_if_local(expr * e, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value);
double top_score();
double rescore();
double serious_score(func_decl * fd, const mpz & new_value);
double incremental_score(func_decl * fd, const mpz & new_value);
double top_score(goal_ref const & g);
double rescore(goal_ref const & g);
double serious_score(goal_ref const & g, func_decl * fd, const mpz & new_value);
double incremental_score(goal_ref const & g, func_decl * fd, const mpz & new_value);
#if _EARLY_PRUNE_
double incremental_score_prune(func_decl * fd, const mpz & new_value);
double incremental_score_prune(goal_ref const & g, func_decl * fd, const mpz & new_value);
#endif
double find_best_move(ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double find_best_move_local(expr * e, func_decl * fd, mpz & best_value, unsigned i);
double find_best_move_local(expr * e, ptr_vector<func_decl> & to_evaluate,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
double find_best_move_vns(ptr_vector<func_decl> & to_evaluate, double score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move);
void mk_random_move(ptr_vector<func_decl> & unsat_constants);
void mk_random_move();
bool handle_plateau(void);
bool handle_plateau(double old_score);
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);
void mk_random_move(ptr_vector<func_decl> & unsat_constants);
void mk_random_move(goal_ref const & g);
bool handle_plateau(goal_ref const & g);
bool handle_plateau(goal_ref const & g, double old_score);
inline unsigned check_restart(unsigned curr_value);
};

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

@ -575,7 +575,7 @@ public:
#if _CACHE_TOP_SCORE_
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
#endif
m_tracker.set_score(cur, new_score);
m_tracker.set_score_prune(cur, new_score);
@ -584,12 +584,13 @@ public:
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
#else
m_tracker.set_score(cur, m_tracker.score(cur));
#endif
#endif
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
for (unsigned j = 0; j < ups.size(); j++) {
@ -634,7 +635,7 @@ public:
#if _CACHE_TOP_SCORE_
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
#endif
m_tracker.set_score(cur, new_score);
m_tracker.set_score_prune(cur, new_score);
@ -643,7 +644,7 @@ public:
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
#else
m_tracker.set_score(cur, m_tracker.score(cur));
@ -683,7 +684,7 @@ public:
m_traversal_stack[cur_depth].push_back(ep);
if (cur_depth > max_depth) max_depth = cur_depth;
}
#if _REAL_RS_ || _REAL_PBFS_
#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_
run_serious_update(max_depth);
#else
run_update(max_depth);
@ -729,14 +730,16 @@ public:
#if _CACHE_TOP_SCORE_
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
#endif
prune_score = m_tracker.get_score_prune(cur);
m_tracker.set_score(cur, new_score);
if ((new_score > prune_score) && (m_tracker.has_pos_occ(cur)))
//if ((new_score >= prune_score) && (m_tracker.has_pos_occ(cur)))
pot_benefits = 1;
if ((new_score <= prune_score) && (m_tracker.has_neg_occ(cur)))
//if ((new_score < prune_score) && (m_tracker.has_neg_occ(cur)))
pot_benefits = 1;
if (m_tracker.has_uplinks(cur)) {
@ -771,7 +774,7 @@ public:
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(new_score, m_tracker.get_score(cur));
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
#else
m_tracker.set_score(cur, m_tracker.score(cur));
@ -858,6 +861,104 @@ public:
}
#endif
unsigned run_update_bool_prune_new(unsigned cur_depth) {
expr_fast_mark1 visited;
double prune_score, new_score;
unsigned pot_benefits = 0;
SASSERT(cur_depth < m_traversal_stack_bool.size());
ptr_vector<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);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
prune_score = m_tracker.get_score_prune(cur);
m_tracker.set_score(cur, new_score);
if ((new_score >= prune_score) && (m_tracker.has_pos_occ(cur)))
pot_benefits = 1;
if ((new_score < prune_score) && (m_tracker.has_neg_occ(cur)))
pot_benefits = 1;
if (m_tracker.has_uplinks(cur)) {
ptr_vector<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);
}
}
}
else
{
}
}
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];
new_score = m_tracker.score(cur);
//if (!m_tracker.has_uplinks(cur))
if (m_tracker.is_top_expr(cur))
m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur));
m_tracker.set_score(cur, new_score);
if (m_tracker.has_uplinks(cur)) {
ptr_vector<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;
}
unsigned update_prune_new(func_decl * fd, const mpz & new_value) {
m_tracker.set_value(fd, new_value);
expr * ep = m_tracker.get_entry_point(fd);
unsigned cur_depth = m_tracker.get_distance(ep);
if (m_traversal_stack_bool.size() <= cur_depth)
m_traversal_stack_bool.resize(cur_depth+1);
if (m_traversal_stack.size() <= cur_depth)
m_traversal_stack.resize(cur_depth+1);
if (m_manager.is_bool(ep))
m_traversal_stack_bool[cur_depth].push_back(ep);
else
{
m_traversal_stack[cur_depth].push_back(ep);
run_update_prune(cur_depth);
}
return run_update_bool_prune_new(cur_depth);
}
void randomize_local(ptr_vector<func_decl> & unsat_constants) {
// Randomize _all_ candidates:
@ -901,7 +1002,7 @@ public:
mpz temp = m_tracker.get_random(fd->get_range());
#endif
#if _REAL_RS_ || _REAL_PBFS_
#if _REAL_RS_ || _REAL_PBFS_ || _PAWS_
serious_update(fd, temp);
#else
update(fd, temp);
@ -922,8 +1023,35 @@ public:
randomize_local(m_tracker.get_constants(e));
}
void randomize_local(ptr_vector<expr> const & as, unsigned int flip) {
randomize_local(m_tracker.get_unsat_constants(as, flip));
void randomize_local(goal_ref const & g, unsigned int flip) {
randomize_local(m_tracker.get_unsat_constants(g, flip));
}
void randomize_local_n(goal_ref const & g, ptr_vector<func_decl> & unsat_constants) {
unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size();
func_decl * fd = unsat_constants[r];
sort * srt = fd->get_range();
unsigned bv_sz = m_manager.is_bool(srt) ? 1 : m_bv_util.get_bv_size(srt);
mpz max_val = m_tracker.get_random(srt);
update(fd, max_val);
double max_score = m_tracker.get_top_sum() / g->size();
mpz temp_val;
double temp_score;
for (unsigned i = 1; i < 2; i++)
//for (unsigned i = 1; i < bv_sz; i++)
{
m_mpz_manager.set(temp_val, m_tracker.get_random(srt));
update(fd, temp_val);
temp_score = m_tracker.get_top_sum() / g->size();
if (temp_score > max_score)
{
m_mpz_manager.set(max_val, temp_val);
max_score = temp_score;
}
}
update(fd, max_val);
m_mpz_manager.del(temp_val);
m_mpz_manager.del(max_val);
}
};

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

@ -1509,14 +1509,14 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) {
mk_max_bv_sharing_tactic(m),
// Andreas: It would be cool to get rid of shared top level assertions but which simplification is doing this?
//mk_ctx_simplify_tactic(m, ctx_p),
// Andreas: This one at least eliminates top level duplicates ...
// Andreas: This one at least eliminates top level duplicates ... but has very bad effects on performance!
//mk_simplify_tactic(m),
// Andreas: How does a NNF actually look like? Can it contain ITE operators?
mk_nnf_tactic(m, p));
}
tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {
tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m));
// tactic * t = and_then(mk_simplify_tactic(m), mk_nnf_tactic(m, p), mk_sls_tactic(m));
t->updt_params(p);
return t;
}

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

@ -20,9 +20,7 @@ Notes:
#ifndef _SLS_TRACKER_H_
#define _SLS_TRACKER_H_
#include"for_each_expr.h"
#include"ast_smt2_pp.h"
#include"bv_decl_plugin.h"
#include"goal.h"
#include"model.h"
#include"sls_compilation_settings.h"
@ -88,12 +86,17 @@ private:
obj_map<expr, unsigned> m_where_false;
expr** m_list_false;
#endif
#if _PAWS_
obj_map<expr, unsigned> m_weights;
//obj_map<expr, double> m_weights;
#endif
#if _CACHE_TOP_SCORE_
double m_top_sum;
#endif
#if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_
double m_weight_dist_factor;
#endif
unsigned m_equal_scores;
public:
sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) :
@ -113,15 +116,52 @@ public:
m_mpz_manager.del(m_two);
}
unsigned get_formula_size() {
return m_scores.size();
}
double get_avg_bw(goal_ref const & g) {
double sum = 0.0;
unsigned count = 0;
for (unsigned i = 0; i < g->size(); i++)
{
m_temp_constants.reset();
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(g->form(i));
unsigned sz = this_decls.size();
for (unsigned i = 0; i < sz; i++) {
func_decl * fd = this_decls[i];
m_temp_constants.push_back(fd);
sort * srt = fd->get_range();
sum += (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
count++;
}
}
return sum / count;
}
#if _WEIGHT_DIST_ == 4 || _WEIGHT_TOGGLE_
inline void set_weight_dist_factor(double val) {
m_weight_dist_factor = val;
}
#endif
void reset_equal_scores() {
m_equal_scores = 1;
}
unsigned inc_equal_scores() {
return ++m_equal_scores;
}
#if _CACHE_TOP_SCORE_
inline void adapt_top_sum(double add, double sub) {
inline void adapt_top_sum(expr * e, double add, double sub) {
#if _PAWS_
m_top_sum += m_weights.find(e) * (add - sub);
#else
m_top_sum += add - sub;
#endif
}
inline void set_top_sum(double new_score) {
@ -278,19 +318,21 @@ public:
}
#endif
void uct_forget(ptr_vector<expr> & as) {
#if _UCT_
void uct_forget(goal_ref const & g) {
expr * e;
unsigned touched_old, touched_new;
for (unsigned i = 0; i < as.size(); i++)
for (unsigned i = 0; i < g->size(); i++)
{
e = as[i];
e = g->form(i);
touched_old = m_scores.find(e).touched;
touched_new = (unsigned)((touched_old - 1) * _UCT_FORGET_FACTOR_ + 1);
m_scores.find(e).touched = touched_new;
m_touched += touched_new - touched_old;
}
}
#endif
void initialize(app * n) {
// Build score table
@ -367,12 +409,12 @@ public:
}
};
void calculate_expr_distances(ptr_vector<expr> const & as) {
void calculate_expr_distances(goal_ref const & g) {
// precondition: m_scores is set up.
unsigned sz = as.size();
unsigned sz = g->size();
ptr_vector<app> stack;
for (unsigned i = 0; i < sz; i++)
stack.push_back(to_app(as[i]));
stack.push_back(to_app(g->form(i)));
while (!stack.empty()) {
app * cur = stack.back();
stack.pop_back();
@ -420,12 +462,12 @@ public:
quick_for_each_expr(ffd_proc, visited, e);
}
void initialize(ptr_vector<expr> const & as) {
void initialize(goal_ref const & g) {
init_proc proc(m_manager, *this);
expr_mark visited;
unsigned sz = as.size();
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
expr * e = as[i];
expr * e = g->form(i);
if (!m_top_expr.contains(e))
m_top_expr.insert(e);
else
@ -440,7 +482,7 @@ public:
visited.reset();
for (unsigned i = 0; i < sz; i++) {
expr * e = as[i];
expr * e = g->form(i);
// Andreas: Maybe not fully correct.
#if _FOCUS_ == 2 || _INTENSIFICATION_
initialize_recursive(e);
@ -452,7 +494,7 @@ public:
quick_for_each_expr(ffd_proc, visited, e);
}
calculate_expr_distances(as);
calculate_expr_distances(g);
TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); );
@ -465,16 +507,49 @@ public:
//}
#endif
#if _PAWS_
for (unsigned i = 0; i < sz; i++)
{
expr * e = g->form(i);
if (!m_weights.contains(e))
m_weights.insert(e, _PAWS_INIT_);
}
#endif
#if _EARLY_PRUNE_
for (unsigned i = 0; i < sz; i++)
setup_occs(as[i]);
setup_occs(g->form(i));
#endif
#if _UCT_
m_touched = _UCT_INIT_ ? as.size() : 1;
m_touched = _UCT_INIT_ ? g->size() : 1;
#endif
}
#if _PAWS_
void increase_weight(expr * e)
{
//printf("Increasing %d to", m_weights.find(e));
m_weights.find(e)++;
//m_weights.find(e) *= 1.1;
//printf(" %d\n", m_weights.find(e));
}
void decrease_weight(expr * e)
{
unsigned old_weight = m_weights.find(e);
m_weights.find(e) = old_weight > _PAWS_INIT_ ? old_weight - 1 : _PAWS_INIT_;
//m_weights.find(e) = old_weight > 1.1 ? old_weight / 1.1 : 1;
//printf("Decreasing %d to %d\n", old_weight, m_weights.find(e));
}
unsigned get_weight(expr * e)
//double get_weight(expr * e)
{
return m_weights.find(e);
}
#endif
#if _REAL_RS_ || _REAL_PBFS_
void make_assertion(expr * e)
{
@ -608,7 +683,7 @@ public:
NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now.
}
void randomize(ptr_vector<expr> const & as) {
void randomize(goal_ref const & g) {
TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
@ -622,13 +697,13 @@ public:
TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); );
#if _UCT_RESET_
m_touched = _UCT_INIT_ ? as.size() : 1;
for (unsigned i = 0; i < as.size(); i++)
m_scores.find(as[i]).touched = 1;
m_touched = _UCT_INIT_ ? g->size() : 1;
for (unsigned i = 0; i < g->size(); i++)
m_scores.find(g->form(i)).touched = 1;
#endif
}
void reset(ptr_vector<expr> const & as) {
void reset(goal_ref const & g) {
TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
@ -638,9 +713,9 @@ public:
}
#if _UCT_RESET_
m_touched = _UCT_INIT_ ? as.size() : 1;
for (unsigned i = 0; i < as.size(); i++)
m_scores.find(as[i]).touched = 1;
m_touched = _UCT_INIT_ ? g->size() : 1;
for (unsigned i = 0; i < g->size(); i++)
m_scores.find(g->form(i)).touched = 1;
#endif
}
@ -765,6 +840,7 @@ public:
const mpz & v1 = get_value(arg1);
if (negated) {
//res = (m_mpz_manager.eq(v0, v1)) ? 0.5 * (m_bv_util.get_bv_size(arg0) - 1.0) / m_bv_util.get_bv_size(arg0) : 1.0;
res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0;
TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " <<
m_mpz_manager.to_string(v1) << std::endl; );
@ -811,39 +887,208 @@ public:
SASSERT(a->get_num_args() == 2);
const mpz & x = get_value(a->get_arg(0));
const mpz & y = get_value(a->get_arg(1));
unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]);
int bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]);
if (negated) {
if (m_mpz_manager.gt(x, y))
{
/*mpz diff;
m_mpz_manager.sub(x, y, diff);
m_mpz_manager.inc(diff);
rational n(diff);
n /= rational(m_powers(bv_sz));
double dbl = n.get_double();
// In extreme cases, n is 0.9999 but to_double returns something > 1.0
m_mpz_manager.del(diff);
res = 1.0 + 0.5 * dbl;*/
res = 1.0;
}
else {
//res = (bv_sz - 1.0) / bv_sz;
/* mpz x_copy, y_copy;
m_mpz_manager.set(x_copy, x);
m_mpz_manager.set(y_copy, y);
unsigned lower_gt = 0;
unsigned curr_gt = 0;
int last_pos = -1;
for (int i = 0; i < bv_sz; i++)
{
if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy))
{
lower_gt = curr_gt;
curr_gt = 1;
last_pos = i;
}
else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy))
{
lower_gt = curr_gt;
curr_gt = 0;
last_pos = i;
}
m_mpz_manager.machine_div(x_copy, m_two, x_copy);
m_mpz_manager.machine_div(y_copy, m_two, y_copy);
}
res = (double)(bv_sz - last_pos - 1 + 2 * lower_gt) / (double)(bv_sz + 2);
m_mpz_manager.del(x_copy);
m_mpz_manager.del(y_copy);*/
#if 1
mpz diff;
m_mpz_manager.sub(y, x, diff);
m_mpz_manager.inc(diff);
rational n(diff);
n /= rational(m_powers(bv_sz));
double dbl = 1.0 - n.get_double();
// In extreme cases, n is 0.9999 but to_double returns something > 1.0
res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl;
//res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
m_mpz_manager.del(diff);
#endif
}
}
else {
if (m_mpz_manager.le(x, y))
{
/*mpz diff;
m_mpz_manager.sub(y, x, diff);
m_mpz_manager.inc(diff);
rational n(diff);
n /= rational(m_powers(bv_sz));
double dbl = n.get_double();
// In extreme cases, n is 0.9999 but to_double returns something > 1.0
res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
m_mpz_manager.del(diff);
}
}
else {
if (m_mpz_manager.le(x, y))
res = 1.0 + 0.5 * dbl;*/
res = 1.0;
}
else {
//res = (bv_sz - 1.0) / bv_sz;
/* mpz x_copy, y_copy;
m_mpz_manager.set(x_copy, x);
m_mpz_manager.set(y_copy, y);
unsigned lower_le = 1;
unsigned curr_le = 1;
int last_pos = -1;
for (int i = 0; i < bv_sz; i++)
{
if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy))
{
lower_le = curr_le;
curr_le = 0;
last_pos = i;
}
else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy))
{
lower_le = curr_le;
curr_le = 1;
last_pos = i;
}
m_mpz_manager.machine_div(x_copy, m_two, x_copy);
m_mpz_manager.machine_div(y_copy, m_two, y_copy);
}
res = (double)(bv_sz - last_pos - 1 + 2 * lower_le) / (double)(bv_sz + 2);*/
#if 1
mpz diff;
m_mpz_manager.sub(x, y, diff);
rational n(diff);
n /= rational(m_powers(bv_sz));
double dbl = n.get_double();
double dbl = 1.0 - n.get_double();
res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl;
m_mpz_manager.del(diff);
#endif
}
}
TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " <<
m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; );
}
/* else if (m_bv_util.is_bv_sle(n)) { // x <= y
app * a = to_app(n);
SASSERT(a->get_num_args() == 2);
const mpz & x = get_value(a->get_arg(0));
const mpz & y = get_value(a->get_arg(1));
int bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]);
mpz x_unsigned;
mpz y_unsigned;
const mpz & p = m_powers(bv_sz);
const mpz & p_half = m_powers(bv_sz-1);
if (x >= p_half) { m_mpz_manager.sub(x, p, x_unsigned); }
if (y >= p_half) { m_mpz_manager.sub(y, p, y_unsigned); }
if (negated) {
if (x_unsigned > y_unsigned)
res = 1.0;
else {
mpz x_copy, y_copy;
m_mpz_manager.set(x_copy, x);
m_mpz_manager.set(y_copy, y);
unsigned lower_gt = 0;
unsigned curr_gt = 0;
int last_pos = -1;
for (int i = 0; i < bv_sz; i++)
{
if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy))
{
lower_gt = curr_gt;
curr_gt = 1;
last_pos = i;
}
else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy))
{
lower_gt = curr_gt;
curr_gt = 0;
last_pos = i;
}
m_mpz_manager.machine_div(x_copy, m_two, x_copy);
m_mpz_manager.machine_div(y_copy, m_two, y_copy);
}
res = (double)(bv_sz - last_pos - 1 + 2 * lower_gt) / (double)(bv_sz + 2);
m_mpz_manager.del(x_copy);
m_mpz_manager.del(y_copy);
}
}
else {
if (x_unsigned <= y_unsigned)
res = 1.0;
else {
mpz x_copy, y_copy;
m_mpz_manager.set(x_copy, x);
m_mpz_manager.set(y_copy, y);
unsigned lower_le = 1;
unsigned curr_le = 1;
int last_pos = -1;
for (int i = 0; i < bv_sz; i++)
{
if (m_mpz_manager.is_odd(x_copy) && m_mpz_manager.is_even(y_copy))
{
lower_le = curr_le;
curr_le = 0;
last_pos = i;
}
else if (m_mpz_manager.is_even(x_copy) && m_mpz_manager.is_odd(y_copy))
{
lower_le = curr_le;
curr_le = 1;
last_pos = i;
}
m_mpz_manager.machine_div(x_copy, m_two, x_copy);
m_mpz_manager.machine_div(y_copy, m_two, y_copy);
}
res = (double)(bv_sz - last_pos - 1 + 2 * lower_le) / (double)(bv_sz + 2);
}
}
TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " <<
m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; );
m_mpz_manager.del(x_unsigned);
m_mpz_manager.del(y_unsigned);
}*/
else if (m_bv_util.is_bv_sle(n)) { // x <= y
app * a = to_app(n);
SASSERT(a->get_num_args() == 2);
@ -857,31 +1102,61 @@ public:
if (negated) {
if (x > y)
{
/*mpz diff;
m_mpz_manager.sub(x, y, diff);
m_mpz_manager.inc(diff);
rational n(diff);
n /= rational(m_powers(bv_sz));
double dbl = n.get_double();
// In extreme cases, n is 0.9999 but to_double returns something > 1.0
m_mpz_manager.del(diff);
res = 1.0 + 0.5 * dbl;*/
res = 1.0;
}
else {
//res = (bv_sz - 1.0) / bv_sz;
#if 1
mpz diff;
m_mpz_manager.sub(y, x, diff);
m_mpz_manager.inc(diff);
rational n(diff);
n /= p;
double dbl = n.get_double();
res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
double dbl = 1.0 - n.get_double();
//res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl;
m_mpz_manager.del(diff);
#endif
}
TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " <<
m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; );
}
else {
if (x <= y)
{
/*mpz diff;
m_mpz_manager.sub(y, x, diff);
m_mpz_manager.inc(diff);
rational n(diff);
n /= rational(m_powers(bv_sz));
double dbl = n.get_double();
// In extreme cases, n is 0.9999 but to_double returns something > 1.0
m_mpz_manager.del(diff);
res = 1.0 + 0.5 * dbl;*/
res = 1.0;
}
else {
//res = (bv_sz - 1.0) / bv_sz;
#if 1
mpz diff;
m_mpz_manager.sub(x, y, diff);
SASSERT(!m_mpz_manager.is_neg(diff));
rational n(diff);
n /= p;
double dbl = n.get_double();
double dbl = 1.0 - n.get_double();
res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl;
m_mpz_manager.del(diff);
#endif
}
TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " <<
m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; );
@ -1031,13 +1306,13 @@ public:
return m_temp_constants;
}
ptr_vector<func_decl> & get_unsat_constants_gsat(ptr_vector<expr> const & as, unsigned sz) {
ptr_vector<func_decl> & get_unsat_constants_gsat(goal_ref const & g, unsigned sz) {
if (sz == 1)
return get_constants();
m_temp_constants.reset();
for (unsigned i = 0; i < sz; i++) {
expr * q = as[i];
expr * q = g->form(i);
if (m_mpz_manager.eq(get_value(q), m_one))
continue;
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(q);
@ -1051,22 +1326,22 @@ public:
return m_temp_constants;
}
expr * get_unsat_assertion(ptr_vector<expr> const & as, unsigned sz, unsigned int pos) {
expr * get_unsat_assertion(goal_ref const & g, unsigned sz, unsigned int pos) {
for (unsigned i = pos; i < sz; i++) {
expr * q = as[i];
expr * q = g->form(i);
if (m_mpz_manager.neq(get_value(q), m_one))
return q;
}
for (unsigned i = 0; i < pos; i++) {
expr * q = as[i];
expr * q = g->form(i);
if (m_mpz_manager.neq(get_value(q), m_one))
return q;
}
return 0;
}
ptr_vector<func_decl> & get_unsat_constants_walksat(ptr_vector<expr> const & as, unsigned sz, unsigned int pos) {
expr * q = get_unsat_assertion(as, 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;
@ -1143,20 +1418,66 @@ public:
return m_temp_constants;
}
ptr_vector<func_decl> & get_unsat_constants_crsat(ptr_vector<expr> const & as, unsigned sz, unsigned int pos) {
expr * q = get_unsat_assertion(as, sz, pos);
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 go_deeper(q);
}
ptr_vector<func_decl> & get_unsat_constants(ptr_vector<expr> const & as, unsigned int flip) {
unsigned sz = as.size();
void go_deeper_only(expr * e) {
//if (m_manager.is_bool(e)) {
if (m_manager.is_and(e)) {
app * a = to_app(e);
expr * const * args = a->get_args();
unsigned int sz = a->get_num_args();
unsigned cnt_unsat = 0, pos = -1;
for (unsigned int i = 0; i < sz; i++) {
expr * q = args[i];
if (m_mpz_manager.neq(get_value(q), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i;
//if (m_mpz_manager.neq(get_value(q), m_one)) go_deeper(q);
}
go_deeper(args[pos]);
}
else if (m_manager.is_or(e)) {
app * a = to_app(e);
expr * const * args = a->get_args();
unsigned int sz = a->get_num_args();
for (unsigned int i = 0; i < sz; i++) {
expr * q = args[i];
go_deeper(q);
}
}
//}
else
{
ptr_vector<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);
}
}
}
ptr_vector<func_decl> & get_unsat_constants_only(expr * e) {
if (e && !m_temp_constants.size())
go_deeper_only(e);
return m_temp_constants;
}
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(as[0]), m_one))
if (m_mpz_manager.eq(get_value(g->form(0)), m_one))
{
m_temp_constants.reset();
return m_temp_constants;
}
else
return get_constants();
}
@ -1174,6 +1495,7 @@ public:
{
expr * e = g->form(i);
vscore = m_scores.find(e);
#if _PROBABILISTIC_UCT_ == 2
double q = vscore.score * vscore.score;
#else
@ -1203,7 +1525,7 @@ public:
#else
double max = -1.0;
for (unsigned i = 0; i < sz; i++) {
expr * e = as[i];
expr * e = g->form(i);
// for (unsigned i = 0; i < m_where_false.size(); i++) {
// expr * e = m_list_false[i];
vscore = m_scores.find(e);
@ -1221,12 +1543,12 @@ public:
return m_temp_constants;
#if _UCT_ == 1 || _UCT_ == 3
m_scores.find(as[pos]).touched++;
m_scores.find(g->form(pos)).touched++;
m_touched++;
#elif _UCT_ == 2
m_scores.find(as[pos]).touched = flip;
m_scores.find(g->form(pos)).touched = flip;
#endif
expr * e = as[pos];
expr * e = g->form(pos);
// expr * e = m_list_false[pos];
#elif _BFS_ == 3
@ -1304,12 +1626,15 @@ public:
}
}
expr * get_unsat_assertion(goal_ref const & g, unsigned int flip) {
unsigned sz = g->size();
expr * get_unsat_assertion(ptr_vector<expr> const & as, unsigned int flip) {
unsigned sz = as.size();
if (sz == 1)
return as[0];
if (sz == 1) {
if (m_mpz_manager.eq(get_value(g->form(0)), m_zero))
return g->form(0);
else
return 0;
}
m_temp_constants.reset();
#if _FOCUS_ == 1
@ -1353,7 +1678,7 @@ public:
#else
double max = -1.0;
for (unsigned i = 0; i < sz; i++) {
expr * e = as[i];
expr * e = g->form(i);
// for (unsigned i = 0; i < m_where_false.size(); i++) {
// expr * e = m_list_false[i];
vscore = m_scores.find(e);
@ -1371,13 +1696,13 @@ public:
return 0;
#if _UCT_ == 1 || _UCT_ == 3
m_scores.find(as[pos]).touched++;
m_scores.find(g->form(pos)).touched++;
m_touched++;
#elif _UCT_ == 2
m_scores.find(g->form(pos)).touched = flip;
#endif
// return m_list_false[pos];
return as[pos];
return g->form(pos);
#elif _BFS_ == 3
unsigned int pos = -1;
@ -1431,7 +1756,7 @@ public:
unsigned int pos = get_random_uint(16) % sz;
return get_unsat_assertion(g, sz, pos);
#endif
return as[pos];
return g->form(pos);
#elif _FOCUS_ == 2
#if _BFS_
unsigned int pos = flip % sz;
@ -1441,6 +1766,23 @@ public:
return get_unsat_constants_crsat(g, sz, pos);
#endif
}
expr * get_new_unsat_assertion(goal_ref const & g, expr * e) {
unsigned sz = g->size();
if (sz == 1)
return 0;
m_temp_constants.reset();
unsigned cnt_unsat = 0, pos = -1;
for (unsigned i = 0; i < sz; i++)
if (m_mpz_manager.neq(get_value(g->form(i)), m_one) && (get_random_uint(16) % ++cnt_unsat == 0) && (g->form(i) != e)) pos = i;
if (pos == static_cast<unsigned>(-1))
return 0;
return g->form(pos);
}
};
#endif

28
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -28,6 +28,8 @@ Notes:
#include"bv_size_reduction_tactic.h"
#include"aig_tactic.h"
#include"sat_tactic.h"
//#include"nnf_tactic.h"
//#include"sls_tactic.h"
#define MEMLIMIT 300
@ -93,6 +95,32 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
mk_sat_tactic(m));
#endif
/* use full sls
tactic * st = using_params(and_then(preamble_st,
cond(mk_is_qfbv_probe(),
cond(mk_is_qfbv_eq_probe(),
and_then(mk_bv1_blaster_tactic(m),
using_params(mk_smt_tactic(), solver_p)),
and_then(mk_nnf_tactic(m, p), mk_sls_tactic(m))),
mk_smt_tactic())),
main_p);*/
/* use pure dpll
tactic * st = using_params(and_then(mk_simplify_tactic(m),
cond(mk_is_qfbv_probe(),
and_then(mk_bit_blaster_tactic(m),
when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)),
and_then(using_params(and_then(mk_simplify_tactic(m),
mk_solve_eqs_tactic(m)),
local_ctx_p),
if_no_proofs(cond(mk_produce_unsat_cores_probe(),
mk_aig_tactic(),
using_params(mk_aig_tactic(),
big_aig_p))))),
new_sat),
mk_smt_tactic())),
main_p);*/
tactic * st = using_params(and_then(preamble_st,
// If the user sets HI_DIV0=false, then the formula may contain uninterpreted function
// symbols. In this case, we should not use