diff options
| -rw-r--r-- | src/base/abci/abc.c | 2 | ||||
| -rw-r--r-- | src/proof/cec/cecSatG3.c | 3 | ||||
| -rw-r--r-- | src/sat/glucose2/AbcGlucose2.cpp | 25 | ||||
| -rw-r--r-- | src/sat/glucose2/AbcGlucose2.h | 1 |
4 files changed, 22 insertions, 9 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 90d85bde..3312ad07 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36999,7 +36999,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs, int approxLim, int subBatchSz, int adaRecycle ); Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp; int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0; - int fUseAlgoG3 = 0, fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500; + int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500; Cec4_ManSetParams( pPars ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxywvh" ) ) != EOF ) diff --git a/src/proof/cec/cecSatG3.c b/src/proof/cec/cecSatG3.c index bdfa0f90..eaad455b 100644 --- a/src/proof/cec/cecSatG3.c +++ b/src/proof/cec/cecSatG3.c @@ -1564,9 +1564,8 @@ void Cec5_ManLoadInstance( Cec5_Man_t * p, int iObj0, int iObj1, int * piVar0, i int iVar1 = Cec5_ObjGetCnfVar( p, iObj1 ); if( p->pPars->jType > 0 ) { - extern void glucose2_markapprox( void * pSat, int v0, int v1, int nlim ); int nlim = p->approxLim; - glucose2_markapprox( p->pSat, iVar0, iVar1, nlim ); + bmcg2_sat_solver_markapprox( p->pSat, iVar0, iVar1, nlim ); } * piVar0 = iVar0; diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp index c1d77587..99ca112a 100644 --- a/src/sat/glucose2/AbcGlucose2.cpp +++ b/src/sat/glucose2/AbcGlucose2.cpp @@ -132,6 +132,10 @@ void glucose2_solver_setstop(Gluco2::SimpSolver* S, int * pstop) S->pstop = pstop; } +void glucose2_markapprox( Gluco2::SimpSolver* S, int v0, int v1, int nlim ) +{ + S->markApprox(v0, v1, nlim); +} /**Function************************************************************* @@ -228,6 +232,11 @@ void bmcg2_sat_solver_set_stop(bmcg2_sat_solver* s, int * pstop) glucose2_solver_setstop((Gluco2::SimpSolver*)s, pstop); } +void bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim) +{ + glucose2_markapprox((Gluco2::SimpSolver*)s, v0, v1, nlim); +} + abctime bmcg2_sat_solver_set_runtime_limit(bmcg2_sat_solver* s, abctime Limit) { abctime nRuntimeLimit = ((Gluco2::SimpSolver*)s)->nRuntimeLimit; @@ -474,6 +483,11 @@ void glucose2_solver_setstop(Gluco2::Solver* S, int * pstop) S->pstop = pstop; } +void glucose2_markapprox( Gluco2::Solver* S, int v0, int v1, int nlim ) +{ + S->markApprox(v0, v1, nlim); +} + /**Function************************************************************* @@ -570,6 +584,11 @@ void bmcg2_sat_solver_set_stop(bmcg2_sat_solver* s, int * pstop) glucose2_solver_setstop((Gluco2::Solver*)s, pstop); } +void bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim) +{ + glucose2_markapprox((Gluco2::Solver*)s, v0, v1, nlim); +} + abctime bmcg2_sat_solver_set_runtime_limit(bmcg2_sat_solver* s, abctime Limit) { abctime nRuntimeLimit = ((Gluco2::Solver*)s)->nRuntimeLimit; @@ -1536,12 +1555,6 @@ int Glucose2_SolveAig(Gia_Man_t * p, Glucose2_Pars * pPars) return (ret == l_True ? 10 : ret == l_False ? 20 : 0); } -extern "C" { - void glucose2_markapprox( void * pSat, int v0, int v1, int nlim ){ - ((Gluco2::Solver*) pSat)->markApprox(v0, v1, nlim); - } -}; - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/glucose2/AbcGlucose2.h b/src/sat/glucose2/AbcGlucose2.h index 9299d290..d1c15639 100644 --- a/src/sat/glucose2/AbcGlucose2.h +++ b/src/sat/glucose2/AbcGlucose2.h @@ -86,6 +86,7 @@ extern int bmcg2_sat_solver_elim_varnum(bmcg2_sat_solver* s); extern int * bmcg2_sat_solver_read_cex( bmcg2_sat_solver* s ); extern int bmcg2_sat_solver_read_cex_varvalue( bmcg2_sat_solver* s, int ); extern void bmcg2_sat_solver_set_stop( bmcg2_sat_solver* s, int * pstop ); +extern void bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim); extern abctime bmcg2_sat_solver_set_runtime_limit( bmcg2_sat_solver* s, abctime Limit ); extern void bmcg2_sat_solver_set_conflict_budget( bmcg2_sat_solver* s, int Limit ); extern int bmcg2_sat_solver_varnum( bmcg2_sat_solver* s ); |