Version abc60303

abc.dsp

@@ -222,10 +222,6 @@ SOURCE=.\src\base\abci\abcMiter.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\base\abci\abcNewAig.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\base\abci\abcNtbdd.c
 # End Source File
 # Begin Source File
@@ -258,6 +254,10 @@ SOURCE=.\src\base\abci\abcRestruct.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcResub.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcRewrite.c
 # End Source File
 # Begin Source File

abc.rc

@@ -76,9 +76,8 @@ alias compress  "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
 alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
 alias choice    "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
 alias choice2   "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
-alias rwsat     "st; rw -l; rf -l; b -l; rw -l; rf -l"
-alias t         "r c/4/csat_101_opt.blif; st; ps; test"
-alias t2        "r c/5/csat_026.bench; st; ps; test"
-alias r1        "r c/4/csat_101_opt.blif; st; ps"
+alias rwsat     "st; rw -l; b -l; rw -l; rf -l"
+alias rwsat2    "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l"
+alias shake     "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
 
 

readme

@@ -8,3 +8,8 @@ The following steps may be needed to compile it on UNIX:
 
 If compiling as a static library, it is necessary to uncomment
 #define _LIB in "src/abc/main/main.c"
+
+
+Several things to try if it does not compile on your platform:
+- Try running all code through dos2unix (Solaris)
+- Try removing flags from the libs line (LIBS :=) in Makefile (Mac)
\ No newline at end of file

src/base/abc/abc.h

@@ -21,6 +21,10 @@
 #ifndef __ABC_H__
 #define __ABC_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -435,7 +439,7 @@ extern bool               Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 /*=== abcCollapse.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose );
+extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose );
 /*=== abcCut.c ==========================================================*/
 extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti );
 extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti );
@@ -471,7 +475,7 @@ extern void               Abc_NtkFraigStoreClean();
 extern int                Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
 extern DdNode *           Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
 extern char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode );
-extern int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect );
 extern void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 );
 extern int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
 extern void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
@@ -528,6 +532,7 @@ extern char *             Abc_NtkLogicStoreName( Abc_Obj_t * pNodeNew, char * pN
 extern char *             Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pNodeNew, char * pNameOld, char * pSuffix );
 extern void               Abc_NtkCreateCioNamesTable( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern void               Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern Vec_Ptr_t *        Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
 extern Vec_Ptr_t *        Abc_NodeGetFakeNames( int nNames );
 extern void               Abc_NodeFreeNames( Vec_Ptr_t * vNames );
@@ -541,7 +546,7 @@ extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
 extern stmm_table *       Abc_NtkNamesToTable( Vec_Ptr_t * vNodes );
 /*=== abcNetlist.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect );
 extern Abc_Ntk_t *        Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk );
@@ -549,12 +554,12 @@ extern Abc_Ntk_t *        Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk );
 /*=== abcNtbdd.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
 extern Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
-extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly );
+extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fLatchOnly );
 extern void               Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcNtk.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
-extern Abc_Ntk_t *        Abc_NtkStartFromSeq( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern Abc_Ntk_t *        Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk );
@@ -599,7 +604,7 @@ extern void               Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * v
 extern int                Abc_NodeDeref_rec( Abc_Obj_t * pNode );
 extern int                Abc_NodeRef_rec( Abc_Obj_t * pNode );
 /*=== abcRenode.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple );
+extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
 extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
 /*=== abcSat.c ==========================================================*/
 extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose );
@@ -698,10 +703,16 @@ extern Vec_Int_t *        Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
 extern Vec_Int_t *        Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
+/*=== abcVerify.c ==========================================================*/
+extern int *              Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
+extern int *              Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
 
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
+#ifdef __cplusplus
+}
+#endif
 
 #endif
 
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////

src/base/abc/abcAig.c

@@ -295,6 +295,7 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
     // create the cuts if defined
 //    if ( pAnd->pNtk->pManCut )
 //        Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
+    pAnd->pCopy = NULL;
     return pAnd;
 }
 
@@ -331,6 +332,7 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t *
     // create the cuts if defined
 //    if ( pAnd->pNtk->pManCut )
 //        Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
+    pAnd->pCopy = NULL;
     return pAnd;
 }
 

src/base/abc/abcFunc.c

@@ -195,20 +195,25 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
 
   Synopsis    [Converts the network from BDD to SOP representation.]
 
-  Description []
+  Description [If the flag is set to 1, forces the direct phase of all covers.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
+int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
 {
     Abc_Obj_t * pNode;
     DdManager * dd = pNtk->pManFunc;
     DdNode * bFunc;
     Vec_Str_t * vCube;
-    int i;
+    int i, fMode;
+
+    if ( fDirect )
+        fMode = 1;
+    else
+        fMode = -1;
 
     assert( Abc_NtkIsBddLogic(pNtk) ); 
     Cudd_zddVarsFromBddVars( dd, 2 );
@@ -223,7 +228,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
     {
         assert( pNode->pData );
         bFunc = pNode->pData;
-        pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, -1 );
+        pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, fMode );
         if ( pNode->pData == NULL )
         {
             Vec_StrFree( vCube );

src/base/abc/abcInt.h

@@ -43,10 +43,10 @@
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
 

src/base/abc/abcNames.c

@@ -290,6 +290,39 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the name arrays.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) );
+    assert( Abc_NtkPoNum(pNtk) * 2 == Abc_NtkPoNum(pNtkNew) );
+    assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) );
+    assert( st_count(pNtk->tObj2Name) > 0 );
+    assert( st_count(pNtkNew->tObj2Name) == 0 );
+    // copy the CI/CO names if given
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i),    Abc_ObjName(pObj) );
+    Abc_NtkForEachPo( pNtk, pObj, i ) 
+    {
+        Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+0),    Abc_ObjName(pObj), "_pos" );
+        Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+1),    Abc_ObjName(pObj), "_neg" );
+    }
+    if ( !Abc_NtkIsSeq(pNtk) )
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Gets fanin node names.]
 
   Description []

src/base/abc/abcNetlist.c

@@ -83,7 +83,7 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect )
 {
     Abc_Ntk_t * pNtkNew, * pNtkTemp; 
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) );
@@ -101,7 +101,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
     }
     else if ( Abc_NtkIsBddLogic(pNtk) )
     {
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, fDirect);
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
         Abc_NtkSopToBdd(pNtk);
     }
@@ -157,7 +157,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
     assert( Abc_NtkLogicHasSimpleCos(pNtk) );
 
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk,0);
 
     // start the netlist by creating PI/PO/Latch objects
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, pNtk->ntkFunc );
@@ -220,7 +220,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
             Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy );
     // duplicate EXDC 
     if ( pNtk->pExdc )
-        pNtkNew->pExdc = Abc_NtkLogicToNetlist( pNtk->pExdc );
+        pNtkNew->pExdc = Abc_NtkLogicToNetlist( pNtk->pExdc, 0 );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkLogicSopToNetlist(): Network check has failed.\n" );
     return pNtkNew;

src/base/abc/abcNtk.c

