New feature: Add incremental refinement to &scorr command

[zxxr1113]

Summary

Adds an -i switch to the &scorr command that turns on incremental
refinement of the speculative-reduction miter (SRM): instead of rebuilding
the full SRM and re-proving every candidate pair on each iteration, the new
mode reuses UNSAT proofs from previous iterations and re-proves only those
pairs whose SRM cone overlaps the transitive fanout (TFO) of a node whose
class representative changed since the last snapshot.

The default behaviour of &scorr is unchanged; users opt in with -i.

Algorithm

On each refinement iteration, the incremental manager:

1. Snapshots pReprs and pNexts after every SRM construction.
2. On the next round, computes a seed set of nodes whose representative
   changed; performs a forward-TFO BFS across nFrames unrollings (RI
   fanouts cross frames via Gia_ObjRiToRo) to mark every candidate node
   reachable from a seed.
3. Calls a variant SRM builder
   (Gia_ManCorrSpecReduce_Active / Gia_ManCorrSpecReduceInit_Active)
   that emits a candidate PO (a, b) only when pTfoMark[a] || pTfoMark[b].
4. In ring mode, also detects new/rewired ring edges (including the implicit
   tail → head closing edge) and forces them to be emitted even when neither
   endpoint is in the TFO — this preserves soundness when only pNexts
   changes between iterations.
5. Falls back to the full SRM when active_pairs / total_pairs > 70%,
   the ratio at which the active-filter overhead exceeds the work it saves.

The same active-list filter is also wired into the BMC pre-refinement
loop (Cec_ManLSCorrespondenceBmc); the BMC SRM is non-ring so only the
pReprs-based filter is used there.

Usage

abc 01> &r design.aig; &scorr -i
abc 01> &r design.aig; &scorr -i -v # print Incr time / fallback stats
abc 01> &r design.aig; &scorr -i -r # ring mode + incremental

-i is compatible with -c (CBS solver), -r (ring classes),

Files changed

File	Change
src/base/abci/abc.c	Register -i flag; add usage line and contributor note.
src/proof/cec/cec.h	New Cec_ParCor_t::fIncremental field.
src/proof/cec/cecInt.h	Cec_IncrMgr_t struct + 11 extern declarations.
src/proof/cec/cecCorr.c	Wire the active-list filter into the BMC and main refinement loops.
src/proof/cec/cecCorrIncr.c	New file — incremental manager, TFO BFS, and the two _Active SRM builders.
src/proof/cec/module.make	Build the new file.

Performance

Tested on the public HWMCC‘25 benchmark set
(N cases, end-to-end &r file; &scorr [-i]; &ps):

Case	&scorr	&scorr -i	Speed-up
Problem05_label49+token_ring.06.cil-2	393.48s	56.87s	6.92x
Problem05_label47+token_ring.13.cil-2	502.93s	131.63s	3.82x
cal143	1.38s	0.42s	3.29x
cal206	12.67s	4.11s	3.08x
Problem05_label43+token_ring.03.cil-1	138.88s	55.97s	2.48x

Across the full set, the average speedup is 1.5x, and the max speedup is 7x.

Soundness notes

One main correctness concerns identified and handled during development:

• Ring-edge invalidation. A pReprs-only seed set misses rewired
  ring edges whose endpoints' representatives did not change. Detected
  on level_16.aig. Fixed by also snapshotting pNexts and adding the
  explicit/closing edge check in Cec_IncrMgrRingEdgeChanged.

Acknowledgments

The core strategy for this incremental refinement, specifically the concept of only rechecking the nodes that is in the TFO of seeds to prune the speculative-reduction miter, was proposed by Alan Mishchenko.