diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-06 18:43:15 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-06 18:43:15 -0700 |
commit | bd6d95fa2ca85c31137855af247b8d5e464be5b8 (patch) | |
tree | e71816ce4a3d3ed3a4a095336b4b7026a0e25550 /src/sat/glucose/AbcGlucose.cpp | |
parent | f68bd519c69dabfe0c507810d84d3289e082947e (diff) | |
download | abc-bd6d95fa2ca85c31137855af247b8d5e464be5b8.tar.gz abc-bd6d95fa2ca85c31137855af247b8d5e464be5b8.tar.bz2 abc-bd6d95fa2ca85c31137855af247b8d5e464be5b8.zip |
Renaming Glucose namespace to avoid collisions with external solvers.
Diffstat (limited to 'src/sat/glucose/AbcGlucose.cpp')
-rw-r--r-- | src/sat/glucose/AbcGlucose.cpp | 42 |
1 files changed, 21 insertions, 21 deletions
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index b5c6b592..8825b763 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -29,7 +29,7 @@ #include "aig/gia/gia.h" #include "sat/cnf/cnf.h" -using namespace Glucose; +using namespace Gluco; ABC_NAMESPACE_IMPL_START @@ -54,19 +54,19 @@ extern "C" { SeeAlso [] ***********************************************************************/ -Glucose::Solver * glucose_solver_start() +Gluco::Solver * glucose_solver_start() { Solver * S = new Solver; S->setIncrementalMode(); return S; } -void glucose_solver_stop(Glucose::Solver* S) +void glucose_solver_stop(Gluco::Solver* S) { delete S; } -int glucose_solver_addclause(Glucose::Solver* S, int * plits, int nlits) +int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits) { vec<Lit> lits; for ( int i = 0; i < nlits; i++,plits++) @@ -81,14 +81,14 @@ int glucose_solver_addclause(Glucose::Solver* S, int * plits, int nlits) return S->addClause(lits); // returns 0 if the problem is UNSAT } -void glucose_solver_setcallback(Glucose::Solver* S, void * pman, int(*pfunc)(void*, int, int*)) +void glucose_solver_setcallback(Gluco::Solver* S, void * pman, int(*pfunc)(void*, int, int*)) { S->pCnfMan = pman; S->pCnfFunc = pfunc; S->nCallConfl = 1000; } -int glucose_solver_solve(Glucose::Solver* S, int * plits, int nlits) +int glucose_solver_solve(Gluco::Solver* S, int * plits, int nlits) { vec<Lit> lits; for (int i=0;i<nlits;i++,plits++) @@ -97,22 +97,22 @@ int glucose_solver_solve(Glucose::Solver* S, int * plits, int nlits) p.x = *plits; lits.push(p); } - Glucose::lbool res = S->solveLimited(lits); + Gluco::lbool res = S->solveLimited(lits); return (res == l_True ? 1 : res == l_False ? -1 : 0); } -int glucose_solver_addvar(Glucose::Solver* S) +int glucose_solver_addvar(Gluco::Solver* S) { S->newVar(); return S->nVars() - 1; } -int glucose_solver_read_cex_varvalue(Glucose::Solver* S, int ivar) +int glucose_solver_read_cex_varvalue(Gluco::Solver* S, int ivar) { return S->model[ivar] == l_True; } -void glucose_solver_setstop(Glucose::Solver* S, int * pstop) +void glucose_solver_setstop(Gluco::Solver* S, int * pstop) { S->pstop = pstop; } @@ -155,54 +155,54 @@ bmcg_sat_solver * bmcg_sat_solver_start() } void bmcg_sat_solver_stop(bmcg_sat_solver* s) { - glucose_solver_stop((Glucose::Solver*)s); + glucose_solver_stop((Gluco::Solver*)s); } int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits) { - return glucose_solver_addclause((Glucose::Solver*)s,plits,nlits); + return glucose_solver_addclause((Gluco::Solver*)s,plits,nlits); } void bmcg_sat_solver_setcallback(bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*)) { - glucose_solver_setcallback((Glucose::Solver*)s,pman,pfunc); + glucose_solver_setcallback((Gluco::Solver*)s,pman,pfunc); } int bmcg_sat_solver_solve(bmcg_sat_solver* s, int * plits, int nlits) { - return glucose_solver_solve((Glucose::Solver*)s,plits,nlits); + return glucose_solver_solve((Gluco::Solver*)s,plits,nlits); } int bmcg_sat_solver_addvar(bmcg_sat_solver* s) { - return glucose_solver_addvar((Glucose::Solver*)s); + return glucose_solver_addvar((Gluco::Solver*)s); } int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar) { - return glucose_solver_read_cex_varvalue((Glucose::Solver*)s, ivar); + return glucose_solver_read_cex_varvalue((Gluco::Solver*)s, ivar); } void bmcg_sat_solver_setstop(bmcg_sat_solver* s, int * pstop) { - glucose_solver_setstop((Glucose::Solver*)s, pstop); + glucose_solver_setstop((Gluco::Solver*)s, pstop); } int bmcg_sat_solver_varnum(bmcg_sat_solver* s) { - return ((Glucose::Solver*)s)->nVars(); + return ((Gluco::Solver*)s)->nVars(); } int bmcg_sat_solver_clausenum(bmcg_sat_solver* s) { - return ((Glucose::Solver*)s)->nClauses(); + return ((Gluco::Solver*)s)->nClauses(); } int bmcg_sat_solver_learntnum(bmcg_sat_solver* s) { - return ((Glucose::Solver*)s)->nLearnts(); + return ((Gluco::Solver*)s)->nLearnts(); } int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s) { - return ((Glucose::Solver*)s)->conflicts; + return ((Gluco::Solver*)s)->conflicts; } /**Function************************************************************* |