mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 01:40:22 +00:00
Code Activity

expose reorder config

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-22 15:30:06 -07:00
parent aff4b3022a
commit 364fbda925
4 changed files with 15 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_config.cpp
View file

@ -65,6 +65,8 @@ namespace sat {
m_rephase_base = p.rephase_base(); m_rephase_base = p.rephase_base();
m_reorder_base = p.reorder_base(); m_reorder_base = p.reorder_base();
m_reorder_itau = p.reorder_itau();
m_activity_scale = p.reorder_activity_scale();
m_search_sat_conflicts = p.search_sat_conflicts(); m_search_sat_conflicts = p.search_sat_conflicts();
m_search_unsat_conflicts = p.search_unsat_conflicts(); m_search_unsat_conflicts = p.search_unsat_conflicts();
m_phase_sticky = p.phase_sticky(); m_phase_sticky = p.phase_sticky();
@ -72,7 +74,6 @@ namespace sat {
m_restart_initial = p.restart_initial(); m_restart_initial = p.restart_initial();
m_restart_factor = p.restart_factor(); m_restart_factor = p.restart_factor();
m_restart_max = p.restart_max(); m_restart_max = p.restart_max();
m_activity_scale = 100;
m_propagate_prefetch = p.propagate_prefetch(); m_propagate_prefetch = p.propagate_prefetch();
m_inprocess_max = p.inprocess_max(); m_inprocess_max = p.inprocess_max();

2
src/sat/sat_config.h
View file

@ -92,6 +92,8 @@ namespace sat {
bool m_phase_sticky; bool m_phase_sticky;
unsigned m_rephase_base; unsigned m_rephase_base;
unsigned m_reorder_base; unsigned m_reorder_base;
double m_reorder_itau;
unsigned m_reorder_activity_scale;
bool m_propagate_prefetch; bool m_propagate_prefetch;
restart_strategy m_restart; restart_strategy m_restart;
bool m_restart_fast; bool m_restart_fast;

4
src/sat/sat_params.pyg
View file

@ -7,7 +7,9 @@ def_module_params('sat',
('search.unsat.conflicts', UINT, 400, 'period for solving for unsat (in number of conflicts)'), ('search.unsat.conflicts', UINT, 400, 'period for solving for unsat (in number of conflicts)'),
('search.sat.conflicts', UINT, 400, 'period for solving for sat (in number of conflicts)'), ('search.sat.conflicts', UINT, 400, 'period for solving for sat (in number of conflicts)'),
('rephase.base', UINT, 1000, 'number of conflicts per rephase '), ('rephase.base', UINT, 1000, 'number of conflicts per rephase '),
('reorder.base', UINT, UINT_MAX, 'number of conflicts per random reorder '), ('reorder.base', UINT, UINT_MAX, 'number of conflicts per random reorder '),
('reorder.itau', DOUBLE, 4.0, 'inverse temperature for softmax'),
('reorder.activity_scale', UINT, 100, 'scaling factor for activity update'),
('propagate.prefetch', BOOL, True, 'prefetch watch lists for assigned literals'), ('propagate.prefetch', BOOL, True, 'prefetch watch lists for assigned literals'),
('restart', SYMBOL, 'ema', 'restart strategy: static, luby, ema or geometric'), ('restart', SYMBOL, 'ema', 'restart strategy: static, luby, ema or geometric'),
('restart.initial', UINT, 2, 'initial restart (number of conflicts)'), ('restart.initial', UINT, 2, 'initial restart (number of conflicts)'),

16
src/sat/sat_solver.cpp
View file

@ -2196,7 +2196,7 @@ namespace sat {
void solver::update_activity(bool_var v, double p) { void solver::update_activity(bool_var v, double p) {
unsigned old_act = m_activity[v]; unsigned old_act = m_activity[v];
unsigned new_act = (unsigned) (num_vars() * m_config.m_activity_scale * p); unsigned new_act = (unsigned) (m_config.m_activity_scale * p);
m_activity[v] = new_act; m_activity[v] = new_act;
if (!was_eliminated(v) && value(v) == l_undef && new_act != old_act) { if (!was_eliminated(v) && value(v) == l_undef && new_act != old_act) {
m_case_split_queue.activity_changed_eh(v, new_act > old_act); m_case_split_queue.activity_changed_eh(v, new_act > old_act);
@ -3174,16 +3174,16 @@ namespace sat {
// exp(log(exp(logits[i])) - log(sum(exp(logits)))) // exp(log(exp(logits[i])) - log(sum(exp(logits))))
// = // =
// exp(logits[i] - lse) // exp(logits[i] - lse)
svector<float> logits(vars.size(), 0.0); svector<double> logits(vars.size(), 0.0);
float itau = 4.0; double itau = m_config.m_reorder_itau;
float lse = 0; double lse = 0;
float mid = m_rand.max_value()/2; double mid = m_rand.max_value()/2;
float max = 0; double max = 0;
for (float& f : logits) { for (double& f : logits) {
f = itau * (m_rand() - mid)/mid; f = itau * (m_rand() - mid)/mid;
if (f > max) max = f; if (f > max) max = f;
} }
for (float f : logits) { for (double f : logits) {
lse += log(f - max); lse += log(f - max);
} }
lse = max + exp(lse); lse = max + exp(lse);