Version abc60303

10 files changed, 52 insertions, 13 deletions

diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
index c83af527..5d2547ea 100644
--- a/src/sat/aig/aig.h
+++ b/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
-
diff --git a/src/sat/asat/asatmem.h b/src/sat/asat/asatmem.h
index 56115e7d..7351d77b 100644
--- a/src/sat/asat/asatmem.h
+++ b/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
+
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index d798a7a9..62815656 100644
--- a/src/sat/asat/solver.h
+++ b/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
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
index e187845c..d2fa770e 100644
--- a/src/sat/csat/csat_apis.h
+++ b/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                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 4637c030..4e2a295e 100644
--- a/src/sat/fraig/fraig.h
+++ b/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
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index aeea01f1..3b8da17f 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/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*************************************************************
 
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index f5e792eb..890af13c 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/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
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 40028784..94416a5d 100644
--- a/src/sat/msat/msat.h
+++ b/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
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index 091a0c55..397dbcdc 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/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 )
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c
index e594d9c3..4b73d6b3 100644
--- a/src/sat/msat/msatSolverSearch.c
+++ b/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 );