Version abc80209

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 )