From 22388f901a88dddfe629dd3c1406b06fafa9675d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 13 Nov 2020 10:29:31 -0800 Subject: Adding and integrating new SAT solver APIs. --- src/sat/glucose/AbcGlucose.cpp | 83 ++++++++++++++++++++++++++++++++++++++++ src/sat/glucose/AbcGlucose.h | 6 +++ src/sat/glucose/Solver.h | 10 +++++ src/sat/glucose2/AbcGlucose2.cpp | 82 +++++++++++++++++++++++++++++++++++++++ src/sat/glucose2/AbcGlucose2.h | 5 +++ src/sat/glucose2/Solver.h | 10 +++++ 6 files changed, 196 insertions(+) (limited to 'src/sat') 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 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 user_vec; vec 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: diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp index 1e70a2b2..bbb1460a 100644 --- a/src/sat/glucose2/AbcGlucose2.cpp +++ b/src/sat/glucose2/AbcGlucose2.cpp @@ -326,6 +326,31 @@ int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVa return 1; } +int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s) +{ + return ((Gluco2::SimpSolver*)s)->jftr; +} + +void bmcg2_sat_solver_set_jftr(bmcg2_sat_solver* s, int jftr) +{ + ((Gluco2::SimpSolver*)s)->jftr = jftr; +} + +void bmcg2_sat_solver_set_var_fanin_lit(bmcg2_sat_solver* s, int var, int lit0, int lit1) +{ + ((Gluco2::SimpSolver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1); +} + +void bmcg2_sat_solver_start_new_round(bmcg2_sat_solver* s) +{ + ((Gluco2::SimpSolver*)s)->sat_solver_start_new_round(); +} + +void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var) +{ + ((Gluco2::SimpSolver*)s)->sat_solver_mark_cone(var); +} + #else /**Function************************************************************* @@ -351,6 +376,11 @@ void glucose2_solver_stop(Gluco2::Solver* S) delete S; } +void glucose2_solver_reset(Gluco2::Solver* S) +{ + S->reset(); +} + int glucose2_solver_addclause(Gluco2::Solver* S, int * plits, int nlits) { vec lits; @@ -427,6 +457,10 @@ void bmcg2_sat_solver_stop(bmcg2_sat_solver* s) { glucose2_solver_stop((Gluco2::Solver*)s); } +void bmcg2_sat_solver_reset(bmcg2_sat_solver* s) +{ + glucose2_solver_reset((Gluco2::Solver*)s); +} int bmcg2_sat_solver_addclause(bmcg2_sat_solver* s, int * plits, int nlits) { @@ -575,6 +609,54 @@ int bmcg2_sat_solver_minimize_assumptions( bmcg2_sat_solver * s, int * plits, in return nresL + nresR; } +int bmcg2_sat_solver_add_and( bmcg2_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 ( !bmcg2_sat_solver_addclause( s, Lits, 2 ) ) + return 0; + + Lits[0] = Abc_Var2Lit( iVar, !fCompl ); + Lits[1] = Abc_Var2Lit( iVar1, fCompl1 ); + if ( !bmcg2_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 ( !bmcg2_sat_solver_addclause( s, Lits, 3 ) ) + return 0; + + return 1; +} + +int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s) +{ + return ((Gluco2::Solver*)s)->jftr; +} + +void bmcg2_sat_solver_set_jftr(bmcg2_sat_solver* s, int jftr) +{ + ((Gluco2::Solver*)s)->jftr = jftr; +} + +void bmcg2_sat_solver_set_var_fanin_lit(bmcg2_sat_solver* s, int var, int lit0, int lit1) +{ + ((Gluco2::Solver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1); +} + +void bmcg2_sat_solver_start_new_round(bmcg2_sat_solver* s) +{ + ((Gluco2::Solver*)s)->sat_solver_start_new_round(); +} + +void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var) +{ + ((Gluco2::Solver*)s)->sat_solver_mark_cone(var); +} + #endif diff --git a/src/sat/glucose2/AbcGlucose2.h b/src/sat/glucose2/AbcGlucose2.h index 8fc774cd..28304e52 100644 --- a/src/sat/glucose2/AbcGlucose2.h +++ b/src/sat/glucose2/AbcGlucose2.h @@ -97,6 +97,11 @@ extern int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVa extern int bmcg2_sat_solver_quantify( bmcg2_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ); extern int bmcg2_sat_solver_equiv_overlap_check( bmcg2_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ); extern Vec_Str_t * bmcg2_sat_solver_sop( Gia_Man_t * p, int CubeLimit ); +extern int bmcg2_sat_solver_jftr( bmcg2_sat_solver * s ); +extern void bmcg2_sat_solver_set_jftr( bmcg2_sat_solver * s, int jftr ); +extern void bmcg2_sat_solver_set_var_fanin_lit( bmcg2_sat_solver * s, int var, int lit0, int lit1 ); +extern void bmcg2_sat_solver_start_new_round( bmcg2_sat_solver * s ); +extern void bmcg2_sat_solver_mark_cone( bmcg2_sat_solver * s, int var ); extern void Glucose2_SolveCnf( char * pFilename, Glucose2_Pars * pPars ); extern int Glucose2_SolveAig( Gia_Man_t * p, Glucose2_Pars * pPars ); diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h index 3beb60e0..d71d1be8 100644 --- a/src/sat/glucose2/Solver.h +++ b/src/sat/glucose2/Solver.h @@ -64,6 +64,12 @@ public: vec user_vec; vec 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: -- cgit v1.2.3