diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/aig/aig.h | 3 | ||||
-rw-r--r-- | src/aig/aig/aigPart.c | 36 | ||||
-rw-r--r-- | src/aig/fra/fraClaus.c | 4 |
3 files changed, 39 insertions, 4 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index cd810b5e..1124c2fb 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -517,7 +517,8 @@ extern void Aig_ObjOrderInsert( Aig_Man_t * p, int ObjId ); extern void Aig_ObjOrderRemove( Aig_Man_t * p, int ObjId ); extern void Aig_ObjOrderAdvance( Aig_Man_t * p ); /*=== aigPart.c =========================================================*/ -extern Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan ); +extern Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * p ); +extern Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps ); extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize ); extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize ); diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index e2100b57..edf51a2e 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -258,7 +258,7 @@ Vec_Int_t * Part_ManTransferEntry( Part_One_t * p ) Synopsis [Computes supports of the POs in the multi-output AIG.] Description [Returns the array of integer arrays containing indices - of the primary inputs.] + of the primary inputsf or each primary output.] SideEffects [Adds the integer PO number at end of each array.] @@ -346,6 +346,40 @@ Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan ) /**Function************************************************************* + Synopsis [Computes the set of outputs for each input.] + + Description [Returns the array of integer arrays containing indices + of the primary outputsf for each primary input.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p ) +{ + Vec_Ptr_t * vSupps, * vSuppsInv; + Vec_Int_t * vSupp; + int i, k, iIn, iOut; + // get structural supports for each output + vSupps = Aig_ManSupports( p ); + // start the inverse supports + vSuppsInv = Vec_PtrAlloc( Aig_ManPiNum(p) ); + for ( i = 0; i < Aig_ManPiNum(p); i++ ) + Vec_PtrPush( vSuppsInv, Vec_IntAlloc(8) ); + // transforms the supports into the inverse supports + Vec_PtrForEachEntry( vSupps, vSupp, i ) + { + iOut = Vec_IntPop( vSupp ); + Vec_IntForEachEntry( vSupp, iIn, k ) + Vec_IntPush( Vec_PtrEntry(vSuppsInv, iIn), iOut ); + } + Vec_VecFree( (Vec_Vec_t *)vSupps ); + return vSuppsInv; +} + +/**Function************************************************************* + Synopsis [Start char-bases support representation.] Description [] diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c index 8e3a03e1..d95515d5 100644 --- a/src/aig/fra/fraClaus.c +++ b/src/aig/fra/fraClaus.c @@ -515,7 +515,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq ) nCountConst = nCountImps = 0; CostMax = p->nSimWords * 32; - +/* // add the property { Aig_Obj_t * pObj; @@ -528,7 +528,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq ) nCountConst++; // printf( "Added the target property to the set of clauses to be inductively checked.\n" ); } - +*/ pSeq->nWordsPref = p->nSimWordsPref; Aig_ManForEachLoSeq( p->pAig, pObj1, i ) |