mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fix #3397, use it or lose it

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-18 11:06:19 -07:00
parent fbf5fc9482
commit 24dd047892
4 changed files with 4 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_config.cpp
View file

@ -204,10 +204,8 @@ namespace sat {
m_branching_heuristic = BH_VSIDS;
else if (p.branching_heuristic() == symbol("chb"))
m_branching_heuristic = BH_CHB;
else if (p.branching_heuristic() == symbol("lrb"))
m_branching_heuristic = BH_LRB;
else
throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids', 'lrb' or 'chb'");
throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids' or 'chb'");
m_anti_exploration = p.branching_anti_exploration();
m_step_size_init = 0.40;

3
src/sat/sat_config.h
View file

@ -49,8 +49,7 @@ namespace sat {
enum branching_heuristic {
BH_VSIDS,
BH_CHB,
BH_LRB
BH_CHB
};
enum pb_resolve {

2
src/sat/sat_params.pyg
View file

@ -22,7 +22,7 @@ def_module_params('sat',
('variable_decay', UINT, 110, 'multiplier (divided by 100) for the VSIDS activity increment'),
('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'),
('inprocess.out', SYMBOL, '', 'file to dump result of the first inprocessing step and exit'),
('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'),
('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, chb'),
('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'),
('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
('random_seed', UINT, 0, 'random seed'),

15
src/sat/sat_solver.cpp
View file

@ -878,10 +878,6 @@ namespace sat {
case BH_CHB:
m_last_propagation[v] = m_stats.m_conflict;
break;
case BH_LRB:
m_participated[v] = 0;
m_reasoned[v] = 0;
break;
}
if (m_config.m_anti_exploration) {
@ -3472,8 +3468,7 @@ namespace sat {
\brief Reset the mark of the variables in the current lemma.
*/
void solver::reset_lemma_var_marks() {
if (m_config.m_branching_heuristic == BH_LRB ||
m_config.m_branching_heuristic == BH_VSIDS) {
if (m_config.m_branching_heuristic == BH_VSIDS) {
update_lrb_reasoned();
}
literal_vector::iterator it = m_lemma.begin();
@ -3715,14 +3710,6 @@ namespace sat {
m_assignment[(~l).index()] = l_undef;
SASSERT(value(v) == l_undef);
m_case_split_queue.unassign_var_eh(v);
if (m_config.m_branching_heuristic == BH_LRB) {
uint64_t interval = m_stats.m_conflict - m_last_propagation[v];
if (interval > 0) {
auto activity = m_activity[v];
auto reward = (m_config.m_reward_offset * (m_participated[v] + m_reasoned[v])) / interval;
set_activity(v, static_cast<unsigned>(m_step_size * reward + ((1 - m_step_size) * activity)));
}
}
if (m_config.m_anti_exploration) {
m_canceled[v] = m_stats.m_conflict;
}