mirror of https://github.com/YosysHQ/abc.git
Experiments with recent ideas.
This commit is contained in:
Alan Mishchenko
parent
c1e54b8b76
commit
d44d9e2927
|
|
@ -32845,8 +32845,7 @@ usage:
|
|||
***********************************************************************/
|
||||
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;
|
||||
extern int Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
|
||||
int c, nFrames = 1000, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "FWTsvh" ) ) != EOF )
|
||||
|
|
@ -32908,8 +32907,12 @@ int Abc_CommandAbc9Lilac( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
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 );
|
||||
if ( pAbc->pGia->vInitClasses == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Abc_CommandAbc9Lilac(): Init array is not given.\n" );
|
||||
return 0;
|
||||
}
|
||||
Gia_ManLilacTest( pAbc->pGia, pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
|
|
|
|||
|
|
@ -183,6 +183,8 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int
|
|||
sat_solver * pSat;
|
||||
int iVar0, iVar1, iLit, iLit0, iLit1;
|
||||
int i, f, status, nChanges, nMiters, RetValue = 1;
|
||||
assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) );
|
||||
assert( Vec_IntSize(vInit1) == Gia_ManRegNum(p) );
|
||||
|
||||
// start the SAT solver
|
||||
pSat = sat_solver_new();
|
||||
|
|
@ -325,11 +327,12 @@ cleanup:
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
|
||||
int Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
|
||||
{
|
||||
Vec_Int_t * vInit0 = Vec_IntStart( Gia_ManRegNum(p) );
|
||||
Bmc_LilacPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose );
|
||||
Vec_IntFree( vInit0 );
|
||||
return 1;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -38,220 +38,6 @@ static inline word * Gia_ParTestObj( Gia_Man_t * p, int Id ) { return (wor
|
|||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
|
||||
{
|
||||
Cnf_Dat_t * pCnf;
|
||||
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
|
||||
pAig->nRegs = 0;
|
||||
pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
|
||||
Aig_ManStop( pAig );
|
||||
return pCnf;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars, Vec_Int_t * vInit )
|
||||
{
|
||||
Gia_Man_t * pNew, * pTemp;
|
||||
Gia_Obj_t * pObj;
|
||||
int i, f;
|
||||
pNew = Gia_ManStart( fUseVars * 2 * Gia_ManRegNum(p) + nFrames * Gia_ManObjNum(p) );
|
||||
pNew->pName = Abc_UtilStrsav( p->pName );
|
||||
Gia_ManHashAlloc( pNew );
|
||||
Gia_ManConst0(p)->Value = 0;
|
||||
// control/data variables
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
Gia_ManAppendCi( pNew );
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
Gia_ManAppendCi( pNew );
|
||||
// build timeframes
|
||||
assert( !vInit || Vec_IntSize(vInit) == Gia_ManRegNum(p) );
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
{
|
||||
if ( vInit == NULL ) // assume 2
|
||||
pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0;
|
||||
else if ( Vec_IntEntry(vInit, i) == 0 )
|
||||
pObj->Value = 0;
|
||||
else if ( Vec_IntEntry(vInit, i) == 1 )
|
||||
pObj->Value = 1;
|
||||
else if ( Vec_IntEntry(vInit, i) == 2 )
|
||||
pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0;
|
||||
else if ( Vec_IntEntry(vInit, i) == 3 )
|
||||
pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 1;
|
||||
else assert( 0 );
|
||||
}
|
||||
for ( f = 0; f < nFrames; f++ )
|
||||
{
|
||||
Gia_ManForEachPi( p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCi( pNew );
|
||||
Gia_ManForEachAnd( p, pObj, i )
|
||||
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
|
||||
Gia_ManForEachRi( p, pObj, i )
|
||||
pObj->Value = Gia_ObjFanin0Copy(pObj);
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
pObj->Value = Gia_ObjRoToRi(p, pObj)->Value;
|
||||
}
|
||||
Gia_ManForEachRi( p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
|
||||
pNew = Gia_ManCleanup( pTemp = pNew );
|
||||
Gia_ManStop( pTemp );
|
||||
assert( Gia_ManPiNum(pNew) == 2 * Gia_ManRegNum(p) + nFrames * Gia_ManPiNum(p) );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Gia_ManTulipPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nTimeOut, int fVerbose )
|
||||
{
|
||||
int nIterMax = 1000000;
|
||||
int i, iLit, Iter, status;
|
||||
int nLits, * pLits;
|
||||
abctime clkTotal = Abc_Clock();
|
||||
abctime clkSat = 0;
|
||||
Vec_Int_t * vLits, * vMap;
|
||||
sat_solver * pSat;
|
||||
Gia_Obj_t * pObj;
|
||||
Gia_Man_t * p0 = Gia_ManTulipUnfold( p, nFrames, 0, vInit );
|
||||
Gia_Man_t * p1 = Gia_ManTulipUnfold( p, nFrames, 1, vInit );
|
||||
Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
|
||||
Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM );
|
||||
Gia_ManStop( p0 );
|
||||
Gia_ManStop( p1 );
|
||||
assert( Gia_ManRegNum(p) > 0 );
|
||||
if ( fVerbose )
|
||||
printf( "Running with %d frames and %sgiven init state.\n", nFrames, vInit ? "":"no " );
|
||||
|
||||
pSat = sat_solver_new();
|
||||
sat_solver_setnvars( pSat, pCnf->nVars );
|
||||
sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
|
||||
for ( i = 0; i < pCnf->nClauses; i++ )
|
||||
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
|
||||
assert( 0 );
|
||||
|
||||
// add one large OR clause
|
||||
vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
|
||||
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) );
|
||||
|
||||
// create assumptions
|
||||
Vec_IntClear( vLits );
|
||||
Gia_ManForEachPi( pM, pObj, i )
|
||||
if ( i == Gia_ManRegNum(p) )
|
||||
break;
|
||||
else if ( vInit == NULL || (Vec_IntEntry(vInit, i) & 2) )
|
||||
Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1) );
|
||||
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Iter%6d : ", 0 );
|
||||
printf( "Var =%10d ", sat_solver_nvars(pSat) );
|
||||
printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
|
||||
printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
|
||||
printf( "Subset =%6d ", Vec_IntSize(vLits) );
|
||||
Abc_PrintTime( 1, "Time", clkSat );
|
||||
// ABC_PRTr( "Solver time", clkSat );
|
||||
}
|
||||
for ( Iter = 0; Iter < nIterMax; Iter++ )
|
||||
{
|
||||
abctime clk = Abc_Clock();
|
||||
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (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 ( fVerbose )
|
||||
// printf( "\n" );
|
||||
printf( "Timeout reached after %d seconds and %d iterations. ", nTimeOut, Iter );
|
||||
break;
|
||||
}
|
||||
if ( status == l_True )
|
||||
{
|
||||
// if ( fVerbose )
|
||||
// printf( "\n" );
|
||||
printf( "The problem is SAT after %d iterations. ", Iter );
|
||||
break;
|
||||
}
|
||||
assert( status == l_False );
|
||||
nLits = sat_solver_final( pSat, &pLits );
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Iter%6d : ", Iter+1 );
|
||||
printf( "Var =%10d ", sat_solver_nvars(pSat) );
|
||||
printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
|
||||
printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
|
||||
printf( "Subset =%6d ", nLits );
|
||||
Abc_PrintTime( 1, "Time", clkSat );
|
||||
// ABC_PRTr( "Solver time", clkSat );
|
||||
}
|
||||
if ( Vec_IntSize(vLits) == nLits )
|
||||
{
|
||||
// if ( fVerbose )
|
||||
// printf( "\n" );
|
||||
printf( "Reached fixed point with %d entries after %d iterations. ", Vec_IntSize(vLits), Iter+1 );
|
||||
break;
|
||||
}
|
||||
// collect used literals
|
||||
Vec_IntClear( vLits );
|
||||
for ( i = 0; i < nLits; i++ )
|
||||
Vec_IntPush( vLits, Abc_LitNot(pLits[i]) );
|
||||
}
|
||||
// create map
|
||||
vMap = Vec_IntStart( pCnf->nVars );
|
||||
Vec_IntForEachEntry( vLits, iLit, i )
|
||||
Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLit), 1 );
|
||||
|
||||
// create output
|
||||
Vec_IntFree( vLits );
|
||||
if ( vInit )
|
||||
vLits = Vec_IntDup(vInit);
|
||||
else
|
||||
vLits = Vec_IntAlloc(Gia_ManRegNum(p)), Vec_IntFill(vLits, Gia_ManRegNum(p), 2);
|
||||
Gia_ManForEachPi( pM, pObj, i )
|
||||
if ( i == Gia_ManRegNum(p) )
|
||||
break;
|
||||
else if ( (Vec_IntEntry(vLits, i) & 2) && Vec_IntEntry( vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ) )
|
||||
Vec_IntWriteEntry( vLits, i, (Vec_IntEntry(vLits, i) & 1) );
|
||||
Vec_IntFree( vMap );
|
||||
|
||||
// cleanup
|
||||
sat_solver_delete( pSat );
|
||||
Cnf_DataFree( pCnf );
|
||||
Gia_ManStop( pM );
|
||||
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
|
||||
return vLits;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -272,10 +58,7 @@ void Gia_ManRoseInit( Gia_Man_t * p, Vec_Int_t * vInit )
|
|||
{
|
||||
pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
|
||||
pData1 = pData0 + p->iData;
|
||||
if ( vInit == NULL ) // X
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
pData0[i] = pData1[i] = 0;
|
||||
else if ( Vec_IntEntry(vInit, k) == 0 ) // 0
|
||||
if ( Vec_IntEntry(vInit, k) == 0 ) // 0
|
||||
for ( i = 0; i < p->iData; i++ )
|
||||
pData0[i] = ~(word)0, pData1[i] = 0;
|
||||
else if ( Vec_IntEntry(vInit, k) == 1 ) // 1
|
||||
|
|
@ -453,11 +236,7 @@ Vec_Int_t * Gia_ManRosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames,
|
|||
Gia_ManRandomW( 1 );
|
||||
if ( fVerbose )
|
||||
printf( "Running with %d frames, %d words, and %sgiven init state.\n", nFrames, nWords, vInit0 ? "":"no " );
|
||||
if ( vInit0 )
|
||||
vInit = Vec_IntDup(vInit0);
|
||||
else
|
||||
vInit = Vec_IntAlloc(Gia_ManRegNum(p)), Vec_IntFill(vInit, Gia_ManRegNum(p), 2);
|
||||
assert( Vec_IntSize(vInit) == Gia_ManRegNum(p) );
|
||||
vInit = Vec_IntDup(vInit0);
|
||||
Gia_ParTestAlloc( p, nWords );
|
||||
Gia_ManRoseInit( p, vInit );
|
||||
Cost0 = 0;
|
||||
|
|
@ -481,12 +260,33 @@ 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_IntFill(vInit, Vec_IntSize(vInit), 2);
|
||||
// printf( "The resulting init state is invalid.\n" );
|
||||
Vec_IntFreeP( &vInit );
|
||||
return vInit;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
|
||||
{
|
||||
Cnf_Dat_t * pCnf;
|
||||
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
|
||||
pAig->nRegs = 0;
|
||||
pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
|
||||
Aig_ManStop( pAig );
|
||||
return pCnf;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -498,13 +298,209 @@ Vec_Int_t * Gia_ManRosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames,
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
|
||||
Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars, Vec_Int_t * vInit )
|
||||
{
|
||||
Vec_Int_t * vRes;
|
||||
Gia_Man_t * pNew, * pTemp;
|
||||
Gia_Obj_t * pObj;
|
||||
int i, f;
|
||||
pNew = Gia_ManStart( fUseVars * 2 * Gia_ManRegNum(p) + nFrames * Gia_ManObjNum(p) );
|
||||
pNew->pName = Abc_UtilStrsav( p->pName );
|
||||
Gia_ManHashAlloc( pNew );
|
||||
Gia_ManConst0(p)->Value = 0;
|
||||
// control/data variables
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
Gia_ManAppendCi( pNew );
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
Gia_ManAppendCi( pNew );
|
||||
// build timeframes
|
||||
assert( !vInit || Vec_IntSize(vInit) == Gia_ManRegNum(p) );
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
{
|
||||
if ( Vec_IntEntry(vInit, i) == 0 )
|
||||
pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0;
|
||||
else if ( Vec_IntEntry(vInit, i) == 1 )
|
||||
pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 1;
|
||||
else if ( Vec_IntEntry(vInit, i) == 2 )
|
||||
pObj->Value = Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i));
|
||||
else if ( Vec_IntEntry(vInit, i) == 3 )
|
||||
pObj->Value = Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i));
|
||||
else assert( 0 );
|
||||
}
|
||||
for ( f = 0; f < nFrames; f++ )
|
||||
{
|
||||
Gia_ManForEachPi( p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCi( pNew );
|
||||
Gia_ManForEachAnd( p, pObj, i )
|
||||
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
|
||||
Gia_ManForEachRi( p, pObj, i )
|
||||
pObj->Value = Gia_ObjFanin0Copy(pObj);
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
pObj->Value = Gia_ObjRoToRi(p, pObj)->Value;
|
||||
}
|
||||
Gia_ManForEachRi( p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
|
||||
pNew = Gia_ManCleanup( pTemp = pNew );
|
||||
Gia_ManStop( pTemp );
|
||||
assert( Gia_ManPiNum(pNew) == 2 * Gia_ManRegNum(p) + nFrames * Gia_ManPiNum(p) );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Gia_ManTulipPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nTimeOut, int fVerbose )
|
||||
{
|
||||
int nIterMax = 1000000;
|
||||
int i, iLit, Iter, status;
|
||||
int nLits, * pLits;
|
||||
abctime clkTotal = Abc_Clock();
|
||||
abctime clkSat = 0;
|
||||
Vec_Int_t * vLits, * vMap;
|
||||
sat_solver * pSat;
|
||||
Gia_Obj_t * pObj;
|
||||
Gia_Man_t * p0 = Gia_ManTulipUnfold( p, nFrames, 0, vInit );
|
||||
Gia_Man_t * p1 = Gia_ManTulipUnfold( p, nFrames, 1, vInit );
|
||||
Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
|
||||
Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM );
|
||||
Gia_ManStop( p0 );
|
||||
Gia_ManStop( p1 );
|
||||
assert( Gia_ManRegNum(p) > 0 );
|
||||
if ( fVerbose )
|
||||
printf( "Running with %d frames and %sgiven init state.\n", nFrames, vInit ? "":"no " );
|
||||
|
||||
pSat = sat_solver_new();
|
||||
sat_solver_setnvars( pSat, pCnf->nVars );
|
||||
sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
|
||||
for ( i = 0; i < pCnf->nClauses; i++ )
|
||||
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
|
||||
assert( 0 );
|
||||
|
||||
// add one large OR clause
|
||||
vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
|
||||
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) );
|
||||
|
||||
// create assumptions
|
||||
Vec_IntClear( vLits );
|
||||
Gia_ManForEachPi( pM, pObj, i )
|
||||
if ( i == Gia_ManRegNum(p) )
|
||||
break;
|
||||
else if ( !(Vec_IntEntry(vInit, i) & 2) )
|
||||
Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1) );
|
||||
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Iter%6d : ", 0 );
|
||||
printf( "Var =%10d ", sat_solver_nvars(pSat) );
|
||||
printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
|
||||
printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
|
||||
printf( "Subset =%6d ", Vec_IntSize(vLits) );
|
||||
Abc_PrintTime( 1, "Time", clkSat );
|
||||
// ABC_PRTr( "Solver time", clkSat );
|
||||
}
|
||||
for ( Iter = 0; Iter < nIterMax; Iter++ )
|
||||
{
|
||||
abctime clk = Abc_Clock();
|
||||
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (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 ( fVerbose )
|
||||
// printf( "\n" );
|
||||
printf( "Timeout reached after %d seconds and %d iterations. ", nTimeOut, Iter );
|
||||
break;
|
||||
}
|
||||
if ( status == l_True )
|
||||
{
|
||||
// if ( fVerbose )
|
||||
// printf( "\n" );
|
||||
printf( "The problem is SAT after %d iterations. ", Iter );
|
||||
break;
|
||||
}
|
||||
assert( status == l_False );
|
||||
nLits = sat_solver_final( pSat, &pLits );
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Iter%6d : ", Iter+1 );
|
||||
printf( "Var =%10d ", sat_solver_nvars(pSat) );
|
||||
printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
|
||||
printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
|
||||
printf( "Subset =%6d ", nLits );
|
||||
Abc_PrintTime( 1, "Time", clkSat );
|
||||
// ABC_PRTr( "Solver time", clkSat );
|
||||
}
|
||||
if ( Vec_IntSize(vLits) == nLits )
|
||||
{
|
||||
// if ( fVerbose )
|
||||
// printf( "\n" );
|
||||
printf( "Reached fixed point with %d entries after %d iterations. ", Vec_IntSize(vLits), Iter+1 );
|
||||
break;
|
||||
}
|
||||
// collect used literals
|
||||
Vec_IntClear( vLits );
|
||||
for ( i = 0; i < nLits; i++ )
|
||||
Vec_IntPush( vLits, Abc_LitNot(pLits[i]) );
|
||||
}
|
||||
// create map
|
||||
vMap = Vec_IntStart( pCnf->nVars );
|
||||
Vec_IntForEachEntry( vLits, iLit, i )
|
||||
Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLit), 1 );
|
||||
|
||||
// create output
|
||||
Vec_IntFree( vLits );
|
||||
vLits = Vec_IntDup(vInit);
|
||||
Gia_ManForEachPi( pM, pObj, i )
|
||||
if ( i == Gia_ManRegNum(p) )
|
||||
break;
|
||||
else if ( !(Vec_IntEntry(vLits, i) & 2) && !Vec_IntEntry(vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) )
|
||||
Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) | 2 );
|
||||
Vec_IntFree( vMap );
|
||||
|
||||
// cleanup
|
||||
sat_solver_delete( pSat );
|
||||
Cnf_DataFree( pCnf );
|
||||
Gia_ManStop( pM );
|
||||
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
|
||||
return vLits;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
|
||||
{
|
||||
Vec_Int_t * vRes, * vInit;
|
||||
if ( fSim )
|
||||
{
|
||||
vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 );
|
||||
vRes = Gia_ManRosePerform( p, vInit, nFrames, nWords, fVerbose );
|
||||
}
|
||||
else
|
||||
{
|
||||
vInit = vInit0 ? vInit0 : Vec_IntStart( Gia_ManRegNum(p) );
|
||||
vRes = Gia_ManTulipPerform( p, vInit, nFrames, nTimeOut, fVerbose );
|
||||
}
|
||||
if ( vInit != vInit0 )
|
||||
Vec_IntFree( vInit );
|
||||
return vRes;
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue