Version abc70726

7 files changed, 319 insertions, 131 deletions

diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index c758867c..2f121752 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -83,8 +83,16 @@ struct Cnf_Man_t_
     int             nMergeLimit;     // the limit on the size of merged cut
     unsigned *      pTruths[4];      // temporary truth tables
     Vec_Int_t *     vMemory;         // memory for intermediate ISOP representation
+    int             timeCuts; 
+    int             timeMap;
+    int             timeSave;
 };
 
+
+static inline Dar_Cut_t *  Dar_ObjBestCut( Aig_Obj_t * pObj ) { Dar_Cut_t * pCut; int i; Dar_ObjForEachCut( pObj, pCut, i ) if ( pCut->fBest ) return pCut; return NULL; }
+
+static inline int          Cnf_CutSopCost( Cnf_Man_t * p, Dar_Cut_t * pCut ) { return p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth]; }
+
 static inline int          Cnf_CutLeaveNum( Cnf_Cut_t * pCut )    { return pCut->nFanins;                               }
 static inline int *        Cnf_CutLeaves( Cnf_Cut_t * pCut )      { return pCut->pFanins;                               }
 static inline unsigned *   Cnf_CutTruth( Cnf_Cut_t * pCut )       { return (unsigned *)(pCut->pFanins + pCut->nFanins); }
@@ -109,7 +117,9 @@ static inline void         Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut
 ////////////////////////////////////////////////////////////////////////
 
 /*=== cnfCore.c ========================================================*/
-extern Cnf_Dat_t *     Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig );
+extern Cnf_Dat_t *     Cnf_Derive( Aig_Man_t * pAig );
+extern Cnf_Man_t *     Cnf_ManRead();
+extern void            Cnf_ClearMemory();
 /*=== cnfCut.c ========================================================*/
 extern Cnf_Cut_t *     Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj );
 extern void            Cnf_CutPrint( Cnf_Cut_t * pCut );
@@ -121,10 +131,12 @@ extern void            Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops );
 /*=== cnfMan.c ========================================================*/
 extern Cnf_Man_t *     Cnf_ManStart();
 extern void            Cnf_ManStop( Cnf_Man_t * p );
+extern Vec_Int_t *     Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
 extern void            Cnf_DataFree( Cnf_Dat_t * p );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName );
 void *                 Cnf_DataWriteIntoSolver( Cnf_Dat_t * p );
 /*=== cnfMap.c ========================================================*/
+extern void            Cnf_DeriveMapping( Cnf_Man_t * p );
 extern int             Cnf_ManMapForCnf( Cnf_Man_t * p );
 /*=== cnfPost.c ========================================================*/
 extern void            Cnf_ManTransferCuts( Cnf_Man_t * p );
@@ -132,7 +144,7 @@ extern void            Cnf_ManFreeCuts( Cnf_Man_t * p );
 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 );
+extern Vec_Ptr_t *     Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder );
 /*=== 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 );
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index a3a7efaa..7480d45d 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/src/aig/cnf/cnfCore.c
@@ -24,13 +24,15 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static Cnf_Man_t * s_pManCnf = NULL;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Converts AIG into the SAT solver.]
 
   Description []
                
@@ -39,21 +41,97 @@
   SeeAlso     []
 
 ***********************************************************************/
-Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig )
+Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig )
 {
-    Aig_MmFixed_t * pMemCuts;
-    Cnf_Dat_t * pCnf = NULL;
+    Cnf_Man_t * p;
+    Cnf_Dat_t * pCnf;
     Vec_Ptr_t * vMapped;
-    int nIters = 2;
+    Aig_MmFixed_t * pMemCuts;
     int clk;
-
+    // allocate the CNF manager
+    if ( s_pManCnf == NULL )
+        s_pManCnf = Cnf_ManStart();
     // connect the managers
+    p = s_pManCnf;
     p->pManAig = pAig;
 
     // generate cuts for all nodes, assign cost, and find best cuts
 clk = clock();
-    pMemCuts = Dar_ManComputeCuts( pAig );
-PRT( "Cuts", clock() - clk );
+    pMemCuts = Dar_ManComputeCuts( pAig, 10 );
+p->timeCuts = clock() - clk;
+
+    // find the mapping
+clk = clock();
+    Cnf_DeriveMapping( p );
+p->timeMap = clock() - clk;
+//    Aig_ManScanMapping( p, 1 );
+
+    // convert it into CNF
+clk = clock();
+    Cnf_ManTransferCuts( p );
+    vMapped = Cnf_ManScanMapping( p, 1, 1 );
+    pCnf = Cnf_ManWriteCnf( p, vMapped );
+    Vec_PtrFree( vMapped );
+    Aig_MmFixedStop( pMemCuts, 0 );
+p->timeSave = clock() - clk;
+
+PRT( "Cuts   ", p->timeCuts );
+PRT( "Map    ", p->timeMap  );
+PRT( "Saving ", p->timeSave );
+    return pCnf;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cnf_Man_t * Cnf_ManRead()
+{
+    return s_pManCnf;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_ClearMemory()
+{
+    if ( s_pManCnf == NULL )
+        return;
+    Cnf_ManStop( s_pManCnf );
+    s_pManCnf = NULL;
+}
+
+
+#if 0
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_Derive_old( Aig_Man_t * pAig )
+{
 /*
     // iteratively improve area flow
     for ( i = 0; i < nIters; i++ )
@@ -95,6 +173,9 @@ PRT( "Ext ", clock() - clk );
     return NULL;
 }
 
+#endif
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cnf/cnfCut.c b/src/aig/cnf/cnfCut.c
index afe5920a..17ab0c78 100644
--- a/src/aig/cnf/cnfCut.c
+++ b/src/aig/cnf/cnfCut.c
@@ -87,15 +87,14 @@ Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj )
     Cnf_Cut_t * pCut;
     unsigned * pTruth;
     assert( Aig_ObjIsNode(pObj) );
-//    pCutBest = Aig_ObjBestCut( pObj );
-        pCutBest = NULL;
+    pCutBest = Dar_ObjBestCut( pObj );
     assert( pCutBest != NULL );
     assert( pCutBest->nLeaves <= 4 );
     pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
     memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves );
     pTruth = Cnf_CutTruth(pCut);
     *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth;
-    pCut->Cost = p->pSopSizes[0xFFFF & *pTruth] + p->pSopSizes[0xFFFF & ~*pTruth];
+    pCut->Cost = Cnf_CutSopCost( p, pCutBest );
     return pCut;
 }
 
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index e978e322..77bf8650 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -86,6 +86,28 @@ void Cnf_ManStop( Cnf_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the array of CI IDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cnf_DataCollectPiSatNums( 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    []
 
   Description []
diff --git a/src/aig/cnf/cnfMap.c b/src/aig/cnf/cnfMap.c
index a9ba41a0..ad728412 100644
--- a/src/aig/cnf/cnfMap.c
+++ b/src/aig/cnf/cnfMap.c
@@ -28,6 +28,126 @@
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    [Computes area flow of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut, int * pAreaFlows )
+{
+    Aig_Obj_t * pLeaf;
+    int i;
+    pCut->Value = 0;
+    pCut->uSign = 100 * Cnf_CutSopCost( p, pCut );
+    Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
+    {
+        pCut->Value += pLeaf->nRefs;
+        if ( !Aig_ObjIsNode(pLeaf) )
+            continue;
+        assert( pLeaf->nRefs > 0 );
+        pCut->uSign += pAreaFlows[pLeaf->Id] / (pLeaf->nRefs? pLeaf->nRefs : 1);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area flow of the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cnf_CutSuperAreaFlow( Vec_Ptr_t * vSuper, int * pAreaFlows )
+{
+    Aig_Obj_t * pLeaf;
+    int i, nAreaFlow;
+    nAreaFlow = 100 * (Vec_PtrSize(vSuper) + 1);
+    Vec_PtrForEachEntry( vSuper, pLeaf, i )
+    {
+        pLeaf = Aig_Regular(pLeaf);
+        if ( !Aig_ObjIsNode(pLeaf) )
+            continue;
+        assert( pLeaf->nRefs > 0 );
+        nAreaFlow += pAreaFlows[pLeaf->Id] / (pLeaf->nRefs? pLeaf->nRefs : 1);
+    }
+    return nAreaFlow;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_DeriveMapping( Cnf_Man_t * p )
+{
+    Vec_Ptr_t * vSuper;
+    Aig_Obj_t * pObj;
+    Dar_Cut_t * pCut, * pCutBest;
+    int i, k, AreaFlow, * pAreaFlows;
+    // allocate area flows
+    pAreaFlows = ALLOC( int, Aig_ManObjIdMax(p->pManAig) + 1 );
+    memset( pAreaFlows, 0, sizeof(int) * (Aig_ManObjIdMax(p->pManAig) + 1) );
+    // visit the nodes in the topological order and update their best cuts
+    vSuper = Vec_PtrAlloc( 100 );
+    Aig_ManForEachNode( p->pManAig, pObj, i )
+    {
+        // go through the cuts
+        pCutBest = NULL;
+        Dar_ObjForEachCut( pObj, pCut, k )
+        {
+            pCut->fBest = 0;
+            if ( k == 0 )
+                continue;
+            Cnf_CutAssignAreaFlow( p, pCut, pAreaFlows );
+            if ( pCutBest == NULL || pCutBest->uSign > pCut->uSign || 
+                (pCutBest->uSign == pCut->uSign && pCutBest->Value < pCut->Value) )
+                 pCutBest = pCut;
+        }
+        // check the big cut
+//        Aig_ObjCollectSuper( pObj, vSuper );
+        // get the area flow of this cut
+//        AreaFlow = Cnf_CutSuperAreaFlow( vSuper, pAreaFlows );
+        AreaFlow = AIG_INFINITY;
+        if ( AreaFlow >= (int)pCutBest->uSign )
+        {
+            pAreaFlows[pObj->Id] = pCutBest->uSign;
+            pCutBest->fBest = 1;
+        }
+        else
+        {
+            pAreaFlows[pObj->Id] = AreaFlow;
+            pObj->fMarkB = 1; // mark the special node
+        }
+    }
+    Vec_PtrFree( vSuper );
+    free( pAreaFlows );
+
+/*
+    // compute the area of mapping
+    AreaFlow = 0;
+    Aig_ManForEachPo( p->pManAig, pObj, i )
+        AreaFlow += Dar_ObjBestCut(Aig_ObjFanin0(pObj))->uSign / 100 / Aig_ObjFanin0(pObj)->nRefs;
+    printf( "Area of the network = %d.\n", AreaFlow );
+*/
+}
+
+
+
 #if 0
 
 /**Function*************************************************************
@@ -160,45 +280,6 @@ Dar_Cut_t * Cnf_ObjFindBestCut( Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut )
-{
-    Aig_Obj_t * pLeaf;
-    int i;
-    pCut->Cost    = p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth];
-    pCut->Area    = (float)pCut->Cost;
-    pCut->NoRefs  = 0;
-    pCut->FanRefs = 0;
-    Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
-    {
-        if ( !Aig_ObjIsNode(pLeaf) )
-            continue;
-        if ( pLeaf->nRefs == 0 )
-        {
-            pCut->Area += Aig_ObjBestCut(pLeaf)->Area;
-            pCut->NoRefs++;
-        }
-        else
-        {
-            pCut->Area += Aig_ObjBestCut(pLeaf)->Area / pLeaf->nRefs;
-            if ( pCut->FanRefs + pLeaf->nRefs > 15 )
-                pCut->FanRefs = 15;
-            else
-                pCut->FanRefs += pLeaf->nRefs;
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes area flow of the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 void Cnf_CutAssignArea( Cnf_Man_t * p, Dar_Cut_t * pCut )
 {
     Aig_Obj_t * pLeaf;
diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c
index da5edef2..22b30262 100644
--- a/src/aig/cnf/cnfUtil.c
+++ b/src/aig/cnf/cnfUtil.c
@@ -51,11 +51,24 @@ int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
     if ( vMapped )
         Vec_PtrPush( vMapped, pObj );
     // visit the transitive fanin of the selected cut
-//    pCutBest = Aig_ObjBestCut(pObj);
-        pCutBest = NULL;
-    aArea = pCutBest->Value;
-    Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
-        aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped );
+    if ( pObj->fMarkB )
+    {
+        Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
+        Aig_ObjCollectSuper( pObj, vSuper );
+        aArea = Vec_PtrSize(vSuper) + 1;
+        Vec_PtrForEachEntry( vSuper, pLeaf, i )
+            aArea += Aig_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped );
+        Vec_PtrFree( vSuper );
+        ////////////////////////////
+        pObj->fMarkB = 1;
+    }
+    else
+    {
+        pCutBest = Dar_ObjBestCut( pObj );
+        aArea = Cnf_CutSopCost( p, pCutBest );
+        Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
+            aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped );
+    }
     return aArea;
 }
 
@@ -85,7 +98,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
     p->aArea = 0;
     Aig_ManForEachPo( p->pManAig, pObj, i )
         p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
-    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
+    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
     return vMapped;
 }
 
@@ -100,7 +113,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
   SeeAlso     []
 
 ***********************************************************************/
-int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped )
+int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped, int fPreorder )
 {
     Aig_Obj_t * pLeaf;
     Cnf_Cut_t * pCutBest;
@@ -109,15 +122,32 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
         return 0;
     assert( Aig_ObjIsAnd(pObj) );
     assert( pObj->pData != NULL );
+    // add the node to the mapping
+    if ( vMapped && fPreorder )
+         Vec_PtrPush( vMapped, pObj );
     // visit the transitive fanin of the selected cut
-    pCutBest = pObj->pData;
-    assert( pCutBest->Cost < 127 );
-    aArea = pCutBest->Cost;
-    Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
-        aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped );
-    // collect the node first to derive pre-order
-    if ( vMapped )
-        Vec_PtrPush( vMapped, pObj );
+    if ( pObj->fMarkB )
+    {
+        Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
+        Aig_ObjCollectSuper( pObj, vSuper );
+        aArea = Vec_PtrSize(vSuper) + 1;
+        Vec_PtrForEachEntry( vSuper, pLeaf, i )
+            aArea += Cnf_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped, fPreorder );
+        Vec_PtrFree( vSuper );
+        ////////////////////////////
+        pObj->fMarkB = 1;
+    }
+    else
+    {
+        pCutBest = pObj->pData;
+        assert( pCutBest->Cost < 127 );
+        aArea = pCutBest->Cost;
+        Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
+            aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped, fPreorder );
+    }
+    // add the node to the mapping
+    if ( vMapped && !fPreorder )
+         Vec_PtrPush( vMapped, pObj );
     return aArea;
 }
 
