cec: guard the SOP derivation behind ABC_USE_CUDD

[TrevorHansen]

Building this branch with ABC_USE_NO_CUDD=1, as STP's cmake/FindABC.cmake does, fails to link:

libabc-pic.a(cecSatG2.c.o): in function `extractSOP':
cecSatG2.c:(.text.extractSOP+0x70): undefined reference to `Cudd_zddIsop'
cecSatG2.c:(.text.extractSOP+0x9d): undefined reference to `Abc_CountZddCubes'
cecSatG2.c:(.text.computeISOPs+0x140): undefined reference to `Extra_bddCountCubes'
...

extractSOP(), computeISOPs() and Cec_DeriveSOPs() call into CUDD unconditionally, and cecSatG2.c.o is always pulled into the link because the Cec4_* entry points it defines are referenced from giaDup.c, giaEquiv.c, cecChoice.c and others. So the whole no-CUDD configuration is broken, not just an unused corner of it.

ABC_USE_CUDD is how the rest of the tree handles this - aigSplit.c, giaClp.c, giaSupp.c, ifDsd.c and others already guard their BDD code with it, and the Makefile defines it exactly when the CUDD modules are compiled. This guards the three functions and their single call site the same way.

With CUDD enabled nothing changes. Without it, Cec_SimGenRun() skips the SOP derivation instead of failing to link.

Verified by compiling cecSatG2.c both ways - ten undefined CUDD references become zero without CUDD, and the file is unchanged with it - and by building the whole library with ABC_USE_NO_CUDD=1. The one remaining undefined CUDD symbol in the archive, Abc_EnumerateCubeStatesZdd in abc.c.o, is pre-existing and never pulled into a link.

This affects upstream too: the same file on berkeley-abc/abc master has the same ten undefined references in a no-CUDD build.

[TrevorHansen]

Do not merge this as it stands - I found a hazard in it.

Guarding out Cec_DeriveSOPs() does not merely skip a computation. It leaves p->vTTISOPs and p->vTTLut NULL (Gia_Man_t is ABC_CALLOC'd), and getISOPObjId() dereferences both without a check:

char * pSopInfo = pMan->vTTISOPs->pArray + Vec_IntEntry( pMan->vTTLut, ObjId );

That is reached from computeNetworkValues(), generateLutsRankings(), check_implication() and printISOPLUT(), so the SimGen path would segfault rather than report the feature as unavailable. The teardown at the end of Cec_SimGenRun() also frees both vectors unconditionally.

Doing this properly means guarding the whole SimGen feature - Cec_SimGenRun() as well as the three SOP functions, with a stub that reports it needs CUDD, in the style of saigDup.c:592. That is a larger change to a feature there is no test for here.

The immediate build problem is handled on the STP side instead, by building ABC with CUDD (stp/stp#1051); the measured cost is 2.2MB of archive and no change to the emitted CNF. The underlying defect is real and also present on berkeley-abc/abc master, so it is better reported there than patched blind.

[TrevorHansen]

fixed downstream.