luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Experiments with recent ideas.

This commit is contained in:
Alan Mishchenko 2014-03-19 22:15:02 -07:00
parent 37bbbcb2b4
commit 86d3c72beb
5 changed files with 202 additions and 187 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

152
abclib.dsp
View File

@ -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"

39
src/aig/gia/giaMan.c
View File

@ -291,6 +291,43 @@ void Gia_ManPrintTents( Gia_Man_t * p )
// Gia_ObjPrint( p, pObj );
}
/**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.]
@ -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 )
{
/*

96
src/base/abci/abc.c
View File

@ -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 );

99
src/sat/bmc/bmcLilac.c
View File

@ -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 );
}
////////////////////////////////////////////////////////////////////////

3
src/sat/bmc/bmcTulip.c
View File

@ -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;
}