Version abc80705

12 files changed, 198 insertions, 26 deletions

diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index bf109b17..5c742f5d 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -140,6 +140,8 @@ extern void            Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
 extern void *          Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
 extern int             Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
+extern int             Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf );
+extern void            Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf );
 /*=== cnfMap.c ========================================================*/
 extern void            Cnf_DeriveMapping( Cnf_Man_t * p );
 extern int             Cnf_ManMapForCnf( Cnf_Man_t * p );
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index fc71f936..e3e6bfe1 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -20,6 +20,7 @@
 
 #include "cnf.h"
 #include "satSolver.h"
+#include "zlib.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -237,7 +238,7 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable )
   SeeAlso     []
 
 ***********************************************************************/
-void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
+void Cnf_DataWriteIntoFile_old( Cnf_Dat_t * p, char * pFileName, int fReadable )
 {
     FILE * pFile;
     int * pLit, * pStop, i;
@@ -270,6 +271,39 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
   SeeAlso     []
 
 ***********************************************************************/
+void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
+{
+    gzFile pFile;
+    int * pLit, * pStop, i;
+    pFile = gzopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
+        return;
+    }
+    gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
+    gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
+    for ( i = 0; i < p->nClauses; i++ )
+    {
+        for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
+            gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
+        gzprintf( pFile, "0\n" );
+    }
+    gzprintf( pFile, "\n" );
+    gzclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes CNF into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
 {
     sat_solver * pSat;
@@ -379,6 +413,63 @@ int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds the OR-clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf )
+{
+    sat_solver * pSat = p;
+    Aig_Obj_t * pObj;
+    int i, Lit;
+    Aig_ManForEachPo( pCnf->pMan, pObj, i )
+    {
+        Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+        if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
+            return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms polarity of the internal veriables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf )
+{
+    Aig_Obj_t * pObj;
+    int * pVarToPol;
+    int i, iVar;
+    // create map from the variable number to its polarity
+    pVarToPol = CALLOC( int, pCnf->nVars );
+    Aig_ManForEachObj( pCnf->pMan, pObj, i )
+        if ( !Aig_ObjIsPo(pObj) && pCnf->pVarNums[pObj->Id] >= 0 )
+            pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase;
+    // transform literals
+    for ( i = 0; i < pCnf->nLiterals; i++ )
+    {
+        iVar = lit_var(pCnf->pClauses[0][i]);
+        assert( iVar < pCnf->nVars );
+        if ( pVarToPol[iVar] )
+            pCnf->pClauses[0][i] = lit_neg( pCnf->pClauses[0][i] );
+    }
+    free( pVarToPol );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c
index cd47cb58..3738fee5 100644
--- a/src/aig/cnf/cnfUtil.c
+++ b/src/aig/cnf/cnfUtil.c
@@ -140,6 +140,7 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
     else
     {
         pCutBest = pObj->pData;
+//        assert( pCutBest->nFanins > 0 );
         assert( pCutBest->Cost < 127 );
         aArea = pCutBest->Cost;
         Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index e9e7ad9c..6721634e 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -282,7 +282,7 @@ static inline int          Fra_ImpCreate( int Left, int Right )
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraCec.c ========================================================*/
-extern int                 Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose );
+extern int                 Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
 extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose );
 extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose );
 /*=== fraClass.c ========================================================*/
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index d67839a4..e5940992 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -40,7 +40,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVerbose )
+int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
 {
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
@@ -53,6 +53,10 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
     // derive CNF
     pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
 //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
+
+    if ( fFlipBits ) 
+        Cnf_DataTranformPolarity( pCnf );
+
     // convert into SAT solver
     pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     if ( pSat == NULL )
@@ -60,12 +64,27 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
         Cnf_DataFree( pCnf );
         return 1;
     }
-    // add the OR clause for the outputs
-    if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
+
+
+    if ( fAndOuts )
     {
-        sat_solver_delete( pSat );
-        Cnf_DataFree( pCnf );
-        return 1;
+        // assert each output independently
+        if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
+        {
+            sat_solver_delete( pSat );
+            Cnf_DataFree( pCnf );
+            return 1;
+        }
+    }
+    else
+    {
+        // add the OR clause for the outputs
+        if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
+        {
+            sat_solver_delete( pSat );
+            Cnf_DataFree( pCnf );
+            return 1;
+        }
     }
     vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
     Cnf_DataFree( pCnf );
@@ -160,7 +179,7 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose )
 
     // if SAT only, solve without iteration
 clk = clock();
