Skip to content

A
abc
Commit 7517c785 by Alan Mishchenko
Options

Scalable gate-level abstraction.

parent a457cf49
Showing with 108 additions and 102 deletions
src/aig/gia/gia.h
......@@ -292,31 +292,31 @@ static inline void Gia_ManTruthNot( unsigned * pOut, unsigned * pIn, int nVars )
pOut[w] = ~pIn[w];
}
static inline Gia_Obj_t * Gia_Regular( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
static inline Gia_Obj_t * Gia_Not( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); }
static inline Gia_Obj_t * Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
static inline int Gia_IsComplement( Gia_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); }
static inline int Gia_ManCiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis); }
static inline int Gia_ManCoNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCos); }
static inline int Gia_ManPiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis) - p->nRegs; }
static inline int Gia_ManPoNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCos) - p->nRegs; }
static inline int Gia_ManRegNum( Gia_Man_t * p ) { return p->nRegs; }
static inline int Gia_ManObjNum( Gia_Man_t * p ) { return p->nObjs; }
static inline int Gia_ManAndNum( Gia_Man_t * p ) { return p->nObjs - Vec_IntSize(p->vCis) - Vec_IntSize(p->vCos) - 1; }
static inline int Gia_ManCandNum( Gia_Man_t * p ) { return Gia_ManCiNum(p) + Gia_ManAndNum(p); }
static inline int Gia_ManConstrNum( Gia_Man_t * p ) { return p->nConstrs; }
static inline void Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1; }
static inline Gia_Obj_t * Gia_ManConst0( Gia_Man_t * p ) { return p->pObjs; }
static inline Gia_Obj_t * Gia_ManConst1( Gia_Man_t * p ) { return Gia_Not(Gia_ManConst0(p)); }
static inline Gia_Obj_t * Gia_ManObj( Gia_Man_t * p, int v ) { assert( v < p->nObjs ); return p->pObjs + v; }
static inline Gia_Obj_t * Gia_ManCi( Gia_Man_t * p, int v ) { return Gia_ManObj( p, Vec_IntEntry(p->vCis,v) ); }
static inline Gia_Obj_t * Gia_ManCo( Gia_Man_t * p, int v ) { return Gia_ManObj( p, Vec_IntEntry(p->vCos,v) ); }
static inline Gia_Obj_t * Gia_ManPi( Gia_Man_t * p, int v ) { assert( v < Gia_ManPiNum(p) ); return Gia_ManCi( p, v ); }
static inline Gia_Obj_t * Gia_ManPo( Gia_Man_t * p, int v ) { assert( v < Gia_ManPoNum(p) ); return Gia_ManCo( p, v ); }
static inline Gia_Obj_t * Gia_ManRo( Gia_Man_t * p, int v ) { assert( v < Gia_ManRegNum(p) ); return Gia_ManCi( p, Gia_ManPiNum(p)+v ); }
static inline Gia_Obj_t * Gia_ManRi( Gia_Man_t * p, int v ) { assert( v < Gia_ManRegNum(p) ); return Gia_ManCo( p, Gia_ManPoNum(p)+v ); }
static inline Gia_Obj_t * Gia_Regular( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
static inline Gia_Obj_t * Gia_Not( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); }
static inline Gia_Obj_t * Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
static inline int Gia_IsComplement( Gia_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); }
static inline int Gia_ManCiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis); }
static inline int Gia_ManCoNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCos); }
static inline int Gia_ManPiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis) - p->nRegs; }
static inline int Gia_ManPoNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCos) - p->nRegs; }
static inline int Gia_ManRegNum( Gia_Man_t * p ) { return p->nRegs; }
static inline int Gia_ManObjNum( Gia_Man_t * p ) { return p->nObjs; }
static inline int Gia_ManAndNum( Gia_Man_t * p ) { return p->nObjs - Vec_IntSize(p->vCis) - Vec_IntSize(p->vCos) - 1; }
static inline int Gia_ManCandNum( Gia_Man_t * p ) { return Gia_ManCiNum(p) + Gia_ManAndNum(p); }
static inline int Gia_ManConstrNum( Gia_Man_t * p ) { return p->nConstrs; }
static inline void Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1; }
static inline Gia_Obj_t * Gia_ManConst0( Gia_Man_t * p ) { return p->pObjs; }
static inline Gia_Obj_t * Gia_ManConst1( Gia_Man_t * p ) { return Gia_Not(Gia_ManConst0(p)); }
static inline Gia_Obj_t * Gia_ManObj( Gia_Man_t * p, int v ) { assert( v >= 0 && v < p->nObjs ); return p->pObjs + v; }
static inline Gia_Obj_t * Gia_ManCi( Gia_Man_t * p, int v ) { return Gia_ManObj( p, Vec_IntEntry(p->vCis,v) ); }
static inline Gia_Obj_t * Gia_ManCo( Gia_Man_t * p, int v ) { return Gia_ManObj( p, Vec_IntEntry(p->vCos,v) ); }
static inline Gia_Obj_t * Gia_ManPi( Gia_Man_t * p, int v ) { assert( v < Gia_ManPiNum(p) ); return Gia_ManCi( p, v ); }
static inline Gia_Obj_t * Gia_ManPo( Gia_Man_t * p, int v ) { assert( v < Gia_ManPoNum(p) ); return Gia_ManCo( p, v ); }
static inline Gia_Obj_t * Gia_ManRo( Gia_Man_t * p, int v ) { assert( v < Gia_ManRegNum(p) ); return Gia_ManCi( p, Gia_ManPiNum(p)+v ); }
static inline Gia_Obj_t * Gia_ManRi( Gia_Man_t * p, int v ) { assert( v < Gia_ManRegNum(p) ); return Gia_ManCo( p, Gia_ManPoNum(p)+v ); }
static inline int Gia_ObjIsTerm( Gia_Obj_t * pObj ) { return pObj->fTerm; }
static inline int Gia_ObjIsAndOrConst0( Gia_Obj_t * pObj ) { return!pObj->fTerm; }
......
src/aig/gia/giaAbsGla2.c
......@@ -44,9 +44,9 @@ struct Ga2_Man_t_
Vec_Ptr_t * vCnfs; // for each object: CNF0, CNF1
// abstraction
Vec_Int_t * vIds; // abstraction ID for each GIA object
Vec_Int_t * vProofIds; // mapping of GIA objects into their proof IDs
Vec_Int_t * vAbs; // array of abstracted objects
Vec_Int_t * vValues; // array of objects with abstraction ID assigned
Vec_Int_t * vProofIds; // mapping of GIA objects into their proof IDs
int nProofIds; // the counter of proof IDs
int LimAbs; // limit value for starting abstraction objects
int LimPpi; // limit value for starting PPI objects
......@@ -82,13 +82,13 @@ static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj )
static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); }
static inline void Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i); }
static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj) ); }
static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 ); }
static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj) ); }
static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 ); }
static inline int Ga2_ObjIsAbs0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) < p->LimAbs; }
static inline int Ga2_ObjIsLeaf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi; }
static inline int Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Ga2_ObjId(p,pObj) && Ga2_ObjCnf0(p,pObj); }
static inline int Ga2_ObjIsLeaf( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Ga2_ObjId(p,pObj) && !Ga2_ObjCnf0(p,pObj); }
static inline int Ga2_ObjIsAbs0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjId(p,pObj) < p->LimAbs; }
static inline int Ga2_ObjIsLeaf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi; }
static inline int Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjCnf0(p,pObj); }
static inline int Ga2_ObjIsLeaf( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Ga2_ObjId(p,pObj) >= 0 && !Ga2_ObjCnf0(p,pObj); }
static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f ) { return (Vec_Int_t *)Vec_PtrEntry( p->vId2Lit, f ); }
......@@ -96,7 +96,7 @@ static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f )
static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
{
int Id = Ga2_ObjId(p,pObj);
assert( Ga2_ObjId(p,pObj) && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) );
assert( Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) );
if ( f == Vec_PtrSize(p->vId2Lit) )
Vec_PtrPush( p->vId2Lit, Vec_IntStartFull(Vec_IntSize(p->vValues)) );
assert( f < Vec_PtrSize(p->vId2Lit) );
......@@ -105,6 +105,7 @@ static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
// inserts literal of this object
static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit )
{
// assert( Lit > 1 || Gia_ObjIsConst0(pObj) );
assert( Lit > 1 );
assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
Vec_IntSetEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj), Lit );
......@@ -118,6 +119,7 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
Lit = toLitCond( p->nSatVars++, 0 );
Ga2_ObjAddLit( p, pObj, f, Lit );
}
// assert( Lit > 1 || Gia_ObjIsConst0(pObj) );
assert( Lit > 1 );
return Lit;
}
......@@ -280,9 +282,21 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N )
Ga2_ManBreakTree_rec( p, pObj, 1, N );
}
// verify that the tree is split correctly
CountMarks = 0;
Vec_IntFreeP( &p->vMapping );
p->vMapping = Vec_IntStart( Gia_ManObjNum(p) );
Gia_ManForEachRo( p, pObj, i )
{
Gia_Obj_t * pObjRi = Gia_ObjRoToRi(p, pObj);
assert( pObj->fPhase );
assert( Gia_ObjFanin0(pObjRi)->fPhase );
// create map
Vec_IntWriteEntry( p->vMapping, Gia_ObjId(p, pObj), Vec_IntSize(p->vMapping) );
Vec_IntPush( p->vMapping, 1 );
Vec_IntPush( p->vMapping, Gia_ObjFaninId0p(p, pObjRi) );
Vec_IntPush( p->vMapping, Gia_ObjFaninC0(pObjRi) ? 0x55555555 : 0xAAAAAAAA );
Vec_IntPush( p->vMapping, -1 ); // placeholder for ref counter
}
CountMarks = Gia_ManRegNum(p);
Gia_ManForEachAnd( p, pObj, i )
{
if ( !pObj->fPhase )
......@@ -352,16 +366,18 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->pGia = pGia;
p->pPars = pPars;
// markings
p->nMarked = Ga2_ManMarkup( pGia, 5 ) + Gia_ManRegNum( p->pGia );
p->nMarked = Ga2_ManMarkup( pGia, 5 );
p->vCnfs = Vec_PtrAlloc( 1000 );
Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
// abstraction
p->vIds = Vec_IntStart( Gia_ManObjNum(pGia) );
p->vIds = Vec_IntStartFull( Gia_ManObjNum(pGia) );
p->vProofIds = Vec_IntAlloc(0);
p->vAbs = Vec_IntAlloc( 1000 );
p->vValues = Vec_IntAlloc( 1000 );
p->vProofIds = Vec_IntAlloc(0);
Vec_IntPush( p->vValues, -1 );
// add constant
Ga2_ObjSetId( p, Gia_ManConst0(pGia), 0 );
Vec_IntPush( p->vValues, 0 );
// refinement
p->pRnm = Rnm_ManStart( pGia );
// SAT solver and variables
......@@ -383,9 +399,9 @@ void Ga2_ManReportMemory( Ga2_Man_t * p )
double memOth = sizeof(Ga2_Man_t);
memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCnfs );
memOth += Vec_IntMemory( p->vIds );
memOth += Vec_IntMemory( p->vProofIds );
memOth += Vec_IntMemory( p->vAbs );
memOth += Vec_IntMemory( p->vValues );
memOth += Vec_IntMemory( p->vProofIds );
memOth += Vec_IntMemory( p->vLits );
memOth += Vec_IntMemory( p->vIsopMem );
memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536;
......@@ -411,8 +427,8 @@ void Ga2_ManStop( Ga2_Man_t * p )
Vec_VecFree( (Vec_Vec_t *)p->vCnfs );
Vec_VecFree( (Vec_Vec_t *)p->vId2Lit );
Vec_IntFree( p->vIds );
Vec_IntFree( p->vAbs );
Vec_IntFree( p->vProofIds );
Vec_IntFree( p->vAbs );
Vec_IntFree( p->vValues );
Vec_IntFree( p->vLits );
Vec_IntFree( p->vIsopMem );
......@@ -631,7 +647,7 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
int s = 0;
}
// assign abstraction ID to the node
if ( Ga2_ObjId(p,pObj) == 0 )
if ( Ga2_ObjId(p,pObj) == -1 )
{
Ga2_ObjSetId( p, pObj, Vec_IntSize(p->vValues) );
Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) );
......@@ -643,9 +659,7 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
return;
assert( Vec_IntFind(p->vAbs, Gia_ObjId(p->pGia, pObj)) == -1 );
Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) );
if ( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) )
return;
assert( Gia_ObjIsAnd(pObj) );
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
// compute parameters
nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj);
uTruth = Ga2_ObjTruth( p->pGia, pObj );
......@@ -654,11 +668,47 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(~uTruth, nLeaves, p->vIsopMem) );
}
void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
{
Vec_Int_t * vLeaves;
Gia_Obj_t * pFanin;
int k, iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f );
assert( iLitOut > 1 );
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
if ( f == 0 && Gia_ObjIsRo(p->pGia, pObj) )
{
iLitOut = Abc_LitNot( iLitOut );
sat_solver2_addclause( p->pSat, &iLitOut, &iLitOut + 1, Gia_ObjId(p->pGia, pObj) );
}
else
{
vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
Vec_IntClear( p->vLits );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f - Gia_ObjIsRo(p->pGia, pObj) ) );
Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) );
}
}
void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
{
Gia_Obj_t * pObj;
int i;
// Ga2_ObjAddLit( p, Gia_ManConst0(p->pGia), f, 0 );
int Lit = Ga2_ObjFindOrAddLit( p, Gia_ManConst0(p->pGia), f );
Lit = Abc_LitNot( Lit );
sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, 0 );
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
if ( i >= p->LimAbs )
Ga2_ManAddToAbsOneStatic( p, pObj, f );
}
void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
{
Vec_Int_t * vLeaves, * vMap;
Gia_Obj_t * pObj, * pFanin;
int f, i, k, iLitOut;
int f, i, k;
// add abstraction objects
Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
{
......@@ -669,6 +719,7 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
// add PPI objects
Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
{
/*
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
pFanin = Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj));
......@@ -676,9 +727,10 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
Ga2_ManSetupNode( p, pFanin, 0 );
continue;
}
*/
vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
if ( !Ga2_ObjId( p, pFanin ) )
if ( Ga2_ObjId( p, pFanin ) == -1 )
Ga2_ManSetupNode( p, pFanin, 0 );
}
// clean mapping in the timeframes
......@@ -686,51 +738,8 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
Vec_IntFillExtra( vMap, Vec_IntSize(p->vValues), -1 );
// add new clauses to the timeframes
for ( f = 0; f <= p->pPars->iFrame; f++ )
Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
{
iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f );
assert( iLitOut > 1 );
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( f == 0 )
{
iLitOut = Abc_LitNot( iLitOut );
sat_solver2_addclause( p->pSat, &iLitOut, &iLitOut + 1, Gia_ObjId(p->pGia, pObj) );
}
else
{
Gia_Obj_t * pObjRi = Gia_ObjRoToRi( p->pGia, pObj );
int iFanLit = Ga2_ObjFindOrAddLit( p, Gia_ObjFanin0(pObjRi), f-1 );
int fCompl = Abc_LitIsCompl(iLitOut) ^ Abc_LitIsCompl(iFanLit) ^ Gia_ObjFaninC0(pObjRi);
sat_solver2_add_buffer( p->pSat, Abc_Lit2Var(iLitOut), Abc_Lit2Var(iFanLit), fCompl, 0, Gia_ObjId(p->pGia, pObj) );
}
continue;
}
assert( Gia_ObjIsAnd(pObj) );
vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
Vec_IntClear( p->vLits );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) );
Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) );
}
}
void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
{
Vec_Int_t * vLeaves;
Gia_Obj_t * pObj, * pFanin;
int i, k, iLitOut;
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
{
if ( i < p->LimAbs )
continue;
vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
Vec_IntClear( p->vLits );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) );
iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f );
Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) );
}
Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
Ga2_ManAddToAbsOneStatic( p, pObj, f );
}
void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues )
......@@ -756,11 +765,10 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues )
// shrink values
Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
{
if ( !i ) continue;
assert( Ga2_ObjId(p,pObj) );
assert( Ga2_ObjId(p,pObj) >= 0 );
if ( i < nValues )
continue;
Ga2_ObjSetId( p, pObj, 0 );
Ga2_ObjSetId( p, pObj, -1 );
}
Vec_IntShrink( p->vValues, nValues );
Vec_PtrShrink( p->vCnfs, 2 * nValues );
......@@ -799,14 +807,14 @@ Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p )
Vec_IntWriteEntry( vGateClasses, 0, 1 );
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
{
if ( Gia_ObjIsRo(p->pGia, pObj) )
if ( Gia_ObjIsAnd(pObj) )
Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 );
else if ( Gia_ObjIsRo(p->pGia, pObj) )
{
Vec_IntWriteEntry( vGateClasses, Gia_ObjId(p->pGia, pObj), 1 );
pObj = Gia_ObjRoToRi( p->pGia, pObj );
Vec_IntWriteEntry( vGateClasses, Gia_ObjFaninId0p(p->pGia, pObj), 1 );
}
else if ( Gia_ObjIsAnd(pObj) )
Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 );
else if ( !Gia_ObjIsConst0(pObj) )
assert( 0 );
}
......@@ -819,7 +827,7 @@ Vec_Int_t * Ga2_ManAbsDerive( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
vToAdd = Vec_IntAlloc( 1000 );
Vec_IntPush( vToAdd, 0 ); // const 0
// Vec_IntPush( vToAdd, 0 ); // const 0
Gia_ManForEachRo( p, pObj, i )
if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, Gia_ObjId(p, pObj)) )
Vec_IntPush( vToAdd, Gia_ObjId(p, pObj) );
......@@ -874,8 +882,6 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
Gia_Obj_t * pLeaf;
int nLeaves, * pLeaves;
int i, Lit, pLits[5];
if ( Gia_ObjIsCo(pObj) )
return Abc_LitNotCond( Ga2_ManUnroll_rec(p, Gia_ObjFanin0(pObj), f), Gia_ObjFaninC0(pObj) );
if ( Gia_ObjIsConst0(pObj) || (f==0 && Gia_ObjIsRo(p->pGia, pObj)) )
{
if ( fSimple )
......@@ -888,6 +894,8 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
}
return 0;
}
if ( Gia_ObjIsCo(pObj) )
return Abc_LitNotCond( Ga2_ManUnroll_rec(p, Gia_ObjFanin0(pObj), f), Gia_ObjFaninC0(pObj) );
assert( pObj->fPhase );
if ( Ga2_ObjIsLeaf0(p, pObj) )
return Ga2_ObjFindOrAddLit( p, pObj, f );
......@@ -1014,8 +1022,6 @@ void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pv
k = Gia_ObjId(p->pGia, pObj);
if ( Ga2_ObjIsAbs(p, pObj) )
continue;
if ( Gia_ObjIsConst0(pObj) )
continue;
assert( pObj->fPhase );
assert( Ga2_ObjIsLeaf(p, pObj) );
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
......
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