@@ -148,6 +148,64 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
 
 /**Function*************************************************************
 
+  Synopsis    [Starts a new network using existing network as a model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pObjNew;
+    int i;
+    if ( pNtk == NULL )
+        return NULL;
+    // start the network
+    pNtkNew = Abc_NtkAlloc( Type, Func );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkNew->pSpec = NULL;
+    // clean the node copy fields
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+    // map the constant nodes
+    if ( Abc_NtkConst1(pNtk) )
+        Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew);
+    // clone the PIs/POs/latches
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        Abc_NtkDupObj(pNtkNew, pObj);
+        pObjNew = pObj->pCopy;
+        Abc_NtkDupObj(pNtkNew, pObj);
+        // connect second to the first
+        pObjNew->pCopy = pObj->pCopy;
+        // collect first to old
+        pObj->pCopy = pObjNew;
+    }
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        pObjNew = Abc_NtkDupObj(pNtkNew, pObj);
+        Vec_PtrPush( pNtkNew->vCis, pObjNew );
+        Vec_PtrPush( pNtkNew->vCos, pObjNew );
+    }
+    // transfer the names
+    Abc_NtkDupCioNamesTableDual( pNtk, pNtkNew );
+//    Abc_ManTimeDup( pNtk, pNtkNew );
+    // check that the CI/CO/latches are copied correctly
+    assert( Abc_NtkCiNum(pNtk)    == Abc_NtkCiNum(pNtkNew) );
+    assert( Abc_NtkCoNum(pNtk)* 2 == Abc_NtkCoNum(pNtkNew) );
+    assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Finalizes the network using the existing network as a model.]
 
   Description []

src/base/abc/abcObj.c

@@ -227,7 +227,18 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     {
         pNtk->nLatches--;
     }
-    else 
+    else if ( Abc_ObjIsPo(pObj) )
+    {
+        assert( Abc_NtkPoNum(pObj->pNtk) == 1 );
+        Vec_PtrRemove( pObj->pNtk->vCos, pObj );
+        pObj->pNtk->nPos--;
+        // add the name to the table
+        if ( !stmm_delete( pObj->pNtk->tObj2Name, (char **)&pObj, NULL ) )
+        {
+            assert( 0 ); // the PO is not in the table
+        }
+    }
+    else
         assert( 0 );
     // recycle the net itself
     Abc_ObjRecycle( pObj );

src/base/abci/abcAuto.c

@@ -51,7 +51,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
     int nOutputs, nInputs, i;
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
         return;
 
     // get information about the network

src/base/abci/abcClpBdd.c

@@ -25,6 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkFromGlobalBddsDual( Abc_Ntk_t * pNtk );
 static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc );
 
 ////////////////////////////////////////////////////////////////////////
@@ -42,20 +43,23 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose )
 {
     Abc_Ntk_t * pNtkNew;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0) == NULL )
         return NULL;
     if ( fVerbose )
         printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
 
     // create the new network
-    pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
+    if ( fDualRail )
+        pNtkNew = Abc_NtkFromGlobalBddsDual( pNtk );
+    else
+        pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
     Abc_NtkFreeGlobalBdds( pNtk );
     if ( pNtkNew == NULL )
     {
@@ -127,6 +131,42 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromGlobalBddsDual( Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pNodeNew;
+    DdManager * dd = pNtk->pManGlob;
+    int i;
+    // start the new network
+    pNtkNew = Abc_NtkStartFromDual( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    // make sure the new manager has the same number of inputs
+    Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 );
+    // process the POs
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Cudd_Not( Vec_PtrEntry(pNtk->vFuncsGlob, i) ) );
+        Abc_ObjAddFanin( pNode->pCopy->pCopy, pNodeNew );
+        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) );
+        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+    }
+    Extra_ProgressBarStop( pProgress );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the network with the given global BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc )
 {
     Abc_Obj_t * pNodeNew, * pTemp;

src/base/abci/abcCut.c

@@ -57,41 +57,6 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
 
     assert( Abc_NtkIsStrash(pNtk) );
-/*
-    if ( pParams->fMulti )
-    {
-        Abc_Obj_t * pNode, * pNodeA, * pNodeB, * pNodeC;
-        int nFactors;
-        // lebel the nodes, which will be the roots of factor-cuts
-        // mark the multiple-fanout nodes
-        Abc_AigForEachAnd( pNtk, pNode, i )
-            if ( pNode->vFanouts.nSize > 1 )
-                pNode->fMarkB = 1;
-        // unmark the control inputs of MUXes and inputs of EXOR gates
-        Abc_AigForEachAnd( pNtk, pNode, i )
-        {
-            if ( !Abc_NodeIsMuxType(pNode) )
-                continue;
-
-            pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeA, &pNodeB );
-            // if real children are used, skip
-            if ( Abc_ObjFanin0(pNode)->vFanouts.nSize > 1 || Abc_ObjFanin1(pNode)->vFanouts.nSize > 1 )
-                continue;
-
-            if ( pNodeC->vFanouts.nSize == 2 )
-                pNodeC->fMarkB = 0;
-            if ( Abc_ObjRegular(pNodeA) == Abc_ObjRegular(pNodeB) && Abc_ObjRegular(pNodeA)->vFanouts.nSize == 2 )
-                Abc_ObjRegular(pNodeA)->fMarkB = 0;
-       }
-        // mark the PO drivers
-//        Abc_NtkForEachCo( pNtk, pNode, i )
-//            Abc_ObjFanin0(pNode)->fMarkB = 1;
-        nFactors = 0;
-        Abc_AigForEachAnd( pNtk, pNode, i )
-            nFactors += pNode->fMarkB;
-        printf( "Total nodes = %6d.  Total factors = %6d.\n", Abc_NtkNodeNum(pNtk), nFactors );
-    }
-*/
     // start the manager
     pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
     p = Cut_ManStart( pParams );
@@ -135,13 +100,6 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     }
     Vec_PtrFree( vNodes );
     Vec_IntFree( vChoices );
-/*
-    if ( pParams->fMulti )
-    {
-        Abc_NtkForEachObj( pNtk, pNode, i )
-            pNode->fMarkB = 0;
-    }
-*/
 PRT( "Total", clock() - clk );
 //Abc_NtkPrintCuts_( p, pNtk, 0 );
 //    Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );

src/base/abci/abcDsd.c

@@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
     assert( Abc_NtkIsStrash(pNtk) );
 
     // perform FPGA mapping
-    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
         return NULL;
     if ( fVerbose )
         printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );

src/base/abci/abcEspresso.c

