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

New proof-based abstraction code.

This commit is contained in:
Alan Mishchenko 2011-10-25 18:32:06 +08:00
parent f7fd329787
commit 0f77840520
7 changed files with 747 additions and 64 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
abclib.dsp
View File

@ -3503,10 +3503,6 @@ SOURCE=.\src\aig\saig\saigAbsCba.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigAbsGla.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigAbsPba.c
# End Source File
# Begin Source File
@ -3551,6 +3547,14 @@ SOURCE=.\src\aig\saig\saigDup.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigGlaCba.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigGlaPba.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigHaig.c
# End Source File
# Begin Source File

3
src/aig/gia/gia.h
View File

@ -603,7 +603,8 @@ Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia );
int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame );
extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fUseCnf );
extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf );
extern int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars );
/*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName );
extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );

40
src/aig/gia/giaAbs.c
View File

@ -379,7 +379,7 @@ 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_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
extern Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Vec_Int_t * vGateClasses;
Aig_Man_t * pAig;
@ -393,7 +393,43 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
*/
// perform abstraction
pAig = Gia_ManToAigSimple( pGia );
vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
vGateClasses = Aig_Gla1ManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
Aig_ManStop( pAig );
// update the map
Vec_IntFreeP( &pGia->vGateClasses );
pGia->vGateClasses = vGateClasses;
return 1;
}
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 );
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) );
}
*/
// perform abstraction
pAig = Gia_ManToAigSimple( pGia );
vGateClasses = Aig_Gla2ManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
Aig_ManStop( pAig );
// update the map

3
src/aig/saig/module.make
View File

@ -1,6 +1,5 @@
SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigAbsCba.c \
src/aig/saig/saigAbsGla.c \
src/aig/saig/saigAbsPba.c \
src/aig/saig/saigAbsStart.c \
src/aig/saig/saigAbsVfa.c \
@ -12,6 +11,8 @@ SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigConstr.c \
src/aig/saig/saigConstr2.c \
src/aig/saig/saigDup.c \
src/aig/saig/saigGlaCba.c \
src/aig/saig/saigGlaPba.c \
src/aig/saig/saigHaig.c \
src/aig/saig/saigInd.c \
src/aig/saig/saigIoa.c \

102
src/aig/saig/saigAbsGla.c → src/aig/saig/saigGlaCba.c
View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [saigAbsGla.c]
FileName [saigGlaCba.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigAbsGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: saigGlaCba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@ -29,8 +29,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Aig_GlaMan_t_ Aig_GlaMan_t;
struct Aig_GlaMan_t_
typedef struct Aig_Gla1Man_t_ Aig_Gla1Man_t;
struct Aig_Gla1Man_t_
{
// user data
Aig_Man_t * pAig;
@ -79,7 +79,7 @@ struct Aig_GlaMan_t_
SeeAlso []
***********************************************************************/
static inline int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl )
static inline int Aig_Gla1AddConst( sat_solver * pSat, int iVar, int fCompl )
{
lit Lit = toLitCond( iVar, fCompl );
if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
@ -98,7 +98,7 @@ static inline int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl )
SeeAlso []
***********************************************************************/
static inline int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
static inline int Aig_Gla1AddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
{
lit Lits[2];
@ -126,7 +126,7 @@ static inline int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int
SeeAlso []
***********************************************************************/
static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
static inline int Aig_Gla1AddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
{
lit Lits[3];
@ -160,7 +160,7 @@ static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iV
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_GlaCollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses )
Vec_Int_t * Aig_Gla1CollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vAssigned;
Aig_Obj_t * pObj;
@ -197,7 +197,7 @@ Vec_Int_t * Aig_GlaCollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses )
SeeAlso []
***********************************************************************/
void Aig_GlaCollectAbstr( Aig_GlaMan_t * p )
void Aig_Gla1CollectAbstr( Aig_Gla1Man_t * p )
{
Aig_Obj_t * pObj;
int i, Entry;
@ -210,20 +210,20 @@ void Aig_GlaCollectAbstr( Aig_GlaMan_t * p )
assert( Entry == 1 );
pObj = Aig_ManObj( p->pAig, i );
if ( Vec_IntFind( p->vAssigned, Aig_ObjId(pObj) ) == -1 )
printf( "Aig_GlaCollectAbstr(): Object not found\n" );
printf( "Aig_Gla1CollectAbstr(): Object not found\n" );
if ( Aig_ObjIsNode(pObj) )
{
if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObj) ) == -1 )
printf( "Aig_GlaCollectAbstr(): Node's fanin is not found\n" );
printf( "Aig_Gla1CollectAbstr(): Node's fanin is not found\n" );
if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId1(pObj) ) == -1 )
printf( "Aig_GlaCollectAbstr(): Node's fanin is not found\n" );
printf( "Aig_Gla1CollectAbstr(): Node's fanin is not found\n" );
}
else if ( Saig_ObjIsLo(p->pAig, pObj) )
{
Aig_Obj_t * pObjLi;
pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObjLi) ) == -1 )
printf( "Aig_GlaCollectAbstr(): Flop's fanin is not found\n" );
printf( "Aig_Gla1CollectAbstr(): Flop's fanin is not found\n" );
}
else assert( Aig_ObjIsConst1(pObj) );
}
@ -258,13 +258,13 @@ void Aig_GlaCollectAbstr( Aig_GlaMan_t * p )
SeeAlso []
***********************************************************************/
void Aig_GlaDeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
void Aig_Gla1DeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
{
if ( pObj->pData )
return;
assert( Aig_ObjIsNode(pObj) );
Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin0(pObj) );
Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin1(pObj) );
Aig_Gla1DeriveAbs_rec( pNew, Aig_ObjFanin0(pObj) );
Aig_Gla1DeriveAbs_rec( pNew, Aig_ObjFanin1(pObj) );
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}
@ -279,7 +279,7 @@ void Aig_GlaDeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
Aig_Man_t * Aig_Gla1DeriveAbs( Aig_Gla1Man_t * p )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
@ -303,7 +303,7 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
// create internal nodes
Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i )
// pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_GlaDeriveAbs_rec( pNew, pObj );
Aig_Gla1DeriveAbs_rec( pNew, pObj );
// create PO
Saig_ManForEachPo( p->pAig, pObj, i )
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
@ -332,7 +332,7 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
SeeAlso []
***********************************************************************/
int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
int Aig_Gla1FetchVar( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
{
int i, iVecId, iSatVar;
assert( k < p->nFrames );
@ -368,7 +368,7 @@ int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
SeeAlso []
***********************************************************************/
int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
{
if ( k == p->nFrames )
{
@ -388,17 +388,17 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
assert( k < p->nFrames );
assert( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) );
if ( Aig_ObjIsConst1(pObj) )
return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 0 );
return Aig_Gla1AddConst( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 0 );
if ( Saig_ObjIsLo(p->pAig, pObj) )
{
Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
if ( k == 0 )
{
Aig_GlaFetchVar( p, Aig_ObjFanin0(pObjLi), 0 );
return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 1 );
Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObjLi), 0 );
return Aig_Gla1AddConst( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 1 );
}
return Aig_GlaAddBuffer( p->pSat, Aig_GlaFetchVar(p, pObj, k),
Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1),
return Aig_Gla1AddBuffer( p->pSat, Aig_Gla1FetchVar(p, pObj, k),
Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObjLi), k-1),
Aig_ObjFaninC0(pObjLi) );
}
else
@ -407,9 +407,9 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
int i, Entry;
assert( Aig_ObjIsNode(pObj) );
if ( p->vObj2Cnf == NULL )
return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k),
Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k),
Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k),
return Aig_Gla1AddNode( p->pSat, Aig_Gla1FetchVar(p, pObj, k),
Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObj), k),
Aig_Gla1FetchVar(p, Aig_ObjFanin1(pObj), k),
Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
// derive clauses
assert( pObj->fMarkA );
@ -422,7 +422,7 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
// derive variables
Cnf_CollectLeaves( pObj, p->vLeaves, 0 );
Vec_PtrForEachEntry( Aig_Obj_t *, p->vLeaves, pObj, i )
Aig_GlaFetchVar( p, pObj, k );
Aig_Gla1FetchVar( p, pObj, k );
// translate clauses
assert( Vec_IntSize(vClauses) >= 2 );
assert( Vec_IntEntry(vClauses, 0) == 0 );
@ -433,7 +433,7 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
Vec_IntClear( p->vLits );
continue;
}
Vec_IntPush( p->vLits, (Entry & 1) ^ (2 * Aig_GlaFetchVar(p, Aig_ManObj(p->pAig, Entry >> 1), k)) );
Vec_IntPush( p->vLits, (Entry & 1) ^ (2 * Aig_Gla1FetchVar(p, Aig_ManObj(p->pAig, Entry >> 1), k)) );
if ( i == Vec_IntSize(vClauses) - 1 || Vec_IntEntry(vClauses, i+1) == 0 )
{
if ( !sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits)+Vec_IntSize(p->vLits) ) )
@ -455,12 +455,12 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
SeeAlso []
***********************************************************************/
Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fNaiveCnf )
Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, int fNaiveCnf )
{
Aig_GlaMan_t * p;
Aig_Gla1Man_t * p;
int i;
p = ABC_CALLOC( Aig_GlaMan_t, 1 );
p = ABC_CALLOC( Aig_Gla1Man_t, 1 );
p->pAig = pAig;
p->vAssigned = Vec_IntAlloc( 1000 );
p->vIncluded = Vec_IntStart( Aig_ManObjNumMax(pAig) );
@ -511,7 +511,7 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fNaiveCnf )
SeeAlso []
***********************************************************************/
void Aig_GlaManStop( Aig_GlaMan_t * p )
void Aig_Gla1ManStop( Aig_Gla1Man_t * p )
{
Vec_IntFreeP( &p->vAssigned );
Vec_IntFreeP( &p->vIncluded );
@ -551,7 +551,7 @@ void Aig_GlaManStop( Aig_GlaMan_t * p )
SeeAlso []
***********************************************************************/
Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p, int iFrame )
Abc_Cex_t * Aig_Gla1DeriveCex( Aig_Gla1Man_t * p, int iFrame )
{
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
@ -600,7 +600,7 @@ Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p, int iFrame )
SeeAlso []
***********************************************************************/
void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c )
void Aig_Gla1PrintAbstr( Aig_Gla1Man_t * p, int f, int r, int v, int c )
{
if ( r == 0 )
printf( "== %3d ==", f );
@ -621,7 +621,7 @@ void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c )
SeeAlso []
***********************************************************************/
void Aig_GlaExtendIncluded( Aig_GlaMan_t * p )
void Aig_Gla1ExtendIncluded( Aig_Gla1Man_t * p )
{
Aig_Obj_t * pObj;
int i, k;
@ -651,11 +651,11 @@ void Aig_GlaExtendIncluded( Aig_GlaMan_t * p )
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
{
int nStart = 0;
Vec_Int_t * vResult = NULL;
Aig_GlaMan_t * p;
Aig_Gla1Man_t * p;
Aig_Man_t * pAbs;
Aig_Obj_t * pObj;
Abc_Cex_t * pCex;
@ -673,14 +673,14 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
}
// start the solver
p = Aig_GlaManStart( pAig, fNaiveCnf );
p = Aig_Gla1ManStart( pAig, fNaiveCnf );
p->nFramesMax = nFramesMax;
p->nConfLimit = nConfLimit;
p->fVerbose = fVerbose;
// include constant node
Vec_IntWriteEntry( p->vIncluded, 0, 1 );
Aig_GlaFetchVar( p, Aig_ManConst1(pAig), 0 );
Aig_Gla1FetchVar( p, Aig_ManConst1(pAig), 0 );
// set runtime limit
if ( TimeLimit )
@ -692,16 +692,16 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
// initialize abstraction in this timeframe
Aig_ManForEachObjVec( p->vAssigned, pAig, pObj, i )
if ( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) )
if ( !Aig_GlaObjAddToSolver( p, pObj, f ) )
if ( !Aig_Gla1ObjAddToSolver( p, pObj, f ) )
printf( "Error! SAT solver became UNSAT.\n" );
// create output literal to represent property failure
pObj = Aig_ManPo( pAig, 0 );
iSatVar = Aig_GlaFetchVar( p, Aig_ObjFanin0(pObj), f );
iSatVar = Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObj), f );
Lit = toLitCond( iSatVar, Aig_ObjFaninC0(pObj) );
// try solving the abstraction
Aig_GlaCollectAbstr( p );
Aig_Gla1CollectAbstr( p );
for ( r = 0; r < 1000000; r++ )
{
// try to find a counter-example
@ -730,9 +730,9 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
}
clk = clock();
// derive abstraction
pAbs = Aig_GlaDeriveAbs( p );
pAbs = Aig_Gla1DeriveAbs( p );
// derive counter-example
pCex = Aig_GlaDeriveCex( p, f );
pCex = Aig_Gla1DeriveCex( p, f );
// verify the counter-example
RetValue = Saig_ManVerifyCex( pAbs, pCex );
if ( RetValue == 0 )
@ -746,7 +746,7 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
assert( Vec_IntEntry( p->vIncluded, Aig_ObjId(pObj) ) == 0 );
Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 );
for ( g = 0; g <= f; g++ )
if ( !Aig_GlaObjAddToSolver( p, pObj, g ) )
if ( !Aig_Gla1ObjAddToSolver( p, pObj, g ) )
printf( "Error! SAT solver became UNSAT.\n" );
}
if ( Vec_IntSize(vPPiRefine) == 0 )
@ -763,9 +763,9 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
p->timeRef += clock() - clk;
// prepare abstraction
Aig_GlaCollectAbstr( p );
Aig_Gla1CollectAbstr( p );
if ( fVerbose )
Aig_GlaPrintAbstr( p, f, r, p->pSat->size, nConfAft - nConfBef );
Aig_Gla1PrintAbstr( p, f, r, p->pSat->size, nConfAft - nConfBef );
}
if ( RetValue != l_False )
break;
@ -786,9 +786,9 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
}
// prepare return value
if ( !fNaiveCnf && p->vIncluded )
Aig_GlaExtendIncluded( p );
Aig_Gla1ExtendIncluded( p );
vResult = p->vIncluded; p->vIncluded = NULL;
Aig_GlaManStop( p );
Aig_Gla1ManStop( p );
return vResult;
}

518
src/aig/saig/saigGlaPba.c Normal file
View File

@ -0,0 +1,518 @@
/**CFile****************************************************************
FileName [saigGlaPba.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Gate level abstraction.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigGlaPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
#include "satSolver.h"
#include "satStore.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Aig_Gla2Man_t_ Aig_Gla2Man_t;
struct Aig_Gla2Man_t_
{
// user data
Aig_Man_t * pAig;
int nConfMax;
int nFramesMax;
int fVerbose;
// unrolling
Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID
Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID)
Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID
Vec_Int_t * vCla2Obj; // maps sat Var into its first clause
// SAT solver
sat_solver * pSat;
// statistics
int timePre;
int timeSat;
int timeTotal;
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Adds constant to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Aig_Gla2AddConst( sat_solver * pSat, int iVar, int fCompl )
{
lit Lit = toLitCond( iVar, fCompl );
if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Adds buffer to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Aig_Gla2AddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
{
lit Lits[2];
Lits[0] = toLitCond( iVar0, 0 );
Lits[1] = toLitCond( iVar1, !fCompl );
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
return 0;
Lits[0] = toLitCond( iVar0, 1 );
Lits[1] = toLitCond( iVar1, fCompl );
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Adds buffer to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Aig_Gla2AddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
{
lit Lits[3];
Lits[0] = toLitCond( iVar, 1 );
Lits[1] = toLitCond( iVar0, fCompl0 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
return 0;
Lits[0] = toLitCond( iVar, 1 );
Lits[1] = toLitCond( iVar1, fCompl1 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
return 0;
Lits[0] = toLitCond( iVar, 0 );
Lits[1] = toLitCond( iVar0, !fCompl0 );
Lits[2] = toLitCond( iVar1, !fCompl1 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Finds existing SAT variable or creates a new one.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_Gla2FetchVar( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int k )
{
int i, iVecId, iSatVar;
assert( k < p->nFramesMax );
iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
if ( iVecId == 0 )
{
iVecId = Vec_IntSize( p->vVec2Var ) / p->nFramesMax;
for ( i = 0; i < p->nFramesMax; i++ )
Vec_IntPush( p->vVec2Var, 0 );
Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId );
}
iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFramesMax + k );
if ( iSatVar == 0 )
{
iSatVar = Vec_IntSize( p->vVar2Inf ) / 2;
Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) );
Vec_IntPush( p->vVar2Inf, k );
Vec_IntWriteEntry( p->vVec2Var, iVecId * p->nFramesMax + k, iSatVar );
}
return iSatVar;
}
/**Function*************************************************************
Synopsis [Assigns variables to the AIG nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_Gla2AssignVars_rec( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int f )
{
int nVars = Vec_IntSize(p->vVar2Inf);
Aig_Gla2FetchVar( p, pObj, f );
if ( nVars == Vec_IntSize(p->vVar2Inf) )
return;
if ( Aig_ObjIsConst1(pObj) )
return;
if ( Saig_ObjIsPo( p->pAig, pObj ) )
{
Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
return;
}
if ( Aig_ObjIsPi( pObj ) )
{
if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 )
Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 );
return;
}
assert( Aig_ObjIsNode(pObj) );
Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
Aig_Gla2AssignVars_rec( p, Aig_ObjFanin1(pObj), f );
}
/**Function*************************************************************
Synopsis [Creates SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p )
{
Vec_Int_t * vPoLits;
Aig_Obj_t * pObj;
int i, f, ObjId, nVars, RetValue = 1;
// assign variables
// 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
p->pSat = sat_solver_new();
sat_solver_store_alloc( p->pSat );
sat_solver_setnvars( p->pSat, Vec_IntSize(p->vVar2Inf)/2 );
// add clauses
nVars = Vec_IntSize( p->vVar2Inf );
Vec_IntForEachEntryDouble( p->vVar2Inf, ObjId, f, i )
{
if ( ObjId == -1 )
continue;
pObj = Aig_ManObj( p->pAig, ObjId );
if ( Aig_ObjIsNode(pObj) )
{
RetValue &= Aig_Gla2AddNode( p->pSat, Aig_Gla2FetchVar(p, pObj, f),
Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f),
Aig_Gla2FetchVar(p, Aig_ObjFanin1(pObj), f),
Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
Vec_IntPush( p->vCla2Obj, ObjId );
Vec_IntPush( p->vCla2Obj, ObjId );
Vec_IntPush( p->vCla2Obj, ObjId );
}
else if ( Saig_ObjIsLo(p->pAig, pObj) )
{
if ( f == 0 )
{
RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 1 );
Vec_IntPush( p->vCla2Obj, ObjId );
}
else
{
Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f),
Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObjLi), f-1),
Aig_ObjFaninC0(pObjLi) );
Vec_IntPush( p->vCla2Obj, ObjId );
Vec_IntPush( p->vCla2Obj, ObjId );
}
}
else if ( Saig_ObjIsPo(p->pAig, pObj) )
{
RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f),
Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f),
Aig_ObjFaninC0(pObj) );
Vec_IntPush( p->vCla2Obj, ObjId );
Vec_IntPush( p->vCla2Obj, ObjId );
}
else if ( Aig_ObjIsConst1(pObj) )
{
RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 0 );
Vec_IntPush( p->vCla2Obj, ObjId );
}
else assert( Saig_ObjIsPi(p->pAig, pObj) );
}
// add output clause
vPoLits = Vec_IntAlloc( p->nFramesMax );
for ( f = 0; 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 );
Vec_IntPush( p->vCla2Obj, 0 );
assert( nVars == Vec_IntSize(p->vVar2Inf) );
assert( ((Sto_Man_t *)p->pSat->pStore)->nClauses == Vec_IntSize(p->vCla2Obj) );
sat_solver_store_mark_roots( p->pSat );
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nFramesMax )
{
Aig_Gla2Man_t * p;
int i;
p = ABC_CALLOC( Aig_Gla2Man_t, 1 );
p->pAig = pAig;
p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) );
p->vVec2Var = Vec_IntAlloc( 1 << 20 );
p->vVar2Inf = Vec_IntAlloc( 1 << 20 );
p->vCla2Obj = Vec_IntAlloc( 1 << 20 );
// skip first vector ID
p->nFramesMax = nFramesMax;
for ( i = 0; i < p->nFramesMax; i++ )
Vec_IntPush( p->vVec2Var, -1 );
// skip first SAT variable
Vec_IntPush( p->vVar2Inf, -1 );
Vec_IntPush( p->vVar2Inf, -1 );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_Gla2ManStop( Aig_Gla2Man_t * p )
{
Vec_IntFreeP( &p->vObj2Vec );
Vec_IntFreeP( &p->vVec2Var );
Vec_IntFreeP( &p->vVar2Inf );
Vec_IntFreeP( &p->vCla2Obj );
if ( p->pSat )
sat_solver_delete( p->pSat );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Finds the set of clauses involved in the UNSAT core.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose, int * piRetValue )
{
Vec_Int_t * vCore;
void * pSatCnf;
Intp_Man_t * pManProof;
int RetValue, clk = clock();
if ( piRetValue )
*piRetValue = -1;
// solve the problem
RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_Undef )
{
printf( "Conflict limit is reached.\n" );
return NULL;
}
if ( RetValue == l_True )
{
printf( "The BMC problem is SAT.\n" );
if ( piRetValue )
*piRetValue = 0;
return NULL;
}
if ( fVerbose )
{
printf( "SAT solver returned UNSAT after %d conflicts. ", pSat->stats.conflicts );
ABC_PRT( "Time", clock() - clk );
}
assert( RetValue == l_False );
pSatCnf = sat_solver_store_release( pSat );
// derive the UNSAT core
clk = clock();
pManProof = Intp_ManAlloc();
vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 );
Intp_ManFree( pManProof );
Sto_ManFree( (Sto_Man_t *)pSatCnf );
if ( fVerbose )
{
printf( "SAT core contains %d clauses (out of %d). ", Vec_IntSize(vCore), pSat->stats.clauses );
ABC_PRT( "Time", clock() - clk );
}
return vCore;
}
/**Function*************************************************************
Synopsis [Collects abstracted objects.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore )
{
Vec_Int_t * vResult;
Aig_Obj_t * pObj;
int i, ClaId;
vResult = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
Vec_IntWriteEntry( vResult, 0, 1 ); // add const1
Vec_IntForEachEntry( vCore, ClaId, i )
{
pObj = Aig_ManObj( p->pAig, Vec_IntEntry(p->vCla2Obj, ClaId) );
if ( Saig_ObjIsPi(p->pAig, pObj) || Saig_ObjIsPo(p->pAig, pObj) )
continue;
assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) );
Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 );
}
return vResult;
}
/**Function*************************************************************
Synopsis [Performs gate-level localization abstraction.]
Description [Returns array of objects included in the abstraction. This array
may contain only const1, flop outputs, and internal nodes, that is, objects
that should have clauses added to the SAT solver.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
{
int nStart = 0;
Aig_Gla2Man_t * p;
Vec_Int_t * vCore, * vResult;
int clk, clkTotal = clock();
assert( Saig_ManPoNum(pAig) == 1 );
if ( fVerbose )
{
if ( TimeLimit )
printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit );
else
printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax );
}
// start the solver
clk = clock();
p = Aig_Gla2ManStart( pAig, nFramesMax );
if ( !Aig_Gla2CreateSatSolver( p ) )
{
printf( "Error! SAT solver became UNSAT.\n" );
Aig_Gla2ManStop( p );
return NULL;
}
p->timePre += clock() - clk;
// set runtime limit
if ( TimeLimit )
sat_solver_set_runtime_limit( p->pSat, clock() + TimeLimit * CLOCKS_PER_SEC );
// compute UNSAT core
clk = clock();
vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
if ( vCore == NULL )
{
Aig_Gla2ManStop( p );
return NULL;
}
p->timeSat += clock() - clk;
p->timeTotal = clock() - clkTotal;
// print stats
if ( fVerbose )
{
ABC_PRTP( "Pre ", p->timePre, p->timeTotal );
ABC_PRTP( "Sat ", p->timeSat, p->timeTotal );
ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
}
// prepare return value
vResult = Aig_Gla2ManCollect( p, vCore );
Vec_IntFree( vCore );
Aig_Gla2ManStop( p );
return vResult;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

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

@ -379,6 +379,7 @@ static int Abc_CommandAbc9AbsCba ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9AbsPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ReachM ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -832,6 +833,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&abs_pba", Abc_CommandAbc9AbsPba, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_derive", Abc_CommandAbc9GlaDerive, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reachm", Abc_CommandAbc9ReachM, 0 );
@ -28714,12 +28716,12 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &abs_cba [-SFCMT num] [-vh]\n" );
Abc_Print( -2, "usage: &abs_cba [-SFCT num] [-vh]\n" );
Abc_Print( -2, "\t refines abstracted flop 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-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
// 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-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -29020,6 +29022,11 @@ 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 )
{
Abc_Print( 1, "The number of frames should be a positive integer.\n" );
return 0;
}
pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf );
if ( pPars->nStart == 0 )
pAbc->nFrames = pPars->iFrame;
@ -29028,12 +29035,12 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &gla_cba [-SFCMT num] [-cvh]\n" );
Abc_Print( -2, "usage: &gla_cba [-FCT 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-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-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
// 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-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" );
@ -29041,6 +29048,122 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Saig_ParBmc_t Pars, * pPars = &Pars;
int c;
Saig_ParBmcSetDefaultParams( pPars );
pPars->nStart = 0; //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
pPars->nFramesMax = 10; //pPars->nStart + 10;
pPars->nConfLimit = 1000000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTcvh" ) ) != EOF )
{
switch ( c )
{
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nStart < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesMax < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nConfLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConfLimit < 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;
}
pPars->nTimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTimeOut < 0 )
goto usage;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
if ( Gia_ManPoNum(pAbc->pGia) > 1 )
{
Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
return 0;
}
if ( pPars->nFramesMax < 1 )
{
Abc_Print( 1, "The number of frames should be a positive integer.\n" );
return 0;
}
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, "\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-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-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");
return 1;
}
/**Function*************************************************************
Synopsis []