Producing AIG after structural mapping.

5 files changed, 40 insertions, 25 deletions

diff --git a/src/aig/gia/giaFx.c b/src/aig/gia/giaFx.c
index 8a8c7416..4ca28b69 100644
--- a/src/aig/gia/giaFx.c
+++ b/src/aig/gia/giaFx.c
@@ -193,7 +193,7 @@ Vec_Wec_t * Gia_ManFxRetrieve( Gia_Man_t * p, Vec_Str_t ** pvCompl, int fReverse
     // compute truth tables
     nCutSize = Gia_ManLutSizeMax( p );
     nWords = Abc_Truth6WordNum( nCutSize );
-    vTruths = Gia_ManComputeTruths( p, Abc_MaxInt(6, nCutSize), nItems - Gia_ManCiNum(p), fReverse );
+    vTruths = Gia_ManComputeTruths( p, nCutSize, nItems - Gia_ManCiNum(p), fReverse );
     vCover = Vec_IntAlloc( 1 << 16 );
     // collect cubes
     vCubes = Vec_WecAlloc( 1000 );
diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c
index fe7b52a6..f8146406 100644
--- a/src/aig/gia/giaJf.c
+++ b/src/aig/gia/giaJf.c
@@ -1446,8 +1446,7 @@ Gia_Man_t * Jf_ManDeriveGia( Jf_Man_t * p )
     Vec_Int_t * vCover    = Vec_IntAlloc( 1 << 16 );
     Vec_Int_t * vLeaves   = Vec_IntAlloc( 16 );
     int i, k, iLit, Class, * pCut;
-    word uTruth;
-    assert( p->pPars->fCutMin );
+    word * pTruth, uTruth = 0;
     // create new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
     pNew->pName = Abc_UtilStrsav( p->pGia->pName );
@@ -1457,6 +1456,8 @@ Gia_Man_t * Jf_ManDeriveGia( Jf_Man_t * p )
     Gia_ManForEachCi( p->pGia, pObj, i )
         Vec_IntWriteEntry( vCopies, Gia_ObjId(p->pGia, pObj), Gia_ManAppendCi(pNew) );
     // iterate through nodes used in the mapping
+    if ( !p->pPars->fCutMin )
+        Gia_ObjComputeTruthTableStart( p->pGia, p->pPars->nLutSize );
     Gia_ManHashStart( pNew );
     Gia_ManForEachAnd( p->pGia, pObj, i )
     {
@@ -1464,30 +1465,42 @@ Gia_Man_t * Jf_ManDeriveGia( Jf_Man_t * p )
             continue;
         pCut = Jf_ObjCutBest( p, i );
 //        printf( "Best cut of node %d:  ", i );  Jf_CutPrint(pCut);
-        Class = Jf_CutFuncClass( pCut );
-        uTruth = p->pPars->fFuncDsd ? Sdm_ManReadDsdTruth(p->pDsd, Class) : *Vec_MemReadEntry(p->vTtMem, Class);
-        assert( p->pDsd == NULL || Sdm_ManReadDsdVarNum(p->pDsd, Class) == Jf_CutSize(pCut) );
-        if ( Jf_CutSize(pCut) == 0 )
+        // get the truth table
+        if ( p->pPars->fCutMin )
         {
-            assert( Class == 0 );
-            Vec_IntWriteEntry( vCopies, i, Jf_CutFunc(pCut) );
-            continue;
+            Class = Jf_CutFuncClass( pCut );
+            uTruth = p->pPars->fFuncDsd ? Sdm_ManReadDsdTruth(p->pDsd, Class) : *Vec_MemReadEntry(p->vTtMem, Class);
+            assert( p->pDsd == NULL || Sdm_ManReadDsdVarNum(p->pDsd, Class) == Jf_CutSize(pCut) );
+            if ( Jf_CutSize(pCut) == 0 )
+            {
+                assert( Class == 0 );
+                Vec_IntWriteEntry( vCopies, i, Jf_CutFunc(pCut) );
+                continue;
+            }
+            if ( Jf_CutSize(pCut) == 1 )
+            {
+                assert( Class == 1 );
+                iLit = Abc_LitNotCond( Jf_CutLit(pCut, 1) , Jf_CutFuncCompl(pCut) );
+                iLit = Abc_Lit2LitL( Vec_IntArray(vCopies), iLit );
+                Vec_IntWriteEntry( vCopies, i, iLit );
+                continue;
+            }
+            pTruth = &uTruth;
         }
-        if ( Jf_CutSize(pCut) == 1 )
+        else
         {
-            assert( Class == 1 );
-            iLit = Abc_LitNotCond( Jf_CutLit(pCut, 1) , Jf_CutFuncCompl(pCut) );
-            iLit = Abc_Lit2LitL( Vec_IntArray(vCopies), iLit );
-            Vec_IntWriteEntry( vCopies, i, iLit );
-            continue;
+            Vec_IntClear( vLeaves );
+            Jf_CutForEachLit( pCut, iLit, k )
+                Vec_IntPush( vLeaves, Abc_Lit2Var(iLit) );
+            pTruth = Gia_ObjComputeTruthTableCut( p->pGia, pObj, vLeaves );
         }
-        // collect leaves
+        // collect incoming literals
         Vec_IntClear( vLeaves );
         Jf_CutForEachLit( pCut, iLit, k )
             Vec_IntPush( vLeaves, Abc_Lit2LitL(Vec_IntArray(vCopies), iLit) );
         // create GIA
-        iLit = Dsm_ManDeriveGia( pNew, uTruth, vLeaves, vCover );
-        iLit = Abc_LitNotCond( iLit, Jf_CutFuncCompl(pCut) );
+        iLit = Dsm_ManDeriveGia( pNew, pTruth, vLeaves, vCover );
+        iLit = Abc_LitNotCond( iLit, (p->pPars->fCutMin && Jf_CutFuncCompl(pCut)) );
         Vec_IntWriteEntry( vCopies, i, iLit );
     }
     Gia_ManForEachCo( p->pGia, pObj, i )
@@ -1495,6 +1508,8 @@ Gia_Man_t * Jf_ManDeriveGia( Jf_Man_t * p )
         iLit = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) );
         Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
     }
