Skip to content

Commit d40b694

Browse files
committed
No floating point issue
1 parent 66aef0d commit d40b694

File tree

1 file changed

+7
-3
lines changed

1 file changed

+7
-3
lines changed

src/counter.cpp

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -197,8 +197,9 @@ void Counter::compute_score(TWD::TreeDecomposition& tdec, uint32_t nodes, bool p
197197
<< " nodes: " << nodes
198198
<< " rt/width(=rt): " << rt
199199
<< " rt*conf.td_exp_mult: " << rt*conf.td_exp_mult
200-
<< " exp(rt*conf.td_exp_mult)/conf.td_divider: "
201-
<< exp(rt*conf.td_exp_mult)/conf.td_divider);
200+
<< " rt: " << rt
201+
<< " conf.td_exp_mult: " << conf.td_exp_mult
202+
<< " conf.td_divider: " << conf.td_divider);
202203
}
203204

204205
// Calc td score
@@ -4169,7 +4170,10 @@ void Counter::set_lit_weight(Lit l, const FF& w) {
41694170
*weights[l.raw()] = *w;
41704171
var_weights[l.var()] = weights[l.raw()]->dup();
41714172
*var_weights[l.var()] += *weights[l.neg().raw()];
4172-
if (w->is_zero()) add_irred_cl({l.neg()});
4173+
if (w->is_zero()) {
4174+
add_irred_cl({l.neg()});
4175+
verb_print(3, "Weight is zero, adding clause: " << l.neg());
4176+
}
41734177
}
41744178

41754179
void Counter::init_decision_stack() {

0 commit comments

Comments
 (0)