diff options
Diffstat (limited to 'src/sat/glucose2/AbcGlucose2.cpp')
| -rw-r--r-- | src/sat/glucose2/AbcGlucose2.cpp | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp index 23c904c8..9a8b97eb 100644 --- a/src/sat/glucose2/AbcGlucose2.cpp +++ b/src/sat/glucose2/AbcGlucose2.cpp @@ -99,15 +99,16 @@ void glucose2_solver_setcallback(Gluco2::SimpSolver* S, void * pman, int(*pfunc) int glucose2_solver_solve(Gluco2::SimpSolver* S, int * plits, int nlits) { - vec<Lit> lits; - for (int i=0;i<nlits;i++,plits++) - { - Lit p; - p.x = *plits; - lits.push(p); - } - Gluco2::lbool res = S->solveLimited(lits, 0); - return (res == l_True ? 1 : res == l_False ? -1 : 0); +// vec<Lit> lits; +// for (int i=0;i<nlits;i++,plits++) +// { +// Lit p; +// p.x = *plits; +// lits.push(p); +// } +// Gluco2::lbool res = S->solveLimited(lits, 0); +// return (res == l_True ? 1 : res == l_False ? -1 : 0); + return S->solveLimited(plits, nlits, 0); } int glucose2_solver_addvar(Gluco2::SimpSolver* S) @@ -383,6 +384,10 @@ void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var) ((Gluco2::SimpSolver*)s)->sat_solver_mark_cone(var); } +void bmcg2_sat_solver_prelocate( bmcg2_sat_solver * s, int var_num ){ + ((Gluco2::SimpSolver*)s)->prelocate(var_num); +} + #else /**Function************************************************************* @@ -721,6 +726,10 @@ void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var) ((Gluco2::Solver*)s)->sat_solver_mark_cone(var); } +void bmcg2_sat_solver_prelocate( bmcg2_sat_solver * s, int var_num ){ + ((Gluco2::Solver*)s)->prelocate(var_num); +} + #endif |