Improvements to the new technology mapper.

src/aig/gia/gia.h

@@ -242,16 +242,19 @@ struct Jf_Par_t_
     int            nRounds;
     int            DelayTarget;
     int            fAreaOnly;
+    int            fOptEdge;
     int            fCoarsen;
     int            fCutMin;
     int            fUseTts;
+    int            fGenCnf;
     int            fVerbose;
     int            fVeryVerbose;
     int            nLutSizeMax;
     int            nCutNumMax;
-    int            Delay;
-    int            Area;
-    int            Edge;
+    word           Delay;
+    word           Area;
+    word           Edge;
+    word           Clause;
 };
 
 static inline unsigned     Gia_ObjCutSign( unsigned ObjId )       { return (1 << (ObjId & 31));                                 }

src/base/abci/abc.c

@@ -29847,7 +29847,7 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Jf_ManSetDefaultPars( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDacmtvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDaekmtcvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -29904,7 +29904,10 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             pPars->fAreaOnly ^= 1;
             break;
-        case 'c':
+        case 'e':
+            pPars->fOptEdge ^= 1;
+            break;
+        case 'k':
             pPars->fCoarsen ^= 1;
             break;
         case 'm':
@@ -29913,6 +29916,9 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pPars->fUseTts ^= 1;
             break;
+        case 'c':
+            pPars->fGenCnf ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -29951,16 +29957,18 @@ usage:
         sprintf(Buffer, "best possible" );
     else
         sprintf(Buffer, "%d", pPars->DelayTarget );
-    Abc_Print( -2, "usage: &jf [-KCRD num] [-acmtvwh]\n" );
+    Abc_Print( -2, "usage: &jf [-KCRD num] [-akmtcvwh]\n" );
     Abc_Print( -2, "\t           performs technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : LUT size for the mapping (2 <= K <= %d) [default = %d]\n", pPars->nLutSizeMax, pPars->nLutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (1 <= C <= %d) [default = %d]\n", pPars->nCutNumMax, pPars->nCutNum );
     Abc_Print( -2, "\t-R num   : the number of mapping rounds [default = %d]\n", pPars->nRounds );
     Abc_Print( -2, "\t-D num   : sets the delay constraint for the mapping [default = %s]\n", Buffer );
     Abc_Print( -2, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fAreaOnly? "yes": "no" );
-    Abc_Print( -2, "\t-c       : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );
+    Abc_Print( -2, "\t-e       : toggles edge vs node minimization [default = %s]\n", pPars->fOptEdge? "yes": "no" );
+    Abc_Print( -2, "\t-k       : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );
     Abc_Print( -2, "\t-m       : toggles cut minimization [default = %s]\n", pPars->fCutMin? "yes": "no" );
     Abc_Print( -2, "\t-t       : toggles truth tables for minimization [default = %s]\n", pPars->fUseTts? "yes": "no" );
+    Abc_Print( -2, "\t-c       : toggles mapping for CNF generation [default = %s]\n", pPars->fGenCnf? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : toggles very verbose output [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");

src/map/if/ifTruth.c

@@ -675,6 +675,42 @@ int If_CutComputeTruth2( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut
     return 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+int If_CutComputeTruth3( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+    int fCompl, truthId;
+    int iFuncLit0   = pCut0->iDsd;
+    int iFuncLit1   = pCut1->iDsd;
+    int nWords      = Abc_TtWordNum( pCut->nLimit );
+    word * pTruth0s = Vec_MemReadEntry( p->vTtMem, Abc_Lit2Var(iFuncLit0) );
+    word * pTruth1s = Vec_MemReadEntry( p->vTtMem, Abc_Lit2Var(iFuncLit1) );
+    word * pTruth0  = (word *)p->puTemp[0];
+    word * pTruth1  = (word *)p->puTemp[1];
+    word * pTruth   = (word *)p->puTemp[2];
+    Abc_TtCopy( pTruth0, pTruth0s, nWords, fCompl0 ^ pCut0->fCompl ^ Abc_LitIsCompl(iFuncLit0) );
+    Abc_TtCopy( pTruth1, pTruth1s, nWords, fCompl1 ^ pCut1->fCompl ^ Abc_LitIsCompl(iFuncLit1) );
+    Abc_TtStretch( pTruth0, pCut->nLimit, pCut0->pLeaves, pCut0->nLeaves, pCut->pLeaves, pCut->nLeaves );
+    Abc_TtStretch( pTruth1, pCut->nLimit, pCut1->pLeaves, pCut1->nLeaves, pCut->pLeaves, pCut->nLeaves );
+    fCompl         = (pTruth0[0] & pTruth1[0] & 1);
+    Abc_TtAnd( pTruth, pTruth0, pTruth1, nWords, fCompl );
+    pCut->nLeaves  = Abc_TtMinBase( pTruth, pCut->pLeaves, pCut->nLeaves );
+    truthId        = Vec_MemHashInsert( p->vTtMem, pTruth );
+    pCut->iDsd     = Abc_Var2Lit( truthId, fCompl );
+    assert( (pTruth[0] & 1) == 0 );
+    return 1;
+}
+*/
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/misc/extra/extra.h

@@ -226,6 +226,7 @@ extern int         Sdm_ManReadDsdAndNum( Sdm_Man_t * p, int iDsd );
 extern int         Sdm_ManReadDsdClauseNum( Sdm_Man_t * p, int iDsd );
 extern word        Sdm_ManReadDsdTruth( Sdm_Man_t * p, int iDsd );
 extern char *      Sdm_ManReadDsdStr( Sdm_Man_t * p, int iDsd );
+extern void        Sdm_ManReadCnfCosts( Sdm_Man_t * p, int * pCosts, int nCosts );
 
 /*=== extraUtilProgress.c ================================================================*/
 

src/misc/extra/extraUtilDsd.c

@@ -1014,6 +1014,14 @@ char * Sdm_ManReadDsdStr( Sdm_Man_t * p, int iDsd )
 {
     return p->pDsd6[iDsd].pStr;
 }
+void Sdm_ManReadCnfCosts( Sdm_Man_t * p, int * pCosts, int nCosts )
+{
+    int i;
+    assert( nCosts == DSD_CLASS_NUM );
+    pCosts[0] = pCosts[1] = 0;
+    for ( i = 2; i < DSD_CLASS_NUM; i++ )
+        pCosts[i] = Sdm_ManReadDsdClauseNum( p, i );
+}
 
 
 /**Function*************************************************************
@@ -1104,6 +1112,46 @@ void Sdm_ManTest()
     Sdm_ManFree( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+void Sdm_ManCompareCnfSizes()
+{
+    Vec_Int_t * vMemory;
+    word uTruth;
+    int i, nSop0, nSop1, nVars, nCla, RetValue;
+    vMemory = Vec_IntAlloc( 1 << 16 );
+    for ( i = 1; i < DSD_CLASS_NUM; i++ )
+    {
+        uTruth = Sdm_ManReadDsdTruth( s_SdmMan, i );
+        nVars = Sdm_ManReadDsdVarNum( s_SdmMan, i );
+        nCla = Sdm_ManReadDsdClauseNum( s_SdmMan, i );
+
+        RetValue = Kit_TruthIsop( &uTruth, nVars, vMemory, 0 );
+        nSop0 = Vec_IntSize(vMemory);
+
+        uTruth = ~uTruth;
+        RetValue = Kit_TruthIsop( &uTruth, nVars, vMemory, 0 );
+        nSop1 = Vec_IntSize(vMemory);
+
+        if ( nSop0 + nSop1 != nCla )
+            printf( "Class %4d : %d + %d != %d\n", i, nSop0, nSop1, nCla );
+        else
+            printf( "Class %4d : %d + %d == %d\n", i, nSop0, nSop1, nCla );
+    }
+    Vec_IntFree( vMemory );
+}
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////