summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/gia.h3
-rw-r--r--src/aig/gia/giaAbs.c40
-rw-r--r--src/aig/saig/module.make3
-rw-r--r--src/aig/saig/saigGlaCba.c (renamed from src/aig/saig/saigAbsGla.c)102
-rw-r--r--src/aig/saig/saigGlaPba.c518
5 files changed, 611 insertions, 55 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 5f2b94a4..d3165526 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -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 );
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index ba50b238..54b65484 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -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
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 4efc1d80..df6fd7cb 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -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 \
diff --git a/src/aig/saig/saigAbsGla.c b/src/aig/saig/saigGlaCba.c
index 69b4cb66..8fca4796 100644
--- a/src/aig/saig/saigAbsGla.c
+++ b/src/aig/saig/saigGlaCba.c
@@ -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;
}
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
new file mode 100644
index 00000000..e18b6830
--- /dev/null
+++ b/src/aig/saig/saigGlaPba.c
@@ -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
+
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-19 04:04:56 +0000