Skip to content

A
abc
Commit 24d27e55 by Alan Mishchenko
Options

Improvements to the new abstraction code.

parent ef288ed5
Showing with 62 additions and 47 deletions
src/aig/saig/saigGlaCba.c
...@@ -37,6 +37,11 @@ struct Aig_Gla1Man_t_ ...@@ -37,6 +37,11 @@ struct Aig_Gla1Man_t_
int nConfLimit; int nConfLimit;
int nFramesMax; int nFramesMax;
int fVerbose; int fVerbose;
// unrolling
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
// abstraction // abstraction
Vec_Int_t * vAssigned; // collects objects whose SAT variables have been created 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) Vec_Int_t * vIncluded; // maps obj ID into its status (0=unused; 1=included in abstraction)
...@@ -45,11 +50,6 @@ struct Aig_Gla1Man_t_ ...@@ -45,11 +50,6 @@ struct Aig_Gla1Man_t_
Vec_Int_t * vPPis; // pseudo primary inputs Vec_Int_t * vPPis; // pseudo primary inputs
Vec_Int_t * vFlops; // flops Vec_Int_t * vFlops; // flops
Vec_Int_t * vNodes; // nodes Vec_Int_t * vNodes; // nodes
// unrolling
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
// CNF computation // CNF computation
Vec_Ptr_t * vLeaves; Vec_Ptr_t * vLeaves;
Vec_Ptr_t * vVolume; Vec_Ptr_t * vVolume;
...@@ -295,10 +295,9 @@ Aig_Man_t * Aig_Gla1DeriveAbs( Aig_Gla1Man_t * p ) ...@@ -295,10 +295,9 @@ Aig_Man_t * Aig_Gla1DeriveAbs( Aig_Gla1Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Aig_Gla1FetchVar( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k ) static inline int Aig_Gla1FetchVecId( Aig_Gla1Man_t * p, Aig_Obj_t * pObj )
{ {
int i, iVecId, iSatVar; int i, iVecId;
assert( k < p->nFrames );
iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) ); iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
if ( iVecId == 0 ) if ( iVecId == 0 )
{ {
...@@ -308,6 +307,25 @@ int Aig_Gla1FetchVar( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k ) ...@@ -308,6 +307,25 @@ int Aig_Gla1FetchVar( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId ); Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId );
Vec_IntPushOrderReverse( p->vAssigned, Aig_ObjId(pObj) ); Vec_IntPushOrderReverse( p->vAssigned, Aig_ObjId(pObj) );
} }
return iVecId;
}
/**Function*************************************************************
Synopsis [Finds existing SAT variable or creates a new one.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Aig_Gla1FetchVar( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
{
int iVecId, iSatVar;
assert( k < p->nFrames );
iVecId = Aig_Gla1FetchVecId( p, pObj );
iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + k ); iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + k );
if ( iSatVar == 0 ) if ( iSatVar == 0 )
{ {
...@@ -357,12 +375,12 @@ int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k ) ...@@ -357,12 +375,12 @@ int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj); Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
if ( k == 0 ) if ( k == 0 )
{ {
Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObjLi), 0 ); Aig_Gla1FetchVecId( p, Aig_ObjFanin0(pObjLi) );
return Aig_Gla1AddConst( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 1 ); return Aig_Gla1AddConst( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 1 );
} }
return Aig_Gla1AddBuffer( p->pSat, Aig_Gla1FetchVar(p, pObj, k), return Aig_Gla1AddBuffer( p->pSat, Aig_Gla1FetchVar(p, pObj, k),
Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObjLi), k-1), Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObjLi), k-1),
Aig_ObjFaninC0(pObjLi) ); Aig_ObjFaninC0(pObjLi) );
} }
else else
{ {
...@@ -371,9 +389,9 @@ int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k ) ...@@ -371,9 +389,9 @@ int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
assert( Aig_ObjIsNode(pObj) ); assert( Aig_ObjIsNode(pObj) );
if ( p->vObj2Cnf == NULL ) if ( p->vObj2Cnf == NULL )
return Aig_Gla1AddNode( p->pSat, Aig_Gla1FetchVar(p, pObj, k), return Aig_Gla1AddNode( p->pSat, Aig_Gla1FetchVar(p, pObj, k),
Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObj), k), Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObj), k),
Aig_Gla1FetchVar(p, Aig_ObjFanin1(pObj), k), Aig_Gla1FetchVar(p, Aig_ObjFanin1(pObj), k),
Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) ); Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
// derive clauses // derive clauses
assert( pObj->fMarkA ); assert( pObj->fMarkA );
vClauses = Vec_PtrEntry( p->vObj2Cnf, Aig_ObjId(pObj) ); vClauses = Vec_PtrEntry( p->vObj2Cnf, Aig_ObjId(pObj) );
...@@ -418,31 +436,26 @@ int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k ) ...@@ -418,31 +436,26 @@ int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Int_t * Aig_Gla1CollectAssigned( Aig_Man_t * p, Vec_Int_t * vGateClasses ) void Aig_Gla1CollectAssigned( Aig_Gla1Man_t * p, Vec_Int_t * vGateClasses )
{ {
Vec_Int_t * vAssigned;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int i, Entry; int i, Entry;
vAssigned = Vec_IntAlloc( 1000 ); Vec_IntForEachEntryReverse( vGateClasses, Entry, i )
Vec_IntForEachEntry( vGateClasses, Entry, i )
{ {
if ( Entry == 0 ) if ( Entry == 0 )
continue; continue;
assert( Entry == 1 ); assert( Entry == 1 );
pObj = Aig_ManObj( p, i ); pObj = Aig_ManObj( p->pAig, i );
Vec_IntPush( vAssigned, Aig_ObjId(pObj) ); Aig_Gla1FetchVecId( p, pObj );
if ( Aig_ObjIsNode(pObj) ) if ( Aig_ObjIsNode(pObj) )
{ {
Vec_IntPush( vAssigned, Aig_ObjFaninId0(pObj) ); Aig_Gla1FetchVecId( p, Aig_ObjFanin0(pObj) );
Vec_IntPush( vAssigned, Aig_ObjFaninId1(pObj) ); Aig_Gla1FetchVecId( p, Aig_ObjFanin1(pObj) );
} }
else if ( Saig_ObjIsLo(p, pObj) ) else if ( Saig_ObjIsLo(p->pAig, pObj) )
Vec_IntPush( vAssigned, Aig_ObjFaninId0(Saig_ObjLoToLi(p, pObj)) ); Aig_Gla1FetchVecId( p, Aig_ObjFanin0(Saig_ObjLoToLi(p->pAig, pObj)) );
else assert( Aig_ObjIsConst1(pObj) ); else assert( Aig_ObjIsConst1(pObj) );
} }
Vec_IntUniqify( vAssigned );
Vec_IntReverseOrder( vAssigned );
return vAssigned;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -464,34 +477,36 @@ Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, ...@@ -464,34 +477,36 @@ Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld,
p = ABC_CALLOC( Aig_Gla1Man_t, 1 ); p = ABC_CALLOC( Aig_Gla1Man_t, 1 );
p->pAig = pAig; p->pAig = pAig;
p->nFrames = 32; p->nFrames = 32;
// unrolling
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++ )
Vec_IntPush( p->vVec2Var, -1 );
// skip first SAT variable
Vec_IntPush( p->vVar2Inf, -1 );
Vec_IntPush( p->vVar2Inf, -1 );
// abstraction
p->vAssigned = Vec_IntAlloc( 1000 );
if ( vGateClassesOld ) if ( vGateClassesOld )
{ {
p->vAssigned = Aig_Gla1CollectAssigned( pAig, vGateClassesOld );
p->vIncluded = Vec_IntDup( vGateClassesOld ); p->vIncluded = Vec_IntDup( vGateClassesOld );
Aig_Gla1CollectAssigned( p, vGateClassesOld );
assert( fNaiveCnf ); assert( fNaiveCnf );
} }
else else
{
p->vAssigned = Vec_IntAlloc( 1000 );
p->vIncluded = Vec_IntStart( Aig_ManObjNumMax(pAig) ); p->vIncluded = Vec_IntStart( Aig_ManObjNumMax(pAig) );
}
// components
p->vPis = Vec_IntAlloc( 1000 ); p->vPis = Vec_IntAlloc( 1000 );
p->vPPis = Vec_IntAlloc( 1000 ); p->vPPis = Vec_IntAlloc( 1000 );
p->vFlops = Vec_IntAlloc( 1000 ); p->vFlops = Vec_IntAlloc( 1000 );
p->vNodes = 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 );
// skip first vector ID
for ( i = 0; i < p->nFrames; i++ )
Vec_IntPush( p->vVec2Var, -1 );
// skip first SAT variable
Vec_IntPush( p->vVar2Inf, -1 );
Vec_IntPush( p->vVar2Inf, -1 );
// CNF computation // CNF computation
if ( !fNaiveCnf ) if ( !fNaiveCnf )
{ {
...@@ -523,6 +538,10 @@ Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, ...@@ -523,6 +538,10 @@ Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld,
***********************************************************************/ ***********************************************************************/
void Aig_Gla1ManStop( Aig_Gla1Man_t * p ) void Aig_Gla1ManStop( Aig_Gla1Man_t * p )
{ {
Vec_IntFreeP( &p->vObj2Vec );
Vec_IntFreeP( &p->vVec2Var );
Vec_IntFreeP( &p->vVar2Inf );
Vec_IntFreeP( &p->vAssigned ); Vec_IntFreeP( &p->vAssigned );
Vec_IntFreeP( &p->vIncluded ); Vec_IntFreeP( &p->vIncluded );
...@@ -531,10 +550,6 @@ void Aig_Gla1ManStop( Aig_Gla1Man_t * p ) ...@@ -531,10 +550,6 @@ void Aig_Gla1ManStop( Aig_Gla1Man_t * p )
Vec_IntFreeP( &p->vFlops ); Vec_IntFreeP( &p->vFlops );
Vec_IntFreeP( &p->vNodes ); Vec_IntFreeP( &p->vNodes );
Vec_IntFreeP( &p->vObj2Vec );
Vec_IntFreeP( &p->vVec2Var );
Vec_IntFreeP( &p->vVar2Inf );
if ( p->vObj2Cnf ) if ( p->vObj2Cnf )
{ {
Vec_PtrFreeP( &p->vLeaves ); Vec_PtrFreeP( &p->vLeaves );
...@@ -692,7 +707,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int ...@@ -692,7 +707,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int
// include constant node // include constant node
Vec_IntWriteEntry( p->vIncluded, 0, 1 ); Vec_IntWriteEntry( p->vIncluded, 0, 1 );
Aig_Gla1FetchVar( p, Aig_ManConst1(pAig), 0 ); Aig_Gla1FetchVecId( p, Aig_ManConst1(pAig) );
// set runtime limit // set runtime limit
if ( TimeLimit ) if ( TimeLimit )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment