SRI-CSL / yices2 / 26809828217

69%

master: 71%

Build Type

push

github

Committed by ahmed-irfan

Commit Message

Protect re-resolved learned clauses from deletion (CaDiCaL-style used flag)

Add a per-clause "used recently" counter to the CDCL(T) learned-clause
header and have reduce_clause_database keep any clause whose counter is
nonzero, decrementing it so the protection decays once the clause sits
idle for a reduce interval. This mirrors CaDiCaL's used flag but layers
it on yices's existing activity-based selection rather than glue tiers.

A clause is marked used only when it is re-resolved during conflict
analysis (the conflict clause itself and any learned antecedent), not
when it is first learned. Freshly-learned clauses therefore start
unprotected (used = 0) and earn protection only by proving useful again;
in the meantime they are covered by the reason-clause lock and their high
initial activity. This avoids a degenerate first reduce that would
otherwise protect the entire young database and delete nothing.

The counter occupies existing padding in learned_clause_t, so the struct
does not grow on 64-bit. Full regression suite passes (1726/0).

Coverage Stats

17 of 17 new or added lines in 1 file covered. (100.0%)

1 existing line in 1 file now uncovered.

87492 of 127163 relevant lines covered (68.8%)

1578188.4 hits per line