summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaAbsGla2.c181
1 files changed, 89 insertions, 92 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index fc6a5ef3..17fb5d87 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -37,29 +37,27 @@ struct Ga2_Man_t_
// user data
Gia_Man_t * pGia; // working AIG manager
Gia_ParVta_t * pPars; // parameters
- // internal data
- int nObjs; // the number of objects (abstracted and PPIs)
- int nObjsAlloc; // the number of objects allocated
- Vec_Int_t * vAbs; // array of abstracted objects
- int nAbs; // starting extended abstraction
+ // markings
int nMarked; // total number of marked nodes and flops
-// Vec_Int_t * vExtra; // additional objects
- // object structure
- Vec_Int_t * pvLeaves; // leaves for each object
- Vec_Int_t * pvCnfs0; // positive CNF
- Vec_Int_t * pvCnfs1; // negative CNF
- Vec_Int_t * pvMaps; // mapping into SAT vars for each frame (these should be organized by frame, not by object!)
+ // data storage
+ Vec_Int_t * vId2Data; // mapping of object ID into its data for each object
+ Vec_Ptr_t * vDatas; // for each object: leaves, CNF0, CNF1
+ // abstraction
+ Vec_Int_t * vAbs; // array of abstracted objects
+ int nAbsStart; // marker of the abstracted objects
+ // refinement
+ Rnm_Man_t * pRnm; // refinement manager
+ // SAT solver and variables
+ Vec_Ptr_t * vId2Lit; // mapping of object ID into SAT literal for each timeframe
+ sat_solver2 * pSat; // incremental SAT solver
+ int nSatVars; // the number of SAT variables
// temporaries
Vec_Int_t * vCnf;
Vec_Int_t * vLits;
Vec_Int_t * vIsopMem;
- // other data
- Rnm_Man_t * pRnm; // refinement manager
- sat_solver2 * pSat; // incremental SAT solver
- int nSatVars; // the number of SAT variables
+ char * pSopSizes, ** pSops; // CNF representation
int nCexes; // the number of counter-examples
int nObjAdded; // objs added during refinement
- char * pSopSizes, ** pSops; // CNF representation
// statistics
clock_t timeStart;
clock_t timeInit;
@@ -69,19 +67,19 @@ struct Ga2_Man_t_
clock_t timeOther;
};
-// returns literal of this object, or -1 if the literal is not assigned
+// returns literal of this object, or -1 if SAT variable of the object is not assigned
static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
{
Vec_Int_t * vMap;
assert( pObj->fPhase );
if ( pObj->Value == 0 )
return -1;
- vMap = &p->pvMaps[pObj->Value];
- if ( f >= Vec_IntSize(vMap) )
+ vMap = (Vec_Int_t *)Vec_PtrEntry(p->vMaps, f);
+ if ( pObj->Value >= Vec_IntSize(vMap) )
return -1;
- return Vec_IntEntry( vMap, f );
+ return Vec_IntEntry( vMap, pObj->Value );
}
-// inserts the literal for this object
+// inserts literal of this object
static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit )
{
Vec_Int_t * vMap;
@@ -89,9 +87,12 @@ static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Li
assert( pObj->fPhase );
assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
if ( pObj->Value == 0 )
- pObj->Value = p->nObjs++;
- vMap = &p->pvMaps[pObj->Value];
- Vec_IntSetEntry( vMap, f, Lit );
+ {
+ pObj->Value = Vec_IntSize(p->vAbs);
+ Vec_IntEntry( p->vAbs, Gia_ObjId(p, pObj) );
+ }
+ vMap = (Vec_Int_t *)Vec_PtrEntry(p->vMaps, f);
+ Vec_IntSetEntry( vMap, pObj->Value, Lit );
}
// returns
static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
@@ -265,25 +266,30 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
{
Ga2_Man_t * p;
p = ABC_CALLOC( Ga2_Man_t, 1 );
+ p->timeStart = clock();
+ // user data
p->pGia = pGia;
p->pPars = pPars;
- // internal data
- p->vAbs = Vec_IntAlloc( 100 );
-// p->vExtra = Vec_IntAlloc( 100 );
- // object structure
- p->nObjsAlloc = 256;
- p->pvLeaves = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc );
- p->pvCnfs0 = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc );
- p->pvCnfs1 = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc );
- p->pvMaps = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc );
+ // markings
+ p->nMarked = Gia_ManRegNum(p->pGia) + Ga2_ManMarkup( pGia, 5 );
+ // data storage
+ p->vId2Data = Vec_IntStart( Gia_ManObjNum(pGia) );
+ p->vDatas = Vec_PtrAlloc( 1000 );
+ Vec_PtrPush( p->vDatas, Vec_IntAlloc(0) );
+ Vec_PtrPush( p->vDatas, Vec_IntAlloc(0) );
+ Vec_PtrPush( p->vDatas, Vec_IntAlloc(0) );
+ // abstraction
+ p->nAbsStart= 1;
+ p->vAbs = Vec_IntAlloc( 1000 );
+ Vec_IntPush( p->vAbs, -1 );
+ // refinement
+ p->pRnm = Rnm_ManStart( pGia );
+ // SAT solver and variables
+ p->vId2Lit = Vec_PtrAlloc( 1000 );
// temporaries
p->vCnf = Vec_IntAlloc( 100 );
p->vLits = Vec_IntAlloc( 100 );
p->vIsopMem = Vec_IntAlloc( 100 );
- // prepare AIG
- p->timeStart = clock();
- p->nMarked = Gia_ManRegNum(p->pGia) + Ga2_ManMarkup( pGia, 5 );
- p->pRnm = Rnm_ManStart( pGia );
Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
return p;
}
@@ -305,24 +311,15 @@ void Ga2_ManStop( Ga2_Man_t * p )
// if ( p->pPars->fVerbose )
Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
- for ( i = 0; i < p->nObjsAlloc; i++ )
- {
- ABC_FREE( p->pvLeaves->pArray );
- ABC_FREE( p->pvCnfs0->pArray );
- ABC_FREE( p->pvCnfs1->pArray );
- ABC_FREE( p->pvMaps->pArray );
- }
- ABC_FREE( p->pvLeaves );
- ABC_FREE( p->pvCnfs0 );
- ABC_FREE( p->pvCnfs1 );
- ABC_FREE( p->pvMaps );
+ Vec_IntFree( p->vId2Data );
+ Vec_VecFree( (Vec_Vec_t *)p->vDatas );
+ Vec_IntFree( p->vAbs );
+ Vec_VecFree( (Vec_Vec_t *)p->vId2Lit );
Vec_IntFree( p->vCnf );
Vec_IntFree( p->vLits );
Vec_IntFree( p->vIsopMem );
- Vec_IntFree( p->vAbs );
-// Vec_IntFree( p->vExtra );
- sat_solver2_delete( p->pSat );
Rnm_ManStop( p->pRnm, 1 );
+ sat_solver2_delete( p->pSat );
ABC_FREE( p->pSopSizes );
ABC_FREE( p->pSops[1] );
ABC_FREE( p->pSops );
@@ -591,46 +588,41 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In
***********************************************************************/
void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj )
{
- int Id = p->nObjs++;
- Vec_Int_t * vLeaves = &p->pvLeaves[Id];
- Vec_Int_t * vCnf0 = &p->pvCnfs0[Id];
- Vec_Int_t * vCnf1 = &p->pvCnfs1[Id];
- Vec_Int_t * vMap = &p->pvMaps[Id];
+ Vec_Int_t * vLeaves, * vCnf0, * vCnf1;
unsigned uTruth;
- assert( pObj->Value == 0 );
- assert( p->nObjs > 1 );
- // prepare leaves
- if ( Vec_IntSize(vLeaves) == 0 )
- {
- Vec_IntGrow( vLeaves, 5 );
- Ga2_ManCollectLeaves_rec( p->pGia, pObj, vLeaves, 1 );
- assert( Vec_IntSize(vLeaves) < 6 );
- // compute truth table
- uTruth = Ga2_ManComputeTruth( p->pGia, pObj, vLeaves );
- // prepare CNF
- Ga2_ManCnfCompute( uTruth, Vec_IntSize(vLeaves), vCnf0, p->vIsopMem );
- uTruth = (~uTruth) & Abc_InfoMask( (1 << Vec_IntSize(vLeaves)) );
- Ga2_ManCnfCompute( uTruth, Vec_IntSize(vLeaves), vCnf1, p->vIsopMem );
- // prepare mapping
- Vec_IntGrow( vMap, 100 );
- }
- else
- Vec_IntClear( vMap );
- // remember the number
- pObj->Value = Id;
- // realloc
- if ( p->nObjs == p->nObjsAlloc )
- {
- p->pvLeaves = ABC_REALLOC( Vec_Int_t, p->pvLeaves, 2 * p->nObjsAlloc );
- p->pvCnfs0 = ABC_REALLOC( Vec_Int_t, p->pvCnfs0, 2 * p->nObjsAlloc );
- p->pvCnfs1 = ABC_REALLOC( Vec_Int_t, p->pvCnfs1, 2 * p->nObjsAlloc );
- p->pvMaps = ABC_REALLOC( Vec_Int_t, p->pvMaps, 2 * p->nObjsAlloc );
- memset( p->pvLeaves + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc );
- memset( p->pvCnfs0 + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc );
- memset( p->pvCnfs1 + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc );
- memset( p->pvMaps + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc );
- p->nObjsAlloc *= 2;
- }
+ // create new data entry
+ assert( Vec_IntEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj) ) == 0 );
+ Vec_IntWriteEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj), Vec_IntSize(p->vDatas) );
+ Vec_IntPush( p->vDatas, (vLeaves = Vec_IntAlloc(5)) );
+ Vec_IntPush( p->vDatas, (vCnf0 = Vec_IntAlloc(8)) );
+ Vec_IntPush( p->vDatas, (vCnf1 = Vec_IntAlloc(8)) );
+ // derive leaves
+ Ga2_ManCollectLeaves_rec( p->pGia, pObj, vLeaves, 1 );
+ assert( Vec_IntSize(vLeaves) < 6 );
+ // compute truth table
+ uTruth = Ga2_ManComputeTruth( p->pGia, pObj, vLeaves );
+ // prepare CNF
+ Ga2_ManCnfCompute( uTruth, Vec_IntSize(vLeaves), vCnf0, p->vIsopMem );
+ uTruth = (~uTruth) & Abc_InfoMask( (1 << Vec_IntSize(vLeaves)) );
+ Ga2_ManCnfCompute( uTruth, Vec_IntSize(vLeaves), vCnf1, p->vIsopMem );
+}
+static inline Vec_Int_t * Ga2_ManNodeLeaves( Ga2_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( Vec_IntEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj) ) == 0 )
+ Ga2_ManSetupNode( p, pObj );
+ return (Vec_Int_t *)Vec_PtrEntry( p->vDatas, Vec_IntEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj) ) );
+}
+static inline Vec_Int_t * Ga2_ManNodeCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj )
+{
+ int Num = Vec_IntEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj) );
+ assert( Num > 0 );
+ return (Vec_Int_t *)Vec_PtrEntry( p->vDatas, Num + 1 );
+}
+static inline Vec_Int_t * Ga2_ManNodeCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj )
+{
+ int Num = Vec_IntEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj) );
+ assert( Num > 0 );
+ return (Vec_Int_t *)Vec_PtrEntry( p->vDatas, Num + 2 );
}
void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
@@ -649,7 +641,7 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
void Ga2_ManRemoveFromAbs( Ga2_Man_t * p )
{
Gia_Obj_t * pObj;
- int i;
+ int i, k;
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
{
if ( i < p->nAbs )
@@ -657,6 +649,7 @@ void Ga2_ManRemoveFromAbs( Ga2_Man_t * p )
assert( pObj->fMark0 == 1 );
pObj->fMark0 = 0;
pObj->Value = 0;
+
}
Vec_IntShrink( p->vAbs, p->nAbs );
}
@@ -687,13 +680,17 @@ void Ga2_ManRestart( Ga2_Man_t * p )
Vec_IntShrink( &p->pvLeaves[i], 0 );
Vec_IntShrink( &p->pvCnfs0[i], 0 );
Vec_IntShrink( &p->pvCnfs1[i], 0 );
- Vec_IntShrink( &p->pvMaps[i], 0 );
}
+ // clear abstraction
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
{
assert( pObj->fMark0 );
pObj->fMark0 = 0;
}
+ // clear mapping into timeframes
+ Vec_VecFreeP( (Vec_Vec_t **)&p->vMaps );
+ p->vMaps = Vec_PtrAlloc( 1000 );
+ Vec_PtrPush( p->vMaps, Vec_IntAlloc(0) );
// clear SAT variable numbers (begin with 1)
if ( p->pSat ) sat_solver2_delete( p->pSat );
p->pSat = sat_solver2_new();
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 10:07:16 +0000