diff options
Diffstat (limited to 'src/sat/glucose/AbcGlucose.h')
| -rw-r--r-- | src/sat/glucose/AbcGlucose.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h index e030293b..83ad8dcc 100644 --- a/src/sat/glucose/AbcGlucose.h +++ b/src/sat/glucose/AbcGlucose.h @@ -93,6 +93,8 @@ extern int bmcg_sat_solver_learntnum( bmcg_sat_solver* s ); extern int bmcg_sat_solver_conflictnum( bmcg_sat_solver* s ); extern int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot ); extern int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl ); +extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[2], Gia_Man_t * p, int iLit, int(*pFuncCiToKeep)(int), int fHash ); +extern int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ); extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars ); extern int Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars ); |