@@ -54,7 +54,7 @@ void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose )
     if ( Abc_NtkHasMapping(pNtk) )
         Abc_NtkUnmap(pNtk);
     else if ( Abc_NtkHasBdd(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
     // minimize SOPs of all nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
         if ( i ) Abc_NodeEspresso( pNode );

src/base/abci/abcFxu.c

@@ -57,7 +57,7 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
     if ( Abc_NtkIsMappedLogic(pNtk) )
         Abc_NtkUnmap(pNtk);
     else if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
     else
     { // to make sure the SOPs are SCC-free
 //        Abc_NtkSopToBdd(pNtk);

src/base/abci/abcMap.c

@@ -521,8 +521,8 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
 
     // duplicate the network
     pNtkNew2 = Abc_NtkDup( pNtk );
-    pNtkNew  = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1 );
-    Abc_NtkBddToSop( pNtkNew );
+    pNtkNew  = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1, 0 );
+    Abc_NtkBddToSop( pNtkNew, 0 );
 
     // set the old network to point to the new network
     Abc_NtkForEachCi( pNtk, pNode, i )

src/base/abci/abcMiter.c

@@ -414,7 +414,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
 
 /**Function*************************************************************
 
-  Synopsis    [Derives the miter of two cofactors of one output.]
+  Synopsis    [Quantifies all the PIs existentially from the only PO of the network.]
 
   Description []
                
@@ -470,7 +470,7 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter )
             if ( !Abc_ObjIsComplement(pChild) )
             {
                 // if the miter is constant 1, return immediately
-                printf( "MITER IS CONSTANT 1!\n" );
+//                printf( "MITER IS CONSTANT 1!\n" );
                 return 0;
             }
         }

src/base/abci/abcNewAig.c

@@ -65,7 +65,7 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk )
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );

src/base/abci/abcNtbdd.c

@@ -27,7 +27,7 @@
 static void        Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node );
-static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode );
+static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -243,7 +243,7 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
+DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly )
 {
     int fReorder = 1;
     ProgressBar * pProgress;
@@ -276,10 +276,10 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
         Abc_NtkForEachLatch( pNtk, pNode, i )
         {
             Extra_ProgressBarUpdate( pProgress, i, NULL );
-            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) );
+            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax );
             if ( bFunc == NULL )
             {
-                printf( "Constructing global BDDs timed out.\n" );
+                printf( "Constructing global BDDs is aborted.\n" );
                 Extra_ProgressBarStop( pProgress );
                 Cudd_Quit( dd );
                 return NULL;
@@ -296,10 +296,10 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
         Abc_NtkForEachCo( pNtk, pNode, i )
         {
             Extra_ProgressBarUpdate( pProgress, i, NULL );
-            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) );
+            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax );
             if ( bFunc == NULL )
             {
-                printf( "Constructing global BDDs timed out.\n" );
+                printf( "Constructing global BDDs is aborted.\n" );
                 Extra_ProgressBarStop( pProgress );
                 Cudd_Quit( dd );
                 return NULL;
@@ -339,21 +339,25 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode )
+DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax )
 {
     DdNode * bFunc, * bFunc0, * bFunc1;
     assert( !Abc_ObjIsComplement(pNode) );
-    if ( Cudd_ReadKeys(dd) > 5000000 )
+    if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
+    {
+        printf( "The number of live nodes reached %d.\n", nBddSizeMax );
+        fflush( stdout );
         return NULL;
+    }
     // if the result is available return
     if ( pNode->pCopy )
         return (DdNode *)pNode->pCopy;
     // compute the result for both branches
-    bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0) ); 
+    bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax ); 
     if ( bFunc0 == NULL )
         return NULL;
     Cudd_Ref( bFunc0 );
-    bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1) ); 
+    bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax ); 
     if ( bFunc1 == NULL )
         return NULL;
     Cudd_Ref( bFunc1 );
@@ -423,7 +427,7 @@ double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
     Vec_PtrForEachEntry( vNodes, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)dd->vars[i];
     // build the BDD of the cone
-    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR );  Cudd_Ref( bFunc );
+    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000 );  Cudd_Ref( bFunc );
     bFunc = Cudd_NotCond( bFunc, pNode != pNodeR );
     // count minterms
     Result = Cudd_CountMinterm( dd, bFunc, dd->size );

src/base/abci/abcPrint.c

@@ -644,7 +644,7 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
 
     // get hold of the SOP of the node
     CountConst = CountBuf = CountInv = CountAnd = CountOr = CountOther = CounterTotal = 0;

src/base/abci/abcProve.c

@@ -29,7 +29,7 @@ extern int  Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, i
 extern int  Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
 
-static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue );
+static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails );
 static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
@@ -53,8 +53,8 @@ static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fV
 int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose )
 {
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2;
-    int nConfs, nImps, nBTLimit, RetValue;
+    int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2;  // was 5000
+    int nConfs, nImps, nBTLimit, RetValue, nSatFails;
     int nIter = 0, clk, timeStart = clock();
 
     // get the starting network
@@ -85,7 +85,10 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU
         nIter++;
 
         if ( fVerbose )
+        {
             printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter, nConfs, nBTLimit );
+            fflush( stdout );
+        }
 
         // try brute-force SAT
         clk = clock();
@@ -116,25 +119,30 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU
         {
             // try FRAIGing
             clk = clock();
-            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue );  Abc_NtkDelete( pNtkTemp );
+            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue, &nSatFails );  Abc_NtkDelete( pNtkTemp );
             Abc_NtkMiterPrint( pNtk, "FRAIGing   ", clk, fVerbose );
+//            printf( "NumFails = %d\n", nSatFails );
             if ( RetValue >= 0 )
                 break;
         }
+        else
+            nSatFails = 1000;
 
         // increase resource limits
-        nConfs   = ABC_MIN( nConfs * 3 / 2, 1000000000 );
+//        nConfs   = ABC_MIN( nConfs * 3 / 2, 1000000000 );   // was 4/2
+        nConfs   = nSatFails * nBTLimit / 2;   
         nImps    = ABC_MIN( nImps  * 3 / 2, 1000000000 );
         nBTLimit = ABC_MIN( nBTLimit * 8,   1000000000 );
 
         // timeout at 5 minutes
-        if ( clock() - timeStart >= 300 * CLOCKS_PER_SEC )
-            break;
-        if ( nIter == 4 )
+//        if ( clock() - timeStart >= 1200 * CLOCKS_PER_SEC )
+//            break;
+        if ( nIter == 7 )
             break;
     }    
-    while ( (nConfLimit == 0 || nConfs <= nConfLimit) && 
-            (nImpLimit  == 0 || nImps  <= nImpLimit ) );
+//    while ( (nConfLimit == 0 || nConfs <= nConfLimit) && 
+//            (nImpLimit  == 0 || nImps  <= nImpLimit ) );
+    while ( 1 );
 
     // try to prove it using brute force SAT
     if ( RetValue < 0 )
@@ -144,6 +152,12 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
     }
 
+    // assign the model if it was proved by rewriting (const 1 miter)
+    if ( RetValue == 0 && pNtk->pModel == NULL )
+    {
+        pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
+        memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) );
+    }
     *ppNtk = pNtk;
     return RetValue;
 }
@@ -159,7 +173,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue )
+Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails )
 {
     Abc_Ntk_t * pNtkNew;
     Fraig_Params_t Params, * pParams = &Params;
@@ -190,19 +204,24 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue )
     Fraig_ManProveMiter( pMan );
     RetValue = Fraig_ManCheckMiter( pMan );
 
+    // create the network 
+    pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
+
     // save model
     if ( RetValue == 0 )
     {
         pModel = Fraig_ManReadModel( pMan );
-        FREE( pNtk->pModel );
-        pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
-        memcpy( pNtk->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtk) );
+        FREE( pNtkNew->pModel );
+        pNtkNew->pModel = ALLOC( int, Abc_NtkCiNum(pNtkNew) );
+        memcpy( pNtkNew->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtkNew) );
     }
-    // create the network 
-    pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
+
+    // save the return values
+    *pRetValue = RetValue;
+    *pNumFails = Fraig_ManReadSatFails( pMan );
+
     // delete the fraig manager
     Fraig_ManFree( pMan );
-    *pRetValue = RetValue;
     return pNtkNew;
 }
 

src/base/abci/abcReconv.c

@@ -489,18 +489,20 @@ void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
+DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
 {
+    Abc_Obj_t * pNode;
     DdNode * bFunc0, * bFunc1, * bFunc;
     int i;
     // get the nodes in the cut without fanins in the DFS order
-    Abc_NodeConeCollect( &pNode, 1, vLeaves, vVisited, 0 );
+    Abc_NodeConeCollect( &pRoot, 1, vLeaves, vVisited, 0 );
     // set the elementary BDDs
     Vec_PtrForEachEntry( vLeaves, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)pbVars[i];
     // compute the BDDs for the collected nodes
     Vec_PtrForEachEntry( vVisited, pNode, i )
     {
+        assert( !Abc_ObjIsPi(pNode) );
         bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
         bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
         bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );    Cudd_Ref( bFunc );

src/base/abci/abcRenode.c

@@ -33,6 +33,7 @@ static void        Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nF
 static void        Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk );
 static void        Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh );
 static void        Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk );
+static void        Abc_NtkRenodeSetBoundsFactor( Abc_Ntk_t * pNtk );
 static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
 
 ////////////////////////////////////////////////////////////////////////
@@ -50,7 +51,7 @@ static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple )
+Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor )
 {
     Abc_Ntk_t * pNtkNew;
 
@@ -69,6 +70,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
         Abc_NtkRenodeSetBoundsMulti( pNtk, nThresh );
     else if ( fSimple )
         Abc_NtkRenodeSetBoundsSimple( pNtk );
+    else if ( fFactor )
+        Abc_NtkRenodeSetBoundsFactor( pNtk );
     else
         Abc_NtkRenodeSetBounds( pNtk, nThresh, nFaninMax );
 
@@ -564,6 +567,32 @@ void Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Sets a factor-cut boundary.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRenodeSetBoundsFactor( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    // make sure the mark is not set
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        assert( pNode->fMarkA == 0 );
+    // mark the nodes where expansion stops using pNode->fMarkA
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->fMarkA = (pNode->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pNode));
+    // mark the PO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjFanin0(pNode)->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collects the fanins of a large node.]
 
   Description []

src/base/abci/abcRestruct.c

@@ -332,9 +332,15 @@ Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_C
             return NULL;
         Vec_PtrPush( p->vLeaves, pLeaf );
     }
+
+    if ( pRoot->Id == 29 )
+    {
+        int x = 0;
+    }
+
 clk = clock();
     // collect the internal nodes of the cut
-    Abc_NodeConeCollect( &pRoot, 1, p->vLeaves, p->vVisited, 0 );
+//    Abc_NodeConeCollect( &pRoot, 1, p->vLeaves, p->vVisited, 0 );
     // derive the BDD of the cut
     bFunc = Abc_NodeConeBdd( p->dd, p->dd->vars, pRoot, p->vLeaves, p->vVisited );  Cudd_Ref( bFunc );
 p->timeBdd += clock() - clk;

src/base/abci/abcSat.c

@@ -400,6 +400,10 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
 
     assert( Abc_NtkIsStrash(pNtk) );
 
+    // clean the CI node pointers
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = NULL;
+
     // start the data structures
     vNodes = Vec_PtrAlloc( 1000 );   // the nodes corresponding to vars in the solver
     vSuper = Vec_PtrAlloc( 100 );    // the nodes belonging to the given implication supergate

src/base/abci/abcStrash.c

@@ -58,7 +58,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
@@ -108,7 +108,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     assert( Abc_NtkIsStrash(pNtk1) );
     assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); 
     if ( Abc_NtkIsBddLogic(pNtk2) )
-        Abc_NtkBddToSop(pNtk2);
+        Abc_NtkBddToSop(pNtk2, 0);
     // check that the networks have the same PIs
     // reorder PIs of pNtk2 according to pNtk1
     if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1 ) )

src/base/abci/abcSweep.c

@@ -545,7 +545,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
     while ( nSweptNew );
     // conver back to BDD
     if ( fConvert )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
     // report
     if ( fVerbose )
         printf( "Sweep removed %d nodes.\n", nSwept );

src/base/abci/abcSymm.c

@@ -88,7 +88,7 @@ void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
 
     // compute the global functions
 clk = clock();
-    dd = Abc_NtkGlobalBdds( pNtk, 0 );
+    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 0 );
     Cudd_AutodynDisable( dd );
     Cudd_zddVarsFromBddVars( dd, 2 );
 clkBdd = clock() - clk;

src/base/abci/abcUnate.c

@@ -73,7 +73,7 @@ void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose )
     int clkBdd, clkUnate;
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
         return;
 clkBdd = clock() - clk;
 

src/base/abci/abcUnreach.c

@@ -58,7 +58,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     }
 
     // compute the global BDDs of the latches
-    dd = Abc_NtkGlobalBdds( pNtk, 1 );    
+    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 1 );    
     if ( dd == NULL )
         return 0;
     if ( fVerbose )
@@ -331,7 +331,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
 
     // transform the network to the SOP representation
-    Abc_NtkBddToSop( pNtkNew );
+    Abc_NtkBddToSop( pNtkNew, 0 );
     return pNtkNew;
 }
 

src/base/abci/abcVanEijk.c

@@ -713,7 +713,7 @@ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit )
 Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;
+    Abc_Obj_t * pClass, * pNode, * pRepr, * pObj, *pObjNew;
     Abc_Obj_t * pMiter, * pTotal;
     Vec_Ptr_t * vCone;
     int i, k;
@@ -766,6 +766,30 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
         pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter );
     }
 
+/*
+    // create the only PO
+    pObjNew = Abc_NtkCreatePo( pNtkNew );
+    // add the PO name
+    Abc_NtkLogicStoreName( pObjNew, "DC" );
+    // add the PO
+    Abc_ObjAddFanin( pObjNew, pTotal );
+
+    // quontify the PIs existentially
+    pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew );
+
+    // get the new PO
+    pObjNew = Abc_NtkPo( pNtkNew, 0 );
+    // remember the miter output
+    pTotal = Abc_ObjChild0( pObjNew );
+    // remove the PO
+    Abc_NtkDeleteObj( pObjNew );
+
+    // make the old network point to the new things
+    Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = Abc_NtkPi( pNtkNew, i );
+*/
+
     // for each CO, create PO (skip POs equal to CIs because of name conflict)
     Abc_NtkForEachPo( pNtk, pObj, i )
         if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )

src/base/abci/abcVanImp.c

@@ -870,7 +870,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I
 {
     Abc_Ntk_t * pNtkNew; 
     Vec_Ptr_t * vCone;
-    Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2;
+    Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2, * pObjNew;
     unsigned Imp;
     int i, k;
 
@@ -942,6 +942,29 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I
         pMiter = Abc_AigAnd( pNtkNew->pManFunc, pNode1->pCopy, Abc_ObjNot(pNode2->pCopy) );
         pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter );
     }
+/*
+    // create the only PO
+    pObjNew = Abc_NtkCreatePo( pNtkNew );
+    // add the PO name
+    Abc_NtkLogicStoreName( pObjNew, "DC" );
+    // add the PO
+    Abc_ObjAddFanin( pObjNew, pTotal );
+
+    // quontify the PIs existentially
+    pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew );
+
+    // get the new PO
+    pObjNew = Abc_NtkPo( pNtkNew, 0 );
+    // remember the miter output
+    pTotal = Abc_ObjChild0( pObjNew );
+    // remove the PO
+    Abc_NtkDeleteObj( pObjNew );
+
+    // make the old network point to the new things
+    Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = Abc_NtkPi( pNtkNew, i );
+*/
 
     // for each CO, create PO (skip POs equal to CIs because of name conflict)
     Abc_NtkForEachPo( pNtk, pObj, i )

src/base/abci/abcVerify.c

@@ -26,8 +26,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
-static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
-static int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
 static void  Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel );
 static void  Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
 
@@ -78,7 +76,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // convert the miter into a CNF
-    pCnf = Abc_NtkRenode( pMiter, 0, 100, 1, 0, 0 );
+    pCnf = Abc_NtkRenode( pMiter, 0, 100, 1, 0, 0, 0 );
     Abc_NtkDelete( pMiter );
     if ( pCnf == NULL )
     {
@@ -235,7 +233,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // convert the miter into a CNF
-    pCnf = Abc_NtkRenode( pFrames, 0, 100, 1, 0, 0 );
+    pCnf = Abc_NtkRenode( pFrames, 0, 100, 1, 0, 0, 0 );
     Abc_NtkDelete( pFrames );
     if ( pCnf == NULL )
     {

src/base/abci/module.make

@@ -19,6 +19,8 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcRefactor.c \
     src/base/abci/abcRenode.c \
+    src/base/abci/abcRestruct.c \
+    src/base/abci/abcResub.c \
     src/base/abci/abcRewrite.c \
     src/base/abci/abcSat.c \
     src/base/abci/abcStrash.c \

src/base/cmd/cmd.c

@@ -1252,7 +1252,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // write out the current network
-    pNetlist = Abc_NtkLogicToNetlist(pNtk);
+    pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
     Io_WriteBlif( pNetlist, "_sis_in.blif", 1 );
     Abc_NtkDelete( pNetlist );
 
@@ -1388,7 +1388,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // write out the current network
-    pNetlist = Abc_NtkLogicToNetlist(pNtk);
+    pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
     Io_WriteBlif( pNetlist, "_mvsis_in.blif", 1 );
     Abc_NtkDelete( pNetlist );
 

src/base/cmd/cmd.h

@@ -21,6 +21,10 @@
 #ifndef __CMD_H__
 #define __CMD_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -57,9 +61,13 @@ extern void        Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * v
 /*=== cmdHist.c ========================================================*/
 extern void          Cmd_HistoryAddCommand( Abc_Frame_t * pAbc, char * command );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/base/io/io.c

@@ -45,6 +45,7 @@ static int IoCommandWriteGml    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteList   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -83,6 +84,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_list",    IoCommandWriteList,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_pla",     IoCommandWritePla,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 );
 }
 
 /**Function*************************************************************
@@ -1174,7 +1176,7 @@ int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv )
     if ( Abc_NtkIsSopLogic(pNtk) )
         Abc_NtkLogicMakeDirectSops(pNtk);
     // derive the netlist
-    pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+    pNtkTemp = Abc_NtkLogicToNetlist(pNtk,1);
     if ( pNtkTemp == NULL )
     {
         fprintf( pAbc->Out, "Writing BENCH has failed.\n" );
@@ -1358,6 +1360,12 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
         return 0;
     }
 
+    if ( Abc_NtkGetLevelNum(pNtk) > 1 )
+    {
+        fprintf( pAbc->Out, "PLA writing is available for collapsed networks.\n" );
+        return 0;
+    }
+
     if ( Abc_NtkLatchNum(pNtk) > 0 )
     {
         fprintf( pAbc->Out, "Latches are writed at PI/PO pairs in the PLA file.\n" );
@@ -1368,11 +1376,12 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
     {
         goto usage;
     }
+
     // get the input file name
     FileName = argv[globalUtilOptind];
 
     // derive the netlist
-    pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+    pNtkTemp = Abc_NtkLogicToNetlist(pNtk,1);
     if ( pNtkTemp == NULL )
     {
         fprintf( pAbc->Out, "Writing PLA has failed.\n" );
@@ -1434,7 +1443,7 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
     FileName = argv[globalUtilOptind];
 
     // derive the netlist
-    pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+    pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0);
     if ( pNtkTemp == NULL )
     {
         fprintf( pAbc->Out, "Writing PLA has failed.\n" );
@@ -1452,6 +1461,96 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    Abc_Ntk_t * pNtk;
+    char * FileName;
+    int c;
+    int fNames;
+
+    fNames = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'n':
+                fNames ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    pNtk = pAbc->pNtkCur;
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+
+    if ( pNtk->pModel == NULL )
+    {
+        fprintf( pAbc->Out, "Counter-example is not available.\n" );
+        return 0;
+    }
+
+    // write the counter-example into the file
+    {
+        Abc_Obj_t * pObj;
+        FILE * pFile = fopen( FileName, "w" );
+        int i;
+        if ( pFile == NULL )
+        {
+            fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", FileName );
+            return 1;
+        }
+        if ( fNames )
+        {
+            Abc_NtkForEachPi( pNtk, pObj, i )
+                fprintf( pFile, "%s=%c ", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) );
+        }
+        else
+        {
+            Abc_NtkForEachPi( pNtk, pObj, i )
+                fprintf( pFile, "%c", '0'+(pNtk->pModel[i]==1) );
+        }
+        fprintf( pFile, "\n" );
+        fclose( pFile );
+    }
+
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_counter [-nh] <file>\n" );
+    fprintf( pAbc->Err, "\t         writes the counter-example derived by \"prove\" or \"sat\"\n" );
+    fprintf( pAbc->Err, "\t         the file contains values for each PI in the natural order\n" );
+    fprintf( pAbc->Err, "\t-n     : write input names into the file [default = %s]\n", fNames? "yes": "no" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/io/io.h

@@ -21,6 +21,10 @@
 #ifndef __IO_H__
 #define __IO_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -94,9 +98,13 @@ extern int                Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteVerilog.c ==========================================================*/
 extern void               Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/base/io/ioInt.h

@@ -41,9 +41,9 @@
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/base/io/ioWriteBlif.c

