Fixing time primtouts throughout the code.

10 files changed, 14 insertions, 12 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index c25c6e48..723a7dd7 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -23,6 +23,7 @@
 #include "src/sat/cnf/cnf.h"
 #include "src/sat/bsat/satSolver2.h"
 #include "src/base/main/main.h"
+#include "src/aig/saig/saig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -187,7 +188,7 @@ Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPi
 int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose )
 {
     extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
-    extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
+//    extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
     int fAddOneLayer = 1;
     Abc_Cex_t * pCexNew = NULL;
     Gia_Man_t * pAbs;
diff --git a/src/aig/ivy/ivyFastMap.c b/src/aig/ivy/ivyFastMap.c
index feeb36f2..34d2796e 100644
--- a/src/aig/ivy/ivyFastMap.c
+++ b/src/aig/ivy/ivyFastMap.c
@@ -84,7 +84,7 @@ static int  Ivy_FastMapNodeDeref( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
 
 
 extern clock_t s_MappingTime;
-extern clock_t s_MappingMem;
+extern int s_MappingMem;
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index c0f97530..afedabc2 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -37,10 +37,10 @@ ABC_NAMESPACE_IMPL_START
 //extern int s_TotalNodes = 0;
 //extern int s_TotalChanges = 0;
 
-int s_MappingTime = 0;
+clock_t s_MappingTime = 0;
 int s_MappingMem = 0;
-int s_ResubTime = 0;
-int s_ResynTime = 0;
+clock_t s_ResubTime = 0;
+clock_t s_ResynTime = 0;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index 6e2b95c3..8ae4795a 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -117,7 +117,7 @@ static Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required );
 static Vec_Ptr_t *   Abc_CutFactorLarge( Abc_Obj_t * pNode, int nLeavesMax );
 static int           Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
 
-extern int s_ResubTime;
+extern clock_t s_ResubTime;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index e7e8cff3..eff37870 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -684,8 +684,9 @@ char * Io_NtkDeriveSop( Mem_Flex_t * pMem, word uTruth, int nVars, Vec_Int_t * v
     // check the case of constant cover
     if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
     {
+        char * pStr0 = " 0\n", * pStr1 = " 1\n";
         assert( RetValue == 0 );
-        return Vec_IntSize(vCover) == 0 ? " 0\n" : " 1\n";
+        return Vec_IntSize(vCover) == 0 ? pStr0 : pStr1;
     }
     // derive the AIG for that tree
     pSop = Abc_SopCreateFromIsop( pMem, nVars, vCover );
diff --git a/src/map/fpga/fpgaCore.c b/src/map/fpga/fpgaCore.c
index 64b26689..987d782f 100644
--- a/src/map/fpga/fpgaCore.c
+++ b/src/map/fpga/fpgaCore.c
@@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START
 static int  Fpga_MappingPostProcess( Fpga_Man_t * p );
 
 extern clock_t s_MappingTime;
-extern clock_t s_MappingMem;
+extern int s_MappingMem;
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index 0ddfafd6..f42c29eb 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -27,7 +27,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern int s_MappingTime;
+extern clock_t s_MappingTime;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c
index d34cf538..37c98f0d 100644
--- a/src/map/if/ifSeq.c
+++ b/src/map/if/ifSeq.c
@@ -27,7 +27,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern int s_MappingTime;
+extern clock_t s_MappingTime;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index acb8542c..7d681299 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -76,7 +76,7 @@ struct Res_Man_t_
 
 extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
 
-extern int s_ResynTime;
+extern clock_t s_ResynTime;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c
index 48724136..8badc61d 100644
--- a/src/proof/llb/llb3Nonlin.c
+++ b/src/proof/llb/llb3Nonlin.c
@@ -65,7 +65,7 @@ struct Llb_Mnn_t_
 
 };
 
-extern int timeBuild, timeAndEx, timeOther;
+extern clock_t timeBuild, timeAndEx, timeOther;
 extern int nSuppMax;
 
 ////////////////////////////////////////////////////////////////////////