-    RetValue = Fra_FraigSat( pAig, (sint64)2*nBTLimitStart, (sint64)0, 0 );
+    RetValue = Fra_FraigSat( pAig, (sint64)2*nBTLimitStart, (sint64)0, 1, 0, 0 );
     if ( fVerbose )
     {
         printf( "Initial SAT:      Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
@@ -228,7 +247,7 @@ PRT( "Time", clock() - clk );
     if ( RetValue == -1 )
     {
 clk = clock();
-        RetValue = Fra_FraigSat( pAig, (sint64)nBTLimitLast, (sint64)0, 0 );
+        RetValue = Fra_FraigSat( pAig, (sint64)nBTLimitLast, (sint64)0, 1, 0, 0 );
         if ( fVerbose )
         {
             printf( "Final SAT:            Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index ab076472..1935bb7f 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -437,6 +437,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
  
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
+    p->pPars->nBTLimitNode = 0;
     // derive and refine e-classes using K initialized frames
     if ( fUseOldSimulation )
     {
@@ -529,6 +530,7 @@ p->timeTrav += clock() - clk2;
             pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
         else
             pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+//        Cnf_DataTranformPolarity( pCnf );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
 
         p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index e1d3edd1..b0f3b1fb 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -377,6 +377,7 @@ extern ABC_DLL void            Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManTransformInitValues( Ntl_Man_t * p );
 extern ABC_DLL Vec_Vec_t *     Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVerbose );
+extern ABC_DLL void            Ntl_ManFilterRegisterClasses( Aig_Man_t * pAig, Vec_Int_t * vRegClasses, int fVerbose );
 extern ABC_DLL int             Ntl_ManLatchNum( Ntl_Man_t * p );
 extern ABC_DLL int             Ntl_ManIsComb( Ntl_Man_t * p );
 extern ABC_DLL int             Ntl_ModelCombLeafNum( Ntl_Mod_t * p );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index f6f1ebb2..f4d33cf1 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -649,9 +649,9 @@ Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p, int nMinDomSize )
     if ( pAig->vClockDoms )
     {
         if ( Vec_VecSize(pAig->vClockDoms) == 0 )
-            printf( "Clock domains are small. Seq synthesis is not performed.\n" );
+            printf( "Register classes are small. Seq synthesis is not performed.\n" );
         else
-            printf( "Performing seq synthesis for %d clock domains.\n", Vec_VecSize(pAig->vClockDoms) );
+            printf( "Performing seq synthesis for %d register classes.\n", Vec_VecSize(pAig->vClockDoms) );
         printf( "\n" );
     }
     return pAig;
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 6449cc33..bd39956e 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -320,6 +320,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
     // perform SCL for the given design
     pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
     Aig_ManStop( pTemp );
+    if ( pNew->vRegClasses && Vec_IntSize(pNew->vRegClasses) && pAigCol->pReprs )
+        Ntl_ManFilterRegisterClasses( pAigCol, pNew->vRegClasses, fVerbose );
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
@@ -353,6 +355,8 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
     // perform SCL for the given design
     pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
     Aig_ManStop( pTemp );
+    if ( p->vRegClasses && Vec_IntSize(p->vRegClasses) && pAigCol->pReprs )
+        Ntl_ManFilterRegisterClasses( pAigCol, p->vRegClasses, fVerbose );
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index 4fd1762c..51f3b818 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -403,7 +403,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
         printf( "The number of register clases = %d.\n", nClasses );
         for ( i = 0; i <= ClassMax; i++ )
             if ( pClassNums[i] )
-                printf( "%d:%d  ", i, pClassNums[i] );
+                printf( "(%d, %d)  ", i, pClassNums[i] );
         printf( "\n" );
     }
     // skip if there is only one class
@@ -416,7 +416,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
             vPart = Vec_IntStartNatural( Vec_IntSize(pMan->vRegClasses) );
             Vec_PtrPush( vParts, vPart );
         }
-        printf( "There is only one clock domain with %d registers.\n", Vec_IntSize(pMan->vRegClasses) );
+        printf( "There is only one class with %d registers.\n", Vec_IntSize(pMan->vRegClasses) );
         free( pClassNums );
         return (Vec_Vec_t *)vParts;
     }
@@ -434,12 +434,13 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
         Vec_PtrPush( vParts, vPart );
     }
     free( pClassNums );
+    Vec_VecSort( (Vec_Vec_t *)vParts, 1 );
     // report the selected classes
     if ( fVerbose )
     {
         printf( "The number of selected register clases = %d.\n", Vec_PtrSize(vParts) );
         Vec_PtrForEachEntry( vParts, vPart, i )
-            printf( "%d:%d  ", i, Vec_IntSize(vPart) );
+            printf( "(%d, %d)  ", i, Vec_IntSize(vPart) );
         printf( "\n" );
     }
     return (Vec_Vec_t *)vParts;
