Skip to content

A
abc
Commit bc81cf2d by Alan Mishchenko
Options

Improvements to the new abstraction code.

parent 1dcdba1b
Showing with 156 additions and 83 deletions
src/aig/gia/giaAbs.c
......@@ -379,25 +379,29 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
***********************************************************************/
int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
{
extern Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
extern Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Vec_Int_t * vGateClasses;
Vec_Int_t * vGateClasses, * vGateClassesOld = NULL;
Aig_Man_t * pAig;
/*
// check if flop classes are given
if ( pGia->vGateClasses == NULL )
Abc_Print( 0, "Initial gate map is not given. Abstraction begins from scratch.\n" );
else
{
Abc_Print( 0, "Initial gate map is not given. Trivial abstraction is assumed.\n" );
pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pGia) );
Abc_Print( 0, "Initial gate map is given. Abstraction refines this map.\n" );
vGateClassesOld = pGia->vGateClasses; pGia->vGateClasses = NULL;
fNaiveCnf = 1;
}
*/
// perform abstraction
pAig = Gia_ManToAigSimple( pGia );
vGateClasses = Aig_Gla1ManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
assert( vGateClassesOld == NULL || Vec_IntSize(vGateClassesOld) == Aig_ManObjNumMax(pAig) );
vGateClasses = Aig_Gla1ManTest( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
Aig_ManStop( pAig );
// update the map
Vec_IntFreeP( &pGia->vGateClasses );
Vec_IntFreeP( &vGateClassesOld );
pGia->vGateClasses = vGateClasses;
return 1;
}
......@@ -415,26 +419,63 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
***********************************************************************/
int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
{
extern Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose );
extern Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose );
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Vec_Int_t * vGateClasses;
Aig_Man_t * pAig;
/*
// check if flop classes are given
if ( pGia->vGateClasses == NULL )
{
Abc_Print( 0, "Initial gate map is not given. Trivial abstraction is assumed.\n" );
pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pGia) );
Abc_Print( 0, "Initial gate map is not given. Abstraction begins from scratch.\n" );
pAig = Gia_ManToAigSimple( pGia );
}
else
{
Gia_Man_t * pGiaAbs;
Abc_Print( 0, "Initial gate map is given. Abstraction refines this map.\n" );
pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses );
pAig = Gia_ManToAigSimple( pGiaAbs );
Gia_ManStop( pGiaAbs );
}
*/
// perform abstraction
pAig = Gia_ManToAigSimple( pGia );
vGateClasses = Aig_Gla2ManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
vGateClasses = Aig_Gla2ManTest( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
Aig_ManStop( pAig );
// update the map
// update the BMC depth
if ( vGateClasses )
p->iFrame = p->nFramesMax;
// update the abstraction map (hint: AIG and GIA have one-to-one obj ID match)
if ( pGia->vGateClasses && vGateClasses )
{
Gia_Obj_t * pObj;
int i, Counter = 0;
Gia_ManForEachObj1( pGia, pObj, i )
{
if ( !~pObj->Value )
continue;
if ( !Vec_IntEntry(pGia->vGateClasses, i) )
continue;
// this obj was abstracted before
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(pGia, pObj) );
// if corresponding AIG object is not abstracted, remove abstraction
if ( !Vec_IntEntry(vGateClasses, Gia_Lit2Var(pObj->Value)) )
{
Vec_IntWriteEntry( pGia->vGateClasses, i, 0 );
Counter++;
}
}
Vec_IntFree( vGateClasses );
if ( p->fVerbose )
Abc_Print( 1, "Repetition of abstraction removed %d entries from the old abstraction map.\n", Counter );
}
else
{
Vec_IntFreeP( &pGia->vGateClasses );
pGia->vGateClasses = vGateClasses;
}
return 1;
}
......
src/aig/saig/saigGlaCba.c
......@@ -151,43 +151,6 @@ static inline int Aig_Gla1AddNode( sat_solver * pSat, int iVar, int iVar0, int i
/**Function*************************************************************
Synopsis [Returns the array of neighbors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_Gla1CollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vAssigned;
Aig_Obj_t * pObj;
int i, Entry;
vAssigned = Vec_IntAlloc( 1000 );
Vec_IntForEachEntry( vGateClasses, Entry, i )
{
if ( Entry == 0 )
continue;
assert( Entry == 1 );
pObj = Aig_ManObj( p, i );
Vec_IntPush( vAssigned, Aig_ObjId(pObj) );
if ( Aig_ObjIsNode(pObj) )
{
Vec_IntPush( vAssigned, Aig_ObjFaninId0(pObj) );
Vec_IntPush( vAssigned, Aig_ObjFaninId1(pObj) );
}
else if ( Saig_ObjIsLo(p, pObj) )
Vec_IntPush( vAssigned, Aig_ObjFaninId0(Saig_ObjLoToLi(p, pObj)) );
else assert( Aig_ObjIsConst1(pObj) );
}
Vec_IntUniqify( vAssigned );
return vAssigned;
}
/**Function*************************************************************
Synopsis [Derives abstraction components (PIs, PPIs, flops, nodes).]
Description []
......@@ -446,6 +409,44 @@ int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
/**Function*************************************************************
Synopsis [Returns the array of neighbors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_Gla1CollectAssigned( Aig_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vAssigned;
Aig_Obj_t * pObj;
int i, Entry;
vAssigned = Vec_IntAlloc( 1000 );
Vec_IntForEachEntry( vGateClasses, Entry, i )
{
if ( Entry == 0 )
continue;
assert( Entry == 1 );
pObj = Aig_ManObj( p, i );
Vec_IntPush( vAssigned, Aig_ObjId(pObj) );
if ( Aig_ObjIsNode(pObj) )
{
Vec_IntPush( vAssigned, Aig_ObjFaninId0(pObj) );
Vec_IntPush( vAssigned, Aig_ObjFaninId1(pObj) );
}
else if ( Saig_ObjIsLo(p, pObj) )
Vec_IntPush( vAssigned, Aig_ObjFaninId0(Saig_ObjLoToLi(p, pObj)) );
else assert( Aig_ObjIsConst1(pObj) );
}
Vec_IntUniqify( vAssigned );
Vec_IntReverseOrder( vAssigned );
return vAssigned;
}
/**Function*************************************************************
Synopsis []
Description []
......@@ -455,16 +456,25 @@ int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
SeeAlso []
***********************************************************************/
Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, int fNaiveCnf )
Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int fNaiveCnf )
{
Aig_Gla1Man_t * p;
int i;
p = ABC_CALLOC( Aig_Gla1Man_t, 1 );
p->pAig = pAig;
p->nFrames = 32;
if ( vGateClassesOld )
{
p->vAssigned = Aig_Gla1CollectAssigned( pAig, vGateClassesOld );
p->vIncluded = Vec_IntDup( vGateClassesOld );
assert( fNaiveCnf );
}
else
{
p->vAssigned = Vec_IntAlloc( 1000 );
p->vIncluded = Vec_IntStart( Aig_ManObjNumMax(pAig) );
p->nFrames = 32;
}
p->vPis = Vec_IntAlloc( 1000 );
p->vPPis = Vec_IntAlloc( 1000 );
......@@ -651,9 +661,8 @@ void Aig_Gla1ExtendIncluded( Aig_Gla1Man_t * p )
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
{
int nStart = 0;
Vec_Int_t * vResult = NULL;
Aig_Gla1Man_t * p;
Aig_Man_t * pAbs;
......@@ -664,6 +673,9 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
int nConfBef, nConfAft, clk, clkTotal = clock();
assert( Saig_ManPoNum(pAig) == 1 );
if ( nFramesMax == 0 )
nFramesMax = ABC_INFINITY;
if ( fVerbose )
{
if ( TimeLimit )
......@@ -673,7 +685,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
}
// start the solver
p = Aig_Gla1ManStart( pAig, fNaiveCnf );
p = Aig_Gla1ManStart( pAig, vGateClassesOld, fNaiveCnf );
p->nFramesMax = nFramesMax;
p->nConfLimit = nConfLimit;
p->fVerbose = fVerbose;
......@@ -695,6 +707,10 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
if ( !Aig_Gla1ObjAddToSolver( p, pObj, f ) )
printf( "Error! SAT solver became UNSAT.\n" );
// skip checking if we are not supposed to
if ( f < nStart )
continue;
// create output literal to represent property failure
pObj = Aig_ManPo( pAig, 0 );
iSatVar = Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObj), f );
......@@ -702,7 +718,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
// try solving the abstraction
Aig_Gla1CollectAbstr( p );
for ( r = 0; r < 1000000; r++ )
for ( r = 0; r < ABC_INFINITY; r++ )
{
// try to find a counter-example
clk = clock();
......@@ -724,7 +740,10 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
else if ( RetValue != l_False )
printf( " SAT solver returned UNDECIDED after %5d conflicts.\n", nConfAft - nConfBef );
else
printf( " SAT solver returned UNSAT after %5d conflicts.\n", nConfAft - nConfBef );
{
printf( " SAT solver returned UNSAT after %5d conflicts. ", nConfAft - nConfBef );
Abc_PrintTime( 1, "Total time", clock() - clkTotal );
}
}
break;
}
......
src/aig/saig/saigGlaPba.c
......@@ -34,7 +34,7 @@ struct Aig_Gla2Man_t_
{
// user data
Aig_Man_t * pAig;
int nConfMax;
int nStart;
int nFramesMax;
int fVerbose;
// unrolling
......@@ -226,8 +226,8 @@ int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
int i, f, ObjId, nVars, RetValue = 1;
// assign variables
// for ( f = p->nFramesMax - 1; f >= 0; f-- )
for ( f = 0; f < p->nFramesMax; f++ )
for ( f = p->nFramesMax - 1; f >= 0; f-- )
// for ( f = 0; f < p->nFramesMax; f++ )
Aig_Gla2AssignVars_rec( p, Aig_ManPo(p->pAig, 0), f );
// create SAT solver
......@@ -301,7 +301,7 @@ int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
// add output clause
vPoLits = Vec_IntAlloc( p->nFramesMax );
for ( f = 0; f < p->nFramesMax; f++ )
for ( f = p->nStart; f < p->nFramesMax; f++ )
Vec_IntPush( vPoLits, 2 * Aig_Gla2FetchVar(p, Aig_ManPo(p->pAig, 0), f) );
RetValue &= sat_solver_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) );
Vec_IntFree( vPoLits );
......@@ -311,11 +311,12 @@ int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
assert( nVars == Vec_IntSize(p->vVar2Inf) );
assert( ((Sto_Man_t *)p->pSat->pStore)->nClauses == Vec_IntSize(p->vCla2Obj) );
// Sto_ManDumpClauses( ((Sto_Man_t *)p->pSat->pStore), "temp_sto.cnf" );
sat_solver_store_mark_roots( p->pSat );
if ( p->fVerbose )
printf( "The resulting SAT problem contains %d vars, %d clauses, and %d literals.\n",
p->pSat->size, p->pSat->stats.clauses, p->pSat->stats.tot_literals );
return RetValue;
}
......@@ -330,7 +331,7 @@ int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
SeeAlso []
***********************************************************************/
Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nFramesMax )
Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nStart, int nFramesMax, int fVerbose )
{
Aig_Gla2Man_t * p;
int i;
......@@ -345,7 +346,9 @@ Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nFramesMax )
p->vCla2Fra = Vec_IntAlloc( 1 << 20 );
// skip first vector ID
p->nStart = nStart;
p->nFramesMax = nFramesMax;
p->fVerbose = fVerbose;
for ( i = 0; i < p->nFramesMax; i++ )
Vec_IntPush( p->vVec2Var, -1 );
......@@ -416,7 +419,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
}
if ( fVerbose )
{
printf( "SAT solver returned UNSAT after %d conflicts. ", pSat->stats.conflicts );
printf( "SAT solver returned UNSAT after %7d conflicts. ", pSat->stats.conflicts );
ABC_PRT( "Time", clock() - clk );
}
assert( RetValue == l_False );
......@@ -428,7 +431,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
Intp_ManFree( pManProof );
if ( fVerbose )
{
printf( "SAT core contains %d clauses (out of %d). ", Vec_IntSize(vCore), ((Sto_Man_t *)pSatCnf)->nRoots );
printf( "SAT core contains %8d clauses (out of %8d). ", Vec_IntSize(vCore), ((Sto_Man_t *)pSatCnf)->nRoots );
ABC_PRT( "Time", clock() - clk );
}
Sto_ManFree( (Sto_Man_t *)pSatCnf );
......@@ -500,9 +503,8 @@ Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore )
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
{
int nStart = 0;
Aig_Gla2Man_t * p;
Vec_Int_t * vCore, * vResult;
int clk, clkTotal = clock();
......@@ -518,7 +520,7 @@ Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, i
// start the solver
clk = clock();
p = Aig_Gla2ManStart( pAig, nFramesMax );
p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose );
if ( !Aig_Gla2CreateSatSolver( p ) )
{
printf( "Error! SAT solver became UNSAT.\n" );
......
src/base/abci/abc.c
......@@ -29022,11 +29022,16 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
return 0;
}
if ( pPars->nFramesMax < 1 )
if ( pPars->nFramesMax < 0 )
{
Abc_Print( 1, "The number of frames should be a positive integer.\n" );
return 0;
}
if ( pPars->nStart > 0 && pPars->nStart >= pPars->nFramesMax )
{
Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
return 0;
}
pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf );
if ( pPars->nStart == 0 )
pAbc->nFrames = pPars->iFrame;
......@@ -29035,13 +29040,13 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &gla_cba [-FCT num] [-cvh]\n" );
Abc_Print( -2, "usage: &gla_cba [-SFCT num] [-cvh]\n" );
Abc_Print( -2, "\t refines abstracted object map with CEX-based abstraction\n" );
// Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll (0=unused) [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
// Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-T num : an approximate timeout in seconds (0=unused) [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-c : toggle using naive CNF computation [default = %s]\n", fNaiveCnf? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
......@@ -29145,19 +29150,25 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "The number of frames should be a positive integer.\n" );
return 0;
}
if ( pPars->nStart >= pPars->nFramesMax )
{
Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
return 0;
}
if ( pPars->nStart )
Abc_Print( 0, "The starting frame is specified. The resulting abstraction may be unsound.\n" );
pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars );
if ( pPars->nStart == 0 )
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
// printf( "This command is currently not enabled.\n" );
return 0;
usage:
Abc_Print( -2, "usage: &gla_pba [-FCT num] [-vh]\n" );
Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-vh]\n" );
Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" );
// Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment