1 files changed, 82 insertions, 7 deletions

diff --git a/src/base/abci/abcRec3.c b/src/base/abci/abcRec3.c
index 6bf3dce7..e76d904a 100644
--- a/src/base/abci/abcRec3.c
+++ b/src/base/abci/abcRec3.c
@@ -928,25 +928,21 @@ Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
     assert( Gia_ObjIsAnd( Gia_ObjFanin0(pGiaPo) ) );
     Gia_ObjCollectInternal( pGia, Gia_ObjFanin0(pGiaPo) );
     assert( Vec_IntSize(pGia->vTtNodes) > 0 );
+
     // collect HOP nodes for leaves
     Vec_PtrClear( p->vLabelsP );
     for ( i = 0; i < nLeaves; i++ )
-    {
-        pHopObj = Hop_IthVar( pMan, pCanonPerm[i] );
-        pHopObj = Hop_NotCond( pHopObj, (uCanonPhase >> i) & 1 );
-        Vec_PtrPush(p->vLabelsP, pHopObj);
-    }
+        Vec_PtrPush( p->vLabelsP, Hop_NotCond(Hop_IthVar(pMan, pCanonPerm[i]), (uCanonPhase >> i) & 1) );
+
     // compute HOP nodes for internal nodes
     Gia_ManForEachObjVec( pGia->vTtNodes, pGia, pGiaTemp, i )
     {
         pGiaTemp->fMark0 = 0; // unmark node marked by Gia_ObjCollectInternal()
-
         if ( Gia_ObjIsAnd(Gia_ObjFanin0(pGiaTemp)) )
             pFan0 = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjNum(pGia, Gia_ObjFanin0(pGiaTemp)) + nLeaves);
         else
             pFan0 = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjCioId(Gia_ObjFanin0(pGiaTemp)));
         pFan0 = Hop_NotCond(pFan0, Gia_ObjFaninC0(pGiaTemp));
-
         if ( Gia_ObjIsAnd(Gia_ObjFanin1(pGiaTemp)) )
             pFan1 = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjNum(pGia, Gia_ObjFanin1(pGiaTemp)) + nLeaves);
         else
@@ -963,6 +959,85 @@ Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
     return Hop_NotCond( pHopObj,  Gia_ObjFaninC0(pGiaPo) ^ ((uCanonPhase >> nLeaves) & 1) );    
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Reexpresses the best structure of the cut in the GIA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_RecToGia3( Gia_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj, Vec_Int_t * vLeaves, int fHash )
+{
+    Lms_Man_t * p = s_pMan3;
+    char pCanonPerm[16];
+    unsigned uCanonPhase;
+    int iFan0, iFan1, iGiaObj;
+    Gia_Man_t * pGia = p->pGia;
+    Gia_Obj_t * pGiaPo, * pGiaTemp = NULL;
+    int i, uSupport, BestPo = -1, nLeaves = If_CutLeaveNum(pCut);
+    assert( pIfMan->pPars->fCutMin == 1 );
+    assert( nLeaves > 1 );
+    assert( nLeaves == Vec_IntSize(vLeaves) );
+
+    // compute support
+    uSupport = Abc_TtSupport( If_CutTruthW(pCut), nLeaves );
+    if ( uSupport == 0 )
+        return Abc_LitNotCond( 0, (int)(*If_CutTruthW(pCut) & 1) );
+    if ( !Abc_TtSuppIsMinBase(uSupport) || uSupport == 1 )
+    {
+        assert( Abc_TtSuppOnlyOne(uSupport) );
+        return Abc_LitNotCond( Vec_IntEntry(vLeaves, Abc_TtSuppFindFirst(uSupport)), (int)(*If_CutTruthW(pCut) & 1) );
+    }
+    assert( Gia_WordCountOnes(uSupport) == nLeaves );
+
+    // get the best output for this node
+    If_CutFindBestStruct( pIfMan, pCut, pCanonPerm, &uCanonPhase, &BestPo );
+    assert( BestPo >= 0 );
+    pGiaPo = Gia_ManCo( pGia, BestPo );
+
+    // collect internal nodes into pGia->vTtNodes
+    if ( pGia->vTtNodes == NULL )
+        pGia->vTtNodes = Vec_IntAlloc( 256 );
+    assert( Gia_ObjIsAnd( Gia_ObjFanin0(pGiaPo) ) );
+    Gia_ObjCollectInternal( pGia, Gia_ObjFanin0(pGiaPo) );
+    assert( Vec_IntSize(pGia->vTtNodes) > 0 );
+
+    // collect GIA nodes for leaves
+    Vec_IntClear( p->vLabels );
+    for (i = 0; i < nLeaves; i++)
+        Vec_IntPush( p->vLabels, Abc_LitNotCond(Vec_IntEntry(vLeaves, pCanonPerm[i]), (uCanonPhase >> i) & 1) );
+
+    // compute HOP nodes for internal nodes
+    Gia_ManForEachObjVec( pGia->vTtNodes, pGia, pGiaTemp, i )
+    {
+        pGiaTemp->fMark0 = 0; // unmark node marked by Gia_ObjCollectInternal()
+        if ( Gia_ObjIsAnd(Gia_ObjFanin0(pGiaTemp)) )
+            iFan0 = Vec_IntEntry(p->vLabels, Gia_ObjNum(pGia, Gia_ObjFanin0(pGiaTemp)) + nLeaves);
+        else
+            iFan0 = Vec_IntEntry(p->vLabels, Gia_ObjCioId(Gia_ObjFanin0(pGiaTemp)));
+        iFan0 = Abc_LitNotCond(iFan0, Gia_ObjFaninC0(pGiaTemp));
+        if ( Gia_ObjIsAnd(Gia_ObjFanin1(pGiaTemp)) )
+            iFan1 = Vec_IntEntry(p->vLabels, Gia_ObjNum(pGia, Gia_ObjFanin1(pGiaTemp)) + nLeaves);
+        else
+            iFan1 = Vec_IntEntry(p->vLabels, Gia_ObjCioId(Gia_ObjFanin1(pGiaTemp)));
+        iFan1 = Abc_LitNotCond(iFan1, Gia_ObjFaninC1(pGiaTemp));
+        if ( fHash )
+            iGiaObj = Gia_ManHashAnd(pMan, iFan0, iFan1);
+        else
+            iGiaObj = Gia_ManAppendAnd(pMan, iFan0, iFan1);
+        Vec_IntPush(p->vLabels, iGiaObj);
+    }
+    // get the final result
+    assert( Gia_ObjIsAnd(pGiaTemp) );
+    iGiaObj = Vec_IntEntry(p->vLabels, Gia_ObjNum(pGia, pGiaTemp) + nLeaves);
+    // complement the result if needed
+    return Abc_LitNotCond( iGiaObj,  Gia_ObjFaninC0(pGiaPo) ^ ((uCanonPhase >> nLeaves) & 1) );    
+}
+
 
 /**Function*************************************************************