@@ -53,7 +53,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
 {
     Abc_Ntk_t * pNtkTemp;
     // derive the netlist
-    pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+    pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0);
     if ( pNtkTemp == NULL )
     {
         fprintf( stdout, "Writing BLIF has failed.\n" );

src/base/io/ioWriteDot.c

@@ -412,7 +412,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
 
     // mark the nodes from the set
     Vec_PtrForEachEntry( vNodes, pNode, i )

src/base/io/ioWritePla.c

@@ -88,7 +88,7 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
     nProducts = 0;
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
-        pDriver = Abc_ObjFanin0Ntk(pNode);
+        pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pNode) );
         if ( !Abc_ObjIsNode(pDriver) )
         {
             nProducts++;
@@ -138,9 +138,10 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
         pCubeOut[i] = '1';
 
         // consider special cases of nodes
-        pDriver = Abc_ObjFanin0Ntk(pNode);
+        pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pNode) );
         if ( !Abc_ObjIsNode(pDriver) )
         {
+            assert( Abc_ObjIsCi(pDriver) );
             pCubeIn[(int)pDriver->pCopy] = '1' - Abc_ObjFaninC0(pNode);
             fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut );
             pCubeIn[(int)pDriver->pCopy] = '-';
@@ -152,17 +153,29 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
                 fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut );
             continue;
         }
+
+        // make sure the cover is not complemented
+        assert( !Abc_SopIsComplement( pDriver->pData ) );
+
         // write the cubes
         nFanins = Abc_ObjFaninNum(pDriver);
         Abc_SopForEachCube( pDriver->pData, nFanins, pCube )
         {
             Abc_ObjForEachFanin( pDriver, pFanin, k )
+            {
+                pFanin = Abc_ObjFanin0Ntk(pFanin);
+                assert( (int)pFanin->pCopy < nInputs );
                 pCubeIn[(int)pFanin->pCopy] = pCube[k];
+            }
             fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut );
         }
         // clean the cube for future writing
         Abc_ObjForEachFanin( pDriver, pFanin, k )
+        {
+            pFanin = Abc_ObjFanin0Ntk(pFanin);
+            assert( Abc_ObjIsCi(pFanin) );
             pCubeIn[(int)pFanin->pCopy] = '-';
+        }
         Extra_ProgressBarUpdate( pProgress, i, NULL );
     }
     Extra_ProgressBarStop( pProgress );
@@ -171,6 +184,8 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
     // clean the CI nodes
     Abc_NtkForEachCi( pNtk, pNode, i )
         pNode->pCopy = NULL;
+    free( pCubeIn );
+    free( pCubeOut );
     return 1;
 }
 

src/base/main/main.h

@@ -21,6 +21,10 @@
 #ifndef __MAIN_H__
 #define __MAIN_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         TYPEDEFS                                 ///
 ////////////////////////////////////////////////////////////////////////
@@ -104,8 +108,12 @@ extern void            Abc_FrameSetLibGen( void * pLib );
 extern void            Abc_FrameSetLibSuper( void * pLib );      
 extern void            Abc_FrameSetFlag( char * pFlag, char * pValue );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif

src/base/main/mainInt.h

@@ -102,8 +102,8 @@ extern void            Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
 extern void            Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
 extern void            Abc_UtilsSource( Abc_Frame_t * pAbc );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif

src/base/seq/seq.h

@@ -21,6 +21,10 @@
 #ifndef __SEQ_H__
 #define __SEQ_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -82,9 +86,13 @@ extern int             Seq_MapComputeAreaFlows( Abc_Ntk_t * pNtk, int fVerbose )
 extern Vec_Ptr_t *     Seq_NtkReachNodes( Abc_Ntk_t * pNtk, int fFromPos );
 extern int             Seq_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/base/seq/seqInt.h

@@ -21,6 +21,10 @@
 #ifndef __SEQ_INT_H__
 #define __SEQ_INT_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -240,9 +244,13 @@ extern int                   Seq_ObjFanoutLMin( Abc_Obj_t * pObj );
 extern int                   Seq_ObjFanoutLSum( Abc_Obj_t * pObj );
 extern int                   Seq_ObjFaninLSum( Abc_Obj_t * pObj );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/base/seq/seqRetCore.c

@@ -107,7 +107,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
 
     // start the network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );

src/bdd/dsd/dsd.h

@@ -28,6 +28,10 @@
 #ifndef __DSD_H__
 #define __DSD_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                      TYPEDEF DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -114,8 +118,12 @@ extern void            Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode );
 /*=== dsdLocal.c =======================================================*/
 extern DdNode *        Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                           END OF FILE                            ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
\ No newline at end of file

src/bdd/dsd/dsdInt.h

@@ -83,9 +83,9 @@ extern void         Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode );
 extern void         Dsd_TreeUnmark( Dsd_Manager_t * dMan );
 extern DdNode *     Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                           END OF FILE                            ///
 ////////////////////////////////////////////////////////////////////////
 
-
-#endif
\ No newline at end of file

src/bdd/parse/parse.h

@@ -47,7 +47,8 @@
 extern DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormula, int nVars, int nRanks, 
       char * ppVarNames[], DdManager * dd, DdNode * pbVars[] );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif

src/bdd/parse/parseInt.h

