diff options
| -rw-r--r-- | abclib.dsp | 152 | ||||
| -rw-r--r-- | src/aig/gia/giaMan.c | 39 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 96 | ||||
| -rw-r--r-- | src/sat/bmc/bmcLilac.c | 99 | ||||
| -rw-r--r-- | src/sat/bmc/bmcTulip.c | 3 |
5 files changed, 202 insertions, 187 deletions
@@ -729,162 +729,10 @@ SOURCE=.\src\base\test\test.c # Begin Group "abc2" # PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\base\abc2\abc2.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2_.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2_power.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Blifi.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Blifo.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Core.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Dup.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Equiv.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Extract.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Flatten.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Func.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Fx.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Gia.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Hash.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Insert.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Logic.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Map.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Merge.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Mfs.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Multi.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Ntk.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Part.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Print.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Rec.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Slack.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Strash.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Time.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Truth.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Util.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Veri.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Verify.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2\abc2Vero.c -# End Source File # End Group # Begin Group "abc2d" # PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\base\abc2d\abc2d.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2d\ast2.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2d\magic.c -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2d\magic.h -# End Source File -# Begin Source File - -SOURCE=.\src\base\abc2d\util.c -# End Source File # End Group # End Group # Begin Group "bdd" diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index e78cb849..d3ee3f48 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -293,6 +293,43 @@ void Gia_ManPrintTents( Gia_Man_t * p ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintInitClasses( Vec_Int_t * vInits ) +{ + int i, Value; + int Counts[4] = {0}; + Vec_IntForEachEntry( vInits, Value, i ) + Counts[Value]++; + for ( i = 0; i < 4; i++ ) + printf( "%d = %d ", i, Counts[i] ); + printf( "X = %d\n", Counts[2] + Counts[3] ); + Vec_IntForEachEntry( vInits, Value, i ) + { + Counts[Value]++; + if ( Value == 0 ) + printf( "0" ); + else if ( Value == 1 ) + printf( "1" ); + else if ( Value == 2 ) + printf( "x" ); + else if ( Value == 3 ) + printf( "X" ); + else assert( 0 ); + } + printf( "\n" ); + +} + +/**Function************************************************************* + Synopsis [Prints stats for the AIG.] Description [] @@ -385,6 +422,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars ) Gia_ManPrintFlopClasses( p ); Gia_ManPrintGateClasses( p ); Gia_ManPrintObjClasses( p ); + if ( p->vInitClasses ) + Gia_ManPrintInitClasses( p->vInitClasses ); if ( pPars && pPars->fTents ) { /* diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d3fcb137..e54a62e9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -400,6 +400,7 @@ static int Abc_CommandAbc9ICheck ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9FunFaTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Tulip ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Lilac ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -964,6 +965,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&funfatest", Abc_CommandAbc9FunFaTest, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&tulip", Abc_CommandAbc9Tulip, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&lilac", Abc_CommandAbc9Lilac, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 ); @@ -32820,7 +32822,99 @@ int Abc_CommandAbc9Tulip( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: &tulip [-FWT num] [-svh]\n" ); - Abc_Print( -2, "\t experimental prcedure for testing new ideas\n" ); + Abc_Print( -2, "\t experimental procedure\n" ); + Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n", nFrames ); + Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n", nWords ); + Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut ); + Abc_Print( -2, "\t-s : toggles using ternary simulation [default = %s]\n", fSim? "yes": "no" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Lilac( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Vec_Int_t * Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ); + Vec_Int_t * vTemp; + int c, nFrames = 1000, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FWTsvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'W': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + nWords = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nWords < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nTimeOut < 0 ) + goto usage; + break; + case 's': + fSim ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Lilac(): There is no AIG.\n" ); + return 0; + } + if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9Lilac(): AIG is combinational.\n" ); + return 0; + } + pAbc->pGia->vInitClasses = Gia_ManLilacTest( pAbc->pGia, vTemp = pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose ); + Vec_IntFreeP( &vTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &lilac [-FWT num] [-svh]\n" ); + Abc_Print( -2, "\t experimental procedure\n" ); Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n", nFrames ); Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n", nWords ); Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut ); diff --git a/src/sat/bmc/bmcLilac.c b/src/sat/bmc/bmcLilac.c index e1386061..1d41312b 100644 --- a/src/sat/bmc/bmcLilac.c +++ b/src/sat/bmc/bmcLilac.c @@ -115,40 +115,47 @@ void Bmc_LilacUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int SeeAlso [] ***********************************************************************/ -int Bmc_LilacPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap ) +int Bmc_LilacPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap, Vec_Int_t * vCopies ) { Gia_Obj_t * pObj = Gia_ManObj( pNew, iIdNew ); - int iLitPart0, iLitPart1; - if ( pObj->Value ) - return pObj->Value; - if ( Vec_IntEntry(vSatMap, iIdNew) ) + int iLitPart0, iLitPart1, iRes; + if ( Vec_IntEntry(vCopies, iIdNew) ) + return Vec_IntEntry(vCopies, iIdNew); + if ( Vec_IntEntry(vSatMap, iIdNew) >= 0 || Gia_ObjIsCi(pObj) ) { Vec_IntPush( vPartMap, iIdNew ); - return (pObj->Value = Gia_ManAppendCi(pPart)); + iRes = Gia_ManAppendCi(pPart); + Vec_IntWriteEntry( vCopies, iIdNew, iRes ); + return iRes; } - iLitPart0 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap ); - iLitPart1 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap ); + assert( Gia_ObjIsAnd(pObj) ); + iLitPart0 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap, vCopies ); + iLitPart1 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap, vCopies ); iLitPart0 = Abc_LitNotCond( iLitPart0, Gia_ObjFaninC0(pObj) ); iLitPart1 = Abc_LitNotCond( iLitPart1, Gia_ObjFaninC1(pObj) ); Vec_IntPush( vPartMap, iIdNew ); - return (pObj->Value = Gia_ManAppendAnd( pPart, iLitPart0, iLitPart1 )); + iRes = Gia_ManAppendAnd( pPart, iLitPart0, iLitPart1 ); + Vec_IntWriteEntry( vCopies, iIdNew, iRes ); + return iRes; } -Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap ) +Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap, Vec_Int_t * vCopies ) { Gia_Man_t * pPart; int i, iLit, iLitPart; - Gia_ManCleanValue( pNew ); + Vec_IntFill( vCopies, Gia_ManObjNum(pNew), 0 ); Vec_IntFillExtra( vSatMap, Gia_ManObjNum(pNew), -1 ); pPart = Gia_ManStart( 1000 ); pPart->pName = Abc_UtilStrsav( pNew->pName ); - Gia_ManConst0(pNew)->Value = 0; Vec_IntClear( vPartMap ); + Vec_IntPush( vPartMap, 0 ); Vec_IntForEachEntry( vMiters, iLit, i ) { if ( iLit == -1 ) continue; - iLitPart = Bmc_LilacPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap ); + assert( iLit >= 2 ); + iLitPart = Bmc_LilacPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap, vCopies ); Gia_ManAppendCo( pPart, Abc_LitNotCond(iLitPart, Abc_LitIsCompl(iLit)) ); + Vec_IntPush( vPartMap, -1 ); } assert( Gia_ManPoNum(pPart) > 0 ); assert( Vec_IntSize(vPartMap) == Gia_ManObjNum(pPart) ); @@ -166,17 +173,16 @@ Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vM SeeAlso [] ***********************************************************************/ -int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int fVerbose ) +int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose ) { int nSatVars = 1; - int nTimeOut = 0; - Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap; + Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap, * vCopies; Gia_Man_t * pNew, * pPart; Gia_Obj_t * pObj; Cnf_Dat_t * pCnf; sat_solver * pSat; - int i, f, status, iVar0, iVar1, iLit, iLit0, iLit1; - int fChanges, RetValue = 1; + int iVar0, iVar1, iLit, iLit0, iLit1; + int i, f, status, nChanges, nMiters, RetValue = 1; // start the SAT solver pSat = sat_solver_new(); @@ -198,21 +204,31 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int vMiters = Vec_IntAlloc( 1000 ); vSatMap = Vec_IntAlloc( 1000 ); vPartMap = Vec_IntAlloc( 1000 ); + vCopies = Vec_IntAlloc( 1000 ); for ( f = 0; f < nFrames; f++ ) { + abctime clk = Abc_Clock(); Bmc_LilacUnfold( pNew, p, vLits0, 0 ); Bmc_LilacUnfold( pNew, p, vLits1, 1 ); assert( Vec_IntSize(vLits0) == Vec_IntSize(vLits1) ); + nMiters = 0; Vec_IntClear( vMiters ); Vec_IntForEachEntryTwo( vLits0, vLits1, iLit0, iLit1, i ) - if ( (iLit0 > 2 || iLit1 > 2) && iLit0 != iLit1 ) - Vec_IntPush( vMiters, Gia_ManHashXor(pNew, iLit0, iLit1) ); + if ( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 ) + Vec_IntPush( vMiters, Gia_ManHashXor(pNew, iLit0, iLit1) ), nMiters++; else Vec_IntPush( vMiters, -1 ); + assert( Vec_IntSize(vMiters) == Gia_ManRegNum(p) ); + if ( fVerbose ) + printf( "Frame %4d : ", f ); if ( Vec_IntSum(vMiters) + Vec_IntSize(vLits1) == 0 ) + { + if ( fVerbose ) + printf( "Trivial\n" ); continue; + } // create new part - pPart = Bmc_LilacPart( pNew, vSatMap, vMiters, vPartMap ); + pPart = Bmc_LilacPart( pNew, vSatMap, vMiters, vPartMap, vCopies ); pCnf = Cnf_DeriveGiaRemapped( pPart ); Cnf_DataLiftGia( pCnf, pPart, nSatVars ); nSatVars += pCnf->nVars; @@ -223,28 +239,35 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int // stitch the clauses Gia_ManForEachPi( pPart, pObj, i ) { - int iIdPart = Gia_ObjId(pPart, pObj); - iVar0 = pCnf->pVarNums[iIdPart]; - iVar1 = Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, iIdPart) ); + iVar0 = pCnf->pVarNums[Gia_ObjId(pPart, pObj)]; + iVar1 = Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, Gia_ObjId(pPart, pObj)) ); if ( iVar1 == -1 ) continue; sat_solver_add_buffer( pSat, iVar0, iVar1, 0 ); } // transfer variables - Gia_ManForEachAnd( pPart, pObj, i ) + Gia_ManForEachCand( pPart, pObj, i ) if ( pCnf->pVarNums[i] >= 0 ) + { + assert( Gia_ObjIsCi(pObj) || Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, i) ) == -1 ); Vec_IntWriteEntry( vSatMap, Vec_IntEntry(vPartMap, i), pCnf->pVarNums[i] ); + } Cnf_DataFree( pCnf ); Gia_ManStop( pPart ); // perform runs - fChanges = 0; + nChanges = 0; Vec_IntForEachEntry( vMiters, iLit, i ) { if ( iLit == -1 ) continue; + assert( Vec_IntEntry(vSatMap, Abc_Lit2Var(iLit)) > 0 ); + iLit = Abc_Lit2LitV( Vec_IntArray(vSatMap), iLit ); status = sat_solver_solve( pSat, &iLit, &iLit + 1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_True ) + { + nChanges++; continue; + } if ( status == l_Undef ) { printf( "Timeout reached after %d seconds. \n", nTimeOut ); @@ -254,17 +277,26 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int assert( status == l_False ); iLit0 = Vec_IntEntry( vLits0, i ); iLit1 = Vec_IntEntry( vLits1, i ); - assert( (iLit0 > 2 || iLit1 > 2) && iLit0 != iLit1 ); - if ( iLit1 > 2 ) + assert( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 ); + if ( iLit1 >= 2 ) Vec_IntWriteEntry( vLits1, i, iLit0 ); else Vec_IntWriteEntry( vLits0, i, iLit1 ); iLit0 = Vec_IntEntry( vLits0, i ); iLit1 = Vec_IntEntry( vLits1, i ); assert( iLit0 == iLit1 ); - fChanges = 1; } - if ( !fChanges ) + if ( fVerbose ) + { + printf( "Vars =%7d ", nSatVars ); + printf( "Clause =%10d ", sat_solver_nclauses(pSat) ); + printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) ); + printf( "AIG =%7d ", Gia_ManAndNum(pNew) ); + printf( "Miters =%5d ", nMiters ); + printf( "SAT =%5d ", nChanges ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + if ( nChanges == 0 ) { printf( "Reached a fixed point after %d frames. \n", f+1 ); break; @@ -279,6 +311,7 @@ cleanup: Vec_IntFree( vMiters ); Vec_IntFree( vSatMap ); Vec_IntFree( vPartMap ); + Vec_IntFree( vCopies ); return RetValue; } @@ -293,9 +326,11 @@ cleanup: SeeAlso [] ***********************************************************************/ -void Bmc_LilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int fVerbose ) +void Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ) { - Bmc_LilacPerform( p, vInit, vInit, nFrames, fVerbose ); + Vec_Int_t * vInit0 = Vec_IntStart( Gia_ManRegNum(p) ); + Bmc_LilacPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose ); + Vec_IntFree( vInit0 ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bmc/bmcTulip.c b/src/sat/bmc/bmcTulip.c index 29e8781f..8c32d699 100644 --- a/src/sat/bmc/bmcTulip.c +++ b/src/sat/bmc/bmcTulip.c @@ -481,9 +481,9 @@ Vec_Int_t * Gia_ManRosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, Gia_ParTestFree( p ); printf( "After %d frames, found a sequence to produce %d x-values (out of %d). ", f, Cost, Gia_ManRegNum(p) ); Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); -// Vec_IntFreeP( &vInit ); Vec_IntFill(vInit, Vec_IntSize(vInit), 2); // printf( "The resulting init state is invalid.\n" ); + Vec_IntFreeP( &vInit ); return vInit; } @@ -505,7 +505,6 @@ Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int vRes = Gia_ManRosePerform( p, vInit, nFrames, nWords, fVerbose ); else vRes = Gia_ManTulipPerform( p, vInit, nFrames, nTimeOut, fVerbose ); - Vec_IntFreeP( &vRes ); return vRes; } |