lutpack: do not trust an approximate cofactor support in the MUX split

`lutpack` aborts on some networks with

  abc: src/opt/lpk/lpkAbcMux.c:192: Lpk_MuxSplit:
       Assertion `iVarVac < (int)p->nVars' failed.

Reproducer (a 24.7k-LUT `sqrt` netlist produced by `if -K 10 -Z 6`, ~10 s):

  read_blif sqrt-mapped.blif; lutpack

Lpk_MuxSplit() splits one component off a function and stores the new component
in a *vacant* fanin slot of the retained one:

  p->uSupp  = Kit_TruthSupport( Pol ? pTruth1 : pTruth0, p->nVars );
  p->uSupp |= (1 << Var);
  iVarVac   = Kit_WordFindFirstBit( ~p->uSupp );
  assert( iVarVac < (int)p->nVars );

A vacant slot is supposed to be guaranteed by Lpk_MuxAnalize(), which rejects a
candidate variable when

  nSuppSizeL = max(nSuppSize0 + 2*!Polarity, nSuppSize1 + 2*Polarity) > p->nVars

but it reads nSuppSize0/nSuppSize1 out of the *cached* p->puSupps[].  When those
came from Lpk_ComputeSupports() they are not exact: that routine builds two
BDDs of the function in opposite variable orders and stitches the two support
estimates together at the cofactoring variable, and the result can be a strict
subset of the true cofactor support.  Lpk_MuxAnalize() then admits a variable
whose split needs one slot more than the function has.

On the reproducer this happens for a 12-variable component at Var = 3,
Polarity = 1: the cached support of cofactor 1 is 0x3f7 (9 variables) while the
truth table's is 0xff7 (11).  The guard sees 9 + 2 = 11 <= 12 and accepts;
the split then produces uSupp = 0xff7 | (1 << 3) = 0xfff, which is full.

Instrumenting the same run shows the estimate differs from the exact support in
484 of 101970 cofactor supports, and is narrower in 352 of them, so this is not
a one-off.

Rather than change the support estimator or weaken the assertion -- which
documents a real invariant of Lpk_MuxSplit() -- re-derive the single support the
split depends on, once the candidate has been chosen, and decline the MUX
decomposition when it does not fit.  That is one cofactor and one support scan
per accepted candidate, not per candidate variable.  On the reproducer lutpack
then completes and yields the same result as recomputing every cached support
from the truth table (24694 -> 24635 nodes, 237 levels in both cases).

src/opt/lpk/lpkAbcDec.c

@@ -202,6 +202,24 @@ pMan->timeEvalMuxAn += Abc_Clock() - clk;
     assert( pResMux == NULL || pResDsd == NULL );
     if ( pResMux )
     {
+        // Lpk_MuxAnalize() decides feasibility from the cached cofactor supports in
+        // p->puSupps.  Those may have come from Lpk_ComputeSupports(), which derives
+        // them from two BDDs built in opposite variable orders and stitches the halves
+        // together, and that estimate can be a strict SUBSET of the true cofactor
+        // support.  When it is, the component retained by the split below ends up with
+        // no vacant fanin slot for the component that is split off, and Lpk_MuxSplit()
+        // fails its assertion `iVarVac < (int)p->nVars'.  Re-derive the one support the
+        // split actually depends on and decline the MUX decomposition if it does not fit.
+        unsigned * pTruthThis = Lpk_FunTruth( p, 0 );
+        unsigned * pTruthCof  = Lpk_FunTruth( p, 1 );
+        unsigned uSuppExact;
+        if ( pResMux->Polarity )
+            Kit_TruthCofactor1New( pTruthCof, pTruthThis, p->nVars, pResMux->Variable );
+        else
+            Kit_TruthCofactor0New( pTruthCof, pTruthThis, p->nVars, pResMux->Variable );
+        uSuppExact = Kit_TruthSupport( pTruthCof, p->nVars ) | ( 1 << pResMux->Variable );
+        if ( Kit_WordCountOnes( uSuppExact ) >= (int)p->nVars )
+            return 0;
 clk = Abc_Clock();
         p2 = Lpk_MuxSplit( pMan, p, pResMux->Variable, pResMux->Polarity );
 pMan->timeEvalMuxSp += Abc_Clock() - clk;