@@ -67,7 +67,8 @@ extern void               Parse_StackOpPush   ( Parse_StackOp_t * p, int Oper );
 extern int                Parse_StackOpPop    ( Parse_StackOp_t * p );
 extern void               Parse_StackOpFree   ( Parse_StackOp_t * p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif

src/bdd/reo/reo.h

@@ -19,6 +19,10 @@
 #ifndef __REO_H__
 #define __REO_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #include <stdio.h>
 #include <stdlib.h>
 #include "extra.h"
@@ -215,8 +219,12 @@ extern DdNode *   Extra_ReorderCudd( DdManager * dd, DdNode * aFunc, int pPermut
 extern int        Extra_bddReorderTest( DdManager * dd, DdNode * bF ); 
 extern int        Extra_addReorderTest( DdManager * dd, DdNode * aF ); 
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         END OF FILE                              ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif

src/generic.h

@@ -21,6 +21,10 @@
 #ifndef __zzz_H__
 #define __zzz_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -42,10 +46,14 @@
 ////////////////////////////////////////////////////////////////////////
 
 /*=== zzz.c ==========================================================*/
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/map/fpga/fpga.h

@@ -19,6 +19,10 @@
 #ifndef __FPGA_H__
 #define __FPGA_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -153,8 +157,12 @@ extern int             Fpga_ManCheckConsistency( Fpga_Man_t * p );
 extern void            Fpga_ManCleanData0( Fpga_Man_t * pMan );
 extern Fpga_NodeVec_t * Fpga_CollectNodeTfo( Fpga_Man_t * pMan, Fpga_Node_t * pNode );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif

src/map/fpga/fpgaInt.h

@@ -376,8 +376,8 @@ extern void              Fpga_MappingSetChoiceLevels( Fpga_Man_t * pMan );
 /*=== CUDD package.c ===============================================================*/
 extern unsigned int      Cudd_Prime( unsigned int p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif

src/map/fpga/fpgaTruth.c

@@ -94,8 +94,7 @@ void * Fpga_TruthsCutBdd( void * dd, Fpga_Cut_t * pCut )
         Cudd_RecursiveDeref( dd, (DdNode*)pCut->uSign );
         pCut->uSign = 0;
     }
-    printf( "%d ", vVisited->nSize );
-
+//    printf( "%d ", vVisited->nSize );
     Fpga_NodeVecFree( vVisited );
     Cudd_Deref( bFunc );
     return bFunc;

src/map/mapper/mapper.h

@@ -19,6 +19,10 @@
 #ifndef __MAPPER_H__
 #define __MAPPER_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -180,7 +184,12 @@ extern void            Map_ManCleanData( Map_Man_t * p );
 extern void            Map_MappingSetupTruthTables( unsigned uTruths[][2] );
 extern void            Map_MappingSetupTruthTablesLarge( unsigned uTruths[][32] );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif

src/map/mapper/mapperInt.h

@@ -470,8 +470,8 @@ extern void              Map_NodeVecWriteEntry( Map_NodeVec_t * p, int i, Map_No
 extern Map_Node_t *      Map_NodeVecReadEntry( Map_NodeVec_t * p, int i );
 extern void              Map_NodeVecSortByLevel( Map_NodeVec_t * p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif

src/map/mio/mio.h

@@ -19,6 +19,10 @@
 #ifndef __MIO_H__
 #define __MIO_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -133,7 +137,13 @@ extern void              Mio_DeriveGateDelays( Mio_Gate_t * pGate,
                             float * ptDelaysRes, float * ptPinDelayMax );
 extern Mio_Gate_t *      Mio_GateCreatePseudo( int nInputs );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif
+

src/map/mio/mioInt.h

@@ -118,8 +118,8 @@ struct  Mio_PinStruct_t_
 /*=== mioRead.c =============================================================*/
 /*=== mioUtils.c =============================================================*/
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif

src/map/pga/pga.h

@@ -21,6 +21,10 @@
 #ifndef __PGA_H__
 #define __PGA_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -64,9 +68,13 @@ extern Vec_Ptr_t *   Pga_DoMapping( Pga_Man_t * p );
 extern Pga_Man_t *   Pga_ManStart( Pga_Params_t * pParams );
 extern void          Pga_ManStop( Pga_Man_t * p );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/map/pga/pgaInt.h

@@ -124,9 +124,9 @@ extern float       Pga_MappingSetRefsAndArea( Pga_Man_t * p );
 extern float       Pga_MappingGetSwitching( Pga_Man_t * p );
 extern void        Pga_MappingPrintOutputArrivals( Pga_Man_t * p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/map/super/super.h

@@ -19,6 +19,10 @@
 #ifndef __SUPER_H__
 #define __SUPER_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -44,8 +48,13 @@
 ////////////////////////////////////////////////////////////////////////
 
 /*=== superCore.c =============================================================*/
+    
+#ifdef __cplusplus
+}
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif

src/map/super/superInt.h

@@ -55,8 +55,8 @@ extern void       Super2_Precompute( int nInputs, int nLevels, int fVerbose );
 /*=== superGate.c =============================================================*/
 extern void       Super_Precompute( Mio_Library_t * pLibGen, int nInputs, int nLevels, float tDelayMax, float tAreaMax, int TimeLimit, bool fSkipInv, bool fWriteOldFormat, int fVerbose );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif

src/misc/extra/extra.h

@@ -29,6 +29,10 @@
 #ifndef __EXTRA_H__
 #define __EXTRA_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #ifdef _WIN32
 #define inline __inline // compatible with MS VS 6.0
 #endif
@@ -434,4 +438,8 @@ extern int         globalUtilOptind;
 
 /**AutomaticEnd***************************************************************/
 
+#ifdef __cplusplus
+}
+#endif
+
 #endif /* __EXTRA_H__ */

src/misc/mvc/mvc.h

@@ -724,9 +724,9 @@ extern Mvc_Manager_t *  Mvc_ManagerAllocCube( int nWords );
 extern Mvc_Manager_t *  Mvc_ManagerFreeCover( Mvc_Cover_t * pCover );
 extern Mvc_Manager_t *  Mvc_ManagerFreeCube( Mvc_Cover_t * pCube, int nWords );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/misc/st/st.h

@@ -14,6 +14,10 @@
 #ifndef ST_INCLUDED
 #define ST_INCLUDED
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 typedef struct st_table_entry st_table_entry;
 struct st_table_entry {
     char *key;
@@ -85,4 +89,8 @@ extern void st_free_gen (st_generator *);
 
 #define ST_OUT_OF_MEM -10000
 
+#ifdef __cplusplus
+}
+#endif
+
 #endif /* ST_INCLUDED */

src/misc/st/stmm.h

@@ -14,6 +14,10 @@
 #ifndef STMM_INCLUDED
 #define STMM_INCLUDED
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #include "extra.h"
 
 typedef struct stmm_table_entry stmm_table_entry;
@@ -116,4 +120,8 @@ EXTERN void stmm_clean ARGS ((stmm_table *));
 
 */
 
+#ifdef __cplusplus
+}
+#endif
+
 #endif /* STMM_INCLUDED */

src/misc/util/util_hack.h

@@ -21,6 +21,10 @@
 #ifndef __UTIL_HACK_H__
 #define __UTIL_HACK_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
@@ -84,4 +88,8 @@ extern char *      Extra_UtilFileSearch( char *file, char *path, char *mode );
 extern char *      globalUtilOptarg;
 extern int         globalUtilOptind;
 
+#ifdef __cplusplus
+}
+#endif
+
 #endif

src/misc/vec/vec.h

@@ -21,6 +21,10 @@
 #ifndef __VEC_H__
 #define __VEC_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -50,9 +54,13 @@
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/misc/vec/vecInt.h

@@ -696,9 +696,9 @@ static inline void Vec_IntSortUnsigned( Vec_Int_t * p )
             (int (*)(const void *, const void *)) Vec_IntSortCompareUnsigned );
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/misc/vec/vecPtr.h

@@ -529,10 +529,10 @@ static inline void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
             (int (*)(const void *, const void *)) Vec_PtrSortCompare );
 }
 
+#endif
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/misc/vec/vecStr.h

@@ -501,9 +501,9 @@ static inline void Vec_StrSort( Vec_Str_t * p, int fReverse )
                 (int (*)(const void *, const void *)) Vec_StrSortCompare1 );
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/misc/vec/vecVec.h

@@ -256,9 +256,9 @@ static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry )
         Vec_PtrPushUnique( (Vec_Ptr_t*)p->pArray[Level], Entry );
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/opt/cut/cut.h

@@ -21,6 +21,10 @@
 #ifndef __CUT_H__
 #define __CUT_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -133,9 +137,13 @@ extern void             Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node );
 /*=== cutTruth.c ==========================================================*/
 extern void             Cut_TruthCanonicize( Cut_Cut_t * pCut );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/opt/cut/cutInt.h

@@ -141,9 +141,9 @@ extern int                 Cut_TableReadTime( Cut_HashTable_t * pTable );
 /*=== cutTruth.c ==========================================================*/
 extern void                Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/opt/cut/cutList.h

@@ -199,9 +199,9 @@ static inline Cut_Cut_t * Cut_ListFinish( Cut_List_t * p )
     return pHead;
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/opt/dec/dec.h

