Version abc90329

Makefile

@@ -12,7 +12,7 @@ MODULES := \
 	src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr \
 	src/bdd/parse src/bdd/reo src/bdd/cas \
 	src/map/fpga src/map/mapper src/map/mio src/map/super \
-	src/map/if src/map/amap \
+	src/map/if src/map/amap src/map/cov \
 	src/misc/extra src/misc/mvc src/misc/st src/misc/util \
 	src/misc/nm src/misc/vec src/misc/hash \
 	src/misc/bzlib src/misc/zlib \

abclib.dsp

@@ -1954,14 +1954,6 @@ SOURCE=.\src\map\if\ifTruth.c
 SOURCE=.\src\map\if\ifUtil.c
 # End Source File
 # End Group
-# Begin Group "ply"
-
-# PROP Default_Filter ""
-# End Group
-# Begin Group "pcm"
-
-# PROP Default_Filter ""
-# End Group
 # Begin Group "amap"
 
 # PROP Default_Filter ""
@@ -2026,6 +2018,46 @@ SOURCE=.\src\map\amap\amapRule.c
 SOURCE=.\src\map\amap\amapUniq.c
 # End Source File
 # End Group
+# Begin Group "cov"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\cov\cov.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\cov\covBuild.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\cov\covCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\cov\covInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\cov\covMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\cov\covMinEsop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\cov\covMinMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\cov\covMinSop.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\cov\covMinUtil.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "misc"
 
@@ -3547,6 +3579,10 @@ SOURCE=.\src\aig\cec\cecCec.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\cec\cecChoice.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\cec\cecClass.c
 # End Source File
 # Begin Source File
@@ -3555,6 +3591,10 @@ SOURCE=.\src\aig\cec\cecCore.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\cec\cecCorr.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\cec\cecInt.h
 # End Source File
 # Begin Source File
@@ -3651,6 +3691,10 @@ SOURCE=.\src\aig\gia\giaCof.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaCSat.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaDfs.c
 # End Source File
 # Begin Source File
@@ -3703,6 +3747,10 @@ SOURCE=.\src\aig\gia\giaMap.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaPat.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaRetime.c
 # End Source File
 # Begin Source File

src/aig/aig/aig.h

@@ -647,7 +647,7 @@ extern void            Aig_ManCleanPioNumbers( Aig_Man_t * p );
 extern int             Aig_ManChoiceNum( Aig_Man_t * p );
 extern char *          Aig_FileNameGenericAppend( char * pBase, char * pSuffix );
 extern unsigned        Aig_ManRandom( int fReset );
-extern void            Aig_ManRandomInfo( Vec_Ptr_t * vInfo, int iWordStart, int iWordStop );
+extern void            Aig_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop );
 extern void            Aig_NodeUnionLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr );
 extern void            Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr );
 

src/aig/aig/aigMffc.c

@@ -176,9 +176,15 @@ void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin,
 int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp )
 {
     int ConeSize1, ConeSize2;
+    if ( vSupp ) Vec_PtrClear( vSupp );
+    if ( !Aig_ObjIsNode(pNode) )
+    {
+        if ( Aig_ObjIsPi(pNode) && vSupp )
+            Vec_PtrPush( vSupp, pNode );
+        return 0;
+    }
     assert( !Aig_IsComplement(pNode) );
     assert( Aig_ObjIsNode(pNode) );
-    if ( vSupp ) Vec_PtrClear( vSupp );
     Aig_ManIncrementTravId( p );
     ConeSize1 = Aig_NodeDeref_rec( pNode, LevelMin, NULL, NULL );
     Aig_NodeMffsSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL );

src/aig/aig/aigRepr.c

@@ -287,6 +287,10 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
     }
     else
     {
+//        Aig_ManForEachObj( p, pObj, i )
+//            if ( p->pReprs[i] )
+//                printf( "Substituting %d for %d.\n", p->pReprs[i]->Id, pObj->Id );
+
         Aig_ManForEachPo( p, pObj, i )
             Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
     }

src/aig/aig/aigTable.c

@@ -236,6 +236,7 @@ void Aig_TableProfile( Aig_Man_t * p )
 {
     Aig_Obj_t * pEntry;
     int i, Counter;
+    printf( "Table size = %d. Entries = %d.\n", p->nTableSize, Aig_ManNodeNum(p) );
     for ( i = 0; i < p->nTableSize; i++ )
     {
         Counter = 0;

src/aig/aig/aigUtil.c

@@ -1189,11 +1189,11 @@ unsigned Aig_ManRandom( int fReset )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManRandomInfo( Vec_Ptr_t * vInfo, int iWordStart, int iWordStop )
+void Aig_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop )
 {
     unsigned * pInfo;
     int i, w;
-    Vec_PtrForEachEntry( vInfo, pInfo, i )
+    Vec_PtrForEachEntryStart( vInfo, pInfo, i, iInputStart )
         for ( w = iWordStart; w < iWordStop; w++ )
             pInfo[w] = Aig_ManRandom(0);
 }

src/aig/cec/cec.h

@@ -61,6 +61,7 @@ struct Cec_ParSim_t_
     int              fCheckMiter;   // the circuit is the miter
     int              fFirstStop;    // stop on the first sat output
     int              fSeqSimulate;  // performs sequential simulation
+    int              fLatchCorr;    // consider only latch outputs
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
 };
@@ -113,6 +114,36 @@ struct Cec_ParCec_t_
     int              fVerbose;      // verbose stats
 };
 
+// sequential register correspodence parameters
+typedef struct Cec_ParCor_t_ Cec_ParCor_t;
+struct Cec_ParCor_t_
+{
+    int              nWords;        // the number of simulation words
+    int              nRounds;       // the number of simulation rounds
+    int              nFrames;       // the number of time frames
+    int              nBTLimit;      // conflict limit at a node
+    int              fLatchCorr;    // consider only latch outputs
+    int              fUseRings;     // use rings
+    int              fUseCSat;      // use circuit-based solver
+    int              fFirstStop;    // stop on the first sat output
+    int              fUseSmartCnf;  // use smart CNF computation
+    int              fVeryVerbose;  // verbose stats
+    int              fVerbose;      // verbose stats
+};
+
+// sequential register correspodence parameters
+typedef struct Cec_ParChc_t_ Cec_ParChc_t;
+struct Cec_ParChc_t_
+{
+    int              nWords;        // the number of simulation words
+    int              nRounds;       // the number of simulation rounds
+    int              nBTLimit;      // conflict limit at a node
+    int              fFirstStop;    // stop on the first sat output
+    int              fUseSmartCnf;  // use smart CNF computation
+    int              fVeryVerbose;  // verbose stats
+    int              fVerbose;      // verbose stats
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -124,12 +155,18 @@ struct Cec_ParCec_t_
 /*=== cecCec.c ==========================================================*/
 extern int           Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars );
 extern int           Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose );
+/*=== cecChoice.c ==========================================================*/
+extern Gia_Man_t *   Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars );
+/*=== cecCorr.c ==========================================================*/
+extern Gia_Man_t *   Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
 /*=== cecCore.c ==========================================================*/
 extern void          Cec_ManSatSetDefaultParams( Cec_ParSat_t * p );
 extern void          Cec_ManSimSetDefaultParams( Cec_ParSim_t * p );
 extern void          Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p );
 extern void          Cec_ManFraSetDefaultParams( Cec_ParFra_t * p );
 extern void          Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
+extern void          Cec_ManCorSetDefaultParams( Cec_ParCor_t * p );
+extern void          Cec_ManChcSetDefaultParams( Cec_ParChc_t * p );
 extern Gia_Man_t *   Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars );
 extern Gia_Man_t *   Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
 extern void          Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars );

src/aig/cec/cecChoice.c

+/**CFile****************************************************************
+
+  FileName    [cecChoice.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Computation of structural choices.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecChoice.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
+{
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/cec/cecClass.c

@@ -293,6 +293,48 @@ int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
 
 /**Function*************************************************************
 
+  Synopsis    [Refines one equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i )
+{
+    int iRepr, Ent;
+    if ( Gia_ObjIsConst(p->pAig, i) )
+    {
+        Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
+        return 1;
+    }
+    if ( !Gia_ObjIsClass(p->pAig, i) )
+        return 0;
+    assert( Gia_ObjIsClass(p->pAig, i) );
+    iRepr = Gia_ObjRepr( p->pAig, i );
+    if ( iRepr == GIA_VOID )
+        iRepr = i;
+    // collect nodes
+    Vec_IntClear( p->vClassOld );
+    Vec_IntClear( p->vClassNew );
+    Gia_ClassForEachObj( p->pAig, iRepr, Ent )
+    {
+        if ( Ent == i )
+            Vec_IntPush( p->vClassNew, Ent );
+        else
+            Vec_IntPush( p->vClassOld, Ent );
+    }
+    assert( Vec_IntSize( p->vClassNew ) == 1 );
+    Cec_ManSimClassCreate( p->pAig, p->vClassOld );
+    Cec_ManSimClassCreate( p->pAig, p->vClassNew );
+    assert( !Gia_ObjIsClass(p->pAig, i) );
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes hash key of the simuation info.]
 
   Description []
@@ -797,8 +839,12 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
     p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
     p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
     // set starting representative of internal nodes to be constant 0
-    Gia_ManForEachObj( p->pAig, pObj, i )
-        Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
+    if ( p->pPars->fLatchCorr )
+        Gia_ManForEachObj( p->pAig, pObj, i )
+            Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
+    else
+        Gia_ManForEachObj( p->pAig, pObj, i )
+            Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
     // if sequential simulation, set starting representative of ROs to be constant 0
     if ( p->pPars->fSeqSimulate )
         Gia_ManForEachRo( p->pAig, pObj, i )

src/aig/cec/cecCore.c

@@ -156,6 +156,56 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
+{
+    memset( p, 0, sizeof(Cec_ParCor_t) );
+    p->nWords         =      15;  // the number of simulation words
+    p->nRounds        =      15;  // the number of simulation rounds
+    p->nFrames        =       1;  // the number of time frames
+    p->nBTLimit       =     100;  // conflict limit at a node
+    p->fLatchCorr     =       0;  // consider only latch outputs
+    p->fUseRings      =       1;  // combine classes into rings
+    p->fUseCSat       =       1;  // use circuit-based solver
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fUseSmartCnf   =       0;  // use smart CNF computation
+    p->fVeryVerbose   =       0;  // verbose stats
+    p->fVerbose       =       0;  // verbose stats
+}  
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p )
+{
+    memset( p, 0, sizeof(Cec_ParChc_t) );
+    p->nWords         =      15;  // the number of simulation words
+    p->nRounds        =      15;  // the number of simulation rounds
+    p->nBTLimit       =    1000;  // conflict limit at a node
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fUseSmartCnf   =       0;  // use smart CNF computation
+    p->fVeryVerbose   =       0;  // verbose stats
+    p->fVerbose       =       0;  // verbose stats
+}  
+
+/**Function*************************************************************
+
   Synopsis    [Core procedure for SAT sweeping.]
 
   Description []
@@ -171,7 +221,8 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
     Cec_ManPat_t * pPat;
     pPat = Cec_ManPatStart();
     Cec_ManSatSolve( pPat, pAig, pPars );
-    pNew = Gia_ManDupDfsSkip( pAig );
+//    pNew = Gia_ManDupDfsSkip( pAig );
+    pNew = Gia_ManDup( pAig );
     Cec_ManPatStop( pPat );
     return pNew;
 }
@@ -193,7 +244,7 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
     int RetValue, clkTotal = clock();
     if ( pPars->fSeqSimulate )
         printf( "Performing sequential simulation of %d frames with %d words.\n", 
-            pPars->nWords, pPars->nRounds );
+            pPars->nRounds, pPars->nWords );
     Aig_ManRandom( 1 );
     pSim = Cec_ManSimStart( pAig, pPars );
     if ( pAig->pReprs == NULL )
@@ -286,7 +337,7 @@ p->timeSim += clock() - clk;
 //        Gia_WriteAiger( pSrm, "gia_srm.aig", 0, 0 );
 
         if ( pPars->fVeryVerbose )
-            Gia_ManPrintStats( pSrm );
+            Gia_ManPrintStats( pSrm, 0 );
         if ( Gia_ManCoNum(pSrm) == 0 )
         {
             Gia_ManStop( pSrm );

src/aig/cec/cecInt.h

@@ -85,15 +85,19 @@ struct Cec_ManSat_t_
     int              nRecycles;      // the number of times SAT solver was recycled
     int              nCallsSince;    // the number of calls since the last recycle
     Vec_Ptr_t *      vFanins;        // fanins of the CNF node
+    // counter-examples
+    Vec_Int_t *      vCex;           // the latest counter-example
+    Vec_Int_t *      vVisits;        // temporary array for visited nodes  
     // SAT calls statistics
     int              nSatUnsat;      // the number of proofs
     int              nSatSat;        // the number of failure
     int              nSatUndec;      // the number of timeouts
     int              nSatTotal;      // the number of calls
+    int              nCexLits;
     // conflicts
-    int              nConfUnsat;
-    int              nConfSat;
-    int              nConfUndec;
+    int              nConfUnsat;     // conflicts in unsat problems
+    int              nConfSat;       // conflicts in sat problems
+    int              nConfUndec;     // conflicts in undec problems
     // runtime stats
     int              timeSatUnsat;   // unsat
     int              timeSatSat;     // sat
@@ -164,6 +168,7 @@ struct Cec_ManFra_t_
 
 /*=== cecCore.c ============================================================*/
 /*=== cecClass.c ============================================================*/
+extern int                  Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
 extern int                  Cec_ManSimClassesPrepare( Cec_ManSim_t * p );
 extern int                  Cec_ManSimClassesRefine( Cec_ManSim_t * p );
 extern int                  Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos );
@@ -183,10 +188,16 @@ extern void                 Cec_ManFraStop( Cec_ManFra_t * p );
 /*=== cecPat.c ============================================================*/
 extern void                 Cec_ManPatSavePattern( Cec_ManPat_t *  pPat, Cec_ManSat_t *  p, Gia_Obj_t * pObj );
 extern Vec_Ptr_t *          Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nWords );
+extern Vec_Ptr_t *          Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit );
+/*=== cecSeq.c ============================================================*/
+extern int                  Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo );
+extern int                  Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState );
+extern void                 Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex );
 /*=== cecSolve.c ============================================================*/
 extern int                  Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
 extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
-extern void                 Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
+extern Vec_Str_t *          Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
+extern Vec_Int_t *          Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
 /*=== ceFraeep.c ============================================================*/
 extern Gia_Man_t *          Cec_ManFraSpecReduction( Cec_ManFra_t * p );
 extern int                  Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew );

src/aig/cec/cecMan.c

@@ -52,6 +52,8 @@ Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
     p->pSatVars     = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
     p->vUsedNodes   = Vec_PtrAlloc( 1000 );
     p->vFanins      = Vec_PtrAlloc( 100 );
+    p->vCex         = Vec_IntAlloc( 100 );
+    p->vVisits      = Vec_IntAlloc( 100 );
     return p;
 }
 
@@ -81,6 +83,7 @@ void Cec_ManSatPrintStats( Cec_ManSat_t * p )
     printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
         p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
     ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
+    ABC_PRT( "Total time", p->timeTotal );
 }
 
 /**Function*************************************************************
@@ -98,6 +101,8 @@ void Cec_ManSatStop( Cec_ManSat_t * p )
 {
     if ( p->pSat )
         sat_solver_delete( p->pSat );
+    Vec_IntFree( p->vCex );
+    Vec_IntFree( p->vVisits );
     Vec_PtrFree( p->vUsedNodes );
     Vec_PtrFree( p->vFanins );
     ABC_FREE( p->pSatVars );

src/aig/cec/cecPat.c

@@ -450,7 +450,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nW
     int nBits = 32 * nWords;
     int clk = clock();
     vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
-    Aig_ManRandomInfo( vInfo, 0, nWords );
+    Aig_ManRandomInfo( vInfo, 0, 0, nWords );
     vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
     Vec_PtrCleanSimInfo( vPres, 0, nWords );
     while ( pMan->iStart < Vec_StrSize(pMan->vStorage) )
@@ -464,7 +464,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nW
         if ( k == nBits-1 )
         {
             Vec_PtrReallocSimInfo( vInfo );
-            Aig_ManRandomInfo( vInfo, nWords, 2*nWords );
+            Aig_ManRandomInfo( vInfo, 0, nWords, 2*nWords );
             Vec_PtrReallocSimInfo( vPres );
             Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
             nWords *= 2;
@@ -486,6 +486,77 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nW
     return vInfo;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Packs patterns into array of simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit )
+{
+    Vec_Int_t * vPat;
+    Vec_Ptr_t * vInfo, * vPres;
+    int k, nSize, iStart, kMax = 0, nPatterns = 0;
+    int nWords = nWordsInit;
+    int nBits = 32 * nWords;
+//    int RetValue;
+    assert( nRegs <= nInputs );
+    vPat  = Vec_IntAlloc( 100 );
+
+    vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
+    Vec_PtrCleanSimInfo( vInfo, 0, nWords );
+    Aig_ManRandomInfo( vInfo, nRegs, 0, nWords );
+
+    vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
+    Vec_PtrCleanSimInfo( vPres, 0, nWords );
+    iStart = 0;
+    while ( iStart < Vec_IntSize(vCexStore) )
+    {
+        nPatterns++;
+        // skip the output number
+        iStart++;
+        // get the number of items
+        nSize = Vec_IntEntry( vCexStore, iStart++ );
+        if ( nSize <= 0 )
+            continue;
+        // extract pattern
+        Vec_IntClear( vPat );
+        for ( k = 0; k < nSize; k++ )
+            Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
+        // add pattern to storage
+        for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) )
+            if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
+                break;
+
+//        k = kMax + 1;
+//        RetValue = Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) );
+//        assert( RetValue == 1 );
+
+        kMax = AIG_MAX( kMax, k );
+        if ( k == nBits-1 )
+        {
+            Vec_PtrReallocSimInfo( vInfo );
+            Vec_PtrCleanSimInfo( vInfo, nWords, 2*nWords );
+            Aig_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords );
+
+            Vec_PtrReallocSimInfo( vPres );
+            Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
+            nWords *= 2;
+            nBits *= 2;
+        }
+    }
+//    printf( "packed %d patterns into %d vectors (out of %d)\n", nPatterns, kMax, nBits );
+    Vec_PtrFree( vPres );
+    Vec_IntFree( vPat );
+    return vInfo;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/cec/cecSeq.c

@@ -42,23 +42,32 @@
 void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex )
 {
     unsigned * pInfo;
-    int k, w, nWords;
+    int k, i, w, nWords;
     assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) );
-    assert( pCex->nBits <= Vec_PtrSize(vInfo) );
+    assert( pCex->nBits - pCex->nRegs + Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
     nWords = Vec_PtrReadWordsSimInfo( vInfo );
+/*
     for ( k = 0; k < pCex->nRegs; k++ )
     {
         pInfo = Vec_PtrEntry( vInfo, k );
         for ( w = 0; w < nWords; w++ )
             pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0;
     }
-    for ( ; k < pCex->nBits; k++ )
+*/
+    for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
     {
         pInfo = Vec_PtrEntry( vInfo, k );
         for ( w = 0; w < nWords; w++ )
+            pInfo[w] = 0;
+    }
+
+    for ( i = pCex->nRegs; i < pCex->nBits; i++ )
+    {
+        pInfo = Vec_PtrEntry( vInfo, k++ );
+        for ( w = 0; w < nWords; w++ )
             pInfo[w] = Aig_ManRandom(0);
         // set simulation pattern and make sure it is second (first will be erased during simulation)
-        pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, k ); 
+        pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, i ); 
         pInfo[0] <<= 1;
     }
     for ( ; k < Vec_PtrSize(vInfo); k++ )
@@ -85,13 +94,13 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce
     unsigned * pInfo;
     int k, w, nWords;
     nWords = Vec_PtrReadWordsSimInfo( vInfo );
-    assert( Gia_ManRegNum(pAig) == pCex->nRegs );
+    assert( pCex == NULL || Gia_ManRegNum(pAig) == pCex->nRegs );
     assert( Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
     for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
     {
         pInfo = Vec_PtrEntry( vInfo, k );
         for ( w = 0; w < nWords; w++ )
-            pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0;
+            pInfo[w] = (pCex && Aig_InfoHasBit(pCex->pData, k))? ~0 : 0;
     }
 
     for ( ; k < Vec_PtrSize(vInfo); k++ )
@@ -212,9 +221,10 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
         printf( "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" );
         return -1;
     }
-    if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis )
+//    if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis )
+    if ( Gia_ManPiNum(pAig) != pCex->nPis )
     {
-        printf( "Cec_ManSeqResimulateCounter(): Parameters of the ccounter-example differ.\n" );
+        printf( "Cec_ManSeqResimulateCounter(): The number of PIs in the AIG and the counter-example differ.\n" );
         return -1;
     }
     if ( pPars->fVerbose )
@@ -251,6 +261,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
     int nAddFrames = 10; // additional timeframes to simulate
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
     Vec_Ptr_t * vSimInfo; 
+    Vec_Str_t * vStatus;
     Gia_Cex_t * pState;
     Gia_Man_t * pSrm;
     int r, nPats, RetValue = -1;
@@ -284,13 +295,14 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
 //        Gia_ManPrintCounterExample( pState );
         // derive speculatively reduced model
         pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
-        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManPiNum(pAig) * pPars->nFrames );
+        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * pPars->nFrames) );
         // allocate room for simulation info
         vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
             Gia_ManPiNum(pAig) * (pPars->nFrames + nAddFrames), pPars->nWords );
         Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState );
         // fill in simulation info with counter-examples
-        Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
+        vStatus = Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
+        Vec_StrFree( vStatus );
         Gia_ManStop( pSrm );
         // resimulate and refine the classes
         RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState );

src/aig/cec/cecSolve.c

@@ -556,18 +556,10 @@ p->timeSatUndec += clock() - clk;
 ***********************************************************************/
 void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
 {
-    static int Counter;
-//    char Buffer[1000];
-
     Bar_Progress_t * pProgress = NULL;
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
     int i, status, clk = clock(), clk2;
-
-//    sprintf( Buffer, "gia%03d.aig", Counter++ );
-//Gia_WriteAiger( pAig, Buffer, 0, 0 );
-//printf( "Dumpted slice into file \"%s\".\n", Buffer );
-
     // reset the manager
     if ( pPat )
     {
@@ -595,13 +587,6 @@ clk2 = clock();
         pObj->fMark0 = (status == 0);
         pObj->fMark1 = (status == 1);
 /*
-printf( "Output %6d : ", i );
-printf( "conf = %6d ", p->pSat->stats.conflicts );
-printf( "prop = %6d ", p->pSat->stats.propagations );
-ABC_PRT( "time", clock() - clk2 );
-*/
-
-/*
         if ( status == -1 )
         {
             Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
@@ -653,6 +638,8 @@ void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pOb
         unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
         if ( Cec_ObjSatVarValue( pSat, pObj ) != Aig_InfoHasBit( pInfo, iPat ) )
             Aig_InfoXorBit( pInfo, iPat );
+        pSat->nCexLits++;
+//        Vec_IntPush( pSat->vCex, Gia_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) );
         return;
     }
     assert( Gia_ObjIsAnd(pObj) );
@@ -672,44 +659,207 @@ void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pOb
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats )
+Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats )
 {
     Bar_Progress_t * pProgress = NULL;
+    Vec_Str_t * vStatus;
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
-    int iPat = 1, nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
+    int iPat = 0, nPatsInit, nPats;
     int i, status, clk = clock();
+    nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
     Gia_ManSetPhase( pAig );
     Gia_ManLevelNum( pAig );
     Gia_ManResetTravId( pAig );
     p = Cec_ManSatCreate( pAig, pPars );
+    vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
     pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
     Gia_ManForEachCo( pAig, pObj, i )
     {
+        Bar_ProgressUpdate( pProgress, i, "SAT..." );
         if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+        {
+            if ( Gia_ObjFaninC0(pObj) )
+            {
+                printf( "Constant 1 output of SRM!!!\n" );
+                Vec_StrPush( vStatus, 0 );
+            }
+            else
+            {
+                printf( "Constant 0 output of SRM!!!\n" );
+                Vec_StrPush( vStatus, 1 );
+            }
             continue;
-        Bar_ProgressUpdate( pProgress, i, "BMC..." );
+        }
         status = Cec_ManSatCheckNode( p, pObj );
+//printf( "output %d   status = %d\n", i, status );
+        Vec_StrPush( vStatus, (char)status );
         if ( status != 0 )
             continue;
+        // resize storage
+        if ( iPat == nPats )
+        {
+            int nWords = Vec_PtrReadWordsSimInfo(vPatts);
+            Vec_PtrReallocSimInfo( vPatts );
+            Vec_PtrCleanSimInfo( vPatts, nWords, 2*nWords );
+            nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
+        }
+        if ( iPat % nPatsInit == 0 )
+            iPat++;
         // save the pattern
         Gia_ManIncrementTravId( pAig );
+//        Vec_IntClear( p->vCex );
         Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs );
-        if ( iPat == nPats )
-            break;
+//        Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
+//        Cec_ManSatAddToStore( p->vCexStore, p->vCex );
+//        if ( iPat == nPats )
+//            break;
         // quit if one of them is solved
-        if ( pPars->fFirstStop )
-            break;
+//        if ( pPars->fFirstStop )
+//            break;
+//        if ( iPat == 32 * 15 * 16 - 1 )
+//            break;
     }
     p->timeTotal = clock() - clk;
     Bar_ProgressStop( pProgress );
     if ( pPars->fVerbose )
         Cec_ManSatPrintStats( p );
+//    printf( "Total number of cex literals = %d. (Ave = %d)\n", p->nCexLits, p->nCexLits/p->nSatSat );
     Cec_ManSatStop( p );
     if ( pnPats )
         *pnPats = iPat-1;
+    return vStatus;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Save values in the cone of influence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out )
+{
+    int i, Entry;
+    Vec_IntPush( vCexStore, Out );
+    if ( vCex == NULL ) // timeout
+    {
+        Vec_IntPush( vCexStore, -1 );
+        return;
+    }
+    // write the counter-example
+    Vec_IntPush( vCexStore, Vec_IntSize(vCex) );
+    Vec_IntForEachEntry( vCex, Entry, i )
+        Vec_IntPush( vCexStore, Entry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Save values in the cone of influence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        pSat->nCexLits++;
+        Vec_IntPush( pSat->vCex, Gia_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Cec_ManSatSolveMiter_rec( pSat, p, Gia_ObjFanin0(pObj) );
+    Cec_ManSatSolveMiter_rec( pSat, p, Gia_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of solving for the POs of the AIG.]
+
+  Description [Labels the nodes that have been proved (pObj->fMark1) 
+  and returns the set of satisfying assignments.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Vec_Int_t * vCexStore;
+    Vec_Str_t * vStatus;
+    Cec_ManSat_t * p;
+    Gia_Obj_t * pObj;
+    int i, status, clk = clock();
+    // prepare AIG
+    Gia_ManSetPhase( pAig );
+    Gia_ManLevelNum( pAig );
+    Gia_ManResetTravId( pAig );
+    // create resulting data-structures
+    vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
+    vCexStore = Vec_IntAlloc( 10000 );
+    // perform solving
+    p = Cec_ManSatCreate( pAig, pPars );
+    pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
+    Gia_ManForEachCo( pAig, pObj, i )
+    {
+        Vec_IntClear( p->vCex );
+        Bar_ProgressUpdate( pProgress, i, "SAT..." );
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+        {
+            if ( Gia_ObjFaninC0(pObj) )
+            {
+                printf( "Constant 1 output of SRM!!!\n" );
+                Cec_ManSatAddToStore( vCexStore, p->vCex, i ); // trivial counter-example
+                Vec_StrPush( vStatus, 0 );
+            }
+            else
+            {
+                printf( "Constant 0 output of SRM!!!\n" );
+                Vec_StrPush( vStatus, 1 );
+            }
+            continue;
+        }
+        status = Cec_ManSatCheckNode( p, pObj );
+        Vec_StrPush( vStatus, (char)status );
+        if ( status == -1 )
+        {
+            Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
+            continue;
+        }
+        if ( status == 1 )
+            continue;
+        assert( status == 0 );
+        // save the pattern
+        Gia_ManIncrementTravId( pAig );
+        Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
+//        Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
+        Cec_ManSatAddToStore( vCexStore, p->vCex, i );
+    }
+    p->timeTotal = clock() - clk;
+    Bar_ProgressStop( pProgress );
+//    if ( pPars->fVerbose )
+//        Cec_ManSatPrintStats( p );
+    Cec_ManSatStop( p );
+    *pvStatus = vStatus;
+    return vCexStore;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/cec/module.make

 SRC +=    src/aig/cec/cecCec.c \
+    src/aig/cec/cecChoice.c \
     src/aig/cec/cecClass.c \
     src/aig/cec/cecCore.c \
+    src/aig/cec/cecCorr.c \
     src/aig/cec/cecIso.c \
     src/aig/cec/cecMan.c \
     src/aig/cec/cecPat.c \

src/aig/gia/gia.h

@@ -52,6 +52,15 @@ struct Gia_Rpr_t_
     unsigned       fColorB :  1;  // marks cone of B
 };
 
+typedef struct Gia_Plc_t_ Gia_Plc_t;
+struct Gia_Plc_t_
+{
+    unsigned       fFixed  :  1;  // the placement of this object is fixed
+    unsigned       xCoord  : 15;  // x-ooordinate of the placement
+    unsigned       fUndef  :  1;  // the placement of this object is not assigned
+    unsigned       yCoord  : 15;  // y-ooordinate of the placement
+};
+
 typedef struct Gia_Obj_t_ Gia_Obj_t;
 struct Gia_Obj_t_
 {
@@ -117,6 +126,8 @@ struct Gia_Man_t_
     Gia_Cex_t *    pCexComb;      // combinational counter-example
     int *          pCopies;       // intermediate copies
     Vec_Int_t *    vFlopClasses;  // classes of flops for retiming/merging/etc
+    unsigned char* pSwitching;    // switching activity for each object
+    Gia_Plc_t *    pPlacement;    // placement of the objects
 };
 
 
@@ -247,7 +258,7 @@ static inline int          Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t *
 static inline int          Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj));  }
 
 static inline Gia_Obj_t *  Gia_ObjFromLit( Gia_Man_t * p, int iLit )           { return Gia_NotCond( Gia_ManObj(p, Gia_Lit2Var(iLit)), Gia_LitIsCompl(iLit) );  }
-static inline int          Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Gia_Var2Lit( Gia_ObjId(p, pObj), Gia_IsComplement(pObj) );              }
+static inline int          Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Gia_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); }
 static inline int          Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit )      { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) );        }
 
 static inline int          Gia_ObjValue( Gia_Obj_t * pObj )                    { return pObj->Value;                                        }
@@ -375,8 +386,10 @@ static inline void        Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num )   { p
 static inline int         Gia_ObjIsConst( Gia_Man_t * p, int Id )            { return Gia_ObjRepr(p, Id) == 0;                                   }
 static inline int         Gia_ObjIsHead( Gia_Man_t * p, int Id )             { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0;  }
 static inline int         Gia_ObjIsNone( Gia_Man_t * p, int Id )             { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; }
-static inline int         Gia_ObjIsTail( Gia_Man_t * p, int Id )             { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0;          }
-static inline int         Gia_ObjIsClass( Gia_Man_t * p, int Id )            { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0;           }
+static inline int         Gia_ObjIsTail( Gia_Man_t * p, int Id )             { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0;                  }
+static inline int         Gia_ObjIsClass( Gia_Man_t * p, int Id )            { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0;                   }
+static inline int         Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k )  { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0;  }
+static inline int         Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k);                     }
 
 #define Gia_ManForEachConst( p, i )                            \
     for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else
@@ -419,6 +432,8 @@ static inline int *      Gia_ObjGateFanins( Gia_Man_t * p, int Id )         { re
     for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ )
 #define Gia_ManForEachCo( p, pObj, i )                                  \
     for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ManCo(p, i)); i++ )
+#define Gia_ManForEachCoReverse( p, pObj, i )                           \
+    for ( i = Vec_IntSize(p->vCos) - 1; (i >= 0) && ((pObj) = Gia_ManCo(p, i)); i-- )
 #define Gia_ManForEachCoDriver( p, pObj, i )                            \
     for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ObjFanin0(Gia_ManCo(p, i))); i++ )
 #define Gia_ManForEachPi( p, pObj, i )                                  \
@@ -443,7 +458,9 @@ extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p );
 /*=== giaAiger.c ===========================================================*/
 extern Gia_Man_t *         Gia_ReadAiger( char * pFileName, int fCheck );
 extern void                Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
+extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
 /*=== giaCsat.c ============================================================*/
+extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus );
 /*=== giaCof.c =============================================================*/
 extern void                Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
 extern Gia_Man_t *         Gia_ManDupCof( Gia_Man_t * p, int iVar );
@@ -455,6 +472,10 @@ extern void                Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int
 extern int                 Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes );
 extern int                 Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
 /*=== giaDup.c ============================================================*/
+extern Gia_Man_t *         Gia_ManDupOrderDfs( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManDupOrderAiger( Gia_Man_t * p );
+
 extern Gia_Man_t *         Gia_ManDup( Gia_Man_t * p );  
 extern Gia_Man_t *         Gia_ManDupSelf( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
@@ -508,19 +529,22 @@ extern int                 Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
 extern int                 Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 );
 extern int                 Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 );
 extern Gia_Man_t *         Gia_ManRehash( Gia_Man_t * p );
+extern void                Gia_ManHashProfile( Gia_Man_t * p );
 /*=== giaLogic.c ===========================================================*/
 extern void                Gia_ManTestDistance( Gia_Man_t * p );
 extern void                Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars );
  /*=== giaMan.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManStart( int nObjsMax ); 
 extern void                Gia_ManStop( Gia_Man_t * p );  
-extern void                Gia_ManPrintStats( Gia_Man_t * p ); 
+extern void                Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ); 
 extern void                Gia_ManPrintStatsShort( Gia_Man_t * p ); 
 extern void                Gia_ManPrintMiterStatus( Gia_Man_t * p ); 
 extern void                Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
 extern void                Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
 /*=== giaMap.c ===========================================================*/
 extern void                Gia_ManPrintMappingStats( Gia_Man_t * p );
+/*=== giaPat.c ===========================================================*/
+extern void                Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
 /*=== giaRetime.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose );
 /*=== giaSat.c ============================================================*/
@@ -535,6 +559,9 @@ extern Gia_Man_t *         Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int
 extern int *               Gia_SortFloats( float * pArray, int * pPerm, int nSize );
 /*=== giaSim.c ============================================================*/
 extern int                 Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
+/*=== giaSwitch.c ============================================================*/
+extern float               Gia_ManEvaluateSwitching( Gia_Man_t * p );
+extern float               Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
 /*=== giaTsim.c ============================================================*/
 extern Gia_Man_t *         Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose );
 /*=== giaUtil.c ===========================================================*/

src/aig/gia/giaAiger.c

