summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/aig/aig.h12
-rw-r--r--src/sat/asat/asatmem.h4
-rw-r--r--src/sat/asat/solver.h8
-rw-r--r--src/sat/csat/csat_apis.h8
-rw-r--r--src/sat/fraig/fraig.h12
-rw-r--r--src/sat/fraig/fraigApi.c2
-rw-r--r--src/sat/fraig/fraigInt.h4
-rw-r--r--src/sat/msat/msat.h11
-rw-r--r--src/sat/msat/msatSolverCore.c2
-rw-r--r--src/sat/msat/msatSolverSearch.c2
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 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-06 15:26:26 +0000