2 files changed, 46 insertions, 0 deletions
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 4343bf9a..f7d1d38c 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -157,6 +157,8 @@ extern void            Cnf_ManPostprocess( Cnf_Man_t * p );
 /*=== cnfUtil.c ========================================================*/
 extern Vec_Ptr_t *     Aig_ManScanMapping( Cnf_Man_t * p, int fCollect );
 extern Vec_Ptr_t *     Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder );
+extern Vec_Int_t *     Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
+extern Vec_Int_t *     Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
 /*=== cnfWrite.c ========================================================*/
 extern void            Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
 extern Cnf_Dat_t *     Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );
diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c
index 3738fee5..7da9fb47 100644
--- a/src/aig/cnf/cnfUtil.c
+++ b/src/aig/cnf/cnfUtil.c
@@ -182,6 +182,50 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
     return vMapped;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of CI IDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
+{
+    Vec_Int_t * vCiIds;
+    Aig_Obj_t * pObj;
+    int i;
+    vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );
+    Aig_ManForEachPi( p, pObj, i )
+        Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
+    return vCiIds;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of CI IDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
+{
+    Vec_Int_t * vCoIds;
+    Aig_Obj_t * pObj;
+    int i;
+    vCoIds = Vec_IntAlloc( Aig_ManPoNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+        Vec_IntPush( vCoIds, pCnf->pVarNums[pObj->Id] );
+    return vCoIds;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////