summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h3
-rw-r--r--src/aig/gia/giaAbsGla.c240
-rw-r--r--src/aig/gia/giaAbsVta.c14
-rw-r--r--src/base/abci/abc.c18
4 files changed, 193 insertions, 82 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 245d7d5d..40c74d8a 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -212,6 +212,7 @@ struct Gia_ParVta_t_
int nRatioMin; // stop when less than this % of object is abstracted
int fUseTermVars; // use terminal variables
int fUseRollback; // use rollback to the starting number of frames
+ int fPropFanout; // propagate fanout implications
int fDumpVabs; // dumps the abstracted model
char * pFileVabs; // dumps the abstracted model into this file
int fVerbose; // verbose flag
@@ -698,7 +699,7 @@ extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf );
extern int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver );
/*=== giaAbsGla.c ===========================================================*/
-extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars );
+extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, int fStartVta );
/*=== giaAbsVta.c ===========================================================*/
extern void Gia_VtaSetDefaultParams( Gia_ParVta_t * p );
extern Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs );
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 815111b9..53c95650 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -74,6 +74,7 @@ struct Gla_Man_t_
int nAbsOld; // previous abstraction
// other data
int nCexes; // the number of counter-examples
+ int nObjAdded; // total number of objects added
int nSatVars; // the number of SAT variables
Cnf_Dat_t * pCnf; // CNF derived for the nodes
sat_solver2 * pSat; // incremental SAT solver
@@ -83,7 +84,7 @@ struct Gla_Man_t_
Vec_Int_t * vObjCounts; // object counters
// refinement
Vec_Int_t * pvRefis; // vectors of each object
- Vec_Int_t * vPrioSels; // selected priorities
+// Vec_Int_t * vPrioSels; // selected priorities
// statistics
int timeInit;
int timeSat;
@@ -98,13 +99,13 @@ static int Gla_ManCheckVar( Gla_Man_t * p, int iObj, int iFrame );
static int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame );
// object procedures
-static inline int Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
-static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
-static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj ); }
+static inline int Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
+static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
+static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj ); }
static inline int Gla_ObjSatValue( Gla_Man_t * p, int iGia, int f ) { return Gla_ManCheckVar(p, p->pObj2Obj[iGia], f) ? sat_solver2_var_value( p->pSat, Gla_ManGetVar(p, p->pObj2Obj[iGia], f) ) : 0; }
-static inline Rfn_Obj_t * Gla_ObjRef( Gla_Man_t * p, int iObj, int f ) { return (Rfn_Obj_t *)Vec_IntGetEntryP( &(p->pvRefis[iObj]), f ); }
-static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) { *((int *)p) = 0; }
+static inline Rfn_Obj_t * Gla_ObjRef( Gla_Man_t * p, Gia_Obj_t * pObj, int f ) { return (Rfn_Obj_t *)Vec_IntGetEntryP( &(p->pvRefis[Gia_ObjId(p->pGia, pObj)]), f ); }
+static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) { *((int *)p) = 0; }
// iterator through abstracted objects
@@ -387,7 +388,7 @@ void Gla_ManCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pGiaObj, Vec_Int_t *
}
void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int_t * vCos, Vec_Int_t * vRoAnds )
{
- Gla_Obj_t * pObj, * pFanin;
+ Gla_Obj_t * pObj, * pFanin;
Gia_Obj_t * pGiaObj;
int i, k;
@@ -409,6 +410,7 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int
Vec_IntUniqify( vPis );
Vec_IntUniqify( vPPis );
Vec_IntSort( vCos, 0 );
+ // sorting PIs/PPIs/COs leads to refinements that are more "well-aligned"...
// mark const/PIs/PPIs
Gia_ManIncrementTravId( p->pGia );
@@ -432,6 +434,67 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int
/**Function*************************************************************
+ Synopsis [Drive implications of the given node towards primary outputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManRefSetAndPropFanout_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign )
+{
+ int i, Id = Gia_ObjId(p->pGia, pObj);
+ Rfn_Obj_t * pRef0, * pRef1, * pRef = Gla_ObjRef( p, pObj, f );
+ Gia_Obj_t * pFanout;
+ int k;
+ if ( (int)pRef->Sign != Sign )
+ return;
+ assert( pRef->fVisit == 0 );
+ pRef->fVisit = 1;
+ if ( pRef->fPPi )
+ {
+ assert( (int)pRef->Prio > 0 );
+ for ( i = p->pPars->iFrame; i >= 0; i-- )
+ if ( !Gla_ObjRef(p, pObj, i)->fVisit )
+ Gia_ManRefSetAndPropFanout_rec( p, pObj, i, vSelect, Sign );
+ Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) );
+ return;
+ }
+ if ( (Gia_ObjIsCo(pObj) && f == p->pPars->iFrame) || Gia_ObjIsPo(p->pGia, pObj) )
+ return;
+ if ( Gia_ObjIsRi(p->pGia, pObj) )
+ {
+ pFanout = Gia_ObjRiToRo(p->pGia, pObj);
+ if ( !Gla_ObjRef(p, pFanout, f+1)->fVisit )
+ Gia_ManRefSetAndPropFanout_rec( p, pFanout, f+1, vSelect, Sign );
+ return;
+ }
+ assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) );
+ Gia_ObjForEachFanoutStatic( p->pGia, pObj, pFanout, k )
+ {
+// Rfn_Obj_t * pRefF = Gla_ObjRef(p, pFanout, f);
+ if ( Gla_ObjRef(p, pFanout, f)->fVisit )
+ continue;
+ if ( Gia_ObjIsCo(pFanout) )
+ {
+ Gia_ManRefSetAndPropFanout_rec( p, pFanout, f, vSelect, Sign );
+ continue;
+ }
+ assert( Gia_ObjIsAnd(pFanout) );
+ pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pFanout), f );
+ pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pFanout), f );
+ if ( ((pRef0->Value ^ Gia_ObjFaninC0(pFanout)) == 0 && pRef0->fVisit) ||
+ ((pRef1->Value ^ Gia_ObjFaninC1(pFanout)) == 0 && pRef1->fVisit) ||
+ ( ((pRef0->Value ^ Gia_ObjFaninC0(pFanout)) == 1 && pRef0->fVisit) &&
+ ((pRef1->Value ^ Gia_ObjFaninC1(pFanout)) == 1 && pRef1->fVisit) ) )
+ Gia_ManRefSetAndPropFanout_rec( p, pFanout, f, vSelect, Sign );
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Selects assignments to be refined.]
Description []
@@ -441,23 +504,30 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int
SeeAlso []
***********************************************************************/
-void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vRes, int Sign )
+void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign )
{
- int Id = Gia_ObjId(p->pGia, pObj);
- Rfn_Obj_t * pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );
+ int i, Id = Gia_ObjId(p->pGia, pObj);
+ Rfn_Obj_t * pRef = Gla_ObjRef( p, pObj, f );
assert( (int)pRef->Sign == Sign );
if ( pRef->fVisit )
return;
- pRef->fVisit = 1;
+ if ( p->pPars->fPropFanout )
+ Gia_ManRefSetAndPropFanout_rec( p, pObj, f, vSelect, Sign );
+ else
+ pRef->fVisit = 1;
if ( pRef->fPPi )
{
assert( (int)pRef->Prio > 0 );
- assert( (int)pRef->Prio < Vec_IntSize(p->vPrioSels) );
- Vec_IntAddToEntry( p->vObjCounts, f, 1 );
- if ( Vec_IntEntry( p->vPrioSels, pRef->Prio ) == 0 ) // not selected yet
+ if ( p->pPars->fPropFanout )
{
- Vec_IntWriteEntry( p->vPrioSels, pRef->Prio, 1 );
- Vec_IntPush( vRes, Gia_ObjId(p->pGia, pObj) );
+ for ( i = p->pPars->iFrame; i >= 0; i-- )
+ if ( !Gla_ObjRef(p, pObj, i)->fVisit )
+ Gia_ManRefSetAndPropFanout_rec( p, pObj, i, vSelect, Sign );
+ }
+ else
+ {
+ Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) );
+ Vec_IntAddToEntry( p->vObjCounts, f, 1 );
}
return;
}
@@ -466,19 +536,19 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( f > 0 )
- Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vRes, Sign );
+ Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vSelect, Sign );
return;
}
if ( Gia_ObjIsAnd(pObj) )
{
- Rfn_Obj_t * pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
- Rfn_Obj_t * pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f );
+ Rfn_Obj_t * pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f );
+ Rfn_Obj_t * pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pObj), f );
if ( pRef->Value == 1 )
{
if ( pRef0->Prio > 0 )
- Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
+ Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign );
if ( pRef1->Prio > 0 )
- Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
+ Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign );
}
else // select one value
{
@@ -487,23 +557,23 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v
if ( pRef0->Prio <= pRef1->Prio ) // choice
{
if ( pRef0->Prio > 0 )
- Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
+ Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign );
}
else
{
if ( pRef1->Prio > 0 )
- Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
+ Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign );
}
}
else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
{
if ( pRef0->Prio > 0 )
- Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
+ Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign );
}
else if ( (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
{
if ( pRef1->Prio > 0 )
- Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
+ Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign );
}
else assert( 0 );
}
@@ -540,14 +610,13 @@ void Gla_ManVerifyUsingTerSim( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPi
Gia_ObjTerSimSet0( pObj );
}
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
- {
- if ( Vec_IntEntry(p->vPrioSels, i+1) == 0 ) // not selected
- Gia_ObjTerSimSetX( pObj );
- else if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
+ Gia_ObjTerSimSetX( pObj );
+ Gia_ManForEachObjVec( vRes, p->pGia, pObj, i )
+ if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSet0( pObj );
- }
+
Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
@@ -575,6 +644,7 @@ void Gla_ManVerifyUsingTerSim( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPi
Gia_ObjTerSimSetC( pObj );
}
+
/**Function*************************************************************
Synopsis [Performs refinement.]
@@ -590,7 +660,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
{
int fVerify = 1;
static int Sign = 0;
- Vec_Int_t * vPis, * vPPis, * vCos, * vRoAnds, * vRes = NULL;
+ Vec_Int_t * vPis, * vPPis, * vCos, * vRoAnds, * vSelect = NULL;
Rfn_Obj_t * pRef, * pRef0, * pRef1;
Gia_Obj_t * pObj;
int i, f;
@@ -626,7 +696,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
for ( f = 0; f <= p->pPars->iFrame; f++ )
{
// constant
- pRef = Gla_ObjRef( p, 0, f ); Gla_ObjClearRef( pRef );
+ pRef = Gla_ObjRef( p, Gia_ManConst0(p->pGia), f ); Gla_ObjClearRef( pRef );
pRef->Value = 0;
pRef->Prio = 0;
pRef->Sign = Sign;
@@ -634,7 +704,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
{
// assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
- pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
+ pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef );
pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
pRef->Prio = 0;
pRef->Sign = Sign;
@@ -645,7 +715,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
{
// assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
- pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
+ pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef );
pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
pRef->Prio = i+1;
pRef->fPPi = 1;
@@ -656,7 +726,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
{
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
- pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
+ pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef );
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( f == 0 )
@@ -667,7 +737,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
}
else
{
- pRef0 = Gla_ObjRef( p, Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj)), f-1 );
+ pRef0 = Gla_ObjRef( p, Gia_ObjRoToRi(p->pGia, pObj), f-1 );
pRef->Value = pRef0->Value;
pRef->Prio = pRef0->Prio;
pRef->Sign = Sign;
@@ -675,8 +745,8 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
continue;
}
assert( Gia_ObjIsAnd(pObj) );
- pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
- pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f );
+ pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f );
+ pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pObj), f );
pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)) & (pRef1->Value ^ Gia_ObjFaninC1(pObj));
if ( p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] != ~0 &&
@@ -701,8 +771,8 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
// output nodes
Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
{
- pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
- pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
+ pRef = Gla_ObjRef( p, pObj, f ); Gla_ObjClearRef( pRef );
+ pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f );
pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj));
pRef->Prio = pRef0->Prio;
assert( pRef->fVisit == 0 );
@@ -712,7 +782,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
// make sure the output value is 1
pObj = Gia_ManPo( p->pGia, 0 );
- pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), p->pPars->iFrame );
+ pRef = Gla_ObjRef( p, pObj, p->pPars->iFrame );
if ( pRef->Value != 1 )
printf( "\nCounter-example verification has failed!!!\n" );
@@ -728,27 +798,33 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
}
// select objects
- vRes = Vec_IntAlloc( 100 );
- Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 );
+ vSelect = Vec_IntAlloc( 100 );
+// Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 );
Vec_IntFill( p->vObjCounts, p->pPars->iFrame+1, 0 );
- Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vRes, Sign );
+ Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vSelect, Sign );
+ Vec_IntUniqify( vSelect );
+
+// printf( "\nSelected %d.\n", Vec_IntSize(vSelect) );
+
/*
for ( f = 0; f < p->pPars->iFrame; f++ )
printf( "%2d", Vec_IntEntry(p->vObjCounts, f) );
printf( "\n" );
*/
if ( fVerify )
- Gla_ManVerifyUsingTerSim( p, vPis, vPPis, vRoAnds, vCos, vRes );
+ Gla_ManVerifyUsingTerSim( p, vPis, vPPis, vRoAnds, vCos, vSelect );
// remap them into GLA objects
- Gia_ManForEachObjVec( vRes, p->pGia, pObj, i )
- Vec_IntWriteEntry( vRes, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] );
+ Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
+ Vec_IntWriteEntry( vSelect, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vRoAnds );
Vec_IntFree( vCos );
- return vRes;
+
+ p->nObjAdded += Vec_IntSize(vSelect);
+ return vSelect;
}
@@ -888,7 +964,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
p->vAbs = Vec_IntAlloc( 100 );
p->vTemp = Vec_IntAlloc( 100 );
p->vAddedNew = Vec_IntAlloc( 100 );
- p->vPrioSels = Vec_IntAlloc( 100 );
+// p->vPrioSels = Vec_IntAlloc( 100 );
p->vObjCounts = Vec_IntAlloc( 100 );
// internal data
@@ -897,6 +973,8 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
Aig_ManStop( pAig );
// create working GIA
p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping );
+ if ( pPars->fPropFanout )
+ Gia_ManStaticFanoutStart( p->pGia );
//printf( "Old GIA = %d. New GIA = %d.\n", Gia_ManObjNum(pGia0), Gia_ManObjNum(p->pGia) );
// derive new gate map
@@ -1051,7 +1129,7 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vAbs = Vec_IntAlloc( 100 );
p->vTemp = Vec_IntAlloc( 100 );
p->vAddedNew = Vec_IntAlloc( 100 );
- p->vPrioSels = Vec_IntAlloc( 100 );
+// p->vPrioSels = Vec_IntAlloc( 100 );
// internal data
pAig = Gia_ManToAigSimple( p->pGia );
p->pCnf = Cnf_DeriveOther( pAig, 1 );
@@ -1136,8 +1214,8 @@ void Gla_ManStop( Gla_Man_t * p )
Gla_Obj_t * pGla;
int i;
// if ( p->pPars->fVerbose )
- Abc_Print( 1, "SAT solver: Variables = %d. Clauses = %d. Conflicts = %d. Cexes = %d.\n",
- sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes );
+ Abc_Print( 1, "SAT solver: Vars = %d. Clauses = %d. Confs = %d. Cexes = %d. ObjAdded = %d\n",
+ sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded );
for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
ABC_FREE( p->pvRefis[i].pArray );
Gla_ManForEachObj( p, pGla )
@@ -1145,11 +1223,12 @@ void Gla_ManStop( Gla_Man_t * p )
Cnf_DataFree( p->pCnf );
if ( p->pGia0 != NULL )
Gia_ManStop( p->pGia );
+// Gia_ManStaticFanoutStart( p->pGia0 );
sat_solver2_delete( p->pSat );
Vec_IntFreeP( &p->vObjCounts );
Vec_IntFreeP( &p->vCla2Obj );
Vec_IntFreeP( &p->vAddedNew );
- Vec_IntFreeP( &p->vPrioSels );
+// Vec_IntFreeP( &p->vPrioSels );
Vec_IntFreeP( &p->vTemp );
Vec_IntFreeP( &p->vAbs );
ABC_FREE( p->pvRefis );
@@ -1563,7 +1642,7 @@ void Gla_ManReportMemory( Gla_Man_t * p )
double memSat = sat_solver2_memory( p->pSat );
double memPro = sat_solver2_memory_proof( p->pSat );
double memMap = p->nObjs * sizeof(Gla_Obj_t) + Gia_ManObjNum(p->pGia) * sizeof(int);
- double memRef = Gia_ManObjNum(p->pGia) * sizeof(Vec_Int_t) + Vec_IntCap(p->vPrioSels) * sizeof(int);
+ double memRef = Gia_ManObjNum(p->pGia) * sizeof(Vec_Int_t);
double memOth = sizeof(Gla_Man_t);
for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ )
memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int);
@@ -1625,7 +1704,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
-int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
+int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
{
extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
Gla_Man_t * p;
@@ -1636,30 +1715,41 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
+
// compute intial abstraction
if ( pAig->vGateClasses == NULL )
{
- int nFramesMaxOld = pPars->nFramesMax;
- int nFramesStartOld = pPars->nFramesStart;
- int nTimeOutOld = pPars->nTimeOut;
- int nDumpOld = pPars->fDumpVabs;
- pPars->nFramesMax = pPars->nFramesStart;
- pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 );
- pPars->nTimeOut = 20;
- pPars->fDumpVabs = 0;
- RetValue = Gia_VtaPerformInt( pAig, pPars );
- pPars->nFramesMax = nFramesMaxOld;
- pPars->nFramesStart = nFramesStartOld;
- pPars->nTimeOut = nTimeOutOld;
- pPars->fDumpVabs = nDumpOld;
- // create gate classes
- Vec_IntFreeP( &pAig->vGateClasses );
- if ( pAig->vObjClasses )
- pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses );
- Vec_IntFreeP( &pAig->vObjClasses );
+ if ( fStartVta )
+ {
+ int nFramesMaxOld = pPars->nFramesMax;
+ int nFramesStartOld = pPars->nFramesStart;
+ int nTimeOutOld = pPars->nTimeOut;
+ int nDumpOld = pPars->fDumpVabs;
+ pPars->nFramesMax = pPars->nFramesStart;
+ pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 );
+ pPars->nTimeOut = 20;
+ pPars->fDumpVabs = 0;
+ RetValue = Gia_VtaPerformInt( pAig, pPars );
+ pPars->nFramesMax = nFramesMaxOld;
+ pPars->nFramesStart = nFramesStartOld;
+ pPars->nTimeOut = nTimeOutOld;
+ pPars->fDumpVabs = nDumpOld;
+ // create gate classes
+ Vec_IntFreeP( &pAig->vGateClasses );
+ if ( pAig->vObjClasses )
+ pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses );
+ Vec_IntFreeP( &pAig->vObjClasses );
+ // return if VTA solve the problem if could not start
+ if ( RetValue == 0 || pAig->vGateClasses == NULL )
+ return RetValue;
+ }
+ else
+ {
+ pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
+ Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
+ Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
+ }
}
- if ( RetValue == 0 || pAig->vGateClasses == NULL )
- return RetValue;
// start the manager
clk = clock();
p = Gla_ManStart( pAig, pPars );
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 40e5a45c..c6f5e238 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -126,7 +126,7 @@ static inline int Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert
// - the first entry is the number of timeframes (F)
// - the next (F+1) entries give the beginning position of each timeframe
// - the following entries give the object IDs
-// invariant: assert( vec[vec[0]+2] == size(vec) );
+// invariant: assert( vec[vec[0]+1] == size(vec) );
extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
@@ -1624,6 +1624,18 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
+
+/*
+ // compute intial abstraction
+ if ( pAig->vObjClasses == NULL )
+ {
+ pAig->vObjClasses = Vec_IntAlloc( 5 );
+ Vec_IntPush( pAig->vObjClasses, 1 );
+ Vec_IntPush( pAig->vObjClasses, 3 );
+ Vec_IntPush( pAig->vObjClasses, 4 );
+ Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) );
+ }
+*/
// start the manager
p = Vga_ManStart( pAig, pPars );
p->pSat->fVerbose = p->pPars->fVerbose;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9167c54c..d1c1e5a9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27382,12 +27382,12 @@ usage:
int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParVta_t Pars, * pPars = &Pars;
- int c;
+ int c, fStartVta = 0;
Gia_VtaSetDefaultParams( pPars );
pPars->nFramesStart = 30;
pPars->nLearntMax = 100000;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrfdavh" ) ) != EOF )
{
switch ( c )
{
@@ -27483,9 +27483,15 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
pPars->fUseRollback ^= 1;
break;
+ case 'f':
+ pPars->fPropFanout ^= 1;
+ break;
case 'd':
pPars->fDumpVabs ^= 1;
break;
+ case 'a':
+ fStartVta ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -27525,14 +27531,14 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "The starting frame should be 1 or larger.\n" );
return 0;
}
- pAbc->Status = Gia_GlaPerform( pAbc->pGia, pPars );
+ pAbc->Status = Gia_GlaPerform( pAbc->pGia, pPars, fStartVta );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
- Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-dvh]\n" );
- Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" );
+ Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-fdavh]\n" );
+ Abc_Print( -2, "\t performs gate-level abstraction of a sequential miter\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
// Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
@@ -27543,7 +27549,9 @@ usage:
Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
// Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
// Abc_Print( -2, "\t-r : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" );
+ Abc_Print( -2, "\t-f : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
+ Abc_Print( -2, "\t-a : toggle using VTA to kick start GLA [default = %s]\n", fStartVta? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 04:07:09 +0000