diff --git a/src/mcsat/bool/bool_plugin.c b/src/mcsat/bool/bool_plugin.c index f1b112d37..8df154ae8 100644 --- a/src/mcsat/bool/bool_plugin.c +++ b/src/mcsat/bool/bool_plugin.c @@ -100,9 +100,6 @@ typedef struct { /** Number of Reduce Clause DB Calls */ uint32_t num_clause_db_reduce; - /** bump factor for bool vars -- geq 1. Higher number means more weightage **/ - uint32_t bool_var_bump_factor; - } heuristic_params; struct { @@ -131,9 +128,6 @@ void bool_plugin_heuristics_init(bool_plugin_t* bp) { bp->heuristic_params.lemma_reduce_interval = 300; bp->heuristic_params.lemma_reduce_fraction = 0.75; bp->heuristic_params.num_clause_db_reduce = 0; - - // Bool var scoring - bp->heuristic_params.bool_var_bump_factor = 5; } static @@ -741,9 +735,8 @@ term_t bool_plugin_explain_propagation(plugin_t* plugin, variable_t var, ivector } ivector_push(reasons, opposite_term(t_i)); - // Bump the reason variable -- give more weightage to boolean reasons - bp->ctx->bump_variable_n(bp->ctx, x_i, - bp->heuristic_params.bool_var_bump_factor); + // Bump the reason variable + bp->ctx->bump_variable(bp->ctx, x_i); } return bool2term(var_value);