Experiments with SAT sweeping.

2 files changed, 20 insertions, 6 deletions

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 );