diff options
Diffstat (limited to 'src/sat/glucose')
-rw-r--r-- | src/sat/glucose/AbcGlucose.cpp | 83 | ||||
-rw-r--r-- | src/sat/glucose/AbcGlucose.h | 6 | ||||
-rw-r--r-- | src/sat/glucose/Solver.h | 10 |
3 files changed, 99 insertions, 0 deletions
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index f6eada93..da6a3add 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -326,6 +326,32 @@ int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1 return 1; } +int bmcg_sat_solver_jftr(bmcg_sat_solver* s) +{ + return ((Gluco::SimpSolver*)s)->jftr; +} + +void bmcg_sat_solver_set_jftr(bmcg_sat_solver* s, int jftr) +{ + ((Gluco::SimpSolver*)s)->jftr = jftr; +} + +void bmcg_sat_solver_set_var_fanin_lit(bmcg_sat_solver* s, int var, int lit0, int lit1) +{ + ((Gluco::SimpSolver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1); +} + +void bmcg_sat_solver_start_new_round(bmcg_sat_solver* s) +{ + ((Gluco::SimpSolver*)s)->sat_solver_start_new_round(); +} + +void bmcg_sat_solver_mark_cone(bmcg_sat_solver* s, int var) +{ + ((Gluco::SimpSolver*)s)->sat_solver_mark_cone(var); +} + + #else /**Function************************************************************* @@ -351,6 +377,11 @@ void glucose_solver_stop(Gluco::Solver* S) delete S; } +void glucose_solver_reset(Gluco::Solver* S) +{ + S->reset(); +} + int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits) { vec<Lit> lits; @@ -427,6 +458,10 @@ void bmcg_sat_solver_stop(bmcg_sat_solver* s) { glucose_solver_stop((Gluco::Solver*)s); } +void bmcg_sat_solver_reset(bmcg_sat_solver* s) +{ + glucose_solver_reset((Gluco::Solver*)s); +} int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits) { @@ -575,6 +610,54 @@ int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int return nresL + nresR; } +int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl ) +{ + int Lits[3]; + + Lits[0] = Abc_Var2Lit( iVar, !fCompl ); + Lits[1] = Abc_Var2Lit( iVar0, fCompl0 ); + if ( !bmcg_sat_solver_addclause( s, Lits, 2 ) ) + return 0; + + Lits[0] = Abc_Var2Lit( iVar, !fCompl ); + Lits[1] = Abc_Var2Lit( iVar1, fCompl1 ); + if ( !bmcg_sat_solver_addclause( s, Lits, 2 ) ) + return 0; + + Lits[0] = Abc_Var2Lit( iVar, fCompl ); + Lits[1] = Abc_Var2Lit( iVar0, !fCompl0 ); + Lits[2] = Abc_Var2Lit( iVar1, !fCompl1 ); + if ( !bmcg_sat_solver_addclause( s, Lits, 3 ) ) + return 0; + + return 1; +} + +int bmcg_sat_solver_jftr(bmcg_sat_solver* s) +{ + return ((Gluco::Solver*)s)->jftr; +} + +void bmcg_sat_solver_set_jftr(bmcg_sat_solver* s, int jftr) +{ + ((Gluco::Solver*)s)->jftr = jftr; +} + +void bmcg_sat_solver_set_var_fanin_lit(bmcg_sat_solver* s, int var, int lit0, int lit1) +{ + ((Gluco::Solver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1); +} + +void bmcg_sat_solver_start_new_round(bmcg_sat_solver* s) +{ + ((Gluco::Solver*)s)->sat_solver_start_new_round(); +} + +void bmcg_sat_solver_mark_cone(bmcg_sat_solver* s, int var) +{ + ((Gluco::Solver*)s)->sat_solver_mark_cone(var); +} + #endif diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h index 026c22ee..02816131 100644 --- a/src/sat/glucose/AbcGlucose.h +++ b/src/sat/glucose/AbcGlucose.h @@ -97,6 +97,12 @@ extern int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ); extern int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ); extern Vec_Str_t * bmcg_sat_solver_sop( Gia_Man_t * p, int CubeLimit ); +extern int bmcg_sat_solver_jftr( bmcg_sat_solver * s ); +extern void bmcg_sat_solver_set_jftr( bmcg_sat_solver * s, int jftr ); +extern void bmcg_sat_solver_set_var_fanin_lit( bmcg_sat_solver * s, int var, int lit0, int lit1 ); +extern void bmcg_sat_solver_start_new_round( bmcg_sat_solver * s ); +extern void bmcg_sat_solver_mark_cone( bmcg_sat_solver * s, int var ); + extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars ); extern int Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars ); diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h index 43b13db7..3d7d26ea 100644 --- a/src/sat/glucose/Solver.h +++ b/src/sat/glucose/Solver.h @@ -64,6 +64,12 @@ public: vec<int> user_vec; vec<Lit> user_lits; + // circuit-based solving + int jftr; + void sat_solver_set_var_fanin_lit(int, int, int); + void sat_solver_start_new_round(); + void sat_solver_mark_cone(int); + // Problem specification: // Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. @@ -457,6 +463,10 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ v inline void Solver::addVar(Var v) { while (v >= nVars()) newVar(); } +inline void Solver::sat_solver_set_var_fanin_lit(int var, int lit0, int lit1) {} +inline void Solver::sat_solver_start_new_round() {} +inline void Solver::sat_solver_mark_cone(int var) {} + //================================================================================================= // Debug etc: |