summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaAbs.c36
-rw-r--r--src/aig/gia/giaAig.c1
-rw-r--r--src/aig/gia/giaDup.c117
-rw-r--r--src/aig/gia/giaMan.c46
-rw-r--r--src/aig/saig/saigAbsGla.c542
-rw-r--r--src/base/abci/abc.c23
-rw-r--r--src/misc/vec/vecInt.h30
-rw-r--r--src/sat/bsat/satSolver.c2
9 files changed, 535 insertions, 264 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 2d677638..f53d05f3 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -603,6 +603,7 @@ 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 );
/*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName );
extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
@@ -659,6 +660,7 @@ extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
+extern Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses );
/*=== giaEnable.c ==========================================================*/
extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index f5327f8f..511f418c 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -366,6 +366,42 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
}
+/**Function*************************************************************
+
+ Synopsis [Derive unrolled timeframes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars )
+{
+ extern Vec_Int_t * Aig_GlaManTest( 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_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
+ Aig_ManStop( pAig );
+
+ // update the map
+ Vec_IntFreeP( &pGia->vGateClasses );
+ pGia->vGateClasses = vGateClasses;
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index a38cf083..221593a1 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -350,6 +350,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
else
assert( 0 );
pObj->Value = Gia_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
+ assert( i == 0 || Aig_ObjId(ppNodes[i]) == i );
}
Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
ABC_FREE( ppNodes );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index fdf94837..b879cb05 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1586,8 +1586,8 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
Synopsis [Performs abstraction of the AIG to preserve the included gates.]
- Description [The array contains PIs, LOs, and internal nodes included.
- 0=unsed, 1=PI, 2=PPI, 3=FF, 4=AND.]
+ Description [The array contains 1 for those objects (const, RO, AND)
+ that are included in the abstraction; 0, otherwise.]
SideEffects []
@@ -1596,51 +1596,110 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
***********************************************************************/
Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{
+ Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, nFlops = 0;
assert( Gia_ManPoNum(p) == 1 );
- Gia_ManFillValue( p );
+ assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
+
+ // create included objects and their fanins
+ vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
+
+ // create additional arrays
+ vPis = Vec_IntAlloc( 1000 );
+ vPPis = Vec_IntAlloc( 1000 );
+ vFlops = Vec_IntAlloc( 1000 );
+ vNodes = Vec_IntAlloc( 1000 );
+ Gia_ManForEachObjVec( vAssigned, p, pObj, i )
+ {
+ if ( Gia_ObjIsPi(p, pObj) )
+ Vec_IntPush( vPis, Gia_ObjId(p,pObj) );
+ else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
+ Vec_IntPush( vPPis, Gia_ObjId(p,pObj) );
+ else if ( Gia_ObjIsAnd(pObj) )
+ Vec_IntPush( vNodes, Gia_ObjId(p,pObj) );
+ else if ( Gia_ObjIsRo(p, pObj) )
+ Vec_IntPush( vFlops, Gia_ObjId(p,pObj) );
+ else assert( Gia_ObjIsConst0(pObj) );
+ }
+
// start the new manager
pNew = Gia_ManStart( 5000 );
pNew->pName = Gia_UtilStrsav( p->pName );
- // create PIs
+ // create constant
+ Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
- Gia_ManForEachPi( p, pObj, i )
- if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 1 )
- pObj->Value = Gia_ManAppendCi(pNew);
+ // create PIs
+ Gia_ManForEachObjVec( vPis, p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
// create additional PIs
- Gia_ManForEachPi( p, pObj, i )
- if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 2 )
- pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManForEachObjVec( vPPis, p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
// create ROs
- Gia_ManForEachRo( p, pObj, i )
- if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 3 )
- pObj->Value = Gia_ManAppendCi(pNew);
- // create POs
- Gia_ManHashAlloc( pNew );
+ Gia_ManForEachObjVec( vFlops, p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ // create internal nodes
+ Gia_ManForEachObjVec( vNodes, p, pObj, i )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ // create PO
Gia_ManForEachPo( p, pObj, i )
- {
- Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
- Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- }
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
// create RIs
- Gia_ManForEachRo( p, pObj, i )
- if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 3 )
- {
- pObj = Gia_ObjRoToRi(p, pObj);
- Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
- Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
- nFlops++;
- }
- Gia_ManHashStop( pNew );
- Gia_ManSetRegNum( pNew, nFlops );
+ Gia_ManForEachObjVec( vFlops, p, pObj, i )
+ Gia_ObjRoToRi(p, pObj)->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ObjRoToRi(p, pObj)) );
+ Gia_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
// clean up
pNew = Gia_ManSeqCleanup( pTemp = pNew );
+ assert( Gia_ManObjNum(pTemp) == Gia_ManObjNum(pNew) );
Gia_ManStop( pTemp );
+
+ Vec_IntFree( vPis );
+ Vec_IntFree( vPPis );
+ Vec_IntFree( vFlops );
+ Vec_IntFree( vNodes );
+ Vec_IntFree( vAssigned );
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis [Returns the array of neighbors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses )
+{
+ Vec_Int_t * vAssigned;
+ Gia_Obj_t * pObj;
+ int i, Entry;
+ vAssigned = Vec_IntAlloc( 1000 );
+ Vec_IntForEachEntry( vGateClasses, Entry, i )
+ {
+ if ( Entry == 0 )
+ continue;
+ assert( Entry == 1 );
+ pObj = Gia_ManObj( p, i );
+ Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) );
+ if ( Gia_ObjIsAnd(pObj) )
+ {
+ Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, pObj) );
+ Vec_IntPush( vAssigned, Gia_ObjFaninId1p(p, pObj) );
+ }
+ else if ( Gia_ObjIsRo(p, pObj) )
+ Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)) );
+ else assert( Gia_ObjIsConst0(pObj) );
+ }
+ Vec_IntUniqify( vAssigned );
+ return vAssigned;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index ab0c9bc1..f09ca7b5 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -179,7 +179,8 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p )
}
Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 );
Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 );
- printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d ", Counter0, Counter1 );
+ printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d (%.2f %%) ",
+ Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) );
if ( Counter0 + Counter1 < Gia_ManRegNum(p) )
printf( "and there are other FF classes..." );
printf( "\n" );
@@ -198,7 +199,10 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p )
***********************************************************************/
void Gia_ManPrintGateClasses( Gia_Man_t * p )
{
- int i, Counter[5];
+ Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes;
+ Gia_Obj_t * pObj;
+ int i;
+
if ( p->vGateClasses == NULL )
return;
if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) )
@@ -206,12 +210,38 @@ void Gia_ManPrintGateClasses( Gia_Man_t * p )
printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" );
return;
}
- for ( i = 0; i < 5; i++ )
- Counter[i] = Vec_IntCountEntry( p->vGateClasses, i );
- printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d AND = %d Unused = %d\n",
- Counter[1], Counter[2], Counter[3], Counter[4], Counter[0] );
- if ( Counter[0] + Counter[1] + Counter[2] + Counter[3] + Counter[4] != Gia_ManObjNum(p) )
- printf( "Gia_ManPrintGateClasses(): Mismatch in the object count.\n" );
+
+ // create included objects and their fanins
+ vAssigned = Gia_GlaCollectAssigned( p, p->vGateClasses );
+
+ // create additional arrays
+ vPis = Vec_IntAlloc( 1000 );
+ vPPis = Vec_IntAlloc( 1000 );
+ vFlops = Vec_IntAlloc( 1000 );
+ vNodes = Vec_IntAlloc( 1000 );
+ Gia_ManForEachObjVec( vAssigned, p, pObj, i )
+ {
+ if ( Gia_ObjIsPi(p, pObj) )
+ Vec_IntPush( vPis, Gia_ObjId(p,pObj) );
+ else if ( !Vec_IntEntry(p->vGateClasses, Gia_ObjId(p,pObj)) )
+ Vec_IntPush( vPPis, Gia_ObjId(p,pObj) );
+ else if ( Gia_ObjIsAnd(pObj) )
+ Vec_IntPush( vNodes, Gia_ObjId(p,pObj) );
+ else if ( Gia_ObjIsRo(p, pObj) )
+ Vec_IntPush( vFlops, Gia_ObjId(p,pObj) );
+ else assert( Gia_ObjIsConst0(pObj) );
+ }
+
+ printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%)\n",
+ Vec_IntSize(vPis), Vec_IntSize(vPPis),
+ Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1),
+ Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1) );
+
+ Vec_IntFree( vPis );
+ Vec_IntFree( vPPis );
+ Vec_IntFree( vFlops );
+ Vec_IntFree( vNodes );
+ Vec_IntFree( vAssigned );
}
/**Function*************************************************************
diff --git a/src/aig/saig/saigAbsGla.c b/src/aig/saig/saigAbsGla.c
index 3915c24b..5c8263eb 100644
--- a/src/aig/saig/saigAbsGla.c
+++ b/src/aig/saig/saigAbsGla.c
@@ -37,20 +37,24 @@ struct Aig_GlaMan_t_
int nFramesMax;
int fVerbose;
// abstraction
- Vec_Int_t * vAbstr; // collects objects used in the abstraction
- Vec_Int_t * vUsed; // maps object ID into its status (0=unused; 1=used)
+ Vec_Int_t * vAssigned; // collects objects whose SAT variables have been created
+ Vec_Int_t * vIncluded; // maps obj ID into its status (0=unused; 1=included in abstraction)
+ // components
Vec_Int_t * vPis; // primary inputs
Vec_Int_t * vPPis; // pseudo primary inputs
Vec_Int_t * vFlops; // flops
Vec_Int_t * vNodes; // nodes
// unrolling
- int iFrame;
int nFrames;
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
// SAT solver
sat_solver * pSat;
+ // statistics
+ int timeSat;
+ int timeRef;
+ int timeTotal;
};
////////////////////////////////////////////////////////////////////////
@@ -59,121 +63,6 @@ struct Aig_GlaMan_t_
/**Function*************************************************************
- Synopsis [Performs abstraction of the AIG to preserve the included gates.]
-
- Description [The array contains 1 if the obj is included; 0 otherwise.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Aig_GlaDupAbsGates( Aig_Man_t * p, Vec_Int_t * vUsed, int * pnRealPis )
-{
- Aig_Man_t * pNew;
- Aig_Obj_t * pObj, * pObjLi, * pObjLo;
- int i, nFlops = 0, RetValue;
- assert( Aig_ManPoNum(p) == 1 );
- // start the new manager
- pNew = Aig_ManStart( 5000 );
- pNew->pName = Aig_UtilStrsav( p->pName );
- // create constant
- Aig_ManCleanData( p );
- Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- // create PIs
- Saig_ManForEachPi( p, pObj, i )
- if ( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) )
- pObj->pData = Aig_ObjCreatePi(pNew);
- if ( pnRealPis )
- *pnRealPis = Aig_ManPiNum(pNew);
- // create additional PIs
- Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
- if ( Vec_IntEntry(vUsed, Aig_ObjId(pObjLo)) && !Vec_IntEntry(vUsed, Aig_ObjId(pObjLi)) )
- pObjLo->pData = Aig_ObjCreatePi(pNew);
- Aig_ManForEachNode( p, pObj, i )
- {
- if ( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) &&
- (!Vec_IntEntry(vUsed, Aig_ObjFaninId0(pObj)) ||
- !Vec_IntEntry(vUsed, Aig_ObjFaninId1(pObj))) )
- pObj->pData = Aig_ObjCreatePi(pNew);
- }
- // create ROs
- Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
- if ( Vec_IntEntry(vUsed, Aig_ObjId(pObjLo)) && Vec_IntEntry(vUsed, Aig_ObjId(pObjLi)) )
- pObjLo->pData = Aig_ObjCreatePi(pNew), nFlops++;
- // create internal nodes
- Aig_ManForEachNode( p, pObj, i )
- {
- if ( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) &&
- Vec_IntEntry(vUsed, Aig_ObjFaninId0(pObj)) &&
- Vec_IntEntry(vUsed, Aig_ObjFaninId1(pObj)) )
- pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- }
- // create PO
- Saig_ManForEachPo( p, pObj, i )
- pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
- // create RIs
- Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
- if ( Vec_IntEntry(vUsed, Aig_ObjId(pObjLo)) && Vec_IntEntry(vUsed, Aig_ObjId(pObjLi)) )
- pObjLi->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObjLi) );
- Aig_ManSetRegNum( pNew, nFlops );
- // clean up
- RetValue = Aig_ManCleanup( pNew );
- assert( RetValue == 0 );
- return pNew;
-}
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
-{
- Aig_Man_t * pNew;
- Aig_Obj_t * pObj;
- int i, nFlops = 0, RetValue;
- assert( Aig_ManPoNum(p) == 1 );
- // start the new manager
- pNew = Aig_ManStart( 5000 );
- pNew->pName = Aig_UtilStrsav( p->pAig->pName );
- // create constant
- Aig_ManCleanData( p->pAig );
- Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
- // create PIs
- Aig_ManForEachObjVec( p->vPis, p->pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi(pNew);
- // create additional PIs
- Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi(pNew);
- // create ROs
- Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi(pNew);
- // create internal nodes
- Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i )
- pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
- // create PO
- Saig_ManForEachPo( p->pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
- // create RIs
- Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i )
- Saig_ObjLoToLi(p->pAig, pObj)->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(Saig_ObjLoToLi(p->pAig, pObj)) );
- Aig_ManSetRegNum( pNew, Vec_IntSize(p->vFlops) );
- // clean up
- RetValue = Aig_ManCleanup( pNew );
- assert( RetValue == 0 );
- return pNew;
-}
-
-/**Function*************************************************************
-
Synopsis [Adds constant to the solver.]
Description []
@@ -183,7 +72,7 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
SeeAlso []
***********************************************************************/
-int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl )
+static inline int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl )
{
lit Lit = toLitCond( iVar, fCompl );
if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
@@ -202,7 +91,7 @@ int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl )
SeeAlso []
***********************************************************************/
-int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
+static inline int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
{
lit Lits[2];
@@ -230,7 +119,7 @@ int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
SeeAlso []
***********************************************************************/
-int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
+static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
{
lit Lits[3];
@@ -253,6 +142,155 @@ int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fComp
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Returns the array of neighbors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Aig_GlaCollectAssigned( 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 []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_GlaCollectAbstr( Aig_GlaMan_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i, Entry;
+/*
+ // make sure every neighbor of included objects is assigned a variable
+ Vec_IntForEachEntry( p->vIncluded, Entry, i )
+ {
+ if ( Entry == 0 )
+ continue;
+ 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" );
+ if ( Aig_ObjIsNode(pObj) )
+ {
+ if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObj) ) == -1 )
+ printf( "Aig_GlaCollectAbstr(): 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" );
+ }
+ 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" );
+ }
+ else assert( Aig_ObjIsConst1(pObj) );
+ }
+*/
+ Vec_IntClear( p->vPis );
+ Vec_IntClear( p->vPPis );
+ Vec_IntClear( p->vFlops );
+ Vec_IntClear( p->vNodes );
+ Vec_IntForEachEntryReverse( p->vAssigned, Entry, i )
+ {
+ pObj = Aig_ManObj( p->pAig, Entry );
+ if ( Saig_ObjIsPi(p->pAig, pObj) )
+ Vec_IntPush( p->vPis, Aig_ObjId(pObj) );
+ else if ( !Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) )
+ Vec_IntPush( p->vPPis, Aig_ObjId(pObj) );
+ else if ( Aig_ObjIsNode(pObj) )
+ Vec_IntPush( p->vNodes, Aig_ObjId(pObj) );
+ else if ( Saig_ObjIsLo(p->pAig, pObj) )
+ Vec_IntPush( p->vFlops, Aig_ObjId(pObj) );
+ else assert( Aig_ObjIsConst1(pObj) );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives abstraction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj;
+ int i, nFlops = 0, RetValue;
+ assert( Saig_ManPoNum(p->pAig) == 1 );
+ // start the new manager
+ pNew = Aig_ManStart( 5000 );
+ pNew->pName = Aig_UtilStrsav( p->pAig->pName );
+ // create constant
+ Aig_ManCleanData( p->pAig );
+ Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
+ // create PIs
+ Aig_ManForEachObjVec( p->vPis, p->pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi(pNew);
+ // create additional PIs
+ Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi(pNew);
+ // create ROs
+ Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi(pNew);
+ // create internal nodes
+ Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i )
+ pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // create PO
+ Saig_ManForEachPo( p->pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ // create RIs
+ Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i )
+ {
+ assert( Saig_ObjIsLo(p->pAig, pObj) );
+ pObj = Saig_ObjLoToLi( p->pAig, pObj );
+ pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ }
+ Aig_ManSetRegNum( pNew, Vec_IntSize(p->vFlops) );
+ // clean up
+ RetValue = Aig_ManCleanup( pNew );
+ assert( RetValue == 0 );
+ return pNew;
+}
/**Function*************************************************************
@@ -268,17 +306,15 @@ int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fComp
int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
{
int i, iVecId, iSatVar;
- if ( !Vec_IntEntry(p->vUsed, Aig_ObjId(pObj)) )
- {
- Vec_IntWriteEntry( p->vUsed, Aig_ObjId(pObj), 1 );
- Vec_IntPush( p->vAbstr, Aig_ObjId(pObj) );
- }
+ assert( k < p->nFrames );
iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
if ( iVecId == 0 )
{
iVecId = Vec_IntSize( p->vVec2Var ) / p->nFrames;
for ( i = 0; i < p->nFrames; i++ )
Vec_IntPush( p->vVec2Var, 0 );
+ Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId );
+ Vec_IntPushOrderReverse( p->vAssigned, Aig_ObjId(pObj) );
}
iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + k );
if ( iSatVar == 0 )
@@ -304,27 +340,42 @@ int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
***********************************************************************/
int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
{
- assert( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) );
+ if ( k == p->nFrames )
+ {
+ int i, j, nVecIds = Vec_IntSize( p->vVec2Var ) / p->nFrames;
+ Vec_Int_t * vVec2VarNew = Vec_IntAlloc( 4 * nVecIds * p->nFrames );
+ for ( i = 0; i < nVecIds; i++ )
+ {
+ for ( j = 0; j < p->nFrames; j++ )
+ Vec_IntPush( vVec2VarNew, Vec_IntEntry( p->vVec2Var, i * p->nFrames + j ) );
+ for ( j = 0; j < p->nFrames; j++ )
+ Vec_IntPush( vVec2VarNew, i ? 0 : -1 );
+ }
+ Vec_IntFree( p->vVec2Var );
+ p->vVec2Var = vVec2VarNew;
+ p->nFrames *= 2;
+ }
+ 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 );
- if ( Saig_ObjIsPi(p->pAig, pObj) )
- return 1;
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 );
- if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObjLi)) )
- return 1;
- return Aig_GlaAddBuffer( p->pSat, Aig_GlaFetchVar(p, pObj, k), Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1), Aig_ObjFaninC0(pObjLi) );
+ }
+ return Aig_GlaAddBuffer( p->pSat, Aig_GlaFetchVar(p, pObj, k),
+ Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1),
+ Aig_ObjFaninC0(pObjLi) );
}
assert( Aig_ObjIsNode(pObj) );
- if ( Vec_IntEntry(p->vUsed, Aig_ObjFaninId0(pObj)) && Vec_IntEntry(p->vUsed, Aig_ObjFaninId1(pObj)) )
- return 0;
return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k),
- Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k),
- Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k),
- Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
+ Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k),
+ Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k),
+ Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
}
/**Function*************************************************************
@@ -344,19 +395,19 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig )
int i;
p = ABC_CALLOC( Aig_GlaMan_t, 1 );
- p->pAig = pAig;
- p->vAbstr = Vec_IntAlloc( 1000 );
- p->vUsed = Vec_IntStart( Aig_ManObjNumMax(pAig) );
- p->nFrames = 16;
+ p->pAig = pAig;
+ 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 );
- p->vFlops = Vec_IntAlloc( 1000 );
- p->vNodes = Vec_IntAlloc( 1000 );
+ p->vPis = Vec_IntAlloc( 1000 );
+ p->vPPis = Vec_IntAlloc( 1000 );
+ p->vFlops = Vec_IntAlloc( 1000 );
+ p->vNodes = Vec_IntAlloc( 1000 );
- p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) );
- p->vVec2Var = Vec_IntAlloc( 1 << 20 );
- p->vVar2Inf = Vec_IntAlloc( 1 << 20 );
+ p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) );
+ p->vVec2Var = Vec_IntAlloc( 1 << 20 );
+ p->vVar2Inf = Vec_IntAlloc( 1 << 20 );
// skip first vector ID
for ( i = 0; i < p->nFrames; i++ )
@@ -367,7 +418,7 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig )
// start the SAT solver
p->pSat = sat_solver_new();
- sat_solver_setnvars( p->pSat, 1000 );
+ sat_solver_setnvars( p->pSat, 256 );
return p;
}
@@ -385,8 +436,8 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig )
***********************************************************************/
void Aig_GlaManStop( Aig_GlaMan_t * p )
{
- Vec_IntFreeP( &p->vAbstr );
- Vec_IntFreeP( &p->vUsed );
+ Vec_IntFreeP( &p->vAssigned );
+ Vec_IntFreeP( &p->vIncluded );
Vec_IntFreeP( &p->vPis );
Vec_IntFreeP( &p->vPPis );
@@ -413,57 +464,47 @@ void Aig_GlaManStop( Aig_GlaMan_t * p )
SeeAlso []
***********************************************************************/
-void Aig_GlaCollectAbstr( Aig_GlaMan_t * p )
+Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p, int iFrame )
{
- Aig_Obj_t * pObj, * pObjLi, * pObjLo;
- int i;
- Vec_IntClear( p->vPis );
- Vec_IntClear( p->vPPis );
- Vec_IntClear( p->vFlops );
- Vec_IntClear( p->vNodes );
-
- Saig_ManForEachPi( p->pAig, pObj, i )
- if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObj)) )
- Vec_IntPush( p->vPis, Aig_ObjId(pObj) );
-
- Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
- if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObjLo)) )
+ Abc_Cex_t * pCex;
+ Aig_Obj_t * pObj;
+ int i, f, iVecId, iSatId;
+ pCex = Abc_CexAlloc( Vec_IntSize(p->vFlops), Vec_IntSize(p->vPis) + Vec_IntSize(p->vPPis), iFrame+1 );
+ pCex->iFrame = iFrame;
+ Aig_ManForEachObjVec( p->vPis, p->pAig, pObj, i )
+ {
+ iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
+ assert( iVecId > 0 );
+ for ( f = 0; f <= iFrame; f++ )
{
- if ( Vec_IntEntry(p->vUsed, Aig_ObjFaninId0(pObjLi)) )
- Vec_IntPush( p->vFlops, Aig_ObjId(pObjLo) );
- else
- Vec_IntPush( p->vPPis, Aig_ObjId(pObjLo) );
+ iSatId = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + f );
+ if ( iSatId == 0 )
+ continue;
+ assert( iSatId > 0 );
+ if ( sat_solver_var_value(p->pSat, iSatId) )
+ Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + i );
}
-
- Aig_ManForEachNode( p->pAig, pObj, i )
- if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObj)) )
+ }
+ Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i )
+ {
+ iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
+ assert( iVecId > 0 );
+ for ( f = 0; f <= iFrame; f++ )
{
- if ( Vec_IntEntry(p->vUsed, Aig_ObjFaninId0(pObj)) && Vec_IntEntry(p->vUsed, Aig_ObjFaninId1(pObj)) )
- Vec_IntPush( p->vNodes, Aig_ObjId(pObjLo) );
- else
- Vec_IntPush( p->vPPis, Aig_ObjId(pObjLo) );
+ iSatId = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + f );
+ if ( iSatId == 0 )
+ continue;
+ assert( iSatId > 0 );
+ if ( sat_solver_var_value(p->pSat, iSatId) )
+ Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Vec_IntSize(p->vPis) + i );
}
+ }
+ return pCex;
}
/**Function*************************************************************
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p )
-{
- return NULL;
-}
-
-/**Function*************************************************************
-
- Synopsis []
+ Synopsis [Prints current abstraction statistics.]
Description []
@@ -472,45 +513,72 @@ Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p )
SeeAlso []
***********************************************************************/
-void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r )
+void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c )
{
- printf( "Fra %3d : Ref %3d : PI =%6d PPI =%6d Flop =%6d Node =%6d\n",
- f, r, Vec_IntSize(p->vPis), Vec_IntSize(p->vPPis), Vec_IntSize(p->vFlops), Vec_IntSize(p->vNodes) );
+ if ( r == 0 )
+ printf( "== %3d ==", f );
+ else
+ printf( " " );
+ printf( " %4d PI =%6d PPI =%6d FF =%6d Node =%6d Var =%7d Conf =%6d\n",
+ r, Vec_IntSize(p->vPis), Vec_IntSize(p->vPPis), Vec_IntSize(p->vFlops), Vec_IntSize(p->vNodes), v, c );
}
/**Function*************************************************************
- Synopsis [Perform variable frame abstraction.]
+ Synopsis [Performs gate-level localization abstraction.]
- Description []
+ 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 []
***********************************************************************/
-void Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose )
+Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
{
+ int nStart = 0;
+ Vec_Int_t * vResult = NULL;
Aig_GlaMan_t * p;
Aig_Man_t * pAbs;
Aig_Obj_t * pObj;
Abc_Cex_t * pCex;
- Vec_Int_t * vPPisToRefine;
+ Vec_Int_t * vPPiRefine;
int f, g, r, i, iSatVar, Lit, Entry, RetValue;
+ int nConfBef, nConfAft, 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
p = Aig_GlaManStart( pAig );
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 );
+
+ // set runtime limit
+ if ( TimeLimit )
+ sat_solver_set_runtime_limit( p->pSat, clock() + TimeLimit * CLOCKS_PER_SEC );
+
// iterate over the timeframes
for ( f = 0; f < nFramesMax; f++ )
{
// initialize abstraction in this timeframe
- Aig_ManForEachObjVec( p->vAbstr, pAig, pObj, i )
- Aig_GlaObjAddToSolver( p, pObj, f );
+ Aig_ManForEachObjVec( p->vAssigned, pAig, pObj, i )
+ if ( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) )
+ if ( !Aig_GlaObjAddToSolver( p, pObj, f ) )
+ printf( "Error! SAT solver became UNSAT.\n" );
// create output literal to represent property failure
pObj = Aig_ManPo( pAig, 0 );
@@ -518,41 +586,83 @@ void Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerb
Lit = toLitCond( iSatVar, Aig_ObjFaninC0(pObj) );
// try solving the abstraction
- Aig_GlaPrintAbstr( p, f, -1 );
+ Aig_GlaCollectAbstr( p );
for ( r = 0; r < 1000000; r++ )
{
+ // try to find a counter-example
+ clk = clock();
+ nConfBef = p->pSat->stats.conflicts;
RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1,
(ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+ nConfAft = p->pSat->stats.conflicts;
+ p->timeSat += clock() - clk;
if ( RetValue != l_True )
+ {
+ if ( fVerbose )
+ {
+ if ( r == 0 )
+ printf( "== %3d ==", f );
+ else
+ printf( " " );
+ if ( TimeLimit && clock() > clkTotal + TimeLimit * CLOCKS_PER_SEC )
+ printf( " SAT solver timed out after %d seconds.\n", TimeLimit );
+ 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 );
+ }
break;
- // derive abstraction
- Aig_GlaCollectAbstr( p );
- // derive counter-example
- pCex = Aig_GlaDeriveCex( p );
+ }
+ clk = clock();
// derive abstraction
pAbs = Aig_GlaDeriveAbs( p );
+ // derive counter-example
+ pCex = Aig_GlaDeriveCex( p, f );
+ // verify the counter-example
+ RetValue = Saig_ManVerifyCex( pAbs, pCex );
+ if ( RetValue == 0 )
+ printf( "Error! CEX is invalid.\n" );
// perform refinement
- vPPisToRefine = Saig_ManCbaFilterInputs( pAig, Vec_IntSize(p->vPis), pCex, 0 );
- // update
- Vec_IntForEachEntry( vPPisToRefine, Entry, i )
+ vPPiRefine = Saig_ManCbaFilterInputs( pAbs, Vec_IntSize(p->vPis), pCex, 0 );
+ Vec_IntForEachEntry( vPPiRefine, Entry, i )
{
+ pObj = Aig_ManObj( pAig, Vec_IntEntry(p->vPPis, Entry) );
+ assert( Aig_ObjIsNode(pObj) || Saig_ObjIsLo(p->pAig, pObj) );
+ assert( Vec_IntEntry( p->vIncluded, Aig_ObjId(pObj) ) == 0 );
+ Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 );
for ( g = 0; g <= f; g++ )
- Aig_GlaObjAddToSolver( p, Aig_ManObj(pAig, Vec_IntEntry(p->vPPis, Entry)), g );
+ if ( !Aig_GlaObjAddToSolver( p, pObj, g ) )
+ printf( "Error! SAT solver became UNSAT.\n" );
}
- Vec_IntFree( vPPisToRefine );
- // print abstraction
- Aig_GlaPrintAbstr( p, f, r );
+ Vec_IntFree( vPPiRefine );
+ Aig_ManStop( pAbs );
+ Abc_CexFree( pCex );
+ p->timeRef += clock() - clk;
+
+ // prepare abstraction
+ Aig_GlaCollectAbstr( p );
+ if ( fVerbose )
+ Aig_GlaPrintAbstr( p, f, r, p->pSat->size, nConfAft - nConfBef );
}
if ( RetValue != l_False )
break;
}
- Aig_GlaPrintAbstr( p, f, -1 );
+ p->timeTotal = clock() - clkTotal;
if ( f == nFramesMax )
printf( "Finished %d frames without exceeding conflict limit (%d).\n", f, nConfLimit );
else
printf( "Ran out of conflict limit (%d) at frame %d.\n", nConfLimit, f );
-
+ // print stats
+ if ( fVerbose )
+ {
+ ABC_PRTP( "Sat ", p->timeSat, p->timeTotal );
+ ABC_PRTP( "Ref ", p->timeRef, p->timeTotal );
+ ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
+ }
+ // prepare return value
+ vResult = p->vIncluded; p->vIncluded = NULL;
Aig_GlaManStop( p );
+ return vResult;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a8bd177f..f07a5c5c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28858,12 +28858,12 @@ int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
*/
if ( pAbc->pGia->vGateClasses == NULL )
{
- Abc_Print( -1, "Abstraction flop map is missing.\n" );
+ Abc_Print( -1, "Abstraction gate map is missing.\n" );
return 0;
}
-// pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses );
-// Abc_CommandUpdate9( pAbc, pTemp );
- printf( "This command is currently not enabled.\n" );
+ pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses );
+ Abc_CommandUpdate9( pAbc, pTemp );
+// printf( "This command is currently not enabled.\n" );
return 0;
usage:
@@ -28890,8 +28890,9 @@ int Abc_CommandAbc9GlaCba( 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 = pPars->nStart + 10;
+ pPars->nStart = 0; //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
+ pPars->nFramesMax = 50; //pPars->nStart + 10;
+ pPars->nConfLimit = 5000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTvh" ) ) != EOF )
{
@@ -28971,11 +28972,11 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
-// pAbc->Status = Gia_ManCbaPerform( 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" );
+ pAbc->Status = Gia_ManGlaCbaPerform( 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:
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 545cf8a6..ec17795e 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -657,6 +657,36 @@ static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry )
SeeAlso []
***********************************************************************/
+static inline void Vec_IntPushOrderReverse( Vec_Int_t * p, int Entry )
+{
+ int i;
+ if ( p->nSize == p->nCap )
+ {
+ if ( p->nCap < 16 )
+ Vec_IntGrow( p, 16 );
+ else
+ Vec_IntGrow( p, 2 * p->nCap );
+ }
+ p->nSize++;
+ for ( i = p->nSize-2; i >= 0; i-- )
+ if ( p->pArray[i] < Entry )
+ p->pArray[i+1] = p->pArray[i];
+ else
+ break;
+ p->pArray[i+1] = Entry;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts the entry while preserving the increasing order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
static inline int Vec_IntPushUniqueOrder( Vec_Int_t * p, int Entry )
{
int i;
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index de186047..a3da3e30 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1485,6 +1485,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
// int nConfs = 0;
double Ratio = (s->stats.learnts == 0)? 0.0 :
s->stats.learnts_literals / (double)s->stats.learnts;
+ if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+ break;
if (s->verbosity >= 1)
{
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 07:48:15 +0000