@@ -21,6 +21,10 @@
 #ifndef __DEC_H__
 #define __DEC_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -699,9 +703,13 @@ static inline Dec_Edge_t Dec_GraphAddNodeMux( Dec_Graph_t * pGraph, Dec_Edge_t e
     return eNode;
 }
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/opt/dec/decAbc.c

@@ -18,7 +18,7 @@
 
 #include "abc.h"
 #include "dec.h"
-#include "aig.h"
+//#include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -214,6 +214,7 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpda
   SeeAlso     []
 
 ***********************************************************************/
+/*
 Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
 {
     Dec_Node_t * pNode;
@@ -235,7 +236,7 @@ Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
     // complement the result if necessary
     return Aig_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
 }
-
+*/
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/opt/fxu/fxu.h

@@ -19,6 +19,10 @@
 #ifndef __FXU_H__
 #define __FXU_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -74,9 +78,13 @@ struct FxuDataStruct
 /*===== fxu.c ==========================================================*/
 extern int          Fxu_FastExtract( Fxu_Data_t * pData );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/opt/fxu/fxuInt.h

@@ -529,8 +529,9 @@ extern int          Fxu_HeapSingleReadMaxWeight( Fxu_HeapSingle * p );
 extern Fxu_Single * Fxu_HeapSingleReadMax( Fxu_HeapSingle * p );
 extern Fxu_Single * Fxu_HeapSingleGetMax( Fxu_HeapSingle * p );  
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         END OF FILE                              ///
 ////////////////////////////////////////////////////////////////////////
-#endif
 

src/opt/rwr/rwr.h

@@ -21,6 +21,10 @@
 #ifndef __RWR_H__
 #define __RWR_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -145,9 +149,13 @@ extern void              Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName );
 extern void              Rwr_ListAddToTail( Rwr_Node_t ** ppList, Rwr_Node_t * pNode );
 extern char *            Rwr_ManGetPractical( Rwr_Man_t * p );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/opt/sim/sim.h

@@ -21,6 +21,10 @@
 #ifndef __SIM_H__
 #define __SIM_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 /*
     The ideas realized in this package are described in the paper:
     "Detecting Symmetries in Boolean Functions using Circuit Representation, 
@@ -217,9 +221,13 @@ extern int             Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWord
 extern void            Sim_UtilCountPairsAll( Sym_Man_t * p );
 extern int             Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/opt/xyz/xyz.h

@@ -18,6 +18,13 @@
 
 ***********************************************************************/
 
+#ifndef __XYZ_H__
+#define __XYZ_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #include "abc.h"
 #include "xyzInt.h"
 
@@ -89,8 +96,15 @@ extern void        Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj );
 /*=== xyzTest.c ===========================================================*/
 extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
 
+

src/sat/aig/aig.h

@@ -21,6 +21,10 @@
 #ifndef __AIG_H__
 #define __AIG_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 /*
     AIG is an And-Inv Graph with structural hashing.
     It is always structurally hashed. It means that at any time:
@@ -358,10 +362,14 @@ extern void                Aig_PatternFill( Aig_Pattern_t * pPat );
 extern int                 Aig_PatternCount( Aig_Pattern_t * pPat );
 extern void                Aig_PatternRandom( Aig_Pattern_t * pPat );
 extern void                Aig_PatternFree( Aig_Pattern_t * pPat );
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-

src/sat/asat/asatmem.h

@@ -70,7 +70,9 @@ extern char *              Asat_MmStepEntryFetch( Asat_MmStep_t * p, int nBytes
 extern void                Asat_MmStepEntryRecycle( Asat_MmStep_t * p, char * pEntry, int nBytes );
 extern int                 Asat_MmStepReadMemUsage( Asat_MmStep_t * p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif
+

src/sat/asat/solver.h

@@ -22,6 +22,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef solver_h
 #define solver_h
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #ifdef _WIN32
 #define inline __inline // compatible with MS VS 6.0
 #endif
@@ -141,5 +145,9 @@ struct solver_t
 
     stats    solver_stats;
 };
+ 
+#ifdef __cplusplus
+}
+#endif
 
 #endif

src/sat/csat/csat_apis.h

@@ -206,12 +206,12 @@ extern void                  ABC_TargetResFree( CSAT_Target_ResultT * p );
 
 extern void CSAT_SetCaller(ABC_Manager mng, enum CSAT_CallerT caller);
 
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
 #ifdef __cplusplus
 }
 #endif
 
 #endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////

src/sat/fraig/fraig.h

@@ -18,7 +18,11 @@
 
 #ifndef __FRAIG_H__
 #define __FRAIG_H__
- 
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -106,6 +110,7 @@ extern int *               Fraig_ManReadModel( Fraig_Man_t * p );
 extern int                 Fraig_ManReadPatternNumRandom( Fraig_Man_t * p );
 extern int                 Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p );
 extern int                 Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p );
+extern int                 Fraig_ManReadSatFails( Fraig_Man_t * p );      
 
 extern void                Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );        
 extern void                Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );      
@@ -208,4 +213,9 @@ extern Fraig_NodeVec_t *   Fraig_CollectSupergate( Fraig_Node_t * pNode, int fSt
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
+ 
+#ifdef __cplusplus
+}
+#endif
+
 #endif

src/sat/fraig/fraigApi.c

@@ -64,6 +64,8 @@ int               Fraig_ManReadPatternNumRandom( Fraig_Man_t * p )            {
 int               Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p )           { return p->iWordStart * 32;  }
 // returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns)
 int               Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p )   { return p->iPatsPerm;        }
+// returns the number of times FRAIG package timed out
+int               Fraig_ManReadSatFails( Fraig_Man_t * p )                    { return p->nSatFails;        }      
 
 /**Function*************************************************************
 

src/sat/fraig/fraigInt.h

@@ -441,8 +441,8 @@ extern int                 Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig
 /*=== fraigVec.c ===============================================================*/
 extern void                Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif

src/sat/msat/msat.h

@@ -21,6 +21,10 @@
 #ifndef __MSAT_H__
 #define __MSAT_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -154,8 +158,13 @@ extern double           Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p );
 extern int              Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit );  
 extern int              Msat_VarHeapReadMax( Msat_VarHeap_t * p );  
 extern int              Msat_VarHeapGetMax( Msat_VarHeap_t * p );  
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif

src/sat/msat/msatSolverCore.c

@@ -176,7 +176,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
         nConflictsLimit *= 1.5;
         nLearnedLimit   *= 1.1;
         // if the limit on the number of backtracks is given, quit the restart loop
-        if ( nBackTrackLimit > 0 )
+        if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
             break;
         // if the runtime limit is exceeded, quit the restart loop
         if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )

src/sat/msat/msatSolverSearch.c

@@ -599,7 +599,7 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi
                 Msat_SolverCancelUntil( p, p->nLevelRoot );
                 return MSAT_UNKNOWN; 
             }
-            else if ( nBackTrackLimit > 0 && nConfs > nBackTrackLimit ) {
+            else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) {
                 // Reached bound on number of conflicts:
                 Msat_QueueClear( p->pQueue );
                 Msat_SolverCancelUntil( p, p->nLevelRoot );