@@ -447,6 +448,57 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
 
 /**Function*************************************************************
 
+  Synopsis    [Filter register clases using clock-domain information.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManFilterRegisterClasses( Aig_Man_t * pAig, Vec_Int_t * vRegClasses, int fVerbose )
+{
+    Aig_Obj_t * pObj, * pRepr;
+    int i, k, nOmitted, nTotal;
+    if ( pAig->pReprs == NULL )
+        return;
+    assert( pAig->nRegs > 0 );
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->PioNum = -1;
+    k = 0;
+    Aig_ManForEachLoSeq( pAig, pObj, i )
+        pObj->PioNum = k++;
+    // consider equivalences
+    nOmitted = nTotal = 0;
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        pRepr = pAig->pReprs[pObj->Id];
+        if ( pRepr == NULL )
+            continue;
+        nTotal++;
+        assert( Aig_ObjIsPi(pObj) );
+        assert( Aig_ObjIsPi(pRepr) || Aig_ObjIsConst1(pRepr) );
+        if ( Aig_ObjIsConst1(pRepr) )
+            continue;
+        assert( pObj->PioNum >= 0 && pRepr->PioNum >= 0 );
+        // remove equivalence if they belong to different classes
+        if ( Vec_IntEntry( vRegClasses, pObj->PioNum ) == 
+             Vec_IntEntry( vRegClasses, pRepr->PioNum ) )
+             continue;
+         pAig->pReprs[pObj->Id] = NULL;
+         nOmitted++;
+    }
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->PioNum = -1;
+    if ( fVerbose )
+        printf( "Omitted %d (out of %d) equivs due to register class mismatch.\n", 
+            nOmitted, nTotal );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of CIs in the model.]
 
   Description []
diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c
index 64508474..fc56b387 100644
--- a/src/aig/nwk/nwkTiming.c
+++ b/src/aig/nwk/nwkTiming.c
@@ -589,14 +589,14 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj )
         {
             if ( pManTime )
             {
-                // it may happen that a box-input (CO) was already marked as visited
-                // when some other box-input of the same box was visited - here we undo this
                 iBox = Tim_ManBoxForCo( pManTime, pTemp->PioId );
-                if ( Tim_ManIsCoTravIdCurrent( pManTime, pTemp->PioId ) )
-                    Tim_ManSetPreviousTravIdBoxInputs( pManTime, iBox );
-                Tim_ManSetCoArrival( pManTime, pTemp->PioId, tArrival );
                 if ( iBox >= 0 ) // this CO is an input of the box
                 {
+                    // it may happen that a box-input (CO) was already marked as visited
+                    // when some other box-input of the same box was visited - here we undo this
+                    if ( Tim_ManIsCoTravIdCurrent( pManTime, pTemp->PioId ) )
+                        Tim_ManSetPreviousTravIdBoxInputs( pManTime, iBox );
+                    Tim_ManSetCoArrival( pManTime, pTemp->PioId, tArrival );
                     Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
                     iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
                     nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
@@ -673,14 +673,14 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj )
         {
             if ( pManTime )
             {
-                // it may happen that a box-output (CI) was already marked as visited
-                // when some other box-output of the same box was visited - here we undo this
                 iBox = Tim_ManBoxForCi( pManTime, pTemp->PioId );
-                if ( Tim_ManIsCiTravIdCurrent( pManTime, pTemp->PioId ) )
-                    Tim_ManSetPreviousTravIdBoxOutputs( pManTime, iBox );
-                Tim_ManSetCiRequired( pManTime, pTemp->PioId, tRequired );
                 if ( iBox >= 0 ) // this CI is an output of the box
                 {
+                    // it may happen that a box-output (CI) was already marked as visited
+                    // when some other box-output of the same box was visited - here we undo this
+                    if ( Tim_ManIsCiTravIdCurrent( pManTime, pTemp->PioId ) )
+                        Tim_ManSetPreviousTravIdBoxOutputs( pManTime, iBox );
+                    Tim_ManSetCiRequired( pManTime, pTemp->PioId, tRequired );
                     Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox );
                     iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
                     nTerms = Tim_ManBoxInputNum( pManTime, iBox );
diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
index afc4a34a..ae8d02ec 100644
--- a/src/aig/saig/saigInter.c
+++ b/src/aig/saig/saigInter.c
@@ -412,7 +412,7 @@ int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
         pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
         RetValue = Fra_FraigMiterStatus( pAigTemp );
         Aig_ManStop( pAigTemp );
-//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0 );
+//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
     }
     assert( RetValue != -1 );
     Aig_ManStop( pMiter );