From 505747d443b4e72af88777716b6f204491b29377 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 2 Nov 2014 21:43:49 -0800 Subject: Improvements to &fftest (adding computation of fixed parameters). --- src/sat/bmc/bmcFault.c | 314 ++++++++++++++++++++++++++++++++----------------- 1 file changed, 206 insertions(+), 108 deletions(-) diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index 289151b1..5ae44d2f 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -229,11 +229,11 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p ) +Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, Vec_Int_t * vMap ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; - int i; + int i, iFuncVars = 0; pNew = Gia_ManStart( 3 * Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); @@ -243,9 +243,18 @@ Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p ) Gia_ManForEachAnd( p, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(Gia_ManAppendCi(pNew)), pObj->Value ); - pObj->Value = Gia_ManHashOr( pNew, Gia_ManAppendCi(pNew), pObj->Value ); + + if ( Vec_IntEntry(vMap, iFuncVars++) ) + pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(Gia_ManAppendCi(pNew)), pObj->Value ); + else + Gia_ManAppendCi(pNew); + + if ( Vec_IntEntry(vMap, iFuncVars++) ) + pObj->Value = Gia_ManHashOr( pNew, Gia_ManAppendCi(pNew), pObj->Value ); + else + Gia_ManAppendCi(pNew); } + assert( iFuncVars == Vec_IntSize(vMap) ); Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); pNew = Gia_ManCleanup( pTemp = pNew ); @@ -265,11 +274,11 @@ Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p ) +Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p, Vec_Int_t * vMap ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; - int i; + int i, iFuncVars = 0; pNew = Gia_ManStart( 4 * Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); @@ -279,8 +288,12 @@ Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p ) Gia_ManForEachAnd( p, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - pObj->Value = Gia_ManHashXor( pNew, Gia_ManAppendCi(pNew), pObj->Value ); + if ( Vec_IntEntry(vMap, iFuncVars++) ) + pObj->Value = Gia_ManHashXor( pNew, Gia_ManAppendCi(pNew), pObj->Value ); + else + Gia_ManAppendCi(pNew); } + assert( iFuncVars == Vec_IntSize(vMap) ); Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); pNew = Gia_ManCleanup( pTemp = pNew ); @@ -300,11 +313,11 @@ Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p ) +Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, Vec_Int_t * vMap ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; - int i, iCtrl0, iCtrl1, iCtrl2, iCtrl3, iMuxA, iMuxB; + int i, iCtrl0, iCtrl1, iCtrl2, iCtrl3, iMuxA, iMuxB, iFuncVars = 0; pNew = Gia_ManStart( 9 * Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); @@ -313,10 +326,26 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p ) pObj->Value = Gia_ManAppendCi( pNew ); Gia_ManForEachAnd( p, pObj, i ) { - iCtrl0 = Gia_ManAppendCi(pNew); - iCtrl1 = Gia_ManAppendCi(pNew); - iCtrl2 = Gia_ManAppendCi(pNew); - iCtrl3 = Gia_ManAppendCi(pNew); + if ( Vec_IntEntry(vMap, iFuncVars++) ) + iCtrl0 = Gia_ManAppendCi(pNew); + else + iCtrl0 = 0, Gia_ManAppendCi(pNew); + + if ( Vec_IntEntry(vMap, iFuncVars++) ) + iCtrl1 = Gia_ManAppendCi(pNew); + else + iCtrl1 = 0, Gia_ManAppendCi(pNew); + + if ( Vec_IntEntry(vMap, iFuncVars++) ) + iCtrl2 = Gia_ManAppendCi(pNew); + else + iCtrl2 = 0, Gia_ManAppendCi(pNew); + + if ( Vec_IntEntry(vMap, iFuncVars++) ) + iCtrl3 = Gia_ManAppendCi(pNew); + else + iCtrl3 = 0, Gia_ManAppendCi(pNew); + if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) iCtrl0 = Abc_LitNot(iCtrl0); else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) @@ -325,10 +354,12 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p ) iCtrl2 = Abc_LitNot(iCtrl2); else //if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) iCtrl3 = Abc_LitNot(iCtrl3); + iMuxA = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl1, iCtrl0 ); iMuxB = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl3, iCtrl2 ); pObj->Value = Gia_ManHashMux( pNew, Gia_ObjFanin1(pObj)->Value, iMuxB, iMuxA ); } + assert( iFuncVars == Vec_IntSize(vMap) ); Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); pNew = Gia_ManCleanup( pTemp = pNew ); @@ -803,46 +834,49 @@ Gia_Man_t * Gia_ManDeriveDup( Gia_Man_t * p, int nPisNew ) SeeAlso [] ***********************************************************************/ -int Gia_ManFaultAnalyze( sat_solver * pSat, Vec_Int_t * vPars, Vec_Int_t * vLits, int Iter ) +int Gia_ManFaultAnalyze( sat_solver * pSat, Vec_Int_t * vPars, Vec_Int_t * vMap, Vec_Int_t * vLits, int Iter ) { + int nConfLimit = 100; int status, i, v, iVar, Lit; int nUnsats = 0, nRuns = 0; abctime clk = Abc_Clock(); - Vec_IntFill( vLits, Vec_IntSize(vPars), 0 ); + assert( Vec_IntSize(vPars) == Vec_IntSize(vMap) ); + // check presence of each variable + Vec_IntClear( vLits ); + Vec_IntAppend( vLits, vMap ); for ( v = 0; v < Vec_IntSize(vPars); v++ ) { - if ( Vec_IntEntry(vLits, v) ) + if ( !Vec_IntEntry(vLits, v) ) continue; + assert( Vec_IntEntry(vLits, v) == 1 ); nRuns++; Lit = Abc_Var2Lit( Vec_IntEntry(vPars, v), 0 ); - status = sat_solver_solve( pSat, &Lit, &Lit+1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + status = sat_solver_solve( pSat, &Lit, &Lit+1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_Undef ) - { - //printf( "Var %d timed out\n", v ); continue; - } if ( status == l_False ) { nUnsats++; - //printf( "Var %d is UNSAT\n", v ); + assert( Vec_IntEntry(vMap, v) == 1 ); + Vec_IntWriteEntry( vMap, v, 0 ); Lit = Abc_LitNot(Lit); //status = sat_solver_addclause( pSat, &Lit, &Lit+1 ); //assert( status ); continue; } Vec_IntForEachEntry( vPars, iVar, i ) - if ( !Vec_IntEntry(vLits, i) && sat_solver_var_value(pSat, iVar) ) - Vec_IntWriteEntry( vLits, i, 1 ); - assert( Vec_IntEntry(vLits, v) == 1 ); + if ( Vec_IntEntry(vLits, i) && sat_solver_var_value(pSat, iVar) ) + Vec_IntWriteEntry( vLits, i, 0 ); + assert( Vec_IntEntry(vLits, v) == 0 ); } - printf( "Iteration %3d has determined %5d (out of %5d) parameters after %6d SAT calls. ", Iter, nUnsats, Vec_IntSize(vPars), nRuns ); + printf( "Iteration %3d has determined %5d (out of %5d) parameters after %6d SAT calls. ", Iter, Vec_IntSize(vMap) - Vec_IntCountPositive(vMap), Vec_IntSize(vPars), nRuns ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return nUnsats; } /**Function************************************************************* - Synopsis [] + Synopsis [Generate miter, CNF and solver.] Description [] @@ -851,61 +885,20 @@ int Gia_ManFaultAnalyze( sat_solver * pSat, Vec_Int_t * vPars, Vec_Int_t * vLits SeeAlso [] ***********************************************************************/ -void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars ) +int Gia_ManFaultPrepare( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars, int nFuncVars, Vec_Int_t * vMap, Vec_Int_t * vTests, Vec_Int_t * vLits, Gia_Man_t ** ppMiter, Cnf_Dat_t ** ppCnf, sat_solver ** ppSat, int fWarmUp ) { - int nIterMax = 1000000, nVars, nPars; - int i, Iter, Iter2, status, nFuncVars = -1; - abctime clkSat = 0, clkTotal = Abc_Clock(); - Vec_Int_t * vLits, * vTests, * vPars = NULL; - Gia_Man_t * p0 = NULL, * p1 = NULL, * pM; + Gia_Man_t * p0, * p1, * pM; Gia_Obj_t * pObj; Cnf_Dat_t * pCnf; sat_solver * pSat; + int i, Iter, status; + abctime clkSat = 0; - if ( pPars->Algo == 0 && Gia_FormStrCount( pPars->pFormStr, &nVars, &nPars ) ) - return; - - // select algorithm - if ( pPars->Algo == 0 ) - printf( "FFTEST is computing test patterns for fault model \"%s\"...\n", pPars->pFormStr ); - else if ( pPars->Algo == 1 ) - printf( "FFTEST is computing test patterns for %sdelay faults...\n", pPars->fBasic ? "single " : "" ); - else if ( pPars->Algo == 2 ) - printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", pPars->fBasic ? "single " : "" ); - else if ( pPars->Algo == 3 ) - printf( "FFTEST is computing test patterns for %scomplement faults...\n", pPars->fBasic ? "single " : "" ); - else if ( pPars->Algo == 4 ) - printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", pPars->fBasic ? "single " : "" ); - else - { - printf( "Unrecognized algorithm (%d).\n", pPars->Algo ); - return; - } - - // select algorithm - if ( pPars->Algo == 0 ) - nFuncVars = Gia_ManCiNum(p); - else if ( pPars->Algo == 1 ) - nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p); - else if ( pPars->Algo == 2 ) - nFuncVars = Gia_ManCiNum(p); - else if ( pPars->Algo == 3 ) - nFuncVars = Gia_ManCiNum(p); - else if ( pPars->Algo == 4 ) - nFuncVars = Gia_ManCiNum(p); - - // collect test patterns from file - if ( pPars->pFileName ) - vTests = Gia_ManGetTestPatterns( pPars->pFileName ); - else - vTests = Vec_IntAlloc( 10000 ); - if ( vTests == NULL ) - return; - if ( Vec_IntSize(vTests) % nFuncVars != 0 ) + if ( Vec_IntSize(vTests) && (Vec_IntSize(vTests) % nFuncVars != 0) ) { printf( "The number of symbols in the input patterns (%d) does not divide evenly on the number of test variables (%d).\n", Vec_IntSize(vTests), nFuncVars ); Vec_IntFree( vTests ); - return; + return 0; } // select algorithm @@ -918,11 +911,11 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars ) p1 = Gia_ManFaultUnfold( p, 1 ); } else if ( pPars->Algo == 2 ) - p1 = Gia_ManStuckAtUnfold( p ); + p1 = Gia_ManStuckAtUnfold( p, vMap ); else if ( pPars->Algo == 3 ) - p1 = Gia_ManFlipUnfold( p ); + p1 = Gia_ManFlipUnfold( p, vMap ); else if ( pPars->Algo == 4 ) - p1 = Gia_ManFOFUnfold( p ); + p1 = Gia_ManFOFUnfold( p, vMap ); if ( pPars->Algo != 1 ) p0 = Gia_ManDeriveDup( pG, Gia_ManCiNum(p1) - Gia_ManCiNum(pG) ); // Gia_AigerWrite( p1, "newfault.aig", 0, 0 ); @@ -944,7 +937,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars ) assert( 0 ); // add one large OR clause - vLits = Vec_IntAlloc( Gia_ManCoNum(p) ); + Vec_IntClear( vLits ); Gia_ManForEachCo( pM, pObj, i ) Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) ); sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); @@ -964,25 +957,31 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars ) { int nTests = Vec_IntSize(vTests) / nFuncVars; assert( Vec_IntSize(vTests) % nFuncVars == 0 ); - printf( "Reading %d pre-computed test patterns from file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pPars->pFileName ); + if ( pPars->pFileName ) + printf( "Reading %d pre-computed test patterns from file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pPars->pFileName ); + else + printf( "Reading %d pre-computed test patterns from previous rounds.\n", Vec_IntSize(vTests) / nFuncVars ); for ( Iter = 0; Iter < nTests; Iter++ ) { - abctime clk = Abc_Clock(); - status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - clkSat += Abc_Clock() - clk; - if ( status == l_Undef ) - { - if ( pPars->fVerbose ) - printf( "\n" ); - printf( "Timeout reached after %d seconds and adding %d tests.\n", pPars->nTimeOut, Iter ); - goto finish; - } - if ( status == l_False ) + if ( fWarmUp ) { - if ( pPars->fVerbose ) - printf( "\n" ); - printf( "The problem is UNSAT after adding %d tests.\n", Iter ); - goto finish; + abctime clk = Abc_Clock(); + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + clkSat += Abc_Clock() - clk; + if ( status == l_Undef ) + { + if ( pPars->fVerbose ) + printf( "\n" ); + printf( "Timeout reached after %d seconds and adding %d tests.\n", pPars->nTimeOut, Iter ); + return 0; + } + if ( status == l_False ) + { + if ( pPars->fVerbose ) + printf( "\n" ); + printf( "The problem is UNSAT after adding %d tests.\n", Iter ); + return 0; + } } // get pattern Vec_IntClear( vLits ); @@ -1010,14 +1009,14 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars ) if ( pPars->fVerbose ) printf( "\n" ); printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter ); - goto finish; + return 0; } if ( status == l_False ) { if ( pPars->fVerbose ) printf( "\n" ); printf( "The problem is UNSAT after %d iterations.\n", Iter ); - goto finish; + return 0; } // initialize simple pattern Vec_IntFill( vLits, nFuncVars, Iter ); @@ -1026,10 +1025,120 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars ) } } + printf( "Using miter with: AIG nodes = %6d. CNF variables = %6d. CNF clauses = %8d.\n", Gia_ManAndNum(pM), pCnf->nVars, pCnf->nClauses ); + + *ppMiter = pM; + *ppCnf = pCnf; + *ppSat = pSat; + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars ) +{ + int nIterMax = 1000000, nVars, nPars; + int i, Iter, Iter2, status, nFuncVars = -1; + abctime clk, clkSat = 0, clkTotal = Abc_Clock(); + Vec_Int_t * vLits, * vMap = NULL, * vTests, * vPars = NULL; + Gia_Man_t * p0 = NULL, * p1 = NULL, * pM; + Gia_Obj_t * pObj; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + + if ( pPars->Algo == 0 && Gia_FormStrCount( pPars->pFormStr, &nVars, &nPars ) ) + return; + + // select algorithm + if ( pPars->Algo == 0 ) + printf( "FFTEST is computing test patterns for fault model \"%s\"...\n", pPars->pFormStr ); + else if ( pPars->Algo == 1 ) + printf( "FFTEST is computing test patterns for %sdelay faults...\n", pPars->fBasic ? "single " : "" ); + else if ( pPars->Algo == 2 ) + printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", pPars->fBasic ? "single " : "" ); + else if ( pPars->Algo == 3 ) + printf( "FFTEST is computing test patterns for %scomplement faults...\n", pPars->fBasic ? "single " : "" ); + else if ( pPars->Algo == 4 ) + printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", pPars->fBasic ? "single " : "" ); + else + { + printf( "Unrecognized algorithm (%d).\n", pPars->Algo ); + return; + } + + // select algorithm + if ( pPars->Algo == 0 ) + nFuncVars = Gia_ManCiNum(p); + else if ( pPars->Algo == 1 ) + nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p); + else if ( pPars->Algo == 2 ) + nFuncVars = Gia_ManCiNum(p); + else if ( pPars->Algo == 3 ) + nFuncVars = Gia_ManCiNum(p); + else if ( pPars->Algo == 4 ) + nFuncVars = Gia_ManCiNum(p); + + // collect test patterns from file + if ( pPars->pFileName ) + vTests = Gia_ManGetTestPatterns( pPars->pFileName ); + else + vTests = Vec_IntAlloc( 10000 ); + if ( vTests == NULL ) + return; + + // select algorithm + vMap = Vec_IntAlloc( 0 ); + if ( pPars->Algo == 2 ) + Vec_IntFill( vMap, 2 * Gia_ManAndNum(p), 1 ); + else if ( pPars->Algo == 3 ) + Vec_IntFill( vMap, Gia_ManAndNum(p), 1 ); + else if ( pPars->Algo == 4 ) + Vec_IntFill( vMap, 4 * Gia_ManAndNum(p), 1 ); + + // prepare SAT solver + vLits = Vec_IntAlloc( Gia_ManCoNum(p) ); + if ( !Gia_ManFaultPrepare(p, pG, pPars, nFuncVars, vMap, vTests, vLits, &pM, &pCnf, &pSat, 1) ) + return; + // iterate through the test vectors for ( Iter = pPars->fStartPats ? 2 : Vec_IntSize(vTests) / nFuncVars; Iter < nIterMax; Iter++ ) { - abctime clk = Abc_Clock(); + // collect parameter variables + if ( pPars->nIterCheck && vPars == NULL ) + { + vPars = Vec_IntAlloc( Gia_ManPiNum(pM) - nFuncVars ); + Gia_ManForEachPi( pM, pObj, i ) + if ( i >= nFuncVars ) + Vec_IntPush( vPars, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ); + assert( Vec_IntSize(vPars) == Gia_ManPiNum(pM) - nFuncVars ); + } + // derive unit parameter variables + if ( Iter && pPars->nIterCheck && (Iter % pPars->nIterCheck) == 0 ) + { + Gia_ManFaultAnalyze( pSat, vPars, vMap, vLits, Iter ); + // cleanup + Gia_ManStop( pM ); + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + // recompute + if ( !Gia_ManFaultPrepare(p, pG, pPars, nFuncVars, vMap, vTests, vLits, &pM, &pCnf, &pSat, 0) ) + { + printf( "This should never happen.\n" ); + return; + } + Vec_IntFreeP( &vPars ); + } + // solve + clk = Abc_Clock(); status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); clkSat += Abc_Clock() - clk; if ( pPars->fVerbose ) @@ -1064,18 +1173,6 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars ) Vec_IntAppend( vTests, vLits ); // add constraint Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars ); - // collect parameter variables - if ( pPars->nIterCheck && vPars == NULL ) - { - vPars = Vec_IntAlloc( Gia_ManPiNum(pM) - nFuncVars ); - Gia_ManForEachPi( pM, pObj, i ) - if ( i >= nFuncVars ) - Vec_IntPush( vPars, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ); - assert( Vec_IntSize(vPars) == Gia_ManPiNum(pM) - nFuncVars ); - } - // derive unit parameter variables - if ( pPars->nIterCheck && !(Iter % pPars->nIterCheck) ) - Gia_ManFaultAnalyze( pSat, vPars, vLits, Iter ); } finish: // print results @@ -1202,6 +1299,7 @@ finish: Cnf_DataFree( pCnf ); Gia_ManStop( pM ); Vec_IntFree( vTests ); + Vec_IntFree( vMap ); Vec_IntFree( vLits ); Vec_IntFreeP( &vPars ); } -- cgit v1.2.3