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

Dynamic delta trigger decrease

Browse source
This commit is contained in:
Miguel Neves 2017-10-10 15:59:53 -07:00
parent 4d91169118
commit 01897831fb
2 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/sat/sat_lookahead.cpp
View file

@ -914,6 +914,7 @@ namespace sat {
void lookahead::init() { void lookahead::init() {
m_delta_trigger = 0.0; m_delta_trigger = 0.0;
m_delta_decrease = 0.0;
m_config.m_dl_success = 0.8; m_config.m_dl_success = 0.8;
m_inconsistent = false; m_inconsistent = false;
m_qhead = 0; m_qhead = 0;
@ -1608,6 +1609,7 @@ namespace sat {
void lookahead::compute_lookahead_reward() { void lookahead::compute_lookahead_reward() {
init_lookahead_reward(); init_lookahead_reward();
TRACE("sat", display_lookahead(tout); ); TRACE("sat", display_lookahead(tout); );
m_delta_decrease = pow(m_config.m_delta_rho, 1.0 / (double)m_lookahead.size());
unsigned base = 2; unsigned base = 2;
bool change = true; bool change = true;
literal last_changed = null_literal; literal last_changed = null_literal;
@ -1811,7 +1813,8 @@ namespace sat {
} }
} }
else { else {
m_delta_trigger *= m_config.m_delta_rho; SASSERT(m_delta_decrease > 0.0);
m_delta_trigger *= m_delta_decrease;
} }
} }
} }

5
src/sat/sat_lookahead.h
View file

@ -89,7 +89,7 @@ namespace sat {
m_min_cutoff = 30; m_min_cutoff = 30;
m_preselect = false; m_preselect = false;
m_level_cand = 600; m_level_cand = 600;
m_delta_rho = (double)0.99995; m_delta_rho = (double)0.25;
m_dl_max_iterations = 2; m_dl_max_iterations = 2;
m_tc1_limit = 10000000; m_tc1_limit = 10000000;
m_reward_type = ternary_reward; m_reward_type = ternary_reward;
@ -146,7 +146,8 @@ namespace sat {
}; };
config m_config; config m_config;
double m_delta_trigger; double m_delta_trigger;
double m_delta_decrease;
drat m_drat; drat m_drat;
literal_vector m_assumptions; literal_vector m_assumptions;