@@ -194,6 +194,25 @@ int Gia_ReadInt( unsigned char * pPos )
 
 /**Function*************************************************************
 
+  Synopsis    [Reads decoded value.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Gia_ReadDiffValue( char ** ppPos, int iPrev )
+{
+    int Item = Gia_ReadAigerDecode( ppPos );
+    if ( Item & 1 )
+        return iPrev + (Item >> 1);
+    return iPrev - (Item >> 1);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Read equivalence classes from the string.]
 
   Description []
@@ -238,7 +257,7 @@ Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize )
 
 /**Function*************************************************************
 
-  Synopsis    [Reads decoded value.]
+  Synopsis    [Read flop classes from the string.]
 
   Description []
   
@@ -247,12 +266,13 @@ Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned Gia_ReadDiffValue( char ** ppPos, int iPrev )
+void Gia_ReadFlopClasses( unsigned char ** ppPos, Vec_Int_t * vClasses, int nSize )
 {
-    int Item = Gia_ReadAigerDecode( ppPos );
-    if ( Item & 1 )
-        return iPrev + (Item >> 1);
-    return iPrev - (Item >> 1);
+    int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4;
+    assert( nAlloc/4 == nSize );
+    assert( Vec_IntSize(vClasses) == nSize );
+    memcpy( Vec_IntArray(vClasses), *ppPos, 4*nSize );
+    *ppPos += 4 * nSize;
 }
 
 /**Function*************************************************************
@@ -290,6 +310,50 @@ int * Gia_ReadMapping( unsigned char ** ppPos, int nSize )
 
 /**Function*************************************************************
 
+  Synopsis    [Read switching from the string.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned char * Gia_ReadSwitching( unsigned char ** ppPos, int nSize )
+{
+    unsigned char * pSwitching;
+    int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4;
+    assert( nAlloc == nSize );
+    pSwitching = ABC_ALLOC( unsigned char, nSize );
+    memcpy( pSwitching, *ppPos, nSize );
+    *ppPos += nSize;
+    return pSwitching;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read placement from the string.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Plc_t * Gia_ReadPlacement( unsigned char ** ppPos, int nSize )
+{
+    Gia_Plc_t * pPlacement;
+    int nAlloc = Gia_ReadInt( *ppPos ); *ppPos += 4;
+    assert( nAlloc/4 == nSize );
+    pPlacement = ABC_ALLOC( Gia_Plc_t, nSize );
+    memcpy( pPlacement, *ppPos, 4*nSize );
+    *ppPos += 4 * nSize;
+    return pPlacement;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads the AIG in the binary AIGER format.]
 
   Description []
@@ -455,6 +519,13 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
             pNew->pReprs = Gia_ReadEquivClasses( &pCur, Gia_ManObjNum(pNew) );
             pNew->pNexts = Gia_ManDeriveNexts( pNew );
         }
+        if ( *pCur == 'f' )
+        {
+            pCur++;
+            // read flop classes
+            pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) );
+            Gia_ReadFlopClasses( &pCur, pNew->vFlopClasses, Gia_ManRegNum(pNew) );
+        }
         if ( *pCur == 'm' )
         {
             pCur++;
@@ -465,6 +536,13 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
         {
             pCur++;
             // read placement
+            pNew->pPlacement = Gia_ReadPlacement( &pCur, Gia_ManObjNum(pNew) );
+        }
+        if ( *pCur == 's' )
+        {
+            pCur++;
+            // read switching activity
+            pNew->pSwitching = Gia_ReadSwitching( &pCur, Gia_ManObjNum(pNew) );
         }
         if ( *pCur == 'n' )
         {
@@ -762,7 +840,10 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
 
     // create normalized AIG
     if ( !Gia_ManIsNormalized(pInit) )
+    {
+        printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" );
         p = Gia_ManDupNormalized( pInit );
+    }
     else
         p = pInit;
 
@@ -831,6 +912,15 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         fwrite( pEquivs, 1, nEquivSize, pFile );
         ABC_FREE( pEquivs );
     }
+    // write flop classes
+    if ( p->vFlopClasses )
+    {
+        char Buffer[10];
+        int nSize = 4*Gia_ManRegNum(p);
+        fprintf( pFile, "f" );
+        fwrite( Buffer, 1, 4, pFile );
+        fwrite( Vec_IntArray(p->vFlopClasses), 1, nSize, pFile );
+    }
     // write mapping
     if ( p->pMapping )
     {
@@ -841,6 +931,26 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         ABC_FREE( pMaps );
     }
     // write placement
+    if ( p->pPlacement )
+    {
+        char Buffer[10];
+        int nSize = 4*Gia_ManObjNum(p);
+        Gia_WriteInt( Buffer, nSize );
+        fprintf( pFile, "p" );
+        fwrite( Buffer, 1, 4, pFile );
+        fwrite( p->pPlacement, 1, nSize, pFile );
+    }
+    // write flop classes
+    if ( p->pSwitching )
+    {
+        char Buffer[10];
+        int nSize = Gia_ManObjNum(p);
+        Gia_WriteInt( Buffer, nSize );
+        fprintf( pFile, "s" );
+        fwrite( Buffer, 1, 4, pFile );
+        fwrite( p->pSwitching, 1, nSize, pFile );
+    }
+    // write name
     if ( p->pName )
         fprintf( pFile, "n%s%c", p->pName, '\0' );
     fprintf( pFile, "\nThis file was produced by the GIA package in ABC on %s\n", Gia_TimeStamp() );
@@ -850,6 +960,24 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         Gia_ManStop( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits )
+{
+    char Buffer[100];
+    sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum );
+    Gia_WriteAiger( p, Buffer, 0, 0 );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaCSat2.c → src/aig/gia/giaCSat.c

 /**CFile****************************************************************
 
-  FileName    [giaCSat2.c]
+  FileName    [giaCSat.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: giaCSat2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: giaCSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -48,10 +48,10 @@ struct Cbs_Que_t_
 {
     int           iHead;        // beginning of the queue
     int           iTail;        // end of the queue
-    int           nSize;        // allocated size
+   int           nSize;        // allocated size
     Gia_Obj_t **  pData;        // nodes stored in the queue
 };
-
+ 
 typedef struct Cbs_Man_t_ Cbs_Man_t;
 struct Cbs_Man_t_
 {
@@ -60,6 +60,20 @@ struct Cbs_Man_t_
     Cbs_Que_t     pProp;        // propagation queue
     Cbs_Que_t     pJust;        // justification queue
     Vec_Int_t *   vModel;       // satisfying assignment
+    // SAT calls statistics
+    int           nSatUnsat;    // the number of proofs
+    int           nSatSat;      // the number of failure
+    int           nSatUndec;    // the number of timeouts
+    int           nSatTotal;    // the number of calls
+    // conflicts
+    int           nConfUnsat;   // conflicts in unsat problems
+    int           nConfSat;     // conflicts in sat problems
+    int           nConfUndec;   // conflicts in undec problems
+    // runtime stats
+    int           timeSatUnsat; // unsat
+    int           timeSatSat;   // sat
+    int           timeSatUndec; // undecided
+    int           timeTotal;    // total runtime
 };
 
 static inline int   Cbs_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->fMark0;                        }
@@ -196,7 +210,8 @@ static inline void Cbs_ManSaveModel( Cbs_Man_t * p, Vec_Int_t * vCex )
     p->pProp.iHead = 0;
     Cbs_QueForEachEntry( p->pProp, pVar, i )
         if ( Gia_ObjIsCi(pVar) )
-            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
+//            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
+            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) );
 } 
 
 /**Function*************************************************************
@@ -714,7 +729,7 @@ void Cbs_ManSolveTest( Gia_Man_t * pGia )
             CountUndec++;
         else 
         {
-            int iLit, k;
+//            int iLit, k;
             vCex = Cbs_ReadModel( p );
 
 //        printf( "complemented = %d.  ", Gia_ObjFaninC0(pRoot) );
@@ -738,6 +753,132 @@ void Cbs_ManSolveTest( Gia_Man_t * pGia )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Prints statistics of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cbs_ManSatPrintStats( Cbs_Man_t * p )
+{
+    printf( "CO = %6d  ", Gia_ManCoNum(p->pAig) );
+    printf( "Conf = %5d  ", p->Pars.nBTLimit );
+    printf( "JustMax = %5d  ", p->Pars.nJustLimit );
+    printf( "\n" );
+    printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
+        p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
+    ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
+    printf( "Sat   calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
+        p->nSatSat,   100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
+    ABC_PRTP( "Time", p->timeSatSat,   p->timeTotal );
+    printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
+        p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
+    ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
+    ABC_PRT( "Total time", p->timeTotal );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure to test the new SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus )
+{
+    extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
+    Cbs_Man_t * p; 
+    Vec_Int_t * vCex, * vVisit, * vCexStore;
+    Vec_Str_t * vStatus;
+    Gia_Obj_t * pRoot; 
+    int i, status, clk, clkTotal = clock();
+    assert( Gia_ManRegNum(pAig) == 0 );
+    // prepare AIG
+    Gia_ManCreateRefs( pAig );
+    Gia_ManCleanMark0( pAig );
+    Gia_ManCleanMark1( pAig );
+    // create logic network
+    p = Cbs_ManAlloc();
+    p->Pars.nBTLimit = nConfs;
+    p->pAig   = pAig;
+    // create resulting data-structures
+    vStatus   = Vec_StrAlloc( Gia_ManPoNum(pAig) );
+    vCexStore = Vec_IntAlloc( 10000 );
+    vVisit    = Vec_IntAlloc( 100 );
+    vCex      = Cbs_ReadModel( p );
+    // solve for each output
+    Gia_ManForEachCo( pAig, pRoot, i )
+    {
+        Vec_IntClear( vCex );
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
+        {
+            if ( Gia_ObjFaninC0(pRoot) )
+            {
+                printf( "Constant 1 output of SRM!!!\n" );
+                Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
+                Vec_StrPush( vStatus, 0 );
+            }
+            else
+            {
+                printf( "Constant 0 output of SRM!!!\n" );
+                Vec_StrPush( vStatus, 1 );
+            }
+            continue;
+        }
+        clk = clock();
+        p->Pars.fUseHighest = 1;
+        p->Pars.fUseLowest  = 0;
+        status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
+        if ( status == -1 )
+        {
+            p->Pars.fUseHighest = 0;
+            p->Pars.fUseLowest  = 1;
+            status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
+        }
+        Vec_StrPush( vStatus, (char)status );
+        if ( status == -1 )
+        {
+            p->nSatUndec++;
+            p->nConfUndec += p->Pars.nBTThis;
+            Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
+            p->timeSatUndec += clock() - clk;
+            continue;
+        }
+        if ( status == 1 )
+        {
+            p->nSatUnsat++;
+            p->nConfUnsat += p->Pars.nBTThis;
+            p->timeSatUnsat += clock() - clk;
+            continue;
+        }
+        p->nSatSat++;
+        p->nConfUnsat += p->Pars.nBTThis;
+//        Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
+        Cec_ManSatAddToStore( vCexStore, vCex, i );
+        p->timeSatSat += clock() - clk;
+    }
+    Vec_IntFree( vVisit );
+    p->nSatTotal = Gia_ManPoNum(pAig);
+    p->timeTotal = clock() - clkTotal;
+//    Cbs_ManSatPrintStats( p );
+    Cbs_ManStop( p );
+    *pvStatus = vStatus;
+//    printf( "Total number of cex literals = %d. (Ave = %d)\n", 
+//         Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat, 
+//        (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
+    return vCexStore;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaCSatA.c

-/**CFile****************************************************************
-
-  FileName    [giaSolver.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Scalable AIG package.]
-
-  Synopsis    [Circuit-based SAT solver.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: giaSolver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "gia.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Sat_Cla_t_ Sat_Cla_t;
-struct Sat_Cla_t_
-{
-    unsigned       hWatch0;          // watched list for 0 literal
-    unsigned       hWatch1;          // watched list for 1 literal
-    int            Activity;         // activity of the clause
-    int            nLits;            // the number of literals
-    int            pLits[0];         // the array of literals  
-};
-
-typedef struct Sat_Fan_t_ Sat_Fan_t;
-struct Sat_Fan_t_
-{
-    unsigned       iFan      : 31;   // ID of the fanin/fanout
-    unsigned       fCompl    :  1;   // complemented attribute
-};
-
-typedef struct Sat_Obj_t_ Sat_Obj_t;
-struct Sat_Obj_t_
-{
-    unsigned       hHandle;          // node handle
-    unsigned       fAssign   :  1;   // terminal node (CI/CO)
-    unsigned       fValue    :  1;   // value under 000 pattern
-    unsigned       fMark0    :  1;   // first user-controlled mark
-    unsigned       fMark1    :  1;   // second user-controlled mark
-    unsigned       nFanouuts : 28;   // the number of fanouts
-    unsigned       nFanins   :  8;   // the number of fanins
-    unsigned       Level     : 24;   // logic level
-    unsigned       hNext;            // next one on this level 
-    unsigned       hWatch0;          // watched list for 0 literal
-    unsigned       hWatch1;          // watched list for 1 literal
-    unsigned       hReason;          // reason for this variable
-    unsigned       Depth;            // decision depth
-    Sat_Fan_t      Fanios[0];        // the array of fanins/fanouts
-};
-
-typedef struct Sat_Man_t_ Sat_Man_t;
-struct Sat_Man_t_
-{
-    Gia_Man_t *    pGia;             // the original AIG manager
-    // circuit
-    Vec_Int_t      vCis;             // the vector of CIs (PIs + LOs)
-    Vec_Int_t      vObjs;            // the vector of objects
-    // learned clauses         
-    Vec_Int_t      vClauses;         // the vector of clauses
-    // solver data
-    Vec_Int_t      vTrail;           // variable queue               
-    Vec_Int_t      vTrailLim;        // pointer into the trail               
-    int            iHead;            // variable queue 
-    int            iTail;            // variable queue
-    int            iRootLevel;       // first decision
-    // levelized order
-    int            iLevelTop;        // the largest unassigned level 
-    Vec_Int_t      vLevels;          // the linked lists of levels
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-

src/aig/gia/giaCof.c

@@ -859,7 +859,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
     if ( fVerbose )
     { 
         printf( "Cofactoring %d signals.\n", Vec_IntSize(vSigs) );
-        Gia_ManPrintStats( p );
+        Gia_ManPrintStats( p, 0 );
     }
     if ( Vec_IntSize( vSigs ) > 200 )
     {
@@ -885,7 +885,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
         if ( fVerbose )
             printf( "Cofactored variable %d.\n", iVar );
         if ( fVerbose )
-            Gia_ManPrintStats( pAig );
+            Gia_ManPrintStats( pAig, 0 );
     }
     Vec_IntFree( vSigsNew );
     return pAig;

src/aig/gia/giaDup.c

@@ -30,6 +30,226 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Removes pointers to the unmarked nodes..]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupRemapEquiv( Gia_Man_t * pNew, Gia_Man_t * p )
+{
+    Vec_Int_t * vClass;
+    int i, k, iNode, iRepr, iPrev;
+    if ( p->pReprs == NULL )
+        return;
+    assert( pNew->pReprs == NULL && pNew->pNexts == NULL );
+    // start representatives
+    pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
+    for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
+        Gia_ObjSetRepr( pNew, i, GIA_VOID );
+    // iterate over constant candidates
+    Gia_ManForEachConst( p, i )
+        Gia_ObjSetRepr( pNew, Gia_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
+    // iterate over class candidates
+    vClass = Vec_IntAlloc( 100 );
+    Gia_ManForEachClass( p, i )
+    {
+        Vec_IntClear( vClass );
+        Gia_ClassForEachObj( p, i, k )
+            Vec_IntPushUnique( vClass, Gia_Lit2Var(Gia_ManObj(p, k)->Value) );
+        assert( Vec_IntSize( vClass ) > 1 );
+        Vec_IntSort( vClass, 0 );
+        iRepr = iPrev = Vec_IntEntry( vClass, 0 );
+        Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
+        {
+            Gia_ObjSetRepr( pNew, iNode, iRepr );
+            assert( iPrev < iNode );
+            iPrev = iNode;
+        }
+    }
+    Vec_IntFree( vClass );
+    pNew->pNexts = Gia_ManDeriveNexts( pNew );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps combinational inputs when objects are DFS ordered.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupRemapCis( Gia_Man_t * pNew, Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj, * pObjNew;
+    int i;
+    assert( Vec_IntSize(p->vCis) == Vec_IntSize(pNew->vCis) );
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        assert( Gia_ObjCioId(pObj) == i );
+        pObjNew = Gia_ObjFromLit( pNew, pObj->Value );
+        assert( !Gia_IsComplement(pObjNew) );
+        Vec_IntWriteEntry( pNew->vCis, i, Gia_ObjId(pNew, pObjNew) );
+        Gia_ObjSetCioId( pObjNew, i );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps combinational outputs when objects are DFS ordered.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupRemapCos( Gia_Man_t * pNew, Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj, * pObjNew;
+    int i;
+    assert( Vec_IntSize(p->vCos) == Vec_IntSize(pNew->vCos) );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        assert( Gia_ObjCioId(pObj) == i );
+        pObjNew = Gia_ObjFromLit( pNew, pObj->Value );
+        assert( !Gia_IsComplement(pObjNew) );
+        Vec_IntWriteEntry( pNew->vCos, i, Gia_ObjId(pNew, pObjNew) );
+        Gia_ObjSetCioId( pObjNew, i );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManDupOrderDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return pObj->Value;
+    if ( Gia_ObjIsCi(pObj) )
+        return pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    if ( Gia_ObjIsCo(pObj) )
+        return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while putting objects in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManDupOrderDfs_rec( pNew, p, pObj );
+    Gia_ManForEachCi( p, pObj, i )
+        if ( !~pObj->Value )
+            pObj->Value = Gia_ManAppendCi(pNew);
+    assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
+    Gia_ManDupRemapCis( pNew, p );
+    Gia_ManDupRemapEquiv( pNew, p );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while putting objects in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCoReverse( p, pObj, i )
+        Gia_ManDupOrderDfs_rec( pNew, p, pObj );
+    Gia_ManForEachCi( p, pObj, i )
+        if ( !~pObj->Value )
+            pObj->Value = Gia_ManAppendCi(pNew);
+    assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
+    Gia_ManDupRemapCis( pNew, p );
+    Gia_ManDupRemapCos( pNew, p );
+    Gia_ManDupRemapEquiv( pNew, p );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while putting first PIs, then nodes, then POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManDupRemapEquiv( pNew, p );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    assert( Gia_ManIsNormalized(pNew) );
+    return pNew;
+}
+
+
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates AIG without any changes.]
 
   Description []
@@ -296,7 +516,7 @@ int Gia_ManDupDfs2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
     if ( pNew->pHTable )
         return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-}
+} 
 
 /**Function*************************************************************
 

src/aig/gia/giaEmbed.c

@@ -36,6 +36,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define GIA_PLACE_SIZE 0x7fff 
+// objects will be placed in box [0, GIA_PLACE_SIZE] x [0, GIA_PLACE_SIZE]
 
 typedef float  Emb_Dat_t;
 
@@ -247,6 +249,7 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
         Emb_ObjAddFanin( Emb_ManObj(p,Gia_ObjValue(pObjRo)), Emb_ManObj(p,Gia_ObjValue(pObjRi)) );
     assert( nNodes  == Emb_ManNodeNum(p) );
     assert( hHandle == p->nObjData );
+    assert( p->nObjs == Gia_ManObjNum(pGia) );
     if ( hHandle != p->nObjData )
         printf( "Emb_ManStartSimple(): Fatal error in internal representation.\n" );
     // make sure the fanin/fanout counters are correct
@@ -1407,7 +1410,7 @@ void Emb_ManComputeSolutions( Emb_Man_t * p, int nDims, int nSols )
 
 /**Function*************************************************************
 
-  Synopsis    [Projects into square of size [0;0xffff] x [0;0xffff].]
+  Synopsis    [Projects into square of size [0;GIA_PLACE_SIZE] x [0;GIA_PLACE_SIZE].]
 
   Description []
                
@@ -1432,7 +1435,7 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
         Min0 = ABC_MIN( Min0, pY0[k] );
         Max0 = ABC_MAX( Max0, pY0[k] );
     }
-    Str0 = 1.0*0xffff/(Max0 - Min0);
+    Str0 = 1.0*GIA_PLACE_SIZE/(Max0 - Min0);
     // update the coordinates
     for ( k = 0; k < p->nObjs; k++ )
         pY0[k] = (pY0[k] != 0.0) ? ((pY0[k] - Min0) * Str0) : 0.0;
@@ -1446,7 +1449,7 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
         Min1 = ABC_MIN( Min1, pY1[k] );
         Max1 = ABC_MAX( Max1, pY1[k] );
     }
-    Str1 = 1.0*0xffff/(Max1 - Min1);
+    Str1 = 1.0*GIA_PLACE_SIZE/(Max1 - Min1);
     // update the coordinates
     for ( k = 0; k < p->nObjs; k++ )
         pY1[k] = (pY1[k] != 0.0) ? ((pY1[k] - Min1) * Str1) : 0.0;
@@ -1455,12 +1458,12 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
     pPerm0 = Gia_SortFloats( pY0, NULL, p->nObjs );
     pPerm1 = Gia_SortFloats( pY1, NULL, p->nObjs );
 
-    // average solutions and project them into square [0;0xffff] x [0;0xffff]
+    // average solutions and project them into square [0;GIA_PLACE_SIZE] x [0;GIA_PLACE_SIZE]
     p->pPlacement = ABC_ALLOC( unsigned short, 2 * p->nObjs );
     for ( k = 0; k < p->nObjs; k++ )
     {
-        p->pPlacement[2*pPerm0[k]+0] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
-        p->pPlacement[2*pPerm1[k]+1] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
+        p->pPlacement[2*pPerm0[k]+0] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs);
+        p->pPlacement[2*pPerm1[k]+1] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs);
     }
     ABC_FREE( pPerm0 );
     ABC_FREE( pPerm1 );
@@ -1568,8 +1571,8 @@ void Emb_ManPlacementRefine( Emb_Man_t * p, int nIters, int fVerbose )
         pPermY = Gia_SortFloats( pVertY, NULL, p->nObjs );
         for ( k = 0; k < p->nObjs; k++ )
         {
-            p->pPlacement[2*pPermX[k]+0] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
-            p->pPlacement[2*pPermY[k]+1] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
+            p->pPlacement[2*pPermX[k]+0] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs);
+            p->pPlacement[2*pPermY[k]+1] = (unsigned short)(int)(1.0 * k * GIA_PLACE_SIZE / p->nObjs);
         }
         ABC_FREE( pPermX );
         ABC_FREE( pPermY );
@@ -1783,7 +1786,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI
 void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars )
 {
     Emb_Man_t * p;
-    int clk, clkSetup;
+    int i, clk, clkSetup;
 //   Gia_ManTestDistance( pGia );
 
     // transform AIG into internal data-structure
@@ -1843,6 +1846,17 @@ if ( pPars->fVerbose )
 ABC_PRT( "Image dump", clock() - clk );
     }
 
+    // transfer placement
+    if ( Gia_ManObjNum(pGia) == p->nObjs )
+    {
+        // assuming normalized ordering of the AIG
+        pGia->pPlacement = ABC_CALLOC( Gia_Plc_t, p->nObjs );
+        for ( i = 0; i < p->nObjs; i++ ) 
+        {
+            pGia->pPlacement[i].xCoord = p->pPlacement[2*i+0];
+            pGia->pPlacement[i].yCoord = p->pPlacement[2*i+1];
+        }
+    }
     Emb_ManStop( p );
 }
 

src/aig/gia/giaEquiv.c

@@ -226,6 +226,10 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
     assert( Gia_ManEquivCheckLits( p, nLits ) );
     if ( fVerbose )
     {
+        printf( "Const0 = " );
+        Gia_ManForEachConst( p, i )
+            printf( "%d ", i );
+        printf( "\n" );
         Counter = 0;
         Gia_ManForEachClass( p, i )
             Gia_ManEquivPrintOne( p, i, ++Counter );
@@ -275,15 +279,15 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int
 void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
 {
     Gia_Obj_t * pRepr;
-    if ( ~pObj->Value )
-        return;
-    assert( Gia_ObjIsAnd(pObj) );
     if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
     {
         Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut );
         pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
         return;
     }
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
     Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
     Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll, fDualOut );
     pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -303,18 +307,25 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
 Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose )
 {
     Gia_Man_t * pNew;
-    Gia_Obj_t * pObj, * pRepr;
+    Gia_Obj_t * pObj;
     int i;
+    if ( !p->pReprs )
+    {
+        printf( "Gia_ManEquivReduce(): Equivalence classes are not available.\n" );
+        return NULL;
+    }
     if ( fDualOut && (Gia_ManPoNum(p) & 1) )
     {
         printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
+/*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
         printf( "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" );
         return NULL;
     }
+*/
     Gia_ManSetPhase( p );
     if ( fDualOut )
         Gia_ManEquivSetColors( p, fVerbose );
