From 1abd0457abb9f522da48e24996545b155285bac9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 24 Apr 2022 10:25:46 -0700 Subject: Experiments with SAT sweeping. --- src/sat/glucose2/AbcGlucose2.cpp | 25 +++++++++++++++++++------ src/sat/glucose2/AbcGlucose2.h | 1 + 2 files changed, 20 insertions(+), 6 deletions(-) (limited to 'src/sat/glucose2') 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 ); -- cgit v1.2.3