@@ -132,7 +162,7 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect )
+Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
 {
     Vec_Ptr_t * vMapped = NULL;
     Aig_Obj_t * pObj;
@@ -146,8 +176,8 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect )
     // collect nodes reachable from POs in the DFS order through the best cuts
     p->aArea = 0;
     Aig_ManForEachPo( p->pManAig, pObj, i )
-        p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
-    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
+        p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder );
+    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
     return vMapped;
 }
 
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 22c4240a..41a00732 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -127,42 +127,15 @@ int Cnf_IsopCountLiterals( Vec_Int_t * vIsop, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Cnf_SopWriteCube( char Cube, int * pVars, int fCompl, int * pLiterals )
-{
-    int nLits = 4, b;
-    for ( b = 0; b < 4; b++ )
-    {
-        if ( Cube % 3 == 0 )
-            *pLiterals++ = 2 * pVars[b] + !fCompl;
-        else if ( Cube % 3 == 1 )
-            *pLiterals++ = 2 * pVars[b] + fCompl;
-        else
-            nLits--;
-        Cube = Cube / 3;
-    }
-    return nLits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the cube and returns the number of literals in it.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int fCompl, int * pLiterals )
+int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int * pLiterals )
 {
     int nLits = nVars, b;
     for ( b = 0; b < nVars; b++ )
     {
-        if ( (Cube & 3) == 1 )
-            *pLiterals++ = 2 * pVars[b] + !fCompl;
-        else if ( (Cube & 3) == 2 )
-            *pLiterals++ = 2 * pVars[b] + fCompl;
+        if ( (Cube & 3) == 1 ) // value 0 --> write positive literal
+            *pLiterals++ = 2 * pVars[b];
+        else if ( (Cube & 3) == 2 ) // value 1 --> write negative literal
+            *pLiterals++ = 2 * pVars[b] + 1;
         else
             nLits--;
         Cube >>= 2;
@@ -186,9 +159,10 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
     Aig_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
     Cnf_Cut_t * pCut;
+    Vec_Int_t * vCover, * vSopTemp;
     int OutVar, pVars[32], * pLits, ** pClas;
     unsigned uTruth;
-    int i, k, nLiterals, nClauses, nCubes, Cube, Number;
+    int i, k, nLiterals, nClauses, Cube, Number;
 
     // count the number of literals and clauses
     nLiterals = 1 + Aig_ManPoNum( p->pManAig );
@@ -249,6 +223,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
     pCnf->nVars = Number;
 
     // assign the clauses
+    vSopTemp = Vec_IntAlloc( 1 << 16 );
     pLits = pCnf->pClauses[0];
     pClas = pCnf->pClauses;
     Vec_PtrForEachEntry( vMapped, pObj, i )
@@ -267,48 +242,36 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
         if ( pCut->nFanins < 5 )
         {
             uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
-            nCubes = p->pSopSizes[uTruth];
-            for ( k = 0; k < nCubes; k++ )
-            {
-                *pClas++ = pLits;
-                *pLits++ = 2 * OutVar + 1; 
-                pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 0, pLits );
-            }
+            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
+            vCover = vSopTemp;
         }
         else
+            vCover = pCut->vIsop[1];
+        Vec_IntForEachEntry( vCover, Cube, k )
         {
-            Vec_IntForEachEntry( pCut->vIsop[1], Cube, k )
-            {
-                *pClas++ = pLits;
-                *pLits++ = 2 * OutVar + 1; 
-                pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 0, pLits );
-            }
+            *pClas++ = pLits;
+            *pLits++ = 2 * OutVar; 
+            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
         }
 
         // negative polarity of the cut
         if ( pCut->nFanins < 5 )
         {
             uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
-            nCubes = p->pSopSizes[uTruth];
-            for ( k = 0; k < nCubes; k++ )
-            {
-                *pClas++ = pLits;
-                *pLits++ = 2 * OutVar; 
-                pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 1, pLits );
-            }
+            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
+            vCover = vSopTemp;
         }
         else
+            vCover = pCut->vIsop[0];
+        Vec_IntForEachEntry( vCover, Cube, k )
         {
-            Vec_IntForEachEntry( pCut->vIsop[0], Cube, k )
-            {
-                *pClas++ = pLits;
-                *pLits++ = 2 * OutVar; 
-                pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 1, pLits );
-            }
+            *pClas++ = pLits;
+            *pLits++ = 2 * OutVar + 1; 
+            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
         }
-//printf( "%d ", pClas-pCnf->pClauses );
     }
-
+    Vec_IntFree( vSopTemp );
+ 
     // write the constant literal
     OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ];
     assert( OutVar <= Aig_ManObjIdMax(p->pManAig) );