+    if ( !p->pPars->fCutMin )
+        Gia_ObjComputeTruthTableStop( p->pGia );
     Vec_IntFree( vCopies );
     Vec_IntFree( vLeaves );
     Vec_IntFree( vCover );
@@ -1527,7 +1542,7 @@ void Jf_ManSetDefaultPars( Jf_Par_t * pPars )
     pPars->fOptEdge     =  1; 
     pPars->fCoarsen     =  0;
     pPars->fCutMin      =  0;
-    pPars->fFuncDsd      =  0;
+    pPars->fFuncDsd     =  0;
     pPars->fGenCnf      =  0;
     pPars->fPureAig     =  0;
     pPars->fVerbose     =  0;
diff --git a/src/aig/gia/giaTruth.c b/src/aig/gia/giaTruth.c
index f1fecd36..c596048a 100644
--- a/src/aig/gia/giaTruth.c
+++ b/src/aig/gia/giaTruth.c
@@ -185,7 +185,7 @@ word * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj )
         p->nTtWords  = Abc_Truth6WordNum( p->nTtVars );
         p->vTtNums   = Vec_IntStart( Gia_ManObjNum(p) + 1000 );
         p->vTtNodes  = Vec_IntAlloc( 256 );
-        p->vTtInputs = Vec_PtrAllocTruthTables( p->nTtVars );
+        p->vTtInputs = Vec_PtrAllocTruthTables( Abc_MaxInt(6, p->nTtVars) );
         p->vTtMemory = Vec_WrdStart( p->nTtWords * 256 );
     }
     else
@@ -285,7 +285,7 @@ void Gia_ObjComputeTruthTableStart( Gia_Man_t * p, int nVarsMax )
     p->nTtVars   = nVarsMax;
     p->nTtWords  = Abc_Truth6WordNum( p->nTtVars );
     p->vTtNodes  = Vec_IntAlloc( 256 );
-    p->vTtInputs = Vec_PtrAllocTruthTables( p->nTtVars );
+    p->vTtInputs = Vec_PtrAllocTruthTables( Abc_MaxInt(6, p->nTtVars) );
     p->vTtMemory = Vec_WrdStart( p->nTtWords * 64 );
     p->vTtNums   = Vec_IntAlloc( Gia_ManObjNum(p) + 1000 );
     Vec_IntFill( p->vTtNums, Vec_IntCap(p->vTtNums), -ABC_INFINITY );
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 0ee50007..f91d2831 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -88,7 +88,7 @@ extern void          Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX
 extern int           Dau_DsdCheck1Step( word * pTruth, int nVarsInit );
 
 /*=== dauGia.c  ==========================================================*/
-extern int           Dsm_ManDeriveGia( void * p, word uTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover );
+extern int           Dsm_ManDeriveGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover );
 
 /*=== dauMerge.c  ==========================================================*/
 extern void          Dau_DsdRemoveBraces( char * pDsd, int * pMatches );
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
index b795336d..35965a92 100644
--- a/src/opt/dau/dauGia.c
+++ b/src/opt/dau/dauGia.c
@@ -210,14 +210,14 @@ int Dau_DsdToGia( Gia_Man_t * pGia, char * p, int * pLits, Vec_Int_t * vCover )
   SeeAlso     []
 
 ***********************************************************************/
-int Dsm_ManDeriveGia( void * p, word uTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover )
+int Dsm_ManDeriveGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover )
 {
     Gia_Man_t * pGia = (Gia_Man_t *)p;
     char pDsd[1000];
     int nSizeNonDec;
     m_Calls++;
 //    static int Counter = 0; Counter++;
-    nSizeNonDec = Dau_DsdDecompose( &uTruth, Vec_IntSize(vLeaves), 0, 1, pDsd );
+    nSizeNonDec = Dau_DsdDecompose( pTruth, Vec_IntSize(vLeaves), 0, 1, pDsd );
     if ( nSizeNonDec )
         m_NonDsd++;
 //    printf( "%s\n", pDsd );