@@ -323,11 +334,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
-    {
         pObj->Value = Gia_ManAppendCi(pNew);
-        if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
-            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
-    }
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
@@ -662,11 +669,13 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
         printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
+/*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
         printf( "Gia_ManSpecReduce(): AIG is not in a correct topological order.\n" );
         return NULL;
     }
+*/
     vXorLits = Vec_IntAlloc( 1000 );
     Gia_ManSetPhase( p );
     Gia_ManFillValue( p );
@@ -786,11 +795,13 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
         printf( "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
+/*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
         printf( "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" );
         return NULL;
     }
+*/
     assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 );
     p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
     vXorLits = Vec_IntAlloc( 1000 );

src/aig/gia/giaHash.c

@@ -86,7 +86,7 @@ static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1 )
 void Gia_ManHashAlloc( Gia_Man_t * p )  
 {
     assert( p->pHTable == NULL );
-    p->nHTable = Aig_PrimeCudd( p->nObjsAlloc / 3 );
+    p->nHTable = Aig_PrimeCudd( p->nObjsAlloc );
     p->pHTable = ABC_CALLOC( int, p->nHTable );
 }
 
@@ -174,6 +174,34 @@ void Gia_ManHashResize( Gia_Man_t * p )
     ABC_FREE( pHTableOld );
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Profiles the hash table.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Gia_ManHashProfile( Gia_Man_t * p )
+{
+    Gia_Obj_t * pEntry;
+    int i, Counter;
+    printf( "Table size = %d. Entries = %d.\n", p->nHTable, Gia_ManAndNum(p) );
+    for ( i = 0; i < p->nHTable; i++ )
+    {
+        Counter = 0;
+        for ( pEntry = (p->pHTable[i]? Gia_ManObj(p, Gia_Lit2Var(p->pHTable[i])) : NULL); 
+              pEntry; 
+              pEntry = (pEntry->Value? Gia_ManObj(p, Gia_Lit2Var(pEntry->Value)) : NULL) )
+            Counter++;
+        if ( Counter ) 
+            printf( "%d ", Counter );
+    }
+    printf( "\n" );
+}
 
 /**Function*************************************************************
 

src/aig/gia/giaMan.c

@@ -70,6 +70,8 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFree( p->vFlopClasses );
     Vec_IntFree( p->vCis );
     Vec_IntFree( p->vCos );
+    ABC_FREE( p->pPlacement );
+    ABC_FREE( p->pSwitching );
     ABC_FREE( p->pCexComb );
     ABC_FREE( p->pIso );
     ABC_FREE( p->pMapping );
@@ -128,17 +130,48 @@ void Gia_ManPrintClasses( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManPrintStats( Gia_Man_t * p )
+void Gia_ManPrintPlacement( Gia_Man_t * p )
+{
+    int i, nFixed = 0, nUndef = 0;
+    if ( p->pPlacement == NULL )
+        return;
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+    {
+        nFixed += p->pPlacement[i].fFixed;
+        nUndef += p->pPlacement[i].fUndef;
+    }
+    printf( "Placement:  Objects = %8d.  Fixed = %8d.  Undef = %8d.\n", Gia_ManObjNum(p), nFixed, nUndef );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats for the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
 {
     if ( p->pName )
         printf( "%8s : ", p->pName );
-    printf( "i/o =%7d/%7d  ", Gia_ManPiNum(p), Gia_ManPoNum(p) );
+    printf( "i/o =%7d/%7d", Gia_ManPiNum(p), Gia_ManPoNum(p) );
     if ( Gia_ManRegNum(p) )
-        printf( "ff =%7d  ", Gia_ManRegNum(p) );
-    printf( "and =%8d  ", Gia_ManAndNum(p) );
-    printf( "lev =%5d  ", Gia_ManLevelNum(p) );
-    printf( "cut =%5d  ", Gia_ManCrossCut(p) );
-    printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
+        printf( "  ff =%7d", Gia_ManRegNum(p) );
+    printf( "  and =%8d", Gia_ManAndNum(p) );
+    printf( "  lev =%5d", Gia_ManLevelNum(p) );
+    printf( "  cut =%5d", Gia_ManCrossCut(p) );
+    printf( "  mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
+    if ( fSwitch )
+    {
+        if ( p->pSwitching )
+            printf( "  power =%7.2f", Gia_ManEvaluateSwitching(p) );
+        else
+            printf( "  power =%7.2f", Gia_ManComputeSwitching(p, 48, 16, 0) );
+    }
 //    printf( "obj =%5d  ", Gia_ManObjNum(p) );
     printf( "\n" );
 
@@ -147,6 +180,8 @@ void Gia_ManPrintStats( Gia_Man_t * p )
         Gia_ManEquivPrintClasses( p, 0, 0.0 );
     if ( p->pMapping )
         Gia_ManPrintMappingStats( p );
+    if ( p->pPlacement )
+        Gia_ManPrintPlacement( p );
     // print register classes
 //    Gia_ManPrintClasses( p );
 }

src/aig/gia/giaCSat0.c → src/aig/gia/giaPat.c

 /**CFile****************************************************************
 
-  FileName    [giaCsat0.c]
+  FileName    [gia.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [Scalable AIG package.]
 
-  Synopsis    [Circuit-based SAT solver.]
+  Synopsis    []
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: giaCsat0.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -24,14 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int          Sat_ObjXValue( Gia_Obj_t * pObj )          { return (pObj->fMark1 << 1) | pObj->fMark0; }
-static inline void         Sat_ObjSetXValue( Gia_Obj_t * pObj, int v) { pObj->fMark0 = (v & 1); pObj->fMark1 = ((v >> 1) & 1); }
-
-static inline int          Sat_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->Value > 0;                    }
-static inline void         Sat_VarAssign( Gia_Obj_t * pVar, int i )   { assert(!pVar->Value); pVar->Value = i;     }
-static inline void         Sat_VarUnassign( Gia_Obj_t * pVar )        { assert(pVar->Value);  pVar->Value = 0;     }
-static inline int          Sat_VarValue( Gia_Obj_t * pVar )           { assert(pVar->Value);  return pVar->fMark0; }
-static inline void         Sat_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->Value);  pVar->fMark0 = v;    }
+static inline int   Sat_ObjXValue( Gia_Obj_t * pObj )          { return (pObj->fMark1 << 1) | pObj->fMark0;             }
+static inline void  Sat_ObjSetXValue( Gia_Obj_t * pObj, int v) { pObj->fMark0 = (v & 1); pObj->fMark1 = ((v >> 1) & 1); }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -52,7 +46,6 @@ void Gia_SatCollectCone_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisit
 {
     if ( Sat_ObjXValue(pObj) == GIA_UND )
         return;
-    assert( pObj->Value == 0 );
     if ( Gia_ObjIsAnd(pObj) )
     {
         Gia_SatCollectCone_rec( p, Gia_ObjFanin0(pObj), vVisit );
@@ -85,9 +78,9 @@ void Gia_SatCollectCone( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisit )
 
 /**Function*************************************************************
 
-  Synopsis    [Collects nodes in the cone.]
+  Synopsis    [Checks if the counter-examples asserts the output.]
 
-  Description []
+  Description [Assumes that fMark0 and fMark1 are clean. Leaves them clean.]
                
   SideEffects []
 
@@ -104,11 +97,8 @@ void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, V
     Gia_SatCollectCone( p, Gia_ObjFanin0(pRoot), vVisit );
     // set binary values to nodes in the counter-example
     Vec_IntForEachEntry( vCex, Entry, i )
-    {
-        pObj = Gia_NotCond( Gia_ManObj( p, Gia_Lit2Var(Entry) ), Gia_LitIsCompl(Entry) );
-        Sat_ObjSetXValue( Gia_Regular(pObj), Gia_IsComplement(pObj)? GIA_ZER : GIA_ONE );
-        assert( Sat_ObjXValue(Gia_Regular(pObj)) == (Gia_IsComplement(pObj)? GIA_ZER : GIA_ONE) );
-    }
+//        Sat_ObjSetXValue( Gia_ManObj(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
+        Sat_ObjSetXValue( Gia_ManCi(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
     // simulate
     Gia_ManForEachObjVec( vVisit, p, pObj, i )
     {
@@ -132,195 +122,6 @@ void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, V
 }
 
 
-/**Function*************************************************************
-
-  Synopsis    [Undoes the assignment since the given value.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_SatUndo_rec( Gia_Obj_t * pObj, unsigned Value, Vec_Int_t * vCex )
-{
-    if ( pObj->Value < Value )
-        return;
-    pObj->Value = 0;
-    if ( Gia_ObjIsCi(pObj) )
-    {
-        if ( vCex ) Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pObj), !pObj->fPhase) );
-        return;
-    }
-    Gia_SatUndo_rec( Gia_ObjFanin0(pObj), Value, vCex );
-    Gia_SatUndo_rec( Gia_ObjFanin1(pObj), Value, vCex );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Propagates assignments.]
-
-  Description [Returns 1 if UNSAT, 0 if SAT.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_SatProp_rec( Gia_Obj_t * pObj, unsigned Phase, unsigned * pValue, int * pnConfs )
-{
-    int Value = *pValue;
-    if ( pObj->Value )
-        return pObj->fPhase != Phase;
-    if ( Gia_ObjIsCi(pObj) )
-    {
-        pObj->Value = Value;
-        pObj->fPhase = Phase;
-        return 0;
-    }
-    if ( Phase ) // output of AND should be 1
-    {
-        if ( Gia_SatProp_rec( Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), pValue, pnConfs ) )
-            return 1;
-        if ( Gia_SatProp_rec( Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), pValue, pnConfs ) )
-        {
-            Gia_SatUndo_rec( Gia_ObjFanin0(pObj), Value, NULL );
-            return 1;
-        }
-/*
-        if ( Gia_SatProp_rec( Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), pValue, pnConfs ) )
-            return 1;
-        if ( Gia_SatProp_rec( Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), pValue, pnConfs ) )
-        {
-            Gia_SatUndo_rec( Gia_ObjFanin1(pObj), Value, NULL );
-            return 1;
-        }
-*/
-        pObj->Value = Value;
-        pObj->fPhase = 1;
-        return 0; 
-    }
-    // output of AND should be 0
-
-    (*pValue)++;
-    if ( !Gia_SatProp_rec( Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj), pValue, pnConfs ) )
-    {
-        pObj->Value = Value;
-        pObj->fPhase = 0;
-        return 0;
-    }
-    if ( !*pnConfs )
-        return 1;
-
-    (*pValue)++;
-    if ( !Gia_SatProp_rec( Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj), pValue, pnConfs ) )
-    {
-        pObj->Value = Value;
-        pObj->fPhase = 0;
-        return 0;
-    }
-    if ( !*pnConfs )
-        return 1;
-    // cannot be satisfied
-    (*pnConfs)--;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Procedure to solve SAT for the node.]
-
-  Description [Returns 1 if UNSAT, 0 if SAT, and -1 if undecided.]
-               
-  SideEffects [Precondition: pObj->Value should be 0.]
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_SatSolve( Gia_Obj_t * pObj, unsigned Phase, int nConfsMax, Vec_Int_t * vCex )
-{
-    int Value = 1;
-    int nConfs = nConfsMax? nConfsMax : (1<<30);
-    assert( !Gia_IsComplement(pObj) );
-    assert( !Gia_ObjIsConst0(pObj) );
-    assert( pObj->Value == 0 );
-    if ( Gia_SatProp_rec( pObj, Phase, &Value, &nConfs ) )
-    {
-//        if ( nConfs )
-//            printf( "UNSAT after %d conflicts\n", nConfsMax - nConfs );
-//        else
-//            printf( "UNDEC after %d conflicts\n", nConfsMax );
-        return nConfs? 1 : -1;
-    }
-    Vec_IntClear( vCex );
-    Gia_SatUndo_rec( pObj, 1, vCex );
-//    printf( "SAT after %d conflicts\n", nConfsMax - nConfs );
-    return 0;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Procedure to test the new SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_SatSolveTest( Gia_Man_t * p )
-{
-    int nConfsMax = 1000;
-    int CountUnsat, CountSat, CountUndec;
-    Vec_Int_t * vCex;
-    Vec_Int_t * vVisit;
-    Gia_Obj_t * pRoot; 
-    int i, RetValue, clk = clock();
-    // prepare AIG
-    Gia_ManCleanValue( p );
-    Gia_ManCleanMark0( p );
-    Gia_ManCleanMark1( p );
-    vCex   = Vec_IntAlloc( 100 );
-    vVisit = Vec_IntAlloc( 100 );
-    // solve for each output
-    CountUnsat = CountSat = CountUndec = 0;
-    Gia_ManForEachCo( p, pRoot, i )
-    {
-        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
-            continue;
-//printf( "Output %6d : ", i );
-        RetValue = Gia_SatSolve( Gia_ObjFanin0(pRoot), !Gia_ObjFaninC0(pRoot), nConfsMax, vCex );
-        if ( RetValue == 1 )
-            CountUnsat++;
-        else if ( RetValue == -1 )
-            CountUndec++;
-        else 
-        {
-//            Gia_Obj_t * pTemp;
-//            int k;
-            assert( RetValue == 0 );
-            CountSat++;
-/*
-            Vec_IntForEachEntry( vCex, pTemp, k )
-//                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjCioId(Gia_Regular(pTemp)) );
-                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjId(p,Gia_Regular(pTemp)) );
-            printf( "\n" );
-*/
-//            Gia_SatVerifyPattern( p, pRoot, vCex, vVisit );
-        }
-//        Gia_ManCheckMark0( p );
-//        Gia_ManCheckMark1( p );
-    }
-    Vec_IntFree( vCex );
-    Vec_IntFree( vVisit );
-    printf( "Unsat = %d. Sat = %d. Undec = %d.  ", CountUnsat, CountSat, CountUndec );
-    ABC_PRT( "Time", clock() - clk );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaSwitch.c

@@ -73,13 +73,13 @@ static inline unsigned * Gia_SwiDataCo( Gia_ManSwi_t * p, int i )  { return p->p
 void Gia_ManSetDefaultParamsSwi( Gia_ParSwi_t * p )
 {
     memset( p, 0, sizeof(Gia_ParSwi_t) );
-    p->nWords        =   1;  // the number of machine words of simulatation data 
+    p->nWords        =  10;  // the number of machine words of simulatation data 
     p->nIters        =  48;  // the number of all timeframes to simulate
     p->nPref         =  16;  // the number of first timeframes to skip when computing switching
     p->nRandPiFactor =   2;  // primary input transition probability (-1=3/8; 0=1/2; 1=1/4; 2=1/8, etc)
     p->fProbOne      =   0;  // compute probability of signal being one (if 0, compute probability of switching)
     p->fProbTrans    =   1;  // compute signal transition probability (if 0, compute transition probability using probability of being one)
-    p->fVerbose      =   1;  // enables verbose output
+    p->fVerbose      =   0;  // enables verbose output
 }
 
 /**Function*************************************************************
@@ -483,12 +483,14 @@ static inline void Gia_ManSwiSimulateRound( Gia_ManSwi_t * p, int fCount )
         else if ( Gia_ObjIsCo(pObj) )
         {
             assert( Gia_ObjValue(pObj) == GIA_NONE );
-            Gia_ManSwiSimulateCo( p, iCos++, pObj );
+//            Gia_ManSwiSimulateCo( p, iCos++, pObj );
+            Gia_ManSwiSimulateCo( p, Gia_ObjCioId(pObj), pObj );
         }
         else // if ( Gia_ObjIsCi(pObj) )
         {
             assert( Gia_ObjValue(pObj) < p->pAig->nFront );
-            Gia_ManSwiSimulateCi( p, pObj, iCis++ );
+//            Gia_ManSwiSimulateCi( p, pObj, iCis++ );
+            Gia_ManSwiSimulateCi( p, pObj, Gia_ObjCioId(pObj) );
         }
         if ( fCount && !Gia_ObjIsCo(pObj) )
         {
@@ -498,8 +500,8 @@ static inline void Gia_ManSwiSimulateRound( Gia_ManSwi_t * p, int fCount )
                 p->pData1[i] += Gia_ManSwiSimInfoCountOnes( p, Gia_ObjValue(pObj) );
         }
     }
-    assert( Gia_ManCiNum(p->pAig) == iCis );
-    assert( Gia_ManCoNum(p->pAig) == iCos );
+//    assert( Gia_ManCiNum(p->pAig) == iCis );
+//    assert( Gia_ManCoNum(p->pAig) == iCos );
 }
 
 /**Function*************************************************************
@@ -633,12 +635,10 @@ Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * pAig, int nFrames, int nPref
     // set the default parameters
     Gia_ManSetDefaultParamsSwi( pPars ); 
     // override some of the defaults
-    pPars->nWords   = 10;       // set number machine words to simulate
     pPars->nIters   = nFrames;  // set number of total timeframes
     if ( Abc_FrameReadFlag("seqsimframes") )
         pPars->nIters = atoi( Abc_FrameReadFlag("seqsimframes") );
     pPars->nPref    = nPref;    // set number of first timeframes to skip  
-    pPars->fVerbose = 0;        // disable verbose output
     // decide what should be computed
     if ( fProbOne )
     {
@@ -666,7 +666,94 @@ Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * pAig, int nFrames, int nPref
     return vResult;
 }
 
-  ////////////////////////////////////////////////////////////////////////
+/**Function*************************************************************
+
+  Synopsis    [Computes probability of switching (or of being 1).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Gia_ManEvaluateSwitching( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    float SwitchTotal = 0.0;
+    int i;
+    assert( p->pSwitching );
+    ABC_FREE( p->pRefs );
+    Gia_ManCreateRefs( p );
+    Gia_ManForEachObj( p, pObj, i )
+        SwitchTotal += (float)Gia_ObjRefs(p, pObj) * p->pSwitching[i] / 255;
+    return SwitchTotal;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes probability of switching (or of being 1).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne )
+{
+    Gia_Man_t * pDfs;
+    Gia_Obj_t * pObj, * pObjDfs;
+    Vec_Int_t * vSwitching;
+    float * pSwitching, Switch, SwitchTotal = 0.0, SwitchTotal2 = 0.0;
+    int i;
+    Gia_ParSwi_t Pars, * pPars = &Pars;
+    ABC_FREE( p->pSwitching );
+    // set the default parameters
+    Gia_ManSetDefaultParamsSwi( pPars ); 
+    // override some of the defaults
+    pPars->nIters   = nFrames;  // set number of total timeframes
+    pPars->nPref    = nPref;    // set number of first timeframes to skip  
+    // decide what should be computed
+    if ( fProbOne )
+    {
+        // if the user asked to compute propability of 1, we do not need transition information
+        pPars->fProbOne   = 1;  // enable computing probabiblity of being one
+        pPars->fProbTrans = 0;  // disable computing transition probability 
+    }
+    else
+    {
+        // if the user asked for transition propabability, we do not need to compute probability of 1
+        pPars->fProbOne   = 0;  // disable computing probabiblity of being one
+        pPars->fProbTrans = 1;  // enable computing transition probability 
+    }
+    // derives the DFS ordered AIG
+    Gia_ManCreateRefs( p );
+//    pDfs = Gia_ManDupOrderDfs( p );
+    pDfs = Gia_ManDup( p );
+    assert( Gia_ManObjNum(pDfs) == Gia_ManObjNum(p) );
+    // perform the computation of switching activity
+    vSwitching = Gia_ManSwiSimulate( pDfs, pPars );
+    // transfer the computed result to the original AIG
+    p->pSwitching = ABC_CALLOC( unsigned char, Gia_ManObjNum(p) );
+    pSwitching = (float *)vSwitching->pArray;
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        pObjDfs = Gia_ObjFromLit( pDfs, pObj->Value );
+        Switch = pSwitching[ Gia_ObjId(pDfs, pObjDfs) ];
+        p->pSwitching[i] = (char)((Switch >= 1.0) ? 255 : (int)((0.002 + Switch) * 255)); // 0.00196 = (1/255)/2
+        SwitchTotal += (float)Gia_ObjRefs(p, pObj) * p->pSwitching[i] / 255;
+//        SwitchTotal2 += Gia_ObjRefs(p, pObj) * Switch;
+//        printf( "%d = %.2f\n", i, Gia_ObjRefs(p, pObj) * Switch );
+    }
+//    printf( "\nSwitch float = %f. Switch char = %f.\n", SwitchTotal2, SwitchTotal );
+    Vec_IntFree( vSwitching );
+    Gia_ManStop( pDfs );
+    return SwitchTotal;
+}
+
+////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 

src/aig/gia/module.make

@@ -2,6 +2,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaAig.c \
     src/aig/gia/giaAiger.c \
     src/aig/gia/giaCof.c \
+    src/aig/gia/giaCSat.c \
     src/aig/gia/giaDfs.c \
     src/aig/gia/giaDup.c \
     src/aig/gia/giaEmbed.c \
@@ -15,6 +16,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaHash.c \
     src/aig/gia/giaMan.c \
     src/aig/gia/giaMap.c \
+    src/aig/gia/giaPat.c \
     src/aig/gia/giaRetime.c \
     src/aig/gia/giaScl.c \
     src/aig/gia/giaSim.c \

src/aig/int/intCtrex.c

@@ -111,6 +111,8 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
     Cnf_DataFree( pCnf );
     if ( pSat == NULL )
     {
+        printf( "Counter-example generation in command \"int\" has failed.\n" );
+        printf( "Use command \"bmc2\" to produce a valid counter-example.\n" );
         Vec_IntFree( vCiIds );
         return NULL;
     }

src/aig/ssw/sswClass.c

@@ -391,7 +391,8 @@ void Ssw_ClassesPrintOne( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
     int i;
     printf( "{ " );
     Ssw_ClassForEachNode( p, pRepr, pObj, i )
-        printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
+        printf( "%d(%d,%d,%d) ", pObj->Id, pObj->Level, 
+        Aig_SupportSize(p->pAig,pObj), Aig_NodeMffsSupp(p->pAig,pObj,0,NULL) );
     printf( "}\n" );
 }
 
@@ -418,7 +419,8 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
     printf( "Constants { " );
     Aig_ManForEachObj( p->pAig, pObj, i )
         if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
-            printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
+            printf( "%d(%d,%d,%d) ", pObj->Id, pObj->Level, 
+            Aig_SupportSize(p->pAig,pObj), Aig_NodeMffsSupp(p->pAig,pObj,0,NULL) );
     printf( "}\n" );
     Ssw_ManForEachClass( p, ppClass, i )
     {

src/aig/ssw/sswCore.c

@@ -216,6 +216,7 @@ clk = clock();
 p->timeTotal = clock() - clkTotal;
     pAigNew = Aig_ManDupRepr( p->pAig, 0 );
     Aig_ManSeqCleanup( pAigNew );
+//Ssw_ClassesPrint( p->ppClasses, 1 );
     // get the final stats
     p->nLitsEnd  = Ssw_ClassesLitNum( p->ppClasses );
     p->nNodesEnd = Aig_ManNodeNum(pAigNew);

src/aig/ssw/sswLcorr.c

@@ -308,6 +308,9 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
             p->nRecycleCalls = 0;
         }
     }
+//    ABC_PRT( "reduce", p->timeReduce );
+//    Aig_TableProfile( p->pFrames );
+//    printf( "And gates = %d\n", Aig_ManNodeNum(p->pFrames) );
     // resimulate
     if ( p->nPatterns > 0 )
         Ssw_ManSweepResimulate( p );

src/base/abc/abcFunc.c

@@ -595,6 +595,7 @@ Hop_Obj_t * Abc_ConvertSopToAigInternal( Hop_Man_t * pMan, char * pSop )
     Hop_Obj_t * pAnd, * pSum;
     int i, Value, nFanins;
     char * pCube;
+    int fExor = Abc_SopIsExorType(pSop);
     // get the number of variables
     nFanins = Abc_SopGetVarNum(pSop);
     // go through the cubes of the node's SOP
@@ -611,7 +612,10 @@ Hop_Obj_t * Abc_ConvertSopToAigInternal( Hop_Man_t * pMan, char * pSop )
                 pAnd = Hop_And( pMan, pAnd, Hop_Not(Hop_IthVar(pMan,i)) );
         }
         // add to the sum of cubes
-        pSum = Hop_Or( pMan, pSum, pAnd );
+        if ( fExor )
+            pSum = Hop_Exor( pMan, pSum, pAnd );
+        else
+            pSum = Hop_Or( pMan, pSum, pAnd );
     }
     // decide whether to complement the result
     if ( Abc_SopIsComplement(pSop) )
@@ -637,11 +641,8 @@ Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop )
     // consider the constant node
     if ( Abc_SopGetVarNum(pSop) == 0 )
         return Hop_NotCond( Hop_ManConst1(pMan), Abc_SopIsConst0(pSop) );
-    // consider the special case of EXOR function
-    if ( Abc_SopIsExorType(pSop) )
-        return Hop_NotCond( Hop_CreateExor(pMan, Abc_SopGetVarNum(pSop)), Abc_SopIsComplement(pSop) );
     // decide when to use factoring
-    if ( fUseFactor && Abc_SopGetVarNum(pSop) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
+    if ( fUseFactor && Abc_SopGetVarNum(pSop) > 2 && Abc_SopGetCubeNum(pSop) > 1 && !Abc_SopIsExorType(pSop) )
         return Dec_GraphFactorSop( pMan, pSop );
     return Abc_ConvertSopToAigInternal( pMan, pSop );
 }

src/base/abc/abcLib.c

@@ -82,6 +82,8 @@ void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
                 continue;
 //            pNtk->pManFunc = NULL;
             pNtk->pDesign = NULL;
+            if ( pNtk->pManFunc == pNtkSave->pManFunc )
+                pNtk->pManFunc = NULL;
             Abc_NtkDelete( pNtk );
         }
         Vec_PtrFree( pLib->vModules );

src/base/abci/abcGen.c

@@ -599,6 +599,56 @@ void Abc_GenOneHotIntervals( char * pFileName, int nPis, int nRegs, Vec_Ptr_t *
     fclose( pFile );
 }
 
+#include "aig.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Generates structure of L K-LUTs implementing an N-var function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_GenRandom( char * pFileName, int nPis )
+{
+    FILE * pFile;
+    unsigned * pTruth;
+    int i, b, w, nWords = Aig_TruthWordNum( nPis );
+    int nDigitsIn;
+    Aig_ManRandom( 1 );
+    pTruth = ABC_ALLOC( unsigned, nWords );
+    for ( w = 0; w < nWords; w++ )
+        pTruth[w] = Aig_ManRandom( 0 );
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# Random function with %d inputs generated by ABC on %s\n", nPis, Extra_TimeStamp() );
+    fprintf( pFile, ".model rand%d\n", nPis );
+    fprintf( pFile, ".inputs" );
+    nDigitsIn = Extra_Base10Log( nPis );
+    for ( i = 0; i < nPis; i++ )
+        fprintf( pFile, " i%0*d", nDigitsIn, i );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, ".outputs f\n" );
+    fprintf( pFile, ".names" );
+    nDigitsIn = Extra_Base10Log( nPis );
+    for ( i = 0; i < nPis; i++ )
+        fprintf( pFile, " i%0*d", nDigitsIn, i );
+    fprintf( pFile, " f\n" );
+    for ( i = 0; i < (1<<nPis); i++ )
+        if ( Aig_InfoHasBit(pTruth, i) )
+        {
+            for ( b = nPis-1; b >= 0; b-- )
+                fprintf( pFile, "%d", (i>>b)&1 );
+            fprintf( pFile, " 1\n" );
+        }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+    fclose( pFile );
+    ABC_FREE( pTruth );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/abci/abcIvy.c

@@ -946,12 +946,8 @@ Ivy_Obj_t * Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode )
     if ( Abc_NodeIsConst(pNode) )
         return Ivy_NotCond( Ivy_ManConst1(pMan), Abc_SopIsConst0(pSop) );
 
-    // consider the special case of EXOR function
-    if ( Abc_SopIsExorType(pSop) )
-        return Abc_NodeStrashAigExorAig( pMan, pNode, pSop );
-
     // decide when to use factoring
-    if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
+    if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 && !Abc_SopIsExorType(pSop) )
         return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop );
     return Abc_NodeStrashAigSopAig( pMan, pNode, pSop );
 }
@@ -973,6 +969,7 @@ Ivy_Obj_t * Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char *
     Ivy_Obj_t * pAnd, * pSum;
     char * pCube;
     int i, nFanins;
+    int fExor = Abc_SopIsExorType(pSop);
 
     // get the number of node's fanins
     nFanins = Abc_ObjFaninNum( pNode );
@@ -991,7 +988,10 @@ Ivy_Obj_t * Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char *
                 pAnd = Ivy_And( pMan, pAnd, Ivy_Not((Ivy_Obj_t *)pFanin->pCopy) );
         }
         // add to the sum of cubes
-        pSum = Ivy_Or( pMan, pSum, pAnd );
+        if ( fExor )
+            pSum = Ivy_Exor( pMan, pSum, pAnd );
+        else
+            pSum = Ivy_Or( pMan, pSum, pAnd );
     }
     // decide whether to complement the result
     if ( Abc_SopIsComplement(pSop) )

src/base/abci/abcPrint.c

@@ -135,8 +135,10 @@ float Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk )
     Abc_NtkForEachObj( pNtk, pObjAbc, i )
     {
         if ( (pObjAbc2 = Abc_ObjRegular(pObjAbc->pTemp)) && (pObjAig = Aig_Regular(pObjAbc2->pTemp)) )
+        {
             Result += Abc_ObjFanoutNum(pObjAbc) * pSwitching[pObjAig->Id];
-//            Result += pSwitching[pObjAig->Id];
+//            printf( "%d = %.2f\n", i, Abc_ObjFanoutNum(pObjAbc) * pSwitching[pObjAig->Id] );
+        }
     }
     Vec_IntFree( vSwitching );
     Aig_ManStop( pAig );

src/base/io/io.c

@@ -1849,6 +1849,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
 
     if ( argc != globalUtilOptind + 1 )
     {
+        printf( "File name is missing on the command line.\n" );
         goto usage;
     }
     // get the input file name

src/base/io/ioReadBlifMv.c

@@ -1615,7 +1615,7 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
     Vec_Str_t * vFunc = p->pMan->vFunc;
-    char * pProduct, * pOutput;
+    char * pProduct, * pOutput, c;
     int i, Polarity = -1;
 
     p->pMan->nTablesRead++;
@@ -1626,7 +1626,8 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
     if ( Vec_PtrSize(vTokens) == 1 )
     {
         pOutput = Vec_PtrEntry( vTokens, 0 );
-        if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
+        c = pOutput[0];
+        if ( (c!='0'&&c!='1'&&c!='x'&&c!='n') || pOutput[1] )
         {
             sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Io_MvGetLine(p->pMan, pOutput), pOutput );
             return NULL;
@@ -1650,14 +1651,15 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
             sprintf( p->pMan->sError, "Line %d: Cube \"%s\" has size different from the fanin count (%d).", Io_MvGetLine(p->pMan, pProduct), pProduct, nFanins );
             return NULL;
         }
-        if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
+        c = pOutput[0];
+        if ( (c!='0'&&c!='1'&&c!='x'&&c!='n') || pOutput[1] )
         {
             sprintf( p->pMan->sError, "Line %d: Output value \"%s\" is incorrect.", Io_MvGetLine(p->pMan, pProduct), pOutput );
             return NULL;
         }
         if ( Polarity == -1 )
-            Polarity = pOutput[0] - '0';
-        else if ( Polarity != pOutput[0] - '0' )
+            Polarity = (c=='1' || c=='x');
+        else if ( Polarity != (c=='1' || c=='x') )
         {
             sprintf( p->pMan->sError, "Line %d: Output value \"%s\" differs from the value in the first line of the table (%d).", Io_MvGetLine(p->pMan, pProduct), pOutput, Polarity );
             return NULL;

src/base/ver/verCore.c

@@ -2042,6 +2042,11 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
     assert( !Ver_ObjIsConnected(pBox) );
     assert( Ver_NtkIsDefined(pNtkBox) );
     assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 );
+
+    if ( !strcmp(pNtkBox->pName,"add_4u_4u") )
+    {
+        int s = 0;
+    }
 /*
     // clean the PI/PO nets
     Abc_NtkForEachPi( pNtkBox, pTerm, i )
@@ -2134,7 +2139,7 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
                 if ( Length > 0 )
                 {
                     Vec_PtrForEachEntry( vBundles, pBundle, j )
-                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
+                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) && (int)strlen(pBundle->pNameFormal) == Length )
                             break;
                     if ( j == Vec_PtrSize(vBundles) )
                         pBundle = NULL;
@@ -2185,7 +2190,7 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
                 if ( Length > 0 )
                 {
                     Vec_PtrForEachEntry( vBundles, pBundle, j )
-                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
+                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) && (int)strlen(pBundle->pNameFormal) == Length ) 
                             break;
                     if ( j == Vec_PtrSize(vBundles) )
                         pBundle = NULL;
@@ -2193,8 +2198,14 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
             }
             if ( pBundle == NULL )
             {
+                char Buffer[1000];
 //                printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", 
 //                    pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
+                pTermNew = Abc_NtkCreateBo( pNtk );
+                sprintf( Buffer, "_temp_net%d", Abc_ObjId(pTermNew) );
+                pNetAct = Abc_NtkFindOrCreateNet( pNtk, Buffer );
+                Abc_ObjAddFanin( pTermNew, pBox );
+                Abc_ObjAddFanin( pNetAct, pTermNew );
                 continue;
             }
         }

src/map/cov/cov.h

+/**CFile****************************************************************
+
+  FileName    [cov.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Mapping into network of SOPs/ESOPs.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+   
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cov.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __COV_H__
+#define __COV_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#include "abc.h"
+#include "covInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cov_Man_t_  Cov_Man_t;
+typedef struct Cov_Obj_t_  Cov_Obj_t;
+
+// storage for node information
+struct Cov_Obj_t_
+{
+    Min_Cube_t *      pCover[3];    // pos/neg/esop
+    Vec_Int_t *       vSupp;        // computed support (all nodes except CIs)
+};
+
+// storage for additional information
+struct Cov_Man_t_
+{
+    // general characteristics
+    int               nFaninMax;    // the number of vars
+    int               nCubesMax;    // the limit on the number of cubes in the intermediate covers
+    int               nWords;       // the number of words
+    Vec_Int_t *       vFanCounts;   // fanout counts
+    Vec_Ptr_t *       vObjStrs;     // object structures
+    void *            pMemory;      // memory for the internal data strctures
+    Min_Man_t *       pManMin;      // the cube manager
+    int               fUseEsop;     // enables ESOPs
+    int               fUseSop;      // enables SOPs
+    // arrays to map local variables
+    Vec_Int_t *       vComTo0;      // mapping of common variables into first fanin
+    Vec_Int_t *       vComTo1;      // mapping of common variables into second fanin
+    Vec_Int_t *       vPairs0;      // the first var in each pair of common vars
+    Vec_Int_t *       vPairs1;      // the second var in each pair of common vars
+    Vec_Int_t *       vTriv0;       // trival support of the first node
+    Vec_Int_t *       vTriv1;       // trival support of the second node
+    // statistics
+    int               nSupps;       // supports created
+    int               nSuppsMax;    // the maximum number of supports
+    int               nBoundary;    // the boundary size
+    int               nNodes;       // the number of nodes processed
+};
+
+static inline Cov_Obj_t *  Abc_ObjGetStr( Abc_Obj_t * pObj )                       { return Vec_PtrEntry(((Cov_Man_t *)pObj->pNtk->pManCut)->vObjStrs, pObj->Id); }
+
+static inline void         Abc_ObjSetSupp( Abc_Obj_t * pObj, Vec_Int_t * vVec )    { Abc_ObjGetStr(pObj)->vSupp = vVec;   }
+static inline Vec_Int_t *  Abc_ObjGetSupp( Abc_Obj_t * pObj )                      { return Abc_ObjGetStr(pObj)->vSupp;   }
+
+static inline void         Abc_ObjSetCover2( Abc_Obj_t * pObj, Min_Cube_t * pCov ) { Abc_ObjGetStr(pObj)->pCover[2] = pCov; }
+static inline Min_Cube_t * Abc_ObjGetCover2( Abc_Obj_t * pObj )                    { return Abc_ObjGetStr(pObj)->pCover[2]; }
+
+static inline void         Abc_ObjSetCover( Abc_Obj_t * pObj, Min_Cube_t * pCov, int Pol ) { Abc_ObjGetStr(pObj)->pCover[Pol] = pCov; }
+static inline Min_Cube_t * Abc_ObjGetCover( Abc_Obj_t * pObj, int Pol )                    { return Abc_ObjGetStr(pObj)->pCover[Pol]; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== covBuild.c ==========================================================*/
+extern Abc_Ntk_t * Abc_NtkCovDerive( Cov_Man_t * p, Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t * Abc_NtkCovDeriveClean( Cov_Man_t * p, Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t * Abc_NtkCovDeriveRegular( Cov_Man_t * p, Abc_Ntk_t * pNtk );
+/*=== covCore.c ===========================================================*/
+extern Abc_Ntk_t * Abc_NtkSopEsopCover( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
+/*=== covMan.c ============================================================*/
+extern Cov_Man_t * Cov_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax );
+extern void        Cov_ManFree( Cov_Man_t * p );
+extern void        Abc_NodeCovDropData( Cov_Man_t * p, Abc_Obj_t * pObj );
+/*=== covTest.c ===========================================================*/
+extern Abc_Ntk_t * Abc_NtkCovTestSop( Abc_Ntk_t * pNtk );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+

src/map/cov/covMan.c

+/**CFile****************************************************************
+
+  FileName    [covMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Mapping into network of SOPs/ESOPs.]
+
+  Synopsis    [Decomposition manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: covMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cov.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cov_Man_t * Cov_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax )
+{
+    Cov_Man_t * pMan;
+    Cov_Obj_t * pMem;
+    Abc_Obj_t * pObj;
+    int i;
+    assert( pNtk->pManCut == NULL );
+
+    // start the manager
+    pMan = ABC_ALLOC( Cov_Man_t, 1 );
+    memset( pMan, 0, sizeof(Cov_Man_t) );
+    pMan->nFaninMax = nFaninMax;
+    pMan->nCubesMax = 2 * pMan->nFaninMax;
+    pMan->nWords    = Abc_BitWordNum( nFaninMax * 2 );
+
+    // get the cubes
+    pMan->vComTo0 = Vec_IntAlloc( 2*nFaninMax );
+    pMan->vComTo1 = Vec_IntAlloc( 2*nFaninMax );
+    pMan->vPairs0 = Vec_IntAlloc( nFaninMax );
+    pMan->vPairs1 = Vec_IntAlloc( nFaninMax );
+    pMan->vTriv0  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv0, -1 ); 
+    pMan->vTriv1  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv1, -1 ); 
+
+    // allocate memory for object structures
+    pMan->pMemory = pMem = ABC_ALLOC( Cov_Obj_t, sizeof(Cov_Obj_t) * Abc_NtkObjNumMax(pNtk) );
+    memset( pMem, 0, sizeof(Cov_Obj_t) * Abc_NtkObjNumMax(pNtk) );
+    // allocate storage for the pointers to the memory
+    pMan->vObjStrs = Vec_PtrAlloc( Abc_NtkObjNumMax(pNtk) );
+    Vec_PtrFill( pMan->vObjStrs, Abc_NtkObjNumMax(pNtk), NULL );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        Vec_PtrWriteEntry( pMan->vObjStrs, i, pMem + i );
+    // create the cube manager
+    pMan->pManMin = Min_ManAlloc( nFaninMax );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cov_ManFree( Cov_Man_t * p )
+{
+    Vec_Int_t * vSupp;
+    int i;
+    for ( i = 0; i < p->vObjStrs->nSize; i++ )
+    {
+        vSupp = ((Cov_Obj_t *)p->vObjStrs->pArray[i])->vSupp;
+        if ( vSupp ) Vec_IntFree( vSupp );
+    }
+
+    Min_ManFree( p->pManMin );
+    Vec_PtrFree( p->vObjStrs );
+    Vec_IntFree( p->vFanCounts );
+    Vec_IntFree( p->vTriv0 );
+    Vec_IntFree( p->vTriv1 );
+    Vec_IntFree( p->vComTo0 );
+    Vec_IntFree( p->vComTo1 );
+    Vec_IntFree( p->vPairs0 );
+    Vec_IntFree( p->vPairs1 );
+    ABC_FREE( p->pMemory );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Drop the covers at the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeCovDropData( Cov_Man_t * p, Abc_Obj_t * pObj )
+{
+    int nFanouts;
+    assert( p->vFanCounts );
+    nFanouts = Vec_IntEntry( p->vFanCounts, pObj->Id );
+    assert( nFanouts > 0 );
+    if ( --nFanouts == 0 )
+    {
+        Vec_IntFree( Abc_ObjGetSupp(pObj) );
+        Abc_ObjSetSupp( pObj, NULL );
+        Min_CoverRecycle( p->pManMin, Abc_ObjGetCover2(pObj) );
+        Abc_ObjSetCover2( pObj, NULL );
+        p->nSupps--;
+    }
+    Vec_IntWriteEntry( p->vFanCounts, pObj->Id, nFanouts );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/map/cov/covMinEsop.c

+/**CFile****************************************************************
+
+  FileName    [covMinEsop.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Mapping into network of SOPs/ESOPs.]
+
+  Synopsis    [ESOP manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: covMinEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "covInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Min_EsopRewrite( Min_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_EsopMinimize( Min_Man_t * p )
+{
+    int nCubesInit, nCubesOld, nIter;
+    if ( p->nCubes < 3 )
+        return;
+    nIter = 0;
+    nCubesInit = p->nCubes;
+    do {
+        nCubesOld = p->nCubes;
+        Min_EsopRewrite( p );
+        nIter++;
+    }
+    while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+
+//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of rewriting using distance 2 cubes.]
+
+  Description [The weakness of this procedure is that it tries each cube
+  with only one distance-2 cube. If this pair does not lead to improvement
+  the cube is inserted into the cover anyhow, and we try another pair.
+  A possible improvement would be to try this cube with all distance-2
+  cubes, until an improvement is found, or until all such cubes are tried.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_EsopRewrite( Min_Man_t * p )
+{
+    Min_Cube_t * pCube, ** ppPrev;
+    Min_Cube_t * pThis, ** ppPrevT;
+    int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld;
+    int nPairs = 0;
+
+    // insert the bubble before the first cube
+    p->pBubble->pNext = p->ppStore[0];
+    p->ppStore[0] = p->pBubble;
+    p->pBubble->nLits = 0;
+
+    // go through the cubes
+    while ( 1 )
+    {
+        // get the index of the bubble
+        Index = p->pBubble->nLits;
+
+        // find the bubble
+        Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
+            if ( pCube == p->pBubble )
+                break;
+        assert( pCube == p->pBubble );
+
+        // remove the bubble, get the next cube after the bubble
+        *ppPrev = p->pBubble->pNext;
+        pCube = p->pBubble->pNext;
+        if ( pCube == NULL )
+            for ( Index++; Index <= p->nVars; Index++ )
+                if ( p->ppStore[Index] )
+                {
+                    ppPrev = &(p->ppStore[Index]);
+                    pCube = p->ppStore[Index];
+                    break;
+                }
+        // stop if there is no more cubes
+        if ( pCube == NULL )
+            break;
+
+        // find the first dist2 cube
+        Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        if ( pThis == NULL && Index < p->nVars )
+        Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        if ( pThis == NULL && Index < p->nVars - 1 )
+        Min_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT )
+            if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        // continue if there is no dist2 cube
+        if ( pThis == NULL )
+        {
+            // insert the bubble after the cube
+            p->pBubble->pNext = pCube->pNext;
+            pCube->pNext = p->pBubble;
+            p->pBubble->nLits = pCube->nLits;
+            continue;
+        }
+        nPairs++;
+
+        // remove the cubes, insert the bubble instead of pCube
+        *ppPrevT = pThis->pNext;
+        *ppPrev = p->pBubble;
+        p->pBubble->pNext = pCube->pNext;
+        p->pBubble->nLits = pCube->nLits;
+        p->nCubes -= 2;
+
+        // Exorlink-2:
+        // A{v00}     B{v01}      +  A{v10}     B{v11}     =
+        // A{v00+v10} B{v01}      +  A{v10}     B{v01+v11} =
+        // A{v00}     B{v01+v11}  +  A{v00+v10} B{v11}
+
+        // save the dist2 parameters
+        v00 = Min_CubeGetVar( pCube, Var0 );
+        v01 = Min_CubeGetVar( pCube, Var1 );
+        v10 = Min_CubeGetVar( pThis, Var0 );
+        v11 = Min_CubeGetVar( pThis, Var1 );
+//printf( "\n" );
+//Min_CubeWrite( stdout, pCube );
+//Min_CubeWrite( stdout, pThis );
+
+        // derive the first pair of resulting cubes
+        Min_CubeXorVar( pCube, Var0, v10 );
+        pCube->nLits -= (v00 != 3);
+        pCube->nLits += ((v00 ^ v10) != 3);
+        Min_CubeXorVar( pThis, Var1, v01 );
+        pThis->nLits -= (v11 != 3);
+        pThis->nLits += ((v01 ^ v11) != 3);
+
+        // add the cubes
+        nCubesOld = p->nCubes;
+        Min_EsopAddCube( p, pCube );
+        Min_EsopAddCube( p, pThis );
+        // check if the cubes were absorbed
+        if ( p->nCubes < nCubesOld + 2 )
+            continue;
+
+        // pull out both cubes
+        assert( pThis == p->ppStore[pThis->nLits] );
+        p->ppStore[pThis->nLits] = pThis->pNext;
+        assert( pCube == p->ppStore[pCube->nLits] );
+        p->ppStore[pCube->nLits] = pCube->pNext;
+        p->nCubes -= 2;
+
+        // derive the second pair of resulting cubes
+        Min_CubeXorVar( pCube, Var0, v10 );
+        pCube->nLits -= ((v00 ^ v10) != 3);
+        pCube->nLits += (v00 != 3);
+        Min_CubeXorVar( pCube, Var1, v11 );
+        pCube->nLits -= (v01 != 3);
+        pCube->nLits += ((v01 ^ v11) != 3);
+
+        Min_CubeXorVar( pThis, Var0, v00 );
+        pThis->nLits -= (v10 != 3);
+        pThis->nLits += ((v00 ^ v10) != 3);
+        Min_CubeXorVar( pThis, Var1, v01 );
+        pThis->nLits -= ((v01 ^ v11) != 3);
+        pThis->nLits += (v11 != 3);
+
+        // add them anyhow
+        Min_EsopAddCube( p, pCube );
+        Min_EsopAddCube( p, pThis );
+    }
+//    printf( "Pairs = %d  ", nPairs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cube to storage.]
+
+  Description [Returns 0 if the cube is added or removed. Returns 1
+  if the cube is glued with some other cube and has to be added again.
+  Do not forget to clean the storage!]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    Min_Cube_t * pThis, ** ppPrev;
+    // try to find the identical cube
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Min_CubesAreEqual( pCube, pThis ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubeRecycle( p, pCube );
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 0;
+        }
+    }
+    // find a distance-1 cube if it exists
+    if ( pCube->nLits < pCube->nVars )
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransform( pCube, pThis, p->pTemp );
+            pCube->nLits++;
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransform( pCube, pThis, p->pTemp );
+            pCube->nLits--;
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    if ( pCube->nLits > 0 )
+    Min_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev )
+    {
+        if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Min_CubesTransform( pCube, pThis, p->pTemp );
+            Min_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    // add the cube
+    pCube->pNext = p->ppStore[pCube->nLits];
+    p->ppStore[pCube->nLits] = pCube;
+    p->nCubes++;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cube to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
+{
+    assert( pCube != p->pBubble );
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    while ( Min_EsopAddCubeInt( p, pCube ) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/map/cov/covMinMan.c

+/**CFile****************************************************************
+
+  FileName    [covMinMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Mapping into network of SOPs/ESOPs.]
+
+  Synopsis    [SOP manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: covMinMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "covInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Man_t * Min_ManAlloc( int nVars )
+{
+    Min_Man_t * pMan;
+    // start the manager
+    pMan = ABC_ALLOC( Min_Man_t, 1 );
+    memset( pMan, 0, sizeof(Min_Man_t) );
+    pMan->nVars   = nVars;
+    pMan->nWords  = Abc_BitWordNum( nVars * 2 );
+    pMan->pMemMan = Extra_MmFixedStart( sizeof(Min_Cube_t) + sizeof(unsigned) * (pMan->nWords - 1) );
+    // allocate storage for the temporary cover
+    pMan->ppStore = ABC_ALLOC( Min_Cube_t *, pMan->nVars + 1 );
+    // create tautology cubes
+    Min_ManClean( pMan, nVars );
+    pMan->pOne0  = Min_CubeAlloc( pMan );
+    pMan->pOne1  = Min_CubeAlloc( pMan );
+    pMan->pTemp  = Min_CubeAlloc( pMan );
+    pMan->pBubble = Min_CubeAlloc( pMan );  pMan->pBubble->uData[0] = 0;
+    // create trivial cubes
+    Min_ManClean( pMan, 1 );
+    pMan->pTriv0[0] = Min_CubeAllocVar( pMan, 0, 0 );
+    pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 );   
+    pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 );
+    pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 );   
+    Min_ManClean( pMan, nVars );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_ManClean( Min_Man_t * p, int nSupp )
+{
+    // set the size of the cube manager
+    p->nVars  = nSupp;
+    p->nWords = Abc_BitWordNum(2*nSupp);
+    // clean the storage
+    memset( p->ppStore, 0, sizeof(Min_Cube_t *) * (nSupp + 1) );
+    p->nCubes = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_ManFree( Min_Man_t * p )
+{
+    Extra_MmFixedStop( p->pMemMan );
+    ABC_FREE( p->ppStore );
+    ABC_FREE( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/map/cov/covMinUtil.c

+/**CFile****************************************************************
+
+  FileName    [covMinUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Mapping into network of SOPs/ESOPs.]
+
+  Synopsis    [Utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: covMinUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "covInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CubeCreate( Vec_Str_t * vCover, Min_Cube_t * pCube, char Type )
+{
+    int i;
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    for ( i = 0; i < (int)pCube->nVars; i++ )
+        if ( Min_CubeHasBit(pCube, i*2) )
+        {
+            if ( Min_CubeHasBit(pCube, i*2+1) )
+//                fprintf( pFile, "-" );
+                Vec_StrPush( vCover, '-' );
+            else
+//                fprintf( pFile, "0" );
+                Vec_StrPush( vCover, '0' );
+        }
+        else
+        {
+            if ( Min_CubeHasBit(pCube, i*2+1) )
+ //               fprintf( pFile, "1" );
+                Vec_StrPush( vCover, '1' );
+            else
+//                fprintf( pFile, "?" );
+                Vec_StrPush( vCover, '?' );
+        }
+//    fprintf( pFile, " 1\n" );
+    Vec_StrPush( vCover, ' ' );
+    Vec_StrPush( vCover, Type );
+    Vec_StrPush( vCover, '\n' );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverCreate( Vec_Str_t * vCover, Min_Cube_t * pCover, char Type )
+{
+    Min_Cube_t * pCube;
+    assert( pCover != NULL );
+    Vec_StrClear( vCover );
+    Min_CoverForEachCube( pCover, pCube )
+        Min_CubeCreate( vCover, pCube, Type );
+    Vec_StrPush( vCover, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube )
+{
+    int i;
+    assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
+    for ( i = 0; i < (int)pCube->nVars; i++ )
+        if ( Min_CubeHasBit(pCube, i*2) )
+        {
+            if ( Min_CubeHasBit(pCube, i*2+1) )
+                fprintf( pFile, "-" );
+            else
+                fprintf( pFile, "0" );
+        }
+        else
+        {
+            if ( Min_CubeHasBit(pCube, i*2+1) )
+                fprintf( pFile, "1" );
+            else
+                fprintf( pFile, "?" );
+        }
+    fprintf( pFile, " 1\n" );
+//    fprintf( pFile, " %d\n", pCube->nLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube;
+    Min_CoverForEachCube( pCover, pCube )
+        Min_CubeWrite( pFile, pCube );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p )
+{
+    Min_Cube_t * pCube;
+    int i;
+    for ( i = 0; i <= p->nVars; i++ )
+    {
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+        {
+            printf( "%2d : ", i );
+            if ( pCube == p->pBubble )
+            {
+                printf( "Bubble\n" );
+                continue;
+            }
+            Min_CubeWrite( pFile, pCube );
+        }
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
+{
+    char Buffer[1000];
+    Min_Cube_t * pCube;
+    FILE * pFile;
+    int i;
+    sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" );
+    for ( i = strlen(Buffer) - 1; i >= 0; i-- )
+        if ( Buffer[i] == '<' || Buffer[i] == '>' )
+            Buffer[i] = '_';
+    pFile = fopen( Buffer, "w" );
+    fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() );
+    fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 );
+    fprintf( pFile, ".o %d\n", 1 );
+    fprintf( pFile, ".p %d\n", Min_CoverCountCubes(pCover) );
+    if ( fEsop ) fprintf( pFile, ".type esop\n" );
+    Min_CoverForEachCube( pCover, pCube )
+        Min_CubeWrite( pFile, pCube );
+    fprintf( pFile, ".e\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverCheck( Min_Man_t * p )
+{
+    Min_Cube_t * pCube;
+    int i;
+    for ( i = 0; i <= p->nVars; i++ )
+        Min_CoverForEachCube( p->ppStore[i], pCube )
+            assert( i == (int)pCube->nLits );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_CubeCheck( Min_Cube_t * pCube )
+{
+    int i;
+    for ( i = 0; i < (int)pCube->nVars; i++ )
+        if ( Min_CubeGetVar( pCube, i ) == 0 )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the cover from the sorted structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize )
+{
+    Min_Cube_t * pCov = NULL, ** ppTail = &pCov;
+    Min_Cube_t * pCube, * pCube2;
+    int i;
+    for ( i = 0; i <= nSuppSize; i++ )
+    {
+        Min_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 )
+        {
+            assert( i == (int)pCube->nLits );
+            *ppTail = pCube; 
+            ppTail = &pCube->pNext;
+            assert( pCube->uData[0] ); // not a bubble
+        }
+    }
+    *ppTail = NULL;
+    return pCov;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cover in the increasing number of literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube, * pCube2;
+    Min_ManClean( p, p->nVars );
+    Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+    {
+        pCube->pNext = p->ppStore[pCube->nLits];
+        p->ppStore[pCube->nLits] = pCube;
+        p->nCubes++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cover in the increasing number of literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover )
+{
+    Min_Cube_t * pCube;
+    int i, Counter;
+    if ( pCover == NULL )
+        return 0;
+    // clean the cube
+    for ( i = 0; i < (int)pCover->nWords; i++ )
+        p->pTemp->uData[i]  = ~((unsigned)0);
+    // add the bit data
+    Min_CoverForEachCube( pCover, pCube )
+        for ( i = 0; i < (int)pCover->nWords; i++ )
+            p->pTemp->uData[i] &= pCube->uData[i];
+    // count the vars
+    Counter = 0;
+    for ( i = 0; i < (int)pCover->nVars; i++ )
+        Counter += ( Min_CubeGetVar(p->pTemp, i) != 3 );
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/map/cov/module.make

+SRC +=    src/map/cov/covBuild.c \
+    src/map/cov/covCore.c \
+    src/map/cov/covMan.c \
+    src/map/cov/covMinEsop.c \
+    src/map/cov/covMinMan.c \
+    src/map/cov/covMinSop.c \
+    src/map/cov/covMinUtil.c